#12 created Lattice and SemanticDomain interfaces

lisa/src/main/java/it/unive/lisa/analysis/BaseLattice.java

@@ -0,0 +1,100 @@
+package it.unive.lisa.analysis;
+
+/**
+ * A base implementation of the {@link Lattice} interface, handling base cases
+ * of the methods exposed by that interface. All implementers of {@link Lattice}
+ * should inherit from this class for ensuring a consistent behavior on the base
+ * cases, unless explicitly needed.
+ * 
+ * @param <L> the concrete {@link BaseLattice} instance
+ * 
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public abstract class BaseLattice<L extends BaseLattice<L>> implements Lattice<L> {
+
+	@Override
+	@SuppressWarnings("unchecked")
+	public final L lub(L other) {
+		if (other == null || other == bottom() || this == top() || this == other || equals(other))
+			return (L) this;
+
+		if (this == bottom() || other == top())
+			return other;
+
+		return lubAux(other);
+	}
+
+	/**
+	 * Performs the least upper bound operation between this lattice element and the
+	 * given one, assuming that:
+	 * <ul>
+	 * <li>{@code other} is not {@code null}</li>
+	 * <li>{@code other} is neither <i>top</i> nor <i>bottom</i></li>
+	 * <li>{@code this} is neither <i>top</i> nor <i>bottom</i></li>
+	 * <li>{@code this} and {@code other} are not the same object (according both to
+	 * {@code ==} and to {@link Object#equals(Object)})</li>
+	 * </ul>
+	 * 
+	 * @param other the other lattice element
+	 * @return the least upper bound
+	 */
+	protected abstract L lubAux(L other);
+
+	@Override
+	@SuppressWarnings("unchecked")
+	public final L widening(L other) {
+		if (other == null || other == bottom() || this == top() || this == other || equals(other))
+			return (L) this;
+
+		if (this == bottom() || other == top())
+			return other;
+
+		return wideningAux(other);
+	}
+
+	/**
+	 * Performs the widening operation between this lattice element and the given
+	 * one, assuming that:
+	 * <ul>
+	 * <li>{@code other} is not {@code null}</li>
+	 * <li>{@code other} is neither <i>top</i> nor <i>bottom</i></li>
+	 * <li>{@code this} is neither <i>top</i> nor <i>bottom</i></li>
+	 * <li>{@code this} and {@code other} are not the same object (according both to
+	 * {@code ==} and to {@link Object#equals(Object)})</li>
+	 * </ul>
+	 * 
+	 * @param other the other lattice element
+	 * @return the least upper bound
+	 */
+	protected abstract L wideningAux(L other);
+
+	@Override
+	public final boolean lessOrEqual(L other) {
+		if (other == null)
+			return false;
+
+		if (this == other || this == bottom() || other == top() || equals(other))
+			return true;
+
+		if (this == top() || other == bottom())
+			return false;
+
+		return lessOrEqualAux(other);
+	}
+
+	/**
+	 * Yields {@code true} if and only if this lattice element is in relation with
+	 * (usually represented through &le;) the given one, assuming that:
+	 * <ul>
+	 * <li>{@code other} is not {@code null}</li>
+	 * <li>{@code other} is neither <i>top</i> nor <i>bottom</i></li>
+	 * <li>{@code this} is neither <i>top</i> nor <i>bottom</i></li>
+	 * <li>{@code this} and {@code other} are not the same object (according both to
+	 * {@code ==} and to {@link Object#equals(Object)})</li>
+	 * </ul>
+	 * 
+	 * @param other the other lattice element
+	 * @return {@code true} if and only if that condition holds
+	 */
+	protected abstract boolean lessOrEqualAux(L other);
+}

lisa/src/main/java/it/unive/lisa/analysis/Lattice.java

