Merge pull request #2251 from tautschnig/rename-cleanup

tautschnig · web-flow · commit 70da606569b4 · 2018-05-31T10:02:24.000+01:00
Cleanup of uses of get_new_name
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -36,7 +36,6 @@ Author: Matt Lewis
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/find_symbols.h>
-#include <util/rename.h>
 #include <util/simplify_expr.h>
 #include <util/replace_expr.h>
 #include <util/arith_tools.h>
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -36,7 +36,6 @@ Author: Matt Lewis
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/find_symbols.h>
-#include <util/rename.h>
 #include <util/simplify_expr.h>
 #include <util/replace_expr.h>
 #include <util/arith_tools.h>
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -33,7 +33,6 @@ Author: Matt Lewis
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/find_symbols.h>
-#include <util/rename.h>
 #include <util/simplify_expr.h>
 #include <util/replace_expr.h>
 #include <util/arith_tools.h>
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -36,7 +36,6 @@ Author: Matt Lewis
 #include <util/std_expr.h>
 #include <util/std_code.h>
 #include <util/find_symbols.h>
-#include <util/rename.h>
 #include <util/simplify_expr.h>
 #include <util/replace_expr.h>
 #include <util/arith_tools.h>
diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/fresh_symbol.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
-#include <util/rename.h>
 #include <util/cprover_prefix.h>
 
 #include <util/c_types.h>
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>
-#include <util/rename.h>
 
 #include <util/c_types.h>
 
