module author Paolo Masci
 *  date copyright import { execSync } from "child_process" ; import { Connection } from "vscode-languageserver" ; import { PvsLanguageServer } from "../pvsLanguageServer" ; import { SearchResult } from "../common/serverInterface" ; import * as fsUtils from "../common/fsUtils" ; import * as path from 'path' ; import * as colorUtils from '../common/colorUtils' ; export class PvsSearchEngine { protected connection : Connection ; protected pvsLanguageServer : PvsLanguageServer ; constructor ( connection , pvsLanguageServer ) { this . connection = connection ; this . pvsLanguageServer = pvsLanguageServer ; } async searchNasalib ( searchString ) { if ( searchString ) { const nasalibPath = this . pvsLanguageServer . getNasalibPath ( ) ; const normalizedSearchString = searchString . replace ( /\|/g , "\\|" ) ; const findAll = `cd ${ nasalibPath } && ./find-all "${ normalizedSearchString }"` ; console . log ( `[pvs-search-engine] ${ findAll }` ) ; process . env [ "PVS_DIR" ] = this . pvsLanguageServer . getPvsPath ( ) ; process . env [ "PVS_LIBRARY_PATH" ] = nasalibPath ; const search = execSync ( findAll ) ; if ( search ) { const res = [ ] ; const ans = search . toLocaleString ( ) ; if ( colorUtils . isPlainText ( ans ) ) { const txt = ans ; const matchContent = /\*\*\*[\w\W\n]+/g . exec ( txt ) ; if ( matchContent ) { const elems = matchContent [ 0 ] . split ( "***" ) ; for ( let i = 0 ; i < elems . length ; i ++ ) { const subfolderInfo = elems [ i ] . trim ( ) . split ( "\n" ) ; if ( subfolderInfo && subfolderInfo . length > 1 ) { const subfolder = subfolderInfo [ 0 ] . trim ( ) ; for ( let j = 1 ; j < subfolderInfo . length ; j ++ ) { const data = subfolderInfo [ j ] ; const sep = data . indexOf ( ":" ) ; const fname = data . substring ( 0 , sep ) ; let content = data . substring ( sep + 1 ) ; let line = 1 ; const matchLine = /\s*(\d+)\:([\w\W\s]+)/g . exec ( content ) ; if ( matchLine && matchLine . length > 2 ) { content = matchLine [ 2 ] ; line = + matchLine [ 1 ] ; } const searchResult = { fileName : fsUtils . getFileName ( fname ) , fileExtension : fsUtils . getFileExtension ( fname ) , contextFolder : path . join ( nasalibPath , subfolder ) , fileContent : content , line } ; res . push ( searchResult ) ; } } } } } else { let txt = colorUtils . getPlainText ( ans ) ; txt = txt . replace ( /.*\s+Finding\.\.\.\s*\[NOT FOUND\]\s/g , "" ) ; const regex = new RegExp ( /.*\s+Finding\.\.\.\s*\[FOUND\]\s/g ) ; const boundaries = [ ] ; let matchContent = null ; while ( matchContent = regex . exec ( txt ) ) { if ( matchContent . length && matchContent [ 0 ] ) { boundaries . push ( { from : boundaries . length ? boundaries [ boundaries . length - 1 ] . to : 0 , to : matchContent . index } ) ; } } boundaries . push ( { from : boundaries . length ? boundaries [ boundaries . length - 1 ] . to : 0 , to : txt . length } ) ; for ( let i = 0 ; i < boundaries . length ; i ++ ) { const info = txt . substring ( boundaries [ i ] . from , boundaries [ i ] . to ) ; const match = /(.*)\s+Finding\.\.\.\s*\[FOUND\]\s([\w\W\s]+)/g . exec ( info ) ; if ( match && match . length > 2 && match [ 1 ] && match [ 2 ] ) { const subfolder = match [ 1 ] . trim ( ) ; const data = match [ 2 ] . trim ( ) ; const lines = data . split ( "\n" ) ; for ( let l in lines ) { const sep = lines [ l ] . indexOf ( ":" ) ; const fname = lines [ l ] . substring ( 0 , sep ) ; let content = lines [ l ] . substring ( sep + 1 ) ; let line = 1 ; const matchLine = /\s*(\d+)\:([\w\W\s]+)/g . exec ( content ) ; if ( matchLine && matchLine . length > 2 ) { content = matchLine [ 2 ] ; line = + matchLine [ 1 ] ; } if ( content && line && fsUtils . fileExists ( path . join ( nasalibPath , subfolder , fname ) ) ) { const searchResult = { fileName : fsUtils . getFileName ( fname ) , fileExtension : fsUtils . getFileExtension ( fname ) , contextFolder : path . join ( nasalibPath , subfolder ) , fileContent : content , line } ; res . push ( searchResult ) ; } } } } } return res ; } } return null ; } }