Add more robust type name to type identifier conversion

In order to certain that we don't emmit C harnesses containing invalid
identifiers.

The unit test includes both a function to generate the string of all
printable characters and the same string as a string literal in order to
show that the string does include all printable characters and to show
what these characters are.

Author: thomasspriggs

src/ansi-c/type2name.cpp

@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/std_types.h>
 #include <util/symbol_table.h>
 
+#include <regex>
+
 typedef std::unordered_map<irep_idt, std::pair<size_t, bool>> symbol_numbert;
 
 static std::string type2name(
@@ -279,26 +281,47 @@ std::string type2name(const typet &type, const namespacet &ns)
 /// This replaces some invalid characters that can appear in type2name output.
 std::string type_name2type_identifier(const std::string &name)
 {
-  std::string result{};
-  for(char c : name)
-  {
-    switch(c)
+  const auto replace_special_characters = [](const std::string &name) {
+    std::string result{};
+    for(char c : name)
     {
-    case '*':
-      result += "_ptr_";
-      break;
-    case '{':
-      result += "_start_sub_";
-      break;
-    case '}':
-      result += "_end_sub_";
-      break;
-    default:
-      result += c;
-      break;
+      switch(c)
+      {
+      case '*':
+        result += "_ptr_";
+        break;
+      case '{':
+        result += "_start_sub_";
+        break;
+      case '}':
+        result += "_end_sub_";
+        break;
+      default:
+        result += c;
+        break;
+      }
     }
-  }
-  return result;
+    return result;
+  };
+  const auto replace_invalid_characters_with_underscore =
+    [](const std::string &identifier) {
+      static const std::regex non_alpha_numeric{"[^A-Za-z0-9]"};
+      return std::regex_replace(identifier, non_alpha_numeric, "_");
+    };
+  const auto remove_duplicate_underscores = [](const std::string &identifier) {
+    static const std::regex duplicate_underscore{"_+"};
+    return std::regex_replace(identifier, duplicate_underscore, "_");
+  };
+  const auto strip_leading_non_letters = [](const std::string &identifier) {
+    static const std::regex identifier_regex{"[A-Za-z][A-Za-z0-9_]*"};
+    std::smatch match_results;
+    bool found = std::regex_search(identifier, match_results, identifier_regex);
+    POSTCONDITION(found);
+    return match_results.str(0);
+  };
+  return strip_leading_non_letters(
+    remove_duplicate_underscores(replace_invalid_characters_with_underscore(
+      replace_special_characters(name))));
 }
 
 std::string type2identifier(const typet &type, const namespacet &ns)

unit/ansi-c/type2name.cpp

@@ -8,6 +8,8 @@ Author: Thomas Spriggs
 
 #include <testing-utils/use_catch.h>
 
+#include <numeric>
+
 extern std::string type_name2type_identifier(const std::string &name);
 
 TEST_CASE(
@@ -24,3 +26,40 @@ TEST_CASE(
   CHECK(type_name2type_identifier("char*") == "char_ptr_");
   CHECK(type_name2type_identifier("foo{bar}") == "foo_start_sub_bar_end_sub_");
 }
+
+/**
+ * @return A string containing all 7-bit ascii printable characters.
+ */
+static std::string all_printable_characters()
+{
+  const char first = 32;
+  const char last = 127;
+  std::string printable_characters(last - first, ' ');
+  std::iota(printable_characters.begin(), printable_characters.end(), first);
+  return printable_characters;
+}
+
+TEST_CASE(
+  "type_name2type_identifier invalid characters",
+  "[core][ansi-c][type_name2type_identifier]")
+{
+  const std::string printable_characters = all_printable_characters();
+  CHECK(
+    printable_characters ==
+    R"( !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`)"
+    R"(abcdefghijklmnopqrstuvwxyz{|}~)");
+  CHECK(
+    type_name2type_identifier(printable_characters) ==
+    "ptr_0123456789_ABCDEFGHIJKLMNOPQRSTUVWXYZ_abcdefghijklmnopqrstuvwxyz_"
+    "start_sub_end_sub_");
+}
+
+TEST_CASE(
+  "type_name2type_identifier leading digits",
+  "[core][ansi-c][type_name2type_identifier]")
+{
+  CHECK(
+    type_name2type_identifier(
+      "0123456789_banana_0123456789_split_0123456789") ==
+    "banana_0123456789_split_0123456789");
+}