Merge pull request #6504 from tautschnig/modifies-to-assigns

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

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

@@ -150,21 +150,21 @@ void code_contractst::check_apply_loop_contracts(
       loop_end = t;
 
   // check for assigns, invariant, and decreases clauses
-  auto assigns = static_cast<const exprt &>(
+  auto assigns_clause = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_assigns));
   auto invariant = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_loop_invariant));
   auto decreases_clause = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_decreases));
 
   assigns_clauset loop_assigns(
-    assigns.operands(), log, ns, function_name, symbol_table);
+    assigns_clause.operands(), log, ns, function_name, symbol_table);
 
   loop_assigns.add_static_locals_to_write_set(goto_functions, function_name);
 
   if(invariant.is_nil())
   {
-    if(decreases_clause.is_nil() && assigns.is_nil())
+    if(decreases_clause.is_nil() && assigns_clause.is_nil())
       return;
     else
     {
@@ -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;
-  if(assigns.is_nil())
+  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,8 @@ void code_contractst::check_apply_loop_contracts(
   }
   else
   {
-    modifies.insert(assigns.operands().cbegin(), assigns.operands().cend());
+    assigns.insert(
+      assigns_clause.operands().cbegin(), assigns_clause.operands().cend());
 
     // Create snapshots of write set CARs.
     // This must be done before havocing the write set.
@@ -287,13 +288,13 @@ 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);
 
   // Add the havocing code, but only check against the enclosing scope's
   // write set if it was manually specified.
-  if(assigns.is_nil())
+  if(assigns_clause.is_nil())
     insert_before_swap_and_advance(
       goto_function.body,
       loop_head,
@@ -624,7 +625,7 @@ bool code_contractst::apply_function_contract(
   const auto &type = to_code_with_contract_type(function_symbol.type);
 
   // Isolate each component of the contract.
-  auto assigns = type.assigns();
+  auto assigns_clause = type.assigns();
   auto requires = conjunction(type.requires());
   auto ensures = conjunction(type.ensures());
 
@@ -740,24 +741,24 @@ bool code_contractst::apply_function_contract(
   // ASSIGNS clause should not refer to any quantified variables,
   // and only refer to the common symbols to be replaced.
   exprt targets;
-  for(auto &target : assigns)
+  for(auto &target : assigns_clause)
     targets.add_to_operands(std::move(target));
   common_replace(targets);
 
   // Create a sequence of non-deterministic assignments...
   goto_programt havoc_instructions;
 
   // ...for assigns clause targets
-  if(!assigns.empty())
+  if(!assigns_clause.empty())
   {
     assigns_clauset assigns_clause(
       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_assigns.cpp

@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module: Compute objects assigned to in a function
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Compute objects assigned to in a function.
+
+#include "function_assigns.h"
+
+#include <util/std_expr.h>
+
+#include <analyses/local_may_alias.h>
+
+#include "loop_utils.h"
+
+void function_assignst::get_assigns(
+  const local_may_aliast &local_may_alias,
+  const goto_programt::const_targett i_it,
+  assignst &assigns)
+{
+  const goto_programt::instructiont &instruction = *i_it;
+
+  if(instruction.is_assign())
+  {
+    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_assigns_lhs(local_may_alias, i_it, lhs, assigns);
+
+    get_assigns_function(instruction.call_function(), assigns);
+  }
+}
+
+void function_assignst::get_assigns_function(
+  const exprt &function,
+  assignst &assigns)
+{
+  if(function.id() == ID_symbol)
+  {
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
+
+    function_mapt::const_iterator fm_it = function_map.find(identifier);
+
+    if(fm_it != function_map.end())
+    {
+      // already done
+      assigns.insert(fm_it->second.begin(), fm_it->second.end());
+      return;
+    }
+
+    goto_functionst::function_mapt::const_iterator f_it =
+      goto_functions.function_map.find(identifier);
+
+    if(f_it == goto_functions.function_map.end())
+      return;
+
+    local_may_aliast local_may_alias(f_it->second);
+
+    const goto_programt &goto_program = f_it->second.body;
+
+    forall_goto_program_instructions(i_it, goto_program)
+      get_assigns(local_may_alias, i_it, assigns);
+  }
+  else if(function.id() == ID_if)
+  {
+    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, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \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