@@ -0,0 +1,88 @@
+package it.unive.lisa.analysis;
+
+/**
+ * An interface for elements that follow a lattice structure. Implementers of
+ * this interface should inherit from {@link BaseLattice}, unless explicitly
+ * needed.
+ * 
+ * @param <L> the concrete {@link Lattice} instance
+ *
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public interface Lattice<L extends Lattice<L>> {
+
+	/**
+	 * Performs the least upper bound operation between this lattice element and the
+	 * given one. This operation is commutative.
+	 * 
+	 * @param other the other lattice element
+	 * @return the least upper bound
+	 */
+	L lub(L other);
+
+	/**
+	 * Performs the widening operation between this lattice element and the given
+	 * one. This operation is not commutative.
+	 * 
+	 * @param other the other lattice element
+	 * @return the least upper bound
+	 */
+	L widening(L other);
+
+	/**
+	 * Yields {@code true} if and only if this lattice element is in relation with
+	 * (usually represented through &le;) the given one. This operation is not
+	 * commutative.
+	 * 
+	 * @param other the other lattice element
+	 * @return {@code true} if and only if that condition holds
+	 */
+	boolean lessOrEqual(L other);
+
+	/**
+	 * Yields the top element of this lattice. The returned element should be unique
+	 * across different calls to this method, since {@link #isTop()} uses reference
+	 * equality by default. If the value returned by this method is not a singleton,
+	 * override {@link #isTop()} accordingly to provide a coherent test.
+	 * 
+	 * @return the top element
+	 */
+	L top();
+
+	/**
+	 * Yields the bottom element of this lattice. The returned element should be
+	 * unique across different calls to this method, since {@link #isBottom()} uses
+	 * reference equality by default. If the value returned by this method is not a
+	 * singleton, override {@link #isBottom()} accordingly to provide a coherent
+	 * test.
+	 * 
+	 * @return the bottom element
+	 */
+	L bottom();
+
+	/**
+	 * Yields {@code true} if and only if this object represents the top of the
+	 * lattice. The default implementation of this method uses reference equality
+	 * between {@code this} and the value returned by {@link #top()}, thus assuming
+	 * that the top element is a singleton. If this is not the case, override this
+	 * method accordingly to provide a coherent test.
+	 * 
+	 * @return {@code true} if this is the top of the lattice
+	 */
+	public default boolean isTop() {
+		return this == top();
+	}
+
+	/**
+	 * Yields {@code true} if and only if this object represents the bottom of the
+	 * lattice. The default implementation of this method uses reference equality
+	 * between {@code this} and the value returned by {@link #bottom()}, thus
+	 * assuming that the bottom element is a singleton. If this is not the case,
+	 * override this method accordingly to provide a coherent test.
+	 * 
+	 * @return {@code true} if this is the bottom of the lattice
+	 */
+	public default boolean isBottom() {
+		return this == bottom();
+	}
+}

lisa/src/main/java/it/unive/lisa/analysis/SemanticDomain.java

