From a69b88a1fd91d63d7c0717cd6134fdb264609dac Mon Sep 17 00:00:00 2001 From: Abdalrhman M Mohamed Date: Thu, 4 Nov 2021 01:27:04 -0500 Subject: [PATCH] Fix bugs. Signed-off-by: Abdalrhman M Mohamed --- CHANGELOG.md | 6 ++++++ package.json | 32 ++++++++++++++++---------------- src/Kind2.ts | 36 +++++++++++++++++++++++------------- src/treeNode.ts | 12 +++++++++++- 4 files changed, 56 insertions(+), 30 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 28cefb0..5809540 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,9 @@ +### Version 0.3.2 +- Change default values for options to mirror Kind 2's defaults. +- Fix issues with white spaces in paths. +- Fix issues where the extension hangs when Kind 2 generates long outputs. This also fixes issues with high verbosity levels. +- Remove diagnostic messages when Lustre files are closed. + ### Version 0.3.2 - Fix an issue where abstract nodes appear in both abstract and concrete sections. - Hide `show source` button for analysis results. diff --git a/package.json b/package.json index 5ca1280..9bea9ae 100644 --- a/package.json +++ b/package.json @@ -5,7 +5,7 @@ "description": "Language support for Kind 2", "author": "Abdalrhman M Mohamed", "license": "MIT", - "version": "0.3.2", + "version": "0.3.3", "preview": true, "repository": { "type": "git", @@ -65,13 +65,14 @@ "kind2.kind2_path": { "scope": "machine-overridable", "type": "string", - "default": null, + "default": "", "description": "Path to the kind2 executable used by the extension." }, "kind2.smt.smt_solver": { "type": "string", "scope": "machine-overridable", "enum": [ + "detect", "Boolector", "CVC4", "MathSAT", @@ -80,63 +81,62 @@ "Z3" ], "description": "Set the main SMT solver", - "default": null + "default": "detect" }, "kind2.smt.boolector_bin": { "scope": "machine-overridable", "type": "string", - "default": null, + "default": "boolector", "description": "Executable of Boolector solver." }, "kind2.smt.cvc4_bin": { "scope": "machine-overridable", "type": "string", - "default": null, + "default": "cvc4", "description": "Executable of CVC4 solver." }, "kind2.smt.mathsat_bin": { "scope": "machine-overridable", "type": "string", - "default": null, + "default": "mathsat", "description": "Executable of MathSAT solver." }, "kind2.smt.yices_bin": { "scope": "machine-overridable", "type": "string", - "default": null, + "default": "yices", "description": "Executable of Yices solver." }, "kind2.smt.yices2_bin": { "scope": "machine-overridable", "type": "string", - "default": null, + "default": "yices-smt2", "description": "Executable of Yices2 SMT2 solver." }, "kind2.smt.z3_bin": { "scope": "machine-overridable", "type": "string", - "default": null, - "description": "Executable of Z3 solver." + "default": "", + "description": "Executable of Z3 solver. Defaults to the Z3 executable bundled with the extension." }, "kind2.contracts.compositional": { "type": "boolean", "scope": "machine-overridable", "description": "Abstract subnodes with a contract", - "default": null + "default": false }, "kind2.timeout": { "type": "number", "scope": "machine-overridable", - "minimum": 0.0, - "maximum": 300.0, + "minimum": 0, "description": "Wallclock timeout in seconds", - "default": null + "default": 0 }, "kind2.modular": { "type": "boolean", "scope": "machine-overridable", "description": "Bottom-up analysis of each node", - "default": null + "default": false }, "kind2.log_level": { "type": "string", @@ -162,7 +162,7 @@ "Output informational, debug and trace messages" ], "description": "Levels of log messages", - "default": null + "default": "note" } } }, diff --git a/src/Kind2.ts b/src/Kind2.ts index 338328d..faaa738 100644 --- a/src/Kind2.ts +++ b/src/Kind2.ts @@ -175,7 +175,6 @@ export class Kind2 implements TreeDataProvider, CodeLensProvider { newFiles.push(mainFile); } for (let component of components) { - component.file = (component.file as string).replace("%2520", "%20"); this._fileMap.get(uri).add(component.file); // Only add components if this is the first time we see their files. if (this._files.find(f => f.uri === component.file) === undefined) { @@ -215,27 +214,26 @@ export class Kind2 implements TreeDataProvider, CodeLensProvider { await window.showTextDocument(Uri.parse(node.uri, true), { selection: range }); } - public async check(component: Component): Promise { - component.analyses = []; - component.state = "running"; + public async check(mainComponent: Component): Promise { + mainComponent.analyses = []; + mainComponent.state = "running"; let files: File[] = []; - for (const uri of this._fileMap.get(component.uri)) { + for (const uri of this._fileMap.get(mainComponent.uri)) { let file = this._files.find(f => f.uri === uri); files.push(file); } let modifiedComponents: Component[] = []; - modifiedComponents.push(component); + modifiedComponents.push(mainComponent); for (const component of modifiedComponents) { this._treeDataChanged.fire(component); } this._codeLensesChanged.fire(); this.updateDecorations(); let tokenSource = new CancellationTokenSource(); - this._runningChecks.set(component, tokenSource); - await this._client.sendRequest("kind2/check", [component.uri, component.name], tokenSource.token).then((values: string[]) => { + this._runningChecks.set(mainComponent, tokenSource); + await this._client.sendRequest("kind2/check", [mainComponent.uri, mainComponent.name], tokenSource.token).then((values: string[]) => { let results: any[] = values.map(s => JSON.parse(s)); for (const nodeResult of results) { - // TODO: fix file issue and add a link to kind2 website. let component = undefined; let i = 0; while (component === undefined) { @@ -247,7 +245,16 @@ export class Kind2 implements TreeDataProvider, CodeLensProvider { let analysis: Analysis = new Analysis(analysisResult.abstract, analysisResult.concrete, component); for (const propertyResult of analysisResult.properties) { let property = new Property(propertyResult.name, propertyResult.line - 1, propertyResult.file, analysis); - property.state = propertyResult.answer.value === "valid" ? "passed" : "failed"; + switch (propertyResult.answer.value) { + case "valid": + property.state = "passed"; + break; + case "falsifiable": + property.state = "failed"; + break; + default: + property.state = "errored"; + } analysis.properties.push(property); } component.analyses.push(analysis); @@ -258,18 +265,21 @@ export class Kind2 implements TreeDataProvider, CodeLensProvider { modifiedComponents.push(component); } if (results.length == 0) { - component.state = "passed"; + mainComponent.state = "passed"; } }).catch(reason => { window.showErrorMessage(reason.message); - component.state = "errored"; + mainComponent.state = "errored"; }); + if (mainComponent.state === "running") { + mainComponent.state = "errored"; + } for (const component of modifiedComponents) { this._treeDataChanged.fire(component); } this._codeLensesChanged.fire(); this.updateDecorations(); - this._runningChecks.delete(component); + this._runningChecks.delete(mainComponent); } public cancel(component: Component) { diff --git a/src/treeNode.ts b/src/treeNode.ts index 2bd09f6..30b42e4 100644 --- a/src/treeNode.ts +++ b/src/treeNode.ts @@ -39,10 +39,12 @@ export class Component implements Component { get properties(): Property[] { let passedProperties = new Map(); let failedProperties = new Map(); + let erroredProperties = new Map(); for (const analysis of this._analyses) { for (const property of analysis.properties) { if (property.state === "passed") { passedProperties.set(property.name, property); } if (property.state === "failed") { failedProperties.set(property.name, property); } + if (property.state === "errored") { erroredProperties.set(property.name, property); } } } let properties: Property[] = []; @@ -53,6 +55,9 @@ export class Component implements Component { for (const entry of failedProperties) { properties.push(entry[1]); } + for (const entry of erroredProperties) { + properties.push(entry[1]); + } return properties; } get state(): State { @@ -61,17 +66,22 @@ export class Component implements Component { } let passedProperties = new Set(); let failedProperties = new Set(); + let erroredProperties = new Set(); for (const analysis of this._analyses) { for (const property of analysis.properties) { if (property.state === "passed") { passedProperties.add(property.name); } if (property.state === "failed") { failedProperties.add(property.name); } + if (property.state === "errored") { erroredProperties.add(property.name); } } } for (const name of passedProperties) { failedProperties.delete(name); } + if (erroredProperties.size !== 0) { + return "errored"; + } if (failedProperties.size !== 0) { - return "failed" + return "failed"; } return "passed"; }