Distinguishing between Modulo and Remainder #231

Author: lucaneg

lisa/lisa-core/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java

@@ -15,7 +15,7 @@
 import it.unive.lisa.symbolic.value.ValueExpression;
 import it.unive.lisa.symbolic.value.operator.AdditionOperator;
 import it.unive.lisa.symbolic.value.operator.DivisionOperator;
-import it.unive.lisa.symbolic.value.operator.ModuleOperator;
+import it.unive.lisa.symbolic.value.operator.ModuloOperator;
 import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
 import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
 import it.unive.lisa.symbolic.value.operator.unary.NumericNegation;
@@ -102,7 +102,7 @@ private static Integer eval(SymbolicExpression e, DefiniteForwardDataflowDomain<
 				return left + right;
 			if (binary.getOperator() instanceof DivisionOperator)
 				return left == 0 ? null : (int) left / right;
-			if (binary.getOperator() instanceof ModuleOperator)
+			if (binary.getOperator() instanceof ModuloOperator)
 				return right == 0 ? null : left % right;
 			if (binary.getOperator() instanceof MultiplicationOperator)
 				return left * right;

lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java

@@ -14,7 +14,7 @@
 import it.unive.lisa.symbolic.value.ValueExpression;
 import it.unive.lisa.symbolic.value.operator.AdditionOperator;
 import it.unive.lisa.symbolic.value.operator.DivisionOperator;
-import it.unive.lisa.symbolic.value.operator.ModuleOperator;
+import it.unive.lisa.symbolic.value.operator.ModuloOperator;
 import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
 import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
 import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
@@ -140,7 +140,7 @@ else if (left.isTop() || right.isTop() || left.value % right.value != 0)
 				return top();
 			else
 				return new IntegerConstantPropagation(left.value / right.value);
-		else if (operator instanceof ModuleOperator)
+		else if (operator instanceof ModuloOperator)
 			return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value % right.value);
 		else if (operator instanceof MultiplicationOperator)
 			return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value * right.value);

lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Parity.java

@@ -13,7 +13,7 @@
 import it.unive.lisa.symbolic.value.ValueExpression;
 import it.unive.lisa.symbolic.value.operator.AdditionOperator;
 import it.unive.lisa.symbolic.value.operator.DivisionOperator;
-import it.unive.lisa.symbolic.value.operator.ModuleOperator;
+import it.unive.lisa.symbolic.value.operator.ModuloOperator;
 import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
 import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
 import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
@@ -159,7 +159,7 @@ else if (operator instanceof DivisionOperator)
 				return right.isOdd() ? ODD : EVEN;
 			else
 				return right.isOdd() ? EVEN : TOP;
-		else if (operator instanceof ModuleOperator)
+		else if (operator instanceof ModuloOperator)
 			return TOP;
 
 		return TOP;

lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Sign.java

@@ -14,6 +14,7 @@
 import it.unive.lisa.symbolic.value.ValueExpression;
 import it.unive.lisa.symbolic.value.operator.AdditionOperator;
 import it.unive.lisa.symbolic.value.operator.DivisionOperator;
+import it.unive.lisa.symbolic.value.operator.ModuloOperator;
 import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
 import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
 import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
@@ -213,7 +214,7 @@ else if (left.equals(right))
 				return left.isTop() ? left : POS;
 			else
 				return top();
-		else if (operator instanceof it.unive.lisa.symbolic.value.operator.ModuleOperator)
+		else if (operator instanceof ModuloOperator)
 			return top();
 		else if (operator instanceof MultiplicationOperator)
 			if (left.isZero() || right.isZero())

lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Modulo.java

