Supporting recursions #291

lisa-analyzer · Sep 28, 2023 · 49eda2e · 49eda2e
1 parent 898b911
commit 49eda2e
Show file tree

Hide file tree

Showing 7 changed files with 218 additions and 29 deletions.
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java
@@ -593,6 +593,21 @@ public boolean knowsIdentifier(
 		return heapState.knowsIdentifier(id) || valueState.knowsIdentifier(id) || typeState.knowsIdentifier(id);
 	}
 
+	@Override
+	public SimpleAbstractState<H, V, T> withTopMemory() {
+		return new SimpleAbstractState<>(heapState.top(), valueState, typeState);
+	}
+
+	@Override
+	public SimpleAbstractState<H, V, T> withTopValues() {
+		return new SimpleAbstractState<>(heapState, valueState.top(), typeState);
+	}
+
+	@Override
+	public SimpleAbstractState<H, V, T> withTopTypes() {
+		return new SimpleAbstractState<>(heapState, valueState, typeState.top());
+	}
+
 	private static class MutableOracle<H extends HeapDomain<H>,
 			V extends ValueDomain<V>,
 			T extends TypeDomain<T>> implements SemanticOracle {

diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java
@@ -411,4 +411,37 @@ public boolean knowsIdentifier(Identifier id) {
 				return true;
 		return false;
 	}
+
+	@Override
+	public TracePartitioning<A> withTopMemory() {
+		if (isTop() || isBottom() || function == null)
+			return this;
+
+		Map<ExecutionTrace, A> result = mkNewFunction(null, false);
+		for (Entry<ExecutionTrace, A> trace : this)
+			result.put(trace.getKey(), trace.getValue().withTopMemory());
+		return new TracePartitioning<>(lattice, result);
+	}
+
+	@Override
+	public TracePartitioning<A> withTopValues() {
+		if (isTop() || isBottom() || function == null)
+			return this;
+
+		Map<ExecutionTrace, A> result = mkNewFunction(null, false);
+		for (Entry<ExecutionTrace, A> trace : this)
+			result.put(trace.getKey(), trace.getValue().withTopValues());
+		return new TracePartitioning<>(lattice, result);
+	}
+
+	@Override
+	public TracePartitioning<A> withTopTypes() {
+		if (isTop() || isBottom() || function == null)
+			return this;
+
+		Map<ExecutionTrace, A> result = mkNewFunction(null, false);
+		for (Entry<ExecutionTrace, A> trace : this)
+			result.put(trace.getKey(), trace.getValue().withTopTypes());
+		return new TracePartitioning<>(lattice, result);
+	}
 }
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
@@ -97,7 +97,8 @@ public AnalysisState<A> getAbstractResultOf(
 	}
 
 	@Override
