From 28d81160c39bbb2992ae9438369b3e745a9907b6 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Tue, 18 Feb 2025 11:35:36 +0100 Subject: [PATCH 1/2] Fix and tests for #322 --- .../dataflow/issue322/report.json | 38 ++++ ...untyped_~LiSAProgram.foo()_-309356675.json | 1 + .../issue322/untyped_~LiSAProgram.main().json | 1 + .../dataflow/ConstantPropagation.java | 9 +- .../dataflow/ReachingDefinitions.java | 10 +- .../it/unive/lisa/AnalysisTestExecutor.java | 30 ++- .../java/it/unive/lisa/analysis/Issues.java | 203 ++++++++++++++++++ .../unive/lisa/cron/DataflowAnalysesTest.java | 113 ++++++++++ .../cfg/statement/global/AccessGlobal.java | 4 +- .../global/AccessInstanceGlobal.java | 6 +- .../java/it/unive/lisa/program/Global.java | 10 +- .../lisa/symbolic/value/GlobalVariable.java | 81 +++++++ 12 files changed, 482 insertions(+), 24 deletions(-) create mode 100644 lisa/lisa-analyses/imp-testcases/dataflow/issue322/report.json create mode 100644 lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.foo()_-309356675.json create mode 100644 lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.main().json create mode 100644 lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java create mode 100644 lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/GlobalVariable.java diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/issue322/report.json b/lisa/lisa-analyses/imp-testcases/dataflow/issue322/report.json new file mode 100644 index 000000000..7e28fd59e --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/dataflow/issue322/report.json @@ -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" + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.foo()_-309356675.json b/lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.foo()_-309356675.json new file mode 100644 index 000000000..5bd893818 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.foo()_-309356675.json @@ -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"]]}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.main().json b/lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.main().json new file mode 100644 index 000000000..10b6c2008 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/dataflow/issue322/untyped_~LiSAProgram.main().json @@ -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"]]}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java index 127de3326..17b2cb4da 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java @@ -7,7 +7,6 @@ import it.unive.lisa.symbolic.value.BinaryExpression; import it.unive.lisa.symbolic.value.Constant; import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.symbolic.value.OutOfScopeIdentifier; import it.unive.lisa.symbolic.value.UnaryExpression; import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.symbolic.value.operator.AdditionOperator; @@ -212,9 +211,13 @@ public ConstantPropagation pushScope( public ConstantPropagation popScope( ScopeToken scope) throws SemanticException { - if (!(id instanceof OutOfScopeIdentifier)) + if (!id.canBeScoped()) return this; - return new ConstantPropagation(((OutOfScopeIdentifier) id).popScope(scope), constant); + SymbolicExpression popped = id.popScope(scope); + if (popped == null) + return null; + + return new ConstantPropagation((Identifier) popped, constant); } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ReachingDefinitions.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ReachingDefinitions.java index c1a46f9b0..250e65928 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ReachingDefinitions.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/dataflow/ReachingDefinitions.java @@ -3,8 +3,8 @@ import it.unive.lisa.analysis.ScopeToken; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.symbolic.value.OutOfScopeIdentifier; import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.util.representation.ListRepresentation; import it.unive.lisa.util.representation.StringRepresentation; @@ -144,9 +144,13 @@ public ReachingDefinitions pushScope( public ReachingDefinitions popScope( ScopeToken scope) throws SemanticException { - if (!(variable instanceof OutOfScopeIdentifier)) + if (!variable.canBeScoped()) + return this; + + SymbolicExpression popped = variable.popScope(scope); + if (popped == null) return null; - return new ReachingDefinitions(((OutOfScopeIdentifier) variable).popScope(scope), programPoint); + return new ReachingDefinitions((Identifier) popped, programPoint); } } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/AnalysisTestExecutor.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/AnalysisTestExecutor.java index 0e0f5254d..a8cf8f3ff 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/AnalysisTestExecutor.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/AnalysisTestExecutor.java @@ -30,8 +30,8 @@ public abstract class AnalysisTestExecutor { - protected static final String EXPECTED_RESULTS_DIR = "imp-testcases"; - protected static final String ACTUAL_RESULTS_DIR = "test-outputs"; + public static final String EXPECTED_RESULTS_DIR = "imp-testcases"; + public static final String ACTUAL_RESULTS_DIR = "test-outputs"; /** * Performs a test, running an analysis. The test will fail if: @@ -82,22 +82,30 @@ public void perform( public void perform( CronConfiguration conf, boolean allMethods) { + Objects.requireNonNull(conf); + Objects.requireNonNull(conf.testDir); + Objects.requireNonNull(conf.programFile); + Path expectedPath = Paths.get(EXPECTED_RESULTS_DIR, conf.testDir); + Path target = Paths.get(expectedPath.toString(), conf.programFile); + Program program = readProgram(target, allMethods); + perform(conf, program); + } + + public void perform( + CronConfiguration conf, + Program program) { String testMethod = getCaller(); System.out.println("### Testing " + testMethod); Objects.requireNonNull(conf); Objects.requireNonNull(conf.testDir); - Objects.requireNonNull(conf.programFile); Path expectedPath = Paths.get(EXPECTED_RESULTS_DIR, conf.testDir); Path actualPath = Paths.get(ACTUAL_RESULTS_DIR, conf.testDir); - Path target = Paths.get(expectedPath.toString(), conf.programFile); if (conf.testSubDir != null) { expectedPath = Paths.get(expectedPath.toString(), conf.testSubDir); actualPath = Paths.get(actualPath.toString(), conf.testSubDir); } - Program program = readProgram(target, allMethods); - setupWorkdir(conf, actualPath); conf.jsonOutput = true; @@ -128,7 +136,8 @@ public void perform( // we parse the program again since the analysis might have // finalized it or modified it, and we want to start from scratch - program = readProgram(target, allMethods); + // TODO: might need to enable this again + // program = readProgram(target, allMethods); conf.optimize = true; actualPath = Paths.get(actualPath.toString(), "optimized"); @@ -399,6 +408,11 @@ private String getCaller() { // 2: it.unive.lisa.test.AnalysisTest.getCaller() // 3: it.unive.lisa.test.AnalysisTest.perform() // 4: caller - return trace[4].getClassName() + "::" + trace[4].getMethodName(); + for (StackTraceElement e : trace) { + if (!e.getClassName().equals("java.lang.Thread") && !e.getClassName().equals(getClass().getName())) + return e.getClassName() + "::" + e.getMethodName(); + } + + throw new AnalysisException("Unable to find caller test method"); } } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java new file mode 100644 index 000000000..2ca7369a0 --- /dev/null +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java @@ -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(); + } + } +} diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java index b73c49461..dac3b6783 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java @@ -9,7 +9,27 @@ import it.unive.lisa.analysis.dataflow.Liveness; import it.unive.lisa.analysis.dataflow.PossibleDataflowDomain; import it.unive.lisa.analysis.dataflow.ReachingDefinitions; +import it.unive.lisa.imp.IMPFeatures; +import it.unive.lisa.imp.types.IMPTypeSystem; import it.unive.lisa.interprocedural.BackwardModularWorstCaseAnalysis; +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 java.util.Arrays; import org.junit.Test; public class DataflowAnalysesTest extends AnalysisTestExecutor { @@ -67,4 +87,97 @@ public void testLiveness() { conf.compareWithOptimization = false; perform(conf); } + + @Test + public void testIssue322() { + Program program = buildProgram(); + + CronConfiguration conf = new CronConfiguration(); + conf.abstractState = DefaultConfiguration.simpleState( + DefaultConfiguration.defaultHeapDomain(), + new PossibleDataflowDomain<>(new ReachingDefinitions()), + DefaultConfiguration.defaultTypeDomain()); + conf.interproceduralAnalysis = new ContextBasedAnalysis<>(FullStackToken.getSingleton()); + conf.optimize = false; + conf.serializeResults = true; + conf.testDir = "dataflow/issue322"; + + perform(conf, program); + } + + private int line = 1; + + private Program buildProgram() { + Program program = new Program(new IMPFeatures(), new IMPTypeSystem()); + 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); + } } \ No newline at end of file diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java index 2559d2400..a959a17d5 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java @@ -13,7 +13,7 @@ import it.unive.lisa.program.cfg.edge.Edge; import it.unive.lisa.program.cfg.statement.Expression; import it.unive.lisa.program.cfg.statement.Statement; -import it.unive.lisa.symbolic.value.Variable; +import it.unive.lisa.symbolic.value.GlobalVariable; import it.unive.lisa.util.datastructures.graph.GraphVisitor; /** @@ -137,7 +137,7 @@ public > AnalysisState forwardSemantics( // unit globals are unique, we can directly access those return entryState.smallStepSemantics( - new Variable(target.getStaticType(), toString(), target.getAnnotations(), getLocation()), + new GlobalVariable(target.getStaticType(), toString(), target.getAnnotations(), getLocation()), this); } } diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java index a777c83e5..230a34985 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java @@ -18,7 +18,7 @@ import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; -import it.unive.lisa.symbolic.value.Variable; +import it.unive.lisa.symbolic.value.GlobalVariable; import it.unive.lisa.type.Type; import it.unive.lisa.type.Untyped; import java.util.HashSet; @@ -141,7 +141,7 @@ public > AnalysisState fwdUnarySemantics( if (seen.add(unit)) { Global global = cu.getInstanceGlobal(target, false); if (global != null) { - Variable var = global.toSymbolicVariable(loc); + GlobalVariable var = global.toSymbolicVariable(loc); AccessChild access = new AccessChild(var.getStaticType(), container, var, loc); result = result.lub(state.smallStepSemantics(access, this)); atLeastOne = true; @@ -162,7 +162,7 @@ public > AnalysisState fwdUnarySemantics( return state.bottom(); Type rectype = Type.commonSupertype(rectypes, Untyped.INSTANCE); - Variable var = new Variable(Untyped.INSTANCE, target, new Annotations(), getLocation()); + GlobalVariable var = new GlobalVariable(Untyped.INSTANCE, target, new Annotations(), getLocation()); HeapDereference container = new HeapDereference(rectype, expr, getLocation()); AccessChild access = new AccessChild(Untyped.INSTANCE, container, var, getLocation()); return state.smallStepSemantics(access, this); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/Global.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/Global.java index 85cf3ca15..c2e8c13aa 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/Global.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/Global.java @@ -4,7 +4,7 @@ import it.unive.lisa.program.annotations.Annotation; import it.unive.lisa.program.annotations.Annotations; import it.unive.lisa.program.cfg.CodeLocation; -import it.unive.lisa.symbolic.value.Variable; +import it.unive.lisa.symbolic.value.GlobalVariable; import it.unive.lisa.type.Type; import it.unive.lisa.type.Untyped; import java.util.Objects; @@ -224,15 +224,15 @@ public void addAnnotation( } /** - * Creates a {@link Variable} that represent this global, that can be used - * by {@link SemanticDomain}s to reference it. + * Creates a {@link GlobalVariable} that represent this global, that can be + * used by {@link SemanticDomain}s to reference it. * * @param where the location where the variable will be generated * * @return the variable representing this parameter */ - public Variable toSymbolicVariable( + public GlobalVariable toSymbolicVariable( CodeLocation where) { - return new Variable(staticType, name, annotations, where); + return new GlobalVariable(staticType, name, annotations, where); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/GlobalVariable.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/GlobalVariable.java new file mode 100644 index 000000000..bd219dc43 --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/GlobalVariable.java @@ -0,0 +1,81 @@ +package it.unive.lisa.symbolic.value; + +import it.unive.lisa.analysis.ScopeToken; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.program.annotations.Annotations; +import it.unive.lisa.program.cfg.CodeLocation; +import it.unive.lisa.symbolic.ExpressionVisitor; +import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.type.Type; + +/** + * An identifier of a global variable. This can be treated as a regular + * variable, except that it cannot be scoped. + * + * @author Luca Negrini + */ +public class GlobalVariable extends Identifier { + + /** + * Builds the variable. + * + * @param staticType the static type of this variable + * @param name the name of the variable + * @param location the code location of the statement that has generated + * this variable + */ + public GlobalVariable( + Type staticType, + String name, + CodeLocation location) { + this(staticType, name, new Annotations(), location); + } + + /** + * Builds the variable with annotations. + * + * @param staticType the static type of this variable + * @param name the name of the variable + * @param annotations the annotations of this variable + * @param location the code location of the statement that has generated + * this variable + */ + public GlobalVariable( + Type staticType, + String name, + Annotations annotations, + CodeLocation location) { + super(staticType, name, false, annotations, location); + } + + @Override + public boolean canBeScoped() { + return false; + } + + @Override + public SymbolicExpression pushScope( + ScopeToken token) { + return this; + } + + @Override + public SymbolicExpression popScope( + ScopeToken token) + throws SemanticException { + return this; + } + + @Override + public String toString() { + return getName(); + } + + @Override + public T accept( + ExpressionVisitor visitor, + Object... params) + throws SemanticException { + return visitor.visit(this, params); + } +} From 6d2475d6ff8d360531cbeb29540ed160ded6115d Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Tue, 18 Feb 2025 11:44:21 +0100 Subject: [PATCH 2/2] Cleanup of test files --- .../java/it/unive/lisa/analysis/Issues.java | 203 ------------------ 1 file changed, 203 deletions(-) delete mode 100644 lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java deleted file mode 100644 index 2ca7369a0..000000000 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/Issues.java +++ /dev/null @@ -1,203 +0,0 @@ -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(); - } - } -}