From 0f18b68965fdd680bd808390dbb2cd6e8153f66d Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 5 Oct 2018 16:45:06 +0100 Subject: [PATCH] Add validity checks for symbol table mappings --- src/goto-programs/goto_model.h | 2 +- src/util/symbol_table.cpp | 96 ++++++++++++++++++++++++++++++++++ src/util/symbol_table.h | 4 +- unit/util/symbol_table.cpp | 71 +++++++++++++++++++++++++ 4 files changed, 169 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index d6b6c961b7c..69e80ef0fbf 100644 --- a/src/goto-programs/goto_model.h +++ b/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); diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 6557feb5c14..3a7b74db09c 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -2,7 +2,9 @@ #include "symbol_table.h" +#include #include +#include /// 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, + "'"); + } +} diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 6d5725e47ed..3de069d2448 100644 --- a/src/util/symbol_table.h +++ b/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 diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp index c6190cbf005..7d013a2f827 100644 --- a/unit/util/symbol_table.cpp +++ b/unit/util/symbol_table.cpp @@ -3,6 +3,7 @@ /// \file Tests for symbol_tablet #include +#include #include 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]") {