Simplify disjunctions over equalities to intervals

Disjunctions over equalities of integer constants can be rewritten as
closed intervals. This will most commonly appear when expanding
enum_is_in_range.

This also surfaced a bug in to_integer, which used the wrong type
reference.

Author: tautschnig

regression/cbmc/enum_is_in_range/enum_test3-simplified.desc

@@ -0,0 +1,10 @@
+CORE
+enum_test3.c
+--show-goto-functions
+0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4$
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::ev1 = 0
+--
+This test is to demonstrate simplification of enumerated ranges of integers.

regression/validate-trace-xml-schema/check.py

@@ -25,6 +25,7 @@
     ['integer-assignments1', 'integer-typecheck.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
+    ['enum_is_in_range', 'enum_test3-simplified.desc'],
     ['enum_is_in_range', 'format.desc'],
     ['r_w_ok9', 'simplify.desc'],
     ['reachability-slice-interproc2', 'test.desc'],

src/goto-programs/builtin_functions.cpp

@@ -636,7 +636,7 @@ void goto_convertt::do_enum_is_in_range(
     disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
   }
 
-  code_assignt assignment(lhs, disjunction(disjuncts));
+  code_assignt assignment(lhs, simplify_expr(disjunction(disjuncts), ns));
   assignment.add_source_location() = function.source_location();
   assignment.add_source_location().add_pragma("disable:enum-range-check");
   copy(assignment, ASSIGN, dest);

src/util/arith_tools.cpp

@@ -59,13 +59,13 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
     const typet &underlying_type = to_c_enum_type(type).underlying_type();
     if(underlying_type.id() == ID_signedbv)
     {
-      const auto width = to_signedbv_type(type).get_width();
+      const auto width = to_signedbv_type(underlying_type).get_width();
       int_value = bvrep2integer(value, width, true);
       return false;
     }
     else if(underlying_type.id() == ID_unsignedbv)
     {
-      const auto width = to_unsignedbv_type(type).get_width();
+      const auto width = to_unsignedbv_type(underlying_type).get_width();
       int_value = bvrep2integer(value, width, false);
       return false;
     }

src/util/simplify_expr_boolean.cpp

@@ -8,12 +8,15 @@ Author: Daniel Kroening, [email protected]
 
 #include "simplify_expr_class.h"
 
-#include <unordered_set>
-
+#include "arith_tools.h"
+#include "c_types.h"
 #include "expr_util.h"
 #include "mathematical_expr.h"
+#include "namespace.h"
 #include "std_expr.h"
 
+#include <unordered_set>
+
 simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
 {
   if(!expr.has_operands())
@@ -96,6 +99,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
     std::unordered_set<exprt, irep_hash> expr_set;
 
     bool no_change = true;
+    bool may_be_reducible_to_interval =
+      expr.id() == ID_or && expr.operands().size() > 2;
 
     exprt::operandst new_operands = expr.operands();
 
@@ -127,7 +132,70 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
         no_change = false;
       }
       else
+      {
+        if(may_be_reducible_to_interval)
+          may_be_reducible_to_interval = it->id() == ID_equal;
         it++;
+      }
+    }
+
+    if(may_be_reducible_to_interval)
+    {
+      optionalt<symbol_exprt> symbol_opt;
+      std::set<mp_integer> values;
+      for(const exprt &op : new_operands)
+      {
+        equal_exprt eq = to_equal_expr(op);
+        if(eq.lhs().is_constant())
+          std::swap(eq.lhs(), eq.rhs());
+        if(auto s = expr_try_dynamic_cast<symbol_exprt>(eq.lhs()))
+        {
+          if(!symbol_opt.has_value())
+            symbol_opt = *s;
+
+          if(*s == *symbol_opt)
+          {
+            if(auto c = expr_try_dynamic_cast<constant_exprt>(eq.rhs()))
+            {
+              constant_exprt c_tmp = *c;
+              if(c_tmp.type().id() == ID_c_enum_tag)
+                c_tmp.type() = ns.follow_tag(to_c_enum_tag_type(c_tmp.type()));
+              if(auto int_opt = numeric_cast<mp_integer>(c_tmp))
+              {
+                values.insert(*int_opt);
+                continue;
+              }
+            }
+          }
+        }
+
+        symbol_opt.reset();
+        break;
+      }
+
+      if(symbol_opt.has_value() && values.size() >= 3)
+      {
+        mp_integer lower = *values.begin();
+        mp_integer upper = *std::prev(values.end());
+        if(upper - lower + 1 == mp_integer{values.size()})
+        {
+          typet type = symbol_opt->type();
+          if(symbol_opt->type().id() == ID_c_enum_tag)
+          {
+            type = ns.follow_tag(to_c_enum_tag_type(symbol_opt->type()))
+                     .underlying_type();
+          }
+
+          less_than_or_equal_exprt lb{
+            from_integer(lower, type),
+            typecast_exprt::conditional_cast(*symbol_opt, type)};
+          less_than_or_equal_exprt ub{
+            typecast_exprt::conditional_cast(*symbol_opt, type),
+            from_integer(upper, type)};
+
+          return and_exprt{lb, ub};
+        }
+      }
     }
 
     // search for a and !a