module author Paolo Masci
 *  date copyright import { spawn , ChildProcess , execSync } from 'child_process' ; import { PvsVersionDescriptor , SimpleConnection } from '../common/serverInterface' ; import * as path from 'path' ; import * as fsUtils from '../common/fsUtils' ; /**
 * Wrapper class for PVS: spawns a PVS process, and exposes the PVS REPS interface as an asyncronous server.
 * This eay of interacting with PVS emulates what the Emacs interface does
 */ export class PvsProcessLegacy { 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 connection : SimpleConnection ; param msg protected error ( msg ) { if ( msg ) { if ( this . connection ) { this . connection . sendNotification ( 'pvs-error' , msg ) ; } console . log ( '[pvs-process-legacy] pvs-error' , msg ) ; } } constructor param desc param connection constructor ( desc , connection ? ) { this . pvsPath = ( desc && desc . pvsPath ) ? fsUtils . tildeExpansion ( desc . pvsPath ) : __dirname ; this . pvsLibraryPath = path . join ( this . pvsPath , "lib" ) ; this . connection = connection ; } getData ( ) { return this . data ; } resetData ( ) { this . data = "" ; } param data async sendText ( data ) { return new Promise ( ( resolve , reject ) => { this . cb = ( data ) => { resolve ( data ) ; } ; this . resetData ( ) ; this . pvsProcess . stdin . write ( data ) ; } ) ; } /**
     * Sends the quit command (followed by a confirmation) to PVSio
     */ quit ( ) { this . pvsProcess . stdin . write ( "exit; Y" ) ; } returns async activate ( ) { return new Promise ( async ( resolve , reject ) => { if ( this . pvsProcess ) { return Promise . resolve ( true ) ; } const pvsExecutable = path . join ( this . pvsPath , "pvs" ) ; const args = [ `-raw` ] ; console . info ( `${ pvsExecutable } ${ args . join ( " " ) }` ) ; const fileExists = await fsUtils . fileExists ( pvsExecutable ) ; if ( fileExists && ! this . pvsProcess ) { this . pvsProcess = spawn ( pvsExecutable , args ) ; this . pvsProcess . stdout . setEncoding ( "utf8" ) ; this . pvsProcess . stderr . setEncoding ( "utf8" ) ; this . pvsProcess . stdout . on ( "data" , ( data ) => { this . connection . console . log ( data ) ; this . data += data ; const match = /\bpvs\(\d+\)\s*:/g . exec ( data ) ; if ( match && match [ 0 ] ) { if ( ! this . ready ) { this . ready = true ; resolve ( true ) ; } if ( this . cb && typeof this . cb === "function" ) { const res = this . data . replace ( /\bpvs\(\d+\)\s*:/g , "" ) ; this . cb ( res . trim ( ) ) ; } } } ) ; this . pvsProcess . stdin . on ( "data" , ( data ) => { console . log ( "stdin" , data ) ; } ) ; this . pvsProcess . stderr . on ( "data" , ( data ) => { console . log ( "[pvs-process-legacy] Error: " + data ) ; this . error ( data ) ; } ) ; this . pvsProcess . on ( "error" , ( err ) => { console . log ( "[pvs-process-legacy] Process error" ) ; } ) ; this . pvsProcess . on ( "exit" , ( code , signal ) => { console . log ( "[pvs-process-legacy] Process exited" ) ; } ) ; this . pvsProcess . on ( "message" , ( message ) => { console . log ( "[pvs-process-legacy] Process message" ) ; } ) ; } else { console . log ( `\n>>> PVS executable not found at ${ pvsExecutable } <<<\n` ) ; resolve ( false ) ; } } ) ; } returns protected getProcessID ( ) { if ( this . pvsProcess && ! isNaN ( this . pvsProcess . pid ) ) { return this . pvsProcess . pid . toString ( ) ; } return null ; } returns async kill ( ) { return new Promise ( ( resolve , reject ) => { if ( this . pvsProcess ) { const pvs_shell = this . getProcessID ( ) ; this . pvsProcess . stdin . destroy ( ) ; try { execSync ( `kill -9 ${ pvs_shell }` ) ; this . pvsProcess . on ( "close" , ( code , signal ) => { console . log ( "[pvs-process] Process terminated" ) ; resolve ( true ) ; } ) ; } catch ( kill_error ) { console . log ( `[pvsProcess] Warning: Could not kill process id ${ pvs_shell }.` ) ; resolve ( false ) ; } finally { this . pvsProcess = null ; } } else { resolve ( true ) ; } } ) ; } }