Unverified Commit 2c1e8a52 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💾
Browse files

Live analysis MVP

parent f461ad59
......@@ -47,7 +47,7 @@
],
"commands": [
{
"command": "verifpal.coverage",
"command": "verifpal.verify",
"title": "Verifpal: Run Attacker Analysis"
},
{
......
......@@ -6,29 +6,67 @@ import VerifpalLib from './VerifpalLib';
export default class AnalysisDecorations {
export default class AnalysisProvider {
static decorationType = vscode.window.createTextEditorDecorationType({
backgroundColor: 'green',
border: '2px solid white',
static greenDecoration = vscode.window.createTextEditorDecorationType({
border: '2px solid green',
borderRadius: '3px'
})
static decorate(editor: vscode.TextEditor) {
let sourceCode = editor.document.getText()
let regex = /(console\.log)/
let decorationsArray: vscode.DecorationOptions[] = []
const sourceCodeArr = sourceCode.split('\n')
for (let line = 0; line < sourceCodeArr.length; line++) {
let match = sourceCodeArr[line].match(regex)
if (match !== null && match.index !== undefined) {
let range = new vscode.Range(
new vscode.Position(line, match.index),
new vscode.Position(line, match.index + match[1].length)
)
let decoration = { range }
decorationsArray.push(decoration)
static redDecoration = vscode.window.createTextEditorDecorationType({
border: '2px solid red',
borderRadius: '3px'
})
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++) {
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 range = new vscode.Range(
new vscode.Position(line, index),
new vscode.Position(line, index + tq.length)
);
if (parsedResults[i].Resolved) {
failedQueries.push({ range });
} else {
passedQueries.push({ range });
}
}
}
}
editor.setDecorations(AnalysisDecorations.decorationType, decorationsArray);
editor.setDecorations(AnalysisProvider.greenDecoration, passedQueries);
editor.setDecorations(AnalysisProvider.redDecoration, failedQueries);
}
static verify(editor: vscode.TextEditor, edit: vscode.TextEditorEdit) {
let fileContents = editor.document.getText();
vscode.window.showInformationMessage(`Verifpal: Running analysis...`);
return VerifpalLib.getVerify(fileContents).then((result: string) => {
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 p = {
Query: result,
Resolved: verifyResults[i].Resolved,
Summary: verifyResults[i].Summary
}
parsedResults.push(p)
if (parsedResults.length === verifyResults.length) {
vscode.window.showInformationMessage(`Verifpal: Analysis complete.`);
AnalysisProvider.decorate(editor, parsedResults);
}
});
}
});
}
}
\ No newline at end of file
......@@ -69,6 +69,26 @@ export default class VerifpalLib {
});
}
static getKnowledgeMap(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'knowledgeMap']);
}
static getPrettyValue(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'prettyValue']);
}
static getPrettyQuery(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'prettyQuery']);
}
static getPrettyPrint(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'prettyPrint']);
}
static getVerify(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'verify']);
}
static getKnowledgeMapIndexFromConstant(constant: string, knowledgeMap) {
for (let i = 0; i < knowledgeMap.Constants.length; i++) {
if (knowledgeMap.Constants[i].Name === constant) {
......@@ -244,18 +264,4 @@ export default class VerifpalLib {
}
return '';
}
static getKnowledgeMap(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'knowledgeMap']);
}
static getPrettyValue(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'prettyValue']);
}
static getPrettyPrint(fileContents: string) {
return VerifpalLib.execVerifpal(fileContents, ['internal-json', 'prettyPrint']);
}
static getCoverage(fileContents: string, fileName: string): any {}
}
\ No newline at end of file
/* SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi <nadim@symbolic.software>
* SPDX-License-Identifier: GPL-3.0-only */
import * as vscode from 'vscode';
import VerifpalLib from './VerifpalLib';
import HoverProvider from './HoverProvider';
import CoverageProvider from './AnalysisProvider';
import AnalysisProvider from './AnalysisProvider';
import {
configGetEnabled,
configDeterminePath
} from './config';
'use strict';
import * as vscode from 'vscode';
import VerifpalLib from './VerifpalLib';
import {
format
} from 'url';
export function activate(context: vscode.ExtensionContext) {
if (!configGetEnabled()) {
return false;
......@@ -40,17 +35,19 @@ export function activate(context: vscode.ExtensionContext) {
}
});
const showVerifpalPath = () => {
vscode.window.showInformationMessage(`Verifpal path set to '${configDeterminePath()}'`);
}
vscode.workspace.onWillSaveTextDocument(event => {
const openEditor = vscode.window.visibleTextEditors.filter(
editor => editor.document.uri === event.document.uri
)[0]
})
});
const showVerifpalPath = () => {
vscode.window.showInformationMessage(
`Verifpal path set to '${configDeterminePath()}'`
);
}
// vscode.commands.registerCommand('verifpal.coverage', refreshCoverage);
vscode.commands.registerTextEditorCommand('verifpal.verify', AnalysisProvider.verify);
vscode.commands.registerCommand('verifpal.path', showVerifpalPath);
}
......
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