Fix bugs.

Signed-off-by: Abdalrhman M Mohamed <[email protected]>

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.

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"
         }
       }
     },

src/Kind2.ts

@@ -175,7 +175,6 @@ export class Kind2 implements TreeDataProvider<TreeNode>, 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<TreeNode>, CodeLensProvider {
     await window.showTextDocument(Uri.parse(node.uri, true), { selection: range });
   }
 
-  public async check(component: Component): Promise<void> {
-    component.analyses = [];
-    component.state = "running";
+  public async check(mainComponent: Component): Promise<void> {
+    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<TreeNode>, 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<TreeNode>, 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) {

src/treeNode.ts

@@ -39,10 +39,12 @@ export class Component implements Component {
   get properties(): Property[] {
     let passedProperties = new Map<string, Property>();
     let failedProperties = new Map<string, Property>();
+    let erroredProperties = new Map<string, Property>();
     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<string>();
     let failedProperties = new Set<string>();
+    let erroredProperties = new Set<string>();
     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";
   }