Merge pull request #209 from UniVE-SSV/forget-predicate

Identifiers removal by predicate
lisa-analyzer · Jul 20, 2022 · 8f04e85 · 8f04e85
2 parents 2eb7066 + 700cda4
commit 8f04e85
Show file tree

Hide file tree

Showing 11 changed files with 102 additions and 0 deletions.
diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java b/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java
@@ -10,6 +10,7 @@
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.Identifier;
+import java.util.function.Predicate;
 
 /**
  * A generic Cartesian product abstract domain between two non-communicating
@@ -161,6 +162,13 @@ public C forgetIdentifier(Identifier id) throws SemanticException {
 		return mk(newLeft, newRight);
 	}
 
+	@Override
+	public C forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		T1 newLeft = left.forgetIdentifiersIf(test);
+		T2 newRight = right.forgetIdentifiersIf(test);
+		return mk(newLeft, newRight);
+	}
+
 	@Override
 	public C pushScope(ScopeToken scope) throws SemanticException {
 		T1 newLeft = left.pushScope(scope);

diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java b/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java
@@ -23,6 +23,7 @@
 import it.unive.lisa.util.collections.externalSet.ExternalSet;
 import java.util.Collections;
 import java.util.List;
+import java.util.function.Predicate;
 
 /**
  * A monolithic heap implementation that abstracts all heap locations to a
@@ -83,6 +84,11 @@ public MonolithicHeap forgetIdentifier(Identifier id) throws SemanticException {
 		return this;
 	}
 
+	@Override
+	public MonolithicHeap forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		return this;
+	}
+
 	@Override
 	protected MonolithicHeap lubAux(MonolithicHeap other) throws SemanticException {
 		return TOP;

diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java b/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java
@@ -27,6 +27,7 @@
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
+import java.util.function.Predicate;
 import org.apache.commons.collections4.SetUtils;
 
 /**
@@ -78,6 +79,11 @@ public TypeBasedHeap forgetIdentifier(Identifier id) throws SemanticException {
 		return this;
 	}
 
+	@Override
+	public TypeBasedHeap forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		return this;
+	}
+
 	@Override
 	public Satisfiability satisfies(SymbolicExpression expression, ProgramPoint pp) throws SemanticException {
 		// we leave the decision to the value domain

diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeap.java b/lisa/lisa-core/src/main/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeap.java
@@ -23,6 +23,7 @@
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
+import java.util.function.Predicate;
 
 /**
  * A field-insensitive point-based heap implementation that abstracts heap
@@ -113,6 +114,11 @@ public PointBasedHeap forgetIdentifier(Identifier id) throws SemanticException {
 		return from(new PointBasedHeap(heapEnv.forgetIdentifier(id)));
 	}
 
+	@Override
+	public PointBasedHeap forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		return from(new PointBasedHeap(heapEnv.forgetIdentifiersIf(test)));
+	}
+
 	@Override
 	public Satisfiability satisfies(SymbolicExpression expression, ProgramPoint pp) throws SemanticException {
 		// we leave the decision to the value domain

diff --git a/lisa/lisa-core/src/test/java/it/unive/lisa/analysis/value/SubstitutionTest.java b/lisa/lisa-core/src/test/java/it/unive/lisa/analysis/value/SubstitutionTest.java
@@ -23,6 +23,7 @@
 import java.util.Comparator;
 import java.util.HashSet;
 import java.util.List;
+import java.util.function.Predicate;
 import org.junit.Test;
 
 public class SubstitutionTest {
@@ -65,6 +66,11 @@ public Collector forgetIdentifier(Identifier id) throws SemanticException {
 			return rem;
 		}
 
+		@Override
+		public Collector forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+			return null;
+		}
+
 		@Override
 		public Satisfiability satisfies(ValueExpression expression, ProgramPoint pp) throws SemanticException {
 			return null; // not used

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
@@ -15,6 +15,7 @@
 import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
+import java.util.function.Predicate;
 
 /**
  * The abstract analysis state at a given program point. An analysis state is
@@ -271,6 +272,11 @@ public AnalysisState<A, H, V, T> forgetIdentifier(Identifier id) throws Semantic
 		return new AnalysisState<>(state.forgetIdentifier(id), computedExpressions, aliasing);
 	}
 
+	@Override
+	public AnalysisState<A, H, V, T> forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		return new AnalysisState<>(state.forgetIdentifiersIf(test), computedExpressions, aliasing);
+	}
+
 	@Override
 	public int hashCode() {
 		final int prime = 31;

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SemanticDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SemanticDomain.java
@@ -4,6 +4,7 @@
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.Identifier;
+import java.util.function.Predicate;
 
 /**
  * A domain able to determine how abstract information evolves thanks to the
@@ -78,6 +79,19 @@ public interface SemanticDomain<D extends SemanticDomain<D, E, I>, E extends Sym
 	 */
 	D forgetIdentifier(Identifier id) throws SemanticException;
 
