Updated the project to .NET v4.0.

Added helper methods to the statement traverser.
Handle ILocalDeclarationStatement, IAssertStatement, IAssumeStatement in StatementTraverser.
Handle simple logical-and and logical-or expressions in ExpressionTraverser.
Inject assertion that divisor is non-zero for IDivision in ExpressionTraverser.
Added static variable BCT.Host so all parts of translation can access the CCI Metadata host.

6 files changed, 117 insertions, 20 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 9af26786..60479a27 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -3,14 +3,14 @@
   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

     <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>9.0.21022</ProductVersion>

+    <ProductVersion>9.0.30729</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

     <ProjectGuid>{9C8E4D74-0251-479D-ADAC-A9A469977301}</ProjectGuid>

     <OutputType>Exe</OutputType>

     <AppDesignerFolder>Properties</AppDesignerFolder>

     <RootNamespace>BytecodeTranslator</RootNamespace>

     <AssemblyName>BytecodeTranslator</AssemblyName>

-    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <FileUpgradeFlags>

     </FileUpgradeFlags>

@@ -31,6 +31,7 @@
     <IsWebBootstrapper>false</IsWebBootstrapper>

     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

+    <TargetFrameworkProfile />

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -77,19 +78,19 @@
     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="AbsInt, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+    <Reference Include="AbsInt, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\AbsInt.dll</HintPath>

     </Reference>

-    <Reference Include="AIFramework, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+    <Reference Include="AIFramework, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\AIFramework.dll</HintPath>

     </Reference>

-    <Reference Include="Basetypes, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+    <Reference Include="Basetypes, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\Basetypes.dll</HintPath>

     </Reference>

-    <Reference Include="Core, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+    <Reference Include="Core, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\Core.dll</HintPath>

     </Reference>

@@ -178,6 +179,9 @@
       <Install>true</Install>

     </BootstrapperPackage>

   </ItemGroup>

+  <ItemGroup>

+    <None Include="app.config" />

+  </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

        Other similar extension points exist, see Microsoft.Common.targets.

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index c9b89bd9..ba832fa4 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -457,6 +457,10 @@ namespace BytecodeTranslator {
       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

       TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, rexp));

+

+      var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);

+      var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, rexp, Bpl.Expr.Literal(0)));

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

     }

 

     public override void Visit(ISubtraction subtraction) {

@@ -522,7 +526,40 @@ namespace BytecodeTranslator {
       TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, lexp, rexp));

     }

 

-    // TODO: (mschaef) AND and OR are not yet implemented

+    /// <summary>

+    /// There aren't any logical-and expressions or logical-or expressions in CCI.

+    /// Instead they are encoded as "x ? y : 0" for "x && y" and "x ? 1 : y"

+    /// for "x || y".

+    /// TODO:

+    /// If it isn't either of these short forms then emit the proper expression!

+    /// </summary>

+    public override void Visit(IConditional conditional) {

+      CompileTimeConstant ctc = conditional.ResultIfFalse as CompileTimeConstant;

+      if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32) {

+        int v = (int)ctc.Value;

+        if (v == 0) {

+          Visit(conditional.Condition);

+          Bpl.Expr x = TranslatedExpressions.Pop();

+          Visit(conditional.ResultIfTrue);

+          Bpl.Expr y = TranslatedExpressions.Pop();

+          TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, x, y));

+          return;

+        }

+      }

+      ctc = conditional.ResultIfTrue as CompileTimeConstant;

+      if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32) {

+        int v = (int)ctc.Value;

+        if (v == 1) {

+          Visit(conditional.Condition);

+          Bpl.Expr x = TranslatedExpressions.Pop();

+          Visit(conditional.ResultIfFalse);

+          Bpl.Expr y = TranslatedExpressions.Pop();

+          TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, x, y));

+          return;

+        }

+      }

+      base.Visit(conditional);

+    }

 

     #endregion

 

