From 17580f73a7919cff527c5839b37f9e9006b5f64d Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Sun, 6 Jun 2010 03:53:24 +0000
Subject: 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.

---
 BCT/BytecodeTranslator/BytecodeTranslator.csproj | 16 ++++--
 BCT/BytecodeTranslator/ExpressionTraverser.cs    | 39 ++++++++++++-
 BCT/BytecodeTranslator/Prelude.cs                |  2 +-
 BCT/BytecodeTranslator/Program.cs                |  5 +-
 BCT/BytecodeTranslator/StatementTraverser.cs     | 73 ++++++++++++++++++++----
 BCT/BytecodeTranslator/TranslationHelper.cs      |  2 +-
 6 files changed, 117 insertions(+), 20 deletions(-)

(limited to 'BCT')

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>
     /// 
@@ -102,6 +132,29 @@ namespace BytecodeTranslator
       StmtBuilder.Add(new Bpl.BreakCmd(TranslationHelper.CciLocationToBoogieToken(breakStatement.Locations), "I dont know"));
     }
 
+    /// <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>
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;
     }
 
-- 
cgit v1.2.3