Add checks for symbol well-formedness.

src/util/symbol.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #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;
+}

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

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,

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
 

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;
 

unit/util/symbol.cpp

@@ -0,0 +1,54 @@
+/// 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";
+      symbol.mode = "C";
+
+      THEN("Symbol well-formedness check should fail")
+      {
+        REQUIRE_FALSE(symbol.is_well_formed());
+      }
+    }
+  }
+}

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