This is useful for:

+ checking containment in assigns clause verification
+ havocing only valid memory locations in assigns clause replacement
+ havocing only valid memory locations in loop contract application
+ creating history snapshots only for valid `old` expressions

Author: SaswatPadhi

regression/contracts/assigns_enforce_structs_07/main.c

@@ -25,9 +25,12 @@ void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf))
 
 int main()
 {
-  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  struct pair *p = malloc(sizeof(*p));
   f1(p);
+
   struct pair_of_pairs *pp = malloc(sizeof(*pp));
+  if(pp)
+    pp->p = malloc(sizeof(*(pp->p)));
   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
+--enforce-all-contracts _ --malloc-may-fail --malloc-fail-null --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

@@ -2,24 +2,23 @@
 #include <stdint.h>
 #include <stdlib.h>
 
-struct pair
+struct test
 {
-  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)
+void f1(struct test *p) __CPROVER_assigns(p->buf)
+  __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;
+  struct test *p = malloc(sizeof(*p));
+  uint8_t buf_1 = (p == NULL) ? 0 : p->buf[1];
   f1(p);
-  // clang-format off
-  assert(p != NULL ==> p->buf[0] == 0);
-  // clang-format on
-  return 0;
+  assert(p == NULL || p->buf[0] == 0);
+  assert(p == NULL || p->buf[1] == buf_1);
 }

regression/contracts/assigns_replace_07/test.desc

@@ -1,12 +1,13 @@
 CORE
 main.c
---replace-all-calls-with-contracts _ --pointer-check
+--replace-all-calls-with-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^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$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[0\] == 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[1\] == buf_1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
-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/Makefile

@@ -17,8 +17,9 @@ SRC = accelerate/accelerate.cpp \
       branch.cpp \
       call_sequences.cpp \
       contracts/assigns.cpp \
-      contracts/memory_predicates.cpp \
       contracts/contracts.cpp \
+      contracts/memory_predicates.cpp \
+      contracts/utils.cpp \
       concurrency.cpp \
       count_eloc.cpp \
       cover.cpp \

src/goto-instrument/contracts/assigns.cpp

@@ -17,11 +17,11 @@ 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>
 
+#include "utils.h"
+
 assigns_clauset::targett::targett(
   const assigns_clauset &parent,
   const exprt &expr)
@@ -46,27 +46,16 @@ 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{
+    all_dereferences_are_valid(dereference_exprt{address}, parent.ns),
+    all_dereferences_are_valid(dereference_exprt{lhs_address}, parent.ns)};
 
-  // __CPROVER_same_object(lhs, target)
+  exprt::operandst containment_check;
   containment_check.push_back(same_object(lhs_address, address));
 
   // If assigns target was a dereference, comparing objects is enough
-  // and the resulting condition will be
-  // __CPROVER_w_ok(target, sizeof(target))
-  // && __CPROVER_w_ok(lhs, sizeof(lhs))
-  // ==> __CPROVER_same_object(lhs, target)
+  // and the resulting condition will be:
+  // VALID(self) && VALID(lhs) ==> __CPROVER_same_object(lhs, self)
   if(id != ID_dereference)
   {
     const auto lhs_offset = pointer_offset(lhs_address);
@@ -89,19 +78,17 @@ exprt assigns_clauset::targett::generate_containment_check(
       own_offset);
 
     // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
-    // (sizeof(target) + __CPROVER_offset(target))
+    // (sizeof(self) + __CPROVER_offset(self))
     containment_check.push_back(
       binary_relation_exprt(lhs_region, ID_le, own_region));
   }
 
-  // __CPROVER_w_ok(target, sizeof(target))
-  // && __CPROVER_w_ok(lhs, sizeof(lhs))
-  // ==> __CPROVER_same_object(lhs, target)
-  //     && __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));
+  // VALID(self) && VALID(lhs)
+  // ==> __CPROVER_same_object(lhs, self)
+  //  && __CPROVER_offset(lhs) >= __CPROVER_offset(self)
+  //  && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
+  //        (sizeof(self) + __CPROVER_offset(self))
+  return or_exprt{not_exprt{address_validity}, conjunction(containment_check)};
 }
 
 assigns_clauset::assigns_clauset(
@@ -150,12 +137,13 @@ goto_programt assigns_clauset::generate_havoc_code() const
   modifiest modifies;
   for(const auto &target : global_write_set)
     modifies.insert(target.address.object());
-
   for(const auto &target : local_write_set)
     modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
-  append_havoc_code(location, modifies, havoc_statements);
+  havoc_if_validt havoc_gen(modifies, ns);
+  havoc_gen.append_full_havoc_code(location, 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"
@@ -150,7 +151,8 @@ void code_contractst::check_apply_loop_contracts(
   }
 
   // havoc the variables that may be modified
-  append_havoc_code(loop_head->source_location, modifies, havoc_code);
+  havoc_if_validt havoc_gen(modifies, ns);
+  havoc_gen.append_full_havoc_code(loop_head->source_location, havoc_code);
 
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,
@@ -366,6 +368,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 +383,23 @@ 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{all_dereferences_are_valid(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/contracts/utils.cpp

@@ -10,6 +10,64 @@ Date: September 2021
 
 #include "utils.h"
 
+#include <util/pointer_expr.h>
+#include <util/pointer_predicates.h>
+
+static void append_safe_havoc_code_for_expr(
+  const source_locationt location,
+  const namespacet &ns,
+  const exprt &expr,
+  goto_programt &dest,
+  const std::function<void()> &havoc_code_impl)
+{
+  goto_programt skip_program;
+  const auto skip_target = skip_program.add(goto_programt::make_skip(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{all_dereferences_are_valid(expr, ns)}, location));
+
+  havoc_code_impl();
+
+  // add the final skip target
+  dest.destructive_append(skip_program);
+}
+
+void havoc_if_validt::append_object_havoc_code_for_expr(
+  const source_locationt location,
+  const exprt &expr,
+  goto_programt &dest) const
+{
+  append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
+    havoc_utilst::append_object_havoc_code_for_expr(location, expr, dest);
+  });
+}
+
+void havoc_if_validt::append_scalar_havoc_code_for_expr(
+  const source_locationt location,
+  const exprt &expr,
+  goto_programt &dest) const
+{
+  append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
+    havoc_utilst::append_scalar_havoc_code_for_expr(location, expr, dest);
+  });
+}
+
+exprt all_dereferences_are_valid(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(all_dereferences_are_valid(op, ns));
+
+  return conjunction(validity_checks);
+}
+
 exprt generate_lexicographic_less_than_check(
   const std::vector<symbol_exprt> &lhs,
   const std::vector<symbol_exprt> &rhs)