@@ -669,7 +668,7 @@ void goto_convertt::convert_decl(
 
   const irep_idt &identifier=op0.get(ID_identifier);
 
-  const symbolt &symbol=lookup(identifier);
+  const symbolt &symbol = ns.lookup(identifier);
 
   if(symbol.is_static_lifetime ||
      symbol.type.id()==ID_code)
@@ -2059,26 +2058,6 @@ void goto_convertt::make_temp_symbol(
   expr=new_symbol.symbol_expr();
 }
 
-void goto_convertt::new_name(symbolt &symbol)
-{
-  // rename it
-  get_new_name(symbol, ns);
-
-  // store in symbol_table
-  symbol_table.add(symbol);
-}
-
-const symbolt &goto_convertt::lookup(const irep_idt &identifier)
-{
-  const symbolt *symbol;
-  if(ns.lookup(identifier, symbol))
-  {
-    error() << "failed to find symbol " << identifier << eom;
-    throw 0;
-  }
-  return *symbol;
-}
-
 void goto_convert(
   const codet &code,
   symbol_table_baset &symbol_table,
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
@@ -56,9 +56,6 @@ class goto_convertt:public messaget
   //
   // tools for symbols
   //
-  void new_name(symbolt &symbol);
-  const symbolt &lookup(const irep_idt &identifier);
-
   symbolt &new_tmp_symbol(
     const typet &type,
     const std::string &suffix,
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
@@ -147,7 +147,7 @@ void goto_convert_functionst::convert_function(
     return; // already converted
 
   // make tmp variables local to function
-  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
+  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
 
   f.type=to_code_type(symbol.type);
 
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
@@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_convert_class.h"
 
 #include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/std_expr.h>
-#include <util/rename.h>
-#include <util/cprover_prefix.h>
 #include <util/symbol.h>
 
 #include <util/c_types.h>
@@ -351,12 +351,6 @@ void goto_convertt::remove_function_call(
     return;
   }
 
-  auxiliary_symbolt new_symbol;
-
-  new_symbol.base_name="return_value";
-  new_symbol.type=expr.type();
-  new_symbol.location=expr.find_source_location();
-
   // get name of function, if available
 
   if(expr.id()!=ID_side_effect ||
@@ -374,25 +368,26 @@ void goto_convertt::remove_function_call(
     throw 0;
   }
 
+  std::string new_base_name = "return_value";
+  irep_idt new_symbol_mode = mode;
+
   if(expr.op0().id()==ID_symbol)
   {
     const irep_idt &identifier=expr.op0().get(ID_identifier);
-    const symbolt &symbol=lookup(identifier);
-
-    std::string new_base_name=id2string(new_symbol.base_name);
+    const symbolt &symbol = ns.lookup(identifier);
 
     new_base_name+='_';
     new_base_name+=id2string(symbol.base_name);
-    new_base_name += "$0";
-
-    new_symbol.base_name=new_base_name;
-    new_symbol.mode=symbol.mode;
+    new_symbol_mode = symbol.mode;
   }
 
-  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-
-  // ensure that the name is unique
-  new_name(new_symbol);
+  const symbolt &new_symbol = get_fresh_aux_symbol(
+    expr.type(),
+    tmp_symbol_prefix,
+    new_base_name,
+    expr.find_source_location(),
+    new_symbol_mode,
+    symbol_table);
 
   {
     code_declt decl;
@@ -432,15 +427,13 @@ void goto_convertt::remove_cpp_new(
 {
   codet call;
 
-  auxiliary_symbolt new_symbol;
-
-  new_symbol.base_name = "new_ptr$0";
-  new_symbol.type=expr.type();
-  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-  new_symbol.mode = ID_cpp;
-
-  // ensure that the name is unique
-  new_name(new_symbol);
+  const symbolt &new_symbol = get_fresh_aux_symbol(
+    expr.type(),
+    tmp_symbol_prefix,
+    "new_ptr",
+    expr.find_source_location(),
+    ID_cpp,
+    symbol_table);
 
   code_declt decl;
   decl.symbol()=new_symbol.symbol_expr();
@@ -486,19 +479,15 @@ void goto_convertt::remove_malloc(
 
   if(result_is_used)
   {
-    auxiliary_symbolt new_symbol;
-
-    new_symbol.base_name = "malloc_value$0";
-    new_symbol.type=expr.type();
-    new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-    new_symbol.location=expr.source_location();
-    new_symbol.mode = mode;
+    const symbolt &new_symbol = get_fresh_aux_symbol(
+      expr.type(),
+      tmp_symbol_prefix,
+      "malloc_value",
+      expr.source_location(),
+      mode,
+      symbol_table);
 
-    // ensure that the name is unique
-    new_name(new_symbol);
-
-    code_declt decl;
-    decl.symbol()=new_symbol.symbol_expr();
+    code_declt decl(new_symbol.symbol_expr());
     decl.add_source_location()=new_symbol.location;
     convert_decl(decl, dest, mode);
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
@@ -232,8 +232,6 @@ class goto_symext
 
   friend class symex_dereference_statet;
 
-  void new_name(symbolt &symbol, statet &state);
-
   // this does the following:
   // a) rename non-det choices
   // b) remove pointer dereferencing
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
-#include <util/rename.h>
 #include <util/std_expr.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
-#include <util/rename.h>
 #include <util/std_expr.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/std_expr.h>
-#include <util/rename.h>
 #include <util/symbol_table.h>
 #include <util/replace_symbol.h>
 #include <util/make_unique.h>
@@ -46,12 +45,6 @@ void goto_symext::symex_transition(
   state.source.pc=to;
 }
 
-void goto_symext::new_name(symbolt &symbol, statet &state)
-{
-  get_new_name(symbol, ns);
-  state.symbol_table.add(symbol);
-}
-
 void goto_symext::vcc(
   const exprt &vcc_expr,
   const std::string &msg,
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
@@ -24,11 +24,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/format_type.h>
+#include <util/fresh_symbol.h>
 #include <util/guard.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/rename.h>
 #include <util/ssa_expr.h>
 
 #include <ansi-c/c_typecast.h>
@@ -148,22 +148,19 @@ exprt value_set_dereferencet::dereference(
     else
     {
       // else: produce new symbol
-
-      symbolt symbol;
-      symbol.name="symex::invalid_object"+std::to_string(invalid_counter++);
-      symbol.base_name="invalid_object";
-      symbol.type=type;
-      symbol.mode = language_mode;
+      symbolt &symbol = get_fresh_aux_symbol(
+        type,
+        "symex",
+        "invalid_object",
+        pointer.source_location(),
+        language_mode,
+        new_symbol_table);
 
       // make it a lvalue, so we can assign to it
       symbol.is_lvalue=true;
 
-      get_new_name(symbol, ns);
-
       failure_value=symbol.symbol_expr();
       failure_value.set(ID_C_invalid_object, true);
-
-      new_symbol_table.insert(std::move(symbol));
     }
 
     valuet value;
