[TG-9830] [UFC] Exclude symbols with empty module from the symbol module map

src/util/symbol_table.cpp

@@ -28,14 +28,18 @@ std::pair<symbolt &, bool> 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);
 }

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:

src/util/symbol_table_base.h

@@ -24,8 +24,17 @@ class symbol_table_baset
   typedef std::unordered_map<irep_idt, symbolt> 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:

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);
+        }
+      }
     }
   }
 }