From ca77cc0855d43fc153da81986936b97a843ae300 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Tue, 9 Jan 2024 12:11:29 +0100 Subject: [PATCH] Draft implementation of the pentagon abstract domain --- .../lisa/analysis/numeric/Pentagons.java | 223 ++++++++++++++++++ .../lisa/analysis/numeric/UpperBounds.java | 182 ++++++++++++++ 2 files changed, 405 insertions(+) create mode 100644 lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagons.java create mode 100644 lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagons.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagons.java new file mode 100644 index 000000000..182dce0a7 --- /dev/null +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagons.java @@ -0,0 +1,223 @@ +package it.unive.lisa.analysis.numeric; + +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Objects; +import java.util.Set; +import java.util.function.Predicate; + +import org.apache.commons.collections4.CollectionUtils; + +import it.unive.lisa.analysis.BaseLattice; +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.ScopeToken; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.analysis.value.ValueDomain; +import it.unive.lisa.program.cfg.ProgramPoint; +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.ValueExpression; +import it.unive.lisa.symbolic.value.operator.SubtractionOperator; +import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; +import it.unive.lisa.util.representation.MapRepresentation; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; + +public class Pentagons implements ValueDomain, BaseLattice { + + private final ValueEnvironment intervals; + private final ValueEnvironment upperBounds; + + public Pentagons() { + this.intervals = new ValueEnvironment<>(new Interval()).top(); + this.upperBounds = new ValueEnvironment<>(new UpperBounds(true)).top(); + } + + public Pentagons(ValueEnvironment intervals, ValueEnvironment upperBounds) { + this.intervals = intervals; + this.upperBounds = upperBounds; + } + + @Override + public Pentagons assign(Identifier id, ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + throws SemanticException { + ValueEnvironment newBounds = upperBounds.assign(id, expression, pp, oracle); + + // we add the semantics for assignments here as we have access to the whole assigment + if (expression instanceof BinaryExpression) { + BinaryExpression be = (BinaryExpression) expression; + BinaryOperator op = be.getOperator(); + if (op instanceof SubtractionOperator && be.getLeft() instanceof Identifier && be.getRight() instanceof Constant) { + Identifier y = (Identifier) be.getLeft(); + newBounds = newBounds.putState(id, upperBounds.getState(y).add(y)); + } + } + + return new Pentagons( + intervals.assign(id, expression, pp, oracle), + newBounds); + } + + @Override + public Pentagons smallStepSemantics(ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + throws SemanticException { + return new Pentagons( + intervals.smallStepSemantics(expression, pp, oracle), + upperBounds.smallStepSemantics(expression, pp, oracle)); + } + + @Override + public Pentagons assume(ValueExpression expression, ProgramPoint src, ProgramPoint dest, SemanticOracle oracle) + throws SemanticException { + return new Pentagons( + intervals.assume(expression, src, dest, oracle), + upperBounds.assume(expression, src, dest, oracle)); + } + + @Override + public Pentagons forgetIdentifier(Identifier id) throws SemanticException { + return new Pentagons( + intervals.forgetIdentifier(id), + upperBounds.forgetIdentifier(id)); + } + + @Override + public Pentagons forgetIdentifiersIf(Predicate test) throws SemanticException { + return new Pentagons( + intervals.forgetIdentifiersIf(test), + upperBounds.forgetIdentifiersIf(test)); + } + + + @Override + public Satisfiability satisfies(ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + throws SemanticException { + return intervals.satisfies(expression, pp, oracle).glb(upperBounds.satisfies(expression, pp, oracle)); + } + + @Override + public Pentagons pushScope(ScopeToken token) throws SemanticException { + return this; // we do not care about this for the project + } + + @Override + public Pentagons popScope(ScopeToken token) throws SemanticException { + return this; // we do not care about this for the project + } + + @Override + public StructuredRepresentation representation() { + if (isTop()) + return Lattice.topRepresentation(); + if (isBottom()) + return Lattice.bottomRepresentation(); + Map mapping = new HashMap<>(); + for (Identifier id : CollectionUtils.union(intervals.getKeys(), upperBounds.getKeys())) + mapping.put(new StringRepresentation(id), + new StringRepresentation(intervals.getState(id).toString() + ", " + + upperBounds.getState(id).representation())); + return new MapRepresentation(mapping); + } + + @Override + public Pentagons top() { + return new Pentagons(intervals.top(), upperBounds.top()); + } + + @Override + public boolean isTop() { + return intervals.isTop() && upperBounds.isTop(); + } + + @Override + public Pentagons bottom() { + return new Pentagons(intervals.bottom(), upperBounds.bottom()); + } + + @Override + public boolean isBottom() { + return intervals.isBottom() || upperBounds.isBottom(); + } + + @Override + public Pentagons lubAux(Pentagons other) throws SemanticException { + ValueEnvironment newBounds = upperBounds.lub(other.upperBounds); + for (Entry entry : upperBounds) { + Set closure = new HashSet<>(); + for (Identifier bound : entry.getValue()) + if (other.intervals.getState(entry.getKey()).interval.getHigh() + .compareTo(other.intervals.getState(bound).interval.getLow()) < 0) + closure.add(bound); + if (!closure.isEmpty()) + // glb is the union + newBounds.putState(entry.getKey(), + newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); + } + + for (Entry entry : other.upperBounds) { + Set closure = new HashSet<>(); + for (Identifier bound : entry.getValue()) + if (intervals.getState(entry.getKey()).interval.getHigh() + .compareTo(intervals.getState(bound).interval.getLow()) < 0) + closure.add(bound); + if (!closure.isEmpty()) + // glb is the union + newBounds.putState(entry.getKey(), + newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); + } + + return new Pentagons(intervals.lub(other.intervals), newBounds); + } + + @Override + public Pentagons wideningAux(Pentagons other) throws SemanticException { + return new Pentagons(intervals.widening(other.intervals), upperBounds.widening(other.upperBounds)); + } + + @Override + public boolean lessOrEqualAux(Pentagons other) throws SemanticException { + if (!intervals.lessOrEqual(other.intervals)) + return false; + for (Entry entry : other.upperBounds) + for (Identifier bound : entry.getValue()) + if (!(upperBounds.getState(entry.getKey()).contains(bound) + || intervals.getState(entry.getKey()).interval.getHigh() + .compareTo(intervals.getState(bound).interval.getLow()) < 0)) + return false; + + return true; + } + + @Override + public int hashCode() { + return Objects.hash(intervals, upperBounds); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Pentagons other = (Pentagons) obj; + return Objects.equals(intervals, other.intervals) && Objects.equals(upperBounds, other.upperBounds); + } + + @Override + public String toString() { + return representation().toString(); + } + + @Override + public boolean knowsIdentifier(Identifier id) { + return intervals.knowsIdentifier(id) || upperBounds.knowsIdentifier(id); + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java new file mode 100644 index 000000000..ea581282c --- /dev/null +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/UpperBounds.java @@ -0,0 +1,182 @@ +package it.unive.lisa.analysis.numeric; + +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Objects; +import java.util.Set; +import java.util.TreeSet; + +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonGe; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonGt; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonLe; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonLt; +import it.unive.lisa.util.representation.SetRepresentation; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; + +public class UpperBounds implements BaseNonRelationalValueDomain, Iterable { + + private static final UpperBounds TOP = new UpperBounds(true); + private static final UpperBounds BOTTOM = new UpperBounds(new TreeSet<>()); + + private final boolean isTop; + private final Set bounds; + + public UpperBounds() { + this(true); + } + + public UpperBounds(boolean isTop) { + this.bounds = null; + this.isTop = isTop; + } + + public UpperBounds(Set bounds) { + this.bounds = bounds; + this.isTop = false; + } + + + @Override + public StructuredRepresentation representation() { + if (isTop()) + return new StringRepresentation("{}"); + if (isBottom()) + return Lattice.bottomRepresentation(); + return new SetRepresentation(bounds, StringRepresentation::new); + } + + @Override + public UpperBounds top() { + return TOP; + } + + @Override + public UpperBounds bottom() { + return BOTTOM; + } + + @Override + public boolean isBottom() { + return !isTop && bounds.isEmpty(); + } + + @Override + public UpperBounds lubAux(UpperBounds other) throws SemanticException { + Set lub = new HashSet<>(bounds); + lub.retainAll(other.bounds); + return new UpperBounds(lub); + } + + @Override + public UpperBounds glbAux(UpperBounds other) throws SemanticException { + Set lub = new HashSet<>(bounds); + lub.addAll(other.bounds); + return new UpperBounds(lub); + } + + @Override + public boolean lessOrEqualAux(UpperBounds other) throws SemanticException { + return bounds.containsAll(other.bounds); + } + + @Override + public UpperBounds wideningAux(UpperBounds other) throws SemanticException { + return other.bounds.containsAll(bounds) ? other : TOP; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + UpperBounds other = (UpperBounds) obj; + return Objects.equals(bounds, other.bounds) && isTop == other.isTop; + } + + @Override + public int hashCode() { + return Objects.hash(bounds, isTop); + } + + @Override + public ValueEnvironment assumeBinaryExpression(ValueEnvironment environment, + BinaryOperator operator, ValueExpression left, ValueExpression right, ProgramPoint src, ProgramPoint dest, + SemanticOracle oracle) throws SemanticException { + if (!(left instanceof Identifier && right instanceof Identifier)) + return environment; + + + Identifier x = (Identifier) left; + Identifier y = (Identifier) right; + + // glb is the union! + + if (operator instanceof ComparisonEq) { + // x == y + UpperBounds set = environment.getState(x).glb(environment.getState(y)); + return environment.putState(x, set).putState(y, set); + } + + if (operator instanceof ComparisonLt) { + // x < y + UpperBounds set = environment.getState(x).glb(environment.getState(y)) + .glb(new UpperBounds(Collections.singleton(y))); + return environment.putState(x, set); + } + + if (operator instanceof ComparisonLe) { + // x <= y + UpperBounds set = environment.getState(x).glb(environment.getState(y)); + return environment.putState(x, set); + } + + if (operator instanceof ComparisonGt) { + // x > y ---> y < x + UpperBounds set = environment.getState(x).glb(environment.getState(y)) + .glb(new UpperBounds(Collections.singleton(x))); + return environment.putState(y, set); + } + + if (operator instanceof ComparisonGe) { + // x >= y --- > y <= x + UpperBounds set = environment.getState(x).glb(environment.getState(y)); + return environment.putState(y, set); + } + + return environment; + } + + @Override + public Iterator iterator() { + if (bounds == null) + return Collections.emptyIterator(); + return bounds.iterator(); + } + + public boolean contains(Identifier id) { + return bounds != null && bounds.contains(id); + } + + public UpperBounds add(Identifier id) { + Set res = new HashSet<>(); + if (!isTop() && !isBottom()) + res.addAll(bounds); + res.add(id); + return new UpperBounds(res); + } +}