Adds the notion of a local write set to contracts

regression/contracts/assigns_enforce_18/main.c

@@ -0,0 +1,43 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+int y = 0;
+
+void foo(int *xp, int *xq, int a) __CPROVER_assigns(*xp)
+{
+  a = 2;
+  int *yp = malloc(sizeof(int));
+  free(yp);
+  int z = 3;
+  *xp = 1;
+  y = -1;
+}
+
+void bar(int *a, int *b) __CPROVER_assigns(*a, *b)
+{
+  free(a);
+  *b = 0;
+}
+
+void baz(int *a, int *c) __CPROVER_assigns(*a)
+{
+  free(c);
+  *a = 0;
+}
+
+int main()
+{
+  int z = 0;
+  foo(&x, &z, z);
+  assert(x == 1);
+  assert(y == -1);
+  assert(z == 0);
+  int *a = malloc(sizeof(*a));
+  int b = 1;
+  bar(a, &b);
+  assert(b == 0);
+  int *c = malloc(sizeof(*c));
+  baz(&y, c);
+  return 0;
+}

regression/contracts/assigns_enforce_18/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--enforce-all-contracts _ --pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
+^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
+^\[baz.\d+\] line \d+ Check that \*c is assignable: FAILURE$
+^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
+^.* 2 of \d+ failed \(\d+ iteration.*\)$
+^VERIFICATION FAILED$
+--
+^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
+^\[foo.pointer\_primitives.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(tmp\_cc\$\d+\): FAILURE$
+^.* 3 of \d+ failed (\d+ iterations)$
+--
+Checks whether contract enforcement works with functions that deallocate memory.
+We had problems before when freeing a variable, but still keeping it on
+the writable set, which lead to deallocated variables issues.
+Now, if a memory is deallocated, we remove it from the our freely assignable set.

regression/contracts/assigns_enforce_19/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+
+static int b = 0;
+static int c = 0;
+
+int f() __CPROVER_assigns()
+{
+  static int a = 0;
+  a++;
+  return a;
+}
+
+int g(int *points_to_b, int *points_to_c)
+  __CPROVER_assigns(b) // Error: it should also mention c
+{
+  b = 1;
+  c = 2;
+  *points_to_b = 1;
+  *points_to_c = 2;
+}
+
+int main()
+{
+  assert(f() == 1);
+  assert(f() == 2);
+  assert(b == 0);
+  assert(c == 0);
+  g(&b, &c);
+  assert(b == 1);
+  assert(c == 2);
+
+  return 0;
+}

regression/contracts/assigns_enforce_19/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$
+^\[g.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[g.\d+\] line \d+ Check that c is assignable: FAILURE$
+^\[g.\d+\] line \d+ Check that \*points\_to\_b is assignable: SUCCESS$
+^\[g.\d+\] line \d+ Check that \*points\_to\_c is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether contract enforcement works with (local and global) static variables.
+Local static variables should be part of the local write set.
+Global static variables should be included in the global write set,
+otherwise any assignment to it is invalid.

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
 ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
 ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[f4.\d+\] line \d+ Check that p is assignable: FAILURE$
+^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -1,9 +1,11 @@
-KNOWNBUG
+CORE
 main.c
 --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
+^.* 1 of \d+ failed \(\d+ iteration.*\)$
+^VERIFICATION FAILED$
 // bar
 ASSERT \*foo::x > 0
 IF ¬\(\*foo::x = 3\) THEN GOTO \d
@@ -17,9 +19,3 @@ This test checks support for a malloced pointer that is assigned to by
 a function (bar and baz). Both functions bar and baz are being replaced by
 their function contracts, while the calling function foo is being checked
 (by enforcing it's function contracts).
-
-BUG: `z` is being assigned to in `foo`, but is not in `foo`s assigns clause!
-This test is expected to pass but it should not.
-It somehow used to (and still does on *nix), but that seems buggy.
-Most likely the bug is related to `freely_assignable_symbols`,
-which would be properly fixed in a subsequent PR.

src/goto-instrument/contracts/assigns.cpp

@@ -23,7 +23,6 @@ assigns_clauset::targett::targett(
   const assigns_clauset &parent,
   const exprt &expr)
   : address(address_of_exprt(normalize(expr))),
-    expr(expr),
     id(expr.id()),
     parent(parent)
 {
@@ -89,17 +88,18 @@ assigns_clauset::assigns_clauset(
   const exprt &expr,
   const messaget &log,
   const namespacet &ns)
-  : expr(expr), log(log), ns(ns)
+  : location(expr.source_location()), log(log), ns(ns)
 {
   for(const auto &target_expr : expr.operands())
   {
-    add_target(target_expr);
+    add_to_global_write_set(target_expr);
   }
 }
 
-void assigns_clauset::add_target(const exprt &target_expr)
+void assigns_clauset::add_to_global_write_set(const exprt &target_expr)
 {
-  auto insertion_succeeded = targets.emplace(*this, target_expr).second;
+  auto insertion_succeeded =
+    global_write_set.emplace(*this, target_expr).second;
 
   if(!insertion_succeeded)
   {
@@ -110,32 +110,50 @@ void assigns_clauset::add_target(const exprt &target_expr)
   }
 }
 
-void assigns_clauset::remove_target(const exprt &target_expr)
+void assigns_clauset::remove_from_global_write_set(const exprt &target_expr)
 {
-  targets.erase(targett(*this, targett::normalize(target_expr)));
+  global_write_set.erase(targett(*this, target_expr));
+}
+
+void assigns_clauset::add_to_local_write_set(const exprt &expr)
+{
+  local_write_set.emplace(*this, expr);
+}
+
+void assigns_clauset::remove_from_local_write_set(const exprt &expr)
+{
+  local_write_set.erase(targett(*this, expr));
 }
 
 goto_programt assigns_clauset::generate_havoc_code() const
 {
   modifiest modifies;
-  for(const auto &target : targets)
+  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(expr.source_location(), modifies, havoc_statements);
+  append_havoc_code(location, modifies, havoc_statements);
   return havoc_statements;
 }
 
 exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 {
   // If write set is empty, no assignment is allowed.
-  if(targets.empty())
+  if(global_write_set.empty() && local_write_set.empty())
     return false_exprt();
 
   const auto lhs_address = address_of_exprt(targett::normalize(lhs));
 
   exprt::operandst condition;
-  for(const auto &target : targets)
+  for(const auto &target : local_write_set)
+  {
+    condition.push_back(target.generate_containment_check(lhs_address));
+  }
+
+  for(const auto &target : global_write_set)
   {
     condition.push_back(target.generate_containment_check(lhs_address));
   }
@@ -145,11 +163,16 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 exprt assigns_clauset::generate_subset_check(
   const assigns_clauset &subassigns) const
 {
-  if(subassigns.targets.empty())
+  if(subassigns.global_write_set.empty())
     return true_exprt();
 
+  INVARIANT(
+    subassigns.local_write_set.empty(),
+    "Local write set for function calls should be empty at this point.\n" +
+      subassigns.location.as_string());
+
   exprt result = true_exprt();
-  for(const auto &subtarget : subassigns.targets)
+  for(const auto &subtarget : subassigns.global_write_set)
   {
     // TODO: Optimize the implication generated due to the validity check.
     // In some cases, e.g. when `subtarget` is known to be `NULL`,
@@ -158,7 +181,12 @@ exprt assigns_clauset::generate_subset_check(
       w_ok_exprt(subtarget.address, from_integer(0, unsigned_int_type()));
 
     exprt::operandst current_subtarget_found_conditions;
-    for(const auto &target : targets)
+    for(const auto &target : global_write_set)
+    {
+      current_subtarget_found_conditions.push_back(
+        target.generate_containment_check(subtarget.address));
+    }
+    for(const auto &target : local_write_set)
     {
       current_subtarget_found_conditions.push_back(
         target.generate_containment_check(subtarget.address));

src/goto-instrument/contracts/assigns.h

@@ -34,38 +34,40 @@ class assigns_clauset
 
     bool operator==(const targett &other) const
     {
-      return expr == other.expr;
+      return address == other.address;
     }
 
     struct hasht
     {
       std::size_t operator()(const targett &target) const
       {
-        return irep_hash{}(target.expr);
+        return irep_hash{}(target.address);
       }
     };
 
     const address_of_exprt address;
-    const exprt &expr;
     const irep_idt &id;
     const assigns_clauset &parent;
   };
 
   assigns_clauset(const exprt &, const messaget &, const namespacet &);
 
-  void add_target(const exprt &);
-  void remove_target(const exprt &);
+  void add_to_global_write_set(const exprt &);
+  void remove_from_global_write_set(const exprt &);
+  void add_to_local_write_set(const exprt &);
+  void remove_from_local_write_set(const exprt &);
 
   goto_programt generate_havoc_code() const;
   exprt generate_containment_check(const exprt &) const;
   exprt generate_subset_check(const assigns_clauset &) const;
 
-  const exprt &expr;
+  const source_locationt &location;
   const messaget &log;
   const namespacet &ns;
 
 protected:
-  std::unordered_set<targett, targett::hasht> targets;
+  std::unordered_set<targett, targett::hasht> global_write_set;
+  std::unordered_set<targett, targett::hasht> local_write_set;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H