Add a predicate to check validity of all derefs

This is useful for:
+ checking containment in assigns clause verification
+ havocing only valid memory locations in assigns clause replacement
+ creating history snapshots only for valid `old` expressions

Author: SaswatPadhi

regression/contracts/assigns_enforce_structs_07/main.c

@@ -28,6 +28,7 @@ int main()
   struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
   f1(p);
   struct pair_of_pairs *pp = malloc(sizeof(*pp));
+  pp->p = nondet_bool() ? malloc(sizeof(*(pp->p))) : NULL;
   f2(pp);
 
   return 0;

regression/contracts/assigns_enforce_structs_07/test.desc

@@ -1,17 +1,16 @@
-KNOWNBUG
+CORE
 main.c
 --enforce-all-contracts _ --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$
 ^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$
 ^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
 Checks whether CBMC properly evaluates write set of members
 from invalid objects. In this case, they are not writable.
-
-Bug: We need to check the validity of each dereference
-when accessing struct members.

regression/contracts/assigns_replace_07/main.c

@@ -4,22 +4,21 @@
 
 struct pair
 {
-  uint8_t *buf;
-  size_t size;
+  uint8_t buf[8];
 };
 
 void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
-  __CPROVER_ensures(p->buf[0] == 0)
+  __CPROVER_ensures((p == NULL) || p->buf[0] == 0)
 {
-  p->buf[0] = 0;
+  if(p != NULL) p->buf[0] = 0;
 }
 
 int main()
 {
   struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
   f1(p);
   // clang-format off
-  assert(p != NULL ==> p->buf[0] == 0);
+  assert(p == NULL || p->buf[0] == 0);
   // clang-format on
   return 0;
 }

regression/contracts/assigns_replace_07/test.desc

@@ -1,12 +1,12 @@
 CORE
 main.c
 --replace-all-calls-with-contracts _ --pointer-check
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=> p->buf\[0\] \=\= 0: FAILURE$
-^VERIFICATION FAILED$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[0\] == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether CBMC properly evaluates write set of members
-from invalid objects. In this case, they are not writable.
+Checks whether CBMC properly evaluates write set of members from invalid objects.
+Functions are not expected to write to invalid locations; CBMC flags such writes.
+For contract checking, we ignore invalid targets in assigns clauses and assignment LHS.

regression/contracts/invar_loop-entry_check/main.c

@@ -33,17 +33,17 @@ void main()
   assert(x2 == z2);
 
   int y3;
-  s *s1, *s2;
+  s s0, s1, *s2 = &s0;
   s2->n = malloc(sizeof(int));
-  s1->n = s2->n;
+  s1.n = s2->n;
 
   while(y3 > 0)
-    __CPROVER_loop_invariant(s1->n == __CPROVER_loop_entry(s1->n))
+    __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n))
     {
       --y3;
-      s1->n = s1->n + 1;
-      s1->n = s1->n - 1;
+      s0.n = s0.n + 1;
+      s2->n = s2->n - 1;
     }
 
-  assert(*(s1->n) == *(s2->n));
+  assert(*(s1.n) == *(s2->n));
 }

regression/contracts/invar_loop-entry_check/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
@@ -11,7 +11,7 @@ main.c
 ^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
 ^\[main.5\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.3\] .* assertion \*\(s1->n\) == \*\(s2->n\): SUCCESS$
