Moved the creation of Boogie procedures from the MetadataTraverser to the Sink because a procedure needs to be created for every method called in the translated program and not just the methods defined in the assembly being translated. This means the contract provider is needed only in the sink and not by any of the traversers.

5 files changed, 197 insertions, 177 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 14ec1da2..86162129 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -85,8 +85,8 @@ namespace BytecodeTranslator
       IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;

       if (field != null)

       {

-        //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField)));

-        throw new NotImplementedException();

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field.ResolvedField)));

+        return;

       }

       IArrayIndexer/*?*/ arrayIndexer = addressableExpression.Definition as IArrayIndexer;

       if (arrayIndexer != null)

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index c5dae569..9b895fe3 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -29,18 +29,15 @@ namespace BytecodeTranslator {
 

     public readonly TraverserFactory factory;

 

-    public readonly IContractProvider ContractProvider;

-

     public readonly PdbReader/*?*/ PdbReader;

 

     public Bpl.Variable HeapVariable;

 

 

-    public MetadataTraverser(Sink sink, IContractProvider cp, PdbReader/*?*/ pdbReader)

+    public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader)

       : base() {

       this.sink = sink;

       this.factory = sink.Factory;

-      ContractProvider = cp;

       this.PdbReader = pdbReader;

     }

 

@@ -244,140 +241,62 @@ namespace BytecodeTranslator {
     /// </summary>

     public override void Visit(IMethodDefinition method) {

 

-      Dictionary<IParameterDefinition, MethodParameter> formalMap = new Dictionary<IParameterDefinition, MethodParameter>();

       this.sink.BeginMethod();

 

-      try {

-        #region Create in- and out-parameters

-

-        int in_count = 0;

-        int out_count = 0;

-        MethodParameter mp;

-        foreach (IParameterDefinition formal in method.Parameters) {

-

-          mp = new MethodParameter(formal);

-          if (mp.inParameterCopy != null) in_count++;

-          if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))

-            out_count++;

-          formalMap.Add(formal, mp);

-        }

-        this.sink.FormalMap = formalMap;

-

-        #region Look for Returnvalue

+      var proc = this.sink.FindOrCreateProcedure(method, method.IsStatic);

 

-        if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

-          Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(method.Type);

-          out_count++;

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

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

-                  "$result", rettype), false);

-        } else {

-          this.sink.RetVariable = null;

-        }

-

-        #endregion

+      try {

 

-        Bpl.Formal/*?*/ self = null;

-        #region Create 'this' parameter

-        if (!method.IsStatic) {

-          in_count++;

-          Bpl.Type selftype = Bpl.Type.Int;

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

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

-                  "this", selftype), true);

+        if (method.IsAbstract) {

+          throw new NotImplementedException("abstract methods are not yet implemented");

         }

-        #endregion

-

-        Bpl.Variable[] invars = new Bpl.Formal[in_count];

-        Bpl.Variable[] outvars = new Bpl.Formal[out_count];

 

-        int i = 0;

-        int j = 0;

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

 

-        #region Add 'this' parameter as first in parameter

-        if (!method.IsStatic)

-          invars[i++] = self;

-        #endregion

+        #region Add assignements from In-Params to local-Params

 

-        foreach (MethodParameter mparam in formalMap.Values) {

+        foreach (MethodParameter mparam in this.sink.FormalMap.Values) {

           if (mparam.inParameterCopy != null) {

-            invars[i++] = mparam.inParameterCopy;

-          }

-          if (mparam.outParameterCopy != null) {

-            if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)

-              outvars[j++] = mparam.outParameterCopy;

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

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

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

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

           }

         }

 

-        #region add the returnvalue to out if there is one

-        if (this.sink.RetVariable != null) outvars[j] = this.sink.RetVariable;

         #endregion

 

-        #endregion

-

-        #region Check The Method Contracts

-        Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();

-        Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();

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

-

-        IMethodContract contract = ContractProvider.GetMethodContractFor(method);

-

-        if (contract != null) {

-          try {

-            foreach (IPrecondition pre in contract.Preconditions) {

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

-              exptravers.Visit(pre.Condition); // TODO

-              // Todo: Deal with Descriptions

-

-

-              Bpl.Requires req

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

-                      false, exptravers.TranslatedExpressions.Pop(), "");

-              boogiePrecondition.Add(req);

-            }

-

-            foreach (IPostcondition post in contract.Postconditions) {

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

-

-              exptravers.Visit(post.Condition);

-              // Todo: Deal with Descriptions

-

-              Bpl.Ensures ens =

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

-                      false, exptravers.TranslatedExpressions.Pop(), "");

-              boogiePostcondition.Add(ens);

-            }

-

