Implement enum_is_in_range builtin function

This adds a new builtin function that allows user to
explicitly check that an enum has a valid value (and also
this function in an assert).

Author: TGWDB

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" ||

src/goto-programs/goto_convert_class.h

@@ -588,6 +588,26 @@ class goto_convertt:public messaget
   bool get_string_constant(const exprt &expr, irep_idt &);
   exprt get_constant(const exprt &expr);
 
+  /// \brief Converts calls to the built in `enum_is_in_range` function to a
+  ///    test that the given enum value is in the valid range of values for that
+  ///    enum type.
+  ///
+  /// Note that the check for the range of values is done by creating a
+  /// disjunction comparing the expression with each possible valid value.
+  /// \param lhs: The destination for the generated assignment.
+  /// \param function: The `enum_is_in_range` symbol of the source function call.
+  /// \param arguments: A collection of arguments, which is expected to contain a
+  ///    single argument which is an expression that resolves to a value of
+  ///    enum type. The arguments are expected to have been prevalidated by the
+  ///    typechecking process.
+  /// \param dest: The goto program into which the generated assignment is
+  ///    copied.
+  void do_enum_is_in_range(
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments,
+    goto_programt &dest);
+
   // some built-in functions
   void do_atomic_begin(
     const exprt &lhs,