Merge pull request #7679 from tautschnig/cleanup/is_fresh

Decouple is_fresh from code_contractst

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -668,7 +668,8 @@ void code_contractst::apply_function_contract(
   // new program where all contract-derived instructions are added
   goto_programt new_program;
 
-  is_fresh_replacet is_fresh(*this, log, target_function);
+  is_fresh_replacet is_fresh(
+    goto_model, log.get_message_handler(), target_function);
   is_fresh.create_declarations();
   is_fresh.add_memory_map_decl(new_program);
 
@@ -1072,16 +1073,6 @@ void code_contractst::apply_loop_contract(
   }
 }
 
-symbol_tablet &code_contractst::get_symbol_table()
-{
-  return symbol_table;
-}
-
-goto_functionst &code_contractst::get_goto_functions()
-{
-  return goto_functions;
-}
-
 void code_contractst::check_frame_conditions_function(const irep_idt &function)
 {
   // Get the function object before instrumentation.
@@ -1302,7 +1293,8 @@ void code_contractst::add_contract_check(
     instantiation_values.push_back(p);
   }
 
-  is_fresh_enforcet visitor(*this, log, wrapper_function);
+  is_fresh_enforcet visitor(
+    goto_model, log.get_message_handler(), wrapper_function);
   visitor.create_declarations();
   visitor.add_memory_map_decl(check);
 

src/goto-instrument/contracts/contracts.h

@@ -126,10 +126,6 @@ class code_contractst
     exprt decreases_clause,
     const irep_idt &mode);
 
