Check symbol table mappings

src/goto-programs/goto_model.h

@@ -96,7 +96,7 @@ class goto_modelt : public abstract_goto_modelt
   /// reported via DATA_INVARIANT violations or exceptions.
   void validate(const validation_modet vm) const
   {
-    symbol_table.validate();
+    symbol_table.validate(vm);
 
     const namespacet ns(symbol_table);
     goto_functions.validate(ns, vm);

src/util/symbol_table.cpp

@@ -2,7 +2,9 @@
 
 #include "symbol_table.h"
 
+#include <algorithm>
 #include <util/invariant.h>
+#include <util/validate.h>
 
 /// Move or copy a new symbol to the symbol table
 /// \remark: This is a nicer interface than move and achieves the same
@@ -114,3 +116,97 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry)
 
   internal_symbols.erase(entry);
 }
+
+/// Check whether the symbol table is in a valid state
+/// \param vm Determine whether to throw exceptions or trigger INVARIANT
+///   when validation fails
+void symbol_tablet::validate(const validation_modet vm) const
+{
+  // Check that identifiers are mapped to the correct symbol
+  for(const auto &elem : symbols)
+  {
+    const auto symbol_key = elem.first;
+    const auto &symbol = elem.second;
+
+    // Check that symbols[id].name == id
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      symbol.name == symbol_key,
+      "Symbol table entry must map to a symbol with the correct identifier",
+      "Symbol table key '",
+      symbol_key,
+      "' maps to symbol '",
+      symbol.name,
+      "'");
+
+    // Check that the symbol basename is mapped to its full name
+    if(!symbol.base_name.empty())
+    {
+      const auto base_map_search =
+        symbol_base_map.equal_range(symbol.base_name);
+      const bool base_map_matches_symbol =
+        std::find_if(
+          base_map_search.first,
+          base_map_search.second,
+          [&symbol_key](const typename symbol_base_mapt::value_type &match) {
+            return match.second == symbol_key;
+          }) != symbol_base_map.end();
+
+      DATA_CHECK_WITH_DIAGNOSTICS(
+        base_map_matches_symbol,
+        "The base_name of a symbol should map to itself",
+        "Symbol table key '",
+        symbol_key,
+        "' has a base_name '",
+        symbol.base_name,
+        "' which does not map to itself");
+    }
+
+    // Check that the module name of the symbol is mapped to the full name
+    if(!symbol.module.empty())
+    {
+      auto module_map_search = symbol_module_map.equal_range(symbol.module);
+      bool module_map_matches_symbol =
+        std::find_if(
+          module_map_search.first,
+          module_map_search.second,
+          [&symbol_key](const typename symbol_module_mapt::value_type &match) {
+            return match.second == symbol_key;
+          }) != symbol_module_map.end();
+
+      DATA_CHECK_WITH_DIAGNOSTICS(
+        module_map_matches_symbol,
+        "Symbol table module map should map to symbol",
+        "Symbol table key '",
+        symbol_key,
+        "' has a module name of '",
+        symbol.module,
+        "' which does not map to itself");
+    }
+  }
+
+  // Check that all base name map entries point to a symbol entry
+  for(auto base_map_entry : symbol_base_map)
+  {
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      has_symbol(base_map_entry.second),
+      "Symbol table base_name map entries must map to a symbol name",
+      "base_name map entry '",
+      base_map_entry.first,
+      "' maps to non-existant symbol name '",
+      base_map_entry.second,
+      "'");
+  }
+
+  // Check that all module map entries point to a symbol entry
+  for(auto module_map_entry : symbol_module_map)
+  {
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      has_symbol(module_map_entry.second),
+      "Symbol table module map entries must map to a symbol name",
+      "base_name map entry '",
+      module_map_entry.first,
+      "' maps to non-existant symbol name '",
+      module_map_entry.second,
+      "'");
+  }
+}

src/util/symbol_table.h

@@ -111,9 +111,7 @@ class symbol_tablet : public symbol_table_baset
   }
 
   /// Check that the symbol table is well-formed
-  void validate() const
-  {
-  }
+  void validate(const validation_modet vm = validation_modet::INVARIANT) const;
 };
 
 #endif // CPROVER_UTIL_SYMBOL_TABLE_H

unit/util/symbol_table.cpp

@@ -3,6 +3,7 @@
 /// \file Tests for symbol_tablet
 
 #include <testing-utils/catch.hpp>
+#include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
 
 TEST_CASE("Iterating through a symbol table", "[core][utils][symbol_tablet]")
@@ -25,6 +26,76 @@ TEST_CASE("Iterating through a symbol table", "[core][utils][symbol_tablet]")
   REQUIRE(counter == 1);
 }
 
+SCENARIO(
+  "symbol_table_validity_checks",
+  "[core][utils][symbol_table_validity_checks]")
+{
+  GIVEN("A valid symbol table")
+  {
+    symbol_tablet symbol_table;
+
+    symbolt symbol;
+    irep_idt symbol_name = "Test";
+    symbol.name = symbol_name;
+    symbol.base_name = "TestBase";
+    symbol.module = "TestModule";
+
+    symbol_table.insert(symbol);
+
+    THEN("validate() should return")
+    {
+      symbol_table.validate(validation_modet::EXCEPTION);
+    }
+    WHEN("A symbol name is transformed without updating the symbol table")
+    {
+      symbolt &transformed_symbol = symbol_table.get_writeable_ref(symbol_name);
+      transformed_symbol.name = "TransformTest";
+
+      THEN("validate() should throw an exception")
+      {
+        REQUIRE_THROWS_AS(
+          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 "
+      "mapping")
+    {
+      symbolt &transformed_symbol = symbol_table.get_writeable_ref(symbol_name);
+      // Transform the symbol
+      transformed_symbol.base_name = "TransformTestBase";
+
+      THEN("validate() should throw an exception")
+      {
+        REQUIRE_THROWS_AS(
+          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 "
+      "mapping")
+    {
+      symbolt &transformed_symbol = symbol_table.get_writeable_ref(symbol_name);
+      transformed_symbol.module = "TransformTestModule";
+
+      THEN("validate() should throw an exception")
+      {
+        REQUIRE_THROWS_AS(
+          symbol_table.validate(validation_modet::EXCEPTION),
+          incorrect_goto_program_exceptiont);
+      }
+      // Reset symbol to a valid module name
+      transformed_symbol.module = "TestModule";
+    }
+  }
+}
+
 SCENARIO("journalling_symbol_table_writer",
   "[core][utils][journalling_symbol_table_writer]")
 {