introduce pointer_in_range predicate

This adds the predicate __CPROVER_pointer_in_range to the C frontend.  The
expression __CPROVER_pointer_in_range(a, b, c) evaluates to true iff the
following conditions are met:

1) The three pointers a, b, c point to the same object.

2) The object is readable from a to (but not including) c, i.e., c may point
just beyond the end of the sequence.

3) a <= b

4) b <= c

This predicate is an invariant for the standard loop pattern in which a
pointer is used to iterate over an object, stopping when the pointer points
one beyond the end of the sequence.

The benefit over using a<=b && b<=c is that ANSI-C's <= operator is
undefined when the two pointers related by <= do not point into the same
object.

Author: kroening

regression/cbmc/pointer-predicates/in_range1.c

@@ -0,0 +1,13 @@
+int x;
+
+int main()
+{
+  __CPROVER_assert(__CPROVER_pointer_in_range(&x, &x, &x), "property 1");
+  __CPROVER_assert(__CPROVER_pointer_in_range(&x, &x, &x + 1), "property 2");
+  __CPROVER_assert(
+    __CPROVER_pointer_in_range(&x, &x + 1, &x + 1), "property 3");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(&x, &x + 1, &x), "property 4");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(0, &x, &x), "property 5");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(&x, 0, &x), "property 6");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(&x, &x, 0), "property 7");
+}

regression/cbmc/pointer-predicates/in_range1.desc

@@ -0,0 +1,8 @@
+CORE
+in_range1.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

src/ansi-c/c_typecheck_expr.cpp

@@ -2522,6 +2522,24 @@ exprt c_typecheck_baset::do_special_functions(
 
     return live_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "pointer_in_range")
