Enum range check

regression/goto-instrument/enum-range-check-disable/main.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+
+enum day
+{
+  sunday = 1,
+  monday,
+  tuesday = 5,
+  wednesday,
+  thursday = 10,
+  friday,
+  saturday
+};
+
+int main()
+{
+#pragma CPROVER check push
+#pragma CPROVER check disable "enum-range"
+  enum day temp = 100;
+  printf("%d\n", temp);
+#pragma CPROVER check pop
+  return 0;
+}

regression/goto-instrument/enum-range-check-disable/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enum-range-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/enum-range-check1/main.c

@@ -0,0 +1,26 @@
+#include <stdio.h>
+
+enum day
+{
+  sunday = 1,
+  monday,
+  tuesday = 5,
+  wednesday,
+  thursday = 10,
+  friday,
+  saturday
+};
+
+int main()
+{
+  enum day temp = friday;
+  temp = sunday;
+  temp = monday;
+  temp = tuesday;
+  temp = wednesday;
+  temp = thursday;
+  temp = thursday + 1;
+  temp = saturday;
+  printf("%d\n", temp);
+  return 0;
+}

regression/goto-instrument/enum-range-check1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enum-range-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/enum-range-check2/main.c

@@ -0,0 +1,19 @@
+#include <stdio.h>
+
+enum day
+{
+  sunday = 1,
+  monday,
+  tuesday = 5,
+  wednesday,
+  thursday = 10,
+  friday,
+  saturday
+};
+
+int main()
+{
+  enum day temp = 100;
+  printf("%d\n", temp);
+  return 0;
+}

regression/goto-instrument/enum-range-check2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--enum-range-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -47,10 +47,12 @@ class goto_checkt
     ns(_ns),
     local_bitvector_analysis(nullptr)
   {
+    no_enum_check = false;
     enable_bounds_check=_options.get_bool_option("bounds-check");
     enable_pointer_check=_options.get_bool_option("pointer-check");
     enable_memory_leak_check=_options.get_bool_option("memory-leak-check");
     enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
+    enable_enum_range_check = _options.get_bool_option("enum-range-check");
     enable_signed_overflow_check=
       _options.get_bool_option("signed-overflow-check");
     enable_unsigned_overflow_check=
@@ -90,6 +92,7 @@ class goto_checkt
   std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
   goto_programt::const_targett current_target;
   guard_managert guard_manager;
+  bool no_enum_check;
 
   /// Check an address-of expression:
   ///  if it is a dereference then check the pointer
@@ -167,6 +170,7 @@ class goto_checkt
   void div_by_zero_check(const div_exprt &, const guardt &);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void mod_overflow_check(const mod_exprt &, const guardt &);
+  void enum_range_check(const exprt &, const guardt &);
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const binary_relation_exprt &, const guardt &);
   void pointer_overflow_check(const exprt &, const guardt &);
@@ -220,6 +224,7 @@ class goto_checkt
   bool enable_pointer_check;
   bool enable_memory_leak_check;
   bool enable_div_by_zero_check;
+  bool enable_enum_range_check;
   bool enable_signed_overflow_check;
   bool enable_unsigned_overflow_check;
   bool enable_pointer_overflow_check;
@@ -325,6 +330,35 @@ void goto_checkt::div_by_zero_check(
     guard);
 }
 
+void goto_checkt::enum_range_check(const exprt &expr, const guardt &guard)
+{
+  if(!enable_enum_range_check || no_enum_check)
+    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::memberst enum_values = c_enum_type.members();
+
+  std::vector<exprt> disjuncts;
+  for(const auto &enum_value : enum_values)
+  {
+    const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
+    disjuncts.push_back(equal_exprt(expr, val));
+  }
+
+  const exprt check = disjunction(disjuncts);
+
+  add_guarded_property(
+    check,
+    "enum range check",
+    "enum-range-check",
+    expr.find_source_location(),
+    expr,
+    guard);
+}
+
 void goto_checkt::undefined_shift_check(
   const shift_exprt &expr,
   const guardt &guard)
@@ -1668,6 +1702,9 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   forall_operands(it, expr)
     check_rec(*it, guard);
 