-	protected boolean canShortcut(CFG cfg) {
+	protected boolean canShortcut(
+			CFG cfg) {
 		// we want to compute the recursive chain with no shortcuts
 		return !recursion.getMembers().contains(cfg);
 	}
@@ -130,6 +131,9 @@ public AnalysisState<A> find() throws SemanticException {
 		ExpressionSet[] params = new ExpressionSet[actuals.length];
 		for (int i = 0; i < params.length; i++)
 			params[i] = entryState.intermediateStates.getState(actuals[i]).getComputedExpressions();
-		return start.expressionSemantics(this, entryState.postState.top(), params, entryState.intermediateStates);
+		// it should be enough to send values to top, retaining all type
+		// information
+		return start.expressionSemantics(this, entryState.postState.withTopValues(), params,
+				entryState.intermediateStates);
 	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AbstractState.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AbstractState.java
@@ -14,5 +14,35 @@
  * @param <A> the concrete type of the {@link AbstractState}
  */
 public interface AbstractState<A extends AbstractState<A>>
-		extends SemanticOracle, Lattice<A>, SemanticDomain<A, SymbolicExpression, Identifier> {
+		extends
+		SemanticOracle,
+		Lattice<A>,
+		SemanticDomain<A, SymbolicExpression, Identifier> {
+
+	/**
+	 * Yields a copy of this state, but with its memory abstraction set to top.
+	 * This is useful to represent effects of unknown calls that arbitrarily
+	 * manipulate the memory.
+	 * 
+	 * @return the copy with top memory
+	 */
+	A withTopMemory();
+
+	/**
+	 * Yields a copy of this state, but with its value abstraction set to top.
+	 * This is useful to represent effects of unknown calls that arbitrarily
+	 * manipulate the values of variables.
+	 * 
+	 * @return the copy with top values
+	 */
+	A withTopValues();
+
+	/**
+	 * Yields a copy of this state, but with its type abstraction set to top.
+	 * This is useful to represent effects of unknown calls that arbitrarily
+	 * manipulate the values of variables (and their type accordingly).
+	 * 
+	 * @return the copy with top types
+	 */
+	A withTopTypes();
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java
@@ -26,7 +26,8 @@
  * @param <A> the type of {@link AbstractState} embedded in this state
  */
 public class AnalysisState<A extends AbstractState<A>>
-		implements BaseLattice<AnalysisState<A>>,
+		implements
+		BaseLattice<AnalysisState<A>>,
 		StructuredObject,
 		ScopedObject<AnalysisState<A>> {
 
@@ -53,7 +54,9 @@ public class AnalysisState<A extends AbstractState<A>>
 	 *                               analysis state
 	 * @param computedExpression the expression that has been computed
 	 */
-	public AnalysisState(A state, SymbolicExpression computedExpression) {
+	public AnalysisState(
+			A state,
+			SymbolicExpression computedExpression) {
 		this(state, new ExpressionSet(computedExpression), null);
 	}
 
@@ -64,7 +67,9 @@ public AnalysisState(A state, SymbolicExpression computedExpression) {
 	 *                                analysis state
 	 * @param computedExpressions the expressions that have been computed
 	 */
-	public AnalysisState(A state, ExpressionSet computedExpressions) {
+	public AnalysisState(
+			A state,
+			ExpressionSet computedExpressions) {
 		this(state, computedExpressions, null);
 	}
 
@@ -77,7 +82,10 @@ public AnalysisState(A state, ExpressionSet computedExpressions) {
 	 * @param info               the additional information to be computed
 	 *                               during fixpoint computations
 	 */
-	public AnalysisState(A state, SymbolicExpression computedExpression, FixpointInfo info) {
+	public AnalysisState(
+			A state,
+			SymbolicExpression computedExpression,
+			FixpointInfo info) {
 		this(state, new ExpressionSet(computedExpression), info);
 	}
 
@@ -90,7 +98,10 @@ public AnalysisState(A state, SymbolicExpression computedExpression, FixpointInf
 	 * @param info                the additional information to be computed
 	 *                                during fixpoint computations
 	 */
-	public AnalysisState(A state, ExpressionSet computedExpressions, FixpointInfo info) {
+	public AnalysisState(
+			A state,
+			ExpressionSet computedExpressions,
+			FixpointInfo info) {
 		this.state = state;
 		this.computedExpressions = computedExpressions;
 		this.info = info;
@@ -125,7 +136,8 @@ public FixpointInfo getFixpointInformation() {
 	 * 
 	 * @return the mapped information
 	 */
-	public Lattice<?> getInfo(String key) {
+	public Lattice<?> getInfo(
+			String key) {
 		return info == null ? null : info.get(key);
 	}
 
@@ -140,7 +152,9 @@ public Lattice<?> getInfo(String key) {
 	 * 
 	 * @return the mapped information
 	 */
-	public <T> T getInfo(String key, Class<T> type) {
+	public <T> T getInfo(
+			String key,
+			Class<T> type) {
 		return info == null ? null : info.get(key, type);
 	}
 
@@ -156,7 +170,9 @@ public <T> T getInfo(String key, Class<T> type) {
 	 * 
 	 * @return a new instance with the updated mapping
 	 */
-	public AnalysisState<A> storeInfo(String key, Lattice<?> info) {
+	public AnalysisState<A> storeInfo(
+			String key,
+			Lattice<?> info) {
 		FixpointInfo fixinfo = this.info == null ? new FixpointInfo() : this.info;
 		fixinfo = fixinfo.put(key, info);
 		return new AnalysisState<>(state, computedExpressions, fixinfo);
@@ -177,7 +193,10 @@ public AnalysisState<A> storeInfo(String key, Lattice<?> info) {
 	 * 
 	 * @throws SemanticException if something goes wrong during the lub
 	 */
-	public AnalysisState<A> weakStoreInfo(String key, Lattice<?> info) throws SemanticException {
+	public AnalysisState<A> weakStoreInfo(
+			String key,
+			Lattice<?> info)
+			throws SemanticException {
 		FixpointInfo fixinfo = this.info == null ? new FixpointInfo() : this.info;
 		fixinfo = fixinfo.putWeak(key, info);
 		return new AnalysisState<>(state, computedExpressions, fixinfo);
@@ -330,7 +349,9 @@ public SemanticDomain.Satisfiability satisfies(
 	}
 
 	@Override
-	public AnalysisState<A> pushScope(ScopeToken scope) throws SemanticException {
+	public AnalysisState<A> pushScope(
+			ScopeToken scope)
+			throws SemanticException {
 		return new AnalysisState<>(
 				state.pushScope(scope),
 				onAllExpressions(this.computedExpressions, scope, true),
@@ -339,55 +360,69 @@ public AnalysisState<A> pushScope(ScopeToken scope) throws SemanticException {
 
 	private static ExpressionSet onAllExpressions(
 			ExpressionSet computedExpressions,
-			ScopeToken scope, boolean push) throws SemanticException {
+			ScopeToken scope,
+			boolean push)
+			throws SemanticException {
 		Set<SymbolicExpression> result = new HashSet<>();
 		for (SymbolicExpression exp : computedExpressions)
 			result.add(push ? exp.pushScope(scope) : exp.popScope(scope));
 		return new ExpressionSet(result);
 	}
 
 	@Override
-	public AnalysisState<A> popScope(ScopeToken scope) throws SemanticException {
+	public AnalysisState<A> popScope(
+			ScopeToken scope)
+			throws SemanticException {
 		return new AnalysisState<>(
 				state.popScope(scope),
 				onAllExpressions(this.computedExpressions, scope, false),
 				info);
 	}
 
 	@Override
-	public AnalysisState<A> lubAux(AnalysisState<A> other) throws SemanticException {
+	public AnalysisState<A> lubAux(
+			AnalysisState<A> other)
+			throws SemanticException {
 		return new AnalysisState<>(
 				state.lub(other.state),
 				computedExpressions.lub(other.computedExpressions),
 				info == null ? other.info : info.lub(other.info));
 	}
 
 	@Override
-	public AnalysisState<A> glbAux(AnalysisState<A> other) throws SemanticException {
+	public AnalysisState<A> glbAux(
+			AnalysisState<A> other)
+			throws SemanticException {
 		return new AnalysisState<>(
 				state.glb(other.state),
 				computedExpressions.glb(other.computedExpressions),
 				info == null ? null : info.glb(other.info));
 	}
 
 	@Override
-	public AnalysisState<A> wideningAux(AnalysisState<A> other) throws SemanticException {
+	public AnalysisState<A> wideningAux(
+			AnalysisState<A> other)
+			throws SemanticException {
 		return new AnalysisState<>(
 				state.widening(other.state),
 				computedExpressions.lub(other.computedExpressions),
 				info == null ? other.info : info.widening(other.info));
 	}
 
 	@Override
-	public AnalysisState<A> narrowingAux(AnalysisState<A> other) throws SemanticException {
+	public AnalysisState<A> narrowingAux(
+			AnalysisState<A> other)
+			throws SemanticException {
 		return new AnalysisState<>(
 				state.narrowing(other.state),
 				computedExpressions.glb(other.computedExpressions),
 				info == null ? null : info.narrowing(other.info));
 	}
 
 	@Override
-	public boolean lessOrEqualAux(AnalysisState<A> other) throws SemanticException {
+	public boolean lessOrEqualAux(
+			AnalysisState<A> other)
+			throws SemanticException {
 		return state.lessOrEqual(other.state)
 				&& computedExpressions.lessOrEqual(other.computedExpressions)
 				&& (info == null ? true : info.lessOrEqual(other.info));
@@ -424,7 +459,9 @@ public boolean isBottom() {
 	 * 
 	 * @throws SemanticException if an error occurs during the computation
 	 */
-	public AnalysisState<A> forgetIdentifier(Identifier id) throws SemanticException {
+	public AnalysisState<A> forgetIdentifier(
+			Identifier id)
+			throws SemanticException {
 		return new AnalysisState<>(state.forgetIdentifier(id), computedExpressions, info);
 	}
 
@@ -439,7 +476,9 @@ public AnalysisState<A> forgetIdentifier(Identifier id) throws SemanticException
 	 * 
 	 * @throws SemanticException if an error occurs during the computation
 	 */
-	public AnalysisState<A> forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+	public AnalysisState<A> forgetIdentifiersIf(
+			Predicate<Identifier> test)
+			throws SemanticException {
 		return new AnalysisState<>(state.forgetIdentifiersIf(test), computedExpressions, info);
 	}
 
@@ -453,7 +492,9 @@ public AnalysisState<A> forgetIdentifiersIf(Predicate<Identifier> test) throws S
 	 * 
 	 * @throws SemanticException if an error occurs during the computation
 	 */
-	public AnalysisState<A> forgetIdentifiers(Iterable<Identifier> ids) throws SemanticException {
+	public AnalysisState<A> forgetIdentifiers(
+			Iterable<Identifier> ids)
+			throws SemanticException {
 		AnalysisState<A> result = this;
 		for (Identifier id : ids)
 			result = result.forgetIdentifier(id);
@@ -471,7 +512,8 @@ public int hashCode() {
 	}
 
 	@Override
-	public boolean equals(Object obj) {
+	public boolean equals(
+			Object obj) {
 		if (this == obj)
 			return true;
 		if (obj == null)
@@ -533,4 +575,38 @@ public StructuredRepresentation representationWithInfo() {
 	public String toString() {
 		return representation().toString();
 	}
+
+	/**
+	 * Yields a copy of this state, but with the {@link AbstractState}'s inner
+	 * memory abstraction set to top. This is useful to represent effects of
+	 * unknown calls that arbitrarily manipulate the memory.
+	 * 
+	 * @return the copy with top memory
+	 */
+	public AnalysisState<A> withTopMemory() {
+		return new AnalysisState<>(state.withTopMemory(), computedExpressions, info);
+	}
+
+	/**
+	 * Yields a copy of this state, but with the {@link AbstractState}'s inner
+	 * value abstraction set to top. This is useful to represent effects of
+	 * unknown calls that arbitrarily manipulate the values of variables.
+	 * 
+	 * @return the copy with top value
+	 */
+	public AnalysisState<A> withTopValues() {
+		return new AnalysisState<>(state.withTopValues(), computedExpressions, info);
+	}
+
+	/**
+	 * Yields a copy of this state, but with the {@link AbstractState}'s inner
+	 * type abstraction set to top. This is useful to represent effects of
+	 * unknown calls that arbitrarily manipulate the values of variables (and
+	 * their type accordingly).
+	 * 
+	 * @return the copy with top type
+	 */
+	public AnalysisState<A> withTopTypes() {
+		return new AnalysisState<>(state.withTopTypes(), computedExpressions, info);
+	}
 }