Display failing Branches

client/package.json

@@ -135,6 +135,16 @@
 				"command": "viper.showSettings",
 				"title": "display settings effectively used by Viper-IDE",
 				"category": "Viper"
+			},
+			{
+				"command": "viper.declareField",
+				"title": "add field declaration on top of this file",
+				"category": "Viper"
+			},
+			{
+				"command": "viper.displayExploredBranches",
+				"title": "display explored branches of method",
+				"category": "Viper"
 			}
 		],
 		"menus": {

client/src/ExtensionState.ts

@@ -57,6 +57,7 @@ export class State {
     public static abortButton: StatusBar;
 
     public static diagnosticCollection: vscode.DiagnosticCollection;
+    public static textDecorators: Map<vscode.Uri, vscode.TextEditorDecorationType>;
 
     public static viperApi: ViperApi;
 
@@ -91,6 +92,7 @@ export class State {
         this.showViperStatusBarItems();
 
         this.diagnosticCollection = vscode.languages.createDiagnosticCollection();
+        this.textDecorators = new Map<vscode.Uri, vscode.TextEditorDecorationType>();
     }
 
     public static showViperStatusBarItems():  void {
@@ -350,6 +352,7 @@ export interface UnitTestCallback {
     internalErrorDetected: () => void;
     verificationStopped: (success: boolean) => void;
     verificationStarted: (backend: string, filename: string) => void;
+    showRedBeams: (decorationOptions: object[]) => void
 }
 
 type Disposable = { dispose(): any }; // eslint-disable-line @typescript-eslint/no-explicit-any

client/src/VerificationController.ts

@@ -19,8 +19,7 @@ import { Helper } from './Helper';
 import { ViperFileState } from './ViperFileState';
 import { Color } from './StatusBar';
 import { Settings } from './Settings';
-import { restart } from './extension';
-
+import { restart, removeDiagnostics } from './extension';
 
 export interface ITask {
     type: TaskType;
@@ -524,7 +523,7 @@ export class VerificationController {
                     fileState.verifying = true;
 
                     //clear all diagnostics
-                    State.diagnosticCollection.clear();
+                    removeDiagnostics();
 
                     //start progress updater
                     clearInterval(this.progressUpdater);
@@ -702,7 +701,7 @@ export class VerificationController {
                             verifiedFile.timingInfo = { total: params.time, timings: this.timings };
                         }
 
-                        const diagnostics = params.diagnostics
+                        const diagnostics = (params.diagnostics === undefined ? [] : params.diagnostics)
                             .map(this.translateLsp2VsCodeDiagnosticSeverity);
                         const nofErrors = diagnostics
                             .filter(diag => diag.severity == vscode.DiagnosticSeverity.Error)

client/src/ViperProtocol.ts

@@ -28,6 +28,8 @@ export class Commands {
     //SERVER TO CLIENT
     //Server notifies client about a state change
     static StateChange: NotificationType<StateChangeParams> = new NotificationType("StateChange");
+    // Server notifies the client about details of branch failure for displaying red beams
+    static BranchFailureDetails: NotificationType<BranchFailureDetails> = new NotificationType("BranchFailureDetails");
     //LOGGING
     //Log a message to the output
     static Log: NotificationType<LogParams> = new NotificationType("Log");
@@ -301,6 +303,12 @@ export interface ProgressParams {
     logLevel: LogLevel;
 }
 
+export interface BranchFailureDetails {
+    // errorMessage: string; // tree string
+    uri: string;
+    ranges: Range[];
+}
+
 export interface MyProtocolDecorationOptions {
     hoverMessage: string;
     range: Range;

client/src/extension.ts

@@ -22,7 +22,7 @@ import * as rimraf from 'rimraf';
 import * as vscode from 'vscode';
 import { URI } from 'vscode-uri';
 import { State } from './ExtensionState';
-import { HintMessage, Commands, StateChangeParams, LogLevel, LogParams, UnhandledViperServerMessageTypeParams, FlushCacheParams, Backend, Position, VerificationNotStartedParams } from './ViperProtocol';
+import { HintMessage, Commands, StateChangeParams, LogLevel, LogParams, UnhandledViperServerMessageTypeParams, FlushCacheParams, Backend, Position, VerificationNotStartedParams, BranchFailureDetails } from './ViperProtocol';
 import { Log } from './Log';
 import { Helper } from './Helper';
 import { locateViperTools } from './ViperTools';
@@ -326,6 +326,30 @@ function registerContextHandlers(context: vscode.ExtensionContext, location: Loc
         const document = await vscode.workspace.openTextDocument({ language: 'json', content: JSON.stringify(settings, null, 2) });
         await vscode.window.showTextDocument(document, vscode.ViewColumn.Two);
     }));
+
+    // add field declaration
+    context.subscriptions.push(vscode.commands.registerCommand('viper.declareField', async (fieldName) => {
+        const fieldType = await vscode.window.showInputBox({ prompt: 'Enter type: ' });
+        await vscode.window.activeTextEditor.edit(editBuilder => editBuilder.insert(new vscode.Position(0,0), `field ${fieldName} : ${fieldType}`));
+    }));
+
+    // display branches of a method explored by verification
+    context.subscriptions.push(vscode.commands.registerCommand('viper.displayExploredBranches', async (methodName, path) => {
+      const dotPreviewExt = vscode.extensions.getExtension('tintinweb.graphviz-interactive-preview');
+      if (dotPreviewExt) {
+        const options = {
+            uri: vscode.Uri.file(path),
+            title: `Method ${methodName} - Explored branches`
+        }
+        await vscode.commands.executeCommand("graphviz-interactive-preview.preview.beside", options);
+      } else {
+          const item: vscode.MessageItem = { title: "Show extension" };
+          const answer = await vscode.window.showErrorMessage("Cannot display explored branches: 'Graphviz interactive preview' extension not installed.", item);
+          if (answer===item) {
+              await vscode.commands.executeCommand('extension.open', 'tintinweb.graphviz-interactive-preview');
+          }
+      }
+    }));
 }
 
 function showNotReadyHint(): void {
@@ -334,6 +358,8 @@ function showNotReadyHint(): void {
 
 function registerClientHandlers(): void {
     State.client.onNotification(Commands.StateChange, (params: StateChangeParams) => State.verificationController.handleStateChange(params));
+
+    State.client.onNotification(Commands.BranchFailureDetails, (details: BranchFailureDetails) => showRedBeams(details));
 
     State.client.onNotification(Commands.Hint, (data: HintMessage) => {
         Log.hint(data.message, "Viper", data.showSettingsButton);
@@ -450,15 +476,57 @@ function considerStartingBackend(newBackend: Backend): Promise<void> {
     });
 }
 
-function removeDiagnostics(activeFileOnly: boolean): void {
+export function removeDiagnostics(activeFileOnly: boolean = false): void {
     if (activeFileOnly) {
         if (vscode.window.activeTextEditor) {
             const uri = vscode.window.activeTextEditor.document.uri;
             State.diagnosticCollection.delete(uri);
+            clearRedBeams(activeFileOnly);
             Log.log(`Diagnostics successfully removed for file ${uri}`, LogLevel.Debug);
         }
     } else {
         State.diagnosticCollection.clear();
+        clearRedBeams();
         Log.log(`All diagnostics successfully removed`, LogLevel.Debug);
     }
 }
+
+function showRedBeams(details: BranchFailureDetails): void {
+    const uri = vscode.Uri.parse(details.uri, false)
+    const textDecorator = getDecorationType();
+    State.textDecorators.set(uri, textDecorator);
+    const decorationOptions = details.ranges.map(r => {
+        return { hoverMessage : new vscode.MarkdownString("Branch fails"),
+                range :    new vscode.Range(
+                               new vscode.Position(r.start.line, r.start.character),
+                               new vscode.Position(r.end.line, r.end.character)
+                           )
+               }
+    });
+    vscode.window.activeTextEditor.setDecorations(textDecorator, decorationOptions);
+
+    if (State.unitTest) State.unitTest.showRedBeams(decorationOptions);
+}
+
+function clearRedBeams(activeFileOnly: boolean = false): void {
+    if (activeFileOnly) {
+        const uri = vscode.window.activeTextEditor.document.uri;
+        const textDecorator = State.textDecorators.get(uri);
+        State.textDecorators.delete(uri);
+        textDecorator.dispose();
+    } else {
+        for (const textDecorator of State.textDecorators.values()) {
+          textDecorator.dispose();
+        }
+        State.textDecorators.clear();
+    }
+}
+
+function getDecorationType() : vscode.TextEditorDecorationType {
+    return vscode.window.createTextEditorDecorationType({
+      isWholeLine: true,
+      rangeBehavior: 0,
+      gutterIconPath: State.context.asAbsolutePath(`images/beam.jpg`),
+      overviewRulerColor: "#ff2626"
+    });
+}

client/src/test/4_failingBranches.test.ts

@@ -0,0 +1,37 @@
+import assert from 'assert';
+import TestHelper, { SETUP_TIMEOUT, SILICON, BRANCH1, BRANCH2 } from './TestHelper';
+import * as fs from 'fs';
+import * as path from 'path';
+
+suite('ViperIDE Failing Branches Tests', () => {
+
+    const tempFolderPath =  TestHelper.getTestDataPath('tmp');
+
+    suiteSetup(async function() {
+        this.timeout(SETUP_TIMEOUT);
+        await TestHelper.setup();
+    });
+
+    suiteTeardown(async function() {
+        await TestHelper.teardown();
+    });
+
+    async function testFile(file: string, expected : object) {
+        await TestHelper.openFile(file);
+        await TestHelper.waitForVerification(file);
+        const actual = TestHelper.getDecorationOptions()[0]["range"];
+        assert.deepEqual(actual, expected, "Beam ranges not equal");
+    }
+
+    test("1. nested branches - if", async function() {
+        this.timeout(35000);
+        TestHelper.resetErrors();
+        await testFile(BRANCH1, {c:{"c":5,"e":0},e:{"c":11,"e":0}});
+    });
+
+    test("2. nested branches - else", async function() {
+        this.timeout(35000);
+        TestHelper.resetErrors();
+        await testFile(BRANCH2, {c:{"c":11,"e":0},e:{"c":17,"e":0}});
+    });
+});

client/src/test/TestHelper.ts

@@ -12,6 +12,7 @@ import * as myExtension from '../extension';
 import { State, UnitTestCallback } from '../ExtensionState';
 import { Log } from '../Log';
 import { Common, LogLevel, Output } from '../ViperProtocol';
+import * as fs from 'fs';
 
 export const PROJECT_ROOT = path.join(__dirname, "..", "..");
 export const DATA_ROOT = path.join(PROJECT_ROOT, "src", "test", "data");
@@ -26,6 +27,8 @@ export const EMPTY = 'empty.sil';
 export const EMPTY_TXT = 'empty.txt';
 export const LONG = 'longDuration.vpr';
 export const WARNINGS = 'warnings.vpr';
+export const BRANCH1 = 'branch1.vpr'
+export const BRANCH2 = 'branch2.vpr'
 
 
 export default class TestHelper {
@@ -80,7 +83,7 @@ export default class TestHelper {
         Log.logWithOrigin("UnitTest", msg, LogLevel.Verbose);
     }
 
-    private static getTestDataPath(fileName: string): string {
+    public static getTestDataPath(fileName: string): string {
         return path.join(DATA_ROOT, fileName);
     }
 
@@ -336,10 +339,15 @@ export default class TestHelper {
             }, timeoutMs);
         });
     }
+
+    public static getDecorationOptions(): object[] {
+        return TestHelper.callbacks.decorationOptions;
+    }
 }
 
 class UnitTestCallbackImpl implements UnitTestCallback {
     private errorDetected = false;
+    private decorationOptions_ = null;
 
     public get internalError(): boolean {
         return this.errorDetected;
@@ -349,6 +357,10 @@ class UnitTestCallbackImpl implements UnitTestCallback {
         this.errorDetected = false;
     }
 
+    public get decorationOptions(): object[] {
+        return this.decorationOptions_;
+    }
+
     extensionActivated: () => void = () => { };
     extensionRestarted: () => void = () => { };
     backendStarted: (backend: string) => void = () => { };
@@ -359,4 +371,5 @@ class UnitTestCallbackImpl implements UnitTestCallback {
     internalErrorDetected: () => void = () => { this.errorDetected = true; };
     verificationStopped: (success: boolean) => void = () => { };
     verificationStarted: (backend: string, filename: string) => void = () => { };
+    showRedBeams: (decorationOptions: vscode.DecorationOptions[]) => void = (opts) => {this.decorationOptions_ = opts};
 }

client/src/test/data/branch1.vpr

@@ -0,0 +1,19 @@
+define P(z) z == true
+
+method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool)
+requires a ==> c
+ensures P(z) {
+    if (a) {
+       if (bcde) {
+            z := !(bcde && a)
+        } else {
+            z := !(bcde && !a)
+        }
+    } else {
+        if (c) {
+            z := !(c && a)
+        } else {
+            z := !(!c && !a)
+        }
+    }
+}

client/src/test/data/branch2.vpr

@@ -0,0 +1,19 @@
+define P(z) z == true
+
+method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool)
+requires a ==> c
+ensures P(z) {
+    if (a) {
+       if (bcde) {
+            z := (bcde && a)
+        } else {
+            z := !(bcde && !a)
+        }
+    } else {
+        if (c) {
+            z := !(c && a)
+        } else {
+            z := !(!c && !a)
+        }
+    }
+}