Unify havocing code for all contracts

This change fixes multiple known issues:
- (function contracts) entire arrays were not being havoced
- (loop contracts) pointers not checked for nullness before havocing

Author: SaswatPadhi

regression/contracts/assigns_replace_06/main.c

@@ -4,45 +4,30 @@ void foo(char c[]) __CPROVER_assigns(c)
 {
 }
 
-void bar(char d[]) __CPROVER_assigns(d)
+void bar(char *d) __CPROVER_assigns(*d)
 {
 }
 
 int main()
 {
-  char b[10];
-  b[0] = 'a';
-  b[1] = 'b';
-  b[2] = 'c';
-  b[3] = 'd';
-  b[4] = 'e';
-  b[5] = 'f';
-  b[6] = 'g';
-  b[7] = 'h';
-  b[8] = 'i';
-  b[9] = 'j';
+  char b[4] = {'a', 'b', 'c', 'd'};
+
   foo(b);
-  assert(b[0] == 'a');
-  assert(b[1] == 'b');
-  assert(b[5] == 'f');
-  assert(b[6] == 'g');
-  assert(b[7] == 'h');
-  assert(b[8] == 'i');
-  assert(b[9] == 'j');
-
-  b[2] = 'c';
-  b[3] = 'd';
-  b[4] = 'e';
-  bar(b);
+
   assert(b[0] == 'a');
   assert(b[1] == 'b');
   assert(b[2] == 'c');
   assert(b[3] == 'd');
-  assert(b[4] == 'e');
-  assert(b[5] == 'f');
-  assert(b[6] == 'g');
-  assert(b[8] == 'i');
-  assert(b[9] == 'j');
+
+  b[1] = '1';
+  b[3] = '3';
+
+  bar(b + 3);
+
+  assert(b[0] == 'a');
+  assert(b[1] == '1');
+  assert(b[2] == 'c');
+  assert(b[3] == '3');
 
   return 0;
 }

regression/contracts/assigns_replace_06/test.desc

@@ -1,10 +1,19 @@
 CORE
 main.c
---replace-all-calls-with-contracts
+--replace-all-calls-with-contracts _ --pointer-primitive-check
+^\[main.assertion.1\] line \d+ assertion b\[0\] == 'a': FAILURE$
+^\[main.assertion.2\] line \d+ assertion b\[1\] == 'b': FAILURE$
+^\[main.assertion.3\] line \d+ assertion b\[2\] == 'c': FAILURE$
+^\[main.assertion.4\] line \d+ assertion b\[3\] == 'd': FAILURE$
+^\[main.assertion.5\] line \d+ assertion b\[0\] == 'a': FAILURE$
+^\[main.assertion.6\] line \d+ assertion b\[1\] == '1': SUCCESS$
+^\[main.assertion.7\] line \d+ assertion b\[2\] == 'c': FAILURE$
+^\[main.assertion.8\] line \d+ assertion b\[3\] == '3': FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+^\[.+\.pointer_primitives\.\d+] line .*: FAILURE$
 --
-Checks whether the values outside the array range specified by the assigns
-target are not havocked when calling the associated function.
+Checks that entire arrays and fixed single elements are correctly havoced
+when functions are replaced by contracts.

src/goto-instrument/contracts/assigns.cpp

@@ -106,22 +106,6 @@ exprt assigns_clause_targett::compatible_expression(
   return same_object(called_target.get_direct_pointer(), target);
 }
 
