Changed calls to Debug.Assert to Contract.Assert.

Suppress source contexts for empty statements.
Added a "whole program" option. When that is specified, then virtual calls are translated into a series of if-statements that test the dynamic type of the receiver and call the appropriate method. This is done only for subtypes that are defined in the CUA (Code Under Analysis -- which currently consists of just the one assembly being translated). [Note: currently the dynamic type is not implemented. That is next.]

11 files changed, 272 insertions, 15 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index ee7e1756..86fc4a5d 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -123,6 +123,7 @@
     <Compile Include="TranslationException.cs" />

     <Compile Include="TranslationHelper.cs" />

     <Compile Include="TraverserFactory.cs" />

+    <Compile Include="WholeProgram.cs" />

   </ItemGroup>

   <ItemGroup>

     <Content Include="Readme.txt" />

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 86162129..82e37212 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -16,6 +16,7 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;

 

 using Bpl = Microsoft.Boogie;

+using System.Diagnostics.Contracts;

 

 

 namespace BytecodeTranslator

@@ -107,7 +108,7 @@ namespace BytecodeTranslator
         //TODO

         throw new NotImplementedException();

       }

-      Debug.Assert(addressableExpression.Definition is IThisReference);

+      Contract.Assert(addressableExpression.Definition is IThisReference);

     }

 

     public override void Visit(IAddressDereference addressDereference)

@@ -148,7 +149,7 @@ namespace BytecodeTranslator
           selectExprs.Add(currSelectExpr);

           currIndexExpr = e;

         }

-        Debug.Assert(selectExprs.Count == indexExprs.Count);

+        Contract.Assert(selectExprs.Count == indexExprs.Count);

         Bpl.Expr currentStoreExpr = assignmentSourceExpr;

         for (int i = selectExprs.Count - 1; i >= 0; i--)

         {

@@ -482,6 +483,7 @@ namespace BytecodeTranslator
             attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

           }

         }

+

         Bpl.CallCmd call;

         if (attrib != null)

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

