r/w/rw_ok and pointer_in_range depend on deallocated and dead_object

The evaluation of these expressions depends on the specific values of
__CPROVER_deallocated and __CPROVER_dead_object at the time the
expression is used. Therefore, include these as additional operands to
retain the properties expected of an expression (as opposed to a
statement/function call).

Author: tautschnig

src/ansi-c/goto_check_c.cpp

@@ -2013,7 +2013,7 @@ optionalt<exprt> goto_check_ct::expand_pointer_checks(exprt expr)
   {
     // these get an address as first argument and a size as second
     DATA_INVARIANT(
-      expr.operands().size() == 2, "r/w_ok must have two operands");
+      expr.operands().size() == 4, "r/w_ok must have four operands");
 
     const auto conditions = get_pointer_dereferenceable_conditions(
       to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size());

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -635,9 +635,13 @@ exprt instrument_spec_assignst::target_validity_expr(
   // (or is NULL if we allow it explicitly).
   // This assertion will be falsified whenever `start_address` is invalid or
   // not of the right size (or is NULL if we do not allow it explicitly).
-  auto result =
-    or_exprt{not_exprt{car.condition()},
-             w_ok_exprt{car.target_start_address(), car.target_size()}};
+  symbol_exprt deallocated =
+    ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+  symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+  auto result = or_exprt{
+    not_exprt{car.condition()},
+    w_ok_exprt{
+      car.target_start_address(), car.target_size(), deallocated, dead}};
 
   if(allow_null_target)
     result.add_to_operands(null_object(car.target_start_address()));

src/goto-instrument/contracts/utils.cpp

@@ -91,7 +91,11 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
     const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
     CHECK_RETURN(size_of_expr_opt.has_value());
 
-    validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
+    symbol_exprt deallocated =
+      ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+    symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+    validity_checks.push_back(
+      r_ok_exprt{deref->pointer(), *size_of_expr_opt, deallocated, dead});
   }
 
   for(const auto &op : expr.operands())

src/goto-programs/builtin_functions.cpp

@@ -696,7 +696,10 @@ void goto_convertt::do_havoc_slice(
   // char nondet_contents[argument[1]];
   // __CPROVER_array_replace(p, nondet_contents);
 
-  r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
+  symbol_exprt deallocated =
+    ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+  symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+  w_ok_exprt ok_expr{arguments[0], arguments[1], deallocated, dead};
   ok_expr.add_source_location() = source_location;
   source_locationt annotated_location = source_location;
   annotated_location.set("user-provided", false);

src/goto-programs/goto_clean_expr.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_convert_class.h"
 
+#include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/pointer_expr.h>
@@ -73,6 +74,22 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
     return true;
   }
 
+  if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(expr))
+  {
+    if(r_or_w_ok->deallocated_ptr().is_nil())
+      return true;
+    if(r_or_w_ok->dead_ptr().is_nil())
+      return true;
+  }
+  else if(
+    auto pointer_in_range = expr_try_dynamic_cast<pointer_in_range_exprt>(expr))
+  {
+    if(pointer_in_range->deallocated_ptr().is_nil())
+      return true;
+    if(pointer_in_range->dead_ptr().is_nil())
+      return true;
+  }
+
   // We can't flatten quantified expressions by introducing new literals for
   // conditional expressions.  This is because the body of the quantified
   // may refer to bound variables, which are not visible outside the scope
@@ -436,6 +453,33 @@ void goto_convertt::clean_expr(
       expr.operands().size() == 1, "ID_compound_literal has a single operand");
     expr = to_unary_expr(expr).op();
   }
+  else if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(expr))
+  {
+    if(r_or_w_ok->deallocated_ptr().is_nil())
+    {
+      r_or_w_ok->deallocated_ptr() =
+        ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+    }
+    if(r_or_w_ok->dead_ptr().is_nil())
+    {
+      r_or_w_ok->dead_ptr() =
+        ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+    }
+  }
+  else if(
+    auto pointer_in_range = expr_try_dynamic_cast<pointer_in_range_exprt>(expr))
+  {
+    if(pointer_in_range->deallocated_ptr().is_nil())
+    {
+      pointer_in_range->deallocated_ptr() =
+        ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+    }
+    if(pointer_in_range->dead_ptr().is_nil())
+    {
+      pointer_in_range->dead_ptr() =
+        ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+    }
+  }
 }
 
 void goto_convertt::clean_expr_address_of(

src/util/pointer_expr.cpp

@@ -233,7 +233,10 @@ exprt pointer_in_range_exprt::lower() const
     {same_object(op0(), op1()),
      same_object(op1(), op2()),
      r_ok_exprt(
-       op0(), minus_exprt(pointer_offset(op2()), pointer_offset(op0()))),
+       op0(),
+       minus_exprt(pointer_offset(op2()), pointer_offset(op0())),
+       deallocated_ptr(),
+       dead_ptr()),
      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

@@ -369,22 +369,39 @@ inline is_dynamic_object_exprt &to_is_dynamic_object_expr(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
+class pointer_in_range_exprt : public expr_protectedt
 {
 public:
-  explicit pointer_in_range_exprt(exprt a, exprt b, exprt c)
-    : ternary_exprt(
+  pointer_in_range_exprt(
+    exprt a,
+    exprt b,
+    exprt c,
+    exprt is_deallocated,
+    exprt is_dead)
+    : expr_protectedt(
         ID_pointer_in_range,
-        std::move(a),
-        std::move(b),
-        std::move(c),
-        bool_typet())
+        bool_typet{},
+        {std::move(a),
+         std::move(b),
+         std::move(c),
+         std::move(is_deallocated),
+         std::move(is_dead)})
   {
     PRECONDITION(op0().type().id() == ID_pointer);
     PRECONDITION(op1().type().id() == ID_pointer);
     PRECONDITION(op2().type().id() == ID_pointer);
   }
 
+  pointer_in_range_exprt(exprt a, exprt b, exprt c)
+    : pointer_in_range_exprt(
+        std::move(a),
+        std::move(b),
+        std::move(c),
+        nil_exprt{},
+        nil_exprt{})
+  {
+  }
+
   const exprt &lower_bound() const
   {
     return op0();
@@ -400,6 +417,26 @@ class pointer_in_range_exprt : public ternary_exprt
     return op2();
   }
 
+  const exprt &deallocated_ptr() const
+  {
+    return op3();
+  }
+
+  exprt &deallocated_ptr()
+  {
+    return op3();
+  }
+
+  const exprt &dead_ptr() const
+  {
+    return operands()[4];
+  }
+
+  exprt &dead_ptr()
+  {
+    return operands()[4];
+  }
+
   // translate into equivalent conjunction
   exprt lower() const;
 };
@@ -412,14 +449,14 @@ inline bool can_cast_expr<pointer_in_range_exprt>(const exprt &base)
 
 inline void validate_expr(const pointer_in_range_exprt &value)
 {
-  validate_operands(value, 3, "pointer_in_range must have three operands");
+  validate_operands(value, 5, "pointer_in_range must have five 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");
+    expr.operands().size() == 5, "pointer_in_range must have five operands");
   return static_cast<const pointer_in_range_exprt &>(expr);
 }
 
@@ -429,7 +466,7 @@ 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 three operands");
+    expr.operands().size() == 5, "pointer_in_range must have five operands");
   return static_cast<pointer_in_range_exprt &>(expr);
 }
 
