Merge pull request #7721 from tautschnig/cleanup/contracts-symbol-create

Code contracts: cleanup get_fresh_aux_symbol wrappers

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -139,12 +139,13 @@ void code_contractst::check_apply_loop_contracts(
   // Create a temporary to track if we entered the loop,
   // i.e., the loop guard was satisfied.
   const auto entered_loop =
-    new_tmp_symbol(
+    get_fresh_aux_symbol(
       bool_typet(),
+      id2string(loop_head_location.get_function()),
+      std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number),
       loop_head_location,
       mode,
-      symbol_table,
-      std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number))
+      symbol_table)
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(entered_loop, loop_head_location));
@@ -154,8 +155,13 @@ void code_contractst::check_apply_loop_contracts(
   // Create a snapshot of the invariant so that we can check the base case,
   // if the loop is not vacuous and must be abstracted with contracts.
   const auto initial_invariant_val =
-    new_tmp_symbol(
-      bool_typet(), loop_head_location, mode, symbol_table, INIT_INVARIANT)
+    get_fresh_aux_symbol(
+      bool_typet(),
+      id2string(loop_head_location.get_function()),
+      INIT_INVARIANT,
+      loop_head_location,
+      mode,
+      symbol_table)
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(initial_invariant_val, loop_head_location));
@@ -173,10 +179,14 @@ void code_contractst::check_apply_loop_contracts(
 
   // Create a temporary variable to track base case vs inductive case
   // instrumentation of the loop.
-  const auto in_base_case =
-    new_tmp_symbol(
-      bool_typet(), loop_head_location, mode, symbol_table, "__in_base_case")
-      .symbol_expr();
+  const auto in_base_case = get_fresh_aux_symbol(
+                              bool_typet(),
+                              id2string(loop_head_location.get_function()),
+                              "__in_base_case",
+                              loop_head_location,
+                              mode,
+                              symbol_table)
+                              .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(in_base_case, loop_head_location));
   pre_loop_head_instrs.add(
@@ -298,12 +308,13 @@ void code_contractst::check_apply_loop_contracts(
   // havoc (assigns_set);
   // ASSIGN in_loop_havoc_block = false;
   const auto in_loop_havoc_block =
-    new_tmp_symbol(
+    get_fresh_aux_symbol(
       bool_typet(),
+      id2string(loop_head_location.get_function()),
+      std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number),
       loop_head_location,
       mode,
-      symbol_table,
-      std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number))
+      symbol_table)
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
@@ -335,14 +346,26 @@ void code_contractst::check_apply_loop_contracts(
   for(const auto &clause : decreases_clause.operands())
   {
     const auto old_decreases_var =
-      new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table)
+      get_fresh_aux_symbol(
+        clause.type(),
+        id2string(loop_head_location.get_function()),
+        "tmp_cc",
+        loop_head_location,
+        mode,
+        symbol_table)
         .symbol_expr();
     pre_loop_head_instrs.add(
       goto_programt::make_decl(old_decreases_var, loop_head_location));
     old_decreases_vars.push_back(old_decreases_var);
 
     const auto new_decreases_var =
-      new_tmp_symbol(clause.type(), loop_head_location, mode, symbol_table)
+      get_fresh_aux_symbol(
+        clause.type(),
+        id2string(loop_head_location.get_function()),
+        "tmp_cc",
+        loop_head_location,
+        mode,
+        symbol_table)
         .symbol_expr();
     pre_loop_head_instrs.add(
       goto_programt::make_decl(new_decreases_var, loop_head_location));
@@ -1251,8 +1274,10 @@ void code_contractst::add_contract_check(
   optionalt<code_returnt> return_stmt;
   if(code_type.return_type() != empty_typet())
   {
-    symbol_exprt r = new_tmp_symbol(
+    symbol_exprt r = get_fresh_aux_symbol(
                        code_type.return_type(),
+                       id2string(source_location.get_function()),
+                       "tmp_cc",
                        source_location,
                        function_symbol.mode,
                        symbol_table)
@@ -1275,8 +1300,10 @@ void code_contractst::add_contract_check(
   {
     PRECONDITION(!parameter.empty());
     const symbolt &parameter_symbol = ns.lookup(parameter);
-    symbol_exprt p = new_tmp_symbol(
+    symbol_exprt p = get_fresh_aux_symbol(
                        parameter_symbol.type,
+                       id2string(source_location.get_function()),
+                       "tmp_cc",
                        source_location,
                        parameter_symbol.mode,
                        symbol_table)

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

@@ -471,30 +471,22 @@ static dfcc_loop_infot gen_dfcc_loop_info(
 
   auto &loop = loop_nesting_graph[loop_id];
   const auto cbmc_loop_number = loop.latch->loop_number;
-  const auto &language_mode =
-    dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
 
   // Generate "write set" variable
-  const auto &write_set_var =
-    get_fresh_aux_symbol(
-      library.dfcc_type[dfcc_typet::WRITE_SET],
-      id2string(function_id),
-      "__write_set_loop_" + std::to_string(cbmc_loop_number),
-      loop.head->source_location(),
-      language_mode,
-      symbol_table)
-      .symbol_expr();
+  const auto write_set_var = dfcc_utilst::create_symbol(
+    symbol_table,
+    library.dfcc_type[dfcc_typet::WRITE_SET],
+    function_id,
+    "__write_set_loop_" + std::to_string(cbmc_loop_number),
+    loop.head->source_location());
 
   // Generate "address of write set" variable
-  const auto &addr_of_write_set_var =
-    get_fresh_aux_symbol(
-      library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
-      id2string(function_id),
-      "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
-      loop.head->source_location(),
-      language_mode,
-      symbol_table)
-      .symbol_expr();
+  const auto &addr_of_write_set_var = dfcc_utilst::create_symbol(
+    symbol_table,
+    library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
+    function_id,
+    "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
+    loop.head->source_location());
 
   return {
     loop_id,

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

@@ -256,16 +256,12 @@ void dfcc_instrumentt::instrument_harness_function(
   // create a local write set symbol
   const auto &function_symbol =
     dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
-  const auto &write_set = dfcc_utilst::create_symbol(
-                            goto_model.symbol_table,
-                            library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
-                            function_id,
-                            "__write_set_to_check",
-                            function_symbol.location,
-                            function_symbol.mode,
-                            function_symbol.module,
-                            false)
-                            .symbol_expr();
+  const auto write_set = dfcc_utilst::create_symbol(
+    goto_model.symbol_table,
+    library.dfcc_type[dfcc_typet::WRITE_SET_PTR],
+    function_id,
+    "__write_set_to_check",
+    function_symbol.location);
 
   std::set<symbol_exprt> local_statics = get_local_statics(function_id);
 
@@ -663,7 +659,7 @@ void dfcc_instrumentt::instrument_lhs(
   goto_programt &goto_program,
   dfcc_cfg_infot &cfg_info)
 {
-  const auto &mode =
+  const irep_idt &mode =
     dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
 
   goto_programt payload;
@@ -691,18 +687,12 @@ void dfcc_instrumentt::instrument_lhs(
     // ASSIGN lhs := rhs;
     // ```
 
-    auto &check_sym = dfcc_utilst::create_symbol(
+    const auto check_var = dfcc_utilst::create_symbol(
       goto_model.symbol_table,
       bool_typet(),
-      id2string(function_id),
+      function_id,
       "__check_lhs_assignment",
-      lhs_source_location,
-      mode,
-      dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
-        .module,
-      false);
-
-    const auto &check_var = check_sym.symbol_expr();
+      lhs_source_location);
 
     payload.add(goto_programt::make_decl(check_var, lhs_source_location));
 
@@ -950,22 +940,17 @@ void dfcc_instrumentt::instrument_deallocate_call(
   // ----
   // CALL __CPROVER_deallocate(ptr);
   // ```
-  const auto &mode =
-    dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
   goto_programt payload;
 
   auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
     dfcc_utilst::make_null_check_expr(write_set), target_location));
 
-  auto &check_sym = get_fresh_aux_symbol(
+  const auto check_var = dfcc_utilst::create_symbol(
+    goto_model.symbol_table,
     bool_typet(),
-    id2string(function_id),
+    function_id,
     "__check_deallocate",
-    target_location,
-    mode,
-    goto_model.symbol_table);
-
-  const auto &check_var = check_sym.symbol_expr();
+    target_location);
 
   payload.add(goto_programt::make_decl(check_var, target_location));
 
@@ -977,6 +962,8 @@ void dfcc_instrumentt::instrument_deallocate_call(
     target_location));
 
   // add property class on assertion source_location
+  const irep_idt &mode =
+    dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
   source_locationt check_location(target_location);
   check_location.set_property_class("frees");
   std::string comment =
@@ -1040,6 +1027,8 @@ void dfcc_instrumentt::instrument_other(
   const auto &target_location = target->source_location();
   auto &statement = target->get_other().get_statement();
   auto &write_set = cfg_info.get_write_set(target);
+  const irep_idt &mode =
+    dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
 
   if(statement == ID_array_set || statement == ID_array_copy)
   {
@@ -1054,23 +1043,17 @@ void dfcc_instrumentt::instrument_other(
     // ----
     // OTHER {statement = array_set, args = {dest, value}};
     // ```
-    const auto &mode =
-      dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
-        .mode;
     goto_programt payload;
 
     auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
       dfcc_utilst::make_null_check_expr(write_set), target_location));
 
-    auto &check_sym = get_fresh_aux_symbol(
+    const auto check_var = dfcc_utilst::create_symbol(
+      goto_model.symbol_table,
       bool_typet(),
-      id2string(function_id),
+      function_id,
       is_array_set ? "__check_array_set" : "__check_array_copy",
-      target_location,
-      mode,
-      goto_model.symbol_table);
-
-    const auto &check_var = check_sym.symbol_expr();
+      target_location);
 
     payload.add(goto_programt::make_decl(check_var, target_location));
 
@@ -1115,23 +1098,17 @@ void dfcc_instrumentt::instrument_other(
     // ----
     // OTHER {statement = array_replace, args = {dest, src}};
     // ```
-    const auto &mode =
-      dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
-        .mode;
     goto_programt payload;
 
     auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
       dfcc_utilst::make_null_check_expr(write_set), target_location));
 
-    auto &check_sym = get_fresh_aux_symbol(
+    const auto check_var = dfcc_utilst::create_symbol(
+      goto_model.symbol_table,
       bool_typet(),
-      id2string(function_id),
+      function_id,
       "__check_array_replace",
-      target_location,
-      mode,
-      goto_model.symbol_table);
-
-    const auto &check_var = check_sym.symbol_expr();
+      target_location);
 
     payload.add(goto_programt::make_decl(check_var, target_location));
 
@@ -1170,23 +1147,17 @@ void dfcc_instrumentt::instrument_other(
     // ASSERT(check_havoc_object);
     // DEAD check_havoc_object;
     // ```
-    const auto &mode =
-      dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
-        .mode;
     goto_programt payload;
 
     auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
       dfcc_utilst::make_null_check_expr(write_set), target_location));
 
-    auto &check_sym = get_fresh_aux_symbol(
+    const auto check_var = dfcc_utilst::create_symbol(
+      goto_model.symbol_table,
       bool_typet(),
-      id2string(function_id),
+      function_id,
       "__check_havoc_object",
-      target_location,
-      mode,
-      goto_model.symbol_table);
-
-    const auto &check_var = check_sym.symbol_expr();
+      target_location);
 
     payload.add(goto_programt::make_decl(check_var, target_location));