Merge pull request #6334 from padhi-aws-forks/assigns-cleanup

Refactor assigns clause implementation

Author: feliperodri

regression/contracts/assigns_repeated_ignored/main.c

@@ -0,0 +1,13 @@
+int foo(int *x) __CPROVER_assigns(*x, *x)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}

regression/contracts/assigns_repeated_ignored/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^Ignored duplicate expression '\*x' in assigns clause at file main\.c line \d+$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that repeated expressions in assigns clauses are
+correctly detected and ignored.

regression/contracts/assigns_validity_pointer_04/test.desc

@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
+--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
@@ -13,8 +13,13 @@ ASSUME .*::tmp_if_expr
 ASSUME \*z = 7
 --
 --
-Verification:
 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.

regression/contracts/test_aliasing_ensure_indirect/test.desc

@@ -7,7 +7,7 @@ main.c
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
 \[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
-\[foo.\d+\] line \d+ Check compatibility of assigns clause with the called function: SUCCESS
+\[foo.\d+\] line \d+ Check that callee's assigns clause is a subset of caller's: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --

src/goto-instrument/contracts/assigns.cpp

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Specify write set in function contracts.
+Module: Specify write set in code contracts.
 
 Author: Felipe R. Monteiro
 
@@ -19,205 +19,156 @@ Date: July 2021
 #include <util/c_types.h>
 #include <util/pointer_predicates.h>
 
-assigns_clause_targett::assigns_clause_targett(
-  const exprt &object,
-  code_contractst &contract,
-  messaget &log_parameter,
-  const irep_idt &function_id)
-  : contract(contract),
-    init_block(),
-    log(log_parameter),
-    target(pointer_for(object)),
-    target_id(object.id())
+assigns_clauset::targett::targett(
+  const assigns_clauset &parent,
+  const exprt &expr)
+  : address(address_of_exprt(normalize(expr))),
+    expr(expr),
+    id(expr.id()),
+    parent(parent)
 {
-  INVARIANT(
-    target.type().id() == ID_pointer,
-    "Assigns clause targets should be stored as pointer expressions.");
 }
 
-assigns_clause_targett::~assigns_clause_targett()
+exprt assigns_clauset::targett::normalize(const exprt &expr)
 {
+  if(expr.id() != ID_address_of)
+    return expr;
+
+  const auto &object = to_address_of_expr(expr).object();
+  if(object.id() != ID_index)
+    return object;
+
+  return to_index_expr(object).array();
 }
 
-exprt assigns_clause_targett::alias_expression(const exprt &lhs)
+exprt assigns_clauset::targett::generate_containment_check(
+  const address_of_exprt &lhs_address) const
 {
   exprt::operandst condition;
-  exprt lhs_ptr = (lhs.id() == ID_address_of) ? to_address_of_expr(lhs).object()
-                                              : pointer_for(lhs);
 
   // __CPROVER_w_ok(target, sizeof(target))
   condition.push_back(w_ok_exprt(
-    target,
-    size_of_expr(dereference_exprt(target).type(), contract.ns).value()));
+    address,
+    size_of_expr(dereference_exprt(address).type(), parent.ns).value()));
 
   // __CPROVER_same_object(lhs, target)
-  condition.push_back(same_object(lhs_ptr, target));
+  condition.push_back(same_object(lhs_address, address));
 
   // If assigns target was a dereference, comparing objects is enough
-  if(target_id == ID_dereference)
+  if(id == ID_dereference)
   {
     return conjunction(condition);
   }
 
-  const exprt lhs_offset = pointer_offset(lhs_ptr);
-  const exprt target_offset = pointer_offset(target);
+  const auto lhs_offset = pointer_offset(lhs_address);
+  const auto own_offset = pointer_offset(address);
 
   // __CPROVER_offset(lhs) >= __CPROVER_offset(target)
-  condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, target_offset));
+  condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, own_offset));
 
-  const exprt region_lhs = plus_exprt(
+  const auto lhs_region = plus_exprt(
     typecast_exprt::conditional_cast(
-      size_of_expr(lhs.type(), contract.ns).value(), lhs_offset.type()),
+      size_of_expr(lhs_address.object().type(), parent.ns).value(),
+      lhs_offset.type()),
     lhs_offset);
 
-  const exprt region_target = plus_exprt(
+  const exprt own_region = plus_exprt(
     typecast_exprt::conditional_cast(
-      size_of_expr(dereference_exprt(target).type(), contract.ns).value(),
-      target_offset.type()),
-    target_offset);
+      size_of_expr(address.object().type(), parent.ns).value(),
+      own_offset.type()),
+    own_offset);
 
   // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
   // (sizeof(target) + __CPROVER_offset(target))
-  condition.push_back(binary_relation_exprt(region_lhs, ID_le, region_target));
+  condition.push_back(binary_relation_exprt(lhs_region, ID_le, own_region));
 
   return conjunction(condition);
 }
 