+  {
+    // experimental feature for CHC encodings -- do not use
+    if(expr.arguments().size() != 3)
+    {
+      error().source_location = f_op.source_location();
+      error() << "pointer_in_range expects three arguments" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt pointer_in_range_expr = pointer_in_range_exprt(
+      expr.arguments()[0], expr.arguments()[1], expr.arguments()[2]);
+    pointer_in_range_expr.add_source_location() = source_location;
+
+    return pointer_in_range_expr;
+  }
   else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
   {
     if(expr.arguments().size() != 1)

src/ansi-c/cprover_builtin_headers.h

@@ -57,6 +57,7 @@ __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
+__CPROVER_bool __CPROVER_pointer_in_range(const void *, const void *, const void *);
 void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
 
 // float stuff

src/ansi-c/goto_check_c.cpp

@@ -224,7 +224,7 @@ class goto_check_ct
   void conversion_check(const exprt &, const guardt &);
   void float_overflow_check(const exprt &, const guardt &);
   void nan_check(const exprt &, const guardt &);
-  optionalt<exprt> rw_ok_check(exprt);
+  optionalt<exprt> expand_pointer_checks(exprt);
 
   std::string array_name(const exprt &);
 
@@ -1992,14 +1992,14 @@ void goto_check_ct::check(const exprt &expr)
   check_rec(expr, identity);
 }
 
-/// expand the r_ok, w_ok and rw_ok predicates
-optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
+/// expand the r_ok, w_ok, rw_ok, pointer_in_range predicates
+optionalt<exprt> goto_check_ct::expand_pointer_checks(exprt expr)
 {
   bool modified = false;
 
   for(auto &op : expr.operands())
   {
-    auto op_result = rw_ok_check(op);
+    auto op_result = expand_pointer_checks(op);
     if(op_result.has_value())
     {
       op = *op_result;
@@ -2026,6 +2026,22 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
       simplify(c, ns);
     return c;
   }
+  else if(expr.id() == ID_pointer_in_range)
+  {
+    const auto &pointer_in_range_expr = to_pointer_in_range_expr(expr);
+
+    auto expanded = pointer_in_range_expr.lower();
+
+    // rec. call
+    auto expanded_rec_opt = expand_pointer_checks(expanded);
+    if(expanded_rec_opt.has_value())
+      expanded = *expanded_rec_opt;
+
+    if(enable_simplify)
+      simplify(expanded, ns);
+
+    return expanded;
+  }
   else if(modified)
     return std::move(expr);
   else
@@ -2228,7 +2244,7 @@ void goto_check_ct::goto_check(
       }
     }
 
-    i.transform([this](exprt expr) { return rw_ok_check(expr); });
+    i.transform([this](exprt expr) { return expand_pointer_checks(expr); });
 
     for(auto &instruction : new_code.instructions)
     {

src/util/irep_ids.def

@@ -456,6 +456,7 @@ IREP_ID_ONE(object_descriptor)
 IREP_ID_ONE(is_dynamic_object)
 IREP_ID_ONE(dynamic_object)
 IREP_ID_TWO(C_dynamic, #dynamic)
+IREP_ID_ONE(pointer_in_range)
 IREP_ID_ONE(object_size)
 IREP_ID_ONE(separate)
 IREP_ID_ONE(good_pointer)

src/util/pointer_expr.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include "c_types.h"
 #include "expr_util.h"
 #include "pointer_offset_size.h"
+#include "pointer_predicates.h"
 #include "simplify_expr.h"
 
 void dynamic_object_exprt::set_instance(unsigned int instance)
@@ -214,3 +215,15 @@ void dereference_exprt::validate(
     "dereference expression's type must match the base type of the type of its "
     "operand");
 }
+
+exprt pointer_in_range_exprt::lower() const
+{
+  return and_exprt(
+    {same_object(op0(), op1()),
+     same_object(op1(), op2()),
+     r_ok_exprt(
+       op0(), minus_exprt(pointer_offset(op2()), pointer_offset(op0()))),
+     binary_relation_exprt(pointer_offset(op0()), ID_le, pointer_offset(op1())),
+     binary_relation_exprt(
+       pointer_offset(op1()), ID_le, pointer_offset(op2()))});
+}

src/util/pointer_expr.h

@@ -366,6 +366,58 @@ inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr)
   return static_cast<is_dynamic_object_exprt &>(expr);
 }
 
+/// pointer_in_range(a, b, c) evaluates to true iff
+/// same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧ a<=b ∧ b<=c
+/// Note that the last inequality is weak, i.e., b may be equal to c.
+class pointer_in_range_exprt : public ternary_exprt
+{
+public:
+  explicit pointer_in_range_exprt(exprt a, exprt b, exprt c)
+    : ternary_exprt(
+        ID_pointer_in_range,
+        std::move(a),
+        std::move(b),
+        std::move(c),
+        bool_typet())
+  {
+    PRECONDITION(op0().type().id() == ID_pointer);
+    PRECONDITION(op1().type().id() == ID_pointer);
+    PRECONDITION(op2().type().id() == ID_pointer);
+  }
+
+  // translate into equivalent conjunction
+  exprt lower() const;
+};
+
+template <>
+inline bool can_cast_expr<pointer_in_range_exprt>(const exprt &base)
+{
+  return base.id() == ID_pointer_in_range;
+}
+
+inline void validate_expr(const pointer_in_range_exprt &value)
+{
+  validate_operands(value, 3, "pointer_in_range must have three operands");
+}
+
+inline const pointer_in_range_exprt &to_pointer_in_range_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_pointer_in_range);
+  DATA_INVARIANT(
+    expr.operands().size() == 3, "pointer_in_range must have three operands");
+  return static_cast<const pointer_in_range_exprt &>(expr);
+}
+
+/// \copydoc to_pointer_in_range_expr(const exprt &)
+/// \ingroup gr_std_expr
+inline pointer_in_range_exprt &to_pointer_in_range_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_pointer_in_range);
+  DATA_INVARIANT(
+    expr.operands().size() == 3, "pointer_in_range must have one operand");
+  return static_cast<pointer_in_range_exprt &>(expr);
+}
+
 /// \brief Operator to return the address of an object
 class address_of_exprt : public unary_exprt
 {