Unverified Commit 5a381615 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💾
Browse files

Live analysis

parent 2c1e8a52
// A launch configuration that compiles the extension and then opens it inside a new window
{
"version": "0.1.0",
"version": "latest",
"configurations": [
{
"name": "Launch Extension",
......
......@@ -8,23 +8,13 @@
// A task runner that calls a custom npm script that compiles the extension.
{
"version": "0.1.0",
"version": "2.0.0",
// we want to run npm
"command": "npm",
// the command is a shell script
"isShellCommand": true,
// show the output window only if unrecognized errors occur.
"showOutput": "silent",
// we run the custom script "compile" as defined in package.json
"args": ["run", "compile", "--loglevel", "silent"],
// The tsc compiler is started in watching mode
"isWatching": true,
"isBackground": true,
// use the standard tsc in watch mode problem matcher to find compile problems in the output.
"problemMatcher": "$tsc-watch"
}
\ No newline at end of file
......@@ -3,40 +3,72 @@
import * as vscode from 'vscode';
import VerifpalLib from './VerifpalLib';
import {
match
} from 'assert';
let analysisActive = false;
export default class AnalysisProvider {
static greenDecoration = vscode.window.createTextEditorDecorationType({
border: '2px solid green',
borderRadius: '3px'
})
border: '1px solid green',
borderRadius: '3px',
fontWeight: 'bold'
});
static redDecoration = vscode.window.createTextEditorDecorationType({
border: '2px solid red',
borderRadius: '3px'
})
border: '1px solid red',
borderRadius: '3px',
fontWeight: 'bold'
});
static analysisOutput = vscode.window.createOutputChannel("Verifpal Analysis");
static decorate(editor: vscode.TextEditor, parsedResults) {
let fileContents = editor.document.getText();
let passedQueries: vscode.DecorationOptions[] = [];
let failedQueries: vscode.DecorationOptions[] = [];
const fileContentsArray = fileContents.split('\n');
for (let i = 0; i < parsedResults.length; i++) {
if (parsedResults[i].Resolved) {
this.analysisOutput.appendLine(`${parsedResults[i].Query}\n${parsedResults[i].Summary}`);
vscode.window.showInformationMessage(`Verifpal: Query "${parsedResults[i].Query}" failed. Check the Verifpal Analysis output pane for more details.`);
}
}
for (let i = 0; i < parsedResults.length; i++) {
for (let line = 0; line < fileContentsArray.length; line++) {
let tl = fileContentsArray[line].toLowerCase();
let tq = parsedResults[i].Query.toLowerCase();
let index = tl.indexOf(tq)
if (index >= 0) {
let queryIndex = tl.indexOf(tq);
if (queryIndex >= 0) {
let range = new vscode.Range(
new vscode.Position(line, index),
new vscode.Position(line, index + tq.length)
new vscode.Position(line, queryIndex),
new vscode.Position(line, queryIndex + tq.length)
);
if (parsedResults[i].Resolved) {
failedQueries.push({ range });
failedQueries.push({
range
});
} else {
passedQueries.push({ range });
passedQueries.push({
range
});
}
}
if (!parsedResults[i].Resolved) {
continue
}
let constantNames = parsedResults[i].Constants;
for (let ii = 0; ii < constantNames.length; ii++) {
let constMatch = tl.match(`(\\W)${constantNames[ii]}(\\,|\\]|\\)|\\s|\\^|$)`);
if (constMatch !== null && constMatch.index !== undefined) {
let range = new vscode.Range(
new vscode.Position(line, constMatch.index + 1),
new vscode.Position(line, constMatch.index + 1 + constantNames[ii].length)
);
failedQueries.push({
range
});
}
}
}
......@@ -46,19 +78,50 @@ export default class AnalysisProvider {
}
static verify(editor: vscode.TextEditor, edit: vscode.TextEditorEdit) {
if (analysisActive) {
vscode.window.showInformationMessage(`Verifpal: Analysis is already running.`);
return
}
let fileContents = editor.document.getText();
vscode.window.showInformationMessage(`Verifpal: Running analysis...`);
analysisActive = true;
return VerifpalLib.getVerify(fileContents).then((result: string) => {
analysisActive = false;
result = result.split(/\r?\n/).pop() || '';
const verifyResults = JSON.parse(result);
const parsedResults: Object[] = [];
for (let i = 0; i < verifyResults.length; i++) {
let q = JSON.stringify(verifyResults[i].Query)
VerifpalLib.getPrettyQuery(q).then((result: string) => {
let constantNames: string[] = [];
switch (verifyResults[i].Query.Kind) {
case "confidentiality":
for (let ii = 0; ii < verifyResults[i].Query.Constants.length; ii++) {
constantNames.push(verifyResults[i].Query.Constants[ii].Name)
}
break;
case "authentication":
for (let ii = 0; ii < verifyResults[i].Query.Message.Constants.length; ii++) {
constantNames.push(verifyResults[i].Query.Message.Constants[ii].Name)
}
break;
case "freshness":
for (let ii = 0; ii < verifyResults[i].Query.Constants.length; ii++) {
constantNames.push(verifyResults[i].Query.Constants[ii].Name)
}
break;
case "unlinkability":
for (let ii = 0; ii < verifyResults[i].Query.Constants.length; ii++) {
constantNames.push(verifyResults[i].Query.Constants[ii].Name)
}
break;
}
let formattedSummary = verifyResults[i].Summary.replace(/\[(\d|;)+m/gm, '');
let p = {
Query: result,
Resolved: verifyResults[i].Resolved,
Summary: verifyResults[i].Summary
Summary: formattedSummary,
Constants: constantNames
}
parsedResults.push(p)
if (parsedResults.length === verifyResults.length) {
......
......@@ -51,4 +51,4 @@ export function activate(context: vscode.ExtensionContext) {
vscode.commands.registerCommand('verifpal.path', showVerifpalPath);
}
export function deactivate() { }
\ No newline at end of file
export function deactivate() {}
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment