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.

Author: NlightNFotis

src/util/symbol.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "source_location.h"
 #include "std_expr.h"
+#include "suffix.h"
 
 void symbolt::show(std::ostream &out) const
 {
@@ -112,3 +113,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;
+}

src/util/symbol.h

@@ -123,6 +123,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);

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(
+      symbol.is_well_formed(), "Symbol is malformed: ", symbol_key);
+
     // Check that symbols[id].name == id
     DATA_CHECK_WITH_DIAGNOSTICS(
       symbol.name == symbol_key,

unit/Makefile

@@ -50,6 +50,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
 

unit/util/symbol.cpp

@@ -0,0 +1,53 @@
+/// Author: Diffblue Ltd.
+
+/// \file Tests for symbol_tablet
+
+#include <testing-utils/catch.hpp>
+#include <util/exception_utils.h>
+#include <util/symbol.h>
+
+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";
+
+      THEN("Symbol well-formedness check should fail")
+      {
+        REQUIRE_FALSE(symbol.is_well_formed());
+      }
+    }
+  }
+}