replace_history_parametert: use an unordered map to symbol_exprt

There are no ordering requirements here, so we can benefit from O(1)
amortised cost. Also, the value type is always a `symbol_exprt`, not
just a generic `exprt`.

Author: tautschnig

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,
@@ -605,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,
@@ -681,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

@@ -453,7 +453,7 @@ void add_quantified_variable(
 static void replace_history_parameter_rec(
   symbol_table_baset &symbol_table,
   exprt &expr,
-  std::map<exprt, exprt> &parameter2history,
+  std::unordered_map<exprt, symbol_exprt, irep_hash> &parameter2history,
   const source_locationt &location,
   const irep_idt &mode,
   goto_programt &history,
@@ -492,7 +492,7 @@ static void replace_history_parameter_rec(
 
         // 2. Associate the above temporary variable to it's corresponding
         // expression
-        parameter2history[parameter] = tmp_symbol;
+        it = parameter2history.emplace(parameter, tmp_symbol).first;
 
         // 3. Add the required instructions to the instructions list
         // 3.1. Declare the newly created temporary variable
@@ -515,7 +515,7 @@ static void replace_history_parameter_rec(
         history.destructive_append(skip_program);
       }
 
-      expr = parameter2history[parameter];
+      expr = it->second;
     }
     else
     {

src/goto-instrument/contracts/utils.h

@@ -245,7 +245,7 @@ void add_quantified_variable(
 struct replace_history_parametert
 {
   exprt expression_after_replacement;
-  std::map<exprt, exprt> parameter_to_history;
+  std::unordered_map<exprt, symbol_exprt, irep_hash> parameter_to_history;
   goto_programt history_construction;
 };