Adding FixpointInfo #287

lisa-analyzer · Sep 11, 2023 · b44d850 · b44d850
1 parent 2f14160
commit b44d850
Show file tree

Hide file tree

Showing 20 changed files with 570 additions and 109 deletions.
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java
@@ -95,7 +95,7 @@ public AnalysisState<A> prepareEntryStateOfEntryPoint(AnalysisState<A> entryStat
 		}
 
 		// the stack has to be empty
-		return new AnalysisState<>(prepared.getState(), new ExpressionSet(), new SymbolAliasing());
+		return new AnalysisState<>(prepared.getState(), new ExpressionSet());
 	}
 
 	@Override

diff --git a/...sa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java b/...sa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java
@@ -5,6 +5,7 @@
 import it.unive.lisa.analysis.AbstractState;
 import it.unive.lisa.analysis.AnalysisState;
 import it.unive.lisa.analysis.AnalyzedCFG;
+import it.unive.lisa.analysis.FixpointInfo;
 import it.unive.lisa.analysis.OptimizedAnalyzedCFG;
 import it.unive.lisa.analysis.ScopeToken;
 import it.unive.lisa.analysis.SemanticException;
@@ -419,7 +420,7 @@ public AnalysisState<A> getAbstractResultOf(
 				return new AnalysisState<>(
 						entryState.getState().bottom(),
 						call.getMetaVariable(),
-						entryState.getAliasing().bottom());
+						FixpointInfo.BOTTOM);
 		}
 
 		ContextSensitivityToken callerToken = token;

diff --git a/...alyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java b/...alyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java
@@ -2,6 +2,7 @@
 
 import it.unive.lisa.analysis.AbstractState;
 import it.unive.lisa.analysis.AnalysisState;
+import it.unive.lisa.analysis.FixpointInfo;
 import it.unive.lisa.analysis.SemanticException;
 import it.unive.lisa.analysis.StatementStore;
 import it.unive.lisa.analysis.lattices.ExpressionSet;
@@ -93,7 +94,7 @@ public AnalysisState<A> getAbstractResultOf(
 				return new AnalysisState<>(
 						entryState.getState().bottom(),
 						call.getMetaVariable(),
-						entryState.getAliasing().bottom());
+						FixpointInfo.BOTTOM);
 		}
 
 		return super.getAbstractResultOf(call, entryState, parameters, expressions);

diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java
@@ -11,7 +11,6 @@
 import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
 import it.unive.lisa.analysis.numeric.Sign;
-import it.unive.lisa.analysis.symbols.SymbolAliasing;
 import it.unive.lisa.analysis.types.InferredTypes;
 import it.unive.lisa.conf.FixpointConfiguration;
 import it.unive.lisa.conf.LiSAConfiguration;
@@ -71,7 +70,7 @@ SimpleAbstractState<MonolithicHeap, ValueEnvironment<Sign>, TypeEnvironment<Infe
 						new MonolithicHeap(),
 						new ValueEnvironment<>(new Sign()),
 						new TypeEnvironment<>(new InferredTypes())),
-				new ExpressionSet(), new SymbolAliasing());
+				new ExpressionSet());
 	}
 
 	@Test

diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java
@@ -123,7 +123,7 @@ public void setup() throws CallGraphConstructionException, InterproceduralAnalys
 		as = new AnalysisState<>(
 				new SimpleAbstractState<>(new MonolithicHeap(), new ValueEnvironment<>(new Sign()),
 						new TypeEnvironment<>(new InferredTypes())),
-				new ExpressionSet(), new SymbolAliasing());
+				new ExpressionSet());
 		store = new StatementStore<>(as);
 		fake = new Expression(cfg, unknownLocation) {
 
@@ -468,8 +468,10 @@ public void testAssignOnBottom() {
 				boolean isBottom = ((Lattice) instance).isBottom();
 				if (instance instanceof AnalysisState) {
 					AnalysisState state = (AnalysisState) instance;
-					isBottom = state.getState().isBottom() && state.getAliasing().isBottom()
-					// analysis state keeps the assigned id on the stack
+					isBottom = state.getState().isBottom()
+							&& state.getFixpointInformation() != null
+							&& state.getFixpointInformation().isBottom()
+							// analysis state keeps the assigned id on the stack
 							&& state.getComputedExpressions().size() == 1
 							&& state.getComputedExpressions().iterator().next().equals(v);
 				}

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java
@@ -4,7 +4,6 @@
 import it.unive.lisa.analysis.AnalysisState;
 import it.unive.lisa.analysis.AnalyzedCFG;
 import it.unive.lisa.analysis.OptimizedAnalyzedCFG;
-import it.unive.lisa.analysis.symbols.SymbolAliasing;
 import it.unive.lisa.checks.ChecksExecutor;
 import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults;
 import it.unive.lisa.checks.semantic.SemanticCheck;
@@ -166,7 +165,7 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager, AtomicBoo
 				() -> {
 					try {
 						interproc.fixpoint(
-								new AnalysisState<>(state, new Skip(SyntheticLocation.INSTANCE), new SymbolAliasing()),
+								new AnalysisState<>(state, new Skip(SyntheticLocation.INSTANCE)),
 								(Class<? extends WorkingSet<Statement>>) conf.fixpointWorkingSet,
 								fixconf);
 					} catch (FixpointException e) {