module author Paolo Masci
 *  date copyright import { spawn , ChildProcess } from 'child_process' ; import { PvsVersionDescriptor , SimpleConnection } from './common/serverInterface' ; import * as path from 'path' ; import * as fsUtils from './common/fsUtils' ; import { PvsErrorManager } from './pvsErrorManager' ; import { forceLocale } from './common/languageUtils' ; const MAX_LOG_CHUNK = 600 ; export enum ProcessCode { SUCCESS = 0 , PVSNOTFOUND = - 1 , ADDRINUSE = - 2 , COMMFAILURE = - 3 , PVSSTARTFAIL = - 4 , PVSERROR = - 5 , UNSUPPORTEDPLATFORM = - 6 } ; /**
 * Wrapper class for PVS: spawns a PVS process, and exposes the PVS Lisp interface as an asyncronous JSON/RPC server.
 */ export class PvsProcess { protected pvsProcess : ChildProcess = null ; protected pvsVersionInfo : PvsVersionDescriptor ; protected pvsPath : string = null ; protected pvsLibraryPath : string = null ; protected ready : boolean = false ; protected data : string = "" ; protected cb : ( data : string ) => void ; protected buffer : Promise < string > = Promise . resolve ( "" ) ; protected connection : SimpleConnection ; protected enableNotifications : boolean ; protected pvsErrorManager : PvsErrorManager ; protected serverPort : number = 22334 ; protected externalServer : boolean = false ; protected verbose : boolean = false ; protected progressInfoEnabled : boolean = false ; protected verboseLog : boolean = false ; param msg protected error ( msg ) { if ( msg ) { if ( this . connection && this . enableNotifications ) { this . connection . sendNotification ( 'pvs-error' , msg ) ; } else { console . log ( msg ) ; } } } protected warn ( msg ) { if ( msg ) { if ( this . connection && this . connection . console ) { this . connection . console . warn ( msg ) ; } else { console . warn ( msg ) ; } } } protected log ( msg , opt ? ) { opt = opt || { } ; if ( msg && ( this . verbose || opt . force ) ) { if ( ! msg . startsWith ( "127.0.0.1" ) && ! msg . startsWith ( "emacs does not support X;" ) ) { if ( this . connection && this . connection . console ) { this . connection . console . log ( msg ) ; if ( this . progressInfoEnabled ) { const ln = msg . trim ( ) . split ( "\n" ) . filter ( line => { return line . trim ( ) && ! line . includes ( "pvs(" ) && ! ( line . trim ( ) === "nil" ) ; } ) ; this . sendProgressInfo ( ln [ ln . length - 1 ] ) ; } } else { console . log ( msg ) ; } } } } protected sendProgressInfo ( msg ) { if ( msg ) { this . connection ?. sendNotification ( "pvs.progress-info" , msg ) ; } } constructor param desc param connection constructor ( pvsPath , opt ? ) { opt = opt || { } ; this . pvsPath = pvsPath ? fsUtils . tildeExpansion ( pvsPath ) : __dirname ; this . pvsLibraryPath = path . join ( this . pvsPath , "lib" ) ; this . connection = opt . connection ; this . pvsErrorManager = opt . pvsErrorManager ; } /**
     * Utility function, sets the log level
     */ logLevel ( l ) { this . verboseLog = l === "verbose" ; } /**
     * Internal function. Runs the relocate script necessary for starting pvs.
     */ param opt returns async activate ( opt ? ) { if ( this . pvsProcess ) { return ProcessCode . SUCCESS ; } if ( ! this . pvsPath ) { return ProcessCode . PVSNOTFOUND ; } opt = opt || { } ; this . enableNotifications = ! ! opt . enableNotifications ; this . externalServer = ! ! opt . externalServer ; this . verbose = ! ! opt . verbose ; this . serverPort = opt . serverPort || 22334 ; forceLocale ( ) ; const pvs = path . join ( this . pvsPath , "pvs" ) ; const args = opt . externalServer ? [ "-raw" ] : [ "-raw" , "-port" , `${ this . serverPort }` ] ; console . info ( `${ this . pvsPath }/pvs ${ args . join ( " " ) }` ) ; const fileExists = fsUtils . fileExists ( pvs ) ; if ( fileExists ) { let addressInUse = false ; return await new Promise ( ( resolve , reject ) => { if ( this . pvsProcess ) { return resolve ( ProcessCode . SUCCESS ) ; } this . pvsProcess = spawn ( pvs , args ) ; this . pvsProcess . stdout . setEncoding ( "utf8" ) ; this . pvsProcess . stderr . setEncoding ( "utf8" ) ; this . pvsProcess . stdout . on ( "data" , async ( data ) => { if ( addressInUse ) { return ; } this . ready = false ; this . data += data ; this . log ( data ?. length > MAX_LOG_CHUNK && ! this . verboseLog ? data . substr ( 0 , MAX_LOG_CHUNK ) + "\n\n...\n\n" : data ) ; const matchSocketAddressInUse = /(errno 48)/g . exec ( data ) ; if ( matchSocketAddressInUse ) { this . pvsProcess = null ; addressInUse = true ; resolve ( ProcessCode . ADDRINUSE ) ; return ; } const matchNoExecutable = /No executable available in (.+)/gi . exec ( data ) ; if ( matchNoExecutable ) { this . pvsProcess = null ; resolve ( ProcessCode . UNSUPPORTEDPLATFORM ) ; return ; } const yesNoQuery = data . trim ( ) . endsWith ( "(Yes or No)" ) ; if ( yesNoQuery ) { console . log ( data ) ; if ( ! this . pvsProcess ?. stdin ?. destroyed ) { this . pvsProcess ?. stdin ?. write ( "Yes\n" ) ; this . log ( "Yes\n" , { force : true } ) ; } return ; } const matchPvsPrompt = /(?:\[\d+\w*\])?\s+pvs\(\d+\)\s*:/g . exec ( data ) ; const matchProverPrompt = /\bRule\?/g . exec ( data ) ; if ( matchPvsPrompt || matchProverPrompt ) { if ( ! this . ready ) { this . ready = true ; resolve ( ProcessCode . SUCCESS ) ; } if ( this . cb && typeof this . cb === "function" ) { let res = this . data . replace ( /(?:\[\d+\w*\])?\s+pvs\(\d+\)\s*:/g , "" ) . replace ( /\bRule\?/g , "" ) ; res = res . replace ( "[Current process: Initial Lisp Listener]" , "" ) ; this . cb ( res . trim ( ) ) ; } } } ) ; this . pvsProcess . stderr . on ( "data" , ( data ) => { this . error ( data ) ; console . dir ( data , { depth : null } ) ; } ) ; this . pvsProcess . on ( "error" , ( err ) => { this . error ( "[pvs-process] Process error" ) ; console . dir ( err , { depth : null } ) ; } ) ; this . pvsProcess . on ( "exit" , ( code , signal ) => { this . log ( "[pvs-process] Process exited" ) ; console . dir ( { code , signal } ) ; } ) ; this . pvsProcess . on ( "message" , ( message ) => { this . log ( "[pvs-process] Process message" ) ; console . dir ( message , { depth : null } ) ; } ) ; } ) ; } else { this . error ( `\n>>> PVS executable not found at ${ pvs } <<<\n` ) ; return ProcessCode . PVSNOTFOUND ; } } returns async kill ( ) { return new Promise ( async ( resolve , reject ) => { if ( this . pvsProcess ) { let done = false ; const pid = this . getProcessID ( ) ; this . pvsProcess . on ( "close" , ( code , signal ) => { console . log ( "[pvs-process] Process terminated" ) ; this . ready = false ; this . pvsProcess = null ; done = true ; resolve ( true ) ; } ) ; this . pvsProcess . on ( "error" , ( code , signal ) => { console . log ( "[pvs-process] Process terminated" ) ; this . ready = false ; resolve ( true ) ; } ) ; try { if ( this . pvsProcess ) { await new Promise ( ( resolveExit , rejectExit ) => { if ( ! this . pvsProcess ?. stdin ?. destroyed ) { this . pvsProcess ?. stdin ?. write ( "(quit)Y\n" ) ; } setTimeout ( ( ) => { if ( ! done ) { resolveExit ( true ) ; } } , 400 ) ; } ) ; } else { process ?. kill ( pid , "SIGKILL" ) ; } } finally { this . pvsProcess = null ; if ( ! done ) { resolve ( true ) ; } } } else { resolve ( true ) ; } } ) ; } returns protected getProcessID ( ) { if ( this . pvsProcess && ! isNaN ( this . pvsProcess . pid ) ) { return this . pvsProcess . pid ; } return null ; } public async clearContext ( contextFolder ? ) { } param cmd async sendText ( cmd ) { this . buffer = this . buffer . then ( ( ) => { return new Promise ( ( resolve , reject ) => { this . cb = ( data ) => { resolve ( data ) ; } ; this . data = "" ; if ( this . pvsProcess && this . pvsProcess . stdin && ! this . pvsProcess . stdin . destroyed ) { this . progressInfoEnabled = cmd . includes ( "typecheck-file" ) ; this . pvsProcess ?. stdin ?. write ( cmd ) ; this . log ( cmd + "\n" ) ; } } ) ; } ) ; return this . buffer ; } /**
     * Sends the quit command (followed by a confirmation) to the Emacs REPL of PVS
     */ quit ( ) { this . pvsProcess ?. stdin ?. write ( "exit; Y" ) ; } /**
     * returns the current output of the process
     */ getLispInterfaceOutput ( ) { return this . data || "" ; } /**
     * Clears the current lisp output
     */ clearLispInterfaceOutput ( ) { this . data = "" ; } }