If a method has been translated as a function, generate a function call and

not a procedure call for calls to the method.
Use the Location (full path) instead of just the file name for source locations.

3 files changed, 46 insertions, 29 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 73a5951a..d1708608 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -544,27 +544,30 @@ namespace BytecodeTranslator
       }

       #endregion

 

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

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

-        Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

-        Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);

-        if (resolvedMethod.Type is IGenericTypeParameter) {

-          Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

-          toBoxed[unboxed] = boxed;

-          outvars.Add(boxed);

-        }

-        else {

-          outvars.Add(unboxed);

-        }

-        TranslatedExpressions.Push(unboxed);

-      }

       var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

       string methodname = proc.Name;

-

+      var translateAsFunctionCall = proc is Bpl.Function;

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

       Bpl.QKeyValue attrib = null;

-      foreach (var a in resolvedMethod.Attributes) {

-        if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

-          attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

+

+      if (!translateAsFunctionCall) {

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

+          Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

+          Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);

+          if (resolvedMethod.Type is IGenericTypeParameter) {

+            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

+            toBoxed[unboxed] = boxed;

+            outvars.Add(boxed);

+          } else {

+            outvars.Add(unboxed);

+          }

+          TranslatedExpressions.Push(unboxed);

+        }

+

+        foreach (var a in resolvedMethod.Attributes) {

+          if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

+            attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

+          }

         }

       }

 

@@ -599,13 +602,24 @@ namespace BytecodeTranslator
         else {

           this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

         }

-      }

-      else {

-        if (attrib != null)

-          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

-        else

-          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

-        this.StmtTraverser.StmtBuilder.Add(call);

+      } else {

+        if (translateAsFunctionCall) {

+          var func = proc as Bpl.Function;

+          var exprSeq = new Bpl.ExprSeq();

+          foreach (var e in inexpr) {

+            exprSeq.Add(e);

+          }

+          var callFunction = new Bpl.NAryExpr(cloc, new Bpl.FunctionCall(func), exprSeq);

+          this.TranslatedExpressions.Push(callFunction);

+          return;

+

+        } else {

+          if (attrib != null)

+            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

+          else

+            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

+          this.StmtTraverser.StmtBuilder.Add(call);

+        }

       }

 

       foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index b1be6294..e300d3b5 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -289,6 +289,8 @@ namespace BytecodeTranslator {
         Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

         #endregion

 

+        var translatedBody = stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken);

+

         #region Add implementation to Boogie program

         if (proc != null) {

           Bpl.Implementation impl =

@@ -298,13 +300,14 @@ namespace BytecodeTranslator {
                   decl.InParams,

                   decl.OutParams,

                   vseq,

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

+                  translatedBody);

 

           impl.Proc = proc;

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

         } else { // method is translated as a function

-          //Bpl.Function func = decl as Bpl.Function;

-          //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), new List<Bpl.Block>{ new Bpl.Block(

+          //var func = decl as Bpl.Function;

+          //Contract.Assume(func != null);

+          //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), translatedBody.BigBlocks);

         }

         #endregion

 

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 0e13c510..d26f540d 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -97,7 +97,7 @@ namespace BytecodeTranslator
       if (this.PdbReader != null) {

         var slocs = this.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);

         foreach (var sloc in slocs) {

-          fileName = sloc.Document.Name.Value;

+          fileName = sloc.Document.Location;

           lineNumber = sloc.StartLine;

           break;

         }