-
Notifications
You must be signed in to change notification settings - Fork 33
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
12 changed files
with
482 additions
and
24 deletions.
There are no files selected for viewing
38 changes: 38 additions & 0 deletions
38
lisa/lisa-analyses/imp-testcases/dataflow/issue322/report.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,38 @@ | ||
| { | ||
| "warnings" : [ ], | ||
| "files" : [ "report.json", "untyped_~LiSAProgram.foo()_-309356675.json", "untyped_~LiSAProgram.main().json" ], | ||
| "info" : { | ||
| "cfgs" : "2", | ||
| "duration" : "420ms", | ||
| "end" : "2025-02-18T11:31:57.663+01:00", | ||
| "expressions" : "6", | ||
| "files" : "2", | ||
| "globals" : "1", | ||
| "members" : "2", | ||
| "programs" : "1", | ||
| "start" : "2025-02-18T11:31:57.243+01:00", | ||
| "statements" : "6", | ||
| "units" : "0", | ||
| "version" : "0.1b8", | ||
| "warnings" : "0" | ||
| }, | ||
| "configuration" : { | ||
| "analysisGraphs" : "NONE", | ||
| "descendingPhaseType" : "NONE", | ||
| "dumpForcesUnwinding" : "false", | ||
| "fixpointWorkingSet" : "OrderBasedWorkingSet", | ||
| "glbThreshold" : "5", | ||
| "hotspots" : "unset", | ||
| "jsonOutput" : "true", | ||
| "openCallPolicy" : "WorstCasePolicy", | ||
| "optimize" : "false", | ||
| "recursionWideningThreshold" : "5", | ||
| "semanticChecks" : "", | ||
| "serializeInputs" : "false", | ||
| "serializeResults" : "true", | ||
| "syntacticChecks" : "", | ||
| "useWideningPoints" : "true", | ||
| "wideningThreshold" : "5", | ||
| "workdir" : "test-outputs/dataflow/issue322" | ||
| } | ||
| } |
1 change: 1 addition & 0 deletions
1
.../lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.foo()_-309356675.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"name":"untyped ~LiSAProgram::foo()","description":"['program':6:1]","nodes":[{"id":0,"subNodes":[1,2],"text":"~LiSAProgram::g = 2"},{"id":1,"text":"~LiSAProgram::g"},{"id":2,"text":"2"},{"id":3,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["~LiSAProgram::g"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 2"]]}}},{"nodeId":1,"description":{"expressions":["~LiSAProgram::g"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 1"]]}}},{"nodeId":2,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 1"]]}}},{"nodeId":3,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 2"]]}}}]} |
1 change: 1 addition & 0 deletions
1
lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.main().json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"name":"untyped ~LiSAProgram::main()","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"~LiSAProgram::g = 1"},{"id":1,"text":"~LiSAProgram::g"},{"id":2,"text":"1"},{"id":3,"text":"foo()"},{"id":4,"subNodes":[5,6],"text":"~LiSAProgram::g = 3"},{"id":5,"text":"~LiSAProgram::g"},{"id":6,"text":"3"},{"id":7,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":7,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["~LiSAProgram::g"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 1"]]}}},{"nodeId":1,"description":{"expressions":["~LiSAProgram::g"],"state":{"heap":"monolith","type":"#TOP#","value":[]}}},{"nodeId":2,"description":{"expressions":["1"],"state":{"heap":"monolith","type":"#TOP#","value":[]}}},{"nodeId":3,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 2"]]}}},{"nodeId":4,"description":{"expressions":["~LiSAProgram::g"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 3"]]}}},{"nodeId":5,"description":{"expressions":["~LiSAProgram::g"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 2"]]}}},{"nodeId":6,"description":{"expressions":["3"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 2"]]}}},{"nodeId":7,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"~LiSAProgram::g":["int32"]},"value":[["~LiSAProgram::g","~LiSAProgram::g = 3"]]}}}]} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
203 changes: 203 additions & 0 deletions
203
lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,203 @@ | ||
| package it.unive.lisa.analysis; | ||
|
|
||
| import it.unive.lisa.AnalysisTestExecutor; | ||
| import it.unive.lisa.DefaultConfiguration; | ||
| import it.unive.lisa.LiSA; | ||
| import it.unive.lisa.analysis.dataflow.PossibleDataflowDomain; | ||
| import it.unive.lisa.analysis.dataflow.ReachingDefinitions; | ||
| import it.unive.lisa.conf.LiSAConfiguration; | ||
| import it.unive.lisa.conf.LiSAConfiguration.GraphType; | ||
| import it.unive.lisa.interprocedural.context.ContextBasedAnalysis; | ||
| import it.unive.lisa.interprocedural.context.FullStackToken; | ||
| import it.unive.lisa.program.Global; | ||
| import it.unive.lisa.program.Program; | ||
| import it.unive.lisa.program.SourceCodeLocation; | ||
| import it.unive.lisa.program.cfg.CFG; | ||
| import it.unive.lisa.program.cfg.CodeLocation; | ||
| import it.unive.lisa.program.cfg.CodeMemberDescriptor; | ||
| import it.unive.lisa.program.cfg.edge.SequentialEdge; | ||
| import it.unive.lisa.program.cfg.statement.Assignment; | ||
| import it.unive.lisa.program.cfg.statement.Expression; | ||
| import it.unive.lisa.program.cfg.statement.Ret; | ||
| import it.unive.lisa.program.cfg.statement.Statement; | ||
| import it.unive.lisa.program.cfg.statement.call.Call.CallType; | ||
| import it.unive.lisa.program.cfg.statement.call.UnresolvedCall; | ||
| import it.unive.lisa.program.cfg.statement.global.AccessGlobal; | ||
| import it.unive.lisa.program.cfg.statement.literal.Int32Literal; | ||
| import it.unive.lisa.program.language.LanguageFeatures; | ||
| import it.unive.lisa.program.language.hierarchytraversal.HierarcyTraversalStrategy; | ||
| import it.unive.lisa.program.language.hierarchytraversal.SingleInheritanceTraversalStrategy; | ||
| import it.unive.lisa.program.language.parameterassignment.ParameterAssigningStrategy; | ||
| import it.unive.lisa.program.language.parameterassignment.PythonLikeAssigningStrategy; | ||
| import it.unive.lisa.program.language.resolution.JavaLikeMatchingStrategy; | ||
| import it.unive.lisa.program.language.resolution.ParameterMatchingStrategy; | ||
| import it.unive.lisa.program.language.validation.BaseValidationLogic; | ||
| import it.unive.lisa.program.language.validation.ProgramValidationLogic; | ||
| import it.unive.lisa.program.type.BoolType; | ||
| import it.unive.lisa.program.type.Int32Type; | ||
| import it.unive.lisa.program.type.StringType; | ||
| import it.unive.lisa.type.BooleanType; | ||
| import it.unive.lisa.type.NumericType; | ||
| import it.unive.lisa.type.Type; | ||
| import it.unive.lisa.type.TypeSystem; | ||
| import java.util.Arrays; | ||
| import org.junit.Test; | ||
|
|
||
| public class Issues { | ||
|
|
||
| @Test | ||
| public void issue322() { | ||
| var program = buildProgram(); | ||
|
|
||
| LiSAConfiguration conf = new DefaultConfiguration(); | ||
| var valueDomain = new PossibleDataflowDomain<>(new ReachingDefinitions()); | ||
| var heapDomain = DefaultConfiguration.defaultHeapDomain(); | ||
| var typeDomain = DefaultConfiguration.defaultTypeDomain(); | ||
| conf.abstractState = DefaultConfiguration.simpleState(heapDomain, valueDomain, typeDomain); | ||
| conf.interproceduralAnalysis = new ContextBasedAnalysis<>(FullStackToken.getSingleton()); | ||
| conf.optimize = false; // Simplify collecting results | ||
| conf.analysisGraphs = GraphType.HTML; | ||
| conf.serializeInputs = false; | ||
| conf.serializeResults = true; | ||
| conf.jsonOutput = true; | ||
| conf.workdir = AnalysisTestExecutor.ACTUAL_RESULTS_DIR + "/issue322"; | ||
|
|
||
| LiSA lisa = new LiSA(conf); | ||
| lisa.run(program); | ||
|
|
||
| CFG main = program.getEntryPoints().iterator().next(); | ||
| for (AnalyzedCFG<?> result : conf.interproceduralAnalysis.getAnalysisResultsOf(main)) { | ||
| for (Statement node : main.getNodes()) { | ||
| AnalysisState<?> analysisState = result.getAnalysisStateAfter(node); | ||
| SimpleAbstractState<?, ?, ?> state = (SimpleAbstractState<?, ?, ?>) analysisState.getState(); | ||
| PossibleDataflowDomain<?> valueState = (PossibleDataflowDomain<?>) state.getValueState(); | ||
| System.out.println(String.format("After %s, a reaching definition is %s", node, valueState)); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| private int line = 1; | ||
|
|
||
| private Program buildProgram() { | ||
| Program program = new Program(new ExampleFeatures(), new ExampleTypeSystem()); | ||
| Global g = new Global(getNewLocation(), program, "g", false); | ||
| program.addGlobal(g); | ||
| String calleeName = "foo"; | ||
|
|
||
| // Build main CFG | ||
| var cfg1 = new CFG(new CodeMemberDescriptor(getNewLocation(), program, false, "main")); | ||
| Statement s1 = buildAssign(cfg1, buildAccess(cfg1, g), buildInt32Literal(cfg1, 1)); | ||
| Statement s3 = buildUnresolvedCall(cfg1, calleeName); | ||
| Statement s5 = buildAssign(cfg1, buildAccess(cfg1, g), buildInt32Literal(cfg1, 3)); | ||
| Statement s7 = buildRet(cfg1); | ||
| addAsSequence(cfg1, s1, s3, s5, s7); | ||
|
|
||
| // Build callee CFG | ||
| var cfg2 = new CFG(new CodeMemberDescriptor(getNewLocation(), program, false, calleeName)); | ||
| Statement s8 = buildAssign(cfg2, buildAccess(cfg2, g), buildInt32Literal(cfg2, 2)); | ||
| Statement s9 = buildRet(cfg2); | ||
| addAsSequence(cfg2, s8, s9); | ||
|
|
||
| program.addCodeMember(cfg1); | ||
| program.addCodeMember(cfg2); | ||
| program.addEntryPoint(cfg1); | ||
|
|
||
| return program; | ||
| } | ||
|
|
||
| private void addAsSequence( | ||
| CFG cfg, | ||
| Statement... statements) { | ||
| Statement prev = null; | ||
| for (Statement s : Arrays.asList(statements)) { | ||
| cfg.addNode(s, prev == null); | ||
| if (prev != null) { | ||
| cfg.addEdge(new SequentialEdge(prev, s)); | ||
| } | ||
| prev = s; | ||
| } | ||
| } | ||
|
|
||
| private Statement buildAssign( | ||
| CFG cfg, | ||
| Expression target, | ||
| Expression source) { | ||
| return new Assignment(cfg, getNewLocation(), target, source); | ||
| } | ||
|
|
||
| private Statement buildUnresolvedCall( | ||
| CFG cfg, | ||
| String targetName) { | ||
| return new UnresolvedCall(cfg, getNewLocation(), CallType.STATIC, (String) null, targetName); | ||
| } | ||
|
|
||
| private Statement buildRet( | ||
| CFG cfg) { | ||
| return new Ret(cfg, getNewLocation()); | ||
| } | ||
|
|
||
| private Expression buildInt32Literal( | ||
| CFG cfg, | ||
| int value) { | ||
| return new Int32Literal(cfg, getNewLocation(), value); | ||
| } | ||
|
|
||
| private Expression buildAccess( | ||
| CFG cfg, | ||
| Global g) { | ||
| return new AccessGlobal(cfg, getNewLocation(), g.getContainer(), g); | ||
| } | ||
|
|
||
| private CodeLocation getNewLocation() { | ||
| return new SourceCodeLocation("program", line++, 1); | ||
| } | ||
|
|
||
| /** Adapted from IMPFeatures */ | ||
| private static class ExampleFeatures extends LanguageFeatures { | ||
|
|
||
| @Override | ||
| public ParameterMatchingStrategy getMatchingStrategy() { | ||
| return JavaLikeMatchingStrategy.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public HierarcyTraversalStrategy getTraversalStrategy() { | ||
| return SingleInheritanceTraversalStrategy.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public ParameterAssigningStrategy getAssigningStrategy() { | ||
| return PythonLikeAssigningStrategy.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public ProgramValidationLogic getProgramValidationLogic() { | ||
| return new BaseValidationLogic(); | ||
| } | ||
| } | ||
|
|
||
| /** Adapted from IMPTypeSystem */ | ||
| private static class ExampleTypeSystem extends TypeSystem { | ||
|
|
||
| @Override | ||
| public BooleanType getBooleanType() { | ||
| return BoolType.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public StringType getStringType() { | ||
| return StringType.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public NumericType getIntegerType() { | ||
| return Int32Type.INSTANCE; | ||
| } | ||
|
|
||
| @Override | ||
| public boolean canBeReferenced( | ||
| Type type) { | ||
| return type.isInMemoryType(); | ||
| } | ||
| } | ||
| } |
Oops, something went wrong.