Refactor replace_history_parameter

This function had some in/out parameters that were really only used as
out parameters, and also an undocumented (but crucial) `id` parameter.
Said `id` can only have one of two permitted values, so replace one
function with a parameter by two functions that have said `id` encoded
in the name. Return out-parameters by value rather than via references.

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -125,21 +125,16 @@ void code_contractst::check_apply_loop_contracts(
   //
   // Assertions for assigns clause checking are inserted in the loop body.
 
-  // an intermediate goto_program to store generated instructions
-  // to be inserted before the loop head
-  goto_programt pre_loop_head_instrs;
-
   // Process "loop_entry" history variables.
   // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant.
-  std::map<exprt, exprt> history_var_map;
-  replace_history_parameter(
-    symbol_table,
-    invariant,
-    history_var_map,
-    loop_head_location,
-    mode,
-    pre_loop_head_instrs,
-    ID_loop_entry);
+  auto replace_history_result = replace_history_loop_entry(
+    symbol_table, invariant, loop_head_location, mode);
+  invariant.swap(replace_history_result.expression_after_replacement);
+  const auto &history_var_map = replace_history_result.parameter_to_history;
+  // an intermediate goto_program to store generated instructions
+  // to be inserted before the loop head
+  goto_programt &pre_loop_head_instrs =
+    replace_history_result.history_construction;
 
   // Create a temporary to track if we entered the loop,
   // i.e., the loop guard was satisfied.

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -269,22 +269,13 @@ std::map<exprt, exprt> dfcc_instrument_loopt::add_prehead_instructions(
   //   GOTO HEAD;
   // ```
 
-  goto_programt pre_loop_head_instrs;
-  std::map<exprt, exprt> history_var_map;
 
   // initialize loop_entry history vars;
-  {
-    // Process "loop_entry" history variables.
-    // We find and replace all "__CPROVER_loop_entry" in invariant.
-    replace_history_parameter(
-      symbol_table,
-      invariant,
-      history_var_map,
-      loop_head_location,
-      language_mode,
-      pre_loop_head_instrs,
-      ID_loop_entry);
-  }
+  auto replace_history_result = replace_history_loop_entry(
+    symbol_table, invariant, loop_head_location, language_mode);
+  invariant.swap(replace_history_result.expression_after_replacement);
+  goto_programt &pre_loop_head_instrs =
+    replace_history_result.history_construction;
 
   // entered_loop = false
   {
@@ -354,7 +345,7 @@ std::map<exprt, exprt> dfcc_instrument_loopt::add_prehead_instructions(
     goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location));
 
   goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
-  return history_var_map;
+  return replace_history_result.parameter_to_history;
 }
 
 goto_programt::instructiont::targett

src/goto-instrument/contracts/utils.cpp

@@ -450,18 +450,18 @@ void add_quantified_variable(
   }
 }
 
-void replace_history_parameter(
+static void replace_history_parameter_rec(
   symbol_table_baset &symbol_table,
   exprt &expr,
   std::map<exprt, exprt> &parameter2history,
-  source_locationt location,
+  const source_locationt &location,
   const irep_idt &mode,
   goto_programt &history,
   const irep_idt &id)
 {
   for(auto &op : expr.operands())
   {
-    replace_history_parameter(
+    replace_history_parameter_rec(
       symbol_table, op, parameter2history, location, mode, history, id);
   }
 
@@ -527,25 +527,56 @@ void replace_history_parameter(
   }
 }
 
+replace_history_parametert replace_history_old(
+  symbol_table_baset &symbol_table,
+  const exprt &expr,
+  const source_locationt &location,
+  const irep_idt &mode)
+{
+  replace_history_parametert result;
+  result.expression_after_replacement = expr;
+  replace_history_parameter_rec(
+    symbol_table,
+    result.expression_after_replacement,
+    result.parameter_to_history,
+    location,
+    mode,
+    result.history_construction,
+    ID_old);
+  return result;
+}
+
+replace_history_parametert replace_history_loop_entry(
+  symbol_table_baset &symbol_table,
+  const exprt &expr,
+  const source_locationt &location,
+  const irep_idt &mode)
+{
+  replace_history_parametert result;
+  result.expression_after_replacement = expr;
+  replace_history_parameter_rec(
+    symbol_table,
+    result.expression_after_replacement,
+    result.parameter_to_history,
+    location,
+    mode,
+    result.history_construction,
+    ID_loop_entry);
+  return result;
+}
+
 void generate_history_variables_initialization(
   symbol_table_baset &symbol_table,
   exprt &clause,
   const irep_idt &mode,
   goto_programt &program)
 {
-  std::map<exprt, exprt> parameter2history;
-  goto_programt history;
   // Find and replace "old" expression in the "expression" variable
-  replace_history_parameter(
-    symbol_table,
-    clause,
-    parameter2history,
-    clause.source_location(),
-    mode,
-    history,
-    ID_old);
+  auto result =
+    replace_history_old(symbol_table, clause, clause.source_location(), mode);
+  clause.swap(result.expression_after_replacement);
   // Add all the history variable initialization instructions
-  program.destructive_append(history);
+  program.destructive_append(result.history_construction);
 }
 
 bool is_transformed_loop_head(const goto_programt::const_targett &target)

src/goto-instrument/contracts/utils.h

@@ -242,16 +242,28 @@ void add_quantified_variable(
   exprt &expression,
   const irep_idt &mode);
 
-/// This function recursively identifies the "old" expressions within expr
+struct replace_history_parametert
+{
+  exprt expression_after_replacement;
+  std::map<exprt, exprt> parameter_to_history;
+  goto_programt history_construction;
+};
+
+/// This function recursively identifies the "old" expressions within \p expr
 /// and replaces them with corresponding history variables.
-void replace_history_parameter(
+replace_history_parametert replace_history_old(
   symbol_table_baset &symbol_table,
-  exprt &expr,
-  std::map<exprt, exprt> &parameter2history,
-  source_locationt location,
-  const irep_idt &mode,
-  goto_programt &history,
-  const irep_idt &id);
+  const exprt &expr,
+  const source_locationt &location,
+  const irep_idt &mode);
+
+/// This function recursively identifies the "loop_entry" expressions within
+/// \p expr and replaces them with corresponding history variables.
+replace_history_parametert replace_history_loop_entry(
+  symbol_table_baset &symbol_table,
+  const exprt &expr,
+  const source_locationt &location,
+  const irep_idt &mode);
 
 /// This function generates all the instructions required to initialize
 /// history variables.