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())