From efe922e0ec26aa1255ef7fcd3ac281153b05ac4a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 Aug 2017 15:17:32 +0100 Subject: [PATCH 1/2] factor out goto model linking into separate file --- src/goto-programs/Makefile | 1 + src/goto-programs/link_goto_model.cpp | 180 +++++++++++++++++++++++++ src/goto-programs/link_goto_model.h | 23 ++++ src/goto-programs/read_goto_binary.cpp | 180 ++++--------------------- 4 files changed, 228 insertions(+), 156 deletions(-) create mode 100644 src/goto-programs/link_goto_model.cpp create mode 100644 src/goto-programs/link_goto_model.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index c7e2f264cf2..b164beef079 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -26,6 +26,7 @@ SRC = basic_blocks.cpp \ interpreter.cpp \ interpreter_evaluate.cpp \ json_goto_trace.cpp \ + link_goto_model.cpp \ link_to_library.cpp \ loop_ids.cpp \ mm_io.cpp \ diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp new file mode 100644 index 00000000000..6b40fd7173a --- /dev/null +++ b/src/goto-programs/link_goto_model.cpp @@ -0,0 +1,180 @@ +/*******************************************************************\ + +Module: Link Goto Programs + +Author: Michael Tautschnig, Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Link Goto Programs + +#include "link_goto_model.h" + +#include + +#include +#include +#include + +#include + +#include "goto_model.h" + +static void rename_symbols_in_function( + goto_functionst::goto_functiont &function, + const rename_symbolt &rename_symbol) +{ + goto_programt &program=function.body; + rename_symbol(function.type); + + Forall_goto_program_instructions(iit, program) + { + rename_symbol(iit->code); + rename_symbol(iit->guard); + } +} + +/// Link a set of goto functions, considering weak symbols +/// and symbol renaming +static bool link_functions( + symbol_tablet &dest_symbol_table, + goto_functionst &dest_functions, + const symbol_tablet &src_symbol_table, + goto_functionst &src_functions, + const rename_symbolt &rename_symbol, + const std::unordered_set &weak_symbols, + const replace_symbolt &object_type_updates) +{ + namespacet ns(dest_symbol_table); + namespacet src_ns(src_symbol_table); + + // merge functions + Forall_goto_functions(src_it, src_functions) + { + // the function might have been renamed + rename_symbolt::expr_mapt::const_iterator e_it= + rename_symbol.expr_map.find(src_it->first); + + irep_idt final_id=src_it->first; + + if(e_it!=rename_symbol.expr_map.end()) + final_id=e_it->second; + + // already there? + goto_functionst::function_mapt::iterator dest_f_it= + dest_functions.function_map.find(final_id); + + if(dest_f_it==dest_functions.function_map.end()) // not there yet + { + rename_symbols_in_function(src_it->second, rename_symbol); + + goto_functionst::goto_functiont &in_dest_symbol_table= + dest_functions.function_map[final_id]; + + in_dest_symbol_table.body.swap(src_it->second.body); + in_dest_symbol_table.type=src_it->second.type; + } + else // collision! + { + goto_functionst::goto_functiont &in_dest_symbol_table= + dest_functions.function_map[final_id]; + + goto_functionst::goto_functiont &src_func=src_it->second; + + if(in_dest_symbol_table.body.instructions.empty() || + weak_symbols.find(final_id)!=weak_symbols.end()) + { + // the one with body wins! + rename_symbols_in_function(src_func, rename_symbol); + + in_dest_symbol_table.body.swap(src_func.body); + in_dest_symbol_table.type=src_func.type; + } + else if(src_func.body.instructions.empty() || + src_ns.lookup(src_it->first).is_weak) + { + // just keep the old one in dest + } + else if(in_dest_symbol_table.type.get_bool(ID_C_inlined)) + { + // ok, we silently ignore + } + else + { + // the linking code will have ensured that types match + rename_symbol(src_func.type); + assert(base_type_eq(in_dest_symbol_table.type, src_func.type, ns)); + } + } + } + + // apply macros + rename_symbolt macro_application; + + forall_symbols(it, dest_symbol_table.symbols) + if(it->second.is_macro && !it->second.is_type) + { + const symbolt &symbol=it->second; + + assert(symbol.value.id()==ID_symbol); + const irep_idt &id=to_symbol_expr(symbol.value).get_identifier(); + + #if 0 + if(!base_type_eq(symbol.type, ns.lookup(id).type, ns)) + { + std::cerr << symbol << '\n'; + std::cerr << ns.lookup(id) << '\n'; + } + assert(base_type_eq(symbol.type, ns.lookup(id).type, ns)); + #endif + + macro_application.insert_expr(symbol.name, id); + } + + if(!macro_application.expr_map.empty()) + Forall_goto_functions(dest_it, dest_functions) + rename_symbols_in_function(dest_it->second, macro_application); + + if(!object_type_updates.expr_map.empty()) + { + Forall_goto_functions(dest_it, dest_functions) + Forall_goto_program_instructions(iit, dest_it->second.body) + { + object_type_updates(iit->code); + object_type_updates(iit->guard); + } + } + + return false; +} + +void link_goto_model( + goto_modelt &dest, + goto_modelt &src, + message_handlert &message_handler) +{ + typedef std::unordered_set id_sett; + id_sett weak_symbols; + + forall_symbols(it, dest.symbol_table.symbols) + if(it->second.is_weak) + weak_symbols.insert(it->first); + + linkingt linking(dest.symbol_table, + src.symbol_table, + message_handler); + + if(linking.typecheck_main()) + throw 0; + + if(link_functions( + dest.symbol_table, + dest.goto_functions, + src.symbol_table, + src.goto_functions, + linking.rename_symbol, + weak_symbols, + linking.object_type_updates)) + throw 0; +} diff --git a/src/goto-programs/link_goto_model.h b/src/goto-programs/link_goto_model.h new file mode 100644 index 00000000000..e04b85727e9 --- /dev/null +++ b/src/goto-programs/link_goto_model.h @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Read Goto Programs + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Read Goto Programs + +#ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H +#define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H + +class goto_modelt; +class message_handlert; + +void link_goto_model( + goto_modelt &dest, + goto_modelt &src, + message_handlert &); + +#endif // CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 58eafda8fb2..2b4a3805401 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -32,9 +32,8 @@ Module: Read Goto Programs #include -#include - #include "goto_model.h" +#include "link_goto_model.h" #include "read_bin_goto_object.h" #include "elf_reader.h" #include "osx_fat_reader.h" @@ -214,139 +213,12 @@ bool is_goto_binary(const std::string &filename) return false; } -static void rename_symbols_in_function( - goto_functionst::goto_functiont &function, - const rename_symbolt &rename_symbol) -{ - goto_programt &program=function.body; - rename_symbol(function.type); - - Forall_goto_program_instructions(iit, program) - { - rename_symbol(iit->code); - rename_symbol(iit->guard); - } -} - -static bool link_functions( - symbol_tablet &dest_symbol_table, - goto_functionst &dest_functions, - const symbol_tablet &src_symbol_table, - goto_functionst &src_functions, - const rename_symbolt &rename_symbol, - const std::unordered_set &weak_symbols, - const replace_symbolt &object_type_updates) -{ - namespacet ns(dest_symbol_table); - namespacet src_ns(src_symbol_table); - - // merge functions - Forall_goto_functions(src_it, src_functions) - { - // the function might have been renamed - rename_symbolt::expr_mapt::const_iterator e_it= - rename_symbol.expr_map.find(src_it->first); - - irep_idt final_id=src_it->first; - - if(e_it!=rename_symbol.expr_map.end()) - final_id=e_it->second; - - // already there? - goto_functionst::function_mapt::iterator dest_f_it= - dest_functions.function_map.find(final_id); - - if(dest_f_it==dest_functions.function_map.end()) // not there yet - { - rename_symbols_in_function(src_it->second, rename_symbol); - - goto_functionst::goto_functiont &in_dest_symbol_table= - dest_functions.function_map[final_id]; - - in_dest_symbol_table.body.swap(src_it->second.body); - in_dest_symbol_table.type=src_it->second.type; - } - else // collision! - { - goto_functionst::goto_functiont &in_dest_symbol_table= - dest_functions.function_map[final_id]; - - goto_functionst::goto_functiont &src_func=src_it->second; - - if(in_dest_symbol_table.body.instructions.empty() || - weak_symbols.find(final_id)!=weak_symbols.end()) - { - // the one with body wins! - rename_symbols_in_function(src_func, rename_symbol); - - in_dest_symbol_table.body.swap(src_func.body); - in_dest_symbol_table.type=src_func.type; - } - else if(src_func.body.instructions.empty() || - src_ns.lookup(src_it->first).is_weak) - { - // just keep the old one in dest - } - else if(in_dest_symbol_table.type.get_bool(ID_C_inlined)) - { - // ok, we silently ignore - } - else - { - // the linking code will have ensured that types match - rename_symbol(src_func.type); - assert(base_type_eq(in_dest_symbol_table.type, src_func.type, ns)); - } - } - } - - // apply macros - rename_symbolt macro_application; - - forall_symbols(it, dest_symbol_table.symbols) - if(it->second.is_macro && !it->second.is_type) - { - const symbolt &symbol=it->second; - - assert(symbol.value.id()==ID_symbol); - const irep_idt &id=to_symbol_expr(symbol.value).get_identifier(); - - #if 0 - if(!base_type_eq(symbol.type, ns.lookup(id).type, ns)) - { - std::cerr << symbol << '\n'; - std::cerr << ns.lookup(id) << '\n'; - } - assert(base_type_eq(symbol.type, ns.lookup(id).type, ns)); - #endif - - macro_application.insert_expr(symbol.name, id); - } - - if(!macro_application.expr_map.empty()) - Forall_goto_functions(dest_it, dest_functions) - rename_symbols_in_function(dest_it->second, macro_application); - - if(!object_type_updates.expr_map.empty()) - { - Forall_goto_functions(dest_it, dest_functions) - Forall_goto_program_instructions(iit, dest_it->second.body) - { - object_type_updates(iit->code); - object_type_updates(iit->guard); - } - } - - return false; -} - /// reads an object file /// \par parameters: a file_name /// \return true on error, false otherwise bool read_object_and_link( const std::string &file_name, - symbol_tablet &symbol_table, - goto_functionst &functions, + goto_modelt &dest, message_handlert &message_handler) { messaget(message_handler).statistics() << "Reading: " @@ -361,31 +233,17 @@ bool read_object_and_link( message_handler)) return true; - typedef std::unordered_set id_sett; - id_sett weak_symbols; - forall_symbols(it, symbol_table.symbols) - if(it->second.is_weak) - weak_symbols.insert(it->first); - - linkingt linking(symbol_table, - temp_model.symbol_table, - message_handler); - - if(linking.typecheck_main()) - return true; - - if(link_functions( - symbol_table, - functions, - temp_model.symbol_table, - temp_model.goto_functions, - linking.rename_symbol, - weak_symbols, - linking.object_type_updates)) + try + { + link_goto_model(dest, temp_model, message_handler); + } + catch(...) + { return true; + } // reading successful, let's update config - config.set_from_symbol_table(symbol_table); + config.set_from_symbol_table(dest.symbol_table); return false; } @@ -395,12 +253,22 @@ bool read_object_and_link( /// \return true on error, false otherwise bool read_object_and_link( const std::string &file_name, - goto_modelt &goto_model, + symbol_tablet &dest_symbol_table, + goto_functionst &dest_functions, message_handlert &message_handler) { - return read_object_and_link( + goto_modelt goto_model; + + goto_model.symbol_table.swap(dest_symbol_table); + goto_model.goto_functions.swap(dest_functions); + + bool result=read_object_and_link( file_name, - goto_model.symbol_table, - goto_model.goto_functions, + goto_model, message_handler); + + goto_model.symbol_table.swap(dest_symbol_table); + goto_model.goto_functions.swap(dest_functions); + + return result; } From 8e52f8dad8f2dbbb2b36a8f4e0501c3d87691ad8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 Aug 2017 17:35:18 +0100 Subject: [PATCH 2/2] use invariant --- src/goto-programs/link_goto_model.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 6b40fd7173a..2c8b49f74b7 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -104,7 +104,8 @@ static bool link_functions( { // the linking code will have ensured that types match rename_symbol(src_func.type); - assert(base_type_eq(in_dest_symbol_table.type, src_func.type, ns)); + INVARIANT(base_type_eq(in_dest_symbol_table.type, src_func.type, ns), + "linking ensures that types match"); } } } @@ -117,7 +118,7 @@ static bool link_functions( { const symbolt &symbol=it->second; - assert(symbol.value.id()==ID_symbol); + INVARIANT(symbol.value.id()==ID_symbol, "must have symbol"); const irep_idt &id=to_symbol_expr(symbol.value).get_identifier(); #if 0 @@ -126,7 +127,8 @@ static bool link_functions( std::cerr << symbol << '\n'; std::cerr << ns.lookup(id) << '\n'; } - assert(base_type_eq(symbol.type, ns.lookup(id).type, ns)); + INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns), + "type matches"); #endif macro_application.insert_expr(symbol.name, id);