-goto_programt assigns_clause_targett::havoc_code() const
-{
-  goto_programt assigns_havoc;
-  source_locationt location = pointer_object.source_location();
-
-  exprt lhs = dereference_exprt(pointer_object);
-  side_effect_expr_nondett rhs(lhs.type(), location);
-
-  goto_programt::targett target =
-    assigns_havoc.add(goto_programt::make_assignment(
-      code_assignt(std::move(lhs), std::move(rhs)), location));
-  target->code_nonconst().add_source_location() = location;
-
-  return assigns_havoc;
-}
-
 const exprt &assigns_clause_targett::get_direct_pointer() const
 {
   return pointer_object;
@@ -199,47 +183,16 @@ goto_programt assigns_clauset::dead_stmts()
 
 goto_programt assigns_clauset::havoc_code()
 {
-  goto_programt havoc_statements;
-  source_locationt location = assigns.source_location();
-
-  for(assigns_clause_targett *target : targets)
-  {
-    // (1) If the assigned target is not a dereference,
-    // only include the havoc_statement
-
-    // (2) If the assigned target is a dereference, do the following:
-
-    // if(!__CPROVER_w_ok(target, 0)) goto z;
-    //      havoc_statements
-    // z: skip
+  modifiest modifies;
+  std::for_each(
+    targets.begin(),
+    targets.end(),
+    [&modifies](const assigns_clause_targett *t) {
+      modifies.insert(to_address_of_expr(t->get_direct_pointer()).object());
+    });
 
-    // create the z label
-    goto_programt tmp_z;
-    goto_programt::targett z = tmp_z.add(goto_programt::make_skip(location));
-
-    const auto &target_ptr = target->get_direct_pointer();
-
-    if(to_address_of_expr(target_ptr).object().id() == ID_dereference)
-    {
-      // create the condition
-      exprt condition =
-        not_exprt(w_ok_exprt(target_ptr, from_integer(0, unsigned_int_type())));
-      havoc_statements.add(goto_programt::make_goto(z, condition, location));
-    }
-
-    // create havoc_statements
-    for(goto_programt::instructiont instruction :
-        target->havoc_code().instructions)
-    {
-      havoc_statements.add(std::move(instruction));
-    }
-
-    if(to_address_of_expr(target_ptr).object().id() == ID_dereference)
-    {
-      // add the z label instruction
-      havoc_statements.destructive_append(tmp_z);
-    }
-  }
+  goto_programt havoc_statements;
+  append_havoc_code(assigns.source_location(), modifies, havoc_statements);
   return havoc_statements;
 }
 

src/goto-instrument/contracts/assigns.h

@@ -32,7 +32,6 @@ class assigns_clause_targett
   std::vector<symbol_exprt> temporary_declarations() const;
   exprt alias_expression(const exprt &lhs);
   exprt compatible_expression(const assigns_clause_targett &called_target);
-  goto_programt havoc_code() const;
   const exprt &get_direct_pointer() const;
   goto_programt &get_init_block();
 

src/goto-instrument/havoc_utils.cpp

@@ -13,6 +13,8 @@ Date: July 2021
 
 #include "havoc_utils.h"
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/pointer_expr.h>
 
@@ -36,28 +38,57 @@ class havoc_utils_is_constantt : public is_constantt
   const modifiest &modifies;
 };
 
+void append_safe_havoc_code_for_expr(
+  const source_locationt source_location,
+  const exprt &expr,
+  goto_programt &dest,
+  std::function<void()> havoc_code_impl)
+{
+  goto_programt skip_program;
+  goto_programt::targett skip_target =
+    skip_program.add(goto_programt::make_skip(source_location));
+
+  if(expr.id() == ID_dereference)
+  {
+    // check for validity of underlying pointer and skip havocing if invalid
+    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));
+  }
+
+  havoc_code_impl();
+
+  if(expr.id() == ID_dereference)
+    dest.destructive_append(skip_program);
+}
+
 void append_object_havoc_code_for_expr(
   const source_locationt source_location,
-  const exprt &lhs,
+  const exprt &expr,
   goto_programt &dest)
 {
-  codet havoc(ID_havoc_object);
-  havoc.add_source_location() = source_location;
-  havoc.add_to_operands(lhs);
+  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));
+    dest.add(goto_programt::make_other(havoc, source_location));
+  });
 }
 
 void append_scalar_havoc_code_for_expr(
   const source_locationt source_location,
-  const exprt &lhs,
+  const exprt &expr,
   goto_programt &dest)
 {
-  side_effect_expr_nondett rhs(lhs.type(), source_location);
+  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(lhs, std::move(rhs), source_location));
-  t->code_nonconst().add_source_location() = 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(
@@ -73,7 +104,8 @@ void append_havoc_code(
       address_of_exprt address_of_lhs(lhs);
       if(!is_constant(address_of_lhs))
       {
-        append_object_havoc_code_for_expr(source_location, address_of_lhs, dest);
+        append_object_havoc_code_for_expr(
+          source_location, address_of_lhs, dest);
         continue;
       }
     }