From ca77cc0855d43fc153da81986936b97a843ae300 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Tue, 9 Jan 2024 12:11:29 +0100 Subject: [PATCH 01/12] 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); + } +} From a797a9a871f3471258f1d6e7ff162aae68838b6f Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 09:21:21 +0100 Subject: [PATCH 02/12] Draft classes for testing pentagon domain --- .../imp-testcases/numeric/pentagons.imp | 3 +++ .../it/unive/lisa/cron/NumericAnalysesTest.java | 15 +++++++++++++++ 2 files changed, 18 insertions(+) create mode 100644 lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp new file mode 100644 index 000000000..8b216852a --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp @@ -0,0 +1,3 @@ +class ptng { + +} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java index 014d4dc97..012a20773 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java @@ -8,6 +8,7 @@ import it.unive.lisa.analysis.numeric.IntegerConstantPropagation; import it.unive.lisa.analysis.numeric.Interval; import it.unive.lisa.analysis.numeric.Parity; +import it.unive.lisa.analysis.numeric.Pentagons; import it.unive.lisa.analysis.numeric.Sign; import it.unive.lisa.conf.LiSAConfiguration.DescendingPhaseType; import org.junit.Test; @@ -90,4 +91,18 @@ public void testNonRedundantSetOfInterval() { conf.compareWithOptimization = false; perform(conf); } + + @Test + public void testPentagons() { + CronConfiguration conf = new CronConfiguration(); + conf.serializeResults = true; + conf.abstractState = DefaultConfiguration.simpleState( + DefaultConfiguration.defaultHeapDomain(), + new Pentagons(), + DefaultConfiguration.defaultTypeDomain()); + conf.testDir = "numeric"; + conf.testSubDir = "pentagons"; + conf.programFile = "numeric.imp"; + perform(conf); + } } From ebda88b0953159e93980b238069ee4cf48e60d71 Mon Sep 17 00:00:00 2001 From: Luca Olivieri Date: Wed, 10 Jan 2024 11:55:01 +0100 Subject: [PATCH 03/12] Added missing documentation in Pentagons.java and UpperBounds.java --- .../lisa/analysis/numeric/Pentagons.java | 25 ++++++++++ .../lisa/analysis/numeric/UpperBounds.java | 46 +++++++++++++++++++ 2 files changed, 71 insertions(+) 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 index 182dce0a7..972190cb5 100644 --- 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 @@ -29,16 +29,41 @@ import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; +/** + * The pentagons abstract domain, a weakly relational numerical abstract domain. This abstract + * domain captures properties of the form of x ⋲ [a, b] ∧ x < y. It is more precise than the + * well known interval domain, but it is less precise than the octagon domain. + * It is implemented as a {@link ValueDomain}. + * + * @author Luca Negrini + * @author Vincenzo Arceri + */ public class Pentagons implements ValueDomain, BaseLattice { + /** + * The interval environment. + */ private final ValueEnvironment intervals; + + /** + * The upper bounds environment. + */ private final ValueEnvironment upperBounds; + /** + * Builds the pentagons. + */ public Pentagons() { this.intervals = new ValueEnvironment<>(new Interval()).top(); this.upperBounds = new ValueEnvironment<>(new UpperBounds(true)).top(); } + /** + * Builds the pentagons. + * + * @param intervals the underlying {@link ValueEnvironment} + * @param upperBounds the underlying {@link ValueEnvironment} + */ public Pentagons(ValueEnvironment intervals, ValueEnvironment upperBounds) { this.intervals = intervals; this.upperBounds = upperBounds; 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 index ea581282c..305f653de 100644 --- 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 @@ -25,23 +25,57 @@ import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; +/** + * The upper bounds abstract domain. It is implemented as + * a {@link BaseNonRelationalValueDomain}. + * + * @author Luca Negrini + * @author Vincenzo Arceri + */ public class UpperBounds implements BaseNonRelationalValueDomain, Iterable { + /** + * The abstract top element. + */ private static final UpperBounds TOP = new UpperBounds(true); + + /** + * The abstract bottom element. + */ private static final UpperBounds BOTTOM = new UpperBounds(new TreeSet<>()); + /** + * The flag to set abstract top state. + */ private final boolean isTop; + + /** + * The set containing the bounds. + */ private final Set bounds; + /** + * Builds the upper bounds. + */ public UpperBounds() { this(true); } + /** + * Builds the upper bounds. + * + * @param isTop {@code true} if the abstract domain is top; otherwise {@code false}. + */ public UpperBounds(boolean isTop) { this.bounds = null; this.isTop = isTop; } + /** + * Builds the upper bounds. + * + * @param bounds the bounds to set + */ public UpperBounds(Set bounds) { this.bounds = bounds; this.isTop = false; @@ -168,10 +202,22 @@ public Iterator iterator() { return bounds.iterator(); } + /** + * Checks if this bounds contains a specified identifier of a program variable. + * + * @param id the identifier to check + * @return {@code true} if this bounds contains the specified identifier; otherwise, {@code false}. + */ public boolean contains(Identifier id) { return bounds != null && bounds.contains(id); } + /** + * Adds the specified identifier of a program variable in the bounds. + * + * @param id the identifier to add in the bounds. + * @return the updated bounds. + */ public UpperBounds add(Identifier id) { Set res = new HashSet<>(); if (!isTop() && !isBottom()) From db23e87df1012e02db2922301c3049a1192a9d2d Mon Sep 17 00:00:00 2001 From: Luca Olivieri Date: Wed, 10 Jan 2024 13:53:38 +0100 Subject: [PATCH 04/12] Minor fix on NumericAnalysesTest --- .../src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java index 012a20773..919362333 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java @@ -11,6 +11,7 @@ import it.unive.lisa.analysis.numeric.Pentagons; import it.unive.lisa.analysis.numeric.Sign; import it.unive.lisa.conf.LiSAConfiguration.DescendingPhaseType; + import org.junit.Test; public class NumericAnalysesTest extends AnalysisTestExecutor { @@ -102,7 +103,7 @@ public void testPentagons() { DefaultConfiguration.defaultTypeDomain()); conf.testDir = "numeric"; conf.testSubDir = "pentagons"; - conf.programFile = "numeric.imp"; + conf.programFile = "pentagons.imp"; perform(conf); } } From 22f32c6dfcc4eb2f05f4bbd7843bbc8d75a73734 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 14:31:03 +0100 Subject: [PATCH 05/12] Closure for pentagons, first cron tests for pentagons --- .../imp-testcases/numeric/pentagons.imp | 25 +++++++++++- .../numeric/pentagons/report.json | 38 +++++++++++++++++++ ...his,_untyped_b,_untyped_x,_untyped_y).json | 1 + ...his,_untyped_b,_untyped_x,_untyped_y).json | 1 + .../lisa/analysis/numeric/Pentagons.java | 28 ++++++++++++-- 5 files changed, 88 insertions(+), 5 deletions(-) create mode 100644 lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json create mode 100644 lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json create mode 100644 lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp index 8b216852a..bee3c25c2 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp @@ -1,3 +1,26 @@ -class ptng { +class petagons_tests { + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + non_strict_abstraction(b, x, y) { + if(b) { + x = 0; y = 3; + } else { + x = -2; y = 1; + } + } + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + strict_abstraction(b, x, y) { + if(b) { + x = 0; y = 3; + } else { + x = -2; y = 0; + } + } + } \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json new file mode 100644 index 000000000..f232beeaf --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json @@ -0,0 +1,38 @@ +{ + "warnings" : [ ], + "files" : [ "report.json", "untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json", "untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json" ], + "info" : { + "cfgs" : "2", + "duration" : "392ms", + "end" : "2024-01-10T14:28:19.938+01:00", + "expressions" : "16", + "files" : "2", + "globals" : "0", + "members" : "2", + "programs" : "1", + "start" : "2024-01-10T14:28:19.546+01:00", + "statements" : "12", + "units" : "1", + "version" : "0.1b8", + "warnings" : "0" + }, + "configuration" : { + "analysisGraphs" : "NONE", + "descendingPhaseType" : "NONE", + "dumpForcesUnwinding" : "false", + "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "glbThreshold" : "5", + "hotspots" : "unset", + "jsonOutput" : "true", + "openCallPolicy" : "WorstCasePolicy", + "optimize" : "false", + "recursionWideningThreshold" : "5", + "semanticChecks" : "", + "serializeInputs" : "false", + "serializeResults" : "true", + "syntacticChecks" : "", + "useWideningPoints" : "true", + "wideningThreshold" : "5", + "workdir" : "test-outputs/numeric/pentagons" + } +} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json new file mode 100644 index 000000000..b7cb9b550 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::non_strict_abstraction(petagons_tests* this, untyped b, untyped x, untyped y)","description":null,"nodes":[{"id":0,"text":"b"},{"id":1,"subNodes":[2,3],"text":"x = 0"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":"y = 3"},{"id":5,"text":"y"},{"id":6,"text":"3"},{"id":7,"subNodes":[8,9],"text":"x = -2"},{"id":8,"text":"x"},{"id":9,"text":"-2"},{"id":10,"subNodes":[11,12],"text":"y = 1"},{"id":11,"text":"y"},{"id":12,"text":"1"},{"id":13,"text":"ret"}],"edges":[{"sourceId":0,"destId":1,"kind":"TrueEdge"},{"sourceId":0,"destId":7,"kind":"FalseEdge"},{"sourceId":1,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":13,"kind":"SequentialEdge"},{"sourceId":7,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], (y)","y":"[3, 3], {}"}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["3"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["-2"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], (y)","y":"[1, 1], {}"}}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":12,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":13,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, 0], (y)","y":"[1, 3], {}"}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json new file mode 100644 index 000000000..35d01401f --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::strict_abstraction(petagons_tests* this, untyped b, untyped x, untyped y)","description":null,"nodes":[{"id":0,"text":"b"},{"id":1,"subNodes":[2,3],"text":"x = 0"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":"y = 3"},{"id":5,"text":"y"},{"id":6,"text":"3"},{"id":7,"subNodes":[8,9],"text":"x = -2"},{"id":8,"text":"x"},{"id":9,"text":"-2"},{"id":10,"subNodes":[11,12],"text":"y = 0"},{"id":11,"text":"y"},{"id":12,"text":"0"},{"id":13,"text":"ret"}],"edges":[{"sourceId":0,"destId":1,"kind":"TrueEdge"},{"sourceId":0,"destId":7,"kind":"FalseEdge"},{"sourceId":1,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":13,"kind":"SequentialEdge"},{"sourceId":7,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["b"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], (y)","y":"[3, 3], {}"}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["3"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[0, 0], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["-2"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], (y)","y":"[0, 0], {}"}}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":12,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":"#TOP#"},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, -2], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":13,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"b":"#TOP#","this":["petagons_tests*"],"x":["int32"],"y":["int32"]},"value":{"b":"[-Inf, +Inf], {}","x":"[-2, 0], (y)","y":"[0, 3], {}"}}}}]} \ No newline at end of file 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 index 972190cb5..94418e98f 100644 --- 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 @@ -86,7 +86,7 @@ public Pentagons assign(Identifier id, ValueExpression expression, ProgramPoint return new Pentagons( intervals.assign(id, expression, pp, oracle), - newBounds); + newBounds).closure(); } @Override @@ -167,9 +167,29 @@ public Pentagons bottom() { @Override public boolean isBottom() { - return intervals.isBottom() || upperBounds.isBottom(); + return intervals.isBottom() && upperBounds.isBottom(); } + private Pentagons closure() throws SemanticException { + ValueEnvironment newBounds = new ValueEnvironment(upperBounds.lattice, upperBounds.getMap()); + + for (Identifier id1 : intervals.getKeys()) { + Set closure = new HashSet<>(); + for (Identifier id2 : intervals.getKeys()) + if (!id1.equals(id2)) + if (intervals.getState(id1).interval.getHigh() + .compareTo(intervals.getState(id2).interval.getLow()) < 0) + closure.add(id2); + if (!closure.isEmpty()) + // glb is the union + newBounds = newBounds.putState(id1, + newBounds.getState(id1).glb(new UpperBounds(closure))); + + } + + return new Pentagons(intervals, newBounds); + } + @Override public Pentagons lubAux(Pentagons other) throws SemanticException { ValueEnvironment newBounds = upperBounds.lub(other.upperBounds); @@ -181,7 +201,7 @@ public Pentagons lubAux(Pentagons other) throws SemanticException { closure.add(bound); if (!closure.isEmpty()) // glb is the union - newBounds.putState(entry.getKey(), + newBounds = newBounds.putState(entry.getKey(), newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); } @@ -193,7 +213,7 @@ public Pentagons lubAux(Pentagons other) throws SemanticException { closure.add(bound); if (!closure.isEmpty()) // glb is the union - newBounds.putState(entry.getKey(), + newBounds = newBounds.putState(entry.getKey(), newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); } From 2efa3d56bd20812c4c454cb4fb95a09610bb83eb Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 14:46:22 +0100 Subject: [PATCH 06/12] Extended assignment semantics for r = x - y --- .../imp-testcases/numeric/pentagons.imp | 11 +++++ .../numeric/pentagons/report.json | 18 ++++---- ...his,_untyped_x,_untyped_y,_untyped_r).json | 1 + .../lisa/analysis/numeric/Pentagons.java | 42 ++++++++++++------- 4 files changed, 48 insertions(+), 24 deletions(-) create mode 100644 lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp index bee3c25c2..62789687a 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp @@ -21,6 +21,17 @@ class petagons_tests { x = -2; y = 0; } } + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + common_code_pattern_01(x, y, r) { + if(x >= 0 && y >= 0) + if (x > y) { + r = x - y; + assert r >= 0; + } + } } \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json index f232beeaf..33a6040f9 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json @@ -1,17 +1,17 @@ { "warnings" : [ ], - "files" : [ "report.json", "untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json", "untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json" ], + "files" : [ "report.json", "untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json", "untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json", "untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json" ], "info" : { - "cfgs" : "2", - "duration" : "392ms", - "end" : "2024-01-10T14:28:19.938+01:00", - "expressions" : "16", - "files" : "2", + "cfgs" : "3", + "duration" : "426ms", + "end" : "2024-01-10T14:45:14.863+01:00", + "expressions" : "31", + "files" : "3", "globals" : "0", - "members" : "2", + "members" : "3", "programs" : "1", - "start" : "2024-01-10T14:28:19.546+01:00", - "statements" : "12", + "start" : "2024-01-10T14:45:14.437+01:00", + "statements" : "17", "units" : "1", "version" : "0.1b8", "warnings" : "0" diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json new file mode 100644 index 000000000..f1c92d216 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::common_code_pattern_01(petagons_tests* this, untyped x, untyped y, untyped r)","description":null,"nodes":[{"id":0,"subNodes":[1,4],"text":"&&(>=(x, 0), >=(y, 0))"},{"id":1,"subNodes":[2,3],"text":">=(x, 0)"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":">=(y, 0)"},{"id":5,"text":"y"},{"id":6,"text":"0"},{"id":7,"subNodes":[8,9],"text":">(x, y)"},{"id":8,"text":"x"},{"id":9,"text":"y"},{"id":10,"subNodes":[11,12],"text":"r = -(x, y)"},{"id":11,"text":"r"},{"id":12,"subNodes":[13,14],"text":"-(x, y)"},{"id":13,"text":"x"},{"id":14,"text":"y"},{"id":15,"subNodes":[16],"text":"assert >=(r, 0)"},{"id":16,"subNodes":[17,18],"text":">=(r, 0)"},{"id":17,"text":"r"},{"id":18,"text":"0"},{"id":19,"text":"ret"}],"edges":[{"sourceId":0,"destId":7,"kind":"TrueEdge"},{"sourceId":0,"destId":19,"kind":"FalseEdge"},{"sourceId":7,"destId":10,"kind":"TrueEdge"},{"sourceId":7,"destId":19,"kind":"FalseEdge"},{"sourceId":10,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x >= 0 && y >= 0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["x >= 0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["y >= 0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["x > y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[0, +Inf], {}","y":"[0, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[0, +Inf], {}","y":"[0, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[0, +Inf], {}","y":"[0, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":11,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":12,"description":{"expressions":["x - y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":13,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":14,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":15,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":16,"description":{"expressions":["r >= 0"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":17,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":18,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[1, +Inf], {}","x":"[1, +Inf], {}","y":"[0, +Inf], (x)"}}}},{"nodeId":19,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"r":"#TOP#","this":["petagons_tests*"],"x":"#TOP#","y":"#TOP#"},"value":{"r":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}","y":"[-Inf, +Inf], {}"}}}}]} \ No newline at end of file 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 index 94418e98f..6393a37ae 100644 --- 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 @@ -25,6 +25,7 @@ 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.numeric.MathNumber; import it.unive.lisa.util.representation.MapRepresentation; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; @@ -44,7 +45,7 @@ public class Pentagons implements ValueDomain, BaseLattice * The interval environment. */ private final ValueEnvironment intervals; - + /** * The upper bounds environment. */ @@ -73,19 +74,30 @@ public Pentagons(ValueEnvironment intervals, ValueEnvironment newBounds = upperBounds.assign(id, expression, pp, oracle); + ValueEnvironment newIntervals = intervals.assign(id, expression, pp, oracle); - // we add the semantics for assignments here as we have access to the whole assigment + // we add the semantics for assignments here as we have access to the whole assignment 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)); - } + if (op instanceof SubtractionOperator) + if (be.getLeft() instanceof Identifier && be.getRight() instanceof Constant) { + Identifier x = (Identifier) be.getLeft(); + newBounds = newBounds.putState(id, upperBounds.getState(x).add(x)); + } else if (be.getLeft() instanceof Identifier && be.getRight() instanceof Identifier) { + Identifier x = (Identifier) be.getLeft(); + Identifier y = (Identifier) be.getRight(); + + if (newBounds.getState(y).contains(x)) + newIntervals = newIntervals.putState(id, newIntervals.getState(id).glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); + + } } + return new Pentagons( - intervals.assign(id, expression, pp, oracle), + newIntervals, newBounds).closure(); } @@ -119,13 +131,13 @@ public Pentagons forgetIdentifiersIf(Predicate test) throws Semantic 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 @@ -184,12 +196,12 @@ private Pentagons closure() throws SemanticException { // glb is the union newBounds = newBounds.putState(id1, newBounds.getState(id1).glb(new UpperBounds(closure))); - + } - + return new Pentagons(intervals, newBounds); } - + @Override public Pentagons lubAux(Pentagons other) throws SemanticException { ValueEnvironment newBounds = upperBounds.lub(other.upperBounds); @@ -219,7 +231,7 @@ public Pentagons lubAux(Pentagons other) throws SemanticException { 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)); @@ -238,7 +250,7 @@ public boolean lessOrEqualAux(Pentagons other) throws SemanticException { return true; } - + @Override public int hashCode() { return Objects.hash(intervals, upperBounds); @@ -260,7 +272,7 @@ public boolean equals(Object obj) { public String toString() { return representation().toString(); } - + @Override public boolean knowsIdentifier(Identifier id) { return intervals.knowsIdentifier(id) || upperBounds.knowsIdentifier(id); From 1e1c12ce1d07522da99fa76b1976d9d9e66181dd Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 14:53:28 +0100 Subject: [PATCH 07/12] Pentagons pushScope and popScope methods --- .../lisa/analysis/numeric/Pentagons.java | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 deletions(-) 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 index 6393a37ae..0e308220d 100644 --- 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 @@ -62,8 +62,8 @@ public Pentagons() { /** * Builds the pentagons. * - * @param intervals the underlying {@link ValueEnvironment} - * @param upperBounds the underlying {@link ValueEnvironment} + * @param intervals the interval environment + * @param upperBounds the upper bounds environment */ public Pentagons(ValueEnvironment intervals, ValueEnvironment upperBounds) { this.intervals = intervals; @@ -82,16 +82,19 @@ public Pentagons assign(Identifier id, ValueExpression expression, ProgramPoint BinaryExpression be = (BinaryExpression) expression; BinaryOperator op = be.getOperator(); if (op instanceof SubtractionOperator) - if (be.getLeft() instanceof Identifier && be.getRight() instanceof Constant) { + if (be.getLeft() instanceof Identifier) { Identifier x = (Identifier) be.getLeft(); - newBounds = newBounds.putState(id, upperBounds.getState(x).add(x)); - } else if (be.getLeft() instanceof Identifier && be.getRight() instanceof Identifier) { - Identifier x = (Identifier) be.getLeft(); - Identifier y = (Identifier) be.getRight(); - - if (newBounds.getState(y).contains(x)) - newIntervals = newIntervals.putState(id, newIntervals.getState(id).glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); - + + if (be.getRight() instanceof Constant) + // r = x - c + newBounds = newBounds.putState(id, upperBounds.getState(x).add(x)); + else if (be.getRight() instanceof Identifier) { + // r = x - y + Identifier y = (Identifier) be.getRight(); + + if (newBounds.getState(y).contains(x)) + newIntervals = newIntervals.putState(id, newIntervals.getState(id).glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); + } } } @@ -140,12 +143,12 @@ public Satisfiability satisfies(ValueExpression expression, ProgramPoint pp, Sem @Override public Pentagons pushScope(ScopeToken token) throws SemanticException { - return this; // we do not care about this for the project + return new Pentagons(intervals.pushScope(token), upperBounds.pushScope(token)); } @Override public Pentagons popScope(ScopeToken token) throws SemanticException { - return this; // we do not care about this for the project + return new Pentagons(intervals.popScope(token), upperBounds.popScope(token)); } @Override From 28ae9b5f06a3b18f7c35b0774db070c85fc5049d Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 14:54:04 +0100 Subject: [PATCH 08/12] Class renaming --- .../numeric/{Pentagons.java => Pentagon.java} | 58 +++++++++---------- 1 file changed, 29 insertions(+), 29 deletions(-) rename lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/{Pentagons.java => Pentagon.java} (81%) 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/Pentagon.java similarity index 81% rename from lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagons.java rename to lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java index 0e308220d..d734e1d3c 100644 --- 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/Pentagon.java @@ -39,7 +39,7 @@ * @author Luca Negrini * @author Vincenzo Arceri */ -public class Pentagons implements ValueDomain, BaseLattice { +public class Pentagon implements ValueDomain, BaseLattice { /** * The interval environment. @@ -54,7 +54,7 @@ public class Pentagons implements ValueDomain, BaseLattice /** * Builds the pentagons. */ - public Pentagons() { + public Pentagon() { this.intervals = new ValueEnvironment<>(new Interval()).top(); this.upperBounds = new ValueEnvironment<>(new UpperBounds(true)).top(); } @@ -65,13 +65,13 @@ public Pentagons() { * @param intervals the interval environment * @param upperBounds the upper bounds environment */ - public Pentagons(ValueEnvironment intervals, ValueEnvironment upperBounds) { + public Pentagon(ValueEnvironment intervals, ValueEnvironment upperBounds) { this.intervals = intervals; this.upperBounds = upperBounds; } @Override - public Pentagons assign(Identifier id, ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + public Pentagon assign(Identifier id, ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) throws SemanticException { ValueEnvironment newBounds = upperBounds.assign(id, expression, pp, oracle); ValueEnvironment newIntervals = intervals.assign(id, expression, pp, oracle); @@ -99,37 +99,37 @@ else if (be.getRight() instanceof Identifier) { } - return new Pentagons( + return new Pentagon( newIntervals, newBounds).closure(); } @Override - public Pentagons smallStepSemantics(ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + public Pentagon smallStepSemantics(ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) throws SemanticException { - return new Pentagons( + return new Pentagon( intervals.smallStepSemantics(expression, pp, oracle), upperBounds.smallStepSemantics(expression, pp, oracle)); } @Override - public Pentagons assume(ValueExpression expression, ProgramPoint src, ProgramPoint dest, SemanticOracle oracle) + public Pentagon assume(ValueExpression expression, ProgramPoint src, ProgramPoint dest, SemanticOracle oracle) throws SemanticException { - return new Pentagons( + return new Pentagon( intervals.assume(expression, src, dest, oracle), upperBounds.assume(expression, src, dest, oracle)); } @Override - public Pentagons forgetIdentifier(Identifier id) throws SemanticException { - return new Pentagons( + public Pentagon forgetIdentifier(Identifier id) throws SemanticException { + return new Pentagon( intervals.forgetIdentifier(id), upperBounds.forgetIdentifier(id)); } @Override - public Pentagons forgetIdentifiersIf(Predicate test) throws SemanticException { - return new Pentagons( + public Pentagon forgetIdentifiersIf(Predicate test) throws SemanticException { + return new Pentagon( intervals.forgetIdentifiersIf(test), upperBounds.forgetIdentifiersIf(test)); } @@ -142,13 +142,13 @@ public Satisfiability satisfies(ValueExpression expression, ProgramPoint pp, Sem } @Override - public Pentagons pushScope(ScopeToken token) throws SemanticException { - return new Pentagons(intervals.pushScope(token), upperBounds.pushScope(token)); + public Pentagon pushScope(ScopeToken token) throws SemanticException { + return new Pentagon(intervals.pushScope(token), upperBounds.pushScope(token)); } @Override - public Pentagons popScope(ScopeToken token) throws SemanticException { - return new Pentagons(intervals.popScope(token), upperBounds.popScope(token)); + public Pentagon popScope(ScopeToken token) throws SemanticException { + return new Pentagon(intervals.popScope(token), upperBounds.popScope(token)); } @Override @@ -166,8 +166,8 @@ public StructuredRepresentation representation() { } @Override - public Pentagons top() { - return new Pentagons(intervals.top(), upperBounds.top()); + public Pentagon top() { + return new Pentagon(intervals.top(), upperBounds.top()); } @Override @@ -176,8 +176,8 @@ public boolean isTop() { } @Override - public Pentagons bottom() { - return new Pentagons(intervals.bottom(), upperBounds.bottom()); + public Pentagon bottom() { + return new Pentagon(intervals.bottom(), upperBounds.bottom()); } @Override @@ -185,7 +185,7 @@ public boolean isBottom() { return intervals.isBottom() && upperBounds.isBottom(); } - private Pentagons closure() throws SemanticException { + private Pentagon closure() throws SemanticException { ValueEnvironment newBounds = new ValueEnvironment(upperBounds.lattice, upperBounds.getMap()); for (Identifier id1 : intervals.getKeys()) { @@ -202,11 +202,11 @@ private Pentagons closure() throws SemanticException { } - return new Pentagons(intervals, newBounds); + return new Pentagon(intervals, newBounds); } @Override - public Pentagons lubAux(Pentagons other) throws SemanticException { + public Pentagon lubAux(Pentagon other) throws SemanticException { ValueEnvironment newBounds = upperBounds.lub(other.upperBounds); for (Entry entry : upperBounds) { Set closure = new HashSet<>(); @@ -232,16 +232,16 @@ public Pentagons lubAux(Pentagons other) throws SemanticException { newBounds.getState(entry.getKey()).glb(new UpperBounds(closure))); } - return new Pentagons(intervals.lub(other.intervals), newBounds); + return new Pentagon(intervals.lub(other.intervals), newBounds); } @Override - public Pentagons wideningAux(Pentagons other) throws SemanticException { - return new Pentagons(intervals.widening(other.intervals), upperBounds.widening(other.upperBounds)); + public Pentagon wideningAux(Pentagon other) throws SemanticException { + return new Pentagon(intervals.widening(other.intervals), upperBounds.widening(other.upperBounds)); } @Override - public boolean lessOrEqualAux(Pentagons other) throws SemanticException { + public boolean lessOrEqualAux(Pentagon other) throws SemanticException { if (!intervals.lessOrEqual(other.intervals)) return false; for (Entry entry : other.upperBounds) @@ -267,7 +267,7 @@ public boolean equals(Object obj) { return false; if (getClass() != obj.getClass()) return false; - Pentagons other = (Pentagons) obj; + Pentagon other = (Pentagon) obj; return Objects.equals(intervals, other.intervals) && Objects.equals(upperBounds, other.upperBounds); } From 91a2a2fa7022fce362d10d69cd57ca2df2e3d368 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 15:07:34 +0100 Subject: [PATCH 09/12] Extended assignment semantics for pentagons in reminder case --- .../imp-testcases/numeric/pentagons.imp | 12 ++++++++++-- .../numeric/pentagons/report.json | 18 +++++++++--------- ...s_tests__this,_untyped_x,_untyped_len).json | 1 + .../unive/lisa/analysis/numeric/Pentagon.java | 16 +++++++++++++--- .../unive/lisa/cron/NumericAnalysesTest.java | 8 ++++---- 5 files changed, 37 insertions(+), 18 deletions(-) create mode 100644 lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp index 62789687a..b083bf686 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons.imp @@ -32,6 +32,14 @@ class petagons_tests { assert r >= 0; } } - - + + /* + Reference: https://doi.org/10.1016/j.scico.2009.04.004 + */ + common_code_pattern_02(x, len) { + if(len >= 0) { + def r = x % len; + assert r < len; + } + } } \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json index 33a6040f9..785518ce3 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json @@ -1,17 +1,17 @@ { "warnings" : [ ], - "files" : [ "report.json", "untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json", "untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json", "untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json" ], + "files" : [ "report.json", "untyped_petagons_tests.common_code_pattern_01(petagons_tests__this,_untyped_x,_untyped_y,_untyped_r).json", "untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json", "untyped_petagons_tests.non_strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json", "untyped_petagons_tests.strict_abstraction(petagons_tests__this,_untyped_b,_untyped_x,_untyped_y).json" ], "info" : { - "cfgs" : "3", - "duration" : "426ms", - "end" : "2024-01-10T14:45:14.863+01:00", - "expressions" : "31", - "files" : "3", + "cfgs" : "4", + "duration" : "418ms", + "end" : "2024-01-10T15:05:51.619+01:00", + "expressions" : "40", + "files" : "4", "globals" : "0", - "members" : "3", + "members" : "4", "programs" : "1", - "start" : "2024-01-10T14:45:14.437+01:00", - "statements" : "17", + "start" : "2024-01-10T15:05:51.201+01:00", + "statements" : "21", "units" : "1", "version" : "0.1b8", "warnings" : "0" diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json new file mode 100644 index 000000000..a04b8a587 --- /dev/null +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/untyped_petagons_tests.common_code_pattern_02(petagons_tests__this,_untyped_x,_untyped_len).json @@ -0,0 +1 @@ +{"name":"untyped petagons_tests::common_code_pattern_02(petagons_tests* this, untyped x, untyped len)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":">=(len, 0)"},{"id":1,"text":"len"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":"r = %(x, len)"},{"id":4,"text":"r"},{"id":5,"subNodes":[6,7],"text":"%(x, len)"},{"id":6,"text":"x"},{"id":7,"text":"len"},{"id":8,"subNodes":[9],"text":"assert <(r, len)"},{"id":9,"subNodes":[10,11],"text":"<(r, len)"},{"id":10,"text":"r"},{"id":11,"text":"len"},{"id":12,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"TrueEdge"},{"sourceId":0,"destId":12,"kind":"FalseEdge"},{"sourceId":3,"destId":8,"kind":"SequentialEdge"},{"sourceId":8,"destId":12,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["len >= 0"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":1,"description":{"expressions":["len"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":3,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":4,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":5,"description":{"expressions":["x % len"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":6,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":7,"description":{"expressions":["len"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","x":"[-Inf, +Inf], {}"}}}},{"nodeId":8,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":9,"description":{"expressions":["r < len"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":10,"description":{"expressions":["r"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":11,"description":{"expressions":["len"],"state":{"heap":"monolith","type":{"len":"#TOP#","r":["float32","int32"],"this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[0, +Inf], {}","r":"[-Inf, +Inf], (len)","x":"[-Inf, +Inf], {}"}}}},{"nodeId":12,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"len":"#TOP#","this":["petagons_tests*"],"x":"#TOP#"},"value":{"len":"[-Inf, +Inf], {}","x":"[-Inf, +Inf], {}"}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java index d734e1d3c..7271a590f 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java @@ -1,5 +1,6 @@ package it.unive.lisa.analysis.numeric; +import java.util.Collections; import java.util.HashMap; import java.util.HashSet; import java.util.Map; @@ -23,6 +24,7 @@ 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.RemainderOperator; import it.unive.lisa.symbolic.value.operator.SubtractionOperator; import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; import it.unive.lisa.util.numeric.MathNumber; @@ -78,13 +80,12 @@ public Pentagon assign(Identifier id, ValueExpression expression, ProgramPoint p // we add the semantics for assignments here as we have access to the whole assignment if (expression instanceof BinaryExpression) { - BinaryExpression be = (BinaryExpression) expression; BinaryOperator op = be.getOperator(); - if (op instanceof SubtractionOperator) + if (op instanceof SubtractionOperator) { if (be.getLeft() instanceof Identifier) { Identifier x = (Identifier) be.getLeft(); - + if (be.getRight() instanceof Constant) // r = x - c newBounds = newBounds.putState(id, upperBounds.getState(x).add(x)); @@ -96,6 +97,15 @@ else if (be.getRight() instanceof Identifier) { newIntervals = newIntervals.putState(id, newIntervals.getState(id).glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); } } + } else if (op instanceof RemainderOperator && be.getRight() instanceof Identifier) { + // r = u % d + Identifier d = (Identifier) be.getRight(); + MathNumber low = intervals.getState(d).interval.getLow(); + if (low.isPositive() || low.isZero()) + newBounds = newBounds.putState(id, new UpperBounds(Collections.singleton(d))); + else + newBounds = newBounds.putState(id, new UpperBounds().top()); + } } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java index 919362333..36bb9706f 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java @@ -1,5 +1,7 @@ package it.unive.lisa.cron; +import org.junit.Test; + import it.unive.lisa.AnalysisTestExecutor; import it.unive.lisa.CronConfiguration; import it.unive.lisa.DefaultConfiguration; @@ -8,12 +10,10 @@ import it.unive.lisa.analysis.numeric.IntegerConstantPropagation; import it.unive.lisa.analysis.numeric.Interval; import it.unive.lisa.analysis.numeric.Parity; -import it.unive.lisa.analysis.numeric.Pentagons; +import it.unive.lisa.analysis.numeric.Pentagon; import it.unive.lisa.analysis.numeric.Sign; import it.unive.lisa.conf.LiSAConfiguration.DescendingPhaseType; -import org.junit.Test; - public class NumericAnalysesTest extends AnalysisTestExecutor { @Test @@ -99,7 +99,7 @@ public void testPentagons() { conf.serializeResults = true; conf.abstractState = DefaultConfiguration.simpleState( DefaultConfiguration.defaultHeapDomain(), - new Pentagons(), + new Pentagon(), DefaultConfiguration.defaultTypeDomain()); conf.testDir = "numeric"; conf.testSubDir = "pentagons"; From 0329b43e7e6967f2a251e1b74f2ad367d3678dc2 Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 15:12:33 +0100 Subject: [PATCH 10/12] Apply spotless and Javadoc --- .../unive/lisa/analysis/numeric/Pentagon.java | 113 ++++++++++++------ .../lisa/analysis/numeric/UpperBounds.java | 81 ++++++++----- .../unive/lisa/cron/NumericAnalysesTest.java | 5 +- 3 files changed, 128 insertions(+), 71 deletions(-) diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java index 7271a590f..26f682b1a 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java @@ -1,16 +1,5 @@ package it.unive.lisa.analysis.numeric; -import java.util.Collections; -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; @@ -31,12 +20,27 @@ import it.unive.lisa.util.representation.MapRepresentation; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Collections; +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; /** - * The pentagons abstract domain, a weakly relational numerical abstract domain. This abstract - * domain captures properties of the form of x ⋲ [a, b] ∧ x < y. It is more precise than the - * well known interval domain, but it is less precise than the octagon domain. - * It is implemented as a {@link ValueDomain}. + * The pentagons abstract domain, a weakly relational numeric abstract domain. + * This abstract domain captures properties of the form of x \in [a, b] + * ∧ x < y. It is more precise than the well known interval domain, but + * it is less precise than the octagon domain. It is implemented as a + * {@link ValueDomain}. + * + * @see Pentagons: + * A weakly relational abstract domain for the efficient validation of + * array accesses * * @author Luca Negrini * @author Vincenzo Arceri @@ -64,21 +68,28 @@ public Pentagon() { /** * Builds the pentagons. * - * @param intervals the interval environment + * @param intervals the interval environment * @param upperBounds the upper bounds environment */ - public Pentagon(ValueEnvironment intervals, ValueEnvironment upperBounds) { + public Pentagon( + ValueEnvironment intervals, + ValueEnvironment upperBounds) { this.intervals = intervals; this.upperBounds = upperBounds; } @Override - public Pentagon assign(Identifier id, ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + public Pentagon assign( + Identifier id, + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) throws SemanticException { ValueEnvironment newBounds = upperBounds.assign(id, expression, pp, oracle); ValueEnvironment newIntervals = intervals.assign(id, expression, pp, oracle); - // we add the semantics for assignments here as we have access to the whole assignment + // we add the semantics for assignments here as we have access to the + // whole assignment if (expression instanceof BinaryExpression) { BinaryExpression be = (BinaryExpression) expression; BinaryOperator op = be.getOperator(); @@ -86,7 +97,7 @@ public Pentagon assign(Identifier id, ValueExpression expression, ProgramPoint p if (be.getLeft() instanceof Identifier) { Identifier x = (Identifier) be.getLeft(); - if (be.getRight() instanceof Constant) + if (be.getRight() instanceof Constant) // r = x - c newBounds = newBounds.putState(id, upperBounds.getState(x).add(x)); else if (be.getRight() instanceof Identifier) { @@ -94,28 +105,31 @@ else if (be.getRight() instanceof Identifier) { Identifier y = (Identifier) be.getRight(); if (newBounds.getState(y).contains(x)) - newIntervals = newIntervals.putState(id, newIntervals.getState(id).glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); + newIntervals = newIntervals.putState(id, newIntervals.getState(id) + .glb(new Interval(MathNumber.ONE, MathNumber.PLUS_INFINITY))); } } } else if (op instanceof RemainderOperator && be.getRight() instanceof Identifier) { // r = u % d Identifier d = (Identifier) be.getRight(); MathNumber low = intervals.getState(d).interval.getLow(); - if (low.isPositive() || low.isZero()) + if (low.isPositive() || low.isZero()) newBounds = newBounds.putState(id, new UpperBounds(Collections.singleton(d))); else newBounds = newBounds.putState(id, new UpperBounds().top()); } } - return new Pentagon( newIntervals, newBounds).closure(); } @Override - public Pentagon smallStepSemantics(ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + public Pentagon smallStepSemantics( + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) throws SemanticException { return new Pentagon( intervals.smallStepSemantics(expression, pp, oracle), @@ -123,7 +137,11 @@ public Pentagon smallStepSemantics(ValueExpression expression, ProgramPoint pp, } @Override - public Pentagon assume(ValueExpression expression, ProgramPoint src, ProgramPoint dest, SemanticOracle oracle) + public Pentagon assume( + ValueExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) throws SemanticException { return new Pentagon( intervals.assume(expression, src, dest, oracle), @@ -131,33 +149,43 @@ public Pentagon assume(ValueExpression expression, ProgramPoint src, ProgramPoin } @Override - public Pentagon forgetIdentifier(Identifier id) throws SemanticException { + public Pentagon forgetIdentifier( + Identifier id) + throws SemanticException { return new Pentagon( intervals.forgetIdentifier(id), upperBounds.forgetIdentifier(id)); } @Override - public Pentagon forgetIdentifiersIf(Predicate test) throws SemanticException { + public Pentagon forgetIdentifiersIf( + Predicate test) + throws SemanticException { return new Pentagon( intervals.forgetIdentifiersIf(test), upperBounds.forgetIdentifiersIf(test)); } - @Override - public Satisfiability satisfies(ValueExpression expression, ProgramPoint pp, SemanticOracle oracle) + 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 Pentagon pushScope(ScopeToken token) throws SemanticException { + public Pentagon pushScope( + ScopeToken token) + throws SemanticException { return new Pentagon(intervals.pushScope(token), upperBounds.pushScope(token)); } @Override - public Pentagon popScope(ScopeToken token) throws SemanticException { + public Pentagon popScope( + ScopeToken token) + throws SemanticException { return new Pentagon(intervals.popScope(token), upperBounds.popScope(token)); } @@ -196,7 +224,8 @@ public boolean isBottom() { } private Pentagon closure() throws SemanticException { - ValueEnvironment newBounds = new ValueEnvironment(upperBounds.lattice, upperBounds.getMap()); + ValueEnvironment< + UpperBounds> newBounds = new ValueEnvironment(upperBounds.lattice, upperBounds.getMap()); for (Identifier id1 : intervals.getKeys()) { Set closure = new HashSet<>(); @@ -216,7 +245,9 @@ private Pentagon closure() throws SemanticException { } @Override - public Pentagon lubAux(Pentagon other) throws SemanticException { + public Pentagon lubAux( + Pentagon other) + throws SemanticException { ValueEnvironment newBounds = upperBounds.lub(other.upperBounds); for (Entry entry : upperBounds) { Set closure = new HashSet<>(); @@ -246,19 +277,23 @@ public Pentagon lubAux(Pentagon other) throws SemanticException { } @Override - public Pentagon wideningAux(Pentagon other) throws SemanticException { + public Pentagon wideningAux( + Pentagon other) + throws SemanticException { return new Pentagon(intervals.widening(other.intervals), upperBounds.widening(other.upperBounds)); } @Override - public boolean lessOrEqualAux(Pentagon other) throws SemanticException { + public boolean lessOrEqualAux( + Pentagon 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)) + .compareTo(intervals.getState(bound).interval.getLow()) < 0)) return false; return true; @@ -270,7 +305,8 @@ public int hashCode() { } @Override - public boolean equals(Object obj) { + public boolean equals( + Object obj) { if (this == obj) return true; if (obj == null) @@ -287,7 +323,8 @@ public String toString() { } @Override - public boolean knowsIdentifier(Identifier id) { + 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 index 305f653de..89d05308a 100644 --- 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 @@ -1,12 +1,5 @@ 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; @@ -24,10 +17,16 @@ import it.unive.lisa.util.representation.SetRepresentation; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Collections; +import java.util.HashSet; +import java.util.Iterator; +import java.util.Objects; +import java.util.Set; +import java.util.TreeSet; /** - * The upper bounds abstract domain. It is implemented as - * a {@link BaseNonRelationalValueDomain}. + * The upper bounds abstract domain. It is implemented as a + * {@link BaseNonRelationalValueDomain}. * * @author Luca Negrini * @author Vincenzo Arceri @@ -38,7 +37,7 @@ public class UpperBounds implements BaseNonRelationalValueDomain, I * The abstract top element. */ private static final UpperBounds TOP = new UpperBounds(true); - + /** * The abstract bottom element. */ @@ -48,7 +47,7 @@ public class UpperBounds implements BaseNonRelationalValueDomain, I * The flag to set abstract top state. */ private final boolean isTop; - + /** * The set containing the bounds. */ @@ -60,13 +59,15 @@ public class UpperBounds implements BaseNonRelationalValueDomain, I public UpperBounds() { this(true); } - + /** * Builds the upper bounds. * - * @param isTop {@code true} if the abstract domain is top; otherwise {@code false}. + * @param isTop {@code true} if the abstract domain is top; otherwise + * {@code false}. */ - public UpperBounds(boolean isTop) { + public UpperBounds( + boolean isTop) { this.bounds = null; this.isTop = isTop; } @@ -76,12 +77,12 @@ public UpperBounds(boolean isTop) { * * @param bounds the bounds to set */ - public UpperBounds(Set bounds) { + public UpperBounds( + Set bounds) { this.bounds = bounds; this.isTop = false; } - @Override public StructuredRepresentation representation() { if (isTop()) @@ -105,33 +106,42 @@ public UpperBounds bottom() { public boolean isBottom() { return !isTop && bounds.isEmpty(); } - + @Override - public UpperBounds lubAux(UpperBounds other) throws SemanticException { + 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 { + 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 { + public boolean lessOrEqualAux( + UpperBounds other) + throws SemanticException { return bounds.containsAll(other.bounds); } @Override - public UpperBounds wideningAux(UpperBounds other) throws SemanticException { + public UpperBounds wideningAux( + UpperBounds other) + throws SemanticException { return other.bounds.containsAll(bounds) ? other : TOP; } @Override - public boolean equals(Object obj) { + public boolean equals( + Object obj) { if (this == obj) return true; if (obj == null) @@ -148,13 +158,18 @@ public int hashCode() { } @Override - public ValueEnvironment assumeBinaryExpression(ValueEnvironment environment, - BinaryOperator operator, ValueExpression left, ValueExpression right, ProgramPoint src, ProgramPoint dest, - SemanticOracle oracle) throws SemanticException { + 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; @@ -203,12 +218,16 @@ public Iterator iterator() { } /** - * Checks if this bounds contains a specified identifier of a program variable. + * Checks if this bounds contains a specified identifier of a program + * variable. * * @param id the identifier to check - * @return {@code true} if this bounds contains the specified identifier; otherwise, {@code false}. + * + * @return {@code true} if this bounds contains the specified identifier; + * otherwise, {@code false}. */ - public boolean contains(Identifier id) { + public boolean contains( + Identifier id) { return bounds != null && bounds.contains(id); } @@ -216,9 +235,11 @@ public boolean contains(Identifier id) { * Adds the specified identifier of a program variable in the bounds. * * @param id the identifier to add in the bounds. + * * @return the updated bounds. */ - public UpperBounds add(Identifier id) { + public UpperBounds add( + Identifier id) { Set res = new HashSet<>(); if (!isTop() && !isBottom()) res.addAll(bounds); diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java index 36bb9706f..4c4628c33 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/NumericAnalysesTest.java @@ -1,7 +1,5 @@ package it.unive.lisa.cron; -import org.junit.Test; - import it.unive.lisa.AnalysisTestExecutor; import it.unive.lisa.CronConfiguration; import it.unive.lisa.DefaultConfiguration; @@ -13,6 +11,7 @@ import it.unive.lisa.analysis.numeric.Pentagon; import it.unive.lisa.analysis.numeric.Sign; import it.unive.lisa.conf.LiSAConfiguration.DescendingPhaseType; +import org.junit.Test; public class NumericAnalysesTest extends AnalysisTestExecutor { @@ -92,7 +91,7 @@ public void testNonRedundantSetOfInterval() { conf.compareWithOptimization = false; perform(conf); } - + @Test public void testPentagons() { CronConfiguration conf = new CronConfiguration(); From 0495a61488fe8812437267b13c51824a8f90006a Mon Sep 17 00:00:00 2001 From: VincenzoArceri Date: Wed, 10 Jan 2024 15:20:32 +0100 Subject: [PATCH 11/12] Apply spotless --- .../main/java/it/unive/lisa/analysis/numeric/Pentagon.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java index 26f682b1a..e984702e5 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java @@ -32,9 +32,9 @@ /** * The pentagons abstract domain, a weakly relational numeric abstract domain. - * This abstract domain captures properties of the form of x \in [a, b] - * ∧ x < y. It is more precise than the well known interval domain, but - * it is less precise than the octagon domain. It is implemented as a + * This abstract domain captures properties of the form of x \in [a, b] ∧ x + * < y. It is more precise than the well known interval domain, but it is + * less precise than the octagon domain. It is implemented as a * {@link ValueDomain}. * * @see Date: Wed, 10 Jan 2024 15:26:28 +0100 Subject: [PATCH 12/12] Javadoc --- .../it/unive/lisa/analysis/numeric/Pentagon.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java index e984702e5..aa0bea437 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Pentagon.java @@ -31,19 +31,19 @@ import org.apache.commons.collections4.CollectionUtils; /** - * The pentagons abstract domain, a weakly relational numeric abstract domain. - * This abstract domain captures properties of the form of x \in [a, b] ∧ x - * < y. It is more precise than the well known interval domain, but it is - * less precise than the octagon domain. It is implemented as a + * /** The pentagons abstract domain, a weakly relational numeric abstract + * domain. This abstract domain captures properties of the form of x \in [a, b] + * ∧ x < y. It is more precise than the well known interval domain, but + * it is less precise than the octagon domain. It is implemented as a * {@link ValueDomain}. * + * @author Luca Negrini + * @author Vincenzo Arceri + * * @see Pentagons: * A weakly relational abstract domain for the efficient validation of * array accesses - * - * @author Luca Negrini - * @author Vincenzo Arceri */ public class Pentagon implements ValueDomain, BaseLattice {