Introduce enum_is_in_range expression

We previously maintained a function call, which would end up being type
in-consistent if there were multiple uses of
`__CPROVER_enum_is_in_range` with distinct enum types. Instead, have the
C front-end create an (and immediately lower) an expression. The only
bit of care that's currently required is to ensure that goto_check_ct
does not end up creating assertions over the resulting expression.

Author: tautschnig

regression/cbmc/enum_is_in_range/enum_test3-simplified.desc

@@ -1,7 +1,7 @@
 CORE new-smt-backend
 enum_test3.c
 --show-goto-functions
-0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4$
+0 ≤ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ∧ cast\(main::1::ev1, (un)?signedbv\[\d+\]\) ≤ 4
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/ansi-c/c_expr.cpp

@@ -9,6 +9,9 @@ Author: Daniel Kroening, [email protected]
 #include "c_expr.h"
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/namespace.h>
+#include <util/simplify_expr.h>
 
 shuffle_vector_exprt::shuffle_vector_exprt(
   exprt vector1,
@@ -64,3 +67,19 @@ vector_exprt shuffle_vector_exprt::lower() const
 
   return vector_exprt{std::move(operands), type()};
 }
+
+exprt enum_is_in_range_exprt::lower(const namespacet &ns) const
+{
+  const auto &enum_type = to_c_enum_tag_type(op().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(op(), std::move(val)));
+  }
+
+  return simplify_expr(disjunction(disjuncts), ns);
+}

src/ansi-c/c_expr.h

@@ -320,4 +320,54 @@ to_conditional_target_group_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A Boolean expression returning true, iff the value of an enum-typed
+/// symbol equals one of the enum's declared values.
+class enum_is_in_range_exprt : public unary_predicate_exprt
+{
+public:
+  explicit enum_is_in_range_exprt(exprt _op)
+    : unary_predicate_exprt(ID_enum_is_in_range, std::move(_op))
+  {
+    op().add_source_location().add_pragma("disable:enum-range-check");
+  }
+
+  exprt lower(const namespacet &ns) const;
+};
+
+template <>
+inline bool can_cast_expr<enum_is_in_range_exprt>(const exprt &base)
+{
+  return base.id() == ID_enum_is_in_range;
+}
+
+inline void validate_expr(const enum_is_in_range_exprt &expr)
+{
+  validate_operands(
+    expr, 1, "enum_is_in_range expression must have one operand");
+}
+
+/// \brief Cast an exprt to an \ref enum_is_in_range_exprt
+///
+/// \a expr must be known to be \ref enum_is_in_range_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref enum_is_in_range_exprt
+inline const enum_is_in_range_exprt &to_enum_is_in_range_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_enum_is_in_range);
+  const enum_is_in_range_exprt &ret =
+    static_cast<const enum_is_in_range_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_side_effect_expr_overflow(const exprt &)
+inline enum_is_in_range_exprt &to_enum_is_in_range_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_enum_is_in_range);
+  enum_is_in_range_exprt &ret = static_cast<enum_is_in_range_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_expr.cpp

@@ -2118,6 +2118,35 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
         return;
       }
+      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 << identifier << " takes exactly 1 argument, but "
+                        << expr.arguments().size() << " were provided";
+          throw invalid_source_file_exceptiont{
+            error_message.str(), expr.source_location()};
+        }
+        const auto &arg1 = expr.arguments()[0];
+        if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
+        {
+          // Can't enum range check a non-enum
+          std::ostringstream error_message;
+          error_message << identifier << " expects enum, but ("
+                        << expr2c(arg1, *this) << ") has type `"
+                        << type2c(arg1.type(), *this) << '`';
+          throw invalid_source_file_exceptiont{
+            error_message.str(), expr.source_location()};
+        }
+
+        enum_is_in_range_exprt in_range{arg1};
+        in_range.add_source_location() = expr.source_location();
+        exprt lowered = in_range.lower(*this);
+        expr.swap(lowered);
+        return;
+      }
       else if(
         auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
           identifier, expr.arguments(), f_op.source_location()))
@@ -3579,34 +3608,6 @@ exprt c_typecheck_baset::do_special_functions(
     overflow.add_source_location() = tmp.source_location();
     return std::move(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 << identifier << " takes exactly 1 argument, but "
-                    << expr.arguments().size() << " were provided";
-      throw invalid_source_file_exceptiont{
-        error_message.str(), expr.source_location()};
-    }
-    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 << identifier << " expects enum, but ("
-                    << expr2c(arg1, *this) << ") has type `"
-                    << type2c(arg1.type(), *this) << '`';
-      throw invalid_source_file_exceptiont{
-        error_message.str(), expr.source_location()};
-    }
-    else
-    {
-      return expr;
-    }
-  }
   else if(
     identifier == "__builtin_add_overflow" ||
     identifier == "__builtin_sadd_overflow" ||

src/ansi-c/cprover_builtin_headers.h

@@ -137,9 +137,6 @@ __CPROVER_bool __CPROVER_overflow_plus();
 __CPROVER_bool __CPROVER_overflow_shl();
 __CPROVER_bool __CPROVER_overflow_unary_minus();
 
-// enumerations
-__CPROVER_bool __CPROVER_enum_is_in_range();
-
 // contracts
 void __CPROVER_assignable(void *ptr, __CPROVER_size_t size,
   __CPROVER_bool is_ptr_to_ptr);

src/ansi-c/goto_check_c.cpp

@@ -41,6 +41,8 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include "c_expr.h"
+
 #include <algorithm>
 
 class goto_check_ct
@@ -523,19 +525,15 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
   if(!enable_enum_range_check)
     return;
 
-  const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.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();
-
-  std::vector<exprt> disjuncts;
-  for(const auto &enum_value : enum_values)
+  // we might be looking at a lowered enum_is_in_range_exprt, skip over these
+  const auto &pragmas = expr.source_location().get_pragmas();
+  for(const auto &d : pragmas)
   {
-    const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
-    disjuncts.push_back(equal_exprt(expr, val));
+    if(d.first == "disable:enum-range-check")
+      return;
   }
 
-  const exprt check = disjunction(disjuncts);
+  const exprt check = enum_is_in_range_exprt{expr}.lower(ns);
 
   add_guarded_property(
     check,

src/ansi-c/library/cprover.h

@@ -40,6 +40,10 @@ struct __CPROVER_pipet {
   short next_unread;
 };
 
+// enumerations
+// expects one enum-typed argument
+__CPROVER_bool __CPROVER_enum_is_in_range(unsigned long long);
+
 #include "../cprover_builtin_headers.h"
 
 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H

src/goto-programs/builtin_functions.cpp

@@ -615,33 +615,6 @@ 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, 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);
-}
-
 void goto_convertt::do_havoc_slice(
   const exprt &lhs,
   const symbol_exprt &function,
@@ -956,10 +929,6 @@ 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

@@ -610,26 +610,6 @@ 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,

src/util/irep_ids.def

@@ -903,6 +903,7 @@ IREP_ID_TWO(overflow_result_shl, overflow_result-shl)
 IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-)
 IREP_ID_ONE(field_sensitive_ssa)
 IREP_ID_ONE(checked_assigns)
+IREP_ID_ONE(enum_is_in_range)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree