Skip to content

Commit

Permalink
Restored json-only dumping of cfg inputs #230
Browse files Browse the repository at this point in the history
  • Loading branch information
lucaneg committed Nov 7, 2022
1 parent fcf9462 commit 5c6628e
Show file tree
Hide file tree
Showing 10 changed files with 104 additions and 30 deletions.
4 changes: 4 additions & 0 deletions lisa/lisa-core/imp-testcases/visualization/inputs/report.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
{
"warnings" : [ ],
"files" : [ "untyped_A.A(A__this)_cfg.json", "untyped_A.getOne(A__this)_cfg.json", "untyped_A.getPositive(A__this,_untyped_i)_cfg.json", "untyped_A.identity(A__this,_untyped_i)_cfg.json", "untyped_tests.helper(tests__this,_untyped_i,_untyped_dispatcher)_cfg.json", "untyped_tests.main(tests__this)_cfg.json" ]
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped A::A(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"i1 = 0"},{"id":1,"text":"i1"},{"id":2,"text":"0"},{"id":3,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"}],"descriptions":[]}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped A::getOne(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"rec = new tests()"},{"id":1,"text":"rec"},{"id":2,"text":"new tests()"},{"id":3,"subNodes":[4,5],"text":"x = open(rec)"},{"id":4,"text":"x"},{"id":5,"subNodes":[6],"text":"open(rec)"},{"id":6,"text":"rec"},{"id":7,"subNodes":[8,9],"text":"<(x, 10)"},{"id":8,"text":"x"},{"id":9,"text":"10"},{"id":10,"subNodes":[11,12],"text":"x = +(x, 1)"},{"id":11,"text":"x"},{"id":12,"subNodes":[13,14],"text":"+(x, 1)"},{"id":13,"text":"x"},{"id":14,"text":"1"},{"id":15,"subNodes":[16],"text":"return 1"},{"id":16,"text":"1"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":10,"kind":"TrueEdge"},{"sourceId":7,"destId":15,"kind":"FalseEdge"},{"sourceId":10,"destId":7,"kind":"SequentialEdge"}],"descriptions":[]}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped A::getPositive(A* this, untyped i)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"<=(i, 0)"},{"id":1,"text":"i"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":"i = 1"},{"id":4,"text":"i"},{"id":5,"text":"1"},{"id":6,"subNodes":[7,8],"text":"i = 10"},{"id":7,"text":"i"},{"id":8,"text":"10"},{"id":9,"subNodes":[10],"text":"return i"},{"id":10,"text":"i"}],"edges":[{"sourceId":0,"destId":3,"kind":"TrueEdge"},{"sourceId":0,"destId":6,"kind":"FalseEdge"},{"sourceId":3,"destId":9,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"SequentialEdge"}],"descriptions":[]}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped A::identity(A* this, untyped i)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"i3 = 1"},{"id":1,"text":"i3"},{"id":2,"text":"1"},{"id":3,"subNodes":[4],"text":"return i"},{"id":4,"text":"i"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"}],"descriptions":[]}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped tests::helper(tests* this, untyped i, untyped dispatcher)","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"return identity(dispatcher, i)"},{"id":1,"subNodes":[2,3],"text":"identity(dispatcher, i)"},{"id":2,"text":"dispatcher"},{"id":3,"text":"i"}],"edges":[],"descriptions":[]}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped tests::main(tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"a = new A()"},{"id":1,"text":"a"},{"id":2,"text":"new A()"},{"id":3,"subNodes":[4,5],"text":"one = getPositive(a, getOne(a))"},{"id":4,"text":"one"},{"id":5,"subNodes":[6,7],"text":"getPositive(a, getOne(a))"},{"id":6,"text":"a"},{"id":7,"subNodes":[8],"text":"getOne(a)"},{"id":8,"text":"a"},{"id":9,"subNodes":[10,11],"text":"positive = identity(a, one)"},{"id":10,"text":"positive"},{"id":11,"subNodes":[12,13],"text":"identity(a, one)"},{"id":12,"text":"a"},{"id":13,"text":"one"},{"id":14,"subNodes":[15,16],"text":"minusone = -1"},{"id":15,"text":"minusone"},{"id":16,"text":"-1"},{"id":17,"subNodes":[18,19],"text":"negative = identity(a, minusone)"},{"id":18,"text":"negative"},{"id":19,"subNodes":[20,21],"text":"identity(a, minusone)"},{"id":20,"text":"a"},{"id":21,"text":"minusone"},{"id":22,"subNodes":[23,24],"text":"top = helper(this, one, a)"},{"id":23,"text":"top"},{"id":24,"subNodes":[25,26,27],"text":"helper(this, one, a)"},{"id":25,"text":"this"},{"id":26,"text":"one"},{"id":27,"text":"a"},{"id":28,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":14,"kind":"SequentialEdge"},{"sourceId":14,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":22,"kind":"SequentialEdge"},{"sourceId":22,"destId":28,"kind":"SequentialEdge"}],"descriptions":[]}
34 changes: 34 additions & 0 deletions lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,12 @@ public static enum GraphType {
*/
private GraphType analysisGraphs;

/**
* Whether or not the inputs {@link CFG}s to the analysis should be dumped
* in json format
*/
private boolean serializeInputs;

/**
* Whether or not the result of the analysis should be dumped in json
* format, if it is executed
Expand Down Expand Up @@ -307,6 +313,19 @@ public LiSAConfiguration setJsonOutput(boolean jsonOutput) {
return this;
}

/**
* Sets whether or not the the inputs {@link CFG}s to the analysis should be
* dumped in json format.
*
* @param serializeInputs whether or not the graphs should be produced
*
* @return the current (modified) configuration
*/
public LiSAConfiguration setSerializeInputs(boolean serializeInputs) {
this.serializeInputs = serializeInputs;
return this;
}

/**
* Sets whether or not the results of the analyses should be dumped in the
* form of json graphs.
Expand Down Expand Up @@ -443,6 +462,16 @@ public boolean isJsonOutput() {
return jsonOutput;
}

/**
* Yields whether or not the the inputs {@link CFG}s to the analysis should
* be dumped in json format.
*
* @return {@code true} if the graphs should be produced
*/
public boolean isSerializeInputs() {
return serializeInputs;
}

/**
* Yields whether or not the results of the analyses should be dumped in the
* form of json graphs.
Expand Down Expand Up @@ -504,6 +533,7 @@ public int hashCode() {
result = prime * result + (jsonOutput ? 1231 : 1237);
result = prime * result + ((openCallPolicy == null) ? 0 : openCallPolicy.hashCode());
result = prime * result + ((semanticChecks == null) ? 0 : semanticChecks.hashCode());
result = prime * result + (serializeInputs ? 1231 : 1237);
result = prime * result + (serializeResults ? 1231 : 1237);
result = prime * result + ((syntacticChecks == null) ? 0 : syntacticChecks.hashCode());
result = prime * result + wideningThreshold;
Expand Down Expand Up @@ -554,6 +584,8 @@ public boolean equals(Object obj) {
return false;
} else if (!semanticChecks.equals(other.semanticChecks))
return false;
if (serializeInputs != other.serializeInputs)
return false;
if (serializeResults != other.serializeResults)
return false;
if (syntacticChecks == null) {
Expand All @@ -577,6 +609,8 @@ public String toString() {
res.append("LiSA configuration:")
.append("\n workdir: ")
.append(String.valueOf(workdir))
.append("\n serialize inputs: ")
.append(serializeInputs)
.append("\n serialize results: ")
.append(serializeResults)
.append("\n analysis results format: ")
Expand Down
83 changes: 53 additions & 30 deletions lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
import java.util.Collection;
import java.util.IdentityHashMap;
import java.util.Map;
import java.util.concurrent.atomic.AtomicBoolean;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;

Expand Down Expand Up @@ -97,6 +98,23 @@ Collection<Warning> run(Application app, FileManager fileManager) {

Collection<CFG> allCFGs = app.getAllCFGs();

AtomicBoolean htmlViewer = new AtomicBoolean(false), subnodes = new AtomicBoolean(false);
if (conf.isSerializeInputs())
for (CFG cfg : IterationLogger.iterate(LOG, allCFGs, "Dumping input cfgs", "cfgs")) {
SerializableGraph graph = cfg.toSerializableGraph();
String filename = cfg.getDescriptor().getFullSignatureWithParNames() + "_cfg";

try {
fileManager.mkJsonFile(filename, writer -> graph.dump(writer));

dump(fileManager, filename, conf.getAnalysisGraphs(), graph, htmlViewer, subnodes);
} catch (IOException e) {
LOG.error("Exception while dumping the analysis results on {}",
cfg.getDescriptor().getFullSignature());
LOG.error(e);
}
}

CheckTool tool = new CheckTool();
if (!conf.getSyntacticChecks().isEmpty())
ChecksExecutor.executeAll(tool, app, conf.getSyntacticChecks());
Expand All @@ -119,7 +137,7 @@ Collection<Warning> run(Application app, FileManager fileManager) {
}

if (state != null) {
analyze(allCFGs, fileManager);
analyze(allCFGs, fileManager, htmlViewer, subnodes);
Map<CFG, Collection<CFGWithAnalysisResults<A, H, V, T>>> results = new IdentityHashMap<>(allCFGs.size());
for (CFG cfg : allCFGs)
results.put(cfg, interproc.getAnalysisResultsOf(cfg));
Expand All @@ -141,7 +159,8 @@ Collection<Warning> run(Application app, FileManager fileManager) {
return tool.getWarnings();
}

private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
private void analyze(Collection<CFG> allCFGs, FileManager fileManager, AtomicBoolean htmlViewer,
AtomicBoolean subnodes) {
A state = this.state.top();
TimerLogger.execAction(LOG, "Computing fixpoint over the whole program",
() -> {
Expand All @@ -158,7 +177,6 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
GraphType type = conf.getAnalysisGraphs();
if (conf.isSerializeResults() || type != GraphType.NONE) {
int nfiles = fileManager.createdFiles().size();
boolean htmlViewer = false, subnodes = false;

for (CFG cfg : IterationLogger.iterate(LOG, allCFGs, "Dumping analysis results", "cfgs"))
for (CFGWithAnalysisResults<A, H, V, T> result : interproc.getAnalysisResultsOf(cfg)) {
Expand All @@ -172,50 +190,55 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
if (conf.isSerializeResults())
fileManager.mkJsonFile(filename, writer -> graph.dump(writer));

switch (type) {
case DOT:
fileManager.mkDotFile(filename, writer -> graph.toDot().dump(writer));
break;
case GRAPHML:
fileManager.mkGraphmlFile(filename, writer -> graph.toGraphml(false).dump(writer));
break;
case GRAPHML_WITH_SUBNODES:
fileManager.mkGraphmlFile(filename, writer -> graph.toGraphml(true).dump(writer));
subnodes = true;
break;
case HTML:
fileManager.mkHtmlFile(filename, writer -> graph.toHtml(false, "results").dump(writer));
htmlViewer = true;
break;
case HTML_WITH_SUBNODES:
fileManager.mkHtmlFile(filename, writer -> graph.toHtml(true, "results").dump(writer));
htmlViewer = true;
subnodes = true;
break;
case NONE:
break;
default:
throw new AnalysisExecutionException("Unknown graph type: " + type);
}
dump(fileManager, filename, type, graph, htmlViewer, subnodes);
} catch (IOException e) {
LOG.error("Exception while dumping the analysis results on {}",
cfg.getDescriptor().getFullSignature());
LOG.error(e);
}
}

if (htmlViewer && fileManager.createdFiles().size() != nfiles)
if (htmlViewer.get() && fileManager.createdFiles().size() != nfiles)
try {
// we dumped at least one file: need to copy the
// javascript files
fileManager.generateHtmlViewerSupportFiles(subnodes);
fileManager.generateHtmlViewerSupportFiles(subnodes.get());
} catch (IOException e) {
LOG.error("Exception while generating supporting files for the html viwer");
LOG.error(e);
}
}
}

private static void dump(FileManager fileManager, String filename, GraphType type, SerializableGraph graph,
AtomicBoolean htmlViewer, AtomicBoolean subnodes) throws IOException {
switch (type) {
case DOT:
fileManager.mkDotFile(filename, writer -> graph.toDot().dump(writer));
break;
case GRAPHML:
fileManager.mkGraphmlFile(filename, writer -> graph.toGraphml(false).dump(writer));
break;
case GRAPHML_WITH_SUBNODES:
fileManager.mkGraphmlFile(filename, writer -> graph.toGraphml(true).dump(writer));
subnodes.set(true);
break;
case HTML:
fileManager.mkHtmlFile(filename, writer -> graph.toHtml(false, "results").dump(writer));
htmlViewer.set(true);
break;
case HTML_WITH_SUBNODES:
fileManager.mkHtmlFile(filename, writer -> graph.toHtml(true, "results").dump(writer));
htmlViewer.set(true);
subnodes.set(true);
break;
case NONE:
break;
default:
throw new AnalysisExecutionException("Unknown graph type: " + type);
}
}

private static void finalizeApp(Application app) {
for (Program p : app.getPrograms()) {
TypeSystem types = p.getTypes();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,13 @@ public static void ensureAllTested() {
assertTrue("Not all visualization types have been tested", notTested.isEmpty());
}

@Test
public void testInputSerialization() throws AnalysisSetupException {
LiSAConfiguration conf = config();
conf.setSerializeInputs(true);
perform("visualization", "inputs", "program.imp", conf);
}

@Test
public void testDOT() throws AnalysisSetupException {
LiSAConfiguration conf = config();
Expand Down

0 comments on commit 5c6628e

Please sign in to comment.