Cleaned up the sink: removed the OutVars, which was state the sink needed only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is *not* by reference and is *not* an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure.

5 files changed, 71 insertions, 70 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 041998fa..108c0fd1 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -96,6 +96,15 @@ namespace BytecodeTranslator {
     }

 

     public override void Visit(IAddressDereference addressDereference) {

+      IBoundExpression be = addressDereference.Address as IBoundExpression;

+      if (be != null) {

+        IParameterDefinition pd = be.Definition as IParameterDefinition;

+        if (pd != null) {

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

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

+          return;

+        }

+      }

       this.Visit(addressDereference.Address);

       throw new NotImplementedException();

     }

@@ -123,6 +132,18 @@ namespace BytecodeTranslator {
           this.Visit(addressOf.Expression);

           return;

         }

+        IConversion/*?*/ conversion = deref.Address as IConversion;

+        if (conversion != null) {

+          IBoundExpression be = conversion.ValueToConvert as IBoundExpression;

+          if (be != null) {

+            IParameterDefinition pd = be.Definition as IParameterDefinition;

+            if (pd != null) {

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

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

+              return;

+            }

+          }

+        }

         if (targetExpression.Instance != null) {

           // TODO

           throw new NotImplementedException("targetExpr->AddrDeRef->InstanceNull");

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index bba3515a..6a3ebcad 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -41,47 +41,10 @@ namespace BytecodeTranslator {
       ContractProvider = cp;

     }

 

-

     public Bpl.Program TranslatedProgram {

       get { return this.sink.TranslatedProgram; }

     }

 

-    #region Method Helpers

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="param"></param>

-    /// <remarks> (mschaef) only a stub </remarks>

-    private MethodParameter CreateBoogieParameter(IParameterDefinition param) {

-      MethodParameter mparam = new MethodParameter();

-

-      Bpl.Type ptype = Bpl.Type.Int;

-

-      Bpl.Formal v = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

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

-              param.Name.Value, ptype), false);

-

-      Bpl.Formal v_in = null;

-      if (!param.IsOut) {

-        v_in = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

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

-                param.Name.Value + "$in", ptype), true);

-      }

-      Bpl.Formal v_out = null;

-      if (param.IsByReference || param.IsOut) {

-        v_out = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

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

-                param.Name.Value + "$out", ptype), false);

-      }

-      mparam.localParameter = v;

-      mparam.inParameterCopy = v_in;

-      mparam.outParameterCopy = v_out;

-

-      return mparam;

-    }

-

-    #endregion Method Helpers

-

     #region Overrides

 

     public override void Visit(IModule module) {

@@ -130,9 +93,10 @@ namespace BytecodeTranslator {
         MethodParameter mp;

         foreach (IParameterDefinition formal in method.ResolvedMethod.Parameters) {

 

-          mp = CreateBoogieParameter(formal);

+          mp = new MethodParameter(formal);

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

-          if (mp.outParameterCopy != null) out_count++;

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

+            out_count++;

           formalMap.Add(formal, mp);

         }

         this.sink.FormalMap = formalMap;

@@ -176,8 +140,8 @@ namespace BytecodeTranslator {
             invars[i++] = mparam.inParameterCopy;

           }

           if (mparam.outParameterCopy != null) {

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

-            this.sink.OutVars.Add(mparam);

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

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

           }

         }

 

@@ -265,7 +229,7 @@ namespace BytecodeTranslator {
           if (mparam.inParameterCopy != null) {

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

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

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

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

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

           }

         }

@@ -281,17 +245,16 @@ namespace BytecodeTranslator {
         }

 

         #region Create Local Vars For Implementation

-        //Todo: (mschaef) hack, there must be a better way to copy this

-        Bpl.Variable[] vars = new Bpl.Variable[this.sink.LocalVarMap.Values.Count + formalMap.Values.Count];

-        i = 0;

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

-          vars[i++] = v;

-        }

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

         foreach (MethodParameter mparam in formalMap.Values) {

-          vars[i++] = mparam.localParameter;

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

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

         #endregion

 

         Bpl.Implementation impl =

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 7765489a..38eaf0dc 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -38,7 +38,6 @@ namespace BytecodeTranslator {
     public Bpl.Variable ThisVariable = TranslationHelper.TempThisVar();

     public Bpl.Variable RetVariable;

     public readonly Bpl.Program TranslatedProgram = new Bpl.Program();

-    internal List<MethodParameter> OutVars = new List<MethodParameter>();

 

     /// <summary>

     /// Creates a fresh local var of the given Type and adds it to the

@@ -85,7 +84,7 @@ namespace BytecodeTranslator {
     public Bpl.Variable FindParameterVariable(IParameterDefinition param) {

       MethodParameter mp;

       this.FormalMap.TryGetValue(param, out mp);

-      return mp.localParameter;

+      return mp.outParameterCopy;

     }

     public Dictionary<IParameterDefinition, MethodParameter> FormalMap = null;

 

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index c528e846..8ca54050 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -141,13 +141,6 @@ namespace BytecodeTranslator
     public override void Visit(IReturnStatement returnStatement) {

       Bpl.IToken tok = TokenFor(returnStatement);

 

-      #region Copy values of all out parameters to outvariables

-      foreach (MethodParameter mp in this.sink.OutVars) {

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

-          new Bpl.IdentifierExpr(tok, mp.outParameterCopy), new Bpl.IdentifierExpr(tok, mp.localParameter)));

-      }

-      #endregion

-

       if (returnStatement.Expression != null) {

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

         etrav.Visit(returnStatement.Expression);

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index d544bfb8..e27e72c7 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -20,20 +20,45 @@ using Bpl = Microsoft.Boogie;
 namespace BytecodeTranslator {

 

   public class MethodParameter {

-    public MethodParameter() {

-      localParameter = null;

-      inParameterCopy = null;

-      outParameterCopy = null;

-    }

+    

+    /// <summary>

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

+    /// in the Boogie procedure.

+    /// </summary>

+    public Bpl.Formal/*?*/ inParameterCopy;

+    

+    /// <summary>

+    /// A local variable when the underlyingParameter is an in parameter

+    /// and a formal (out) parameter when the underlyingParameter is

+    /// a ref or out parameter.

+    /// </summary>

+    public Bpl.Variable outParameterCopy;

+

+    public IParameterDefinition underlyingParameter;

 

-    public Bpl.Formal localParameter;

-    public Bpl.Formal inParameterCopy;

-    public Bpl.Formal outParameterCopy;

+    public MethodParameter(IParameterDefinition parameterDefinition) {

+

+      this.underlyingParameter = parameterDefinition;

+

+      Bpl.Type ptype = Bpl.Type.Int;

+

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

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

+      var parameterName = parameterDefinition.Name.Value;

+

+      if (!parameterDefinition.IsOut) {

+        this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);

+      }

+      if (parameterDefinition.IsByReference || parameterDefinition.IsOut) {

+        this.outParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$out", ptype), false);

+      } else {

+        this.outParameterCopy = new Bpl.LocalVariable(parameterToken, new Bpl.TypedIdent(typeToken, parameterName, ptype));

+      }

+      

+    }

 

     public override string ToString() {

-      if (this.inParameterCopy != null)

-        return this.inParameterCopy.Name;

-      return base.ToString();

+      return this.underlyingParameter.Name.Value;

     }

   }