Merge pull request #323 from lisa-analyzer/bug322

Fix and tests for #322

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"
+  }
+}

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"]]}}}]}

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"]]}}}]}

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

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

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");
 	}
 }

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

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 <A extends AbstractState<A>> AnalysisState<A> 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);
 	}
 }

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 <A extends AbstractState<A>> AnalysisState<A> 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 <A extends AbstractState<A>> AnalysisState<A> 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);

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