Merge pull request #523 from smowton/factor_fresh_symbol

Factor out fresh symbol generation

Author: Daniel Kroening

src/goto-instrument/code_contracts.cpp

@@ -9,6 +9,7 @@ Date: February 2016
 \*******************************************************************/
 
 #include <util/cprover_prefix.h>
+#include <util/fresh_symbol.h>
 #include <util/replace_symbol.h>
 
 #include <goto-programs/remove_skip.h>
@@ -291,20 +292,13 @@ const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
   const source_locationt &source_location)
 {
-  auxiliary_symbolt new_symbol;
-  new_symbol.type=type;
-  new_symbol.location=source_location;
-
-  symbolt *symbol_ptr;
-
-  do
-  {
-    new_symbol.base_name="tmp_cc$"+std::to_string(++temporary_counter);
-    new_symbol.name=new_symbol.base_name;
-  }
-  while(symbol_table.move(new_symbol, symbol_ptr));
-
-  return *symbol_ptr;
+  return get_fresh_aux_symbol(
+    type,
+    "",
+    "tmp_cc",
+    source_location,
+    irep_idt(),
+    symbol_table);
 }
 
 /*******************************************************************\

src/goto-programs/goto_clean_expr.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/fresh_symbol.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/rename.h>
@@ -33,24 +34,21 @@ symbol_exprt goto_convertt::make_compound_literal(
 {
   const source_locationt source_location=expr.find_source_location();
 
-  auxiliary_symbolt new_symbol;
-  symbolt *symbol_ptr;
-
-  do
-  {
-    new_symbol.base_name="literal$"+std::to_string(++temporary_counter);
-    new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-    new_symbol.is_static_lifetime=source_location.get_function().empty();
-    new_symbol.value=expr;
-    new_symbol.type=expr.type();
-    new_symbol.location=source_location;
-  }
-  while(symbol_table.move(new_symbol, symbol_ptr));
+  symbolt &new_symbol=
+    get_fresh_aux_symbol(
+      expr.type(),
+      tmp_symbol_prefix,
+      "literal",
+      source_location,
+      irep_idt(),
+      symbol_table);
+  new_symbol.is_static_lifetime=source_location.get_function().empty();
+  new_symbol.value=expr;
 
   // The value might depend on a variable, thus
   // generate code for this.
 
-  symbol_exprt result=symbol_ptr->symbol_expr();
+  symbol_exprt result=new_symbol.symbol_expr();
   result.add_source_location()=source_location;
 
   // The lifetime of compound literals is really that of
@@ -62,7 +60,7 @@ symbol_exprt goto_convertt::make_compound_literal(
   convert(code_assign, dest);
 
   // now create a 'dead' instruction
-  if(!symbol_ptr->is_static_lifetime)
+  if(!new_symbol.is_static_lifetime)
   {
     code_deadt code_dead(result);
     targets.destructor_stack.push_back(code_dead);

src/goto-programs/goto_convert.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -2754,24 +2755,21 @@ symbolt &goto_convertt::new_tmp_symbol(
   goto_programt &dest,
   const source_locationt &source_location)
 {
-  auxiliary_symbolt new_symbol;
-  symbolt *symbol_ptr;
-
-  do
-  {
-    new_symbol.base_name="tmp_"+suffix+"$"+std::to_string(++temporary_counter);
-    new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-    new_symbol.type=type;
-    new_symbol.location=source_location;
-  }
-  while(symbol_table.move(new_symbol, symbol_ptr));
+  symbolt &new_symbol=
+    get_fresh_aux_symbol(
+      type,
+      tmp_symbol_prefix,
+      "tmp_"+suffix,
+      source_location,
+      irep_idt(),
+      symbol_table);
 
   code_declt decl;
-  decl.symbol()=symbol_ptr->symbol_expr();
+  decl.symbol()=new_symbol.symbol_expr();
   decl.add_source_location()=source_location;
   convert_decl(decl, dest);
 
-  return *symbol_ptr;
+  return new_symbol;
 }
 
 /*******************************************************************\

src/goto-programs/goto_convert_class.h

@@ -32,7 +32,7 @@ class goto_convertt:public messaget
     symbol_table(_symbol_table),
     ns(_symbol_table),
     temporary_counter(0),
-    tmp_symbol_prefix("goto_convertt::")
+    tmp_symbol_prefix("goto_convertt")
   {
   }
 

src/goto-programs/remove_function_pointers.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
+#include <util/fresh_symbol.h>
 #include <util/replace_expr.h>
 #include <util/source_location.h>
 #include <util/std_expr.h>
@@ -68,8 +69,6 @@ class remove_function_pointerst
     code_function_callt &function_call,
     goto_programt &dest);
 
-  symbolt &new_tmp_symbol();
-
   void compute_address_taken_in_symbols(
     std::set<irep_idt> &address_taken)
   {
@@ -110,37 +109,6 @@ remove_function_pointerst::remove_function_pointerst(
 
 /*******************************************************************\
 
-Function: remove_function_pointerst::new_tmp_symbol
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-symbolt &remove_function_pointerst::new_tmp_symbol()
-{
-  static int temporary_counter;
-
-  auxiliary_symbolt new_symbol;
-  symbolt *symbol_ptr;
-
-  do
-  {
-    new_symbol.base_name=
-      "tmp_return_val$"+std::to_string(++temporary_counter);
-    new_symbol.name=
-      "remove_function_pointers::"+id2string(new_symbol.base_name);
-  }
-  while(symbol_table.move(new_symbol, symbol_ptr));
-
-  return *symbol_ptr;
-}
-
-/*******************************************************************\
-
 Function: remove_function_pointerst::arg_is_type_compatible
 
   Inputs:
@@ -311,9 +279,14 @@ void remove_function_pointerst::fix_return_type(
        code_type.return_type(), ns))
     return;
 
-  symbolt &tmp_symbol=new_tmp_symbol();
-  tmp_symbol.type=code_type.return_type();
-  tmp_symbol.location=function_call.source_location();
+  symbolt &tmp_symbol=
+    get_fresh_aux_symbol(
+      code_type.return_type(),
+      "remove_function_pointers",
+      "tmp_return_val",
+      function_call.source_location(),
+      irep_idt(),
+      symbol_table);
 
   symbol_exprt tmp_symbol_expr;
   tmp_symbol_expr.type()=tmp_symbol.type;

src/goto-programs/remove_instanceof.cpp

@@ -9,6 +9,7 @@ Author: Chris Smowton, [email protected]
 #include "class_hierarchy.h"
 #include "class_identifier.h"
 #include "remove_instanceof.h"
+#include <util/fresh_symbol.h>
 
 #include <sstream>
 
@@ -20,8 +21,7 @@ class remove_instanceoft
     goto_functionst &_goto_functions):
     symbol_table(_symbol_table),
     ns(_symbol_table),
-    goto_functions(_goto_functions),
-    lowered_count(0)
+    goto_functions(_goto_functions)
   {
     class_hierarchy(_symbol_table);
   }
@@ -34,7 +34,6 @@ class remove_instanceoft
   namespacet ns;
   class_hierarchyt class_hierarchy;
   goto_functionst &goto_functions;
-  int lowered_count;
 
   bool lower_instanceof(goto_programt &);
 
@@ -128,15 +127,14 @@ void remove_instanceoft::lower_instanceof(
     symbol_typet jlo("java::java.lang.Object");
     exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
 
-    std::ostringstream symname;
-    symname << "instanceof_tmp::instanceof_tmp" << (++lowered_count);
-    auxiliary_symbolt newsym;
-    newsym.name=symname.str();
-    newsym.type=object_clsid.type();
-    newsym.base_name=newsym.name;
-    newsym.mode=ID_java;
-    newsym.is_type=false;
-    assert(!symbol_table.add(newsym));
+    symbolt &newsym=
+      get_fresh_aux_symbol(
+        object_clsid.type(),
+        "instanceof_tmp",
+        "instanceof_tmp",
+        source_locationt(),
+        ID_java,
+        symbol_table);
 
     auto newinst=goto_program.insert_after(this_inst);
     newinst->make_assignment();

src/java_bytecode/java_object_factory.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 
 #include <util/arith_tools.h>
+#include <util/fresh_symbol.h>
 #include <util/std_types.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -107,8 +108,7 @@ exprt java_object_factoryt::allocate_object(
   bool cast_needed=allocate_type_resolved!=target_type;
   if(!create_dynamic_objects)
   {
-    symbolt &aux_symbol=new_tmp_symbol(symbol_table);
-    aux_symbol.type=allocate_type;
+    symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type);
     aux_symbol.is_static_lifetime=true;
 
     exprt object=aux_symbol.symbol_expr();
@@ -136,8 +136,11 @@ exprt java_object_factoryt::allocate_object(
       // Create a symbol for the malloc expression so we can initialize
       // without having to do it potentially through a double-deref, which
       // breaks the to-SSA phase.
-      symbolt &malloc_sym=new_tmp_symbol(symbol_table, "malloc_site");
-      malloc_sym.type=pointer_typet(allocate_type);
+      symbolt &malloc_sym=new_tmp_symbol(
+        symbol_table,
+        loc,
+        pointer_typet(allocate_type),
+        "malloc_site");
       code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
       code_assignt &malloc_assign=assign;
       malloc_assign.add_source_location()=loc;
@@ -211,8 +214,11 @@ void java_object_factoryt::gen_nondet_init(
     if(!assume_non_null)
     {
       auto returns_null_sym=
-        new_tmp_symbol(symbol_table, "opaque_returns_null");
-      returns_null_sym.type=c_bool_typet(1);
+        new_tmp_symbol(
+          symbol_table,
+          loc,
+          c_bool_typet(1),
+          "opaque_returns_null");
       auto returns_null=returns_null_sym.symbol_expr();
       auto assign_returns_null=
           code_assignt(returns_null, get_nondet_bool(returns_null_sym.type));
@@ -365,8 +371,11 @@ void java_object_factoryt::gen_nondet_array_init(
   auto max_length_expr=from_integer(max_nondet_array_length, java_int_type());
 
   typet allocate_type;
-  symbolt &length_sym=new_tmp_symbol(symbol_table, "nondet_array_length");
-  length_sym.type=java_int_type();
+  symbolt &length_sym=new_tmp_symbol(
+    symbol_table,
+    loc,
+    java_int_type(),
+    "nondet_array_length");
   const auto &length_sym_expr=length_sym.symbol_expr();
 
   // Initialize array with some undetermined length:
@@ -400,17 +409,23 @@ void java_object_factoryt::gen_nondet_array_init(
 
   // Interpose a new symbol, as the goto-symex stage can't handle array indexing
   // via a cast.
-  symbolt &array_init_symbol=new_tmp_symbol(symbol_table, "array_data_init");
-  array_init_symbol.type=init_array_expr.type();
+  symbolt &array_init_symbol=new_tmp_symbol(
+    symbol_table,
+    loc,
+    init_array_expr.type(),
+    "array_data_init");
   const auto &array_init_symexpr=array_init_symbol.symbol_expr();
   codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
   data_assign.add_source_location()=loc;
   init_code.copy_to_operands(data_assign);
 
   // Emit init loop for(array_init_iter=0; array_init_iter!=array.length;
   //                  ++array_init_iter) init(array[array_init_iter]);
-  symbolt &counter=new_tmp_symbol(symbol_table, "array_init_iter");
-  counter.type=length_sym_expr.type();
+  symbolt &counter=new_tmp_symbol(
+    symbol_table,
+    loc,
+    length_sym_expr.type(),
+    "array_init_iter");
   exprt counter_expr=counter.symbol_expr();
 
   exprt java_zero=from_integer(0, java_int_type());
@@ -512,22 +527,19 @@ Function: new_tmp_symbol
 
 \*******************************************************************/
 
