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..b3c95d0 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,19 @@ 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.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. @@ -334,45 +338,56 @@ 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); + jsp = new JsonStreamParser(new InputStreamReader(process.getInputStream())); + while (!monitor.isCanceled() && jsp.hasNext()) { + JsonElement jele = jsp.next(); + debug.println("Parsing JSON element: " + jele.toString()); + result.initializeInc(jele); + if(listener != null){ + listener.onUpdate(result); + } + debug.println(result.getResultMap().toString()); } + debug.println("Exited loop because of isCanceled:" + !monitor.isCanceled() + " ; processIsAlive: " + process.isAlive() + "jspHasNext:" + jsp.hasNext()); } 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.closeInitialization(); } catch (Throwable t) { if (!exceptionThrown) { throw t; @@ -408,7 +423,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..2acc0c3 --- /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; + + +public interface ResultListener { + + public 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..ffd39cf 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,159 @@ public void initialize(String json) { isInitialized = true; } + Analysis kind2Analysis = null; + // for post analysis + Analysis previousAnalysis = null; + boolean emptyAnalysis = false; + public void initializeInc(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; + default: + throw new RuntimeException("Failed to analyze kind2 json output"); + } + this.astInfos.add(astInfo); + break; + + case analysisStart: + // define new analysis + kind2Analysis = new Analysis(jsonElement); + this.put(kind2Analysis.getNodeName(), kind2Analysis); + break; + + case analysisStop: + if (kind2Analysis != null) { + // finish the analysis + 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 closeInitialization(){ + + // build the node tree + // this.buildTree(); + // analyze the result + this.analyze(); + + isInitialized = true; + } + + /** * construct a tree of subcomponents. */ @@ -330,7 +488,7 @@ public Options getOptions() { * @return Kind2 json output. */ public String getJson() { - return json; + return json.toString(); } /**