Fix alias checks within assigns clause

assigns_clauset was calling `compatible_expression` (not
`alias_expression`) on each target, and was thus only comparing the
object IDs (not offsets and sizes).
We fix this by removing `compatible_expression` entirely and calling
`alias_expression` for each from assigns_clauset.

Author: SaswatPadhi

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

@@ -22,7 +22,10 @@ Date: July 2021
 assigns_clauset::targett::targett(
   const assigns_clauset &parent,
   const exprt &expr)
-  : expr(address_of_exprt(expr)), id(expr.id()), parent(parent)
+  : expr(expr),
+    id(expr.id()),
+    object_expr(address_of_exprt(normalize(expr))),
+    parent(parent)
 {
 }
 
@@ -38,18 +41,20 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
   return to_index_expr(object).array();
 }
 
-exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const
+exprt assigns_clauset::targett::generate_containment_check(
+  const exprt &lhs) const
 {
   exprt::operandst condition;
   const auto lhs_ptr =
     (lhs.id() == ID_address_of) ? lhs : address_of_exprt(lhs);
 
   // __CPROVER_w_ok(target, sizeof(target))
   condition.push_back(w_ok_exprt(
-    expr, size_of_expr(dereference_exprt(expr).type(), parent.ns).value()));
+    object_expr,
+    size_of_expr(dereference_exprt(object_expr).type(), parent.ns).value()));
 
   // __CPROVER_same_object(lhs, target)
-  condition.push_back(same_object(lhs_ptr, expr));
+  condition.push_back(same_object(lhs_ptr, object_expr));
 
   // If assigns target was a dereference, comparing objects is enough
   if(id == ID_dereference)
@@ -58,7 +63,7 @@ exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const
   }
 
   const auto lhs_offset = pointer_offset(lhs_ptr);
-  const auto own_offset = pointer_offset(expr);
+  const auto own_offset = pointer_offset(object_expr);
 
   // __CPROVER_offset(lhs) >= __CPROVER_offset(target)
   condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, own_offset));
@@ -70,7 +75,7 @@ exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const
 
   const exprt own_region = plus_exprt(
     typecast_exprt::conditional_cast(
-      size_of_expr(dereference_exprt(expr).type(), parent.ns).value(),
+      size_of_expr(dereference_exprt(object_expr).type(), parent.ns).value(),
       own_offset.type()),
     own_offset);
 
@@ -81,12 +86,6 @@ exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const
   return conjunction(condition);
 }
 
