diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java index 7209019..2f4c2a1 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/Kind2Api.java @@ -9,15 +9,20 @@ import java.io.File; import java.io.IOException; +import java.io.InputStreamReader; import java.net.URI; import java.util.ArrayList; import java.util.HashSet; import java.util.List; import java.util.Set; +import com.google.gson.JsonElement; +import com.google.gson.JsonIOException; +import com.google.gson.JsonStreamParser; + import edu.uiowa.cs.clc.kind2.Kind2Exception; -import edu.uiowa.cs.clc.kind2.results.Result; import edu.uiowa.cs.clc.kind2.lustre.Program; +import edu.uiowa.cs.clc.kind2.results.Result; /** * The primary interface to Kind2. @@ -272,20 +277,17 @@ public String interpret(URI uri, String main, String json) { options.add(uri.getPath()); ProcessBuilder builder = new ProcessBuilder(options); try { - String output = ""; Process process = builder.start(); - while (process.isAlive()) { - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); - sleep(POLL_INTERVAL); + final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); + JsonStreamParser jsp = new JsonStreamParser(reader); + String trace = ""; + while (jsp.hasNext()) { + JsonElement jele = jsp.next(); + if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { + trace = jele.getAsJsonObject().get("trace").toString(); + } } - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); - return output.substring(output.indexOf("trace") + 9, output.length() - 5); + return trace; } catch (IOException e) { throw new Kind2Exception(e.getMessage()); } @@ -303,23 +305,20 @@ public String interpret(String program, String main, String json) { options.add(ApiUtil.writeInterpreterFile(json).toURI().getPath()); ProcessBuilder builder = new ProcessBuilder(options); try { - String output = ""; Process process = builder.start(); process.getOutputStream().write(program.getBytes()); process.getOutputStream().flush(); process.getOutputStream().close(); - while (process.isAlive()) { - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); - sleep(POLL_INTERVAL); + final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); + JsonStreamParser jsp = new JsonStreamParser(reader); + String trace = ""; + while (jsp.hasNext()) { + JsonElement jele = jsp.next(); + if (jele.isJsonObject() && jele.getAsJsonObject().has("trace")) { + trace = jele.getAsJsonObject().get("trace").toString(); + } } - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); - return output.substring(output.indexOf("trace") + 9, output.length() - 5); + return trace; } catch (IOException e) { throw new Kind2Exception(e.getMessage()); } @@ -334,45 +333,71 @@ public String interpret(String program, String main, String json) { * @throws Kind2Exception */ public void execute(String program, Result result, IProgressMonitor monitor) { + this.execute(program, result, monitor, (ResultListener)null); + } + + /** + * Run Kind on a Lustre program + * + * @param program Lustre program as text + * @param result Place to store results as they come in + * @param monitor Used to check for cancellation + * @throws Kind2Exception + */ + public void execute(String program, Result result, IProgressMonitor monitor, ResultListener listener) { try { - callKind2(program, result, monitor); + callKind2(program, result, monitor, listener); } catch (Throwable t) { throw new Kind2Exception(t.getMessage(), t); } } - private void callKind2(String program, Result result, IProgressMonitor monitor) + private void callKind2(String program, Result result, IProgressMonitor monitor, ResultListener listener) throws IOException, InterruptedException { ProcessBuilder builder = getKind2ProcessBuilder(); debug.println("Kind 2 command: " + ApiUtil.getQuotedCommand(builder.command())); Process process = null; - String output = ""; boolean exceptionThrown = false; - + JsonStreamParser jsp; try { process = builder.start(); process.getOutputStream().write(program.getBytes()); process.getOutputStream().flush(); process.getOutputStream().close(); - while (!monitor.isCanceled() && process.isAlive()) { - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); - sleep(POLL_INTERVAL); + final InputStreamReader reader = new InputStreamReader(process.getInputStream(), java.nio.charset.StandardCharsets.UTF_8); + jsp = new JsonStreamParser(reader); + // The following assignment is required because variables used in lambdas must be final or effectively final. + final Process processForMonitor = process; + Thread monitorThread = new Thread(() -> { + while (!monitor.isCanceled() && processForMonitor.isAlive()) { + sleep(POLL_INTERVAL); + } + if (monitor.isCanceled() && processForMonitor.isAlive()) { + debug.println("Monitor canceled, destroying Kind2 process"); + processForMonitor.destroy(); + try { reader.close(); } catch (IOException e) { /* ignore */ } + } + }); + monitorThread.start(); + while (jsp.hasNext()) { + JsonElement jele = jsp.next(); + debug.println("Parsing JSON element: " + jele.toString()); + result.addJsonElement(jele); + if(listener != null){ + listener.onUpdate(result); + } + debug.println(result.getResultMap().toString()); } + } catch (JsonIOException e) { + // ignore JsonIOException, which may occur if the process is destroyed while reading JSON } catch (Throwable t) { exceptionThrown = true; throw t; } finally { try { if (!monitor.isCanceled()) { - int available = process.getInputStream().available(); - byte[] bytes = new byte[available]; - process.getInputStream().read(bytes); - output += new String(bytes); try { - result.initialize(output); + result.finish(); } catch (Throwable t) { if (!exceptionThrown) { throw t; @@ -408,7 +433,7 @@ public void setOtherOptions(List options) { public List getOptions() { List options = new ArrayList<>(); - options.add("-json"); + options.add("-ijson"); if (logLevel != null) { options.add(logLevel.getOption()); } diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java b/src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java new file mode 100644 index 0000000..3f8635f --- /dev/null +++ b/src/main/java/edu/uiowa/cs/clc/kind2/api/ResultListener.java @@ -0,0 +1,10 @@ +package edu.uiowa.cs.clc.kind2.api; + +import edu.uiowa.cs.clc.kind2.results.Result; + +@FunctionalInterface +public interface ResultListener { + + void onUpdate(Result result); + +} diff --git a/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java b/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java index a325bdd..3a1c79a 100644 --- a/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java +++ b/src/main/java/edu/uiowa/cs/clc/kind2/results/Result.java @@ -7,16 +7,21 @@ package edu.uiowa.cs.clc.kind2.results; +import java.math.RoundingMode; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; + import com.google.gson.GsonBuilder; import com.google.gson.JsonArray; import com.google.gson.JsonElement; import com.google.gson.JsonObject; import com.google.gson.JsonParser; -import java.math.RoundingMode; -import java.util.*; -import java.util.stream.Collectors; - /** * The class is the top one in Kind2 explanations. An instance of this class is generated from kind2 * json string using the method {@link Result#analyzeJsonResult(String)}. The returned instance @@ -70,7 +75,7 @@ public class Result { /** * Kind2 json output. */ - private String json; + private JsonArray json; /** * a list of kind2 logs. */ @@ -157,7 +162,7 @@ public static Result analyzeJsonResult(String json) { public void initialize(String json) { JsonArray jsonArray = JsonParser.parseString(json).getAsJsonArray(); - this.json = new GsonBuilder().setPrettyPrinting().create().toJson(jsonArray); + this.json = jsonArray; Analysis kind2Analysis = null; // for post analysis Analysis previousAnalysis = null; @@ -289,6 +294,162 @@ public void initialize(String json) { isInitialized = true; } +private Analysis kind2Analysis = null; +// for post analysis +private Analysis previousAnalysis = null; +private boolean emptyAnalysis = false; + public void addJsonElement(JsonElement jsonElement) { + if (/*init condition */ this.json == null){ + this.json = new JsonArray(); + } + this.json.add(jsonElement); + + JsonObject jsonObject; + String objectType = jsonElement.getAsJsonObject().get(Labels.objectType).getAsString(); + Object kind2Object = Object.getKind2Object(objectType); + switch (kind2Object){ + case kind2Options: + Options options = new Options(jsonElement); + this.options = options; + break; + case log: + Log log = new Log(this, jsonElement); + this.kind2Logs.add(log); + break; + + + case lsp: + jsonObject = jsonElement.getAsJsonObject(); + String kind = jsonObject.get(Labels.kind).getAsString(); + AstInfo astInfo; + switch (kind) { + case "typeDecl": + astInfo = new TypeDeclInfo(jsonElement); + break; + case "constDecl": + case "paramDecl": + astInfo = new ConstDeclInfo(jsonElement); + break; + case "node": + astInfo = new NodeInfo(jsonElement); + break; + case "function": + astInfo = new FunctionInfo(jsonElement); + break; + case "contract": + astInfo = new ContractInfo(jsonElement); + break; + case "lemma": + astInfo = new LemmaInfo(jsonElement); + break; + default: + throw new RuntimeException("Failed to analyze kind2 json output"); + } + this.astInfos.add(astInfo); + break; + + case analysisStart: + // define new analysis + kind2Analysis = new Analysis(jsonElement); + break; + + case analysisStop: + if (kind2Analysis != null) { + // finish the analysis + this.put(kind2Analysis.getNodeName(), kind2Analysis); + NodeResult nodeResult = resultMap.get(kind2Analysis.getNodeName()); + for (Analysis analysis : nodeResult.getAnalyses()) { + List subNodes = analysis.getSubNodes(); + for (String node : subNodes) { + if (resultMap.containsKey(node)) { + nodeResult.addChild(resultMap.get(node)); + } + } + } + + + + + + previousAnalysis = kind2Analysis; + kind2Analysis = null; + } else { + throw new RuntimeException("Failed to analyze kind2 json output"); + } + break; + + case property: + if (kind2Analysis != null) { + Property property = new Property(kind2Analysis, jsonElement); + kind2Analysis.addProperty(property); + } else { + throw new RuntimeException("Can not parse kind2 json output"); + } + break; + + case realizabilityResult: + if (kind2Analysis != null) { + jsonObject = jsonElement.getAsJsonObject(); + String res = jsonObject.get(Labels.result).getAsString(); + if (res.equals(Labels.realizable)) { + kind2Analysis.setRealizabilityResult(RealizabilityResult.realizable); + } else if (res.equals(Labels.unrealizable)) { + kind2Analysis.setRealizabilityResult(RealizabilityResult.unrealizable); + } + JsonElement deadlockElement = jsonObject.get(Labels.deadlockingTrace); + String deadlock = new GsonBuilder().setPrettyPrinting().create().toJson(deadlockElement); + kind2Analysis.setDeadlock(deadlock); + } else { + throw new RuntimeException("Can not parse kind2 json output"); + } + break; + + case postAnalysisStart: + if (previousAnalysis != null) { + PostAnalysis postAnalysis = new PostAnalysis(previousAnalysis, jsonElement); + previousAnalysis.setPostAnalysis(postAnalysis); + } else { + // This can occur sometimes with no previous analysis when the node had no properties to check. + emptyAnalysis = true; + } + break; + + case postAnalysisEnd: + if (previousAnalysis != null && previousAnalysis.getPostAnalysis() != null) { + // finish the post analysis + previousAnalysis = null; + } else if (emptyAnalysis){ + //Do nothing, had a no-analysis postAnalysisStart beforehand. + } else { + throw new RuntimeException("Failed to analyze kind2 json output"); + } + break; + + case modelElementSet: + if (previousAnalysis != null && previousAnalysis.getPostAnalysis() != null) { + PostAnalysis postAnalysis = previousAnalysis.getPostAnalysis(); + ModelElementSet elementSet = new ModelElementSet(postAnalysis, jsonElement); + postAnalysis.addModelElementSet(elementSet); + } else { + // This branch gets hit sometimes when we have empty (nonexistent) analyses of nodes with + // no properties to check, causing missing analyses before postAnalyses, as well as this object. + } + break; + } + + } + + public void finish(){ + + // build the node tree + this.buildTree(); + // analyze the result + this.analyze(); + + isInitialized = true; + } + + /** * construct a tree of subcomponents. */ @@ -330,7 +491,7 @@ public Options getOptions() { * @return Kind2 json output. */ public String getJson() { - return json; + return json == null ? null : json.toString(); } /** diff --git a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java index df79519..e424b8c 100644 --- a/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java +++ b/src/test/java/edu/uiowa/cs/clc/kind2/results/Kind2ResultTests.java @@ -8,18 +8,22 @@ package edu.uiowa.cs.clc.kind2.results; -import org.junit.jupiter.api.BeforeEach; -import org.junit.jupiter.api.Test; - import java.io.IOException; import java.math.RoundingMode; import java.nio.file.Files; import java.nio.file.Paths; -import java.util.Collections; import java.util.List; -import java.util.Map; -import static org.junit.jupiter.api.Assertions.*; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertNull; +import static org.junit.jupiter.api.Assertions.assertTrue; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import com.google.gson.JsonArray; +import com.google.gson.JsonElement; +import com.google.gson.JsonParser; public class Kind2ResultTests { @@ -262,6 +266,36 @@ void namesMapping() assertEquals("kind2 v1.1.0-482-gd69f383a", log.getValue()); } + @Test + void initializeIncMatchesInitialize() + { + String json = "[" + + "{\"objectType\":\"kind2Options\",\"enabled\":[],\"timeout\":0.0,\"bmcMax\":0,\"compositional\":false,\"modular\":false}," + + "{\"objectType\":\"log\",\"level\":\"info\",\"source\":\"parse\",\"value\":\"kind2 v2.0.0\"}," + + "{\"objectType\":\"lsp\",\"kind\":\"node\",\"name\":\"Main\",\"imported\":false}," + + "{\"objectType\":\"analysisStart\",\"top\":\"Sub\",\"concrete\":[],\"abstract\":[],\"assumptions\":[]}," + + "{\"objectType\":\"analysisStop\"}," + + "{\"objectType\":\"analysisStart\",\"top\":\"Main\",\"concrete\":[\"Sub\"],\"abstract\":[],\"assumptions\":[]}," + + "{\"objectType\":\"analysisStop\"}" + + "]"; + + Result expected = Result.analyzeJsonResult(json); + + Result incremental = new Result(); + JsonArray jsonArray = JsonParser.parseString(json).getAsJsonArray(); + for (JsonElement element : jsonArray) + { + incremental.addJsonElement(element); + } + incremental.finish(); + assertEquals(JsonParser.parseString(expected.getJson()), JsonParser.parseString(incremental.getJson())); + assertEquals(expected.getResultMap().keySet(), incremental.getResultMap().keySet()); + assertEquals(expected.getKind2Logs().size(), incremental.getKind2Logs().size()); + assertEquals(expected.getAstInfos().size(), incremental.getAstInfos().size()); + assertTrue(incremental.getNodeResult("Main").getChildren().contains(incremental.getNodeResult("Sub"))); + assertEquals(expected.getNodeResult("Main").getChildren().size(), incremental.getNodeResult("Main").getChildren().size()); + } + @Test void suggestion6() {