Consider local write set in subset check

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

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),

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;

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());
     }
   }
 }