Add an enum-in-range check.

This check can be enabled by using the flag --enum-range-check in
goto-instrument. It inserts assertions before each use of any enum
type expressions that the expression's value is one of the valid
enum values.

Note: It doesn't insert checks for occurrences of enum expressions
on the left hand side of assignments.

Author: angelhof

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);
@@ -1880,7 +1917,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
@@ -60,6 +61,7 @@ void goto_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/goto-instrument/goto_instrument_parse_options.cpp

@@ -1624,6 +1624,7 @@ void goto_instrument_parse_optionst::help()
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
     HELP_GOTO_CHECK
+    " --enum-range-check           checks that all enum type expressions have values in the enum range\n" // NOLINT(*)
     " --uninitialized-check        add checks for uninitialized locals (experimental)\n" // NOLINT(*)
     " --error-label label          check that label is unreachable\n"
     " --stack-depth n              add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)