@@ -814,11 +851,32 @@ class null_pointer_exprt : public constant_exprt
 
 /// \brief A base class for a predicate that indicates that an
 /// address range is ok to read or write or both
-class r_or_w_ok_exprt : public binary_predicate_exprt
+class r_or_w_ok_exprt : public expr_protectedt
 {
 public:
-  explicit r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
-    : binary_predicate_exprt(std::move(pointer), id, std::move(size))
+  r_or_w_ok_exprt(
+    irep_idt id,
+    exprt pointer,
+    exprt size,
+    exprt is_deallocated,
+    exprt is_dead)
+    : expr_protectedt(
+        id,
+        bool_typet{},
+        {std::move(pointer),
+         std::move(size),
+         std::move(is_deallocated),
+         std::move(is_dead)})
+  {
+  }
+
+  r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
+    : r_or_w_ok_exprt(
+        id,
+        std::move(pointer),
+        std::move(size),
+        nil_exprt{},
+        nil_exprt{})
   {
   }
 
@@ -831,6 +889,26 @@ class r_or_w_ok_exprt : public binary_predicate_exprt
   {
     return op1();
   }
+
+  const exprt &deallocated_ptr() const
+  {
+    return op2();
+  }
+
+  exprt &deallocated_ptr()
+  {
+    return op2();
+  }
+
+  const exprt &dead_ptr() const
+  {
+    return op3();
+  }
+
+  exprt &dead_ptr()
+  {
+    return op3();
+  }
 };
 
 template <>
@@ -841,7 +919,7 @@ inline bool can_cast_expr<r_or_w_ok_exprt>(const exprt &base)
 
 inline void validate_expr(const r_or_w_ok_exprt &value)
 {
-  validate_operands(value, 2, "r_or_w_ok must have two operands");
+  validate_operands(value, 4, "r_or_w_ok must have four operands");
 }
 
 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
@@ -857,8 +935,18 @@ inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
 class r_ok_exprt : public r_or_w_ok_exprt
 {
 public:
-  explicit r_ok_exprt(exprt pointer, exprt size)
-    : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
+  r_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
+    : r_or_w_ok_exprt(
+        ID_r_ok,
+        std::move(pointer),
+        std::move(size),
+        std::move(is_deallocated),
+        std::move(is_dead))
+  {
+  }
+
+  r_ok_exprt(exprt pointer, exprt size)
+    : r_ok_exprt(std::move(pointer), std::move(size), nil_exprt{}, nil_exprt{})
   {
   }
 };
@@ -871,7 +959,7 @@ inline bool can_cast_expr<r_ok_exprt>(const exprt &base)
 
 inline void validate_expr(const r_ok_exprt &value)
 {
-  validate_operands(value, 2, "r_ok must have two operands");
+  validate_operands(value, 4, "r_ok must have four operands");
 }
 
 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
@@ -886,8 +974,18 @@ inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
 class w_ok_exprt : public r_or_w_ok_exprt
 {
 public:
-  explicit w_ok_exprt(exprt pointer, exprt size)
-    : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
+  w_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
+    : r_or_w_ok_exprt(
+        ID_w_ok,
+        std::move(pointer),
+        std::move(size),
+        std::move(is_deallocated),
+        std::move(is_dead))
+  {
+  }
+
+  w_ok_exprt(exprt pointer, exprt size)
+    : w_ok_exprt(std::move(pointer), std::move(size), nil_exprt{}, nil_exprt{})
   {
   }
 };
@@ -900,7 +998,7 @@ inline bool can_cast_expr<w_ok_exprt>(const exprt &base)
 
 inline void validate_expr(const w_ok_exprt &value)
 {
-  validate_operands(value, 2, "w_ok must have two operands");
+  validate_operands(value, 4, "w_ok must have four operands");
 }
 
 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)