-exprt assigns_clause_targett::compatible_expression(
-  const assigns_clause_targett &called_target)
-{
-  return same_object(called_target.get_target(), target);
-}
-
-const exprt &assigns_clause_targett::get_target() const
-{
-  return target;
-}
-
 assigns_clauset::assigns_clauset(
-  const exprt &assigns,
-  code_contractst &contract,
-  const irep_idt function_id,
-  messaget log_parameter)
-  : assigns(assigns),
-    parent(contract),
-    function_id(function_id),
-    log(log_parameter)
+  const exprt &expr,
+  const messaget &log,
+  const namespacet &ns)
+  : expr(expr), log(log), ns(ns)
 {
-  for(exprt target : assigns.operands())
+  for(const auto &target_expr : expr.operands())
   {
-    add_target(target);
+    add_target(target_expr);
   }
 }
 
-assigns_clauset::~assigns_clauset()
+void assigns_clauset::add_target(const exprt &target_expr)
 {
-  for(assigns_clause_targett *target : targets)
+  auto insertion_succeeded = targets.emplace(*this, target_expr).second;
+
+  if(!insertion_succeeded)
   {
-    delete target;
+    log.warning() << "Ignored duplicate expression '"
+                  << from_expr(ns, target_expr.id(), target_expr)
+                  << "' in assigns clause at "
+                  << target_expr.source_location().as_string() << messaget::eom;
   }
 }
 
-void assigns_clauset::add_target(exprt target)
+void assigns_clauset::remove_target(const exprt &target_expr)
 {
-  assigns_clause_targett *new_target = new assigns_clause_targett(
-    (target.id() == ID_address_of)
-      ? to_index_expr(to_address_of_expr(target).object()).array()
-      : target,
-    parent,
-    log,
-    function_id);
-  targets.push_back(new_target);
+  targets.erase(targett(*this, targett::normalize(target_expr)));
 }
 
-goto_programt assigns_clauset::havoc_code()
+goto_programt assigns_clauset::generate_havoc_code() const
 {
   modifiest modifies;
-  for(const auto &t : targets)
-    modifies.insert(to_address_of_expr(t->get_target()).object());
+  for(const auto &target : targets)
+    modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
-  append_havoc_code(assigns.source_location(), modifies, havoc_statements);
+  append_havoc_code(expr.source_location(), modifies, havoc_statements);
   return havoc_statements;
 }
 
-exprt assigns_clauset::alias_expression(const exprt &lhs)
+exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 {
   // If write set is empty, no assignment is allowed.
   if(targets.empty())
-  {
     return false_exprt();
-  }
+
+  const auto lhs_address = address_of_exprt(targett::normalize(lhs));
 
   exprt::operandst condition;
-  for(assigns_clause_targett *target : targets)
+  for(const auto &target : targets)
   {
-    condition.push_back(target->alias_expression(lhs));
+    condition.push_back(target.generate_containment_check(lhs_address));
   }
   return disjunction(condition);
 }
 
-exprt assigns_clauset::compatible_expression(
-  const assigns_clauset &called_assigns)
+exprt assigns_clauset::generate_subset_check(
+  const assigns_clauset &subassigns) const
 {
-  if(called_assigns.targets.empty())
-  {
+  if(subassigns.targets.empty())
     return true_exprt();
-  }
 
-  bool first_clause = true;
   exprt result = true_exprt();
-  for(assigns_clause_targett *called_target : called_assigns.targets)
+  for(const auto &subtarget : subassigns.targets)
   {
-    bool first_iter = true;
-    exprt current_target_compatible = false_exprt();
-    for(assigns_clause_targett *target : targets)
-    {
-      if(first_iter)
-      {
-        // TODO: Optimize the validation below and remove code duplication
-        // See GitHub issue #6105 for further details
-
-        // Validating the called target through __CPROVER_w_ok() is
-        // only useful when the called target is a dereference
-        const auto &called_target_ptr = called_target->get_target();
-        if(
-          to_address_of_expr(called_target_ptr).object().id() == ID_dereference)
-        {
-          // or_exprt is short-circuited, therefore
-          // target->compatible_expression(*called_target) would not be
-          // checked on invalid called_targets.
-          current_target_compatible = or_exprt(
-            not_exprt(w_ok_exprt(
-              called_target_ptr, from_integer(0, unsigned_int_type()))),
-            target->compatible_expression(*called_target));
-        }
-        else
-        {
-          current_target_compatible =
-            target->compatible_expression(*called_target);
-        }
-        first_iter = false;
-      }
-      else
-      {
-        current_target_compatible = or_exprt(
-          current_target_compatible,
-          target->compatible_expression(*called_target));
-      }
-    }
-    if(first_clause)
-    {
-      result = current_target_compatible;
-      first_clause = false;
-    }
-    else
+    // TODO: Optimize the implication generated due to the validity check.
+    // In some cases, e.g. when `subtarget` is known to be `NULL`,
+    // the implication can be skipped entirely. See #6105 for more details.
+    auto validity_check =
+      w_ok_exprt(subtarget.address, from_integer(0, unsigned_int_type()));
+
+    exprt::operandst current_subtarget_found_conditions;
+    for(const auto &target : targets)
     {
-      exprt::operandst conjuncts;
-      conjuncts.push_back(result);
-      conjuncts.push_back(current_target_compatible);
-      result = conjunction(conjuncts);
+      current_subtarget_found_conditions.push_back(
+        target.generate_containment_check(subtarget.address));
     }
+
+    auto current_subtarget_found = or_exprt(
+      not_exprt(validity_check),
+      disjunction(current_subtarget_found_conditions));
+
+    result = and_exprt(result, current_subtarget_found);
   }
 
   return result;