Merge pull request #7761 from NlightNFotis/simplify_interval_domain

Author: NlightNFotis

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c

@@ -8,7 +8,7 @@ int main(int argc, char **argv)
 
     __CPROVER_assert(
         __CPROVER_exists { int z; (0 < z && z < 2) &&
-            __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == * i }},
+            __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == *i }},
         "there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1");
 }
 // clang-format on

regression/cbmc/simplify_singleton_interval_7690/negative_test.desc

@@ -0,0 +1,18 @@
+CORE 
+--trace
+singleton_interval_simp_neg.c
+^VERIFICATION FAILED$
+^\[main\.assertion\.1\] line \d expected failure: paths where x is unbounded explored: FAILURE$
+^\[main\.assertion\.2\] line \d+ expected failure: paths where 0 \<= x \<= 15 explored: FAILURE$
+^\[main\.assertion\.3\] line \d+ expected success: paths where x \<= 15 explored: SUCCESS$
+y=-6 \(11111111 11111111 11111111 11111010\)
+x=14 \(00000000 00000000 00000000 00001110\)
+y=34 \(00000000 00000000 00000000 00100010\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests the negative case of the simplification of the singleton interval
+(i.e when the presented interval *is* the *not* the singleton interval - 
+the set of possible values that the bounded variable can take has cardinality
+> 1).

regression/cbmc/simplify_singleton_interval_7690/positive_test.desc

@@ -0,0 +1,14 @@
+CORE 
+--trace
+singleton_interval_simp.c
+^VERIFICATION FAILED$
+^\[main\.assertion\.1\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$
+^\[main\.assertion\.2\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$
+x=15 \(00000000 00000000 00000000 00001111\)
+y=35 \(00000000 00000000 00000000 00100011\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests the positive case of the simplification of the singleton interval
+(i.e when the presented interval *is* the singleton interval)

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c

@@ -0,0 +1,17 @@
+// Positive test for singleton interval simplification.
+// Notice that the sequence of the inequalities in this
+// expression is different to the one in
+// `singleton_interval_in_assume_7690.c`.
+
+int main()
+{
+  int x;
+  __CPROVER_assume(x >= 15 && x <= 15);
+  int y = x + 20;
+
+  __CPROVER_assert(
+    y != 35, "expected failure: only paths where x == 15 explored");
+  __CPROVER_assert(
+    y == 34, "expected failure: only paths where x == 15 explored");
+  return 0;
+}

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c

@@ -0,0 +1,18 @@
+// Negative test for singleton interval simplification.
+
+int main()
+{
+  int x;
+  int y = x + 20;
+
+  __CPROVER_assert(
+    y != -6, "expected failure: paths where x is unbounded explored");
+
+  __CPROVER_assume(x >= 0 && x <= 15);
+  __CPROVER_assert(
+    y != 34, "expected failure: paths where 0 <= x <= 15 explored");
+
+  int z = x + 20;
+  __CPROVER_assert(z != 36, "expected success: paths where x <= 15 explored");
+  return 0;
+}

src/solvers/flattening/boolbv_quantifier.cpp

@@ -50,13 +50,13 @@ get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
   }
   else if(quantifier_expr.id() == ID_and)
   {
-    /**
-     * The min variable
-     * is in the form of "var_expr >= constant".
-     */
+    // The minimum variable can be of the form `var_expr >= constant`, or
+    // it can be of the form `var_expr == constant` (e.g. in the case where
+    // the interval that bounds the variable is a singleton interval (set
+    // with only one element)).
     for(auto &x : quantifier_expr.operands())
     {
-      if(x.id()!=ID_ge)
+      if(x.id() != ID_ge && x.id() != ID_equal)
         continue;
       const auto &x_binary = to_binary_relation_expr(x);
       if(expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant())
@@ -106,24 +106,42 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
   }
   else
   {
-    /**
-     * The max variable
-     * is in the form of "!(var_expr >= constant)".
-     */
+    // There are two potential forms we could come across here. The first one
+    // is `!(var_expr >= constant)` - identified by the first if branch - and
+    // the second is `var_expr == constant` - identified by the second else-if
+    // branch. The second form could be met if previous simplification has
+    // identified a singleton interval - see simplify_boolean_expr.cpp.
     for(auto &x : quantifier_expr.operands())
     {
-      if(x.id()!=ID_not)
-        continue;
-      exprt y = to_not_expr(x).op();
-      if(y.id()!=ID_ge)
-        continue;
-      const auto &y_binary = to_binary_relation_expr(y);
-      if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
+      if(x.id() == ID_not)
       {
-        const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
-        mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
-        over_i-=1;
-        return from_integer(over_i, y_binary.rhs().type());
+        exprt y = to_not_expr(x).op();
+        if(y.id() != ID_ge)
+          continue;
+        const auto &y_binary = to_binary_relation_expr(y);
+        if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
+        {
+          const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
+          mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
+          over_i -= 1;
+          return from_integer(over_i, y_binary.rhs().type());
+        }
+      }
+      else if(x.id() == ID_equal)
+      {
+        const auto &y_binary = to_binary_relation_expr(x);
+        if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant())
+        {
+          return to_constant_expr(y_binary.rhs());
+        }
+      }
+      else
+      {
+        // If you need special handling for a particular expression type (say,
+        // after changes to the simplifier) you need to make sure that you add
+        // an `else if` branch above, otherwise the expression will get skipped
+        // and the constraints will not propagate correctly.
+        continue;
       }
     }
   }

src/util/simplify_expr_boolean.cpp

@@ -99,6 +99,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
     bool no_change = true;
     bool may_be_reducible_to_interval =
       expr.id() == ID_or && expr.operands().size() > 2;
+    bool may_be_reducible_to_singleton_interval =
+      expr.id() == ID_and && expr.operands().size() == 2;
 
     exprt::operandst new_operands = expr.operands();
 
@@ -137,6 +139,96 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
       }
     }
 
+    // NOLINTNEXTLINE(whitespace/line_length)
+    // This block reduces singleton intervals like (value >= 255 && value <= 255)
+    // to just (value == 255). We also need to be careful with the operands
+    // as some of them are erased in the previous step. We proceed only if
+    // no operands have been erased (i.e. the expression structure has been
+    // preserved by previous simplification rounds.)
+    if(may_be_reducible_to_singleton_interval && new_operands.size() == 2)
+    {
+      struct boundst
+      {
+        mp_integer lower;
+        mp_integer higher;
+      };
+      boundst bounds;
+
+      // Before we do anything else, we need to "pattern match" against the
+      // expression and make sure that it has the structure we're looking for.
+      // The structure we're looking for is going to be
+      //      (value >= 255 && !(value >= 256))   -- 255, 256 values indicative.
+      // (this is because previous simplification runs will have transformed
+      //  the less_than_or_equal expression to a not(greater_than_or_equal)
+      // expression)
+
+      // matching (value >= 255)
+      auto const match_first_operand = [&bounds](const exprt &op) -> bool {
+        if(
+          const auto ge_expr =
+            expr_try_dynamic_cast<greater_than_or_equal_exprt>(op))
+        {
+          // The construction of these expressions ensures that the RHS
+          // is constant, therefore if we don't have a constant, it's a
+          // different expression, so we bail.
+          if(!ge_expr->rhs().is_constant())
+            return false;
+          if(
+            auto int_opt =
+              numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
+          {
+            bounds.lower = *int_opt;
+            return true;
+          }
+          return false;
+        }
+        return false;
+      };
+
+      // matching !(value >= 256)
+      auto const match_second_operand = [&bounds](const exprt &op) -> bool {
+        if(const auto not_expr = expr_try_dynamic_cast<not_exprt>(op))
+        {
+          PRECONDITION(not_expr->operands().size() == 1);
+          if(
+            const auto ge_expr =
+              expr_try_dynamic_cast<greater_than_or_equal_exprt>(
+                not_expr->op()))
+          {
+            // If the rhs() is not constant, it has a different structure
+            // (e.g. i >= j)
+            if(!ge_expr->rhs().is_constant())
+              return false;
+            if(
+              auto int_opt =
+                numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
+            {
+              bounds.higher = *int_opt - 1;
+              return true;
+            }
+            return false;
+          }
+          return false;
+        }
+        return false;
+      };
+
+      // We need to match both operands, at the particular sequence we expect.
+      bool structure_matched = match_first_operand(new_operands[0]) &&
+                               match_second_operand(new_operands[1]);
+
+      if(structure_matched && bounds.lower == bounds.higher)
+      {
+        // If we are here, we have matched the structure we expected, so we can
+        // make some reasonable assumptions about where certain info we need is
+        // located at.
+        const auto ge_expr =
+          expr_dynamic_cast<greater_than_or_equal_exprt>(new_operands[0]);
+        equal_exprt new_expr{ge_expr.lhs(), ge_expr.rhs()};
+        return changed(new_expr);
+      }
+    }
+
     if(may_be_reducible_to_interval)
     {
       optionalt<symbol_exprt> symbol_opt;