Merge pull request #6594 from tautschnig/bugfixes/6586-enum-check

Do not generate enum-value checks for function call left-hand sides

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/cbmc/enum_is_in_range/format.desc

@@ -0,0 +1,10 @@
+CORE
+no_duplicate.c
+--show-goto-functions
+main::1::e = 1 ∨ main::1::e = 2 ∨ main::1::e = 4 ∨ main::1::e = 8
+^EXIT=0$
+^SIGNAL=0$
+--
+type: c_enum_tag
+--
+This test is to show that format(expr) also works for enum-typed constants.

regression/cbmc/enum_is_in_range/no_duplicate.c

@@ -0,0 +1,19 @@
+enum enm
+{
+  first = 1,
+  second = 1 << 1,
+  third = 1 << 2,
+  fourth = 1 << 3,
+};
+
+static enum enm efunc(void)
+{
+  return second;
+}
+
+int main(void)
+{
+  enum enm e = efunc();
+  __CPROVER_assert(__CPROVER_enum_is_in_range(e), "enum failure");
+  return (e);
+}

regression/cbmc/enum_is_in_range/no_duplicate.desc

@@ -0,0 +1,11 @@
+CORE
+no_duplicate.c
+--enum-range-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+line 17 enum range check in e: SUCCESS$
+--
+Test that enum range checks aren't applied to function-call left-hand sides, and
+that no extra checks are generated for uses of __CPROVER_enum_is_in_range.

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

@@ -25,6 +25,8 @@
     ['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'],
     # this one wants show-properties instead producing a trace

src/analyses/goto_check_c.cpp

@@ -517,8 +517,7 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
     return;
 
   const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
-  symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
-  const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
+  const c_enum_typet &c_enum_type = ns.follow_tag(c_enum_tag_type);
 
   const c_enum_typet::memberst enum_values = c_enum_type.members();
 
@@ -2148,7 +2147,13 @@ void goto_check_ct::goto_check(
     }
     else if(i.is_function_call())
     {
-      check(i.call_lhs());
+      // Disable enum range checks for left-hand sides as their values are yet
+      // to be set (by this function call).
+      {
+        flag_overridet resetter(i.source_location());
+        resetter.disable_flag(enable_enum_range_check, "enum_range_check");
+        check(i.call_lhs());
+      }
       check(i.call_function());
 
       for(const auto &arg : i.call_arguments())

src/goto-programs/builtin_functions.cpp

@@ -636,8 +636,9 @@ 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/format_expr.cpp

@@ -204,6 +204,10 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
                 << format(pointer_type.base_type()) << ')';
     }
   }
+  else if(type == ID_c_enum_tag)
+  {
+    return os << string2integer(id2string(src.get_value()), 16);
+  }
   else
     return os << src.pretty();
 }

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