Refactor replace_history_parameter

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

@@ -167,7 +167,7 @@ void dfcc_instrument_loopt::operator()(
   goto_programt::targett loop_latch =
     loop.find_latch(goto_function.body).value();
 
-  const auto &history_var_map = add_prehead_instructions(
+  const auto history_var_map = add_prehead_instructions(
     loop_id,
     goto_function,
     symbol_table,
@@ -234,7 +234,8 @@ void dfcc_instrument_loopt::operator()(
   goto_function.body.update();
 }
 
-std::map<exprt, exprt> dfcc_instrument_loopt::add_prehead_instructions(
+std::unordered_map<exprt, symbol_exprt, irep_hash>
+dfcc_instrument_loopt::add_prehead_instructions(
   const std::size_t loop_id,
   goto_functionst::goto_functiont &goto_function,
   symbol_tablet &symbol_table,
@@ -269,22 +270,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 +346,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
@@ -614,7 +606,7 @@ void dfcc_instrument_loopt::add_exit_instructions(
   goto_programt::targett loop_head,
   const symbol_exprt &loop_write_set,
   const symbol_exprt &addr_of_loop_write_set,
-  const std::map<exprt, exprt> &history_var_map,
+  const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
   const symbol_exprt &entered_loop,
   const symbol_exprt &initial_invariant,
   const symbol_exprt &in_base_case,
@@ -690,10 +682,7 @@ void dfcc_instrument_loopt::add_exit_instructions(
 
     // Mark history variables as going out of scope.
     for(const auto &v : history_var_map)
-    {
-      loop_exit_program.add(
-        goto_programt::make_dead(to_symbol_expr(v.second), exit_location));
-    }
+      loop_exit_program.add(goto_programt::make_dead(v.second, exit_location));
 
     // Mark decreases clause snapshots as gong out of scope.
     for(size_t i = 0; i < old_decreases_vars.size(); i++)

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

@@ -197,7 +197,7 @@ class dfcc_instrument_loopt
   /// \param[in] in_base_case temporary variable `in_base_case`.
   /// \param[in] symbol_mode Language mode of the function.
   /// \return `history_var_map` that maps variables to loop_entry variables.
-  std::map<exprt, exprt> add_prehead_instructions(
+  std::unordered_map<exprt, symbol_exprt, irep_hash> add_prehead_instructions(
     const std::size_t loop_id,
     goto_functionst::goto_functiont &goto_function,
     symbol_tablet &symbol_table,
@@ -348,7 +348,7 @@ class dfcc_instrument_loopt
     goto_programt::targett loop_head,
     const symbol_exprt &loop_write_set,
     const symbol_exprt &addr_of_loop_write_set,
-    const std::map<exprt, exprt> &history_var_map,
+    const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
     const symbol_exprt &entered_loop,
     const symbol_exprt &initial_invariant,
     const symbol_exprt &in_base_case,

src/goto-instrument/contracts/utils.cpp

@@ -11,7 +11,6 @@ Date: September 2021
 #include "utils.h"
 
 #include <util/c_types.h>
-#include <util/exception_utils.h>
 #include <util/fresh_symbol.h>
 #include <util/graph.h>
 #include <util/mathematical_expr.h>
@@ -450,81 +449,107 @@ 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,
+  std::unordered_map<exprt, symbol_exprt, irep_hash> &parameter2history,
+  const source_locationt &location,
   const irep_idt &mode,
   goto_programt &history,
-  const irep_idt &id)
+  const irep_idt &history_id)
 {
   for(auto &op : expr.operands())
   {
-    replace_history_parameter(
-      symbol_table, op, parameter2history, location, mode, history, id);
+    replace_history_parameter_rec(
+      symbol_table, op, parameter2history, location, mode, history, history_id);
   }
 
-  if(expr.id() == ID_old || expr.id() == ID_loop_entry)
-  {
-    const auto &parameter = to_history_expr(expr, id).expression();
+  if(expr.id() != ID_old && expr.id() != ID_loop_entry)
+    return;
 
-    const auto &id = parameter.id();
-    if(
-      id == ID_dereference || id == ID_member || id == ID_symbol ||
+  const auto &parameter = to_history_expr(expr, history_id).expression();
+  const auto &id = parameter.id();
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    id == ID_dereference || id == ID_member || id == ID_symbol ||
       id == ID_ptrmember || id == ID_constant || id == ID_typecast ||
-      id == ID_index)
-    {
-      auto it = parameter2history.find(parameter);
+      id == ID_index,
+    "Tracking history of " + id2string(id) +
+      " expressions is not supported yet.",
+    parameter.pretty());
 
-      if(it == parameter2history.end())
-      {
-        // 0. Create a skip target to jump to, if the parameter is invalid
-        goto_programt skip_program;
-        const auto skip_target =
-          skip_program.add(goto_programt::make_skip(location));
-
-        // 1. Create a temporary symbol expression that represents the
-        // history variable
-        symbol_exprt tmp_symbol =
-          new_tmp_symbol(parameter.type(), location, mode, symbol_table)
-            .symbol_expr();
-
-        // 2. Associate the above temporary variable to it's corresponding
-        // expression
-        parameter2history[parameter] = tmp_symbol;
-
-        // 3. Add the required instructions to the instructions list
-        // 3.1. Declare the newly created temporary variable
-        history.add(goto_programt::make_decl(tmp_symbol, location));
-
-        // 3.2. Skip storing the history if the expression is invalid
-        history.add(goto_programt::make_goto(
-          skip_target,
-          not_exprt{
-            all_dereferences_are_valid(parameter, namespacet(symbol_table))},
-          location));
-
-        // 3.3. Add an assignment such that the value pointed to by the new
-        // temporary variable is equal to the value of the corresponding
-        // parameter
-        history.add(
-          goto_programt::make_assignment(tmp_symbol, parameter, location));
-
-        // 3.4. Add a skip target
-        history.destructive_append(skip_program);
-      }
+  // speculatively insert a dummy, which will be replaced below if the insert
+  // actually happened
+  auto entry =
+    parameter2history.insert({parameter, symbol_exprt::typeless(ID_nil)});
 
-      expr = parameter2history[parameter];
-    }
-    else
-    {
-      throw invalid_source_file_exceptiont(
-        "Tracking history of " + id2string(parameter.id()) +
-          " expressions is not supported yet.",
-        expr.source_location());
-    }
+  if(entry.second)
+  {
+    // 1. Create a temporary symbol expression that represents the
+    // history variable
+    entry.first->second =
+      new_tmp_symbol(parameter.type(), location, mode, symbol_table)
+        .symbol_expr();
+
+    // 2. Add the required instructions to the instructions list
+    // 2.1. Declare the newly created temporary variable
+    history.add(goto_programt::make_decl(entry.first->second, location));
+
+    // 2.2. Skip storing the history if the expression is invalid
+    auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
+      not_exprt{
+        all_dereferences_are_valid(parameter, namespacet(symbol_table))},
+      location));
+
+    // 2.3. Add an assignment such that the value pointed to by the new
+    // temporary variable is equal to the value of the corresponding
+    // parameter
+    history.add(
+      goto_programt::make_assignment(entry.first->second, parameter, location));
+
+    // 2.4. Complete conditional jump for invalid-parameter case
+    auto label_instruction = history.add(goto_programt::make_skip(location));
+    goto_instruction->complete_goto(label_instruction);
   }
+
+  expr = entry.first->second;
+}
+
+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(
@@ -533,19 +558,12 @@ void generate_history_variables_initialization(
   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::unordered_map<exprt, symbol_exprt, irep_hash> 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.