From 002e94bff657a195da0f2637bcbb7091e4770dcc Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 10 Feb 2017 13:41:12 +0000 Subject: [PATCH] Factor out fresh symbol generation This code was duplicated in quite a few places. --- src/goto-instrument/code_contracts.cpp | 22 +++--- src/goto-programs/goto_clean_expr.cpp | 28 ++++---- src/goto-programs/goto_convert.cpp | 24 +++---- src/goto-programs/goto_convert_class.h | 2 +- .../remove_function_pointers.cpp | 45 +++--------- src/goto-programs/remove_instanceof.cpp | 22 +++--- src/java_bytecode/java_object_factory.cpp | 72 +++++++++++-------- src/java_bytecode/java_object_factory.h | 2 + src/util/Makefile | 1 + src/util/fresh_symbol.cpp | 62 ++++++++++++++++ src/util/fresh_symbol.h | 27 +++++++ 11 files changed, 187 insertions(+), 120 deletions(-) create mode 100644 src/util/fresh_symbol.cpp create mode 100644 src/util/fresh_symbol.h diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index b82ecc35bd9..46914d78fb0 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -9,6 +9,7 @@ Date: February 2016 \*******************************************************************/ #include +#include #include #include @@ -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); } /*******************************************************************\ diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 9b5b44a44d9..c7fa8637194 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include @@ -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); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index a3124f3b898..293e2ca8571 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -2674,24 +2675,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; } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index feab8197046..997ca676f63 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/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") { } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index b5dac445fda..3893729a1e1 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -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 &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; diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index ee7f5979332..3fc2699ef47 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -9,6 +9,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "class_hierarchy.h" #include "class_identifier.h" #include "remove_instanceof.h" +#include #include @@ -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(); diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index b23e419d216..088a25f7038 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -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,8 +409,11 @@ 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; @@ -409,8 +421,11 @@ void java_object_factoryt::gen_nondet_array_init( // 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(); diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index d111948e365..6122d3e2780 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -38,6 +38,8 @@ exprt get_nondet_bool(const typet &); symbolt &new_tmp_symbol( symbol_tablet &symbol_table, + const source_locationt &, + const typet &, const std::string &prefix="tmp_object_factory"); #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/src/util/Makefile b/src/util/Makefile index 6cc42a18fb8..fefabaed3af 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -22,6 +22,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \ memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \ ssa_expr.cpp json_irep.cpp json_expr.cpp \ + fresh_symbol.cpp \ string_utils.cpp INCLUDES= -I .. diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp new file mode 100644 index 00000000000..fbe6f09b871 --- /dev/null +++ b/src/util/fresh_symbol.cpp @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Fresh auxiliary symbol creation + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#include "fresh_symbol.h" + +/*******************************************************************\ + +Function: get_fresh_aux_symbol + + Inputs: `type`: type of new symbol + `name_prefix`, `basename_prefix`: + new symbol will be named name_prefix::basename_prefix$num + unless name_prefix is empty, in which case the :: prefix + is omitted. + `source_location`: new symbol source loc + `symbol_mode`: new symbol mode + `symbol_table`: table to add the new symbol to + + Outputs: + + Purpose: Installs a fresh-named symbol with the requested name pattern + +\*******************************************************************/ + +symbolt &get_fresh_aux_symbol( + const typet &type, + const std::string &name_prefix, + const std::string &basename_prefix, + const source_locationt &source_location, + const irep_idt &symbol_mode, + symbol_tablet &symbol_table) +{ + static size_t temporary_counter=0; + auxiliary_symbolt new_symbol; + symbolt *symbol_ptr; + + do + { + new_symbol.base_name= + basename_prefix+ + "$"+ + std::to_string(++temporary_counter); + if(name_prefix.empty()) + new_symbol.name=new_symbol.base_name; + else + new_symbol.name= + name_prefix+ + "::"+ + id2string(new_symbol.base_name); + new_symbol.type=type; + new_symbol.location=source_location; + new_symbol.mode=symbol_mode; + } + while(symbol_table.move(new_symbol, symbol_ptr)); + + return *symbol_ptr; +} diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h new file mode 100644 index 00000000000..c3b2749cbe3 --- /dev/null +++ b/src/util/fresh_symbol.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Fresh auxiliary symbol creation + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_FRESH_SYMBOL_H +#define CPROVER_UTIL_FRESH_SYMBOL_H + +#include + +#include +#include +#include +#include + +symbolt &get_fresh_aux_symbol( + const typet &type, + const std::string &name_prefix, + const std::string &basename_prefix, + const source_locationt &source_location, + const irep_idt &symbol_mode, + symbol_tablet &symbol_table); + +#endif // CPROVER_UTIL_FRESH_SYMBOL_H