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/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); + } +}