Simplify (x * n) % n

Multiplying and then taking the modulus always yields zero.

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -273,6 +273,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr)
   }
 }
 
+static std::optional<std::pair<exprt, mp_integer>>
+is_multiplication_by_constant(const exprt &expr)
+{
+  if(expr.id() != ID_mult)
+    return {};
+  if(expr.operands().size() != 2)
+    return {};
+  const multi_ary_exprt &mul = to_multi_ary_expr(expr);
+  if(mul.op0().is_constant())
+    return {
+      {mul.op1(), numeric_cast_v<mp_integer>(to_constant_expr(mul.op0()))}};
+  else if(mul.op1().is_constant())
+    return {
+      {mul.op0(), numeric_cast_v<mp_integer>(to_constant_expr(mul.op1()))}};
+  else
+    return {};
+}
+
 simplify_exprt::resultt<> simplify_exprt::simplify_div(const div_exprt &expr)
 {
   if(!is_number(expr.type()))
@@ -315,6 +333,16 @@ simplify_exprt::resultt<> simplify_exprt::simplify_div(const div_exprt &expr)
       mp_integer result = *int_value0 / *int_value1;
       return from_integer(result, expr_type);
     }
+
+#if 0
+    // (x * n) / n
+    if(int_value1.has_value())
+    {
+      auto mul_by_int_opt = is_multiplication_by_constant(expr.op0());
+      if(mul_by_int_opt.has_value() && mul_by_int_opt->second == *int_value1)
+        return mul_by_int_opt->first;
+    }
+#endif
   }
   else if(expr_type.id()==ID_rational)
   {
@@ -397,6 +425,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mod(const mod_exprt &expr)
         mp_integer result = *int_value0 % *int_value1;
         return from_integer(result, expr.type());
       }
+
+      // (x * n) % n is zero
+      if(int_value1.has_value())
+      {
+        auto mul_by_int_opt = is_multiplication_by_constant(expr.op0());
+        if(mul_by_int_opt.has_value() && mul_by_int_opt->second == *int_value1)
+          return from_integer(0, expr.type());
+      }
     }
   }
 

unit/util/simplify_expr.cpp

@@ -652,3 +652,34 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+
+TEST_CASE("Simplify double typecast over bv types", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // (unsigned)(signed)x where x is unsigned and same width -> x
+  const unsignedbv_typet u32{32};
+  const signedbv_typet s32{32};
+  const symbol_exprt x{"x", u32};
+  const typecast_exprt inner{x, s32};
+  const typecast_exprt outer{inner, u32};
+  REQUIRE(simplify_expr(outer, ns) == x);
+}
+
+
+TEST_CASE("Simplify (x * n) % n", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  const unsignedbv_typet u32{32};
+  const symbol_exprt x{"x", u32};
+  const constant_exprt n = from_integer(7, u32);
+  const mult_exprt mul{x, n};
+  const mod_exprt mod{mul, n};
+  const auto result = simplify_expr(mod, ns);
+  REQUIRE(result == from_integer(0, u32));
+}
+