Made it unnecessary to set the types on the Boogie ASTs as we create them.

Added support for string literals.
Translating structs no longer crashes the translator, but on the other hand, they are just skipped and not translated...
Added a helper method to make sure that generated identifiers are Boogie-legal.

11 files changed, 85 insertions, 24 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 13cb3552..74e52cfc 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -375,7 +375,10 @@ namespace BytecodeTranslator
       }

       else if (constant.Value is string)

       {

-        throw new NotImplementedException("Strings are not translated");

+        var c = this.sink.FindOrCreateConstant((string)(constant.Value));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(c));

+

+        //throw new NotImplementedException("Strings are not translated");

       } else {

         // TODO: (mschaef) hack

         var lit = Bpl.Expr.Literal((int)constant.Value);

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 4bd086c0..8f21d59a 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -497,6 +497,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
     public override Bpl.Variable CreateFieldVariable(IFieldReference field) {

       Bpl.Variable v;

       string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;

+      fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);

       Bpl.IToken tok = field.Token();

 

       if (field.IsStatic) {

@@ -584,9 +585,11 @@ procedure {:inline 1} Alloc() returns (x: ref)
       else {

         // wrap it in the right conversion function

         Bpl.Function conversion;

-        if (value.Type == Bpl.Type.Bool)

+        var originalType = this.underlyingTypes[f.Decl];

+        var boogieType = TranslationHelper.CciTypeToBoogie(originalType);

+        if (boogieType == Bpl.Type.Bool)

           conversion = this.Bool2Box;

-        else if (value.Type == Bpl.Type.Int)

+        else if (boogieType == Bpl.Type.Int)

           conversion = this.Int2Box;

         else

           throw new InvalidOperationException("Unknown Boogie type");

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index e0c4124f..78be9b53 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -84,6 +84,7 @@ namespace BytecodeTranslator {
     {

         Bpl.Variable v;

         string typename = TypeHelper.GetTypeName(type);

+        typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

         Bpl.IToken tok = type.Token();

         Bpl.Type t = this.TypeType;

         Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, t);

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 9fc2f4ee..ce5bff5b 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -186,6 +186,8 @@ namespace BytecodeTranslator {
         base.Visit(typeDefinition);

       } else if (typeDefinition.IsEnum) {

         return; // enums just are translated as ints

+      } else if (typeDefinition.IsStruct) {

+        Console.WriteLine("Skipping definition of '" + TypeHelper.GetTypeName(typeDefinition) + "' because it is a struct!");

       } else {

         Console.WriteLine("Unknown kind of type definition '{0}' was found",

           TypeHelper.GetTypeName(typeDefinition));

@@ -196,8 +198,9 @@ namespace BytecodeTranslator {
     private bool sawCctor = false;

 

     private void CreateStaticConstructor(ITypeDefinition typeDefinition) {

-      var proc = new Bpl.Procedure(Bpl.Token.NoToken,

-          TypeHelper.GetTypeName(typeDefinition) + ".#cctor",

+      var typename = TypeHelper.GetTypeName(typeDefinition);

+      typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

+      var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#cctor",

           new Bpl.TypeVariableSeq(),

           new Bpl.VariableSeq(), // in

           new Bpl.VariableSeq(), // out

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index e08c1b7b..5a2b27d0 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -173,6 +173,21 @@ namespace BytecodeTranslator {
       return null;

     }

 

+    public Bpl.Constant FindOrCreateConstant(string str) {

+      Bpl.Constant c;

+      if (!this.declaredStringConstants.TryGetValue(str, out c)) {

+        var tok = Bpl.Token.NoToken;

+        var t = Bpl.Type.Int;

+        var name = "$string_literal_" + TranslationHelper.TurnStringIntoValidIdentifier(str);

+        var tident = new Bpl.TypedIdent(tok, name, t);

+        c = new Bpl.Constant(tok, tident, true);

+        this.declaredStringConstants.Add(str, c);

+        this.TranslatedProgram.TopLevelDeclarations.Add(c);

+      }

+      return c;

+    }

+    private Dictionary<string, Bpl.Constant> declaredStringConstants = new Dictionary<string, Bpl.Constant>();

+

     private Dictionary<IPropertyDefinition, Bpl.Variable> declaredProperties = new Dictionary<IPropertyDefinition, Bpl.Variable>();

 

     public struct ProcedureInfo {

@@ -268,7 +283,8 @@ namespace BytecodeTranslator {
         Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();

         Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();

 

-        IMethodContract contract = ContractProvider.GetMethodContractFor(method);

+        var possiblyUnspecializedMethod = Unspecialize(method);

+        IMethodContract contract = ContractProvider.GetMethodContractFor(possiblyUnspecializedMethod);

 

         if (contract != null) {

           try {

@@ -338,6 +354,24 @@ namespace BytecodeTranslator {
       this.FindOrCreateProcedure(method, isStatic);

       return this.declaredMethods[method];

     }

+    private static IMethodReference Unspecialize(IMethodReference method) {

+      IMethodReference result = method;

+      var gmir = result as IGenericMethodInstanceReference;

+      if (gmir != null) {

+        result = gmir.GenericMethod;

+      }

+      var smr = result as ISpecializedMethodReference;

+      if (smr != null) {

+        result = smr.UnspecializedVersion;

+      }

+      // Temporary hack until ISpecializedMethodDefinition implements ISpecializedMethodReference

+      var smd = result as ISpecializedMethodDefinition;

+      if (smd != null) {

+        result = smd.UnspecializedVersion;

+      }

+      return result;

+    }

+

 

 

     /// <summary>

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index be104448..bff181c5 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -113,7 +113,7 @@ namespace BytecodeTranslator
       StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);

       StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);

 

-      ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, null);

+      ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this);

       condTraverser.Visit(conditionalStatement.Condition);

       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 04b95b37..30e90f8a 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -104,13 +104,30 @@ namespace BytecodeTranslator {
       }

       var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);

       s = s.Substring(2);

+      s = s.TrimEnd(')');

+      s = TurnStringIntoValidIdentifier(s);

+      return s;

+    }

+

+    public static string TurnStringIntoValidIdentifier(string s) {

       s = s.Replace('(', '$');

+      s = s.Replace(')', '$');

       s = s.Replace(',', '$');

-      s = s.TrimEnd(')');

       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('\n', '$');

+      s = s.Replace('/', '$');

+      s = s.Replace('\\', '$');

+      s = s.Replace('=', '$');

+      s = s.Replace('@', '$');

       return s;

     }

 

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index a9ca1990..8f070d61 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -639,11 +639,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 

 

 

-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

@@ -658,11 +658,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 

 

 

-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 176360d8..c9ddf0dd 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -617,11 +617,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 

 

 

-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

@@ -636,11 +636,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 

 

 

-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
index cde891c4..555b1c5b 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
@@ -625,11 +625,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 

 

 

-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

@@ -644,11 +644,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 

 

 

-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
index 9f63170c..7091a8ea 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -615,11 +615,11 @@ implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: i
 

 

 

-procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

@@ -634,11 +634,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) retu
 

 

 

-procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)

 {

   var local_0: int;