Changes needed to translate both contracts and method bodies. The Statement and Expression traversers need to have a mode that controls two things:

1. Parameters occurring in contracts are translated as the corresponding in-parameter of the corresponding procedure. Parameters occurring in method bodies are translated as the corresponding out-parameter of the corresponding procedure.

2. Method calls in method bodies are translated as call commands. Method calls in contracts are translated as function calls.

6 files changed, 46 insertions, 47 deletions

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index a343402e..b0749e6c 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -20,14 +20,14 @@ namespace BytecodeTranslator {
 

   public class CLRSemantics : TraverserFactory {

 

-    public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {

-      return new CLRExpressionSemantics(sink, statementTraverser);

+    public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

+      return new CLRExpressionSemantics(sink, statementTraverser, contractContext);

     }

 

     public class CLRExpressionSemantics : ExpressionTraverser {

 

-      public CLRExpressionSemantics(Sink sink, StatementTraverser/*?*/ statementTraverser)

-        : base(sink, statementTraverser) { }

+      public CLRExpressionSemantics(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext)

+        : base(sink, statementTraverser, contractContext) { }

 

       public override void Visit(IDivision division) {

         this.Visit(division.LeftOperand);

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index afdb86e0..7f236ebb 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -34,22 +34,23 @@ namespace BytecodeTranslator
     protected readonly StatementTraverser StmtTraverser;

 

     private Bpl.Expr assignmentSourceExpr;

+    private bool contractContext;

 

     #region Constructors

 

-    /// <summary>

-    /// Use this constructor for translating expressions that do *not* occur

-    /// within the context of the statements in a method body.

-    /// </summary>

-    public ExpressionTraverser(Sink sink)

-      : this(sink, null)

-    { }

+    ///// <summary>

+    ///// Use this constructor for translating expressions that do *not* occur

+    ///// within the context of the statements in a method body.

+    ///// </summary>

+    //public ExpressionTraverser(Sink sink)

+    //  : this(sink, null)

+    //{ }

 

     /// <summary>

     /// Use this constructor for translating expressions that do occur within

     /// the context of the statements in a method body.

     /// </summary>

-    public ExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser)

+    public ExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext)

     {

       this.sink = sink;

       ArrayContentsVariable = sink.ArrayContentsVariable;

@@ -58,6 +59,7 @@ namespace BytecodeTranslator
       TranslatedExpressions = new Stack<Bpl.Expr>();

 

       assignmentSourceExpr = null;

+      this.contractContext = contractContext;

     }

 

     #endregion

@@ -80,7 +82,7 @@ namespace BytecodeTranslator
       IParameterDefinition/*?*/ param = addressableExpression.Definition as IParameterDefinition;

       if (param != null)

       {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindParameterVariable(param)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindParameterVariable(param, this.contractContext)));

         return;

       }

       IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;

@@ -119,7 +121,7 @@ namespace BytecodeTranslator
         IParameterDefinition pd = be.Definition as IParameterDefinition;

         if (pd != null)

         {

-          var pv = this.sink.FindParameterVariable(pd);

+          var pv = this.sink.FindParameterVariable(pd, this.contractContext);

           TranslatedExpressions.Push(Bpl.Expr.Ident(pv));

           return;

         }

@@ -198,7 +200,7 @@ namespace BytecodeTranslator
             IParameterDefinition pd = be.Definition as IParameterDefinition;

             if (pd != null)

             {

-              var pv = this.sink.FindParameterVariable(pd);

+              var pv = this.sink.FindParameterVariable(pd, this.contractContext);

               TranslatedExpressions.Push(Bpl.Expr.Ident(pv));

               return;

             }

@@ -229,7 +231,7 @@ namespace BytecodeTranslator
       IParameterDefinition param = targetExpression.Definition as IParameterDefinition;

       if (param != null)

       {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindParameterVariable(param)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindParameterVariable(param, this.contractContext)));

         return;

       }

       #endregion