diff --git a/BCT/BytecodeTranslator/Prelude.cs b/BCT/BytecodeTranslator/Prelude.cs
index 0ebcd9f9..6805a39e 100644
--- a/BCT/BytecodeTranslator/Prelude.cs
+++ b/BCT/BytecodeTranslator/Prelude.cs
@@ -6,7 +6,7 @@ using System.Text;
 namespace BytecodeTranslator {

   class Prelude {

     public static void Emit(Microsoft.Boogie.TokenTextWriter wr) {

-      wr.WriteText(@"// Copyright (c) 2010, Microsoft Corp.

+      wr.Write(@"// Copyright (c) 2010, Microsoft Corp.

 // Bytecode Translator prelude

 

 type Ref;

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 26696250..f9e46d0d 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -14,7 +14,9 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;

 

 namespace BytecodeTranslator {

-  class BCT {

+  public class BCT {

+

+    public static IMetadataHost Host;

 

     static int Main(string[] args) {

 

@@ -38,6 +40,7 @@ namespace BytecodeTranslator {
     static int DoRealWork(string assemblyName) {

 

       var host = new Microsoft.Cci.ILToCodeModel.CodeContractAwareHostEnvironment();

+      Host = host;

 

       IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;

       if (module == null || module == Dummy.Module || module == Dummy.Assembly) {

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 8bc11399..b494ecfd 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -15,6 +15,7 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;

 

 using Bpl = Microsoft.Boogie;

+using System.Diagnostics.Contracts;

 

 

 namespace BytecodeTranslator

@@ -38,24 +39,53 @@ namespace BytecodeTranslator
     }

     #endregion

 

-    public override void Visit(IBlockStatement block) {

-      BasicBlock b = (BasicBlock)block;

-      this.Visit(b);

+    #region Helper Methods

+

+    Bpl.IToken TokenFor(IStatement statement) {

+      return TranslationHelper.CciLocationToBoogieToken(statement.Locations);

     }

 

-    #region Basic Statements

-    /// <summary>

-    /// Visit all statements in a single block

-    /// </summary>

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

-    private void Visit(BasicBlock b) {

+    Bpl.Expr ExpressionFor(IExpression expression) {

+      ExpressionTraverser etrav = new ExpressionTraverser(this);

+      etrav.Visit(expression);

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

+      return etrav.TranslatedExpressions.Pop();

+    }

+

+    #endregion

+

+    public override void Visit(IBlockStatement block) {

       Bpl.StmtListBuilder slb = new Bpl.StmtListBuilder();

 

-      foreach (IStatement st in b.Statements) {

+      foreach (IStatement st in block.Statements) {

         this.Visit(st);

       }

     }

 

+    #region Basic Statements

+

+    public override void Visit(IAssertStatement assertStatement) {

+

+      StmtBuilder.Add(

+        new Bpl.AssertCmd(TokenFor(assertStatement), ExpressionFor(assertStatement.Condition))

+        );

+

+      //ExpressionTraverser etrav = new ExpressionTraverser(this);

+      //etrav.Visit(assertStatement.Condition);

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

+      //var tok = TranslationHelper.CciLocationToBoogieToken(assertStatement.Locations);

+      //var a = new Bpl.AssertCmd(tok, etrav.TranslatedExpressions.Pop());

+      //StmtBuilder.Add(a);

+    }

+

+    public override void Visit(IAssumeStatement assumeStatement) {

+      ExpressionTraverser etrav = new ExpressionTraverser(this);

+      etrav.Visit(assumeStatement.Condition);

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

+      var tok = TranslationHelper.CciLocationToBoogieToken(assumeStatement.Locations);

+      var a = new Bpl.AssumeCmd(tok, etrav.TranslatedExpressions.Pop());

+      StmtBuilder.Add(a);

+    }

 

     /// <summary>

     /// 

@@ -103,6 +133,29 @@ namespace BytecodeTranslator
     }

 

     /// <summary>

+    /// If the local declaration has an initial value, then generate the

+    /// statement "loc := e" from it. Otherwise ignore it.

+    /// </summary>

+    public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {

+      if (localDeclarationStatement.InitialValue == null) return;

+      var loc = this.MethodTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

+      var tok = TokenFor(localDeclarationStatement);

+      var e = ExpressionFor(localDeclarationStatement.InitialValue);

+      StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));

+      return;

+

+      //if (localDeclarationStatement.InitialValue == null) return;

+      //ExpressionTraverser etrav = new ExpressionTraverser(this);

+      //etrav.Visit(localDeclarationStatement.InitialValue);

+      //Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(localDeclarationStatement.Locations);

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

+      //var loc = this.MethodTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

+      //var e = etrav.TranslatedExpressions.Pop();

+      //StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));

+      //return;

+    }

+

+    /// <summary>

     /// 

     /// </summary>

     /// <remarks>(mschaef) not implemented</remarks>

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 0bbad693..9086290a 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -45,7 +45,7 @@ namespace BytecodeTranslator {
 

     #region Temp Stuff that must be replaced as soon as there is real code to deal with this

 

-    public static Bpl.Type CciTypeToBoogie(ITypeDefinition type) {

+    public static Bpl.Type CciTypeToBoogie(ITypeReference type) {

       return Bpl.Type.Int;

     }