From fba232bc2728bec03231d71524f92835496dacd8 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Fri, 3 Sep 2021 19:03:04 +0000
Subject: [PATCH 1/7] Removes deallocated objects from write set

Anything that is local, including local allocations
are now tracked by our freely assignable set.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 .../contracts/assigns_enforce_18/main.c       | 35 ++++++++
 .../contracts/assigns_enforce_18/test.desc    | 21 +++++
 .../assigns_enforce_structs_04/test.desc      |  2 +-
 .../assigns_validity_pointer_04/test.desc     | 14 ++-
 src/goto-instrument/contracts/assigns.cpp     | 39 ++++++--
 src/goto-instrument/contracts/assigns.h       | 11 ++-
 src/goto-instrument/contracts/contracts.cpp   | 88 ++++++++-----------
 src/goto-instrument/contracts/contracts.h     | 24 +++--
 8 files changed, 145 insertions(+), 89 deletions(-)
 create mode 100644 regression/contracts/assigns_enforce_18/main.c
 create mode 100644 regression/contracts/assigns_enforce_18/test.desc

diff --git a/regression/contracts/assigns_enforce_18/main.c b/regression/contracts/assigns_enforce_18/main.c
new file mode 100644
index 00000000000..d773e2e149a
--- /dev/null
+++ b/regression/contracts/assigns_enforce_18/main.c
@@ -0,0 +1,35 @@
+#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;
+}
+
+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);
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc
new file mode 100644
index 00000000000..614f39693a1
--- /dev/null
+++ b/regression/contracts/assigns_enforce_18/test.desc
@@ -0,0 +1,21 @@
+CORE
+main.c
+--enforce-all-contracts _ --pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+^\[bar.\d+\] line \d+ Check that \*b 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$
+^.* 1 of \d+ failed \(\d+ iteration.*\)$
+^VERIFICATION FAILED$
+--
+^\[foo.pointer\_primitives.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(tmp\_cc\$\d+\): FAILURE$
+^.* 8 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.
diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc
index 98d5e666406..10849448fc9 100644
--- a/regression/contracts/assigns_enforce_structs_04/test.desc
+++ b/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$
 --
 --
diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc
index 28accca893f..0d3a03e4367 100644
--- a/regression/contracts/assigns_validity_pointer_04/test.desc
+++ b/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.
diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index b033cfa8763..600626f7930 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/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)
 {
@@ -99,7 +98,7 @@ assigns_clauset::assigns_clauset(
 
 void assigns_clauset::add_target(const exprt &target_expr)
 {
-  auto insertion_succeeded = targets.emplace(*this, target_expr).second;
+  auto insertion_succeeded = write_set.emplace(*this, target_expr).second;
 
   if(!insertion_succeeded)
   {
@@ -112,13 +111,30 @@ void assigns_clauset::add_target(const exprt &target_expr)
 
 void assigns_clauset::remove_target(const exprt &target_expr)
 {
-  targets.erase(targett(*this, targett::normalize(target_expr)));
+  write_set.erase(targett(*this, target_expr));
+}
+
+void assigns_clauset::add_freely_assignable_expr(const exprt &expr)
+{
+  auto insertion_succeeded = freely_assignable_set.emplace(*this, expr).second;
+
+  if(!insertion_succeeded)
+  {
+    log.warning() << "Ignored duplicate expression '"
+                  << from_expr(ns, expr.id(), expr) << "' in assigns clause at "
+                  << expr.source_location().as_string() << messaget::eom;
+  }
+}
+
+void assigns_clauset::remove_freely_assignable_expr(const exprt &expr)
+{
+  freely_assignable_set.erase(targett(*this, targett::normalize(expr)));
 }
 
 goto_programt assigns_clauset::generate_havoc_code() const
 {
   modifiest modifies;
-  for(const auto &target : targets)
+  for(const auto &target : write_set)
     modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
@@ -129,13 +145,18 @@ goto_programt assigns_clauset::generate_havoc_code() const
 exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 {
   // If write set is empty, no assignment is allowed.
-  if(targets.empty())
+  if(write_set.empty() && freely_assignable_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 : freely_assignable_set)
+  {
+    condition.push_back(target.generate_containment_check(lhs_address));
+  }
+
+  for(const auto &target : write_set)
   {
     condition.push_back(target.generate_containment_check(lhs_address));
   }
@@ -145,11 +166,11 @@ 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.write_set.empty())
     return true_exprt();
 
   exprt result = true_exprt();
-  for(const auto &subtarget : subassigns.targets)
+  for(const auto &subtarget : subassigns.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 +179,7 @@ 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 : write_set)
     {
       current_subtarget_found_conditions.push_back(
         target.generate_containment_check(subtarget.address));
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index 5b9d334364d..412876cf975 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -34,19 +34,18 @@ 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;
   };
@@ -56,6 +55,9 @@ class assigns_clauset
   void add_target(const exprt &);
   void remove_target(const exprt &);
 
+  void add_freely_assignable_expr(const exprt &);
+  void remove_freely_assignable_expr(const exprt &);
+
   goto_programt generate_havoc_code() const;
   exprt generate_containment_check(const exprt &) const;
   exprt generate_subset_check(const assigns_clauset &) const;
@@ -65,7 +67,8 @@ class assigns_clauset
   const namespacet &ns;
 
 protected:
-  std::unordered_set<targett, targett::hasht> targets;
+  std::unordered_set<targett, targett::hasht> write_set;
+  std::unordered_set<targett, targett::hasht> freely_assignable_set;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 4aad2ec3b74..c7953a3fa73 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -682,8 +682,6 @@ exprt code_contractst::create_alias_expression(
 void code_contractst::instrument_assign_statement(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,
-  exprt &assigns,
-  std::set<irep_idt> &freely_assignable_symbols,
   assigns_clauset &assigns_clause)
 {
   INVARIANT(
@@ -693,26 +691,19 @@ void code_contractst::instrument_assign_statement(
 
   const exprt &lhs = instruction_iterator->assign_lhs();
 
-  if(
-    freely_assignable_symbols.find(lhs.get(ID_identifier)) ==
-    freely_assignable_symbols.end())
-  {
-    goto_programt alias_assertion;
-    alias_assertion.add(goto_programt::make_assertion(
-      assigns_clause.generate_containment_check(lhs),
-      instruction_iterator->source_location));
-    alias_assertion.instructions.back().source_location.set_comment(
-      "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
-    insert_before_swap_and_advance(
-      program, instruction_iterator, alias_assertion);
-  }
+  goto_programt alias_assertion;
+  alias_assertion.add(goto_programt::make_assertion(
+    assigns_clause.generate_containment_check(lhs),
+    instruction_iterator->source_location));
+  alias_assertion.instructions.back().source_location.set_comment(
+    "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
+  insert_before_swap_and_advance(
+    program, instruction_iterator, alias_assertion);
 }
 
 void code_contractst::instrument_call_statement(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,
-  exprt &assigns,
-  std::set<irep_idt> &freely_assignable_symbols,
   assigns_clauset &assigns_clause)
 {
   INVARIANT(
@@ -742,25 +733,23 @@ void code_contractst::instrument_call_statement(
     instruction_iterator++;
     if(instruction_iterator->is_assign())
     {
-      const exprt &rhs = instruction_iterator->assign_rhs();
-      INVARIANT(
-        rhs.id() == ID_typecast,
-        "malloc is called but the result is not cast. Excluding result from "
-        "the assignable memory frame.");
-      typet cast_type = rhs.type();
-
-      // Make freshly allocated memory assignable, if we can determine its type.
-      assigns_clause.add_target(dereference_exprt(rhs));
+      instrument_assign_statement(
+        instruction_iterator, program, assigns_clause);
+      const exprt &lhs = instruction_iterator->assign_lhs();
+      assigns_clause.add_freely_assignable_expr(dereference_exprt(lhs));
     }
     return; // assume malloc edits no pre-existing memory objects.
   }
+  else if(called_name == "free")
+  {
+    assigns_clause.remove_freely_assignable_expr(dereference_exprt(
+      to_typecast_expr(instruction_iterator->call_arguments().front()).op()));
+    return;
+  }
 
   if(
     instruction_iterator->call_lhs().is_not_nil() &&
-    instruction_iterator->call_lhs().id() == ID_symbol &&
-    freely_assignable_symbols.find(
-      to_symbol_expr(instruction_iterator->call_lhs()).get_identifier()) ==
-      freely_assignable_symbols.end())
+    instruction_iterator->call_lhs().id() == ID_symbol)
   {
     const auto alias_expr = assigns_clause.generate_containment_check(
       instruction_iterator->call_lhs());
@@ -896,24 +885,28 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     return true;
   }
 
+  // Get assigns clause for function
+  const symbolt &target = ns.lookup(function);
+  assigns_clauset assigns(
+    to_code_with_contract_type(target.type).assigns(), log, ns);
+
+  // Adds formal parameters to freely assignable set
+  for(auto &parameter : to_code_type(target.type).parameters())
+  {
+    assigns.add_freely_assignable_expr(
+      ns.lookup(parameter.get_identifier()).symbol_expr());
+  }
+
   // Insert aliasing assertions
-  check_frame_conditions(program, ns.lookup(function));
+  check_frame_conditions(program, assigns);
 
   return false;
 }
 
 void code_contractst::check_frame_conditions(
   goto_programt &program,
-  const symbolt &target)
+  assigns_clauset &assigns)
 {
-  const auto &type = to_code_with_contract_type(target.type);
-  exprt assigns_expr = type.assigns();
-
-  assigns_clauset assigns(assigns_expr, log, ns);
-
-  // Create a list of variables that are okay to assign.
-  std::set<irep_idt> freely_assignable_symbols;
-
   for(auto instruction_it = program.instructions.begin();
       instruction_it != program.instructions.end();
       ++instruction_it)
@@ -921,18 +914,13 @@ void code_contractst::check_frame_conditions(
     if(instruction_it->is_decl())
     {
       // Local variables are always freely assignable
-      freely_assignable_symbols.insert(
-        instruction_it->get_decl().symbol().get_identifier());
-
-      assigns.add_target(instruction_it->get_decl().symbol());
+      assigns.add_freely_assignable_expr(instruction_it->get_decl().symbol());
     }
     else if(instruction_it->is_assign())
     {
       instrument_assign_statement(
         instruction_it,
         program,
-        assigns_expr,
-        freely_assignable_symbols,
         assigns);
     }
     else if(instruction_it->is_function_call())
@@ -940,16 +928,12 @@ void code_contractst::check_frame_conditions(
       instrument_call_statement(
         instruction_it,
         program,
-        assigns_expr,
-        freely_assignable_symbols,
         assigns);
     }
     else if(instruction_it->is_dead())
     {
-      freely_assignable_symbols.erase(
-        instruction_it->get_dead().symbol().get_identifier());
-
-      assigns.remove_target(instruction_it->get_dead().symbol());
+      assigns.remove_freely_assignable_expr(
+        instruction_it->get_dead().symbol());
     }
   }
 }
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
index 97da9806748..ec3c7b348b5 100644
--- a/src/goto-instrument/contracts/contracts.h
+++ b/src/goto-instrument/contracts/contracts.h
@@ -150,7 +150,7 @@ class code_contractst
 
   /// Insert assertion statements into the goto program to ensure that
   /// assigned memory is within the assignable memory frame.
-  void check_frame_conditions(goto_programt &program, const symbolt &target);
+  void check_frame_conditions(goto_programt &, assigns_clauset &);
 
   /// Check if there are any malloc statements which may be repeated because of
   /// a goto statement that jumps back.
@@ -159,24 +159,20 @@ class code_contractst
   /// Inserts an assertion statement into program before the assignment
   /// instruction_it, to ensure that the left-hand-side of the assignment
   /// aliases some expression in original_references, unless it is contained
-  /// in freely_assignable_exprs.
+  /// in freely assignable set.
   void instrument_assign_statement(
-    goto_programt::instructionst::iterator &instruction_it,
-    goto_programt &program,
-    exprt &assigns,
-    std::set<irep_idt> &freely_assignable_symbols,
-    assigns_clauset &assigns_clause);
+    goto_programt::instructionst::iterator &,
+    goto_programt &,
+    assigns_clauset &);
 
   /// Inserts an assertion statement into program before the function call at
   /// ins_it, to ensure that any memory which may be written by the call is
-  /// aliased by some expression in assigns_references,unless it is contained
-  /// in freely_assignable_exprs.
+  /// aliased by some expression in assigns_references, unless it is contained
+  /// in freely assignable set.
   void instrument_call_statement(
-    goto_programt::instructionst::iterator &ins_it,
-    goto_programt &program,
-    exprt &assigns,
-    std::set<irep_idt> &freely_assignable_symbols,
-    assigns_clauset &assigns_clause);
+    goto_programt::instructionst::iterator &,
+    goto_programt &,
+    assigns_clauset &);
 
   /// Creates a boolean expression which is true when there exists an expression
   /// in aliasable_references with the same pointer object and pointer offset as

From c06ccf1a4a46bb061f9bcbdc16182f42853daa45 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Mon, 13 Sep 2021 04:34:37 +0000
Subject: [PATCH 2/7] Removes unused methods from contracts module

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 src/goto-instrument/contracts/contracts.cpp | 13 -------------
 src/goto-instrument/contracts/contracts.h   |  7 -------
 2 files changed, 20 deletions(-)

diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index c7953a3fa73..66deb466831 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -666,19 +666,6 @@ goto_functionst &code_contractst::get_goto_functions()
   return goto_functions;
 }
 
-exprt code_contractst::create_alias_expression(
-  const exprt &lhs,
-  std::vector<exprt> &aliasable_references)
-{
-  exprt::operandst operands;
-  operands.reserve(aliasable_references.size());
-  for(auto aliasable : aliasable_references)
-  {
-    operands.push_back(equal_exprt(lhs, typecast_exprt(aliasable, lhs.type())));
-  }
-  return disjunction(operands);
-}
-
 void code_contractst::instrument_assign_statement(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
index ec3c7b348b5..ea020b47645 100644
--- a/src/goto-instrument/contracts/contracts.h
+++ b/src/goto-instrument/contracts/contracts.h
@@ -174,13 +174,6 @@ class code_contractst
     goto_programt &,
     assigns_clauset &);
 
-  /// Creates a boolean expression which is true when there exists an expression
-  /// in aliasable_references with the same pointer object and pointer offset as
-  /// the address of lhs.
-  exprt create_alias_expression(
-    const exprt &lhs,
-    std::vector<exprt> &aliasable_references);
-
   /// Apply loop contracts, whenever available, to all loops in `function`.
   /// Loop invariants, loop variants, and loop assigns clauses.
   void apply_loop_contract(

From 52387ab96d6b02b762f9f75b63bdc9a549428ec8 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Mon, 13 Sep 2021 18:53:06 +0000
Subject: [PATCH 3/7] Better naming scheme in assigns clause class

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 .../contracts/assigns_enforce_18/test.desc    |  3 +-
 src/goto-instrument/contracts/assigns.cpp     | 37 ++++++++++---------
 src/goto-instrument/contracts/assigns.h       | 15 ++++----
 src/goto-instrument/contracts/contracts.cpp   | 11 +++---
 4 files changed, 33 insertions(+), 33 deletions(-)

diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc
index 614f39693a1..34382f93ad4 100644
--- a/regression/contracts/assigns_enforce_18/test.desc
+++ b/regression/contracts/assigns_enforce_18/test.desc
@@ -12,8 +12,9 @@ main.c
 ^.* 1 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$
-^.* 8 of \d+ failed (\d+ iterations)$
+^.* 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
diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index 600626f7930..ba73de36cfa 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -88,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_global_write_set(target_expr);
   }
 }
 
-void assigns_clauset::add_target(const exprt &target_expr)
+void assigns_clauset::add_global_write_set(const exprt &target_expr)
 {
-  auto insertion_succeeded = write_set.emplace(*this, target_expr).second;
+  auto insertion_succeeded =
+    global_write_set.emplace(*this, target_expr).second;
 
   if(!insertion_succeeded)
   {
@@ -109,14 +110,14 @@ void assigns_clauset::add_target(const exprt &target_expr)
   }
 }
 
-void assigns_clauset::remove_target(const exprt &target_expr)
+void assigns_clauset::remove_global_write_set(const exprt &target_expr)
 {
-  write_set.erase(targett(*this, target_expr));
+  global_write_set.erase(targett(*this, target_expr));
 }
 
-void assigns_clauset::add_freely_assignable_expr(const exprt &expr)
+void assigns_clauset::add_local_write_set(const exprt &expr)
 {
-  auto insertion_succeeded = freely_assignable_set.emplace(*this, expr).second;
+  auto insertion_succeeded = local_write_set.emplace(*this, expr).second;
 
   if(!insertion_succeeded)
   {
@@ -126,37 +127,37 @@ void assigns_clauset::add_freely_assignable_expr(const exprt &expr)
   }
 }
 
-void assigns_clauset::remove_freely_assignable_expr(const exprt &expr)
+void assigns_clauset::remove_local_write_set(const exprt &expr)
 {
-  freely_assignable_set.erase(targett(*this, targett::normalize(expr)));
+  local_write_set.erase(targett(*this, expr));
 }
 
 goto_programt assigns_clauset::generate_havoc_code() const
 {
   modifiest modifies;
-  for(const auto &target : write_set)
+  for(const auto &target : global_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(write_set.empty() && freely_assignable_set.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 : freely_assignable_set)
+  for(const auto &target : local_write_set)
   {
     condition.push_back(target.generate_containment_check(lhs_address));
   }
 
-  for(const auto &target : write_set)
+  for(const auto &target : global_write_set)
   {
     condition.push_back(target.generate_containment_check(lhs_address));
   }
@@ -166,11 +167,11 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 exprt assigns_clauset::generate_subset_check(
   const assigns_clauset &subassigns) const
 {
-  if(subassigns.write_set.empty())
+  if(subassigns.global_write_set.empty())
     return true_exprt();
 
   exprt result = true_exprt();
-  for(const auto &subtarget : subassigns.write_set)
+  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`,
@@ -179,7 +180,7 @@ 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 : write_set)
+    for(const auto &target : global_write_set)
     {
       current_subtarget_found_conditions.push_back(
         target.generate_containment_check(subtarget.address));
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index 412876cf975..9cfd46aa1e8 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -52,23 +52,22 @@ class assigns_clauset
 
   assigns_clauset(const exprt &, const messaget &, const namespacet &);
 
-  void add_target(const exprt &);
-  void remove_target(const exprt &);
-
-  void add_freely_assignable_expr(const exprt &);
-  void remove_freely_assignable_expr(const exprt &);
+  void add_global_write_set(const exprt &);
+  void remove_global_write_set(const exprt &);
+  void add_local_write_set(const exprt &);
+  void remove_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> write_set;
-  std::unordered_set<targett, targett::hasht> freely_assignable_set;
+  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
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 66deb466831..243a70c37b6 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -723,13 +723,13 @@ void code_contractst::instrument_call_statement(
       instrument_assign_statement(
         instruction_iterator, program, assigns_clause);
       const exprt &lhs = instruction_iterator->assign_lhs();
-      assigns_clause.add_freely_assignable_expr(dereference_exprt(lhs));
+      assigns_clause.add_local_write_set(dereference_exprt(lhs));
     }
     return; // assume malloc edits no pre-existing memory objects.
   }
   else if(called_name == "free")
   {
-    assigns_clause.remove_freely_assignable_expr(dereference_exprt(
+    assigns_clause.remove_local_write_set(dereference_exprt(
       to_typecast_expr(instruction_iterator->call_arguments().front()).op()));
     return;
   }
@@ -880,7 +880,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
   // Adds formal parameters to freely assignable set
   for(auto &parameter : to_code_type(target.type).parameters())
   {
-    assigns.add_freely_assignable_expr(
+    assigns.add_local_write_set(
       ns.lookup(parameter.get_identifier()).symbol_expr());
   }
 
@@ -901,7 +901,7 @@ void code_contractst::check_frame_conditions(
     if(instruction_it->is_decl())
     {
       // Local variables are always freely assignable
-      assigns.add_freely_assignable_expr(instruction_it->get_decl().symbol());
+      assigns.add_local_write_set(instruction_it->get_decl().symbol());
     }
     else if(instruction_it->is_assign())
     {
@@ -919,8 +919,7 @@ void code_contractst::check_frame_conditions(
     }
     else if(instruction_it->is_dead())
     {
-      assigns.remove_freely_assignable_expr(
-        instruction_it->get_dead().symbol());
+      assigns.remove_local_write_set(instruction_it->get_dead().symbol());
     }
   }
 }

From c255a150209ac8d0c4ebe7b998b3ff7ad683c65f Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Mon, 13 Sep 2021 19:12:06 +0000
Subject: [PATCH 4/7] Havoc local write set for loop contracts

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 src/goto-instrument/contracts/assigns.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index ba73de36cfa..75d34f6c914 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -138,6 +138,9 @@ goto_programt assigns_clauset::generate_havoc_code() const
   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);
   return havoc_statements;

From e9cfb2cb2fa4adc70963e78454b557d5d826cee5 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Mon, 13 Sep 2021 20:13:50 +0000
Subject: [PATCH 5/7] Fix contract enforcement to work with (local and global)
 static variables

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 .../contracts/assigns_enforce_19/main.c       | 33 +++++++++++++++++++
 .../contracts/assigns_enforce_19/test.desc    | 17 ++++++++++
 src/goto-instrument/contracts/contracts.cpp   | 14 ++++++++
 3 files changed, 64 insertions(+)
 create mode 100644 regression/contracts/assigns_enforce_19/main.c
 create mode 100644 regression/contracts/assigns_enforce_19/test.desc

diff --git a/regression/contracts/assigns_enforce_19/main.c b/regression/contracts/assigns_enforce_19/main.c
new file mode 100644
index 00000000000..2069f227d90
--- /dev/null
+++ b/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;
+}
diff --git a/regression/contracts/assigns_enforce_19/test.desc b/regression/contracts/assigns_enforce_19/test.desc
new file mode 100644
index 00000000000..a2063f2bfa1
--- /dev/null
+++ b/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.
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 243a70c37b6..ded56412535 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -678,6 +678,20 @@ void code_contractst::instrument_assign_statement(
 
   const exprt &lhs = instruction_iterator->assign_lhs();
 
+  // Local static variables are not declared locally, therefore, they are not
+  // included in the local write set during declaration. We check here whether
+  // lhs of the assignment is a local static variable and, if it is indeed
+  // true, we add lhs to our local write set before checking the assignment.
+  if(lhs.id() == ID_symbol)
+  {
+    auto lhs_sym = ns.lookup(lhs.get(ID_identifier));
+    if(
+      lhs_sym.is_static_lifetime &&
+      lhs_sym.location.get_function() ==
+        instruction_iterator->source_location.get_function())
+      assigns_clause.add_local_write_set(lhs);
+  }
+
   goto_programt alias_assertion;
   alias_assertion.add(goto_programt::make_assertion(
     assigns_clause.generate_containment_check(lhs),

From 6d8639582bbb61dcc6091bfc5f3b3ef3db3bdec4 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Mon, 13 Sep 2021 20:25:46 +0000
Subject: [PATCH 6/7] Consider local write set in subset check

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 src/goto-instrument/contracts/assigns.cpp   | 29 ++++++++++++---------
 src/goto-instrument/contracts/assigns.h     |  8 +++---
 src/goto-instrument/contracts/contracts.cpp | 12 ++++-----
 3 files changed, 26 insertions(+), 23 deletions(-)

diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index 75d34f6c914..20b6f8c961d 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -92,11 +92,11 @@ assigns_clauset::assigns_clauset(
 {
   for(const auto &target_expr : expr.operands())
   {
-    add_global_write_set(target_expr);
+    add_to_global_write_set(target_expr);
   }
 }
 
-void assigns_clauset::add_global_write_set(const exprt &target_expr)
+void assigns_clauset::add_to_global_write_set(const exprt &target_expr)
 {
   auto insertion_succeeded =
     global_write_set.emplace(*this, target_expr).second;
@@ -110,24 +110,17 @@ void assigns_clauset::add_global_write_set(const exprt &target_expr)
   }
 }
 
-void assigns_clauset::remove_global_write_set(const exprt &target_expr)
+void assigns_clauset::remove_from_global_write_set(const exprt &target_expr)
 {
   global_write_set.erase(targett(*this, target_expr));
 }
 
-void assigns_clauset::add_local_write_set(const exprt &expr)
+void assigns_clauset::add_to_local_write_set(const exprt &expr)
 {
-  auto insertion_succeeded = local_write_set.emplace(*this, expr).second;
-
-  if(!insertion_succeeded)
-  {
-    log.warning() << "Ignored duplicate expression '"
-                  << from_expr(ns, expr.id(), expr) << "' in assigns clause at "
-                  << expr.source_location().as_string() << messaget::eom;
-  }
+  local_write_set.emplace(*this, expr);
 }
 
-void assigns_clauset::remove_local_write_set(const exprt &expr)
+void assigns_clauset::remove_from_local_write_set(const exprt &expr)
 {
   local_write_set.erase(targett(*this, expr));
 }
@@ -173,6 +166,11 @@ exprt assigns_clauset::generate_subset_check(
   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.global_write_set)
   {
@@ -188,6 +186,11 @@ exprt assigns_clauset::generate_subset_check(
       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));
+    }
 
     auto current_subtarget_found = or_exprt(
       not_exprt(validity_check),
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index 9cfd46aa1e8..1071ce8fb79 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -52,10 +52,10 @@ class assigns_clauset
 
   assigns_clauset(const exprt &, const messaget &, const namespacet &);
 
-  void add_global_write_set(const exprt &);
-  void remove_global_write_set(const exprt &);
-  void add_local_write_set(const exprt &);
-  void remove_local_write_set(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;
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index ded56412535..bbee5d3b58a 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -689,7 +689,7 @@ void code_contractst::instrument_assign_statement(
       lhs_sym.is_static_lifetime &&
       lhs_sym.location.get_function() ==
         instruction_iterator->source_location.get_function())
-      assigns_clause.add_local_write_set(lhs);
+      assigns_clause.add_to_local_write_set(lhs);
   }
 
   goto_programt alias_assertion;
@@ -737,13 +737,13 @@ void code_contractst::instrument_call_statement(
       instrument_assign_statement(
         instruction_iterator, program, assigns_clause);
       const exprt &lhs = instruction_iterator->assign_lhs();
-      assigns_clause.add_local_write_set(dereference_exprt(lhs));
+      assigns_clause.add_to_local_write_set(dereference_exprt(lhs));
     }
     return; // assume malloc edits no pre-existing memory objects.
   }
   else if(called_name == "free")
   {
-    assigns_clause.remove_local_write_set(dereference_exprt(
+    assigns_clause.remove_from_local_write_set(dereference_exprt(
       to_typecast_expr(instruction_iterator->call_arguments().front()).op()));
     return;
   }
@@ -894,7 +894,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
   // Adds formal parameters to freely assignable set
   for(auto &parameter : to_code_type(target.type).parameters())
   {
-    assigns.add_local_write_set(
+    assigns.add_to_local_write_set(
       ns.lookup(parameter.get_identifier()).symbol_expr());
   }
 
@@ -915,7 +915,7 @@ void code_contractst::check_frame_conditions(
     if(instruction_it->is_decl())
     {
       // Local variables are always freely assignable
-      assigns.add_local_write_set(instruction_it->get_decl().symbol());
+      assigns.add_to_local_write_set(instruction_it->get_decl().symbol());
     }
     else if(instruction_it->is_assign())
     {
@@ -933,7 +933,7 @@ void code_contractst::check_frame_conditions(
     }
     else if(instruction_it->is_dead())
     {
-      assigns.remove_local_write_set(instruction_it->get_dead().symbol());
+      assigns.remove_from_local_write_set(instruction_it->get_dead().symbol());
     }
   }
 }

From 39c62dda3abb0a9ffe2532a26ccbf0f0bda80353 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Tue, 14 Sep 2021 17:12:39 +0000
Subject: [PATCH 7/7] Check frame conditions on deallocating

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 regression/contracts/assigns_enforce_18/main.c    | 10 +++++++++-
 regression/contracts/assigns_enforce_18/test.desc |  5 ++++-
 src/goto-instrument/contracts/contracts.cpp       | 15 +++++++++++++--
 3 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/regression/contracts/assigns_enforce_18/main.c b/regression/contracts/assigns_enforce_18/main.c
index d773e2e149a..ef1ae4d163c 100644
--- a/regression/contracts/assigns_enforce_18/main.c
+++ b/regression/contracts/assigns_enforce_18/main.c
@@ -14,12 +14,18 @@ void foo(int *xp, int *xq, int a) __CPROVER_assigns(*xp)
   y = -1;
 }
 
-void bar(int *a, int *b) __CPROVER_assigns(a, *b)
+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;
@@ -31,5 +37,7 @@ int main()
   int b = 1;
   bar(a, &b);
   assert(b == 0);
+  int *c = malloc(sizeof(*c));
+  baz(&y, c);
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc
index 34382f93ad4..ba62f3a2b2e 100644
--- a/regression/contracts/assigns_enforce_18/test.desc
+++ b/regression/contracts/assigns_enforce_18/test.desc
@@ -3,13 +3,16 @@ 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$
-^.* 1 of \d+ failed \(\d+ iteration.*\)$
+^.* 2 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --
 ^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index bbee5d3b58a..a79e24f28cc 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -743,8 +743,19 @@ void code_contractst::instrument_call_statement(
   }
   else if(called_name == "free")
   {
-    assigns_clause.remove_from_local_write_set(dereference_exprt(
-      to_typecast_expr(instruction_iterator->call_arguments().front()).op()));
+    goto_programt alias_assertion;
+    const exprt &lhs_dereference = dereference_exprt(
+      to_typecast_expr(instruction_iterator->call_arguments().front()).op());
+    alias_assertion.add(goto_programt::make_assertion(
+      assigns_clause.generate_containment_check(lhs_dereference),
+      instruction_iterator->source_location));
+    alias_assertion.instructions.back().source_location.set_comment(
+      "Check that " + from_expr(ns, lhs_dereference.id(), lhs_dereference) +
+      " is assignable");
+    assigns_clause.remove_from_local_write_set(lhs_dereference);
+    assigns_clause.remove_from_global_write_set(lhs_dereference);
+    insert_before_swap_and_advance(
+      program, instruction_iterator, alias_assertion);
     return;
   }