goto-instrument: replace "modifies" by "assigns" terminology

All this code collects assignments rather than checking for genuine
value changes (modifications).

Fixes: #6467

Author: tautschnig

src/goto-instrument/Makefile

@@ -38,7 +38,7 @@ SRC = accelerate/accelerate.cpp \
       dump_c.cpp \
       full_slicer.cpp \
       function.cpp \
-      function_modifies.cpp \
+      function_assigns.cpp \
       generate_function_bodies.cpp \
       goto_instrument_languages.cpp \
       goto_instrument_main.cpp \

src/goto-instrument/contracts/assigns.h

@@ -118,7 +118,7 @@ class assigns_clauset
 class havoc_assigns_targetst : public havoc_if_validt
 {
 public:
-  havoc_assigns_targetst(const modifiest &mod, const namespacet &ns)
+  havoc_assigns_targetst(const assignst &mod, const namespacet &ns)
     : havoc_if_validt(mod, ns)
   {
   }

src/goto-instrument/contracts/contracts.cpp

@@ -253,12 +253,12 @@ void code_contractst::check_apply_loop_contracts(
     add_pragma_disable_assigns_check(generated_code));
 
   // havoc the variables that may be modified
-  modifiest modifies;
+  assignst assigns;
   if(assigns_clause.is_nil())
   {
     try
     {
-      get_modifies(local_may_alias, loop, modifies);
+      get_assigns(local_may_alias, loop, assigns);
     }
     catch(const analysis_exceptiont &exc)
     {
@@ -271,7 +271,7 @@ void code_contractst::check_apply_loop_contracts(
   }
   else
   {
-    modifies.insert(
+    assigns.insert(
       assigns_clause.operands().cbegin(), assigns_clause.operands().cend());
 
     // Create snapshots of write set CARs.
@@ -288,7 +288,7 @@ void code_contractst::check_apply_loop_contracts(
       function_name, goto_function.body, loop_head, loop_end, loop_assigns);
   }
 
-  havoc_assigns_targetst havoc_gen(modifies, ns);
+  havoc_assigns_targetst havoc_gen(assigns, ns);
   havoc_gen.append_full_havoc_code(
     loop_head->source_location(), generated_code);
 
@@ -755,10 +755,10 @@ bool code_contractst::apply_function_contract(
       targets.operands(), log, ns, target_function, symbol_table);
 
     // Havoc all targets in the write set
-    modifiest modifies;
-    modifies.insert(targets.operands().cbegin(), targets.operands().cend());
+    assignst assigns;
+    assigns.insert(targets.operands().cbegin(), targets.operands().cend());
 
-    havoc_assigns_targetst havoc_gen(modifies, ns);
+    havoc_assigns_targetst havoc_gen(assigns, ns);
     havoc_gen.append_full_havoc_code(location, havoc_instructions);
   }
 

src/goto-instrument/contracts/utils.h

@@ -25,7 +25,7 @@ Date: September 2021
 class havoc_if_validt : public havoc_utilst
 {
 public:
-  havoc_if_validt(const modifiest &mod, const namespacet &ns)
+  havoc_if_validt(const assignst &mod, const namespacet &ns)
     : havoc_utilst(mod), ns(ns)
   {
   }

src/goto-instrument/function_modifies.cpp renamed to src/goto-instrument/function_assigns.cpp

@@ -1,48 +1,48 @@
 /*******************************************************************\
 
-Module: Modifies
+Module: Compute objects assigned to in a function
 
 Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
 /// \file
-/// Modifies
+/// Compute objects assigned to in a function.
 
-#include "function_modifies.h"
+#include "function_assigns.h"
 
 #include <util/std_expr.h>
 
 #include <analyses/local_may_alias.h>
 
 #include "loop_utils.h"
 
-void function_modifiest::get_modifies(
+void function_assignst::get_assigns(
   const local_may_aliast &local_may_alias,
   const goto_programt::const_targett i_it,
-  modifiest &modifies)
+  assignst &assigns)
 {
   const goto_programt::instructiont &instruction=*i_it;
 
   if(instruction.is_assign())
   {
-    get_modifies_lhs(local_may_alias, i_it, instruction.assign_lhs(), modifies);
+    get_assigns_lhs(local_may_alias, i_it, instruction.assign_lhs(), assigns);
   }
   else if(instruction.is_function_call())
   {
     const exprt &lhs = instruction.call_lhs();
 
     // return value assignment
     if(lhs.is_not_nil())
-      get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
+      get_assigns_lhs(local_may_alias, i_it, lhs, assigns);
 
-    get_modifies_function(instruction.call_function(), modifies);
+    get_assigns_function(instruction.call_function(), assigns);
   }
 }
 
-void function_modifiest::get_modifies_function(
+void function_assignst::get_assigns_function(
   const exprt &function,
-  modifiest &modifies)
+  assignst &assigns)
 {
   if(function.id()==ID_symbol)
   {
@@ -54,7 +54,7 @@ void function_modifiest::get_modifies_function(
     if(fm_it!=function_map.end())
     {
       // already done
-      modifies.insert(fm_it->second.begin(), fm_it->second.end());
+      assigns.insert(fm_it->second.begin(), fm_it->second.end());
       return;
     }
 
@@ -69,11 +69,11 @@ void function_modifiest::get_modifies_function(
     const goto_programt &goto_program=f_it->second.body;
 
     forall_goto_program_instructions(i_it, goto_program)
-      get_modifies(local_may_alias, i_it, modifies);
+      get_assigns(local_may_alias, i_it, assigns);
   }
   else if(function.id()==ID_if)
   {
-    get_modifies_function(to_if_expr(function).true_case(), modifies);
-    get_modifies_function(to_if_expr(function).false_case(), modifies);
+    get_assigns_function(to_if_expr(function).true_case(), assigns);
+    get_assigns_function(to_if_expr(function).false_case(), assigns);
   }
 }

src/goto-instrument/function_assigns.h

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Compute objects assigned to in a function
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Compute objects assigned to in a function.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_ASSIGNS_H
+#define CPROVER_GOTO_INSTRUMENT_FUNCTION_ASSIGNS_H
+
+#include <goto-programs/goto_program.h>
+
+#include <map>
+
+class goto_functionst;
+class local_may_aliast;
+
+class function_assignst
+{
+public:
+  explicit function_assignst(const goto_functionst &_goto_functions)
+    : goto_functions(_goto_functions)
+  {
+  }
+
+  typedef std::set<exprt> assignst;
+
+  void get_assigns(
+    const local_may_aliast &local_may_alias,
+    const goto_programt::const_targett,
+    assignst &);
+
+  void get_assigns_function(const exprt &, assignst &);
+
+  void operator()(const exprt &function, assignst &assigns)
+  {
+    get_assigns_function(function, assigns);
+  }
+
+protected:
+  const goto_functionst &goto_functions;
+
+  typedef std::map<irep_idt, assignst> function_mapt;
+  function_mapt function_map;
+};
+
+#endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_ASSIGNS_H

src/goto-instrument/function_modifies.h

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/remove_skip.h>
 
-#include "function_modifies.h"
+#include "function_assigns.h"
 #include "havoc_utils.h"
 #include "loop_utils.h"
 
@@ -26,23 +26,23 @@ class havoc_loopst
   typedef goto_functionst::goto_functiont goto_functiont;
 
   havoc_loopst(
-    function_modifiest &_function_modifies,
-    goto_functiont &_goto_function):
-    goto_function(_goto_function),
-    local_may_alias(_goto_function),
-    function_modifies(_function_modifies),
-    natural_loops(_goto_function.body)
+    function_assignst &_function_assigns,
+    goto_functiont &_goto_function)
+    : goto_function(_goto_function),
+      local_may_alias(_goto_function),
+      function_assigns(_function_assigns),
+      natural_loops(_goto_function.body)
   {
     havoc_loops();
   }
 
 protected:
   goto_functiont &goto_function;
   local_may_aliast local_may_alias;
-  function_modifiest &function_modifies;
+  function_assignst &function_assigns;
   natural_loops_mutablet natural_loops;
 
-  typedef std::set<exprt> modifiest;
+  typedef std::set<exprt> assignst;
   typedef const natural_loops_mutablet::natural_loopt loopt;
 
   void havoc_loops();
@@ -51,9 +51,7 @@ class havoc_loopst
     const goto_programt::targett loop_head,
     const loopt &);
 
-  void get_modifies(
-    const loopt &,
-    modifiest &);
+  void get_assigns(const loopt &, assignst &);
 };
 
 void havoc_loopst::havoc_loop(
@@ -63,12 +61,12 @@ void havoc_loopst::havoc_loop(
   assert(!loop.empty());
 
   // first find out what can get changed in the loop
-  modifiest modifies;
-  get_modifies(loop, modifies);
+  assignst assigns;
+  get_assigns(loop, assigns);
 
   // build the havocking code
   goto_programt havoc_code;
-  havoc_utilst havoc_gen(modifies);
+  havoc_utilst havoc_gen(assigns);
   havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
 
   // Now havoc at the loop head. Use insert_swap to
@@ -101,12 +99,10 @@ void havoc_loopst::havoc_loop(
   remove_skip(goto_function.body);
 }
 
-void havoc_loopst::get_modifies(
-  const loopt &loop,
-  modifiest &modifies)
+void havoc_loopst::get_assigns(const loopt &loop, assignst &assigns)
 {
   for(const auto &instruction_it : loop)
-    function_modifies.get_modifies(local_may_alias, instruction_it, modifies);
+    function_assigns.get_assigns(local_may_alias, instruction_it, assigns);
 }
 
 void havoc_loopst::havoc_loops()
@@ -119,8 +115,8 @@ void havoc_loopst::havoc_loops()
 
 void havoc_loops(goto_modelt &goto_model)
 {
-  function_modifiest function_modifies(goto_model.goto_functions);
+  function_assignst function_assigns(goto_model.goto_functions);
 
   for(auto &gf_entry : goto_model.goto_functions.function_map)
-    havoc_loopst(function_modifies, gf_entry.second);
+    havoc_loopst(function_assigns, gf_entry.second);
 }

src/goto-instrument/havoc_loops.cpp

@@ -22,7 +22,7 @@ void havoc_utilst::append_full_havoc_code(
   const source_locationt location,
   goto_programt &dest) const
 {
-  for(const auto &expr : modifies)
+  for(const auto &expr : assigns)
     append_havoc_code_for_expr(location, expr, dest);
 }