+  if(expr.type().id() == ID_c_enum_tag)
+    enum_range_check(expr, guard);
+
   if(expr.id()==ID_index)
   {
     bounds_check(to_index_expr(expr), guard);
@@ -1806,6 +1843,8 @@ void goto_checkt::goto_check(
         flag_resetter.set_flag(enable_memory_leak_check, false);
       else if(d.first == "disable:div-by-zero-check")
         flag_resetter.set_flag(enable_div_by_zero_check, false);
+      else if(d.first == "disable:enum-range-check")
+        flag_resetter.set_flag(enable_enum_range_check, false);
       else if(d.first == "disable:signed-overflow-check")
         flag_resetter.set_flag(enable_signed_overflow_check, false);
       else if(d.first == "disable:unsigned-overflow-check")
@@ -1880,7 +1919,13 @@ void goto_checkt::goto_check(
     {
       const code_assignt &code_assign=to_code_assign(i.code);
 
-      check(code_assign.lhs());
+      // Reset the no_enum_check with the flag reset for exception
+      // safety
+      {
+        flag_resett no_enum_check_flag_resetter;
+        no_enum_check_flag_resetter.set_flag(no_enum_check, true);
+        check(code_assign.lhs());
+      }
       check(code_assign.rhs());
 
       // the LHS might invalidate any assertion

src/analyses/goto_check.h

@@ -33,10 +33,11 @@ void goto_check(
   const optionst &options,
   goto_modelt &goto_model);
 
-#define OPT_GOTO_CHECK \
-  "(bounds-check)(pointer-check)(memory-leak-check)" \
-  "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
-  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \
+#define OPT_GOTO_CHECK                                                         \
+  "(bounds-check)(pointer-check)(memory-leak-check)"                           \
+  "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-"     \
+  "overflow-check)"                                                            \
+  "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"
 
 // clang-format off
@@ -53,13 +54,15 @@ void goto_check(
   " --float-overflow-check       check floating-point for +/-Inf\n" \
   " --nan-check                  check floating-point for NaN\n" \
   " --no-built-in-assertions     ignore assertions in built-in library\n" \
+  " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
 // clang-format on
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
   options.set_option("pointer-check", cmdline.isset("pointer-check")); \
   options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
   options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
+  options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
   options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */  \

src/ansi-c/c_typecheck_base.h

@@ -228,8 +228,9 @@ class c_typecheck_baset:
   typet enum_constant_type(
     const mp_integer &min, const mp_integer &max) const;
 
-  typet enum_underlying_type(
-    const mp_integer &min, const mp_integer &max,
+  bitvector_typet enum_underlying_type(
+    const mp_integer &min,
+    const mp_integer &max,
     bool is_packed) const;
 
   // this cleans expressions in array types

src/ansi-c/c_typecheck_type.cpp

@@ -1078,7 +1078,7 @@ typet c_typecheck_baset::enum_constant_type(
   }
 }
 
-typet c_typecheck_baset::enum_underlying_type(
+bitvector_typet c_typecheck_baset::enum_underlying_type(
   const mp_integer &min_value,
   const mp_integer &max_value,
   bool is_packed) const
@@ -1216,6 +1216,8 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
     c_enum_typet::c_enum_membert member;
     member.set_identifier(identifier);
     member.set_base_name(base_name);
+    // Note: The value will be correctly set to a bv type when we know
+    // the width of the bitvector
     member.set_value(integer2string(value));
     enum_members.push_back(member);
 
@@ -1229,6 +1231,20 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
 
   bool is_packed=type.get_bool(ID_C_packed);
 
+  // We use a subtype to store the underlying type.
+  bitvector_typet underlying_type =
+    enum_underlying_type(min_value, max_value, is_packed);
+
+  // Get the width to make the values have a bitvector type
+  std::size_t width = underlying_type.get_width();
+  for(auto &member : enum_members)
+  {
+    // Note: This is inefficient as it first turns integers to strings
+    // and then turns them back to bvrep
+    auto value = string2integer(id2string(member.get_value()));
+    member.set_value(integer2bvrep(value, width));
+  }
+
   // tag?
   if(type.find(ID_tag).is_nil())
   {
@@ -1269,10 +1285,6 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
   for(const auto &member : enum_members)
     body.push_back(member);
 
-  // We use a subtype to store the underlying type.
-  typet underlying_type=
-    enum_underlying_type(min_value, max_value, is_packed);
-
   enum_tag_symbol.type.subtype()=underlying_type;
 
   // is it in the symbol table already?

src/ansi-c/scanner.l

@@ -235,9 +235,10 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 CPROVER_PREFIX  "__CPROVER_"
 
 arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
+enum_check      "enum-range"
 memory_check    ("bounds"|"pointer"|"memory_leak")
 overflow_check  ("signed"|"unsigned"|"pointer"|"float")"-overflow"
-named_check     ["]({arith_check}|{memory_check}|{overflow_check})["]
+named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check})["]
 
 %x GRAMMAR
 %x COMMENT1