Skip to content

Commit

Permalink
Merge pull request #17 from lorchrob/refinement-types
Browse files Browse the repository at this point in the history 
Support refinement type syntax highlighting and realizability checks for non-imported nodes
  • Loading branch information
@daniel-larraz
daniel-larraz authored May 7, 2024
2 parents 0f2862a + b6dbd62 commit cb3bdbe
Show file tree
Hide file tree
Showing 5 changed files with 264 additions and 32 deletions.
10 changes: 10 additions & 0 deletions package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -436,6 +436,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 @@ -459,6 +464,11 @@
"title": "Show trace",
"icon": "$(output)"
},
{
"command": "kind2/deadlock",
"title": "Show trace",
"icon": "$(output)"
},
{
"command": "kind2/check",
"title": "Check component",
Expand Down
169 changes: 149 additions & 20 deletions src/Kind2.ts
View file
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 @@ -284,6 +327,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 +338,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"];
} 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);
}
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";
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);
Expand Down Expand Up @@ -350,4 +461,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
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

0 comments on commit cb3bdbe

Please sign in to comment.