diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 1ac32d2341c..e56aa466bda 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -85,7 +85,7 @@ class is_threaded_domaint:public ai_domain_baset void is_threadedt::compute(const goto_functionst &goto_functions) { // the analysis doesn't actually use the namespace, fake one - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; const namespacet ns(symbol_table); ait is_threaded_analysis; diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index bbb1236e9e7..63d80b223a3 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -105,7 +105,7 @@ bool ansi_c_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) { - symbol_tablet new_symbol_table; + concrete_symbol_tablet new_symbol_table; if(ansi_c_typecheck( parse_tree, diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/src/ansi-c/ansi_c_typecheck.cpp index 50bfe78dffb..59883100857 100644 --- a/src/ansi-c/ansi_c_typecheck.cpp +++ b/src/ansi-c/ansi_c_typecheck.cpp @@ -42,7 +42,7 @@ bool ansi_c_typecheck( const unsigned errors_before= message_handler.get_message_count(messaget::M_ERROR); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; ansi_c_parse_treet ansi_c_parse_tree; ansi_c_typecheckt ansi_c_typecheck( diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 0a49ae57e77..ebc306e1cbf 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -269,6 +269,6 @@ std::string type2name(const typet &type, const namespacet &ns) std::string type2name(const typet &type) { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; return type2name(type, namespacet(symbol_table)); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index c1896935460..633cf93faac 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -68,7 +68,7 @@ class bmct:public safety_checkert protected: const optionst &options; - symbol_tablet new_symbol_table; + concrete_symbol_tablet new_symbol_table; namespacet ns; symex_target_equationt equation; symex_bmct symex; diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index e47d887d292..0aff3887ea4 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -125,7 +125,7 @@ bool cpp_languaget::typecheck( if(module=="") return false; - symbol_tablet new_symbol_table; + concrete_symbol_tablet new_symbol_table; if(cpp_typecheck( cpp_parse_tree, new_symbol_table, module, get_message_handler())) diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 549a5b6d77d..d99d0524f1e 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -102,7 +102,7 @@ bool cpp_typecheck( const unsigned errors_before= message_handler.get_message_count(messaget::M_ERROR); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; cpp_parse_treet cpp_parse_tree; cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table, diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 874e51e0d97..709bf517dd0 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -53,7 +53,7 @@ int linker_script_merget::add_linker_script_definitions() return fail; } - symbol_tablet original_st; + concrete_symbol_tablet original_st; goto_functionst original_gf; fail=read_goto_binary(goto_file, original_st, original_gf, get_message_handler()); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index c32fb2cc11a..5c18b9b6e4b 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -46,7 +46,7 @@ void dump_ct::operator()(std::ostream &os) // add copies of struct types when ID_C_transparent_union is only // annotated to parameter - symbol_tablet symbols_transparent; + concrete_symbol_tablet symbols_transparent; for(const auto &named_symbol : copied_symbol_table.symbols) { const symbolt &symbol=named_symbol.second; diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index bddb1cdeda2..dc61bef1598 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -48,7 +48,7 @@ class dump_ct protected: const goto_functionst &goto_functions; - symbol_tablet copied_symbol_table; + concrete_symbol_tablet copied_symbol_table; const namespacet ns; std::unique_ptr language; const bool harness; diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index 779bf1bfcc1..26686ec7a60 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -106,7 +106,7 @@ bool model_argc_argv( ansi_c_language.parse(iss, ""); config.ansi_c.preprocessor=pp; - symbol_tablet tmp_symbol_table; + concrete_symbol_tablet tmp_symbol_table; ansi_c_language.typecheck(tmp_symbol_table, ""); goto_programt init_instructions; diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 81f19d30c7a..c00eccd5132 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -325,7 +325,7 @@ void goto_unwindt::unwind( i_it!=goto_program.instructions.end();) { #ifdef DEBUG - symbol_tablet st; + concrete_symbol_tablet st; namespacet ns(st); std::cout << "Instruction:\n"; goto_program.output_instruction(ns, "", std::cout, i_it); diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 2f9c5939bc2..afa72b31c1a 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com class goto_modelt { public: - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; goto_functionst goto_functions; void clear() diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index da596927fc2..3fe351caada 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -495,7 +495,7 @@ class goto_program_templatet /// Output goto-program to given stream std::ostream &output(std::ostream &out) const { - return output(namespacet(symbol_tablet()), "", out); + return output(namespacet(concrete_symbol_tablet()), "", out); } /// Output a single instruction diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 9e7a1968ccc..f3c963688cc 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -251,7 +251,7 @@ bool read_object_and_link( /// \return true on error, false otherwise bool read_object_and_link( const std::string &file_name, - symbol_tablet &dest_symbol_table, + concrete_symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, message_handlert &message_handler) { diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index 1cc60e13a37..c3d7499098f 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -18,6 +18,7 @@ class goto_functionst; class goto_modelt; class message_handlert; class symbol_tablet; +class concrete_symbol_tablet; bool read_goto_binary( const std::string &filename, @@ -34,7 +35,7 @@ bool is_goto_binary(const std::string &filename); bool read_object_and_link( const std::string &file_name, - symbol_tablet &, + concrete_symbol_tablet &, goto_functionst &, message_handlert &); diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 5738f3d0c14..6c743764d3d 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -723,7 +723,7 @@ std::ostream &operator<<( const symex_target_equationt::SSA_stept &step) { // may cause lookup failures, since it's blank - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); step.output(ns, out); return out; diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index b0fc17fb03b..637d2f342b7 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -172,7 +172,9 @@ bool ci_lazy_methodst::operator()( while(any_new_methods); // Remove symbols for methods that were declared but never used: - symbol_tablet keep_symbols; + std::unordered_set unreachable_symbols; + for(const auto &sym : symbol_table.symbols) + unreachable_symbols.insert(sym.first); for(const auto &sym : symbol_table.symbols) { @@ -184,16 +186,19 @@ bool ci_lazy_methodst::operator()( continue; } if(sym.second.type.id()==ID_code) - gather_needed_globals(sym.second.value, symbol_table, keep_symbols); - keep_symbols.add(sym.second); + { + gather_needed_globals( + sym.second.value, symbol_table, unreachable_symbols); + } + unreachable_symbols.erase(sym.first); } - debug() << "CI lazy methods: removed " - << symbol_table.symbols.size() - keep_symbols.symbols.size() - << " unreaclass_hierarchyable methods and globals" - << eom; + debug() + << "CI lazy methods: removed " << unreachable_symbols.size() + << " unreachable methods and globals" << eom; - symbol_table.swap(keep_symbols); + for(const irep_idt &symbol_name : unreachable_symbols) + symbol_table.remove(symbol_name); return false; } @@ -425,7 +430,7 @@ void ci_lazy_methodst::get_virtual_method_targets( void ci_lazy_methodst::gather_needed_globals( const exprt &e, const symbol_tablet &symbol_table, - symbol_tablet &needed) + std::unordered_set &unreachable) { if(e.id()==ID_symbol) { @@ -438,12 +443,12 @@ void ci_lazy_methodst::gather_needed_globals( if(findit!=symbol_table.symbols.end() && findit->second.is_static_lifetime) { - needed.add(findit->second); + unreachable.erase(findit->first); } } else forall_operands(opit, e) - gather_needed_globals(*opit, symbol_table, needed); + gather_needed_globals(*opit, symbol_table, unreachable); } /// See param lazy_methods diff --git a/src/java_bytecode/ci_lazy_methods.h b/src/java_bytecode/ci_lazy_methods.h index f910abf2bb8..a0d0860fd7d 100644 --- a/src/java_bytecode/ci_lazy_methods.h +++ b/src/java_bytecode/ci_lazy_methods.h @@ -13,6 +13,7 @@ #define CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H #include +#include #include #include @@ -90,7 +91,7 @@ class ci_lazy_methodst:public messaget void gather_needed_globals( const exprt &e, const symbol_tablet &symbol_table, - symbol_tablet &needed); + std::unordered_set &unreachable); void gather_field_types(const typet &class_type, const namespacet &ns, diff --git a/src/java_bytecode/java_bytecode_parse_tree.cpp b/src/java_bytecode/java_bytecode_parse_tree.cpp index b8a60d8ddca..4db8250f74a 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -83,7 +83,7 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); out << '@' << type2java(type, ns); @@ -109,7 +109,7 @@ void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const void java_bytecode_parse_treet::annotationt::element_value_pairt::output( std::ostream &out) const { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); out << '"' << element_name << '"' << '='; @@ -118,7 +118,7 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output( void java_bytecode_parse_treet::methodt::output(std::ostream &out) const { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); for(const auto &annotation : annotations) diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index 83462732c1d..bd4ee989e4b 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -145,7 +145,7 @@ bool jsil_languaget::to_expr( result=true; else { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; result= jsil_convert(parse_tree, symbol_table, get_message_handler()); diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index a91eaf36f6f..06c4532f6bc 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -925,7 +925,7 @@ bool jsil_typecheck( const unsigned errors_before= message_handler.get_message_count(messaget::M_ERROR); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; jsil_typecheckt jsil_typecheck( symbol_table, diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 76fe7f2445c..1844dd74c7b 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -21,7 +21,7 @@ class language_uit:public messaget { public: language_filest language_files; - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; language_uit( const cmdlinet &cmdline, diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 06398eea3da..d2b4717bedf 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -78,13 +78,13 @@ std::string type_to_name( std::string from_expr(const exprt &expr) { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; return from_expr(namespacet(symbol_table), "", expr); } std::string from_type(const typet &type) { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; return from_type(namespacet(symbol_table), "", type); } @@ -110,6 +110,6 @@ exprt to_expr( std::string type_to_name(const typet &type) { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; return type_to_name(namespacet(symbol_table), "", type); } diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index fbcbcde2ee1..8ca044482a2 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -436,7 +436,7 @@ void dereference( value_setst &value_sets) { optionst options; - symbol_tablet new_symbol_table; + concrete_symbol_tablet new_symbol_table; goto_program_dereferencet goto_program_dereference(ns, new_symbol_table, options, value_sets); goto_program_dereference.dereference_expression(target, expr); diff --git a/src/util/recording_symbol_table.h b/src/util/recording_symbol_table.h new file mode 100644 index 00000000000..f828f686953 --- /dev/null +++ b/src/util/recording_symbol_table.h @@ -0,0 +1,128 @@ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. + +/// \file +/// A symbol table that records which entries have been updated + +#ifndef CPROVER_UTIL_RECORDING_SYMBOL_TABLE_H +#define CPROVER_UTIL_RECORDING_SYMBOL_TABLE_H + +#include +#include +#include "irep.h" +#include "symbol_table.h" + + +/// \brief A symbol table that records which entries have been updated/removed +/// \ingroup gr_symbol_table +/// A caller can pass a `recording_symbol_tablet` into a callee that is +/// expected to mutate it somehow, then after it has run inspect the recording +/// table's journal to determine what has changed more cheaply than examining +/// every symbol. +/// +/// Example of usage: +/// ``` +/// concrete_symbol_tablet actual_table; +/// init_table(actual_table); +/// +/// recording_symbol_tablet journal(actual_table); // Wraps actual_table +/// alter_table(journal); + +/// for(const auto &added : journal.added()) +/// { +/// printf("%s was added\n", added.name); +/// } +class recording_symbol_tablet:public symbol_tablet +{ +public: + typedef std::unordered_set changesett; +private: + symbol_tablet &base_symbol_table; + // Symbols originally in the table will never be marked inserted + changesett inserted; + // get_writeable marks an existing symbol updated + // Inserted symbols are marked updated, removed ones aren't + changesett updated; + // Symbols not originally in the table will never be marked removed + changesett removed; + +private: + explicit recording_symbol_tablet(symbol_tablet &base_symbol_table) + : symbol_tablet( + base_symbol_table.symbols, + base_symbol_table.symbol_base_map, + base_symbol_table.symbol_module_map), + base_symbol_table(base_symbol_table) + { + } + +public: + recording_symbol_tablet(const recording_symbol_tablet &other) + : symbol_tablet( + other.base_symbol_table.symbols, + other.base_symbol_table.symbol_base_map, + other.base_symbol_table.symbol_module_map), + base_symbol_table(other.base_symbol_table) + { + } + + static recording_symbol_tablet wrap(symbol_tablet &base_symbol_table) + { + return recording_symbol_tablet(base_symbol_table); + } + + virtual symbolt *get_writeable(const irep_idt &identifier) override + { + symbolt *result=base_symbol_table.get_writeable(identifier); + if(result) + on_update(identifier); + return result; + } + + virtual std::pair insert(symbolt symbol) override + { + std::pair result= + base_symbol_table.insert(std::move(symbol)); + if(result.second) + on_insert(result.first.name); + return result; + } + + virtual void erase(const symbolst::const_iterator &entry) override + { + base_symbol_table.erase(entry); + on_remove(entry->first); + } + + virtual void clear() override + { + for(const auto &named_symbol : base_symbol_table.symbols) + on_remove(named_symbol.first); + base_symbol_table.clear(); + } + + const changesett &get_inserted() const { return inserted; } + const changesett &get_updated() const { return updated; } + const changesett &get_removed() const { return removed; } + +private: + void on_insert(const irep_idt &id) + { + if(removed.erase(id)==0) + inserted.insert(id); + updated.insert(id); + } + + void on_update(const irep_idt &id) + { + updated.insert(id); + } + + void on_remove(const irep_idt &id) + { + if(inserted.erase(id)==0) + removed.insert(id); + updated.erase(id); + } +}; + +#endif // CPROVER_UTIL_RECORDING_SYMBOL_TABLE_H diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index ed8b67b1bb2..bea73c3826a 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -14,49 +14,10 @@ bool symbol_tablet::add(const symbolt &symbol) return !insert(symbol).second; } -/// Move or copy a new symbol to the symbol table -/// \remark: This is a nicer interface than move and achieves the same -/// result as both move and add -/// \param symbol: The symbol to be added to the symbol table - can be -/// moved or copied in -/// \return Returns a reference to the newly inserted symbol or to the -/// existing symbol if a symbol with the same name already exists in the -/// symbol table, along with a bool that is true if a new symbol was inserted. -std::pair symbol_tablet::insert(symbolt symbol) -{ - // Add the symbol to the table or retrieve existing symbol with the same name - std::pair result= - internal_symbols.emplace(symbol.name, std::move(symbol)); - symbolt &new_symbol=result.first->second; - if(result.second) - { - try - { - symbol_base_mapt::iterator base_result= - internal_symbol_base_map.emplace(new_symbol.base_name, new_symbol.name); - try - { - internal_symbol_module_map.emplace(new_symbol.module, new_symbol.name); - } - catch(...) - { - internal_symbol_base_map.erase(base_result); - throw; - } - } - catch(...) - { - internal_symbols.erase(result.first); - throw; - } - } - return std::make_pair(std::ref(new_symbol), result.second); -} - /// Move a symbol into the symbol table. If there is already a symbol with the /// same name then symbol is unchanged, new_symbol points to the symbol with the /// same name and true is returned. Otherwise, the symbol is moved into the -/// symbol table, symbol is set to be empty, new_symbol points to its new +/// symbol table, symbol is destroyed, new_symbol points to its new /// location in the symbol table and false is returned /// \param symbol: The symbol to be added to the symbol table /// \param new_symbol: Pointer which the function will set to either point to @@ -102,9 +63,67 @@ bool symbol_tablet::remove(const irep_idt &name) return false; } +/// Print the contents of the symbol table +/// \param out: The ostream to direct output to +void symbol_tablet::show(std::ostream &out) const +{ + out << "\n" << "Symbols:" << "\n"; + + forall_symbols(it, symbols) + out << it->second; +} + +/// Print the contents of the symbol table +/// \param out: The ostream to direct output to +/// \param symbol_table: The symbol table to print out +std::ostream &operator<<(std::ostream &out, const symbol_tablet &symbol_table) +{ + symbol_table.show(out); + return out; +} + +/// Move or copy a new symbol to the symbol table +/// \remark: This is a nicer interface than move and achieves the same +/// result as both move and add +/// \param symbol: The symbol to be added to the symbol table - can be +/// moved or copied in +/// \return Returns a reference to the newly inserted symbol or to the +/// existing symbol if a symbol with the same name already exists in the +/// symbol table, along with a bool that is true if a new symbol was inserted. +std::pair concrete_symbol_tablet::insert(symbolt symbol) +{ + // Add the symbol to the table or retrieve existing symbol with the same name + std::pair result= + internal_symbols.emplace(symbol.name, std::move(symbol)); + symbolt &new_symbol=result.first->second; + if(result.second) + { + try + { + symbol_base_mapt::iterator base_result= + internal_symbol_base_map.emplace(new_symbol.base_name, new_symbol.name); + try + { + internal_symbol_module_map.emplace(new_symbol.module, new_symbol.name); + } + catch(...) + { + internal_symbol_base_map.erase(base_result); + throw; + } + } + catch(...) + { + internal_symbols.erase(result.first); + throw; + } + } + return std::make_pair(std::ref(new_symbol), result.second); +} + /// Remove a symbol from the symbol table /// \param entry: an iterator pointing at the symbol to remove -void symbol_tablet::erase(const symbolst::const_iterator &entry) +void concrete_symbol_tablet::erase(const symbolst::const_iterator &entry) { const symbolt &symbol=entry->second; @@ -137,22 +156,3 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry) internal_symbols.erase(entry); } - -/// Print the contents of the symbol table -/// \param out: The ostream to direct output to -void symbol_tablet::show(std::ostream &out) const -{ - out << "\n" << "Symbols:" << "\n"; - - forall_symbols(it, symbols) - out << it->second; -} - -/// Print the contents of the symbol table -/// \param out: The ostream to direct output to -/// \param symbol_table: The symbol table to print out -std::ostream &operator << (std::ostream &out, const symbol_tablet &symbol_table) -{ - symbol_table.show(out); - return out; -} diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 42893a0882d..99533306ace 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -35,137 +35,178 @@ typedef std::multimap symbol_module_mapt; it!=it_end; ++it) -/// \brief The symbol table +/// \brief The base for symbol table implementations /// \ingroup gr_symbol_table class symbol_tablet { public: typedef std::unordered_map symbolst; -private: - symbolst internal_symbols; - symbol_base_mapt internal_symbol_base_map; - symbol_module_mapt internal_symbol_module_map; - public: const symbolst &symbols; const symbol_base_mapt &symbol_base_map; const symbol_module_mapt &symbol_module_map; - symbol_tablet() - : symbols(internal_symbols), - symbol_base_map(internal_symbol_base_map), - symbol_module_map(internal_symbol_module_map) +protected: + symbol_tablet( + const symbolst &symbols, + const symbol_base_mapt &symbol_base_map, + const symbol_module_mapt &symbol_module_map) + : symbols(symbols), + symbol_base_map(symbol_base_map), + symbol_module_map(symbol_module_map) { } - symbol_tablet(const symbol_tablet &other) - : internal_symbols(other.internal_symbols), - internal_symbol_base_map(other.internal_symbol_base_map), - internal_symbol_module_map(other.symbol_module_map), - symbols(internal_symbols), - symbol_base_map(internal_symbol_base_map), - symbol_module_map(internal_symbol_module_map) +public: + bool has_symbol(const irep_idt &name) const { + return symbols.find(name)!=symbols.end(); } - symbol_tablet &operator=(const symbol_tablet &other) + const symbolt *lookup(const irep_idt &identifier) const { - // Copy to temp and then call move assignment - return *this=symbol_tablet(other); + return lookup_impl(symbols, identifier); } - symbol_tablet(symbol_tablet &&other) - : internal_symbols(std::move(other.internal_symbols)), - internal_symbol_base_map(std::move(other.internal_symbol_base_map)), - internal_symbol_module_map(std::move(other.symbol_module_map)), - symbols(internal_symbols), - symbol_base_map(internal_symbol_base_map), - symbol_module_map(internal_symbol_module_map) + virtual symbolt *get_writeable(const irep_idt &identifier)=0; + + const symbolt &lookup_ref(const irep_idt &id) const { + return deref_or_throw(id, lookup(id)); } - symbol_tablet &operator=(symbol_tablet &&other) + symbolt &get_writeable_ref(const irep_idt &id) { - internal_symbols=std::move(other.internal_symbols); - internal_symbol_base_map=std::move(other.internal_symbol_base_map); - internal_symbol_module_map=std::move(other.symbol_module_map); - return *this; + // This casts the constness away that was added passing to deref_or_throw + return const_cast(deref_or_throw(id, get_writeable(id))); } - bool has_symbol(const irep_idt &name) const + bool add(const symbolt &symbol); + + virtual std::pair insert(symbolt symbol)=0; + + bool move(symbolt &symbol, symbolt *&new_symbol); + + bool remove(const irep_idt &name); + + virtual void erase(const symbolst::const_iterator &entry)=0; + + virtual void clear()=0; + + void show(std::ostream &out) const; + +protected: + template + static const symbolt *lookup_impl(Map &map, const irep_idt &id) { - return symbols.find(name)!=symbols.end(); + auto findit=map.find(id); + return findit==map.end() ? nullptr : &findit->second; } - /// Find a symbol in the symbol table for read-only access. - /// \param id: The name of the symbol to look for - /// \return an optional reference, set if found, nullptr otherwise. - const symbolt *lookup(const irep_idt &id) const { return lookup_impl(id); } +private: + static const symbolt &deref_or_throw(const irep_idt &id, const symbolt *sym) + { + if(sym) + return *sym; + throw std::out_of_range("Symbol not found: "+id2string(id)); + } +}; - /// Find a symbol in the symbol table for read-write access. - /// \param id: The name of the symbol to look for - /// \return an optional reference, set if found, unset otherwise. - symbolt *get_writeable(const irep_idt &id) { return lookup_impl(id); } +std::ostream &operator<<( + std::ostream &out, + const symbol_tablet &symbol_table); - /// Find a symbol in the symbol table for read-only access. - /// \param id: The name of the symbol to look for - /// \return A reference to the symbol - /// \throw `std::out_of_range` if no such symbol exists - const symbolt &lookup_ref(const irep_idt &id) const - { return internal_symbols.at(id); } - /// Find a symbol in the symbol table for read-write access. - /// \param id: The name of the symbol to look for - /// \return A reference to the symbol - /// \throw `std::out_of_range` if no such symbol exists - symbolt &get_writeable_ref(const irep_idt &id) - { return internal_symbols.at(id); } +/// \brief A symbol table that actually contains the maps of symbols +/// \ingroup gr_symbol_table +class concrete_symbol_tablet:public symbol_tablet +{ +private: + symbolst internal_symbols; + symbol_base_mapt internal_symbol_base_map; + symbol_module_mapt internal_symbol_module_map; - bool add(const symbolt &symbol); +public: + concrete_symbol_tablet() + : symbol_tablet( + internal_symbols, + internal_symbol_base_map, + internal_symbol_module_map) + { + } - std::pair insert(symbolt symbol); + explicit concrete_symbol_tablet(const symbol_tablet &other) + : symbol_tablet( + internal_symbols, + internal_symbol_base_map, + internal_symbol_module_map), + internal_symbols(other.symbols), + internal_symbol_base_map(other.symbol_base_map), + internal_symbol_module_map(other.symbol_module_map) + { + } - bool move(symbolt &symbol, symbolt *&new_symbol); + concrete_symbol_tablet &operator=(const symbol_tablet &other) + { + // Copy to temp and then call move assignment + return *this=concrete_symbol_tablet(other); + } - void clear() + concrete_symbol_tablet(const concrete_symbol_tablet &other) + : concrete_symbol_tablet(static_cast(other)) { - internal_symbols.clear(); - internal_symbol_base_map.clear(); - internal_symbol_module_map.clear(); } - bool remove(const irep_idt &name); + concrete_symbol_tablet &operator=(const concrete_symbol_tablet &other) + { + // Copy to temp and then call move assignment + return *this=concrete_symbol_tablet(other); + } - void erase(const symbolst::const_iterator &entry); + concrete_symbol_tablet(concrete_symbol_tablet &&other) + : symbol_tablet( + internal_symbols, + internal_symbol_base_map, + internal_symbol_module_map), + internal_symbols(std::move(other.internal_symbols)), + internal_symbol_base_map(std::move(other.internal_symbol_base_map)), + internal_symbol_module_map(std::move(other.symbol_module_map)) + { + } - void show(std::ostream &out) const; + concrete_symbol_tablet &operator=(concrete_symbol_tablet &&other) + { + internal_symbols=std::move(other.internal_symbols); + internal_symbol_base_map=std::move(other.internal_symbol_base_map); + internal_symbol_module_map=std::move(other.symbol_module_map); + return *this; + } - void swap(symbol_tablet &other) + void swap(concrete_symbol_tablet &other) { internal_symbols.swap(other.internal_symbols); internal_symbol_base_map.swap(other.internal_symbol_base_map); internal_symbol_module_map.swap(other.internal_symbol_module_map); } -private: - const symbolt *lookup_impl(const irep_idt &id) const - { return lookup_impl(*this, id); } + virtual symbolt *get_writeable(const irep_idt &identifier) override + { + // We know internal_symbols is non-const, so it's safe to cast away + // the constness introduced by lookup_impl. + return const_cast(lookup_impl(internal_symbols, identifier)); + } - symbolt *lookup_impl(const irep_idt &id) - { return lookup_impl(*this, id); } + virtual std::pair insert(symbolt symbol) override; - template - static auto lookup_impl(T &t, const irep_idt &id) - -> decltype(std::declval().lookup_impl(id)) + virtual void erase(const symbolst::const_iterator &entry) override; + + virtual void clear() override { - const auto it=t.internal_symbols.find(id); - return it==t.internal_symbols.end()?nullptr:&it->second; + internal_symbols.clear(); + internal_symbol_base_map.clear(); + internal_symbol_module_map.clear(); } }; -std::ostream &operator << ( - std::ostream &out, - const symbol_tablet &symbol_table); - #endif // CPROVER_UTIL_SYMBOL_TABLE_H diff --git a/unit/Makefile b/unit/Makefile index c89872fc1d3..4f091bd2934 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -30,6 +30,7 @@ SRC += unit_tests.cpp \ util/expr_iterator.cpp \ util/message.cpp \ util/simplify_expr.cpp \ + util/symbol_table.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index d345468fd99..50e6db47751 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -58,7 +58,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", ansi_c_languaget language; language.set_message_handler(message_handler); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); constant_simplification_mockt mock_ai_domain; diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp index 628af124bc2..fd368ecd389 100644 --- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp +++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp @@ -24,7 +24,7 @@ SCENARIO("does_expr_lose_const", "[core][analyses][does_remove_const][does_expr_remove_const]") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); goto_programt program; does_remove_constt does_remove_const(program, ns); diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp index ccfe0a56647..037a229ea0a 100644 --- a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp +++ b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp @@ -23,7 +23,7 @@ SCENARIO("does_type_preserve_const_correctness", "[core][analyses][does_remove_const][does_type_preserve_const_correctness]") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); goto_programt program; does_remove_constt does_remove_const(program, ns); diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp index 625c8df1121..1b6b8068ac1 100644 --- a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp +++ b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp @@ -23,7 +23,7 @@ SCENARIO("is_type_at_least_as_const", "[core][analyses][does_remove_const][is_type_at_least_as_const]") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); goto_programt program; does_remove_constt does_remove_const(program, ns); diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index 406291025ad..7dbf995e322 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -24,7 +24,7 @@ SCENARIO("java_bytecode_convert_abstract_class", { WHEN("Parsing an interface") { - const symbol_tablet &new_symbol_table= + const concrete_symbol_tablet new_symbol_table= load_java_class("I", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should be abstract") @@ -40,7 +40,7 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Parsing an abstract class") { - const symbol_tablet &new_symbol_table= + const concrete_symbol_tablet new_symbol_table= load_java_class("A", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should be abstract") { @@ -55,7 +55,7 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Passing a concrete class") { - const symbol_tablet &new_symbol_table= + const concrete_symbol_tablet new_symbol_table= load_java_class("C", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { @@ -70,7 +70,7 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Passing a concrete class that implements an interface") { - const symbol_tablet &new_symbol_table= + const concrete_symbol_tablet new_symbol_table= load_java_class( "Implementor", "./java_bytecode/java_bytecode_convert_class"); @@ -88,7 +88,7 @@ SCENARIO("java_bytecode_convert_abstract_class", } WHEN("Passing a concrete class that extends an abstract class") { - const symbol_tablet &new_symbol_table= + const concrete_symbol_tablet new_symbol_table= load_java_class( "Extender", "./java_bytecode/java_bytecode_convert_class"); diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp index 4d2a86944d8..b36279fcbe7 100644 --- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp +++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -31,7 +31,7 @@ exprt convert_exprt_to_string_exprt_unit_test( TEST_CASE("Convert exprt to string exprt") { source_locationt loc; - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); code_blockt code; java_string_library_preprocesst preprocess; diff --git a/unit/miniBDD.cpp b/unit/miniBDD.cpp index d0eba414184..ab8c16cf4d3 100644 --- a/unit/miniBDD.cpp +++ b/unit/miniBDD.cpp @@ -78,7 +78,7 @@ void test4() or_exprt o(and_exprt(a, b), not_exprt(a)); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); std::cout << from_expr(ns, "", o) << std::endl; diff --git a/unit/miniBDD_new.cpp b/unit/miniBDD_new.cpp index b61b0e54093..ba3c62a8e04 100644 --- a/unit/miniBDD_new.cpp +++ b/unit/miniBDD_new.cpp @@ -161,7 +161,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") { GIVEN("A bdd for x&!x") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); @@ -176,7 +176,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x&!x==0") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); @@ -196,7 +196,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x+x==1") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); @@ -216,7 +216,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*y==y*x") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); @@ -237,7 +237,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==2") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); @@ -257,7 +257,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==4") { - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp index 0b3fbcebdf0..ca19fc24aeb 100644 --- a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp +++ b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp @@ -25,7 +25,7 @@ static exprt actual( const unsigned long radix_ul) { const constant_exprt chr=from_integer(character, char_type); - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet ns(symtab); return simplify_expr( get_numeric_value_from_character( diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp index 350f59bdc56..86a89175989 100644 --- a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp +++ b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp @@ -24,7 +24,7 @@ static exprt actual( { const typet char_type=unsignedbv_typet(16); const constant_exprt chr=from_integer(int_value, char_type); - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet ns(symtab); return simplify_expr( diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index c90e0ebd27a..167b59a320a 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -143,7 +143,7 @@ SCENARIO("instantiate_not_contains", { // For printing expression register_language(new_java_bytecode_language); - symbol_tablet symtbl; + concrete_symbol_tablet symtbl; const namespacet ns(symtbl); GIVEN("The not_contains axioms of String.lastIndexOf(String, Int)") @@ -159,7 +159,7 @@ SCENARIO("instantiate_not_contains", func.arguments()=args; // Generating the corresponding axioms and simplifying, recording info - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); @@ -246,7 +246,7 @@ SCENARIO("instantiate_not_contains", a); // Create witness for axiom - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); @@ -304,7 +304,7 @@ SCENARIO("instantiate_not_contains", b); // Create witness for axiom - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); @@ -363,7 +363,7 @@ SCENARIO("instantiate_not_contains", empty); // Create witness for axiom - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); @@ -423,7 +423,7 @@ SCENARIO("instantiate_not_contains", ab); // Create witness for axiom - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort::infot info; @@ -483,7 +483,7 @@ SCENARIO("instantiate_not_contains", cd); // Create witness for axiom - symbol_tablet symtab; + concrete_symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index f1eb485fd4e..4fe76d8396d 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -23,7 +23,7 @@ /// \param class_path: The path to load the class from. Should be relative to /// the unit directory. /// \return The symbol table that is generated by parsing this file. -symbol_tablet load_java_class( +concrete_symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path) { @@ -37,7 +37,7 @@ symbol_tablet load_java_class( config.java.classpath.clear(); config.java.classpath.push_back(class_path); - symbol_tablet new_symbol_table; + concrete_symbol_tablet new_symbol_table; std::unique_ptrjava_lang(new_java_bytecode_language()); diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index d81bb2f7636..c0d588e1784 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -15,7 +15,7 @@ #include -symbol_tablet load_java_class( +concrete_symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path); diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 41f8adad246..07cd2a63008 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -22,7 +22,7 @@ TEST_CASE("Simplify pointer_offset(address of array index)") { config.set_arch("none"); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); array_typet array_type(char_type(), from_integer(2, size_type())); @@ -44,7 +44,7 @@ TEST_CASE("Simplify const pointer offset") { config.set_arch("none"); - symbol_tablet symbol_table; + concrete_symbol_tablet symbol_table; namespacet ns(symbol_table); // build a numeric constant of some pointer type @@ -74,7 +74,7 @@ void test_unnecessary_cast(const typet &type) typecast_exprt( typecast_exprt(symbol_exprt("foo", type), java_int_type()), type), - namespacet(symbol_tablet())); + namespacet(concrete_symbol_tablet())); REQUIRE(simplified.id()==ID_symbol); REQUIRE(simplified.type()==type); @@ -87,7 +87,7 @@ void test_unnecessary_cast(const typet &type) { const exprt simplified=simplify_expr( typecast_exprt(symbol_exprt("foo", type), java_int_type()), - namespacet(symbol_tablet())); + namespacet(concrete_symbol_tablet())); REQUIRE(simplified.id()==ID_typecast); REQUIRE(simplified.type()==java_int_type()); @@ -96,7 +96,7 @@ void test_unnecessary_cast(const typet &type) { const exprt simplified=simplify_expr( typecast_exprt(symbol_exprt("foo", java_int_type()), type), - namespacet(symbol_tablet())); + namespacet(concrete_symbol_tablet())); REQUIRE(simplified.id()==ID_typecast); REQUIRE(simplified.type()==type); @@ -116,7 +116,7 @@ void test_unnecessary_cast(const typet &type) java_int_type()), type), java_int_type()), - namespacet(symbol_tablet())); + namespacet(concrete_symbol_tablet())); REQUIRE( simplified==typecast_exprt(symbol_exprt("foo", type), java_int_type())); diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp new file mode 100644 index 00000000000..f82dfe25b72 --- /dev/null +++ b/unit/util/symbol_table.cpp @@ -0,0 +1,326 @@ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. + +/// \file Tests for symbol_tablet + +#include +#include + +SCENARIO("recording_symbol_table", + "[core][utils][recording_symbol_table]") +{ + GIVEN("A recording_symbol_tablet wrapping an empty concrete_symbol_tablet") + { + concrete_symbol_tablet base_symbol_table; + recording_symbol_tablet symbol_table= + recording_symbol_tablet::wrap(base_symbol_table); + WHEN("A symbol is copied into the symbol table") + { + irep_idt symbol_name1="Test1"; + symbolt symbol; + symbol.name=symbol_name1; + auto result=symbol_table.insert(symbol); + THEN("The insert should succeed") + { + REQUIRE(result.second); + } + THEN("The inserted symbol should have the same name") + { + REQUIRE(result.first.name==symbol_name1); + } + THEN( + "The symbol table should return a symbol from a lookup of that name") + { + REQUIRE(symbol_table.lookup(symbol_name1)!=nullptr); + } + THEN("The symbol table should return the same symbol from a lookup") + { + REQUIRE(&result.first==symbol_table.lookup(symbol_name1)); + } + THEN("The added symbol should appear in the updated collection") + { + REQUIRE(symbol_table.get_updated().count(symbol_name1)==1); + } + THEN("The added symbol should not appear in the removed collection") + { + REQUIRE(symbol_table.get_removed().count(symbol_name1)==0); + } + WHEN("Adding the same symbol again") + { + symbolt symbol; + symbol.name=symbol_name1; + auto result=symbol_table.insert(symbol); + THEN("The insert should fail") + { + REQUIRE(!result.second); + } + } + WHEN("Another symbol table is wrapped around the original symbol table") + { + recording_symbol_tablet symbol_table2= + recording_symbol_tablet::wrap(symbol_table); + WHEN("Adding the same symbol to the second symbol table") + { + symbolt symbol; + symbol.name=symbol_name1; + auto result=symbol_table.insert(symbol); + THEN("The insert should fail") + { + REQUIRE(!result.second); + } + } + WHEN("A symbol is moved into the new symbol table") + { + irep_idt symbol_name2="Test2"; + symbolt symbol; + symbol.name=symbol_name2; + auto result=symbol_table2.insert(std::move(symbol)); + THEN("The insert should succeed") + { + REQUIRE(result.second); + } + THEN("The inserted symbol should have the same name") + { + REQUIRE(result.first.name==symbol_name2); + } + THEN( + "The original symbol table should return a symbol from a lookup " + "of that name") + { + REQUIRE(symbol_table.lookup(symbol_name2)!=nullptr); + } + THEN( + "The new symbol table should return a symbol from a lookup " + "of that name") + { + REQUIRE(symbol_table2.lookup(symbol_name2)!=nullptr); + } + THEN( + "The new symbol table should return the same symbol from a lookup") + { + REQUIRE(&result.first==symbol_table2.lookup(symbol_name2)); + } + THEN( + "The added symbol should appear in the updated collection of the " + "original symbol table") + { + REQUIRE(symbol_table.get_updated().count(symbol_name2)==1); + } + THEN( + "The added symbol should appear in the updated collection of the " + "new symbol table") + { + REQUIRE(symbol_table2.get_updated().count(symbol_name2)==1); + } + THEN( + "The added symbol should not appear in the removed collection of " + "either symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name2)==0); + REQUIRE(symbol_table2.get_removed().count(symbol_name2)==0); + } + WHEN("Using the original symbol name") + { + irep_idt symbol_name1="Test1"; + THEN( + "Both symbol tables should return a symbol from a lookup " + "of that name") + { + REQUIRE(symbol_table.lookup(symbol_name1)!=nullptr); + REQUIRE(symbol_table2.lookup(symbol_name1)!=nullptr); + } + THEN( + "The added symbol should appear in the updated collection " + "of the original symbol table") + { + REQUIRE(symbol_table.get_updated().count(symbol_name1)==1); + } + THEN( + "The added symbol should not appear in the updated collection " + "of the new symbol table") + { + REQUIRE(symbol_table2.get_updated().count(symbol_name1)==0); + } + THEN( + "The added symbol should not appear in the removed collection " + "of either symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name1)==0); + REQUIRE(symbol_table2.get_removed().count(symbol_name1)==0); + } + } + WHEN("Removing the second symbol from the second map") + { + bool failure=symbol_table2.remove(symbol_name2); + THEN("The remove should succeed") + { + REQUIRE(!failure); + } + THEN("The second symbol should not appear in either map") + { + REQUIRE(symbol_table.lookup(symbol_name2)==nullptr); + REQUIRE(symbol_table2.lookup(symbol_name2)==nullptr); + } + THEN( + "The second symbol should not appear in the updated " + "collection of either symbol table") + { + REQUIRE(symbol_table.get_updated().count(symbol_name2)==0); + REQUIRE(symbol_table2.get_updated().count(symbol_name2)==0); + } + THEN( + "The second symbol should not appear in the removed " + "collection of either symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name2)==0); + REQUIRE(symbol_table2.get_removed().count(symbol_name2)==0); + } + } + WHEN("Removing the first symbol from the second map") + { + bool failure=symbol_table2.remove(symbol_name1); + THEN("The remove should succeed") + { + REQUIRE(!failure); + } + THEN("The first symbol should not appear in either map") + { + REQUIRE(symbol_table.lookup(symbol_name1)==nullptr); + REQUIRE(symbol_table2.lookup(symbol_name1)==nullptr); + } + THEN( + "The first symbol should not appear in the updated " + "collection of either symbol table") + { + REQUIRE(symbol_table.get_updated().count(symbol_name1)==0); + REQUIRE(symbol_table2.get_updated().count(symbol_name1)==0); + } + THEN( + "The first symbol should not appear in the removed " + "collection of the first symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name1)==0); + } + THEN( + "The first symbol should appear in the removed " + "collection of the second symbol table") + { + REQUIRE(symbol_table2.get_removed().count(symbol_name1)==1); + } + WHEN("Removing the first symbol from the second map again") + { + bool failure=symbol_table2.remove(symbol_name1); + THEN("The remove should fail") + { + REQUIRE(failure); + } + } + WHEN("Adding the first symbol back into the second map") + { + symbolt symbol; + symbol.name=symbol_name1; + auto result=symbol_table.insert(symbol); + THEN("The insert should succeed") + { + REQUIRE(result.second); + } + THEN( + "Both symbol tables should return a symbol from a lookup " + "of that name") + { + REQUIRE(symbol_table.lookup(symbol_name1)!=nullptr); + REQUIRE(symbol_table2.lookup(symbol_name1)!=nullptr); + } + THEN( + "Both symbol tables should return the same symbol from a " + "lookup") + { + REQUIRE(&result.first==symbol_table.lookup(symbol_name1)); + REQUIRE(&result.first==symbol_table2.lookup(symbol_name1)); + } + THEN( + "The added symbol should appear in the updated collection of " + "both symbol tables") + { + REQUIRE(symbol_table.get_updated().count(symbol_name2)==1); + REQUIRE(symbol_table2.get_updated().count(symbol_name2)==1); + } + THEN( + "The added symbol should not appear in the removed collection " + "of either symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name2)==0); + REQUIRE(symbol_table2.get_removed().count(symbol_name2)==0); + } + WHEN("Removing the first symbol from the second map again") + { + bool failure=symbol_table2.remove(symbol_name1); + THEN("The remove should succeed") + { + REQUIRE(!failure); + } + THEN("The first symbol should not appear in either map") + { + REQUIRE(symbol_table.lookup(symbol_name1)==nullptr); + REQUIRE(symbol_table2.lookup(symbol_name1)==nullptr); + } + THEN( + "The first symbol should not appear in the updated " + "collection of either symbol table") + { + REQUIRE(symbol_table.get_updated().count(symbol_name1)==0); + REQUIRE(symbol_table2.get_updated().count(symbol_name1)==0); + } + THEN( + "The first symbol should not appear in the removed " + "collection of the first symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name1)==0); + } + THEN( + "The first symbol should appear in the removed " + "collection of the second symbol table") + { + REQUIRE(symbol_table2.get_removed().count(symbol_name1)==1); + } + } + } + } + // This is equivalent to removing a symbol after the second symbol + // table is finished with - its updated/removed should be unaffected + WHEN("Removing the second symbol from the first map") + { + bool failure=symbol_table.remove(symbol_name2); + THEN("The remove should succeed") + { + REQUIRE(!failure); + } + THEN("The second symbol should not appear in either map") + { + REQUIRE(symbol_table.lookup(symbol_name2)==nullptr); + REQUIRE(symbol_table2.lookup(symbol_name2)==nullptr); + } + THEN( + "The second symbol should not appear in the updated " + "collection of the first symbol table") + { + REQUIRE(symbol_table.get_updated().count(symbol_name2)==0); + } + THEN( + "The second symbol should appear in the updated " + "collection of the second symbol table") + { + REQUIRE(symbol_table2.get_updated().count(symbol_name2)==1); + } + THEN( + "The second symbol should not appear in the removed " + "collection of either symbol table") + { + REQUIRE(symbol_table.get_removed().count(symbol_name2)==0); + REQUIRE(symbol_table2.get_removed().count(symbol_name2)==0); + } + } + } + } + } + } +}