@@ -503,7 +505,7 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) Works, but still a stub </remarks>

     /// <param name="assignment"></param>

     public override void Visit(IAssignment assignment) {

-      Debug.Assert(TranslatedExpressions.Count == 0);

+      Contract.Assert(TranslatedExpressions.Count == 0);

 

       #region Transform Right Hand Side ...

       this.Visit(assignment.Source);

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 9b895fe3..bb2c08f2 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -15,6 +15,7 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;

 

 using Bpl = Microsoft.Boogie;

+using System.Diagnostics.Contracts;

 

 

 namespace BytecodeTranslator {

@@ -61,7 +62,7 @@ namespace BytecodeTranslator {
 

     private void CreateDispatchMethod(ITypeDefinition type)

     {

-      System.Diagnostics.Debug.Assert(type.IsDelegate);

+      Contract.Assert(type.IsDelegate);

       IMethodDefinition method = null;

       foreach (IMethodDefinition m in type.Methods)

       {

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 0e26be2a..44a404d0 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -29,6 +29,9 @@ namespace BytecodeTranslator {
     [OptionDescription("Heap representation to use", ShortForm = "heap")]

     public HeapRepresentation heapRepresentation = HeapRepresentation.general;

 

+    [OptionDescription("Translate using whole-program assumptions", ShortForm = "whole")]

+    public bool wholeProgram = false;

+

   }

 

   public class BCT {

@@ -52,6 +55,7 @@ namespace BytecodeTranslator {
       var assemblyName = String.IsNullOrEmpty(options.assembly) ? options.GeneralArguments[0] : options.assembly;

 

       try {

+

         HeapFactory heap;

         switch (options.heapRepresentation) {

           case Options.HeapRepresentation.splitFields:

@@ -70,7 +74,9 @@ namespace BytecodeTranslator {
             Console.WriteLine("Unknown setting for /heap");

             return 1;

         }

-        result = TranslateAssembly(assemblyName, heap, options.libpaths);

+

+        result = TranslateAssembly(assemblyName, heap, options.libpaths, options.wholeProgram);

+

       } catch (Exception e) { // swallow everything and just return an error code

         Console.WriteLine("The byte-code translator failed with uncaught exception: {0}", e.Message);

         Console.WriteLine("Stack trace: {0}", e.StackTrace);

@@ -79,7 +85,7 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory, List<string>/*?*/ libPaths) {

+    public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory, List<string> libPaths, bool wholeProgram) {

 

       var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment(libPaths != null ? libPaths : IteratorHelper.GetEmptyEnumerable<string>(), true, true);

       Host = host;

@@ -101,9 +107,12 @@ namespace BytecodeTranslator {
 

       module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader);

 

-      #region Pass 3: Translate the code model to BPL

-      //tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);

-      var factory = new CLRSemantics();

+      #region Translate the code model to BPL

+      TraverserFactory factory;

+      if (wholeProgram)

+        factory = new WholeProgram();

+      else

+        factory = new CLRSemantics();

       MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader, heapFactory);

       TranslationHelper.tmpVarCounter = 0;

       assembly = module as IAssembly;

@@ -111,7 +120,8 @@ namespace BytecodeTranslator {
         translator.Visit(assembly);

       else

         translator.Visit(module);

-      #endregion Pass 3: Translate the code model to BPL

+      #endregion

+

       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(module.Name + ".bpl");

       Prelude.Emit(writer);

       translator.TranslatedProgram.Emit(writer);

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index d29fe0e8..be104448 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -69,6 +69,7 @@ namespace BytecodeTranslator
     }

 

     private void EmitSourceContext(IStatement statement) {

+      if (statement is IEmptyStatement) return;

       var tok = statement.Token();

       string fileName = null;

       int lineNumber = 0;

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
new file mode 100644
index 00000000..be3c06a5
--- /dev/null
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -0,0 +1,238 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+using System.Diagnostics.Contracts;

+

+namespace BytecodeTranslator {

+  class WholeProgram : TraverserFactory {

+

+    /// <summary>

+    /// Table to be filled by the metadata traverser when it first gets to an assembly.

+    /// [TODO: It should be full set of assemblies that are being translated (CUA).]

+    /// 

+    /// The table lists the direct supertypes of all type definitions that it encounters during the

+    /// traversal. (But the table is organized so that subTypes[T] is the list of type definitions

+    /// that are direct subtypes of T.)

+    /// </summary>

+    readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes = new Dictionary<ITypeReference, List<ITypeReference>>();

+

+    public override MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, PdbReader pdbReader, HeapFactory heapFactory) {

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

+    }

+

+    public class WholeProgramMetadataSemantics : MetadataTraverser {

+

+      readonly WholeProgram parent;

+      readonly Sink sink;

+

+      /// <summary>

+      /// TODO: Need to have this populated before any of the assemblies in the CUA are traversed.

+      /// </summary>

+      readonly Dictionary<IAssembly, bool> codeUnderAnalysis = new Dictionary<IAssembly, bool>();

+

+      public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, PdbReader/*?*/ pdbReader)

+        : base(sink, pdbReader) {

+        this.parent = parent;

+        this.sink = sink;

+      }

+

+      public override void Visit(IAssembly assembly) {

+

+        #region When doing whole-program analysis, traverse the assembly gathering type information

+        this.codeUnderAnalysis.Add(assembly, true);

+        var typeRecorder = new RecordSubtypes(this.parent.subTypes);

+        typeRecorder.Visit(assembly);

+        #endregion

+

+        base.Visit(assembly);

+

+      }

+      

+      class RecordSubtypes : BaseMetadataTraverser {

+

+        Dictionary<ITypeReference, List<ITypeReference>> subTypes;

+

+        public RecordSubtypes(Dictionary<ITypeReference, List<ITypeReference>> subTypes) {

+          this.subTypes = subTypes;

+        }

+

+        public override void Visit(ITypeDefinition typeDefinition) {

+          foreach (var baseClass in typeDefinition.BaseClasses) {

+            if (!this.subTypes.ContainsKey(baseClass)) {

+              this.subTypes[baseClass] = new List<ITypeReference>();

+            }

+            this.subTypes[baseClass].Add(typeDefinition);

+          }

+          base.Visit(typeDefinition);

+        }

+      }

+

+    }

+

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

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

+    }

+

+    /// <summary>

+    /// implement virtual method calls to methods defined in the CUA (code under analysis, i.e.,

+    /// the set of assemblies being translated) by a "switch statement" that dispatches to the

+    /// most derived type's method. I.e., make explicit the dynamic dispatch mechanism.

+    /// </summary>

+    public class WholeProgramExpressionSemantics : CLRSemantics.CLRExpressionSemantics {

+

+      readonly WholeProgram parent;

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

+

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

+        : base(sink, statementTraverser) {

+        this.parent = parent;

+        this.subTypes = parent.subTypes;

+      }

+

+      public override void Visit(IMethodCall methodCall) {

+

+        if (!methodCall.IsVirtualCall) {

+          base.Visit(methodCall);

+          return;

+        }

+        var containingType = methodCall.MethodToCall.ContainingType;

+        List<ITypeReference> subTypesOfContainingType;

+        if (!this.subTypes.TryGetValue(containingType, out subTypesOfContainingType)) {

+          base.Visit(methodCall);

+          return;

+        }

+        Contract.Assert(0 < subTypesOfContainingType.Count);

+        Contract.Assert(!methodCall.IsStaticCall);

+        var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;

+        Contract.Assert(!resolvedMethod.IsConstructor);

+        List<IMethodReference> overrides = new List<IMethodReference>();

+        FindOverrides(containingType, resolvedMethod, overrides);

+        if (0 == overrides.Count) {

+          base.Visit(methodCall);

+          return;

+        }

+

+        #region Translate In Parameters

+

+        var inexpr = new List<Bpl.Expr>();

+        #region Create the 'this' argument for the function call

+        this.Visit(methodCall.ThisArgument);

+        inexpr.Add(this.TranslatedExpressions.Pop());

+        #endregion

+

+        Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

+        IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

+        penum.MoveNext();

+        foreach (IExpression exp in methodCall.Arguments) {

+          if (penum.Current == null) {

+            throw new TranslationException("More Arguments than Parameters in functioncall");

+          }

+          this.Visit(exp);

+          Bpl.Expr e = this.TranslatedExpressions.Pop();

+

+          p2eMap.Add(penum.Current, e);

+          if (!penum.Current.IsOut) {

+            inexpr.Add(e);

+          }

+

+          penum.MoveNext();

+        }

+        #endregion

+

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

+

+        // TODO: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

+

+        #region Translate Out vars

+        var outvars = new List<Bpl.IdentifierExpr>();

+

+        foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {

+          if (kvp.Key.IsOut || kvp.Key.IsByReference) {

+            Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

+            if (iexp == null) {

+              throw new TranslationException("Trying to pass complex expression as out in functioncall");

+            }

+            outvars.Add(iexp);

+          }

+        }

+        #endregion

+

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

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

+          outvars.Add(new Bpl.IdentifierExpr(token, v));

+          TranslatedExpressions.Push(new Bpl.IdentifierExpr(token, v));

+        }

+

+        Bpl.QKeyValue attrib = null;

+        foreach (var a in resolvedMethod.Attributes) {

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

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

+            break;

+          }

+        }

+

+        var elseBranch = new Bpl.StmtListBuilder();

+

+        var methodname = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);

+        Bpl.CallCmd call;

+        if (attrib != null)

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

+        else

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

+        elseBranch.Add(call);

+

+        Bpl.IfCmd ifcmd = null;

+

+        Contract.Assume(1 <= overrides.Count);

+        foreach (var m in overrides) {

+          var thenBranch = new Bpl.StmtListBuilder();

+          methodname = TranslationHelper.CreateUniqueMethodName(m); 

+          if (attrib != null)

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

+          else

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

+          thenBranch.Add(call);

+          ifcmd = new Bpl.IfCmd(token,

+            Bpl.LiteralExpr.True,

+            thenBranch.Collect(token),

+            null,

+            elseBranch.Collect(token)

+            );

+          elseBranch = new Bpl.StmtListBuilder();

+          elseBranch.Add(ifcmd);

+        }

+

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

+

+        return;

+      }

+

+      /// <summary>

+      /// Modifies <paramref name="overrides"/> as side-effect.

+      /// </summary>

+      private void FindOverrides(ITypeReference type, IMethodDefinition resolvedMethod, List<IMethodReference> overrides) {

+        Contract.Requires(type != null);

+        Contract.Requires(resolvedMethod != null);

+        Contract.Requires(overrides != null);

+        foreach (var subType in this.subTypes[type]) {

+          var overriddenMethod = MemberHelper.GetImplicitlyOverridingDerivedClassMethod(resolvedMethod, subType.ResolvedType);

+          if (overriddenMethod != Dummy.Method)

+            overrides.Add(overriddenMethod);

+          if (this.subTypes.ContainsKey(subType))

+            FindOverrides(subType, resolvedMethod, overrides);

+        }

+      }

+

+    }

+

+  }

+}

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 6fc21050..ea98c61b 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -101,6 +101,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
     assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;

     assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

     $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));

+    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

     if (z)

     {

         assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

@@ -445,7 +446,7 @@ procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$Sys
 

 

 

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+implementation {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

   var local_0: int;

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index b8e98a5d..043ceccf 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -77,6 +77,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
     assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;

     assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

     RegressionTestInput.ClassWithBoolTypes.b[this] := z;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

     if (z)

     {

         assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

@@ -421,7 +422,7 @@ procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$Sys
 

 

 

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+implementation {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

   var local_0: int;

diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
index 1088f1f7..98d64ff9 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
@@ -87,6 +87,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
     assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;

     assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

     $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);

+    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

     if (z)

     {

         assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

@@ -431,7 +432,7 @@ procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$Sys
 

 

 

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+implementation {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

   var local_0: int;

diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
index 1fa0bd18..56e19305 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -77,6 +77,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
     assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;

     assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

     $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

     if (z)

     {

         assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

@@ -421,7 +422,7 @@ procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$Sys
 

 

 

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+implementation {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

   var local_0: int;

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index 9d7f9204..236ec12f 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssembly(assemblyName, heapFactory, null);

+      BCT.TranslateAssembly(assemblyName, heapFactory, null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;