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/c_typecheck_expr.cpp

@@ -2683,8 +2683,15 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
+    symbol_exprt deallocated =
+      lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+    symbol_exprt dead = lookup(CPROVER_PREFIX "dead_object").symbol_expr();
     exprt pointer_in_range_expr = pointer_in_range_exprt(
-      expr.arguments()[0], expr.arguments()[1], expr.arguments()[2]);
+      expr.arguments()[0],
+      expr.arguments()[1],
+      expr.arguments()[2],
+      deallocated,
+      dead);
     pointer_in_range_expr.add_source_location() = source_location;
 
     return pointer_in_range_expr;
@@ -3103,7 +3110,10 @@ exprt c_typecheck_baset::do_special_functions(
                     ? ID_r_ok
                     : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok : ID_rw_ok;
 
-    r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
+    symbol_exprt deallocated =
+      lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+    symbol_exprt dead = lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+    r_or_w_ok_exprt ok_expr{id, pointer_expr, size_expr, deallocated, dead};
     ok_expr.add_source_location() = source_location;
 
     return std::move(ok_expr);

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/cprover/c_safety_checks.cpp

@@ -147,8 +147,16 @@ void c_safety_checks_rec(
       {
         auto size = from_integer(*size_opt, size_type());
         auto pointer = to_dereference_expr(expr).pointer();
+        symbol_exprt deallocated =
+          ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+        symbol_exprt dead =
+          ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
         auto condition = r_or_w_ok_exprt(
-          access_type == access_typet::W ? ID_w_ok : ID_r_ok, pointer, size);
+          access_type == access_typet::W ? ID_w_ok : ID_r_ok,
+          pointer,
+          size,
+          deallocated,
+          dead);
         condition.add_source_location() = expr.source_location();
         auto assertion_source_location = expr.source_location();
         assertion_source_location.set_property_class("pointer");
@@ -330,8 +338,13 @@ void c_safety_checks(
             const auto &p1 = it->call_arguments()[0];
             const auto &p2 = it->call_arguments()[1];
             const auto &size = it->call_arguments()[2];
-            auto condition =
-              and_exprt(r_ok_exprt(p1, size), r_ok_exprt(p2, size));
+            symbol_exprt deallocated =
+              ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+            symbol_exprt dead =
+              ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+            auto condition = and_exprt(
+              r_ok_exprt{p1, size, deallocated, dead},
+              r_ok_exprt{p2, size, deallocated, dead});
             auto source_location = it->source_location();
             source_location.set_property_class("memcmp");
             source_location.set_comment("memcmp regions must be valid");
@@ -348,7 +361,11 @@ void c_safety_checks(
             // void *memchr(const void *, int, size_t);
             const auto &p = it->call_arguments()[0];
             const auto &size = it->call_arguments()[2];
-            auto condition = r_ok_exprt(p, size);
+            symbol_exprt deallocated =
+              ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+            symbol_exprt dead =
+              ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+            auto condition = r_ok_exprt{p, size, deallocated, dead};
             auto source_location = it->source_location();
             source_location.set_property_class("memchr");
             source_location.set_comment("memchr source must be valid");
@@ -365,7 +382,11 @@ void c_safety_checks(
             // void *memset(void *b, int c, size_t len);
             const auto &pointer = it->call_arguments()[0];
             const auto &size = it->call_arguments()[2];
-            auto condition = w_ok_exprt(pointer, size);
+            symbol_exprt deallocated =
+              ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+            symbol_exprt dead =
+              ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+            auto condition = w_ok_exprt{pointer, size, deallocated, dead};
             auto source_location = it->source_location();
             source_location.set_property_class("memset");
             source_location.set_comment("memset destination must be valid");
@@ -395,7 +416,11 @@ void c_safety_checks(
           {
             const auto &pointer = it->call_arguments()[0];
             const auto &size = it->call_arguments()[2];
-            auto condition = w_ok_exprt(pointer, size);
+            symbol_exprt deallocated =
+              ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
+            symbol_exprt dead =
+              ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+            auto condition = w_ok_exprt{pointer, size, deallocated, dead};
             auto source_location = it->source_location();
             source_location.set_property_class("memset");
             source_location.set_comment("memset destination must be valid");

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

@@ -699,7 +699,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/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,16 +369,23 @@ 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(
+  explicit 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);
@@ -400,6 +407,16 @@ class pointer_in_range_exprt : public ternary_exprt
     return op2();
   }
 
+  const exprt &deallocated_ptr() const
+  {
+    return op3();
+  }
+
+  const exprt &dead_ptr() const
+  {
+    return operands()[4];
+  }
+
   // translate into equivalent conjunction
   exprt lower() const;
 };
@@ -412,14 +429,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 +446,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 +831,22 @@ 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))
+  explicit 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)})
   {
   }
 
@@ -831,6 +859,16 @@ class r_or_w_ok_exprt : public binary_predicate_exprt
   {
     return op1();
   }
+
+  const exprt &deallocated_ptr() const
+  {
+    return op2();
+  }
+
+  const exprt &dead_ptr() const
+  {
+    return op3();
+  }
 };
 
 template <>
@@ -841,7 +879,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 +895,17 @@ 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))
+  explicit 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))
   {
   }
 };
@@ -871,7 +918,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 +933,17 @@ 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))
+  explicit 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))
   {
   }
 };
@@ -900,7 +956,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)