-            foreach (IAddressableExpression mod in contract.ModifiedVariables) {

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

-              exptravers.Visit(mod);

-

-              Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

+        try {

+          method.Body.Dispatch(stmtTraverser);

+        } catch (TranslationException te) {

+          throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());

+        } catch {

+          throw;

+        }

 

-              if (idexp == null) {

-                throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));

-              }

-              boogieModifies.Add(idexp);

-            }

-          } catch (TranslationException te) {

-            throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());

-          } catch {

-            throw;

-          }

+        #region Create Local Vars For Implementation

+        List<Bpl.Variable> vars = new List<Bpl.Variable>();

+        foreach (MethodParameter mparam in this.sink.FormalMap.Values) {

+          if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))

+            vars.Add(mparam.outParameterCopy);

+        }

+        foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

+          vars.Add(v);

         }

 

+        Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

         #endregion

 

-        string MethodName = TranslationHelper.CreateUniqueMethodName(method);

+        Bpl.Implementation impl =

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

+                proc.Name,

+                new Microsoft.Boogie.TypeVariableSeq(),

+                proc.InParams,

+                proc.OutParams,

+                vseq,

+                stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));

 

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

-            MethodName, // make it unique!

-            new Bpl.TypeVariableSeq(),

-            new Bpl.VariableSeq(invars), // in

-            new Bpl.VariableSeq(outvars), // out

-            boogiePrecondition,

-            boogieModifies,

-            boogiePostcondition);

+        impl.Proc = proc;

 

         // Don't need an expression translator because there is a limited set of things

         // that can appear as arguments to custom attributes

@@ -407,62 +326,11 @@ namespace BytecodeTranslator {
               args[argIndex++] = o;

             }

           }

-          proc.AddAttribute(attrName, args);

-        }

-

-        this.sink.TranslatedProgram.TopLevelDeclarations.Add(proc);

-

-        if (method.IsAbstract) {

-          throw new NotImplementedException("abstract methods are not yet implemented");

-        }

-

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

-

-        #region Add assignements from In-Params to local-Params

-

-        foreach (MethodParameter mparam in formalMap.Values) {

-          if (mparam.inParameterCopy != null) {

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

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

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

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

-          }

-        }

-

-        #endregion

-

-        try {

-          method.ResolvedMethod.Body.Dispatch(stmtTraverser);

-        } catch (TranslationException te) {

-          throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());

-        } catch {

-          throw;

+          impl.AddAttribute(attrName, args);

         }

 

-        #region Create Local Vars For Implementation

-        List<Bpl.Variable> vars = new List<Bpl.Variable>();

-        foreach (MethodParameter mparam in formalMap.Values) {

-          if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))

-            vars.Add(mparam.outParameterCopy);

-        }

-        foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

-          vars.Add(v);

-        }

-

-        Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

-        #endregion

-

-        Bpl.Implementation impl =

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

-                MethodName, // make unique

-                new Microsoft.Boogie.TypeVariableSeq(),

-                new Microsoft.Boogie.VariableSeq(invars),

-                new Microsoft.Boogie.VariableSeq(outvars),

-                vseq,

-                stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));

-

-        impl.Proc = proc;

         this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

+

       } catch (TranslationException te) {

         throw new NotImplementedException(te.ToString());

       } catch {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 02df9b32..1fefbe97 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -25,10 +25,12 @@ namespace BytecodeTranslator {
       get { return this.factory; }

     }

     readonly TraverserFactory factory;

+    public readonly IContractProvider ContractProvider;

 

-    public Sink(TraverserFactory factory, HeapFactory heapFactory) {

+    public Sink(TraverserFactory factory, HeapFactory heapFactory, IContractProvider contractProvider) {

       this.factory = factory;

       var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?

+      this.ContractProvider = contractProvider;

       if (this.TranslatedProgram == null)

         this.TranslatedProgram = new Bpl.Program();

     }

@@ -121,13 +123,160 @@ namespace BytecodeTranslator {
       return v;

     }

     /// <summary>

-    /// The keys to the table are tuples of the containing type (its interned key) and the name of the field. That

-    /// should uniquely identify each field.

+    /// The keys to the table are the interned key of the field.

     /// </summary>

     private Dictionary<uint, Bpl.Variable> declaredFields = new Dictionary<uint, Bpl.Variable>();

 

+    public Bpl.Procedure FindOrCreateProcedure(IMethodReference method, bool isStatic) {

+      Bpl.Procedure proc;

+      var key = method.InternedKey;

+      if (!this.declaredMethods.TryGetValue(key, out proc)) {

+        #region Create in- and out-parameters

+

+        int in_count = 0;

+        int out_count = 0;

+        MethodParameter mp;

+        var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();

+        foreach (IParameterDefinition formal in method.Parameters) {

+

+          mp = new MethodParameter(formal);

+          if (mp.inParameterCopy != null) in_count++;

+          if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))

+            out_count++;

+          formalMap.Add(formal, mp);

+        }

+        this.FormalMap = formalMap;

+

+        #region Look for Returnvalue

+

+        if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

+          Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(method.Type);

+          out_count++;

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

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

+                  "$result", rettype), false);