@@ -279,7 +281,7 @@ namespace BytecodeTranslator
       IParameterDefinition param = boundExpression.Definition as IParameterDefinition;

       if (param != null)

       {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindParameterVariable(param)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindParameterVariable(param, this.contractContext)));

         return;

       }

       #endregion

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 5a2b27d0..2c461739 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -128,13 +128,13 @@ namespace BytecodeTranslator {
     /// <param name="param"></param>

     /// <remarks>STUB</remarks>

     /// <returns></returns>

-    public Bpl.Variable FindParameterVariable(IParameterDefinition param) {

+    public Bpl.Variable FindParameterVariable(IParameterDefinition param, bool contractContext) {

       MethodParameter mp;

       ProcedureInfo procAndFormalMap;

       this.declaredMethods.TryGetValue(param.ContainingSignature, out procAndFormalMap);

       var formalMap = procAndFormalMap.FormalMap;

       formalMap.TryGetValue(param, out mp);

-      return mp.outParameterCopy;

+      return contractContext ? mp.inParameterCopy : mp.outParameterCopy;

     }

 

     public Bpl.Variable FindOrCreateFieldVariable(IFieldReference field) {

@@ -288,32 +288,27 @@ namespace BytecodeTranslator {
 

         if (contract != null) {

           try {

+

             foreach (IPrecondition pre in contract.Preconditions) {

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

+              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);

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

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

               // Todo: Deal with Descriptions

-

-

-              Bpl.Requires req

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

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

+              var 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);

-

+              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);

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

               exptravers.Visit(post.Condition);

               // Todo: Deal with Descriptions

-

-              Bpl.Ensures ens =

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

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

+              var 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);

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

               exptravers.Visit(mod);

 

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

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index bff181c5..a062fca1 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -32,12 +32,14 @@ namespace BytecodeTranslator
     private readonly Bpl.Variable ArrayLengthVariable;

 

     public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

+    private bool contractContext;

 

     #region Constructors

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

+    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

       this.sink = sink;

       this.factory = sink.Factory;

       PdbReader = pdbReader;

+      this.contractContext = contractContext;

 

       ArrayContentsVariable = sink.ArrayContentsVariable;

       ArrayLengthVariable = sink.ArrayLengthVariable;

@@ -47,7 +49,7 @@ namespace BytecodeTranslator
     #region Helper Methods

 

     Bpl.Expr ExpressionFor(IExpression expression) {

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

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

       etrav.Visit(expression);

       Contract.Assert(etrav.TranslatedExpressions.Count == 1);

       return etrav.TranslatedExpressions.Pop();

@@ -110,10 +112,10 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) Works, but still a stub</remarks>

     /// <param name="conditionalStatement"></param>

     public override void Visit(IConditionalStatement conditionalStatement) {

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

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

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

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

 

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

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

       condTraverser.Visit(conditionalStatement.Condition);

       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

@@ -136,7 +138,7 @@ namespace BytecodeTranslator
     /// <remarks> TODO: might be wrong for the general case</remarks>

     public override void Visit(IExpressionStatement expressionStatement) {

 

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

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

       etrav.Visit(expressionStatement.Expression);

     }

 

@@ -171,7 +173,7 @@ namespace BytecodeTranslator
       Bpl.IToken tok = returnStatement.Token();

 

       if (returnStatement.Expression != null) {

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

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

         etrav.Visit(returnStatement.Expression);

 

         if (this.sink.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 8162af9e..ba465067 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -22,11 +22,11 @@ namespace BytecodeTranslator {
     {

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

     }

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

-      return new StatementTraverser(sink, pdbReader);

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

+      return new StatementTraverser(sink, pdbReader, contractContext);

     }

-    public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {

-      return new ExpressionTraverser(sink, statementTraverser);

+    public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

+      return new ExpressionTraverser(sink, statementTraverser, contractContext);

     }

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index 872466bb..1710b2a6 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -78,8 +78,8 @@ namespace BytecodeTranslator {
 

     }

 

-    public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {

-      return new WholeProgramExpressionSemantics(this, sink, statementTraverser);

+    public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

+      return new WholeProgramExpressionSemantics(this, sink, statementTraverser, contractContext);

     }

 

     /// <summary>

@@ -92,8 +92,8 @@ namespace BytecodeTranslator {
       readonly WholeProgram parent;

       readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes;

 

-      public WholeProgramExpressionSemantics(WholeProgram parent, Sink sink, StatementTraverser/*?*/ statementTraverser)

-        : base(sink, statementTraverser) {

+      public WholeProgramExpressionSemantics(WholeProgram parent, Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext)

+        : base(sink, statementTraverser, contractContext) {

         this.parent = parent;

         this.subTypes = parent.subTypes;

       }