General hygiene: introduced (fixed) a helper method that creates Boogie tokens. Made it an extension method that takes any object implementing IObjectWithLocations. Much easier to use within the translator.

6 files changed, 36 insertions, 44 deletions

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index 78077ef3..a343402e 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -35,7 +35,7 @@ namespace BytecodeTranslator {
         Bpl.Expr rexp = TranslatedExpressions.Pop();

         Bpl.Expr lexp = TranslatedExpressions.Pop();

 

-        var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);

+        var tok = division.Token();

 

         var loc = this.sink.CreateFreshLocal(division.RightOperand.Type);

         var locExpr = Bpl.Expr.Ident(loc);

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 108c0fd1..20dd5d2e 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -187,7 +187,7 @@ namespace BytecodeTranslator {
     }

     

     public override void Visit(IThisReference thisReference) {

-      TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(thisReference.Locations),

+      TranslatedExpressions.Push(new Bpl.IdentifierExpr(thisReference.Token(),

         this.sink.ThisVariable));

     }

 

@@ -292,7 +292,7 @@ namespace BytecodeTranslator {
         while (TranslatedExpressions.Count > 0) {

           elist.Add(TranslatedExpressions.Pop());

         }

-        TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(field.Locations), HeapVariable), elist));

+        TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(field.Token(), HeapVariable), elist));

       }

     }

 

@@ -354,7 +354,7 @@ namespace BytecodeTranslator {
       }

       #endregion

 

-      Bpl.IToken cloc = TranslationHelper.CciLocationToBoogieToken(methodCall.Locations);

