Maintain a single write set

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

Author: feliperodri

src/goto-instrument/contracts/assigns.cpp

@@ -43,6 +43,36 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
   return to_index_expr(object).array();
 }
 
+assigns_clauset::assigns_clauset(
+  const exprt::operandst &assigns,
+  const messaget &log,
+  const namespacet &ns)
+  : log(log), ns(ns)
+{
+  for(const auto &target_expr : assigns)
+  {
+    add_to_write_set(target_expr);
+  }
+}
+
+void assigns_clauset::add_to_write_set(const exprt &target_expr)
+{
+  auto insertion_succeeded = write_set.emplace(*this, target_expr).second;
+
+  if(!insertion_succeeded)
+  {
+    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::remove_from_write_set(const exprt &target_expr)
+{
+  write_set.erase(targett(*this, target_expr));
+}
+
 exprt assigns_clauset::targett::generate_containment_check(
   const address_of_exprt &lhs_address) const
 {
@@ -91,54 +121,11 @@ exprt assigns_clauset::targett::generate_containment_check(
   return or_exprt{not_exprt{address_validity}, conjunction(containment_check)};
 }
 
-assigns_clauset::assigns_clauset(
-  const exprt::operandst &assigns,
-  const messaget &log,
-  const namespacet &ns)
-  : log(log), ns(ns)
-{
-  for(const auto &target_expr : assigns)
-  {
-    add_to_global_write_set(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;
-
-  if(!insertion_succeeded)
-  {
-    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::remove_from_global_write_set(const exprt &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 source_locationt &location) const
 {
   modifiest modifies;
-  for(const auto &target : global_write_set)
-    modifies.insert(target.address.object());
-  for(const auto &target : local_write_set)
+  for(const auto &target : write_set)
     modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
@@ -151,17 +138,13 @@ assigns_clauset::generate_havoc_code(const source_locationt &location) const
 exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 {
   // If write set is empty, no assignment is allowed.
-  if(global_write_set.empty() && local_write_set.empty())
+  if(write_set.empty())
     return false_exprt();
 
   const auto lhs_address = address_of_exprt(targett::normalize(lhs));
 
   exprt::operandst condition;
-  for(const auto &target : local_write_set)
-  {
-    condition.push_back(target.generate_containment_check(lhs_address));
-  }
-  for(const auto &target : global_write_set)
+  for(const auto &target : write_set)
   {
     condition.push_back(target.generate_containment_check(lhs_address));
   }
@@ -171,26 +154,14 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const
 exprt assigns_clauset::generate_subset_check(
   const assigns_clauset &subassigns) const
 {
-  if(subassigns.global_write_set.empty())
+  if(subassigns.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.local_write_set.begin()
-        ->address.source_location()
-        .as_string());
-
   exprt result = true_exprt();
-  for(const auto &subtarget : subassigns.global_write_set)
+  for(const auto &subtarget : subassigns.write_set)
   {
     exprt::operandst current_subtarget_found_conditions;
-    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)
+    for(const auto &target : write_set)
     {
       current_subtarget_found_conditions.push_back(
         target.generate_containment_check(subtarget.address));

src/goto-instrument/contracts/assigns.h

@@ -58,10 +58,8 @@ class assigns_clauset
     const messaget &,
     const namespacet &);
 
-  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 &);
+  void add_to_write_set(const exprt &);
+  void remove_from_write_set(const exprt &);
 
   goto_programt generate_havoc_code(const source_locationt &) const;
   exprt generate_containment_check(const exprt &) const;
@@ -71,8 +69,7 @@ class assigns_clauset
   const namespacet &ns;
 
 protected:
-  std::unordered_set<targett, targett::hasht> global_write_set;
-  std::unordered_set<targett, targett::hasht> local_write_set;
+  std::unordered_set<targett, targett::hasht> write_set;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H

src/goto-instrument/contracts/contracts.cpp

@@ -678,7 +678,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_to_local_write_set(lhs);
+      assigns_clause.add_to_write_set(lhs);
   }
 
   add_containment_check(program, assigns_clause, instruction_iterator, lhs);
@@ -719,7 +719,7 @@ void code_contractst::instrument_call_statement(
     {
       instrument_assign_statement(instruction_it, body, assigns);
       const exprt &lhs = instruction_it->assign_lhs();
-      assigns.add_to_local_write_set(dereference_exprt(lhs));
+      assigns.add_to_write_set(dereference_exprt(lhs));
     }
     return; // assume malloc edits no pre-existing memory objects.
   }
@@ -728,8 +728,7 @@ void code_contractst::instrument_call_statement(
     const exprt &lhs_dereference = dereference_exprt(
       to_typecast_expr(instruction_it->call_arguments().front()).op());
     add_containment_check(body, assigns, instruction_it, lhs_dereference);
-    assigns.remove_from_local_write_set(lhs_dereference);
-    assigns.remove_from_global_write_set(lhs_dereference);
+    assigns.remove_from_write_set(lhs_dereference);
     return;
   }
 }
@@ -822,7 +821,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_to_local_write_set(
+    assigns.add_to_write_set(
       ns.lookup(parameter.get_identifier()).symbol_expr());
   }
 
@@ -847,7 +846,7 @@ void code_contractst::check_frame_conditions(
     if(instruction_it->is_decl())
     {
       // Local variables are always freely assignable
-      assigns.add_to_local_write_set(instruction_it->get_decl().symbol());
+      assigns.add_to_write_set(instruction_it->get_decl().symbol());
     }
     else if(instruction_it->is_assign())
     {
@@ -859,7 +858,7 @@ void code_contractst::check_frame_conditions(
     }
     else if(instruction_it->is_dead())
     {
-      assigns.remove_from_local_write_set(instruction_it->get_dead().symbol());
+      assigns.remove_from_write_set(instruction_it->get_dead().symbol());
     }
     else if(
       instruction_it->is_other() &&
@@ -868,8 +867,7 @@ void code_contractst::check_frame_conditions(
       const exprt &havoc_argument = dereference_exprt(
         to_typecast_expr(instruction_it->get_other().operands().front()).op());
       add_containment_check(body, assigns, instruction_it, havoc_argument);
-      assigns.remove_from_local_write_set(havoc_argument);
-      assigns.remove_from_global_write_set(havoc_argument);
+      assigns.remove_from_write_set(havoc_argument);
     }
   }
 }