-exprt assigns_clauset::targett::generate_compatibility_check(
-  const assigns_clauset::targett &other_target) const
-{
-  return same_object(other_target.expr, expr);
-}
-
 assigns_clauset::assigns_clauset(
   const exprt &expr,
   const messaget &log,
@@ -101,8 +100,7 @@ assigns_clauset::assigns_clauset(
 
 void assigns_clauset::add_target(const exprt &target_expr)
 {
-  auto insertion_succeeded =
-    targets.emplace(*this, targett::normalize(target_expr)).second;
+  auto insertion_succeeded = targets.emplace(*this, target_expr).second;
 
   if(!insertion_succeeded)
   {
@@ -117,87 +115,54 @@ goto_programt assigns_clauset::generate_havoc_code() const
 {
   modifiest modifies;
   for(const auto &target : targets)
-    modifies.insert(to_address_of_expr(target.expr).object());
+    modifies.insert(target.object_expr.object());
 
   goto_programt havoc_statements;
   append_havoc_code(expr.source_location(), modifies, havoc_statements);
   return havoc_statements;
 }
 
-exprt assigns_clauset::generate_alias_check(const exprt &lhs) const
+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();
-  }
 
   exprt::operandst condition;
   for(const auto &target : targets)
   {
-    condition.push_back(target.generate_alias_check(lhs));
+    condition.push_back(target.generate_containment_check(lhs));
   }
   return disjunction(condition);
 }
 
-exprt assigns_clauset::generate_compatibility_check(
-  const assigns_clauset &called_assigns) const
+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(const auto &called_target : called_assigns.targets)
+  for(const auto &subtarget : subassigns.targets)
   {
-    bool first_iter = true;
-    exprt current_target_compatible = false_exprt();
+    // 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.object_expr, from_integer(0, unsigned_int_type()));
+
+    exprt::operandst current_subtarget_found_conditions;
     for(const auto &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.expr;
-        if(
-          to_address_of_expr(called_target_ptr).object().id() == ID_dereference)
-        {
-          // or_exprt is short-circuited, therefore
-          // target.generate_compatibility_check(*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.generate_compatibility_check(called_target));
-        }
-        else
-        {
-          current_target_compatible =
-            target.generate_compatibility_check(called_target);
-        }
-        first_iter = false;
-      }
-      else
-      {
-        current_target_compatible = or_exprt(
-          current_target_compatible,
-          target.generate_compatibility_check(called_target));
-      }
-    }
-    if(first_clause)
-    {
-      result = current_target_compatible;
-      first_clause = false;
-    }
-    else
-    {
-      result = and_exprt(result, current_target_compatible);
+      current_subtarget_found_conditions.push_back(
+        target.generate_containment_check(subtarget.expr));
     }
+
+    auto current_subtarget_found = or_exprt(
+      not_exprt(validity_check),
+      disjunction(current_subtarget_found_conditions));
+
+    result = and_exprt(result, current_subtarget_found);
   }
 
   return result;

src/goto-instrument/contracts/assigns.h

@@ -30,8 +30,7 @@ class assigns_clauset
 
     static exprt normalize(const exprt &);
 
-    exprt generate_alias_check(const exprt &) const;
-    exprt generate_compatibility_check(const targett &) const;
+    exprt generate_containment_check(const exprt &) const;
 
     bool operator==(const targett &other) const
     {
@@ -46,8 +45,9 @@ class assigns_clauset
       }
     };
 
-    const exprt expr;
+    const exprt &expr;
     const irep_idt &id;
+    address_of_exprt object_expr;
     const assigns_clauset &parent;
   };
 
@@ -56,8 +56,8 @@ class assigns_clauset
   void add_target(const exprt &);
 
   goto_programt generate_havoc_code() const;
-  exprt generate_alias_check(const exprt &) const;
-  exprt generate_compatibility_check(const assigns_clauset &) const;
+  exprt generate_containment_check(const exprt &) const;
+  exprt generate_subset_check(const assigns_clauset &) const;
 
   const exprt &expr;
   const messaget &log;

src/goto-instrument/contracts/contracts.cpp

@@ -699,7 +699,7 @@ void code_contractst::instrument_assign_statement(
   {
     goto_programt alias_assertion;
     alias_assertion.add(goto_programt::make_assertion(
-      assigns_clause.generate_alias_check(lhs),
+      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");
@@ -763,7 +763,7 @@ void code_contractst::instrument_call_statement(
       freely_assignable_symbols.end())
   {
     const auto alias_expr =
-      assigns_clause.generate_alias_check(instruction_iterator->call_lhs());
+      assigns_clause.generate_containment_check(instruction_iterator->call_lhs());
 
     goto_programt alias_assertion;
     alias_assertion.add(goto_programt::make_assertion(
@@ -801,15 +801,15 @@ void code_contractst::instrument_call_statement(
     }
     replace_formal_params(called_assigns);
 
-    // check compatibility of assigns clause with the called function
+    // check subset relationship of assigns clause for called function
     assigns_clauset called_assigns_clause(called_assigns, log, ns);
-    const auto compatibility_check =
-      assigns_clause.generate_compatibility_check(called_assigns_clause);
+    const auto subset_check =
+      assigns_clause.generate_subset_check(called_assigns_clause);
     goto_programt alias_assertion;
     alias_assertion.add(goto_programt::make_assertion(
-      compatibility_check, instruction_iterator->source_location));
+      subset_check, instruction_iterator->source_location));
     alias_assertion.instructions.back().source_location.set_comment(
-      "Check compatibility of assigns clause with the called function");
+      "Check that callee's assigns clause is a subset of caller's");
     program.insert_before_swap(instruction_iterator, alias_assertion);
     ++instruction_iterator;
   }