+      Bpl.IToken cloc = methodCall.Token();

 

       // meeting a constructor is always something special

       if (methodCall.MethodToCall.ResolvedMethod.IsConstructor) {

@@ -406,7 +406,7 @@ namespace BytecodeTranslator {
       Bpl.Expr targetexp = this.TranslatedExpressions.Pop();

       Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;

       if (idexp != null) {

-        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),

+        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(),

           idexp, sourceexp));

         return;

       } else {

@@ -547,7 +547,7 @@ namespace BytecodeTranslator {
       base.Visit(logicalNot);

       Bpl.Expr exp = TranslatedExpressions.Pop();

       TranslatedExpressions.Push(Bpl.Expr.Unary(

-          TranslationHelper.CciLocationToBoogieToken(logicalNot.Locations),

+          logicalNot.Token(),

           Bpl.UnaryOperator.Opcode.Not, exp));

 

     }

@@ -556,7 +556,7 @@ namespace BytecodeTranslator {
     #region CodeContract Expressions

     public override void Visit(IOldValue oldValue) {

       base.Visit(oldValue);

-      TranslatedExpressions.Push(new Bpl.OldExpr(TranslationHelper.CciLocationToBoogieToken(oldValue.Locations),

+      TranslatedExpressions.Push(new Bpl.OldExpr(oldValue.Token(),

         TranslatedExpressions.Pop()));

     }

     

@@ -564,7 +564,7 @@ namespace BytecodeTranslator {
       if (this.sink.RetVariable == null) {

         throw new TranslationException(String.Format("Don't know what to do with return value {0}", returnValue.ToString()));

       }

-      TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(returnValue.Locations),

+      TranslatedExpressions.Push(new Bpl.IdentifierExpr(returnValue.Token(),

         this.sink.RetVariable));

 

     }

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 6a3ebcad..c24f6df9 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -107,8 +107,8 @@ namespace BytecodeTranslator {
         if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Type rettype = Bpl.Type.Int;

           out_count++;

-          this.sink.RetVariable = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),

-              new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),

+          this.sink.RetVariable = new Bpl.Formal(method.Token(),

+              new Bpl.TypedIdent(method.Type.Token(),

                   "$result", rettype), false);

         } else {

           this.sink.RetVariable = null;

@@ -119,8 +119,8 @@ namespace BytecodeTranslator {
         #region Create 'this' parameter

         in_count++;

         Bpl.Type selftype = Bpl.Type.Int;

-        Bpl.Formal self = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),

-            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),

+        Bpl.Formal self = new Bpl.Formal(method.Token(),

+            new Bpl.TypedIdent(method.Type.Token(),

                 "this", selftype), true);

 

         #endregion

@@ -167,7 +167,7 @@ namespace BytecodeTranslator {
 

 

               Bpl.Requires req

-                  = new Bpl.Requires(TranslationHelper.CciLocationToBoogieToken(pre.Locations),

+                  = new Bpl.Requires(pre.Token(),

                       true, exptravers.TranslatedExpressions.Pop(), "");

               boogiePrecondition.Add(req);

             }

@@ -179,7 +179,7 @@ namespace BytecodeTranslator {
               // Todo: Deal with Descriptions

 

               Bpl.Ensures ens =

-                  new Bpl.Ensures(TranslationHelper.CciLocationToBoogieToken(post.Locations),

+                  new Bpl.Ensures(post.Token(),

                       true, exptravers.TranslatedExpressions.Pop(), "");

               boogiePostcondition.Add(ens);

             }

@@ -206,7 +206,7 @@ namespace BytecodeTranslator {
 

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

 

-        Bpl.Procedure proc = new Bpl.Procedure(TranslationHelper.CciLocationToBoogieToken(method.Locations),

+        Bpl.Procedure proc = new Bpl.Procedure(method.Token(),

             MethodName, // make it unique!

             new Bpl.TypeVariableSeq(),

             new Bpl.VariableSeq(invars), // in

@@ -227,7 +227,7 @@ namespace BytecodeTranslator {
 

         foreach (MethodParameter mparam in formalMap.Values) {

           if (mparam.inParameterCopy != null) {

-            Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(method.Locations);

+            Bpl.IToken tok = method.Token();

             stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

               new Bpl.IdentifierExpr(tok, mparam.outParameterCopy),

               new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));

@@ -258,7 +258,7 @@ namespace BytecodeTranslator {
         #endregion

 

         Bpl.Implementation impl =

-            new Bpl.Implementation(TranslationHelper.CciLocationToBoogieToken(method.Locations),

+            new Bpl.Implementation(method.Token(),

                 MethodName, // make unique

                 new Microsoft.Boogie.TypeVariableSeq(),

                 new Microsoft.Boogie.VariableSeq(invars),

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 38eaf0dc..59812d52 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -66,7 +66,7 @@ namespace BytecodeTranslator {
     /// <returns></returns>

     public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {

       Bpl.LocalVariable v;

-      Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(local.Locations);

+      Bpl.IToken tok = local.Token();

       Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);

       if (!localVarMap.TryGetValue(local, out v)) {

         v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));

@@ -94,7 +94,7 @@ namespace BytecodeTranslator {
       Bpl.GlobalVariable v;

       if (!fieldVarMap.TryGetValue(field, out v)) {

         string fieldname = field.ContainingTypeDefinition.ToString() + "." + field.Name.Value;

-        Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(field.Locations);

+        Bpl.IToken tok = field.Token();

         Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);

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

 

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 8ca54050..ab11f7b7 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -40,10 +40,6 @@ namespace BytecodeTranslator
 

     #region Helper Methods

 

-    Bpl.IToken TokenFor(IStatement statement) {

-      return TranslationHelper.CciLocationToBoogieToken(statement.Locations);

-    }

-

     Bpl.Expr ExpressionFor(IExpression expression) {

       ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);

       etrav.Visit(expression);

@@ -65,13 +61,13 @@ namespace BytecodeTranslator
 

     public override void Visit(IAssertStatement assertStatement) {

       StmtBuilder.Add(

-        new Bpl.AssertCmd(TokenFor(assertStatement), ExpressionFor(assertStatement.Condition))

+        new Bpl.AssertCmd(assertStatement.Token(), ExpressionFor(assertStatement.Condition))

         );

     }

 

     public override void Visit(IAssumeStatement assumeStatement) {

       StmtBuilder.Add(

-        new Bpl.AssertCmd(TokenFor(assumeStatement), ExpressionFor(assumeStatement.Condition))

+        new Bpl.AssertCmd(assumeStatement.Token(), ExpressionFor(assumeStatement.Condition))

         );

     }

 

@@ -89,11 +85,11 @@ namespace BytecodeTranslator
       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

 

-      Bpl.IfCmd ifcmd = new Bpl.IfCmd(TokenFor(conditionalStatement),

+      Bpl.IfCmd ifcmd = new Bpl.IfCmd(conditionalStatement.Token(),

           condTraverser.TranslatedExpressions.Pop(),

-          thenTraverser.StmtBuilder.Collect(TokenFor(conditionalStatement.TrueBranch)),

+          thenTraverser.StmtBuilder.Collect(conditionalStatement.TrueBranch.Token()),

           null,

-          elseTraverser.StmtBuilder.Collect(TokenFor(conditionalStatement.FalseBranch))

+          elseTraverser.StmtBuilder.Collect(conditionalStatement.FalseBranch.Token())

           );

 

       StmtBuilder.Add(ifcmd);

@@ -117,7 +113,7 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) Not Implemented</remarks>

     /// <param name="breakStatement"></param>

     public override void Visit(IBreakStatement breakStatement) {

-      StmtBuilder.Add(new Bpl.BreakCmd(TokenFor(breakStatement), "I dont know"));

+      StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));

     }

 

     /// <summary>

@@ -127,7 +123,7 @@ namespace BytecodeTranslator
     public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {

       if (localDeclarationStatement.InitialValue == null) return;

       var loc = this.sink.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

-      var tok = TokenFor(localDeclarationStatement);

+      var tok = localDeclarationStatement.Token();

       var e = ExpressionFor(localDeclarationStatement.InitialValue);

       StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));

       return;

@@ -139,7 +135,7 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) not implemented</remarks>

     /// <param name="returnStatement"></param>

     public override void Visit(IReturnStatement returnStatement) {

-      Bpl.IToken tok = TokenFor(returnStatement);

+      Bpl.IToken tok = returnStatement.Token();

 

       if (returnStatement.Expression != null) {

         ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);

@@ -152,7 +148,7 @@ namespace BytecodeTranslator
         StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

             new Bpl.IdentifierExpr(tok, this.sink.RetVariable), etrav.TranslatedExpressions.Pop()));

       }

-      StmtBuilder.Add(new Bpl.ReturnCmd(TokenFor(returnStatement)));

+      StmtBuilder.Add(new Bpl.ReturnCmd(returnStatement.Token()));

     }

     #endregion

 

@@ -166,7 +162,7 @@ namespace BytecodeTranslator
     public override void Visit(IGotoStatement gotoStatement) {

       String[] target = new String[1] { gotoStatement.TargetStatement.Label.Value };

 

-      Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(TokenFor(gotoStatement), new Bpl.StringSeq(target));

+      Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target));

 

       StmtBuilder.Add(gotocmd);

     }

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index e27e72c7..756f127f 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -23,7 +23,7 @@ namespace BytecodeTranslator {
     

     /// <summary>

     /// All parameters of the method get an associated in parameter

-    /// in the Boogie procedure.

+    /// in the Boogie procedure except for out parameters.

     /// </summary>

     public Bpl.Formal/*?*/ inParameterCopy;

     

@@ -42,8 +42,8 @@ namespace BytecodeTranslator {
 

       Bpl.Type ptype = Bpl.Type.Int;

 

-      var parameterToken = TranslationHelper.CciLocationToBoogieToken(parameterDefinition.Locations);

-      var typeToken = TranslationHelper.CciLocationToBoogieToken(parameterDefinition.Type.Locations);

+      var parameterToken = parameterDefinition.Token();

+      var typeToken = parameterDefinition.Type.Token();

       var parameterName = parameterDefinition.Name.Value;

 

       if (!parameterDefinition.IsOut) {

@@ -64,16 +64,12 @@ namespace BytecodeTranslator {
 

     /// <summary>

     /// Class containing several static helper functions to convert

-    /// from Cci to Boogie Methodology

+    /// from Cci to Boogie

     /// </summary>

-  class TranslationHelper {

+  static class TranslationHelper {

 

-    public static Bpl.IToken CciLocationToBoogieToken(IEnumerable<ILocation> locations) {

-      Bpl.IToken tok = Bpl.Token.NoToken;

-      return tok;

-    }

-

-    public static Bpl.IToken CciLocationToBoogieToken(ILocation location) {

+    public static Bpl.IToken Token(this IObjectWithLocations objectWithLocations) {

+      //TODO: use objectWithLocations.Locations!

       Bpl.IToken tok = Bpl.Token.NoToken;

       return tok;

     }