Cprover enum is in range

doc/cprover-manual/api.md

@@ -125,6 +125,38 @@ stored in the given arrays are equal. The function
 the array **dest**. The function **\_\_CPROVER\_array\_set** initializes
 the array **dest** with the given value.
 
+
+#### \_\_CPROVER\_enum\_is\_in\_range
+
+```C
+__CPROVER_bool __CPROVER_enum_is_in_range();
+```
+
+The function **\_\_CPROVER\_enum\_is\_in\_range** is used to check
+that an enumeration has one of the defined enumeration values. In
+the following example `__CPROVER_enum_is_in_range(ev1)` will return
+true and the assertion will pass
+```C
+enum my_enum { first, second };
+
+int main()
+{
+  enum my_enum ev1 = second;
+  assert(__CPROVER_enum_is_in_range(ev1));
+}
+```
+However, in the example below the assertion will fail
+```C
+enum my_enum { first, second };
+
+int main()
+{
+  enum my_enum ev1 = second + 1;
+  assert(__CPROVER_enum_is_in_range(ev1));
+}
+```
+
+
 #### Uninterpreted Functions
 
 Uninterpreted functions are documented [here](./modeling-nondeterminism.md)).

regression/ansi-c/enum_is_in_range/enum_test10.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  int i = 0;
+  while(i < 10)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(i));
+    i++;
+  }
+  return 0;
+}

regression/ansi-c/enum_is_in_range/enum_test10.desc

@@ -0,0 +1,12 @@
+CORE
+enum_test10.c
+
+^EXIT=(6|70)$
+^SIGNAL=0$
+^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test the type checking of argument for __CPROVER_enum_is_in_range

regression/ansi-c/enum_is_in_range/enum_test12.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  assert(__CPROVER_enum_is_in_range(ev1, ev2));
+  return 0;
+}

regression/ansi-c/enum_is_in_range/enum_test12.desc

@@ -0,0 +1,12 @@
+CORE
+enum_test12.c
+
+^EXIT=(6|70)$
+^SIGNAL=0$
+^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test the type checking of argument for __CPROVER_enum_is_in_range

regression/cbmc/enum_is_in_range/enum_test3.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  while(ev1 != ev2)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test3.desc

@@ -0,0 +1,11 @@
+CORE
+enum_test3.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS
+--
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range
+--
+This test is for the enum_is_in_range working properly, the negation
+is if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test4.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  int i = 0;
+  while(i < 10)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+    i++;
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test4.desc

@@ -0,0 +1,13 @@
+CORE
+enum_test4.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test is for the enum_is_in_range working properly and detecting
+when the enum is not in range. The negation tests are to ensure the
+out of range is detected, and if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test5.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+enum my_enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+};
+
+void testfun(enum my_enum ee)
+{
+}
+
+int main()
+{
+  enum my_enum ev1;
+  enum my_enum ev2;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(ev1));
+  enum my_enum ev3 = ev1;
+  testfun(ev3);
+  testfun(ev2);
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test5.desc

@@ -0,0 +1,16 @@
+CORE
+enum_test5.c
+--enum-range-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main.enum-range-check.6\] line \d+ enum range check in ev3: SUCCESS$
+^\[main.enum-range-check.7\] line \d+ enum range check in ev2: FAILURE$
+--
+^\[main.enum-range-check.6\] line \d+ enum range check in ev3: FAILURE$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test is for the enum_is_in_range working in assume statements
+(and also value passing through assignments of enums). The failure
+test case is checking that range checks do work on enums.
+The negation tests are to ensure the assumption is taken into account
+for ev1 and thus ev3, and if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test7.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+typedef enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+} my_enum;
+
+int main()
+{
+  my_enum ev1;
+  my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  while(!(ev1 == ev2))
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test7.desc

@@ -0,0 +1,11 @@
+CORE
+enum_test7.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS
+--
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range
+--
+This test is for the enum_is_in_range working properly, the negation
+is if the function is not defined.

regression/cbmc/enum_is_in_range/enum_test8.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+typedef enum
+{
+  first,
+  second,
+  third,
+  fourth,
+  fifth
+} my_enum;
+
+int main()
+{
+  my_enum ev1;
+  my_enum ev2;
+  ev1 = first;
+  ev2 = fifth;
+  int i = 0;
+  while(i < 10)
+  {
+    ev1++;
+    assert(__CPROVER_enum_is_in_range(ev1));
+    i++;
+  }
+  return 0;
+}

regression/cbmc/enum_is_in_range/enum_test8.desc

@@ -0,0 +1,13 @@
+CORE
+enum_test8.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): FAILURE$
+--
+^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(ev1\): SUCCESS$
+^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
+--
+This test is for the enum_is_in_range working properly and detecting
+when the enum is not in range. The negation tests are to ensure the
+out of range is detected, and if the function is not defined.

src/ansi-c/c_typecheck_expr.cpp

@@ -2841,6 +2841,33 @@ exprt c_typecheck_baset::do_special_functions(
     overflow.type() = bool_typet{};
     return overflow;
   }
+  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
+  {
+    // Check correct number of arguments
+    if(expr.arguments().size() != 1)
+    {
+      std::ostringstream error_message;
+      error_message << expr.source_location().as_string() << ": " << identifier
+                    << " takes exactly 1 argument, but "
+                    << expr.arguments().size() << " were provided";
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+    auto arg1 = expr.arguments()[0];
+    typecheck_expr(arg1);
+    if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
+    {
+      // Can't enum range check a non-enum
+      std::ostringstream error_message;
+      error_message << expr.source_location().as_string() << ": " << identifier
+                    << " expects enum, but (" << expr2c(arg1, *this)
+                    << ") has type `" << type2c(arg1.type(), *this) << '`';
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+    else
+    {
+      return expr;
+    }
+  }
   else if(
     identifier == "__builtin_add_overflow" ||
     identifier == "__builtin_sub_overflow" ||

src/ansi-c/cprover_builtin_headers.h

@@ -103,3 +103,6 @@ __CPROVER_bool __CPROVER_overflow_mult();
 __CPROVER_bool __CPROVER_overflow_plus();
 __CPROVER_bool __CPROVER_overflow_shl();
 __CPROVER_bool __CPROVER_overflow_unary_minus();
+
+// enumerations
+__CPROVER_bool __CPROVER_enum_is_in_range();

src/goto-programs/builtin_functions.cpp

@@ -610,6 +610,32 @@ exprt make_va_list(const exprt &expr)
   return result;
 }
 
+void goto_convertt::do_enum_is_in_range(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest)
+{
+  PRECONDITION(arguments.size() == 1);
+  const auto enum_expr = arguments.front();
+  const auto enum_type =
+    type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
+  PRECONDITION(enum_type);
+  const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
+  const c_enum_typet::memberst enum_values = c_enum_type.members();
+
+  exprt::operandst disjuncts;
+  for(const auto &enum_value : enum_values)
+  {
+    constant_exprt val{enum_value.get_value(), *enum_type};
+    disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
+  }
+
+  code_assignt assignment(lhs, disjunction(disjuncts));
+  assignment.add_source_location() = function.source_location();
+  copy(assignment, ASSIGN, dest);
+}
+
 /// add function calls to function queue for later processing
 void goto_convertt::do_function_call_symbol(
   const exprt &lhs,
@@ -734,6 +760,10 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
+  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
+  {
+    do_enum_is_in_range(lhs, function, arguments, dest);
+  }
   else if(
     identifier == CPROVER_PREFIX "assert" ||
     identifier == CPROVER_PREFIX "precondition" ||