diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 331f41e074d..ed20b36762a 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -28,14 +28,18 @@ std::pair symbol_tablet::insert(symbolt symbol) { symbol_base_mapt::iterator base_result= internal_symbol_base_map.emplace(new_symbol.base_name, new_symbol.name); - try + if(!new_symbol.module.empty()) { - internal_symbol_module_map.emplace(new_symbol.module, new_symbol.name); - } - catch(...) - { - internal_symbol_base_map.erase(base_result); - throw; + try + { + internal_symbol_module_map.emplace( + new_symbol.module, new_symbol.name); + } + catch(...) + { + internal_symbol_base_map.erase(base_result); + throw; + } } } catch(...) @@ -89,10 +93,8 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry) { const symbolt &symbol=entry->second; - symbol_base_mapt::const_iterator - base_it=symbol_base_map.lower_bound(entry->second.base_name); - symbol_base_mapt::const_iterator - base_it_end=symbol_base_map.upper_bound(entry->second.base_name); + auto base_it = symbol_base_map.lower_bound(symbol.base_name); + const auto base_it_end = symbol_base_map.upper_bound(symbol.base_name); while(base_it!=base_it_end && base_it->second!=symbol.name) ++base_it; INVARIANT( @@ -103,18 +105,23 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry) "current base_name: "+id2string(symbol.base_name)+")"); internal_symbol_base_map.erase(base_it); - symbol_module_mapt::const_iterator - module_it=symbol_module_map.lower_bound(entry->second.module), - module_it_end=symbol_module_map.upper_bound(entry->second.module); - while(module_it!=module_it_end && module_it->second!=symbol.name) - ++module_it; - INVARIANT( - module_it!=module_it_end, - "symbolt::module should not be changed " - "after it is added to the symbol_table " - "(name: "+id2string(symbol.name)+", " - "current module: "+id2string(symbol.module)+")"); - internal_symbol_module_map.erase(module_it); + if(!symbol.module.empty()) + { + auto module_it = symbol_module_map.lower_bound(symbol.module); + auto module_it_end = symbol_module_map.upper_bound(symbol.module); + while(module_it != module_it_end && module_it->second != symbol.name) + ++module_it; + INVARIANT( + module_it != module_it_end, + "symbolt::module should not be changed " + "after it is added to the symbol_table " + "(name: " + + id2string(symbol.name) + + ", " + "current module: " + + id2string(symbol.module) + ")"); + internal_symbol_module_map.erase(module_it); + } internal_symbols.erase(entry); } diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index fdd72175050..2db1ac838c2 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -19,8 +19,11 @@ class symbol_tablet : public symbol_table_baset { private: + /// Value referenced by \ref symbol_table_baset::symbols. symbolst internal_symbols; + /// Value referenced by \ref symbol_table_baset::symbol_base_map. symbol_base_mapt internal_symbol_base_map; + /// Value referenced by \ref symbol_table_baset::symbol_module_map. symbol_module_mapt internal_symbol_module_map; public: diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h index 13aed91f80a..8d3c4b9fa62 100644 --- a/src/util/symbol_table_base.h +++ b/src/util/symbol_table_base.h @@ -24,8 +24,17 @@ class symbol_table_baset typedef std::unordered_map symbolst; public: + /// Read-only field, used to look up symbols given their names. + /// Typically a subclass will have its own corresponding writeable field, and + /// the read-only fields declared here function as "getters" for them. const symbolst &symbols; + /// Read-only field, used to look up symbol names given their base names. + /// See \ref symbols. const symbol_base_mapt &symbol_base_map; + /// Read-only field, used to look up symbol names given their modules. + /// See \ref symbols. + /// Note that symbols whose module is empty are not recorded in this map. + /// Currently only used in EBMC. const symbol_module_mapt &symbol_module_map; public: diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp index 96cc9b9fd7c..69043892bd3 100644 --- a/unit/util/symbol_table.cpp +++ b/unit/util/symbol_table.cpp @@ -59,8 +59,6 @@ SCENARIO( symbol_table.validate(validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } - // Reset symbol to a valid name after the previous test - transformed_symbol.name = symbol_name; } WHEN( "A symbol base_name is transformed without updating the base_name " @@ -76,8 +74,6 @@ SCENARIO( symbol_table.validate(validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } - // Reset symbol to a valid base_name after the previous test - transformed_symbol.base_name = "TestBase"; } WHEN( "A symbol module identifier is transformed without updating the module " @@ -92,8 +88,58 @@ SCENARIO( symbol_table.validate(validation_modet::EXCEPTION), incorrect_goto_program_exceptiont); } - // Reset symbol to a valid module name - transformed_symbol.module = "TestModule"; + } + } +} + +SCENARIO( + "symbol_table_symbol_module_map", + "[core][utils][symbol_table_symbol_module_map]") +{ + GIVEN("A valid symbol table") + { + symbol_tablet symbol_table; + WHEN("Inserting a symbol with non-empty module") + { + symbolt symbol; + symbol.name = "TestName"; + symbol.module = "TestModule"; + symbol_table.insert(std::move(symbol)); + THEN("The symbol module map contains an entry for the symbol") + { + REQUIRE(symbol_table.symbol_module_map.size() == 1); + const auto entry = symbol_table.symbol_module_map.begin(); + REQUIRE(id2string(entry->first) == "TestModule"); + REQUIRE(id2string(entry->second) == "TestName"); + } + WHEN("Removing the symbol again") + { + symbol_table.remove("TestName"); + THEN("The symbol module map no longer contains an entry for the symbol") + { + REQUIRE(symbol_table.symbol_module_map.size() == 0); + } + } + } + WHEN("Inserting a symbol with empty module") + { + symbolt symbol; + symbol.name = "TestName"; + symbol_table.insert(std::move(symbol)); + THEN("The symbol module map does not contain an entry for the symbol") + { + REQUIRE(symbol_table.symbol_module_map.size() == 0); + } + WHEN("Removing the symbol again") + { + symbol_table.remove("TestName"); + THEN( + "The symbol module map still does not contain an entry for the " + "symbol") + { + REQUIRE(symbol_table.symbol_module_map.size() == 0); + } + } } } }