summaryrefslogtreecommitdiff
path: root/BCT
diff options
context:
space:
mode:
Diffstat (limited to 'BCT')
-rw-r--r--BCT/BytecodeTranslator/BytecodeTranslator.csproj16
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs39
-rw-r--r--BCT/BytecodeTranslator/Prelude.cs2
-rw-r--r--BCT/BytecodeTranslator/Program.cs5
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs73
-rw-r--r--BCT/BytecodeTranslator/TranslationHelper.cs2
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;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 20:20:16 +0000