From 7c799c6f3536e873327213d74d01e7f1235b3ca8 Mon Sep 17 00:00:00 2001
From: Mike Barnett <mbarnett@microsoft.com>
Date: Mon, 31 Oct 2011 15:09:08 -0700
Subject: Major changes to the translator traversers because they now are based
 on the new traversers. (The old ones have been marked as obsolete.) All types
 are now encoded as "datatypes" in Boogie. So non-generic types are nullary
 functions and generic types just have at least one type argument. Lots of
 other fixes: string encoding of names is now done by negating Boogie's
 regular expression for identifiers, etc.

---
 BCT/BytecodeTranslator/TranslationHelper.cs | 49 +++++++++--------------------
 1 file changed, 15 insertions(+), 34 deletions(-)

(limited to 'BCT/BytecodeTranslator/TranslationHelper.cs')

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 883d0eaf..a744f405 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -15,7 +15,7 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;
 
 using Bpl = Microsoft.Boogie;
-
+using System.Text.RegularExpressions;
 
 namespace BytecodeTranslator {
 
@@ -131,44 +131,25 @@ namespace BytecodeTranslator {
     }
 
     public static string TurnStringIntoValidIdentifier(string s) {
+
+      // Do this specially just to make the resulting string a little bit more readable.
+      // REVIEW: Just let the main replacement take care of it?
       s = s.Replace("[0:,0:]", "2DArray"); // TODO: Do this programmatically to handle arbitrary arity
       s = s.Replace("[0:,0:,0:]", "3DArray");
       s = s.Replace("[0:,0:,0:,0:]", "4DArray");
       s = s.Replace("[0:,0:,0:,0:,0:]", "5DArray");
-      s = s.Replace('!', '$');
-      s = s.Replace('*', '$');
-      s = s.Replace('+', '$');
-      s = s.Replace('(', '$');
-      s = s.Replace(')', '$');
-      s = s.Replace(',', '$');
       s = s.Replace("[]", "array");
-      s = s.Replace('<', '$');
-      s = s.Replace('>', '$');
-      s = s.Replace(':', '$');
-      s = s.Replace(' ', '$');
-      s = s.Replace('{', '$');
-      s = s.Replace('}', '$');
-      s = s.Replace('-', '$');
-      s = s.Replace(' ', '$');
-      s = s.Replace('\t', '$');
-      s = s.Replace('\r', '$');
-      s = s.Replace('\n', '$');
-      s = s.Replace('\b', '$');
-      s = s.Replace('\x1B', '$');
-      s = s.Replace('/', '$');
-      s = s.Replace('\\', '$');
-      s = s.Replace('=', '$');
-      s = s.Replace('@', '$');
-      s = s.Replace(';', '$');
-      s = s.Replace('%', '$');
-      s = s.Replace('&', '$');
-      s = s.Replace('"', '$');
-      s = s.Replace('[', '$');
-      s = s.Replace(']', '$');
-      s = s.Replace('|', '$');
-      s = s.Replace('+', '$');
-      s = s.Replace('±', '$');
-      s = s.Replace('√', '$');
+
+      // The definition of a Boogie identifier is from BoogiePL.atg.
+      // Just negate that to get which characters should be replaced with a dollar sign.
+
+      // letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
+      // digit = "0123456789".
+      // special = "'~#$^_.?`".
+      // nondigit = letter + special.
+      // ident =  [ '\\' ] nondigit {nondigit | digit}.
+
+      s = Regex.Replace(s, "[^A-Za-z0-9'~#$^_.?`]", "$");
       
       s = GetRidOfSurrogateCharacters(s);
       return s;
-- 
cgit v1.2.3