+        } else {

+          this.RetVariable = null;

+        }

+

+        #endregion

+

+        Bpl.Formal/*?*/ self = null;

+        #region Create 'this' parameter

+        if (!isStatic) {

+          in_count++;

+          Bpl.Type selftype = Bpl.Type.Int;

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

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

+                  "this", selftype), true);

+        }

+        #endregion

+

+        Bpl.Variable[] invars = new Bpl.Formal[in_count];

+        Bpl.Variable[] outvars = new Bpl.Formal[out_count];

+

+        int i = 0;

+        int j = 0;

+

+        #region Add 'this' parameter as first in parameter

+        if (!isStatic)

+          invars[i++] = self;

+        #endregion

+

+        foreach (MethodParameter mparam in formalMap.Values) {

+          if (mparam.inParameterCopy != null) {

+            invars[i++] = mparam.inParameterCopy;

+          }

+          if (mparam.outParameterCopy != null) {

+            if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)

+              outvars[j++] = mparam.outParameterCopy;

+          }

+        }

+

+        #region add the returnvalue to out if there is one

+        if (this.RetVariable != null) outvars[j] = this.RetVariable;

+        #endregion

+

+        #endregion

+

+        #region Check The Method Contracts

+        Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();

+        Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();

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

+

+        IMethodContract contract = ContractProvider.GetMethodContractFor(method);

+

+        if (contract != null) {

+          try {

+            foreach (IPrecondition pre in contract.Preconditions) {

+              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null);

+              exptravers.Visit(pre.Condition); // TODO

+              // Todo: Deal with Descriptions

+

+

+              Bpl.Requires req

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

+                      false, exptravers.TranslatedExpressions.Pop(), "");

+              boogiePrecondition.Add(req);

+            }

+

+            foreach (IPostcondition post in contract.Postconditions) {

+              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null);

+

+              exptravers.Visit(post.Condition);

+              // Todo: Deal with Descriptions

+

+              Bpl.Ensures ens =

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

+                      false, exptravers.TranslatedExpressions.Pop(), "");

+              boogiePostcondition.Add(ens);

+            }

+

+            foreach (IAddressableExpression mod in contract.ModifiedVariables) {

+              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null);

+              exptravers.Visit(mod);

+

+              Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

+

+              if (idexp == null) {

+                throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));

+              }

+              boogieModifies.Add(idexp);

+            }

+          } catch (TranslationException te) {

+            throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());

+          } catch {

+            throw;

+          }

+        }

+

+        #endregion

+

+        string MethodName = TranslationHelper.CreateUniqueMethodName(method);

+

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

+            MethodName,

+            new Bpl.TypeVariableSeq(),

+            new Bpl.VariableSeq(invars), // in

+            new Bpl.VariableSeq(outvars), // out

+            boogiePrecondition,

+            boogieModifies,

+            boogiePostcondition);

+

+

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

+        this.declaredMethods.Add(key, proc);

+      }

+      return proc;

+    }

+    /// <summary>

+    /// The keys to the table are the interned key of the field.

+    /// </summary>

+    private Dictionary<uint, Bpl.Procedure> declaredMethods = new Dictionary<uint, Bpl.Procedure>();

+

     public void BeginMethod() {

       this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

+      this.FormalMap = new Dictionary<IParameterDefinition, MethodParameter>();

     }

 

     public Dictionary<ITypeDefinition, HashSet<Bpl.Constant>> delegateTypeToDelegates =

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 707ab4e5..8667e1a0 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -99,6 +99,9 @@ namespace BytecodeTranslator {
       s = s.Replace(',', '$');

       s = s.TrimEnd(')');

       s = s.Replace("[]", "array");

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

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

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

       return s;

     }

 

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 6efe04e2..8162af9e 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -20,7 +20,7 @@ namespace BytecodeTranslator {
   public abstract class TraverserFactory {

     public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, PdbReader/*?*/ pdbReader, HeapFactory heapFactory)

     {

-      return new MetadataTraverser(new Sink(this, heapFactory), contractProvider, pdbReader);

+      return new MetadataTraverser(new Sink(this, heapFactory, contractProvider), pdbReader);

     }

     public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader) {

       return new StatementTraverser(sink, pdbReader);