From df616e4e1a326c16b1f885328190250ab1c8d36f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 17 Oct 2018 17:21:21 +0100 Subject: [PATCH] Add well-formedness checks for symbols. Add a method that checks a symbol for structural validity according to some predetermined rule, and add it as an extra rule for symbol-table validity that each symbol is well-formed. --- src/util/symbol.cpp | 23 ++++++++ src/util/symbol.h | 3 ++ src/util/symbol_table.cpp | 4 ++ unit/Makefile | 1 + .../goto_model_function_type_consistency.cpp | 1 + unit/util/symbol.cpp | 54 +++++++++++++++++++ unit/util/symbol_table.cpp | 3 +- 7 files changed, 88 insertions(+), 1 deletion(-) create mode 100644 unit/util/symbol.cpp diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index ba7df69ca90..758b18583c1 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "source_location.h" #include "std_expr.h" +#include "suffix.h" /// Dump the state of a symbol object to a given output stream. /// \param out: The stream to output object state to. @@ -121,3 +122,25 @@ symbol_exprt symbolt::symbol_expr() const { return symbol_exprt(name, type); } + +/// Check that the instance object is well formed. +/// \return: true if well-formed; false otherwise. +bool symbolt::is_well_formed() const +{ + // Well-formedness criterion number 1 is for a symbol + // to have a non-empty mode (see #1880) + if(mode.empty()) + { + return false; + } + + // Well-formedness criterion number 2 is for a symbol + // to have it's base name as a suffix to it's more + // general name. + if(!has_suffix(id2string(name), id2string(base_name))) + { + return false; + } + + return true; +} diff --git a/src/util/symbol.h b/src/util/symbol.h index 05a0b7941c3..83d03a3aa62 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -121,6 +121,9 @@ class symbolt PRECONDITION(type.id() == ID_code); value = exprt(ID_compiled); } + + /// Check that a symbol is well formed. + bool is_well_formed() const; }; std::ostream &operator<<(std::ostream &out, const symbolt &symbol); diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 23ef1e327d7..296b2cd0df4 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -128,6 +128,10 @@ void symbol_tablet::validate(const validation_modet vm) const const auto symbol_key = elem.first; const auto &symbol = elem.second; + // First of all, ensure symbol well-formedness + DATA_CHECK_WITH_DIAGNOSTICS( + vm, symbol.is_well_formed(), "Symbol is malformed: ", symbol_key); + // Check that symbols[id].name == id DATA_CHECK_WITH_DIAGNOSTICS( vm, diff --git a/unit/Makefile b/unit/Makefile index 0a5142da73d..fa50d550ba0 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -63,6 +63,7 @@ SRC += analyses/ai/ai.cpp \ util/string_utils/split_string.cpp \ util/string_utils/strip_string.cpp \ util/symbol_table.cpp \ + util/symbol.cpp \ util/unicode.cpp \ # Empty last line diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp index 69cc5265819..10d40282871 100644 --- a/unit/goto-programs/goto_model_function_type_consistency.cpp +++ b/unit/goto-programs/goto_model_function_type_consistency.cpp @@ -22,6 +22,7 @@ SCENARIO( code_typet fun_type2({}, type2); symbolt function_symbol; + function_symbol.mode = "C"; irep_idt function_symbol_name = "foo"; function_symbol.name = function_symbol_name; diff --git a/unit/util/symbol.cpp b/unit/util/symbol.cpp new file mode 100644 index 00000000000..51866532e52 --- /dev/null +++ b/unit/util/symbol.cpp @@ -0,0 +1,54 @@ +/// Author: Diffblue Ltd. + +/// \file Tests for symbol_tablet + +#include +#include +#include + +SCENARIO( + "Constructed symbol validity checks", + "[core][utils][symbol__validity_checks]") +{ + GIVEN("A valid symbol") + { + symbolt symbol; + irep_idt symbol_name = "Test_TestBase"; + symbol.name = symbol_name; + symbol.base_name = "TestBase"; + symbol.module = "TestModule"; + symbol.mode = "C"; + + THEN("Symbol should be well formed") + { + REQUIRE(symbol.is_well_formed()); + } + } + + GIVEN("An improperly initialised symbol") + { + symbolt symbol; + + WHEN("The symbol doesn't have a valid mode") + { + symbol.mode = ""; + + THEN("Symbol well-formedness check should fail") + { + REQUIRE_FALSE(symbol.is_well_formed()); + } + } + + WHEN("The symbol doesn't have base name as a suffix to name") + { + symbol.name = "TEST"; + symbol.base_name = "TestBase"; + symbol.mode = "C"; + + THEN("Symbol well-formedness check should fail") + { + REQUIRE_FALSE(symbol.is_well_formed()); + } + } + } +} diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp index febfff751b3..260dc460603 100644 --- a/unit/util/symbol_table.cpp +++ b/unit/util/symbol_table.cpp @@ -35,10 +35,11 @@ SCENARIO( symbol_tablet symbol_table; symbolt symbol; - irep_idt symbol_name = "Test"; + irep_idt symbol_name = "Test_TestBase"; symbol.name = symbol_name; symbol.base_name = "TestBase"; symbol.module = "TestModule"; + symbol.mode = "C"; symbol_table.insert(symbol);