Minor refactorings

lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java

@@ -476,7 +476,6 @@ public void testIdentifierRewrite() throws SemanticException {
 		assertEquals(xAssign.rewrite(x, fakeProgramPoint, fakeOracle), expectedRewritten);
 
 		// y rewritten in x -> pp1 = {y}
-		// TODO to verify
 		assertEquals(xAssign.rewrite(y, fakeProgramPoint, fakeOracle), new ExpressionSet(y));
 	}
 

lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/ContainsTest.java

@@ -291,7 +291,6 @@ public void test12() throws SemanticException {
 				t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle));
 	}
 
-	// TODO to check
 	@Test
 	public void test13() throws SemanticException {
 		Tarsis t1 = new Tarsis(RegexAutomaton.string("ba"));

lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/DataflowAnalysesTest.java

@@ -0,0 +1,74 @@
+package it.unive.lisa.cron;
+
+import it.unive.lisa.AnalysisTestExecutor;
+import it.unive.lisa.CronConfiguration;
+import it.unive.lisa.DefaultConfiguration;
+import it.unive.lisa.analysis.dataflow.AvailableExpressions;
+import it.unive.lisa.analysis.dataflow.ConstantPropagation;
+import it.unive.lisa.analysis.dataflow.DefiniteDataflowDomain;
+import it.unive.lisa.analysis.dataflow.PossibleDataflowDomain;
+import it.unive.lisa.analysis.dataflow.ReachingDefinitions;
+import it.unive.lisa.conf.LiSAConfiguration.GraphType;
+import it.unive.lisa.interprocedural.BackwardModularWorstCaseAnalysis;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+public class DataflowAnalysesTest extends AnalysisTestExecutor {
+
+	@Test
+	public void testAvailableExpressions() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new DefiniteDataflowDomain<>(new AvailableExpressions()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.testDir = "available-expressions";
+		conf.programFile = "available-expressions.imp";
+		perform(conf);
+	}
+
+	@Test
+	public void testConstantPropagation() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new DefiniteDataflowDomain<>(new ConstantPropagation()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.testDir = "constant-propagation-df";
+		conf.programFile = "constant-propagation.imp";
+		perform(conf);
+	}
+
+	@Test
+	public void testReachingDefinitions() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new PossibleDataflowDomain<>(new ReachingDefinitions()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.testDir = "reaching-definitions";
+		conf.programFile = "reaching-definitions.imp";
+		perform(conf);
+	}
+
+	@Test
+	@Ignore
+	public void testLiveness() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.interproceduralAnalysis = new BackwardModularWorstCaseAnalysis<>();
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new DefiniteDataflowDomain<>(new AvailableExpressions()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.testDir = "liveness";
+		conf.programFile = "liveness.imp";
+		conf.analysisGraphs = GraphType.HTML_WITH_SUBNODES;
+		conf.forceUpdate = true;
+		perform(conf);
+	}
+}

lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NonInterferenceTest.java → lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InformationFlowTest.java

@@ -1,7 +1,12 @@
 package it.unive.lisa.cron;
 
+import java.util.Collection;
+
+import org.junit.Test;
+
 import it.unive.lisa.AnalysisTestExecutor;
 import it.unive.lisa.CronConfiguration;
+import it.unive.lisa.DefaultConfiguration;
 import it.unive.lisa.analysis.AnalysisState;
 import it.unive.lisa.analysis.AnalyzedCFG;
 import it.unive.lisa.analysis.SemanticException;
@@ -10,22 +15,124 @@
 import it.unive.lisa.analysis.nonInterference.NonInterference;
 import it.unive.lisa.analysis.nonrelational.inference.InferenceSystem;
 import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.analysis.taint.BaseTaint;
+import it.unive.lisa.analysis.taint.Taint;
+import it.unive.lisa.analysis.taint.ThreeLevelsTaint;
 import it.unive.lisa.analysis.types.InferredTypes;
 import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults;
 import it.unive.lisa.checks.semantic.SemanticCheck;
+import it.unive.lisa.interprocedural.ReturnTopPolicy;
 import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
 import it.unive.lisa.interprocedural.context.ContextBasedAnalysis;
 import it.unive.lisa.interprocedural.context.FullStackToken;
 import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.CodeMember;
+import it.unive.lisa.program.cfg.Parameter;
 import it.unive.lisa.program.cfg.statement.Assignment;
 import it.unive.lisa.program.cfg.statement.Expression;
 import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.program.cfg.statement.call.CFGCall;
+import it.unive.lisa.program.cfg.statement.call.Call;
+import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.ValueExpression;
-import java.util.Collection;
-import org.junit.Test;
 
-public class NonInterferenceTest extends AnalysisTestExecutor {
+public class InformationFlowTest extends AnalysisTestExecutor {
+
+	@Test
+	public void testTaint() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new ValueEnvironment<>(new Taint()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.serializeResults = true;
+		conf.openCallPolicy = ReturnTopPolicy.INSTANCE;
+		conf.callGraph = new RTACallGraph();
+		conf.interproceduralAnalysis = new ContextBasedAnalysis<>();
+		conf.semanticChecks.add(new TaintCheck<>());
+		conf.testDir = "taint";
+		conf.testSubDir = "2val";
+		conf.programFile = "taint.imp";
+		conf.hotspots = st -> st instanceof Expression && ((Expression) st).getParentStatement() instanceof Call;
+		perform(conf);
+	}
+
+	@Test
+	public void testThreeLevelsTaint() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new ValueEnvironment<>(new ThreeLevelsTaint()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.serializeResults = true;
+		conf.openCallPolicy = ReturnTopPolicy.INSTANCE;
+		conf.callGraph = new RTACallGraph();
+		conf.interproceduralAnalysis = new ContextBasedAnalysis<>();
+		conf.semanticChecks.add(new TaintCheck<>());
+		conf.testDir = "taint";
+		conf.testSubDir = "3val";
+		conf.programFile = "taint.imp";
+		conf.hotspots = st -> st instanceof Expression && ((Expression) st).getParentStatement() instanceof Call;
+		perform(conf);
+	}
+
+	private static class TaintCheck<T extends BaseTaint<T>>
+			implements
+			SemanticCheck<
+					SimpleAbstractState<MonolithicHeap, ValueEnvironment<T>, TypeEnvironment<InferredTypes>>> {
+
+		@Override
+		public boolean visit(
+				CheckToolWithAnalysisResults<
+						SimpleAbstractState<MonolithicHeap, ValueEnvironment<T>, TypeEnvironment<InferredTypes>>> tool,
+				CFG graph,
+				Statement node) {
+			if (!(node instanceof UnresolvedCall))
+				return true;
+
+			UnresolvedCall call = (UnresolvedCall) node;
+
+			try {
+				for (AnalyzedCFG<
+						SimpleAbstractState<
+								MonolithicHeap,
+								ValueEnvironment<T>,
+								TypeEnvironment<InferredTypes>>> result : tool.getResultOf(call.getCFG())) {
+
+					Call resolved = (Call) tool.getResolvedVersion(call, result);
+					if (resolved instanceof CFGCall) {
+						CFGCall cfg = (CFGCall) resolved;
+						for (CodeMember n : cfg.getTargets()) {
+							Parameter[] parameters = n.getDescriptor().getFormals();
+							for (int i = 0; i < parameters.length; i++)
+								if (parameters[i].getAnnotations().contains(BaseTaint.CLEAN_MATCHER)) {
+									AnalysisState<SimpleAbstractState<MonolithicHeap, ValueEnvironment<T>,
+											TypeEnvironment<InferredTypes>>> post = result
+													.getAnalysisStateAfter(call.getParameters()[i]);
+									for (SymbolicExpression e : post.getState().rewrite(post.getComputedExpressions(),
+											node, post.getState())) {
+										T stack = post
+												.getState()
+												.getValueState()
+												.eval((ValueExpression) e, node, post.getState());
+										if (stack.isAlwaysTainted())
+											tool.warnOn(call, "Parameter " + i + " is always tainted");
+										else if (stack.isPossiblyTainted())
+											tool.warnOn(call, "Parameter " + i + " is possibly tainted");
+									}
+								}
+						}
+					}
+				}
+			} catch (SemanticException e1) {
+				e1.printStackTrace();
+			}
+
+			return true;
+		}
+	}
 
 	@Test
 	public void testConfidentialityNI() {

lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/ContextSensitiveAnalysisTest.java → lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/InterproceduralAnalysesTest.java

@@ -7,12 +7,47 @@
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
 import it.unive.lisa.analysis.numeric.Interval;
 import it.unive.lisa.analysis.numeric.Sign;
+import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis;
+import it.unive.lisa.interprocedural.callgraph.CHACallGraph;
 import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
 import it.unive.lisa.interprocedural.context.ContextBasedAnalysis;
 import it.unive.lisa.interprocedural.context.FullStackToken;
+
 import org.junit.Test;
 
-public class ContextSensitiveAnalysisTest extends AnalysisTestExecutor {
+public class InterproceduralAnalysesTest extends AnalysisTestExecutor {
+
+	@Test
+	public void testWorstCaseCHACallGraph() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new ValueEnvironment<>(new Sign()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.interproceduralAnalysis = new ModularWorstCaseAnalysis<>();
+		conf.callGraph = new CHACallGraph();
+		conf.testDir = "interprocedural";
+		conf.testSubDir = "CHA";
+		conf.programFile = "program.imp";
+		perform(conf);
+	}
+
+	@Test
+	public void testWorstCaseRTACallGraph() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+				DefaultConfiguration.defaultHeapDomain(),
+				new ValueEnvironment<>(new Sign()),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.interproceduralAnalysis = new ModularWorstCaseAnalysis<>();
+		conf.callGraph = new RTACallGraph();
+		conf.testDir = "interprocedural";
+		conf.testSubDir = "RTA";
+		conf.programFile = "program.imp";
+		perform(conf);
+	}
 
 	@Test
 	public void testRTAContextSensitive1() {

lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/PointBasedHeapTest.java → lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/MemoryAbstractionsTest.java

@@ -3,11 +3,26 @@
 import it.unive.lisa.AnalysisTestExecutor;
 import it.unive.lisa.CronConfiguration;
 import it.unive.lisa.DefaultConfiguration;
+import it.unive.lisa.analysis.heap.TypeBasedHeap;
 import it.unive.lisa.analysis.heap.pointbased.FieldSensitivePointBasedHeap;
 import it.unive.lisa.analysis.heap.pointbased.PointBasedHeap;
+
 import org.junit.Test;
 
-public class PointBasedHeapTest extends AnalysisTestExecutor {
+public class MemoryAbstractionsTest extends AnalysisTestExecutor {
+
+	@Test
+	public void testTypeBasedHeap() {
+		CronConfiguration conf = new CronConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+				new TypeBasedHeap(),
+				DefaultConfiguration.defaultValueDomain(),
+				DefaultConfiguration.defaultTypeDomain());
+		conf.testDir = "heap/type-based-heap";
+		conf.programFile = "program.imp";
+		perform(conf);
+	}
 
 	@Test
 	public void fieldInsensitivePointBasedHeapTest() {