+	/**
+	 * Forgets all {@link Identifier}s that match the given predicate. This
+	 * means that all information regarding the those identifiers will be lost.
+	 * This method should be invoked whenever an identifier gets out of scope.
+	 * 
+	 * @param test the test to identify the targets of the removal
+	 * 
+	 * @return the semantic domain without information about the ids
+	 * 
+	 * @throws SemanticException if an error occurs during the computation
+	 */
+	D forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException;
+
 	/**
 	 * Forgets all the given {@link Identifier}s. The default implementation of
 	 * this method iterates on {@code ids}, invoking

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java
@@ -13,6 +13,7 @@
 import it.unive.lisa.type.Type;
 import it.unive.lisa.util.collections.externalSet.ExternalSet;
 import java.util.Map;
+import java.util.function.Predicate;
 
 /**
  * An abstract state of the analysis, composed by a heap state modeling the
@@ -239,6 +240,14 @@ public SimpleAbstractState<H, V, T> forgetIdentifier(Identifier id) throws Seman
 				typeState.forgetIdentifier(id));
 	}
 
+	@Override
+	public SimpleAbstractState<H, V, T> forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		return new SimpleAbstractState<>(
+				heapState.forgetIdentifiersIf(test),
+				valueState.forgetIdentifiersIf(test),
+				typeState.forgetIdentifiersIf(test));
+	}
+
 	@Override
 	public int hashCode() {
 		final int prime = 31;

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/dataflow/DataflowDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/dataflow/DataflowDomain.java
@@ -14,6 +14,7 @@
 import java.util.LinkedList;
 import java.util.Set;
 import java.util.function.BooleanSupplier;
+import java.util.function.Predicate;
 
 /**
  * A dataflow domain that collects instances of {@link DataflowElement}. A
@@ -139,6 +140,25 @@ public D forgetIdentifier(Identifier id) throws SemanticException {
 		return mk(domain, updated, false, false);
 	}
 
+	@Override
+	@SuppressWarnings("unchecked")
+	public D forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		if (isTop())
+			return (D) this;
+
+		Collection<E> toRemove = new LinkedList<>();
+		for (E e : elements)
+			if (e.getInvolvedIdentifiers().stream().anyMatch(test::test))
+				toRemove.add(e);
+
+		if (toRemove.isEmpty())
+			return (D) this;
+
+		Set<E> updated = new HashSet<>(elements);
+		updated.removeAll(toRemove);
+		return mk(domain, updated, false, false);
+	}
+
 	@Override
 	public Satisfiability satisfies(ValueExpression expression, ProgramPoint pp) throws SemanticException {
 		// TODO could be refined

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/Environment.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/Environment.java
@@ -17,7 +17,9 @@
 import java.util.Map;
 import java.util.Set;
 import java.util.concurrent.atomic.AtomicReference;
+import java.util.function.Predicate;
 import java.util.function.UnaryOperator;
+import java.util.stream.Collectors;
 import org.apache.commons.lang3.tuple.Pair;
 
 /**
@@ -291,6 +293,19 @@ public M forgetIdentifier(Identifier id) throws SemanticException {
 		return result;
 	}
 
+	@Override
+	@SuppressWarnings("unchecked")
+	public M forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		if (isTop() || isBottom())
+			return (M) this;
+
+		M result = copy();
+		Set<Identifier> keys = result.function.keySet().stream().filter(test::test).collect(Collectors.toSet());
+		keys.forEach(result.function::remove);
+
+		return result;
+	}
+
 	@Override
 	public DomainRepresentation representation() {
 		if (isTop())

diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestDomain.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestDomain.java
@@ -7,6 +7,7 @@
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.Identifier;
+import java.util.function.Predicate;
 
 @SuppressWarnings("unchecked")
 public abstract class TestDomain<T extends TestDomain<T, E>, E extends SymbolicExpression> extends BaseLattice<T>
@@ -42,6 +43,11 @@ public T forgetIdentifier(Identifier id) throws SemanticException {
 		return (T) this;
 	}
 
+	@Override
+	public T forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
+		return (T) this;
+	}
+
 	@Override
 	public Satisfiability satisfies(E expression, ProgramPoint pp) throws SemanticException {
 		return Satisfiability.UNKNOWN;