Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Filter properties generated by abstract interpretation (and more accurately/generally, filter all candidate properties) #18

Closed
wants to merge 8 commits into from
Closed

Filter properties generated by abstract interpretation (and more accurately/generally, filter all candidate properties) #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
b07a873
Update ref type syntax highlighting
lorchrob Mar 19, 2024
416b5f8
Support realizability checks
lorchrob Apr 24, 2024
71dfbca
Update handling of realizability results
lorchrob Apr 29, 2024
28d04e4
Fix handling of realizability checking icons for when an unrealizable…
lorchrob Apr 29, 2024
9d61604
Factor out containsUnrealizable function and remove unused cases of R…
lorchrob Apr 30, 2024
b6dbd62
Don't break property icons
lorchrob May 1, 2024
907f516
Filter out props generated by abstract interpretation
lorchrob May 1, 2024
6bb39ab
Filter out only candidate properties
lorchrob May 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions package.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -368,6 +368,11 @@
"group": "inline@1",
"when": "view == properties && viewItem == hasTrace"
},
{
"command": "kind2/deadlock",
"group": "inline@1",
"when": "view == properties && viewItem == hasDeadlock"
},
{
"command": "kind2/check",
"group": "inline@1",
Expand All @@ -391,6 +396,11 @@
"title": "Show trace",
"icon": "$(output)"
},
{
"command": "kind2/deadlock",
"title": "Show trace",
"icon": "$(output)"
},
{
"command": "kind2/check",
"title": "Check component",
Expand Down
173 changes: 153 additions & 20 deletions src/Kind2.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,14 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
["unreachable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("unreachable")) })],
["stopped", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("stopped")) })],
["unknown", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("unknown")) })],
["errored", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("errored")) })]])
["errored", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("errored")) })],
["realizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("realizable")) })],
["unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("unrealizable")) })],
["contract realizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("contract realizable")) })],
["contract unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("contract unrealizable")) })],
["inputs realizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("inputs realizable")) })],
["inputs unrealizable", window.createTextEditorDecorationType({ gutterIconPath: this._context.asAbsolutePath(statePath("inputs unrealizable")) })],
])
}

onDidChangeCodeLenses?: Event<void> | undefined;
Expand All @@ -47,10 +54,12 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
if (file) {
for (const component of file.components) {
let range = new Range(component.line, 0, component.line, 0);
if (component.state === "running") {

if (component.state.length > 0 && component.state[0] === "running") {
codeLenses.push(new CodeLens(range, { title: "Cancel", command: "kind2/cancel", arguments: [component] }));
} else {
codeLenses.push(new CodeLens(range, { title: "Check", command: "kind2/check", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Check Properties", command: "kind2/check", arguments: [component] }));
codeLenses.push(new CodeLens(range, { title: "Check Realizability", command: "kind2/realizability", arguments: [component] }))
}
codeLenses.push(new CodeLens(range, { title: "Simulate", command: "kind2/interpret", arguments: [component, "[]"] }));
codeLenses.push(new CodeLens(range, { title: "Raw Output", command: "kind2/raw", arguments: [component] }));
Expand All @@ -69,15 +78,30 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
}
else if (element instanceof Component) {
item = new TreeItem(element.name, element.analyses.length === 0 ? TreeItemCollapsibleState.None : TreeItemCollapsibleState.Expanded);
item.contextValue = element.state === "running" ? "running" : "component";
item.iconPath = Uri.file(path.join(this._context.extensionPath, statePath(element.state)));
// item.iconPath = stateIcon(element.state);
item.contextValue = element.state.length > 0 && element.state[0] === "running" ? "running" : "component";
if (element.containsUnrealizable()) { // At least one unrealizable result causes component's icon to be an X
item.iconPath = Uri.file(path.join(this._context.extensionPath, statePath("unrealizable")));
}
else {
item.iconPath = Uri.file(path.join(this._context.extensionPath, statePath(element.state[0])));
}
}
else if (element instanceof Analysis) {
let label = "Abstract: " + (element.abstract.length == 0 ? "none" : "[" + element.abstract.toString() + "]");
label += " - Concrete: " + (element.concrete.length == 0 ? "none" : "[" + element.concrete.toString() + "]");
item = new TreeItem(label, element.properties.length === 0 ? TreeItemCollapsibleState.None : TreeItemCollapsibleState.Expanded);
item.contextValue = "analysis";
if (element.realizability === undefined) {
let label = "Abstract: " + (element.abstract.length == 0 ? "none" : "[" + element.abstract.toString() + "]");
label += " - Concrete: " + (element.concrete.length == 0 ? "none" : "[" + element.concrete.toString() + "]");
item = new TreeItem(label, element.properties.length === 0 ? TreeItemCollapsibleState.None : TreeItemCollapsibleState.Expanded);
item.contextValue = "analysis";
}
else if (element.realizability === "realizable") {
item = new TreeItem(element.realizabilitySource, TreeItemCollapsibleState.None);
item.iconPath = Uri.file(path.join(this._context.extensionPath, statePath("passed")));
}
else {
item = new TreeItem(element.realizabilitySource, TreeItemCollapsibleState.None);
item.iconPath = Uri.file(path.join(this._context.extensionPath, statePath("failed")));
item.contextValue = "hasDeadlock";
}
}
else {
item = new TreeItem(element.name, TreeItemCollapsibleState.None);
Expand Down Expand Up @@ -112,11 +136,26 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
public updateDecorations(): void {
let decorations = new Map<string, Map<State, DecorationOptions[]>>();
for (const file of this._files) {
decorations.set(file.uri, new Map<State, DecorationOptions[]>([["pending", []], ["running", []], ["passed", []], ["reachable", []], ["failed", []], ["unreachable", []], ["stopped", []], ["unknown", []], ["errored", []]]));
decorations.set(file.uri, new Map<State, DecorationOptions[]>([["pending", []], ["running", []], ["passed", []], ["reachable", []], ["failed", []], ["unreachable", []], ["stopped", []], ["unknown", []], ["errored", []], ["realizable", []], ["inputs realizable", []], ["contract realizable", []], ["unrealizable", []], ["inputs unrealizable", []], ["contract unrealizable", []],]));
}
for (const file of this._files) {
for (const component of file.components) {
decorations.get(component.uri)?.get(component.state)?.push({ range: new Range(new Position(component.line, 0), (new Position(component.line, 0))) });
for (const state of component.state) {
if (state.startsWith("contract")) {
decorations.get(component.uri)?.get(state)?.push({ range: new Range(new Position(component.contractLine, 0), (new Position(component.contractLine, 0))) });
}
else if (state.startsWith("inputs")) {
if (component.containsUnrealizable() && component.line === component.contractLine) { // At least one unrealizable result causes component's icon to be an X
decorations.get(component.uri)?.get("unrealizable")?.push({ range: new Range(new Position(component.line, 0), (new Position(component.line, 0))) });
} else {
decorations.get(component.uri)?.get(state)?.push({ range: new Range(new Position(component.line, 0), (new Position(component.line, 0))) });
}
}
else {
decorations.get(component.uri)?.get(state)?.push({ range: new Range(new Position(component.line, 0), (new Position(component.line, 0))) });
}
}

for (const property of component.properties) {
if (decorations.has(property.uri)) {
let decorationOptions: DecorationOptions = { range: new Range(new Position(property.line, 0), (new Position(property.line, 100))) };
Expand All @@ -127,7 +166,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
}
for (const uri of decorations.keys()) {
let editor = window.visibleTextEditors.find(editor => editor.document.uri.toString() === uri);
for (const state of <State[]>["pending", "running", "passed", "reachable", "failed", "unreachable", "stopped", "unknown", "errored"]) {
for (const state of <State[]>["pending", "running", "passed", "reachable", "failed", "unreachable", "stopped", "unknown", "errored", "realizable", "unrealizable", "inputs realizable", "contract realizable", "inputs unrealizable", "contract unrealizable"]) {
editor?.setDecorations(this._decorationTypeMap.get(state)!, decorations.get(uri)?.get(state)!);
}
}
Expand Down Expand Up @@ -204,7 +243,11 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
file = new File(component.file, name);
newFiles.push(file);
}
file.components.push(new Component(component.name, component.startLine - 1, file));
var contractStart = component.contractStartLine - 1;
if (component.contractStartLine === undefined) {
contractStart = component.startLine - 1;
}
file.components.push(new Component(component.name, component.startLine - 1, contractStart, file));
}
}
this._files = this._files.concat(newFiles);
Expand Down Expand Up @@ -239,7 +282,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {

public async check(mainComponent: Component): Promise<void> {
mainComponent.analyses = [];
mainComponent.state = "running";
mainComponent.state = ["running"];
let files: File[] = [];
for (const uri of this._fileMap.get(mainComponent.uri)) {
let file = this._files.find(f => f.uri === uri);
Expand Down Expand Up @@ -267,6 +310,10 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
for (const analysisResult of nodeResult.analyses) {
let analysis: Analysis = new Analysis(analysisResult.abstract, analysisResult.concrete, component);
for (const propertyResult of analysisResult.properties) {
// Filter out candidate properties
if (propertyResult.isCandidate === "true") {
continue
}
let property = new Property(propertyResult.name, propertyResult.line - 1, propertyResult.file, analysis);
switch (propertyResult.answer.value) {
case "valid":
Expand All @@ -284,6 +331,7 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
default:
property.state = "unknown";
}
analysis.realizability = undefined;
analysis.properties.push(property);
}
component.analyses.push(analysis);
Expand All @@ -294,18 +342,85 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
modifiedComponents.push(component);
}
if (results.length == 0) {
mainComponent.state = "passed";
mainComponent.state = ["passed"];
}
}).catch(reason => {
if (reason.message.includes("cancelled")) {
mainComponent.state = "stopped";
mainComponent.state = ["stopped"];
} else {
window.showErrorMessage(reason.message);
mainComponent.state = "errored";
mainComponent.state = ["errored"];
}
});
if (mainComponent.state === "running") {
mainComponent.state = "passed";
if (mainComponent.state.length > 0 && mainComponent.state[0] === "running") {
mainComponent.state = ["passed"];
}
for (const component of modifiedComponents) {
this._treeDataChanged.fire(component);
}
this._codeLensesChanged.fire();
this.updateDecorations();
this._runningChecks.delete(mainComponent);
}

public async realizability(mainComponent: Component): Promise<void> {
mainComponent.analyses = [];
mainComponent.state = ["running"];
let files: File[] = [];
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(mainComponent);
for (const component of modifiedComponents) {
this._treeDataChanged.fire(component);
}
this._codeLensesChanged.fire();
this.updateDecorations();
let tokenSource = new CancellationTokenSource();
this._runningChecks.set(mainComponent, tokenSource);
await this._client.sendRequest("kind2/realizability", [mainComponent.uri, mainComponent.name], tokenSource.token).then((values: string[]) => {
let results: any[] = values.map(s => JSON.parse(s));
for (const nodeResult of results) {
let component = undefined;
let i = 0;
while (component === undefined) {
component = files[i].components.find(c => c.name === nodeResult.name);
++i;
}
for (const analysisResult of nodeResult.analyses) {
let analysis: Analysis = new Analysis([], [], component);
analysis.realizability = analysisResult.realizabilityResult.toLowerCase();
if (analysisResult.context === "contract") {
analysis.realizabilitySource = "contract"
}
else if (analysisResult.context === "environment") {
analysis.realizabilitySource = "inputs"
}
else {
analysis.realizabilitySource = "imported node"
}
component.analyses.push(analysis);
}
if (component.analyses.length == 0) {
component.state = "passed";
}
modifiedComponents.push(component);
}
if (results.length == 0) {
mainComponent.state = ["passed"];
}
}).catch(reason => {
if (reason.message.includes("cancelled")) {
mainComponent.state = ["stopped"];
} else {
window.showErrorMessage(reason.message);
mainComponent.state = ["errored"];
}
});
if (mainComponent.state.length > 0 && mainComponent.state[0] === "running") {
mainComponent.state = ["passed"];
}
for (const component of modifiedComponents) {
this._treeDataChanged.fire(component);
Expand Down Expand Up @@ -350,4 +465,22 @@ export class Kind2 implements TreeDataProvider<TreeNode>, CodeLensProvider {
window.showErrorMessage(reason.message);
});
}


public async deadlock(analysis: Analysis): Promise<void> {
var name = analysis.parent.name
var context = "";
if (analysis.realizabilitySource === "inputs") {
context = "environment"
}
else if (analysis.realizabilitySource === "contract") {
context = "contract"
}
await this._client.sendRequest("kind2/deadlock", [analysis.parent.uri, name, context]).then((dl: string) => {
WebPanel.createOrShow(this._context.extensionPath);
WebPanel.currentPanel?.sendMessage({ uri: analysis.parent.uri, main: analysis.parent.name, json: dl });
}).catch(reason => {
window.showErrorMessage(reason.message);
});
}
}
13 changes: 11 additions & 2 deletions src/extension.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ import {
StreamInfo
} from 'vscode-languageclient';
import { Kind2 } from './Kind2';
import { Component, Property, TreeNode } from './treeNode';
import { Component, Property, TreeNode, Analysis } from './treeNode';
import { WebPanel } from './webviewPanel';

let client: LanguageClient;
Expand Down Expand Up @@ -77,11 +77,16 @@ export async function activate(context: vscode.ExtensionContext) {
workspace.getConfiguration("kind2.contracts").update("compositional", false);
});

registerCommand('kind2/check', async (node: Component) => {
registerCommand('kind2/check', async (node: Component, options) => {
kind2.reveal(node, treeView);
await kind2.check(node);
});

registerCommand('kind2/realizability', async (node: Component, options) => {
kind2.reveal(node, treeView);
await kind2.realizability(node);
});

registerCommand('kind2/cancel', async (node: Component) => {
kind2.cancel(node);
});
Expand All @@ -92,6 +97,10 @@ export async function activate(context: vscode.ExtensionContext) {
await kind2.counterExample(property);
});

registerCommand('kind2/deadlock', async (analysis: Analysis) => {
await kind2.deadlock(analysis);
});

registerCommand('kind2/interpret', async (component: { uri: string, name: string }, json: string) => {
await kind2.interpret(component.uri, component.name, json);
});
Expand Down
Loading
Loading