+^\[main.assertion.3\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

src/goto-instrument/contracts/assigns.cpp

@@ -17,8 +17,6 @@ Date: July 2021
 
 #include <langapi/language_util.h>
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
@@ -46,19 +44,13 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
 exprt assigns_clauset::targett::generate_containment_check(
   const address_of_exprt &lhs_address) const
 {
-  exprt::operandst address_validity;
-  exprt::operandst containment_check;
-
   // __CPROVER_w_ok(target, sizeof(target))
-  address_validity.push_back(w_ok_exprt(
-    address,
-    size_of_expr(dereference_exprt(address).type(), parent.ns).value()));
-
   // __CPROVER_w_ok(lhs, sizeof(lhs))
-  address_validity.push_back(w_ok_exprt(
-    lhs_address,
-    size_of_expr(dereference_exprt(lhs_address).type(), parent.ns).value()));
+  const auto address_validity = and_exprt{
+    validate_all_derefs(dereference_exprt{address}, parent.ns),
+    validate_all_derefs(dereference_exprt{lhs_address}, parent.ns)};
 
+  exprt::operandst containment_check;
   // __CPROVER_same_object(lhs, target)
   containment_check.push_back(same_object(lhs_address, address));
 
@@ -100,8 +92,7 @@ exprt assigns_clauset::targett::generate_containment_check(
   //     && __CPROVER_offset(lhs) >= __CPROVER_offset(target)
   //     && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
   //        (sizeof(target) + __CPROVER_offset(target))
-  return binary_relation_exprt(
-    conjunction(address_validity), ID_implies, conjunction(containment_check));
+  return or_exprt{not_exprt{address_validity}, conjunction(containment_check)};
 }
 
 assigns_clauset::assigns_clauset(
@@ -155,7 +146,7 @@ goto_programt assigns_clauset::generate_havoc_code() const
     modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
-  append_havoc_code(location, modifies, havoc_statements);
+  append_havoc_code_if_valid(location, ns, modifies, havoc_statements);
   return havoc_statements;
 }
 

src/goto-instrument/contracts/contracts.cpp

@@ -33,6 +33,7 @@ Date: February 2016
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
 
 #include "assigns.h"
@@ -366,6 +367,11 @@ void code_contractst::replace_history_parameter(
 
       if(it == parameter2history.end())
       {
+        // 0. Create a skip target to jump to, if the parameter is invalid
+        goto_programt skip_program;
+        const auto skip_target =
+          skip_program.add(goto_programt::make_skip(location));
+
         // 1. Create a temporary symbol expression that represents the
         // history variable
         symbol_exprt tmp_symbol =
@@ -376,14 +382,21 @@ void code_contractst::replace_history_parameter(
         parameter2history[parameter] = tmp_symbol;
 
         // 3. Add the required instructions to the instructions list
-        // 3.1 Declare the newly created temporary variable
+        // 3.1. Declare the newly created temporary variable
         history.add(goto_programt::make_decl(tmp_symbol, location));
 
-        // 3.2 Add an assignment such that the value pointed to by the new
+        // 3.2. Skip storing the history if the expression is invalid
+        history.add(goto_programt::make_goto(
+          skip_target, not_exprt{validate_all_derefs(parameter, ns)}, location));
+
+        // 3.3. Add an assignment such that the value pointed to by the new
         // temporary variable is equal to the value of the corresponding
         // parameter
         history.add(
           goto_programt::make_assignment(tmp_symbol, parameter, location));
+
+        // 3.4. Add a skip target
+        history.destructive_append(skip_program);
       }
 
       expr = parameter2history[parameter];

src/goto-instrument/havoc_utils.cpp

@@ -16,9 +16,11 @@ Date: July 2021
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_predicates.h>
 
 void append_safe_havoc_code_for_expr(
   const source_locationt source_location,
+  const namespacet &ns,
   const exprt &expr,
   goto_programt &dest,
   const std::function<void()> &havoc_code_impl)
@@ -27,47 +29,37 @@ void append_safe_havoc_code_for_expr(
   const auto skip_target =
     skip_program.add(goto_programt::make_skip(source_location));
 
-  // for deref expressions, check for validity of underlying pointer,
-  // and skip havocing if invalid (to avoid spurious pointer deref errors)
-  if(expr.id() == ID_dereference)
-  {
-    const auto condition = not_exprt(w_ok_exprt(
-      to_dereference_expr(expr).pointer(),
-      from_integer(0, unsigned_int_type())));
-    dest.add(goto_programt::make_goto(skip_target, condition, source_location));
-  }
+  // skip havocing only if all pointer derefs in the expression are valid
+  // (to avoid spurious pointer deref errors)
+  dest.add(goto_programt::make_goto(
+    skip_target, not_exprt{validate_all_derefs(expr, ns)}, source_location));
 
   havoc_code_impl();
 
-  // for deref expressions, add the final skip target
-  if(expr.id() == ID_dereference)
-    dest.destructive_append(skip_program);
+  // add the final skip target
+  dest.destructive_append(skip_program);
 }
 
 void append_object_havoc_code_for_expr(
   const source_locationt source_location,
   const exprt &expr,
   goto_programt &dest)
 {
-  append_safe_havoc_code_for_expr(source_location, expr, dest, [&]() {
-    codet havoc(ID_havoc_object);
-    havoc.add_source_location() = source_location;
-    havoc.add_to_operands(expr);
-    dest.add(goto_programt::make_other(havoc, source_location));
-  });
+  codet havoc(ID_havoc_object);
+  havoc.add_source_location() = source_location;
+  havoc.add_to_operands(expr);
+  dest.add(goto_programt::make_other(havoc, source_location));
 }
 
 void append_scalar_havoc_code_for_expr(
   const source_locationt source_location,
   const exprt &expr,
   goto_programt &dest)
 {
-  append_safe_havoc_code_for_expr(source_location, expr, dest, [&]() {
-    side_effect_expr_nondett rhs(expr.type(), source_location);
-    goto_programt::targett t = dest.add(
-      goto_programt::make_assignment(expr, std::move(rhs), source_location));
-    t->code_nonconst().add_source_location() = source_location;
-  });
+  side_effect_expr_nondett rhs(expr.type(), source_location);
+  goto_programt::targett t = dest.add(
+    goto_programt::make_assignment(expr, std::move(rhs), source_location));
+  t->code_nonconst().add_source_location() = source_location;
 }
 
 void append_havoc_code(
@@ -92,3 +84,29 @@ void append_havoc_code(
     append_scalar_havoc_code_for_expr(source_location, expr, dest);
   }
 }
+
+void append_havoc_code_if_valid(
+  const source_locationt source_location,
+  const namespacet &ns,
+  const modifiest &modifies,
+  goto_programt &dest)
+{
+  havoc_utils_is_constantt is_constant(modifies);
+  for(const auto &expr : modifies)
+  {
+    if(expr.id() == ID_index || expr.id() == ID_dereference)
+    {
+      address_of_exprt address_of_expr(expr);
+      if(!is_constant(address_of_expr))
+      {
+        append_safe_havoc_code_for_expr(source_location, ns, expr, dest, [&]() {
+          append_object_havoc_code_for_expr(source_location, expr, dest);
+        });
+        continue;
+      }
+    }
+    append_safe_havoc_code_for_expr(source_location, ns, expr, dest, [&]() {
+      append_scalar_havoc_code_for_expr(source_location, expr, dest);
+    });
+  };
+}

src/goto-instrument/havoc_utils.h

@@ -16,7 +16,7 @@ Date: July 2021
 
 #include <set>
 
-#include <goto-programs/goto_program.h>
+#include <goto-programs/goto_model.h>
 
 #include <util/expr_util.h>
 
@@ -48,6 +48,12 @@ void append_havoc_code(
   const modifiest &modifies,
   goto_programt &dest);
 
+void append_havoc_code_if_valid(
+  const source_locationt source_location,
+  const namespacet &ns,
+  const modifiest &modifies,
+  goto_programt &dest);
+
 void append_object_havoc_code_for_expr(
   const source_locationt source_location,
   const exprt &expr,

src/util/pointer_predicates.cpp

@@ -205,3 +205,17 @@ exprt object_lower_bound(
 
   return binary_relation_exprt(std::move(p_offset), ID_lt, std::move(zero));
 }
+
+exprt validate_all_derefs(const exprt &expr, const namespacet &ns)
+{
+  exprt::operandst validity_checks;
+
+  if(expr.id() == ID_dereference)
+    validity_checks.push_back(
+      good_pointer_def(to_dereference_expr(expr).pointer(), ns));
+
+  for(const auto &op : expr.operands())
+    validity_checks.push_back(validate_all_derefs(op, ns));
+
+  return conjunction(validity_checks);
+}

src/util/pointer_predicates.h

@@ -50,6 +50,8 @@ exprt object_upper_bound(
   const exprt &pointer,
   const exprt &access_size);
 
+exprt validate_all_derefs(const exprt &ptr, const namespacet &);
+
 class is_invalid_pointer_exprt : public unary_predicate_exprt
 {
 public: