introduce __CPROVER_separate

This introduces C syntax for a multi-ary predicate that implies that the
given pointers point to pairwise different objects.

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2538,6 +2538,23 @@ exprt c_typecheck_baset::do_special_functions(
 
     return writeable_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "separate")
+  {
+    // experimental feature for CHC encodings -- do not use
+    if(expr.arguments().size() < 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << "separate expects two or more arguments" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt separate_expr = separate_exprt(expr.arguments());
+    separate_expr.add_source_location() = source_location;
+
+    return separate_expr;
+  }
   else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -23,6 +23,7 @@ __CPROVER_bool __CPROVER_is_cyclic_dll();
 __CPROVER_bool __CPROVER_is_sentinel_dll();
 __CPROVER_bool __CPROVER_is_cstring(const char *);
 __CPROVER_size_t __CPROVER_cstrlen(const char *);
+__CPROVER_bool __CPROVER_separate(const void *, const void *, ...);
 
 // bitvector analysis
 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);

src/ansi-c/expr2c.cpp

@@ -3988,6 +3988,7 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_live_object, "LIVE_OBJECT"},
     {ID_writeable_object, "WRITEABLE_OBJECT"},
     {ID_find_first_set, "__builtin_ffs"},
+    {ID_separate, "SEPARATE"},
     {ID_floatbv_div, "FLOAT/"},
     {ID_floatbv_minus, "FLOAT-"},
     {ID_floatbv_mult, "FLOAT*"},

src/util/irep_ids.def

@@ -457,6 +457,7 @@ IREP_ID_ONE(is_dynamic_object)
 IREP_ID_ONE(dynamic_object)
 IREP_ID_TWO(C_dynamic, #dynamic)
 IREP_ID_ONE(object_size)
+IREP_ID_ONE(separate)
 IREP_ID_ONE(good_pointer)
 IREP_ID_ONE(live_object)
 IREP_ID_ONE(writeable_object)

src/util/pointer_expr.h

@@ -1287,4 +1287,56 @@ inline writeable_object_exprt &to_writeable_object_expr(exprt &expr)
   return ret;
 }
 
+/// A predicate that indicates that the objects pointed to are distinct
+class separate_exprt : public multi_ary_exprt
+{
+public:
+  explicit separate_exprt(exprt::operandst __operands)
+    : multi_ary_exprt(ID_separate, std::move(__operands), bool_typet())
+  {
+  }
+
+  separate_exprt(exprt __op0, exprt __op1)
+    : multi_ary_exprt(
+        std::move(__op0),
+        ID_separate,
+        std::move(__op1),
+        bool_typet())
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<separate_exprt>(const exprt &base)
+{
+  return base.id() == ID_separate;
+}
+
+inline void validate_expr(const separate_exprt &value)
+{
+}
+
+/// \brief Cast an exprt to a \ref separate_exprt
+///
+/// \a expr must be known to be \ref separate_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref separate_exprt
+inline const separate_exprt &to_separate_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_separate);
+  const separate_exprt &ret = static_cast<const separate_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_separate_expr(const exprt &)
+inline separate_exprt &to_separate_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_separate);
+  separate_exprt &ret = static_cast<separate_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H