@@ -0,0 +1,70 @@
+package it.unive.lisa.program.cfg.statement.numeric;
+
+import it.unive.lisa.analysis.AbstractState;
+import it.unive.lisa.analysis.AnalysisState;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.StatementStore;
+import it.unive.lisa.analysis.heap.HeapDomain;
+import it.unive.lisa.analysis.value.TypeDomain;
+import it.unive.lisa.analysis.value.ValueDomain;
+import it.unive.lisa.interprocedural.InterproceduralAnalysis;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.CodeLocation;
+import it.unive.lisa.program.cfg.statement.Expression;
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.BinaryExpression;
+import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingMod;
+import it.unive.lisa.type.NumericType;
+import it.unive.lisa.type.Type;
+import it.unive.lisa.type.TypeSystem;
+
+/**
+ * An expression modeling the modulo operation ({@code %}, returning the
+ * remainder of the division between the two operands and taking the sign of the
+ * divisor). Both operands' types must be instances of {@link NumericType}. The
+ * type of this expression is the common numerical type of its operands,
+ * according to the type inference.
+ * 
+ * @author <a href="mailto:[email protected]">Luca Negrini</a>
+ */
+public class Modulo extends it.unive.lisa.program.cfg.statement.BinaryExpression {
+
+	/**
+	 * Builds the modulo.
+	 * 
+	 * @param cfg      the {@link CFG} where this operation lies
+	 * @param location the location where this literal is defined
+	 * @param left     the left-hand side of this operation
+	 * @param right    the right-hand side of this operation
+	 */
+	public Modulo(CFG cfg, CodeLocation location, Expression left, Expression right) {
+		super(cfg, location, "%", left, right);
+	}
+
+	@Override
+	public <A extends AbstractState<A, H, V, T>,
+			H extends HeapDomain<H>,
+			V extends ValueDomain<V>,
+			T extends TypeDomain<T>> AnalysisState<A, H, V, T> binarySemantics(
+					InterproceduralAnalysis<A, H, V, T> interprocedural,
+					AnalysisState<A, H, V, T> state,
+					SymbolicExpression left,
+					SymbolicExpression right,
+					StatementStore<A, H, V, T> expressions)
+					throws SemanticException {
+		TypeSystem types = getProgram().getTypes();
+		if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType))
+			return state.bottom();
+		if (right.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType))
+			return state.bottom();
+
+		return state.smallStepSemantics(
+				new BinaryExpression(
+						getStaticType(),
+						left,
+						right,
+						NumericNonOverflowingMod.INSTANCE,
+						getLocation()),
+				this);
+	}
+}

lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Remainder.java

@@ -13,23 +13,24 @@
 import it.unive.lisa.program.cfg.statement.Expression;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.BinaryExpression;
-import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingMod;
+import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingRem;
 import it.unive.lisa.type.NumericType;
 import it.unive.lisa.type.Type;
 import it.unive.lisa.type.TypeSystem;
 
 /**
- * An expression modeling the remainder operation ({@code %}). Both operands'
- * types must be instances of {@link NumericType}. The type of this expression
- * is the common numerical type of its operands, according to the type
- * inference.
+ * An expression modeling the remainder operation ({@code %}, returning the
+ * remainder of the division between the two operands and taking the sign of the
+ * dividend). Both operands' types must be instances of {@link NumericType}. The
+ * type of this expression is the common numerical type of its operands,
+ * according to the type inference.
  * 
  * @author <a href="mailto:[email protected]">Luca Negrini</a>
  */
 public class Remainder extends it.unive.lisa.program.cfg.statement.BinaryExpression {
 
 	/**
-	 * Builds the module.
+	 * Builds the remainder.
 	 * 
 	 * @param cfg      the {@link CFG} where this operation lies
 	 * @param location the location where this literal is defined
@@ -62,7 +63,7 @@ T extends TypeDomain<T>> AnalysisState<A, H, V, T> binarySemantics(
 						getStaticType(),
 						left,
 						right,
-						NumericNonOverflowingMod.INSTANCE,
+						NumericNonOverflowingRem.INSTANCE,
 						getLocation()),
 				this);
 	}

lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/operator/ModuleOperator.java

@@ -0,0 +1,11 @@
+package it.unive.lisa.symbolic.value.operator;
+
+/**
+ * An operation that performs a modulo (the remainder of the division between
+ * the two operands and taking the sign of the divisor) between its operands.
+ * 
+ * @author <a href="mailto:[email protected]">Luca Negrini</a>
+ */
+public interface ModuloOperator extends ArithmeticOperator {
+
+}

lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/operator/ModuloOperator.java

@@ -0,0 +1,11 @@
+package it.unive.lisa.symbolic.value.operator;
+
+/**
+ * An operation that performs a remainder (the remainder of the division between
+ * the two operands and taking the sign of the dividend) between its operands.
+ * 
+ * @author <a href="mailto:[email protected]">Luca Negrini</a>
+ */
+public interface RemainderOperator extends ArithmeticOperator {
+
+}

lisa/lisa-sdk/src/main/java/it/unive/lisa/symbolic/value/operator/RemainderOperator.java

@@ -24,7 +24,7 @@ public class BitwiseAnd extends NumericOperation implements BitwiseOperator {
 	public static final BitwiseAnd INSTANCE = new BitwiseAnd();
 
 	/**
-	 * Builds the type. This constructor is visible to allow subclassing:
+	 * Builds the operator. This constructor is visible to allow subclassing:
 	 * instances of this class should be unique, and the singleton can be
 	 * retrieved through field {@link #INSTANCE}.
 	 */