Refine symbol well-formedness checks to handle special cases

The symbol naming check added in df616e4 attempts to assert that the 'base_name'
of a symbol is a suffix of that symbol's 'name'. In general, this should be the
case, but there are certain classes of symbols where this does not currently
hold. This commit adds special cases to handle:

* Type symbols that are typedefs or tags
* Symbols that have been renamed by the linker

With these special cases handled, it is possible to run the CORE regression
tests with --validate-goto-model enabled.

Author: chrisr-diffblue

src/util/symbol.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "source_location.h"
 #include "std_expr.h"
+#include "string_utils.h"
 #include "suffix.h"
 
 /// Dump the state of a symbol object to a given output stream.
@@ -137,11 +138,62 @@ bool symbolt::is_well_formed() const
   // Well-formedness criterion number 2 is for a symbol
   // to have it's base name as a suffix to it's more
   // general name.
+
   // Exception: Java symbols' base names do not have type signatures
   // (for example, they can have name "someclass.method:(II)V" and base name
   // "method")
   if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
-    return false;
+  {
+    bool criterion_must_hold = true;
+
+    // There are some special cases where this criterion doesn't hold, check
+    // to see if we have one of those cases
+
+    if(is_type)
+    {
+      // Typedefs
+      if(
+        type.find(ID_C_typedef).is_not_nil() &&
+        type.find(ID_C_typedef).id() == base_name)
+      {
+        criterion_must_hold = false;
+      }
+
+      // Tag types
+      if(type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name)
+      {
+        criterion_must_hold = false;
+      }
+    }
+
+    // Linker renaming may have added $linkN suffixes to the name, and other
+    // suffixes such as #return_value may have then be subsequently added.
+    // Strip out the first $linkN substring and then see if the criterion holds
+    const auto &unstripped_name = id2string(name);
+    const size_t dollar_link_start_pos = unstripped_name.find("$link");
+
+    if(dollar_link_start_pos != std::string::npos)
+    {
+      size_t dollar_link_end_pos = dollar_link_start_pos + 5;
+      while(isdigit(unstripped_name[dollar_link_end_pos]))
+      {
+        ++dollar_link_end_pos;
+      }
+
+      const auto stripped_name =
+        unstripped_name.substr(0, dollar_link_start_pos) +
+        unstripped_name.substr(dollar_link_end_pos, std::string::npos);
+
+      if(has_suffix(stripped_name, id2string(base_name)))
+        criterion_must_hold = false;
+    }
+
+    if(criterion_must_hold)
+    {
+      // For all other cases this criterion should hold
+      return false;
+    }
+  }
 
   return true;
 }