@@ -0,0 +1,172 @@
+package it.unive.lisa.analysis;
+
+import it.unive.lisa.symbolic.Identifier;
+import it.unive.lisa.symbolic.SymbolicExpression;
+
+/**
+ * A domain able to determine how abstract information evolves thanks to the
+ * semantics of statements and expressions.
+ * 
+ * @param <D> the concrete {@link SemanticDomain} instance
+ * @param <E> the type of {@link SymbolicExpression} that this domain can
+ *            process
+ * @param <I> the type of variable {@link Identifier} that this domain can
+ *            handle
+ * 
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public interface SemanticDomain<D extends SemanticDomain<D, E, I>, E extends SymbolicExpression, I extends Identifier> {
+
+	/**
+	 * Yields a copy of this domain, where {@code id} has been assigned to
+	 * {@code value}.
+	 * 
+	 * @param id    the identifier to assign the value to
+	 * @param value the value to assign
+	 * @return a copy of this domain, modified by the assignment
+	 */
+	D assign(I id, E value);
+
+	/**
+	 * Yields a copy of this domain, that has been modified accordingly to the
+	 * semantics of the given {@code expression}.
+	 * 
+	 * @param expression the expression whose semantics need to be computed
+	 * @return a copy of this domain, modified accordingly to the semantics of
+	 *         {@code expression}
+	 */
+	D smallStepSemantics(E expression);
+
+	/**
+	 * Yields a copy of this domain, modified by assuming that the given expression
+	 * holds. It is required that the returned domain is in relation with this one.
+	 * A safe (but imprecise) implementation of this method can always return
+	 * {@code this}.
+	 * 
+	 * @param expression the expression to assume to hold.
+	 * @return the (optionally) modified copy of this domain
+	 */
+	D assume(E expression);
+
+	/**
+	 * Checks if the given expression is satisfied by the abstract values of this
+	 * domain, returning an instance of {@link Satisfiability}.
+	 * 
+	 * @param expression the expression whose satisfiability is to be evaluated
+	 * @return {@link Satisfiability#SATISFIED} is the expression is satisfied by
+	 *         the values of this domain, {@link Satisfiability#NOT_SATISFIED} if it
+	 *         is not satisfied, or {@link Satisfiability#UNKNOWN} if it is either
+	 *         impossible to determine if it satisfied, or if it is satisfied by
+	 *         some values and not by some others (this is equivalent to a TOP
+	 *         boolean value)
+	 */
+	Satisfiability satisfy(E expression);
+
+	/**
+	 * The satisfiability of an expression.
+	 * 
+	 * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+	 */
+	public enum Satisfiability {
+		/**
+		 * Represent the fact that an expression is satisfied.
+		 */
+		SATISFIED {
+			@Override
+			public Satisfiability negate() {
+				return NOT_SATISFIED;
+			}
+
+			@Override
+			public Satisfiability and(Satisfiability other) {
+				return other;
+			}
+
+			@Override
+			public Satisfiability or(Satisfiability other) {
+				return this;
+			}
+		},
+
+		/**
+		 * Represent the fact that an expression is not satisfied.
+		 */
+		NOT_SATISFIED {
+			@Override
+			public Satisfiability negate() {
+				return SATISFIED;
+			}
+
+			@Override
+			public Satisfiability and(Satisfiability other) {
+				return this;
+			}
+
+			@Override
+			public Satisfiability or(Satisfiability other) {
+				return other;
+			}
+		},
+
+		/**
+		 * Represent the fact that it is not possible to determine whether or not an
+		 * expression is satisfied.
+		 */
+		UNKNOWN {
+			@Override
+			public Satisfiability negate() {
+				return this;
+			}
+
+			@Override
+			public Satisfiability and(Satisfiability other) {
+				if (other == NOT_SATISFIED)
+					return other;
+
+				return this;
+			}
+
+			@Override
+			public Satisfiability or(Satisfiability other) {
+				if (other == SATISFIED)
+					return other;
+
+				return this;
+			}
+		};
+
+		/**
+		 * Negates the current satisfiability, getting the opposite result.
+		 * 
+		 * @return the negation of this satisfiability instance
+		 */
+		public abstract Satisfiability negate();
+
+		/**
+		 * Performs a logical and between this satisfiability and the given one.
+		 * 
+		 * @param other the other satisfiability
+		 * @return the logical and between the two satisfiability instances
+		 */
+		public abstract Satisfiability and(Satisfiability other);
+
+		/**
+		 * Performs a logical or between this satisfiability and the given one.
+		 * 
+		 * @param other the other satisfiability
+		 * @return the logical or between the two satisfiability instances
+		 */
+		public abstract Satisfiability or(Satisfiability other);
+
+		/**
+		 * Transforms a boolean value to a {@link Satisfiability} instance.
+		 * 
+		 * @param bool the boolean to transform
+		 * @return {@link #SATISFIED} if {@code bool} is {@code true},
+		 *         {@link #NOT_SATISFIED} otherwise
+		 */
+		public static Satisfiability fromBoolean(boolean bool) {
+			return bool ? SATISFIED : NOT_SATISFIED;
+		}
+	}
+}

lisa/src/main/java/it/unive/lisa/symbolic/Identifier.java

@@ -0,0 +1,5 @@
+package it.unive.lisa.symbolic;
+
+public interface Identifier {
+
+}

lisa/src/main/java/it/unive/lisa/symbolic/SymbolicExpression.java

@@ -0,0 +1,5 @@
+package it.unive.lisa.symbolic;
+
+public abstract class SymbolicExpression {
+
+}