From c268acaa3046c026f49f8d681f8ff578bb0da86c Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 29 Apr 2024 10:16:40 -0500 Subject: [PATCH 1/3] Support realizability checks --- .../uiowa/kind2/lsp/Kind2LanguageServer.java | 106 ++++++++++++++++++ 1 file changed, 106 insertions(+) diff --git a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java index 4f2f6f7..0e83547 100644 --- a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java +++ b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java @@ -73,6 +73,7 @@ import edu.uiowa.cs.clc.kind2.results.NodeResult; import edu.uiowa.cs.clc.kind2.results.Property; import edu.uiowa.cs.clc.kind2.results.Result; +import edu.uiowa.cs.clc.kind2.results.RealizabilityResult; import edu.uiowa.cs.clc.kind2.results.TypeDeclInfo; /** @@ -361,6 +362,88 @@ public void done() { }); } + @JsonRequest(value = "kind2/realizability", useSegment = false) + public CompletableFuture> realizability(String uri, String name) { + return CompletableFutures.computeAsync(cancelToken -> { + client.logMessage(new MessageParams(MessageType.Info, + "Checking realizability of component " + name + " in " + uri + "...")); + analysisResults.get(uri).remove(name); + Result result = new Result(); + IProgressMonitor monitor = new IProgressMonitor() { + @Override + public boolean isCanceled() { + return cancelToken == null ? false : cancelToken.isCanceled(); + } + + @Override + public void done() { + } + }; + + try { + if (workingDirectory == null) { + workingDirectory = client.workspaceFolders().get().get(0).getUri(); + } + Kind2Api api = getCheckKind2Api(name); + api.includeDir(Paths.get(new URI(uri)).getParent().toString()); + String filepath = computeRelativeFilepath(workingDirectory, uri); + api.setFakeFilepath(filepath); + ArrayList options = new ArrayList<>(); + options.add(Module.CONTRACTCK); + api.execute(getText(uri), + result, + monitor, + options); + } catch (Kind2Exception | IOException | URISyntaxException + | InterruptedException | ExecutionException e) { + throw new ResponseErrorException(new ResponseError( + ResponseErrorCode.InternalError, e.getMessage(), e)); + } + + if (cancelToken.isCanceled()) { + client.logMessage( + new MessageParams(MessageType.Info, "Check cancelled.")); + // Throw an exception for the launcher to handle. + cancelToken.checkCanceled(); + } + + for (Map.Entry entry : result.getResultMap() + .entrySet()) { + analysisResults.get(uri).put(entry.getKey(), entry.getValue()); + } + + List diagnostics = new ArrayList<>(); + for (Log log : result.getAllKind2Logs()) { + Diagnostic diagnostic = logToDiagnostic(log); + if (diagnostic != null) { + diagnostics.add(diagnostic); + } + } + client.publishDiagnostics(new PublishDiagnosticsParams(uri, diagnostics)); + + checkLog(result); + + List nodeResults = new ArrayList<>(); + + for (Map.Entry entry : result.getResultMap() + .entrySet()) { + List analyses = new ArrayList<>(); + for (Analysis analysis : entry.getValue().getAnalyses()) { + String json = analysis.getJson(); + + // Add realizability info + RealizabilityResult res = analysis.getRealizabilityResult(); + json = json.substring(0, json.length() - 2) + ",\"realizabilityResult\": " + res.toString() + '}'; + analyses.add(json); + } + String json = "{\"name\": \"" + entry.getKey() + "\",\"analyses\": " + + analyses.toString() + "}"; + nodeResults.add(json); + } + return nodeResults; + }); + } + @JsonRequest(value = "kind2/counterExample", useSegment = false) public CompletableFuture counterExample(String uri, String component, List abs, List concrete, String property) { @@ -391,6 +474,29 @@ public CompletableFuture counterExample(String uri, String component, }); } + // @JsonRequest(value = "kind2/deadlock", useSegment = false) + // public CompletableFuture deadlock(String uri, String component) { + // return deadlock(uri, component, ""); + // } + + @JsonRequest(value = "kind2/deadlock", useSegment = false) + public CompletableFuture deadlock(String uri, String component, String context) { + return CompletableFuture.supplyAsync(() -> { + if (!analysisResults.containsKey(uri)) { + return null; + } + if (!analysisResults.get(uri).containsKey(component)) { + return null; + } + for (Analysis analysis : analysisResults.get(uri).get(component).getAnalyses()) { + if (analysis.getContext().equals(context)) { + return analysis.getDeadlock(); + } + } + return null; + }); + } + private SolverOption stringToSolver(String solver) { switch (solver.toUpperCase()) { case "BITWUZLA": From 9c5b27c593a09d6d7fd53257d667253ed8d75629 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 29 Apr 2024 10:33:19 -0500 Subject: [PATCH 2/3] Fix bug in json output for realizability checks --- src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java index 0e83547..234d6ce 100644 --- a/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java +++ b/src/main/java/edu/uiowa/kind2/lsp/Kind2LanguageServer.java @@ -433,7 +433,7 @@ public void done() { // Add realizability info RealizabilityResult res = analysis.getRealizabilityResult(); - json = json.substring(0, json.length() - 2) + ",\"realizabilityResult\": " + res.toString() + '}'; + json = json.substring(0, json.length() - 2) + ",\"realizabilityResult\": " + "\"" + res.toString() + "\"" + '}'; analyses.add(json); } String json = "{\"name\": \"" + entry.getKey() + "\",\"analyses\": " From 76a055c131d110ec669eae6fbbf1cb06380a857f Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 6 May 2024 22:01:33 -0500 Subject: [PATCH 3/3] Bump Kind 2 Java API version to 0.3.8 --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index ecbe03e..1ca4e93 100644 --- a/build.gradle +++ b/build.gradle @@ -8,7 +8,7 @@ repositories { } dependencies { - implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.6' + implementation 'edu.uiowa.cs.clc:kind2-java-api:0.3.8' implementation 'org.eclipse.lsp4j:org.eclipse.lsp4j:0.13.0' testImplementation 'org.junit.jupiter:junit-jupiter-api:5.7.2' testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.7.2'