Unify havocing codegen within code contracts

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/Makefile

@@ -43,6 +43,7 @@ SRC = accelerate/accelerate.cpp \
       goto_instrument_parse_options.cpp \
       goto_program2code.cpp \
       havoc_loops.cpp \
+      havoc_utils.cpp \
       horn_encoding.cpp \
       insert_final_assert_false.cpp \
       interrupt.cpp \

src/goto-instrument/contracts/assigns.cpp

@@ -13,6 +13,8 @@ Date: July 2021
 
 #include "assigns.h"
 
+#include <goto-instrument/havoc_utils.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/pointer_predicates.h>
@@ -104,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;
@@ -197,47 +183,12 @@ 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;
+  for(const auto &t : targets)
+    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/contracts/contracts.cpp

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Verify and use annotated invariants and pre/post-conditions
+Module: Verify and use annotated loop and function contracts
 
 Author: Michael Tautschnig
 
@@ -9,20 +9,19 @@ Date: February 2016
 \*******************************************************************/
 
 /// \file
-/// Verify and use annotated invariants and pre/post-conditions
+/// Verify and use annotated loop and function contracts
 
 #include "contracts.h"
 
-#include "assigns.h"
-#include "memory_predicates.h"
-
 #include <algorithm>
 #include <map>
 
 #include <analyses/local_may_alias.h>
 
 #include <ansi-c/c_expr.h>
 
+#include <goto-instrument/havoc_utils.h>
+
 #include <goto-programs/remove_skip.h>
 
 #include <util/c_types.h>
@@ -34,6 +33,9 @@ Date: February 2016
 #include <util/pointer_offset_size.h>
 #include <util/replace_symbol.h>
 
+#include "assigns.h"
+#include "memory_predicates.h"
+
 // Create a lexicographic less-than relation between two tuples of variables.
 // This is used in the implementation of multidimensional decreases clauses.
 static exprt create_lexicographic_less_than(
@@ -185,8 +187,8 @@ void code_contractst::check_apply_loop_contracts(
       "Check loop invariant before entry");
   }
 
-  // havoc variables being written to
-  build_havoc_code(loop_head, modifies, havoc_code);
+  // havoc the variables that may be modified
+  append_havoc_code(loop_head->source_location, modifies, havoc_code);
 
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,

src/goto-instrument/havoc_loops.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 
 #include "function_modifies.h"
+#include "havoc_utils.h"
 #include "loop_utils.h"
 
 class havoc_loopst
@@ -67,7 +68,7 @@ void havoc_loopst::havoc_loop(
 
   // build the havocking code
   goto_programt havoc_code;
-  build_havoc_code(loop_head, modifies, havoc_code);
+  append_havoc_code(loop_head->source_location, modifies, havoc_code);
 
   // Now havoc at the loop head. Use insert_swap to
   // preserve jumps to loop head.

src/goto-instrument/havoc_utils.cpp

@@ -0,0 +1,94 @@
+/*******************************************************************\
+
+Module: Utilities for building havoc code for expressions.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: July 2021
+
+\*******************************************************************/
+
+/// \file
+/// Utilities for building havoc code for expressions
+
+#include "havoc_utils.h"
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/pointer_expr.h>
+
+void append_safe_havoc_code_for_expr(
+  const source_locationt source_location,
+  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(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));
+  }
+
+  havoc_code_impl();
+
+  // for deref expressions, add the final skip target
+  if(expr.id() == ID_dereference)
+    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));
+  });
+}
+
+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;
+  });
+}
+
+void append_havoc_code(
+  const source_locationt source_location,
+  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_object_havoc_code_for_expr(
+          source_location, address_of_expr, dest);
+        continue;
+      }
+    }
+
+    append_scalar_havoc_code_for_expr(source_location, expr, dest);
+  }
+}