From 87a429fee730350b1a8c5ec233ad861a4c6f0ee2 Mon Sep 17 00:00:00 2001 From: Ikutania Date: Thu, 28 Jul 2022 21:21:42 -0400 Subject: [PATCH] Bug Fixes, Edits, and Updates Fixed: Issue #26, #25, #23, #19 Refactored and reduced Placed Debug keys into a single object --- demos/01/.sa4u.json | 4 - lsp/client/src/extension.ts | 5 +- lsp/package.json | 47 ++++++- lsp/server/src/server.ts | 269 ++++++++++++++++++++---------------- sa4u_z3/main.py | 5 + 5 files changed, 206 insertions(+), 124 deletions(-) delete mode 100644 demos/01/.sa4u.json diff --git a/demos/01/.sa4u.json b/demos/01/.sa4u.json deleted file mode 100644 index 78e0a46..0000000 --- a/demos/01/.sa4u.json +++ /dev/null @@ -1,4 +0,0 @@ -{ - "ProtocolDefinitionFile": "CMASI.xml", - "CompilationDir": "compile_commands_dir" -} diff --git a/lsp/client/src/extension.ts b/lsp/client/src/extension.ts index 24a1405..b91ea86 100644 --- a/lsp/client/src/extension.ts +++ b/lsp/client/src/extension.ts @@ -55,9 +55,12 @@ export function activate(context: ExtensionContext) { ); client.onReady().then(() => { - client.onNotification("ServerError", (output: string) => { + client.onNotification('ServerError', (output: string) => { window.showErrorMessage(output); }); + client.onNotification('UpdateConfig', (config: {param:string, value:string}) => { + workspace.getConfiguration().update(config.param, config.value); + }); }); // Start the client. This will also launch the server diff --git a/lsp/package.json b/lsp/package.json index 2bba878..1faf81d 100644 --- a/lsp/package.json +++ b/lsp/package.json @@ -25,11 +25,54 @@ "type": "object", "title": "SA4U", "properties": { - "SA4U.messageDefinition": { + "SA4U.MessageDefinition": { "scope": "resource", "type": "string", "default": "CMASI.xml", - "description": "Message Description XML." + "description": "Message Description XML.", + "order": 1 + }, + "SA4U.PriorTypes": { + "scope": "resource", + "type": "string", + "defualt": "compile_commands_dir", + "description": "SA4U prior types file", + "order": 3 + }, + "SA4U.IgnoreFiles": { + "scope": "resource", + "type": "string", + "editPresentation": "multilineText", + "description": "List of file paths in the directory to ignore. Expected input is /RelativeFilePath/File or AbsoluteFilePath/File", + "order": 4 + }, + "SA4U.CompilationDir": { + "scope": "resource", + "type": "string", + "defualt": "compile_commands_dir", + "description": "SA4U compile commands directory", + "order": 2 + }, + "SA4U.DebugMode": { + "scope": "resource", + "type": "boolean", + "default": false, + "description": "Debug Mode for Developing SA4U", + "order": 20 + }, + "SA4U.DebugModeDockerImage": { + "scope": "resource", + "type": "string", + "default": "", + "description": "SA4U image to use in debug mode.", + "order": 21 + }, + "SA4U.DebugModeMaintainContainerOnExit": { + "scope": "resource", + "type": "boolean", + "default": false, + "description": "Setup the container to remain after exiting", + "order": 21 } } } diff --git a/lsp/server/src/server.ts b/lsp/server/src/server.ts index 63afeec..8068402 100644 --- a/lsp/server/src/server.ts +++ b/lsp/server/src/server.ts @@ -23,7 +23,7 @@ import { TextDocument } from 'vscode-languageserver-textdocument'; import { exec, execSync } from 'child_process'; import { promisify } from 'util'; -import { existsSync, promises } from 'fs'; +import { promises } from 'fs'; // Create a connection for the server, using Node's IPC as a transport. // Also include all preview / proposed LSP features. const connection = createConnection(ProposedFeatures.all); @@ -32,32 +32,82 @@ const connection = createConnection(ProposedFeatures.all); const documents: TextDocuments = new TextDocuments(TextDocument); // Docker image to use for analysis. -const dockerImageName = "sa4u/sa4u:0.7.0"; +const dockerImageName = 'sa4u/sa4u:0.7.0'; + +// Location of config file +const CONFIG_FILE = '.sa4u/config.json'; let hasConfigurationCapability = false; let hasWorkspaceFolderCapability = false; -let messDef: string; let allowConfigurationChanges = false; let startedSA4U_Z3 = false; +// Debug Mode Variables +let maintainContainerOnExit = false; + const execAsync = promisify(exec); -class SA4UConfig { - compilationDir: string - constructor(compilationDir: string) { - this.compilationDir = '/src/' + compilationDir; +class SA4UDebug { + Image: string; + MaintainContainerOnExit: boolean; + constructor(image:string, maintainOnExit:boolean) { + this.Image = image; + this.MaintainContainerOnExit = maintainOnExit; } } -class SA4UIgnoredFiles { - ignoreFilesCommand: string - constructor(ignoreFilesArray: string[]) { - if (ignoreFilesArray.length !== 0) { - this.ignoreFilesCommand = '-i '.concat(ignoreFilesArray.join(' -i ')); +class SA4UConfig { + ProtocolDefinitionFile: string; + CompilationDir: string; + PriorTypes: string; + IgnoreFiles: string[]; + Debug?:SA4UDebug; + constructor(config: any) { + if (config !== '') { + this.ProtocolDefinitionFile = config.MessageDefinition || config.ProtocolDefinitionFile; + this.CompilationDir = config.CompilationDir; + this.PriorTypes = config.PriorTypes; + if (typeof config.IgnoreFiles === 'string') { + if (config.IgnoreFiles.replace(/\s/g, '') !== '') { + this.IgnoreFiles = config.IgnoreFiles.split('\n'); + } else { + this.IgnoreFiles = []; + } + } else { + this.IgnoreFiles = config.IgnoreFiles || []; + } + if (config.DebugMode === true || config.Debug) { + this.Debug = new SA4UDebug(config.DebugModeDockerImage || config.Debug?.Image, config.DebugModeMaintainContainerOnExit || config.Debug?.MaintainContainerOnExit); + } } else { - this.ignoreFilesCommand = ''; + this.ProtocolDefinitionFile = ''; + this.CompilationDir = ''; + this.PriorTypes = ''; + this.IgnoreFiles = []; } - } + } + updateVSCodeConfig(): void { + connection.sendNotification('UpdateConfig', { param: 'SA4U.MessageDefinition', value: this.ProtocolDefinitionFile }); + connection.sendNotification('UpdateConfig', { param: 'SA4U.CompilationDir', value: this.CompilationDir }); + connection.sendNotification('UpdateConfig', { param: 'SA4U.PriorTypes', value: this.PriorTypes }); + connection.sendNotification('UpdateConfig', { param: 'SA4U.IgnoreFiles', value: this.IgnoreFiles?.join('\n') || '' }); + if (this.Debug) { + connection.sendNotification('UpdateConfig', { param: 'SA4U.DebugMode', value: true }); + connection.sendNotification('UpdateConfig', { param: 'SA4U.DebugModeDockerImage', value: this.Debug.Image }); + connection.sendNotification('UpdateConfig', { param: 'SA4U.DebugModeMaintainContainerOnExit', value: this.Debug.MaintainContainerOnExit }); + } + } + async writeToJSON(): Promise { + try { + await promises.writeFile(CONFIG_FILE, JSON.stringify(this, null, ' ')); + } catch (err) { + console.warn(`Failed to write to ${CONFIG_FILE}: ${err}`); + } + } + returnParameters(folder: WorkspaceFolder): string { + const path = getPath(folder, true); + return `${(this.Debug?.MaintainContainerOnExit) ? '' : '--rm '}--mount type=bind,source="${path}",target="/src/" --name sa4u_z3_server_${path.replace(/([^A-Za-z0-9]+)/g, '')} ${this.Debug?.Image ?? dockerImageName} -d True -c "/src/${this.CompilationDir}" ${(this.IgnoreFiles.length === 0) ? '' : '-i '.concat(this.IgnoreFiles.join(' -i '))} -p /src/${this.PriorTypes} -m /src/${this.ProtocolDefinitionFile} --serialize-analysis /src/.sa4u/cache`; + } } async function checkForDockerRunningAndInstalled(): Promise { @@ -74,42 +124,82 @@ async function startDockerContainer() { } } -async function stopDockerContainer(): Promise { +async function restartDockerContainer(): Promise { + if (startedSA4U_Z3) { + startedSA4U_Z3 = false; + const folders = await connection.workspace.getWorkspaceFolders(); + if (folders) { + folders.forEach(async (folder) => { + const path = getPath(folder); + try { + await execAsync(`docker container stop sa4u_z3_server_${path}`); + } catch (err) { + console.log(`Failed to stop the docker container: ${err}`); + } + try { + await execAsync(`docker container rm sa4u_z3_server_${path}`); + } catch (err) { + console.log(`Failed to remove a stopped docker container: ${err}`); + } + dockerContainer(folder); + }); + } + } +} + +async function stopAndRemoveDockerContainer(): Promise { let container_ids; try { - container_ids = (await execAsync(`docker container ls -q -f name=sa4u_z3_server`)).stdout.split('\n').join(' '); + container_ids = (await execAsync(`docker container ls -a -q -f name=sa4u_z3_server`)).stdout.split('\n').join(' '); await execAsync(`docker container stop ${container_ids}`); } catch (err) { console.log(err); } + try { + await execAsync(`docker container rm ${container_ids}`); + } catch (err) { + console.log(`Failed to remove a stopped docker container: ${err}`); + } } -async function getSA4UConfig(): Promise { +async function validateTextDocument(textDocument: TextDocument): Promise { + const folders = await connection.workspace.getWorkspaceFolders(); + if (folders) { + folders.forEach(async (folder) => { + const path = getPath(folder); + try { + await execAsync(`docker container kill -s=HUP sa4u_z3_server_${path}`); + } catch (err) { + console.warn(`Failed to send HUP signal to the contianer: ${err}`); + } + }); + } +} + +async function getConfig() { let readConfig: string; try { - readConfig = (await promises.readFile('.sa4u.json')).toString(); + readConfig = (await promises.readFile(CONFIG_FILE)).toString(); } catch (err) { - console.warn('unable to read SA4U config: ' + err); - return new SA4UConfig(''); + throw `Unable to read ${CONFIG_FILE}: ${err}`; } let configJSON; try { configJSON = JSON.parse(readConfig); } catch (err) { - console.warn(`Failed to parse .sa4u.json as a JSON: ${err}`); - return new SA4UConfig(''); + throw `Failed to parse ${CONFIG_FILE} as a JSON: ${err}`; } - if (configJSON['CompilationDir'] === undefined) { + return configJSON; +} + +async function getSA4UConfig(): Promise { + let configJSON; + try { + configJSON = await getConfig(); + } catch (err) { + console.warn(`${err}`); return new SA4UConfig(''); } - if (!existsSync('.sa4u')){ - try { - await promises.mkdir('.sa4u'); - } catch (err) { - console.warn(`Failed to create .sa4u directory: ${err}`); - return new SA4UConfig(configJSON['CompilationDir']); - } - } const directory = resolve('./'); let readCompileCommands; try { @@ -120,52 +210,42 @@ async function getSA4UConfig(): Promise { } try { await promises.writeFile('.sa4u/compile_commands.json', readCompileCommands); - return new SA4UConfig('.sa4u/'); + configJSON['CompilationDir'] = '.sa4u/'; + return new SA4UConfig(configJSON); } catch (err) { console.warn(`Failed to write compile_commands.json into .sa4u directory: ${err}`); - return new SA4UConfig(configJSON['CompilationDir']); + return new SA4UConfig(configJSON); } } -async function getIgnoredFiles(): Promise { - let readConfig: string; - try { - readConfig = (await promises.readFile('.sa4u.json')).toString(); - } catch (err) { - console.warn('unable to read SA4U config: ' + err); - return new SA4UIgnoredFiles([]); +async function updateConfigurations(): Promise { + if (!(await promises.stat('.sa4u'))){ + try { + await promises.mkdir('.sa4u'); + } catch (err) { + console.warn(`Failed to create .sa4u directory: ${err}`); + } + } + if (!(await promises.stat(CONFIG_FILE))) { + const sa4uJSON = new SA4UConfig(await connection.workspace.getConfiguration('SA4U')); + await sa4uJSON.writeToJSON(); } - let configJSON; try { - configJSON = JSON.parse(readConfig); - if (configJSON['IgnoreFiles'] === undefined) { - return new SA4UIgnoredFiles([]); - } - return new SA4UIgnoredFiles(configJSON['IgnoreFiles']); + const sa4uJSON = new SA4UConfig(await getConfig()); + maintainContainerOnExit = sa4uJSON.Debug?.MaintainContainerOnExit || false; + sa4uJSON.updateVSCodeConfig(); } catch (err) { - console.warn(`Failed to parse .sa4u.json as a JSON: ${err}`); - return new SA4UIgnoredFiles([]); + console.warn(`${err}`); } } -async function updateMessageDefinitionFromFile(): Promise { - try { - const readFile = (await promises.readFile('.sa4u.json')).toString(); - const configJSON = JSON.parse(readFile); - messDef = (configJSON['ProtocolDefinitionFile']?configJSON['ProtocolDefinitionFile']:''); - } catch (err) { - console.warn(`Failed to read .sa4u.json: ${err}`); - } - if (messDef == '') { - const config = await connection.workspace.getConfiguration('SA4U'); - if (config.messageDefinition) - messDef = config.messageDefinition; - } +async function changedConfiguration(change: DidChangeConfigurationParams): Promise { + await (new SA4UConfig(change.settings.SA4U)).writeToJSON(); + restartDockerContainer(); } async function dockerContainer(folder: WorkspaceFolder): Promise { const filePath = decodeURIComponent(folder.uri); - const path = getPath(folder, true); const diagnosticsMap = new Map(); try { // eslint-disable-next-line @typescript-eslint/no-var-requires @@ -229,9 +309,8 @@ async function dockerContainer(folder: WorkspaceFolder): Promise { } } }; - const sa4uConfig = await Promise.all([getSA4UConfig(), getIgnoredFiles()]).then((value) => {return {compilationDir: value[0].compilationDir, ignore: value[1].ignoreFilesCommand};}); - console.log(`using compile dir: ${sa4uConfig.compilationDir}`); - const child = exec(`docker container run --rm --mount type=bind,source="${path}",target="/src/" --name sa4u_z3_server_${path.replace(/([^A-Za-z0-9]+)/g, '')} ${dockerImageName} -d True -c "${sa4uConfig.compilationDir}" ${sa4uConfig.ignore} -p /src/ex_prior.json -m /src/${messDef}`); + const sa4uConfig = await getSA4UConfig(); + const child = exec(`docker container run ${sa4uConfig.returnParameters(folder)}`); const rl = readline.createInterface({input: child.stdout}); rl.on('line', (line: any) => { console.log(line); @@ -250,51 +329,6 @@ async function dockerContainer(folder: WorkspaceFolder): Promise { } } -async function changedConfiguration(change: DidChangeConfigurationParams): Promise { - messDef = change.settings.SA4U.messageDefinition; - try { - const readSA4U = (await promises.readFile('.sa4u.json')).toString(); - const configJSON = JSON.parse(readSA4U); - configJSON['ProtocolDefinitionFile'] = messDef; - await promises.writeFile('.sa4u.json', JSON.stringify(configJSON, null, ' ')); - } catch (err) { - console.warn(`Failed to update .sa4u file: ${err}`); - } - restartDockerContainer(); -} - -async function restartDockerContainer(): Promise { - if (startedSA4U_Z3) { - startedSA4U_Z3 = false; - const folders = await connection.workspace.getWorkspaceFolders(); - if (folders) { - folders.forEach(async (folder) => { - const path = getPath(folder); - try { - await execAsync(`docker container stop sa4u_z3_server_${path}`); - } catch (err) { - console.log(`Failed to stop the docker container: ${err}`); - } - dockerContainer(folder); - }); - } - } -} - -async function validateTextDocument(textDocument: TextDocument): Promise { - const folders = await connection.workspace.getWorkspaceFolders(); - if (folders) { - folders.forEach(async (folder) => { - const path = getPath(folder); - try { - await execAsync(`docker container kill -s=HUP sa4u_z3_server_${path}`); - } catch (err) { - console.warn(`Failed to send HUP signal to the contianer: ${err}`); - } - }); - } -} - function getPath (folder: WorkspaceFolder, basic = false): string { let path = decodeURIComponent(folder.uri); path = path.replace(/(^\w+:|^)\/\//, ''); @@ -339,18 +373,19 @@ connection.onInitialize((params: InitializeParams) => { connection.onInitialized(() => { allowConfigurationChanges = false; - if (hasConfigurationCapability) { - // Register for all configuration changes. - connection.client.register(DidChangeConfigurationNotification.type, undefined); - - } if (hasWorkspaceFolderCapability) { connection.workspace.onDidChangeWorkspaceFolders(_event => { connection.console.log('Workspace folder change event received.'); }); } - Promise.all([checkForDockerRunningAndInstalled(), updateMessageDefinitionFromFile(), stopDockerContainer()]) - .then(() => {startDockerContainer();}, (err) => {connection.sendNotification('ServerError', `Server Failed to start Docker container: ${err}`);}); + Promise.all([checkForDockerRunningAndInstalled(), updateConfigurations(), stopAndRemoveDockerContainer()]).then( + () => {startDockerContainer();}, + (err) => {connection.sendNotification('ServerError', `Server Failed to start Docker container: ${err}`);} + ); + if (hasConfigurationCapability) { + // Register for all configuration changes. + connection.client.register(DidChangeConfigurationNotification.type, undefined); + } }); connection.onDidChangeConfiguration(change => { diff --git a/sa4u_z3/main.py b/sa4u_z3/main.py index 859ec47..5e0a959 100644 --- a/sa4u_z3/main.py +++ b/sa4u_z3/main.py @@ -272,6 +272,7 @@ def main(): ) signal.signal(signal.SIGHUP, HUP_signal_handler) + signal.signal(signal.SIGTERM, TERM_signal_handler) _use_power_of_ten = parsed_args.power_of_ten _enable_scalar_prefixes = not parsed_args.disable_scalar_prefixes @@ -383,6 +384,10 @@ def HUP_signal_handler(sig_num: int, _frame): print("In HUP signal handler...", flush=True) +def TERM_signal_handler(sig_num: int, _frame): + sys.exit() + + def walker(cursor: cindex.Cursor, data: Dict[Any, Any]) -> WalkResult: global _counter, _ignored filename: str = ''