-  // for "helper" classes to update symbol table.
-  symbol_tablet &get_symbol_table();
-  goto_functionst &get_goto_functions();
-
   std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
   get_original_loop_number_map() const
   {

src/goto-instrument/contracts/memory_predicates.cpp

@@ -23,7 +23,6 @@ Date: July 2021
 #include <ansi-c/ansi_c_language.h>
 #include <linking/static_lifetime_init.h>
 
-#include "contracts.h"
 #include "instrument_spec_assigns.h"
 #include "utils.h"
 
@@ -34,6 +33,8 @@ std::set<irep_idt> &functions_in_scope_visitort::function_calls()
 
 void functions_in_scope_visitort::operator()(const goto_programt &prog)
 {
+  messaget log{message_handler};
+
   forall_goto_program_instructions(ins, prog)
   {
     if(ins->is_function_call())
@@ -163,12 +164,13 @@ void is_fresh_baset::add_memory_map_dead(goto_programt &program)
 
 void is_fresh_baset::add_declarations(const std::string &decl_string)
 {
+  messaget log{message_handler};
   log.debug() << "Creating declarations: \n" << decl_string << "\n";
 
   std::istringstream iss(decl_string);
 
   ansi_c_languaget ansi_c_language;
-  ansi_c_language.set_message_handler(log.get_message_handler());
+  ansi_c_language.set_message_handler(message_handler);
   configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor;
   config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE;
   ansi_c_language.parse(iss, "");
@@ -181,10 +183,10 @@ void is_fresh_baset::add_declarations(const std::string &decl_string)
   goto_functionst tmp_functions;
 
   // Add the new functions into the goto functions table.
-  parent.get_goto_functions().function_map[ensures_fn_name].copy_from(
+  goto_model.goto_functions.function_map[ensures_fn_name].copy_from(
     tmp_functions.function_map[ensures_fn_name]);
 
-  parent.get_goto_functions().function_map[requires_fn_name].copy_from(
+  goto_model.goto_functions.function_map[requires_fn_name].copy_from(
     tmp_functions.function_map[requires_fn_name]);
 
   for(const auto &symbol_pair : tmp_symbol_table.symbols)
@@ -194,31 +196,31 @@ void is_fresh_baset::add_declarations(const std::string &decl_string)
       symbol_pair.first == ensures_fn_name ||
       symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc")
     {
-      this->parent.get_symbol_table().insert(symbol_pair.second);
+      goto_model.symbol_table.insert(symbol_pair.second);
     }
     // Parameters are stored as scoped names in the symbol table.
     else if(
       (has_prefix(
          id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") ||
        has_prefix(
          id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) &&
-      parent.get_symbol_table().add(symbol_pair.second))
+      goto_model.symbol_table.add(symbol_pair.second))
     {
       UNREACHABLE;
     }
   }
 
-  if(parent.get_goto_functions().function_map.erase(INITIALIZE_FUNCTION) != 0)
+  if(goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0)
   {
     static_lifetime_init(
-      parent.get_symbol_table(),
-      parent.get_symbol_table().lookup_ref(INITIALIZE_FUNCTION).location);
+      goto_model.symbol_table,
+      goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location);
     goto_convert(
       INITIALIZE_FUNCTION,
-      parent.get_symbol_table(),
-      parent.get_goto_functions(),
+      goto_model.symbol_table,
+      goto_model.goto_functions,
       log.get_message_handler());
-    parent.get_goto_functions().update();
+    goto_model.goto_functions.update();
   }
 }
 
@@ -247,10 +249,10 @@ void is_fresh_baset::update_fn_call(
 /* Declarations for contract enforcement */
 
 is_fresh_enforcet::is_fresh_enforcet(
-  code_contractst &_parent,
-  messaget _log,
-  irep_idt _fun_id)
-  : is_fresh_baset(_parent, _log, _fun_id)
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  const irep_idt &_fun_id)
+  : is_fresh_baset(goto_model, message_handler, _fun_id)
 {
   std::stringstream ssreq, ssensure, ssmemmap;
   ssreq << CPROVER_PREFIX "enforce_requires_is_fresh";
@@ -262,20 +264,20 @@ is_fresh_enforcet::is_fresh_enforcet(
   ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id;
   this->memmap_name = ssmemmap.str();
 
-  const auto &mode = parent.get_symbol_table().lookup_ref(_fun_id).mode;
+  const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode;
   this->memmap_symbol = new_tmp_symbol(
     get_memmap_type(),
     source_locationt(),
     mode,
-    parent.get_symbol_table(),
+    goto_model.symbol_table,
     this->memmap_name,
     true);
 }
 
 void is_fresh_enforcet::create_declarations()
 {
   // Check if symbols are already declared
-  if(parent.get_symbol_table().lookup(requires_fn_name) != nullptr)
+  if(goto_model.symbol_table.has_symbol(requires_fn_name))
     return;
 
   std::ostringstream oss;
@@ -326,10 +328,10 @@ void is_fresh_enforcet::create_ensures_fn_call(goto_programt::targett &ins)
 }
 
 is_fresh_replacet::is_fresh_replacet(
-  code_contractst &_parent,
-  messaget _log,
-  irep_idt _fun_id)
-  : is_fresh_baset(_parent, _log, _fun_id)
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  const irep_idt &_fun_id)
+  : is_fresh_baset(goto_model, message_handler, _fun_id)
 {
   std::stringstream ssreq, ssensure, ssmemmap;
   ssreq << CPROVER_PREFIX "replace_requires_is_fresh";
@@ -341,21 +343,22 @@ is_fresh_replacet::is_fresh_replacet(
   ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id;
   this->memmap_name = ssmemmap.str();
 
-  const auto &mode = parent.get_symbol_table().lookup_ref(_fun_id).mode;
+  const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode;
   this->memmap_symbol = new_tmp_symbol(
     get_memmap_type(),
     source_locationt(),
     mode,
-    parent.get_symbol_table(),
+    goto_model.symbol_table,
     this->memmap_name,
     true);
 }
 
 void is_fresh_replacet::create_declarations()
 {
   // Check if symbols are already declared
-  if(parent.get_symbol_table().lookup(requires_fn_name) != nullptr)
+  if(goto_model.symbol_table.has_symbol(requires_fn_name))
     return;
+
   std::ostringstream oss;
   std::string cprover_prefix(CPROVER_PREFIX);
   oss << "static _Bool " << requires_fn_name

src/goto-instrument/contracts/memory_predicates.h

@@ -14,22 +14,22 @@ Date: July 2021
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
 
-#include <util/message.h>
 #include <util/symbol.h>
 
 #include <goto-programs/goto_program.h>
 
-class code_contractst;
 class goto_functionst;
+class goto_modelt;
+class message_handlert;
 
 class is_fresh_baset
 {
 public:
   is_fresh_baset(
-    code_contractst &_parent,
-    messaget _log,
-    const irep_idt _fun_id)
-    : parent(_parent), log(_log), fun_id(_fun_id)
+    goto_modelt &goto_model,
+    message_handlert &message_handler,
+    const irep_idt &_fun_id)
+    : goto_model(goto_model), message_handler(message_handler), fun_id(_fun_id)
   {
   }
 
@@ -51,9 +51,9 @@ class is_fresh_baset
   virtual void create_requires_fn_call(goto_programt::targett &target) = 0;
   virtual void create_ensures_fn_call(goto_programt::targett &target) = 0;
 
-  code_contractst &parent;
-  messaget log;
-  irep_idt fun_id;
+  goto_modelt &goto_model;
+  message_handlert &message_handler;
+  const irep_idt &fun_id;
 
   // written by the child classes.
   std::string memmap_name;
@@ -68,9 +68,9 @@ class is_fresh_enforcet : public is_fresh_baset
 {
 public:
   is_fresh_enforcet(
-    code_contractst &_parent,
-    messaget _log,
-    const irep_idt _fun_id);
+    goto_modelt &goto_model,
+    message_handlert &message_handler,
+    const irep_idt &_fun_id);
 
   virtual void create_declarations();
 
@@ -83,9 +83,9 @@ class is_fresh_replacet : public is_fresh_baset
 {
 public:
   is_fresh_replacet(
-    code_contractst &_parent,
-    messaget _log,
-    const irep_idt _fun_id);
+    goto_modelt &goto_model,
+    message_handlert &message_handler,
+    const irep_idt &_fun_id);
 
   virtual void create_declarations();
 
@@ -121,8 +121,8 @@ class functions_in_scope_visitort
 public:
   functions_in_scope_visitort(
     const goto_functionst &goto_functions,
-    messaget &log)
-    : goto_functions(goto_functions), log(log)
+    message_handlert &message_handler)
+    : goto_functions(goto_functions), message_handler(message_handler)
   {
   }
 
@@ -133,7 +133,7 @@ class functions_in_scope_visitort
 
 protected:
   const goto_functionst &goto_functions;
-  messaget &log;
+  message_handlert &message_handler;
   std::set<irep_idt> function_set;
 };