-symbolt &new_tmp_symbol(symbol_tablet &symbol_table, const std::string &prefix)
+symbolt &new_tmp_symbol(
+  symbol_tablet &symbol_table,
+  const source_locationt &loc,
+  const typet &type,
+  const std::string &prefix)
 {
-  static size_t temporary_counter=0; // TODO encapsulate as class variable
-
-  auxiliary_symbolt new_symbol;
-  symbolt *symbol_ptr;
-
-  do
-  {
-    new_symbol.name="tmp_object_factory$"+std::to_string(++temporary_counter);
-    new_symbol.base_name=new_symbol.name;
-    new_symbol.mode=ID_java;
-  }
-  while(symbol_table.move(new_symbol, symbol_ptr));
-
-  return *symbol_ptr;
+  return get_fresh_aux_symbol(
+    type,
+    "",
+    prefix,
+    loc,
+    ID_java,
+    symbol_table);
 }
 
 /*******************************************************************\
@@ -572,8 +584,10 @@ exprt object_factory(
 {
   if(type.id()==ID_pointer)
   {
-    symbolt &aux_symbol=new_tmp_symbol(symbol_table);
-    aux_symbol.type=type;
+    symbolt &aux_symbol=new_tmp_symbol(
+      symbol_table,
+      loc,
+      type);
     aux_symbol.is_static_lifetime=true;
 
     exprt object=aux_symbol.symbol_expr();