diff options
21 files changed, 676 insertions, 111 deletions
diff --git a/BCT/BCT.sln b/BCT/BCT.sln index 6c5702ae..905cc2ea 100644 --- a/BCT/BCT.sln +++ b/BCT/BCT.sln @@ -25,6 +25,19 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeModelToIL", "..\..\CCIC EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGenerator", "..\..\CCICodePlex\Ast\Metadata\Sources\ILGenerator\ILGenerator.csproj", "{08156C78-403A-4112-AD81-8646AC51CD2F}"
EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "RegressionTests", "RegressionTests", "{AA77A7CB-972F-4A5C-A16C-3810B448F6EA}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "RegressionTestInput", "RegressionTests\RegressionTestInput\RegressionTestInput.csproj", "{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TranslationTest", "RegressionTests\TranslationTest\TranslationTest.csproj", "{A112AFBA-D6F6-44A4-A683-C3D458A68D84}"
+EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution Items", "{45E691A6-BFA4-4545-93AC-EA7290A6B565}"
+ ProjectSection(SolutionItems) = preProject
+ BCT.vsmdi = BCT.vsmdi
+ Local.testsettings = Local.testsettings
+ TraceAndTestImpact.testsettings = TraceAndTestImpact.testsettings
+ EndProjectSection
+EndProject
Global
GlobalSection(TeamFoundationVersionControl) = preSolution
SccNumberOfProjects = 9
@@ -76,6 +89,9 @@ Global SccLocalPath8 = ..\\..\\Felt\\SourceModel
SccProvider8 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}
EndGlobalSection
+ GlobalSection(TestCaseManagementSettings) = postSolution
+ CategoryFile = BCT.vsmdi
+ EndGlobalSection
GlobalSection(SolutionConfigurationPlatforms) = preSolution
CompilerOnly|Any CPU = CompilerOnly|Any CPU
Debug|Any CPU = Debug|Any CPU
@@ -204,8 +220,33 @@ Global {08156C78-403A-4112-AD81-8646AC51CD2F}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU
{08156C78-403A-4112-AD81-8646AC51CD2F}.Release|Any CPU.ActiveCfg = Release|Any CPU
{08156C78-403A-4112-AD81-8646AC51CD2F}.Release|Any CPU.Build.0 = Release|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Release|Any CPU.Build.0 = Release|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
+ GlobalSection(NestedProjects) = preSolution
+ {3D13D2CC-6387-46FA-BDC2-4BEEFC460118} = {AA77A7CB-972F-4A5C-A16C-3810B448F6EA}
+ {A112AFBA-D6F6-44A4-A683-C3D458A68D84} = {AA77A7CB-972F-4A5C-A16C-3810B448F6EA}
+ {45E691A6-BFA4-4545-93AC-EA7290A6B565} = {AA77A7CB-972F-4A5C-A16C-3810B448F6EA}
+ EndGlobalSection
EndGlobal
diff --git a/BCT/BCT.vsmdi b/BCT/BCT.vsmdi new file mode 100644 index 00000000..08dd31d7 --- /dev/null +++ b/BCT/BCT.vsmdi @@ -0,0 +1,6 @@ +<?xml version="1.0" encoding="UTF-8"?>
+<TestLists xmlns="http://microsoft.com/schemas/VisualStudio/TeamTest/2010">
+ <TestList name="Lists of Tests" id="8c43106b-9dc1-4907-a29f-aa66a61bf5b6">
+ <RunConfiguration id="f898dc7f-7e79-4656-a1cd-5ca50fff2b5d" name="Local" storage="local.testsettings" type="Microsoft.VisualStudio.TestTools.Common.TestRunConfiguration, Microsoft.VisualStudio.QualityTools.Common, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
+ </TestList>
+</TestLists>
\ No newline at end of file diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index 60479a27..e566adff 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -108,6 +108,7 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
+ <Compile Include="CLRSemantics.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
<Compile Include="ClassTraverser.cs" />
@@ -117,6 +118,7 @@ <Compile Include="ToplevelTraverser.cs" />
<Compile Include="TranslationException.cs" />
<Compile Include="TranslationHelper.cs" />
+ <Compile Include="TraverserFactory.cs" />
</ItemGroup>
<ItemGroup>
<Content Include="Readme.txt" />
diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs new file mode 100644 index 00000000..f52b2006 --- /dev/null +++ b/BCT/BytecodeTranslator/CLRSemantics.cs @@ -0,0 +1,52 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+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;
+
+namespace BytecodeTranslator {
+
+ public class CLRSemantics : TraverserFactory {
+
+ public override ExpressionTraverser MakeExpressionTraverser(StatementTraverser parent, Bpl.Variable heapVariable) {
+ return new CLRExpressionSemantics(parent, heapVariable);
+ }
+
+ public class CLRExpressionSemantics : ExpressionTraverser {
+
+ public CLRExpressionSemantics(StatementTraverser stmtTraverser, Bpl.Variable heapvar)
+ : base(stmtTraverser, heapvar) { }
+
+ public override void Visit(IDivision division) {
+ this.Visit(division.LeftOperand);
+ this.Visit(division.RightOperand);
+ Bpl.Expr rexp = TranslatedExpressions.Pop();
+ Bpl.Expr lexp = TranslatedExpressions.Pop();
+
+ var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);
+
+ var loc = this.StmtTraverser.MethodTraverser.CreateFreshLocal(division.RightOperand.Type);
+ var locExpr = Bpl.Expr.Ident(loc);
+ var storeLocal = Bpl.Cmd.SimpleAssign(tok, locExpr, rexp);
+ this.StmtTraverser.StmtBuilder.Add(storeLocal);
+
+ var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, locExpr, Bpl.Expr.Literal(0)));
+ this.StmtTraverser.StmtBuilder.Add(a);
+
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, locExpr));
+ }
+ }
+ }
+}
\ No newline at end of file diff --git a/BCT/BytecodeTranslator/ClassTraverser.cs b/BCT/BytecodeTranslator/ClassTraverser.cs index 67232f83..ce72c9ba 100644 --- a/BCT/BytecodeTranslator/ClassTraverser.cs +++ b/BCT/BytecodeTranslator/ClassTraverser.cs @@ -20,7 +20,10 @@ namespace BytecodeTranslator { /// <summary>
///
/// </summary>
- internal class ClassTraverser : BaseCodeAndContractTraverser {
+ public class ClassTraverser : BaseCodeAndContractTraverser {
+
+ public readonly TraverserFactory factory;
+
public readonly ToplevelTraverser ToplevelTraverser;
private Dictionary<IFieldDefinition, Bpl.GlobalVariable> fieldVarMap = new Dictionary<IFieldDefinition, Microsoft.Boogie.GlobalVariable>();
@@ -32,8 +35,9 @@ namespace BytecodeTranslator { public readonly Bpl.Variable HeapVariable = TranslationHelper.TempHeapVar();
- public ClassTraverser(IContractProvider cp, ToplevelTraverser tlTraverser)
+ public ClassTraverser(TraverserFactory factory, IContractProvider cp, ToplevelTraverser tlTraverser)
: base(cp) {
+ this.factory = factory;
ToplevelTraverser = tlTraverser;
}
@@ -61,7 +65,8 @@ namespace BytecodeTranslator { // check if it's static and so on
MethodTraverser mt;
if (!methodMap.TryGetValue(method, out mt)) {
- mt = new MethodTraverser(this.contractProvider, this);
+ mt = this.factory.MakeMethodTraverser(this, this.contractProvider);
+ this.methodMap.Add(method, mt);
}
mt.Visit(method);
}
@@ -76,4 +81,5 @@ namespace BytecodeTranslator { }
}
+
}
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index ba832fa4..beeb5cb1 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -19,7 +19,7 @@ using Bpl = Microsoft.Boogie; namespace BytecodeTranslator {
- class ExpressionTraverser : BaseCodeTraverser {
+ public class ExpressionTraverser : BaseCodeTraverser {
// warning! this has to be replaced by a HeapVariable from outside
public readonly Bpl.Variable HeapVariable;
@@ -30,24 +30,9 @@ namespace BytecodeTranslator { #region Constructors
- public ExpressionTraverser(StatementTraverser stmtTraverser) {
- HeapVariable = stmtTraverser.HeapVariable;
- StmtTraverser = stmtTraverser;
- TranslatedExpressions = new Stack<Bpl.Expr>();
- }
-
- public ExpressionTraverser(ClassTraverser classTraverser) {
- // TODO
- //StmtTraverser = new StatementTraverser(classTraverser);
- HeapVariable = classTraverser.HeapVariable;
- TranslatedExpressions = new Stack<Bpl.Expr>();
- }
-
- public ExpressionTraverser(MethodTraverser methodTraverser) {
- HeapVariable = methodTraverser.HeapVariable;
- StmtTraverser = new StatementTraverser(methodTraverser);
- TranslatedExpressions = new Stack<Bpl.Expr>();
- }
+ public ExpressionTraverser(StatementTraverser stmtTraverser)
+ : this(stmtTraverser, stmtTraverser.HeapVariable)
+ { }
public ExpressionTraverser(StatementTraverser stmtTraverser, Bpl.Variable heapvar) {
HeapVariable = heapvar;
@@ -55,18 +40,6 @@ namespace BytecodeTranslator { TranslatedExpressions = new Stack<Bpl.Expr>();
}
- public ExpressionTraverser(ClassTraverser classTraverser, Bpl.Variable heapvar) {
- HeapVariable = heapvar;
- // TODO
- //StmtTraverser = new StatementTraverser(classTraverser);
- TranslatedExpressions = new Stack<Bpl.Expr>();
- }
-
- public ExpressionTraverser(MethodTraverser methodTraverser, Bpl.Variable heapvar) {
- HeapVariable = heapvar;
- StmtTraverser = new StatementTraverser(methodTraverser);
- TranslatedExpressions = new Stack<Bpl.Expr>();
- }
#endregion
#region Translate Variable Access
@@ -279,10 +252,7 @@ namespace BytecodeTranslator { field.ContainingType.ResolvedType,
field.ResolvedField) ) );
- ExpressionTraverser etrav = new ExpressionTraverser(StmtTraverser);
- etrav.Visit(instance);
-
- TranslatedExpressions.Push(etrav.TranslatedExpressions.Pop());
+ this.Visit(instance);
// if the field access is not a targetexpression we build a select expression
// otherwise the assignment visitor will build a mapassignment later on
@@ -331,9 +301,8 @@ namespace BytecodeTranslator { Bpl.ExprSeq inexpr = new Bpl.ExprSeq();
#region Create the 'this' argument for the function call
- ExpressionTraverser thistraverser = new ExpressionTraverser(StmtTraverser);
- thistraverser.Visit(methodCall.ThisArgument);
- inexpr.Add(thistraverser.TranslatedExpressions.Pop());
+ this.Visit(methodCall.ThisArgument);
+ inexpr.Add(this.TranslatedExpressions.Pop());
#endregion
Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();
@@ -343,9 +312,9 @@ namespace BytecodeTranslator { if (penum.Current == null) {
throw new TranslationException("More Arguments than Parameters in functioncall");
}
- ExpressionTraverser etrav = new ExpressionTraverser(this.StmtTraverser);
- etrav.Visit(exp);
- Bpl.Expr e = etrav.TranslatedExpressions.Pop();
+ this.Visit(exp);
+ Bpl.Expr e = this.TranslatedExpressions.Pop();
+
p2eMap.Add(penum.Current, e);
if (!penum.Current.IsOut) {
inexpr.Add(e);
@@ -396,48 +365,24 @@ namespace BytecodeTranslator { /// <remarks>(mschaef) Works, but still a stub </remarks>
/// <param name="assignment"></param>
public override void Visit(IAssignment assignment) {
- ExpressionTraverser sourcetrav = new ExpressionTraverser(this.StmtTraverser);
- ExpressionTraverser targettrav = new ExpressionTraverser(this.StmtTraverser);
#region Transform Right Hand Side ...
- sourcetrav.Visit(assignment.Source);
- Bpl.Expr sourceexp = sourcetrav.TranslatedExpressions.Pop();
+ this.Visit(assignment.Source);
+ Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();
#endregion
- #region ... and now Left Hand Side and build the bpl statement
-
- targettrav.Visit(assignment.Target);
-
- if (targettrav.TranslatedExpressions.Count == 1) {
-
- Bpl.Expr targetexp = targettrav.TranslatedExpressions.Pop();
- Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;
- if (idexp != null) {
- StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),
- idexp, sourceexp));
- return;
- } else {
- throw new TranslationException("Trying to create a SimpleAssign with complex/illegal lefthand side");
- }
-
- } else if (targettrav.TranslatedExpressions.Count > 1) {
-
- Bpl.ExprSeq eseq = new Bpl.ExprSeq();
-
- while (targettrav.TranslatedExpressions.Count > 0) {
- eseq.Add(targettrav.TranslatedExpressions.Pop());
- }
+ this.Visit(assignment.Target);
- StmtTraverser.StmtBuilder.Add(Bpl.Cmd.MapAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),
- new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(assignment.Target.Locations),
- HeapVariable), eseq, sourceexp));
+ Bpl.Expr targetexp = this.TranslatedExpressions.Pop();
+ Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;
+ if (idexp != null) {
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),
+ idexp, sourceexp));
return;
} else {
- throw new TranslationException("Trying to create an Assignment but lefthand side cannot be created");
+ throw new TranslationException("Trying to create a SimpleAssign with complex/illegal lefthand side");
}
- #endregion
-
}
@@ -457,10 +402,6 @@ 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) {
@@ -599,4 +540,5 @@ namespace BytecodeTranslator { }
#endregion
}
+
}
diff --git a/BCT/BytecodeTranslator/MethodTraverser.cs b/BCT/BytecodeTranslator/MethodTraverser.cs index fdda674d..7a7170e9 100644 --- a/BCT/BytecodeTranslator/MethodTraverser.cs +++ b/BCT/BytecodeTranslator/MethodTraverser.cs @@ -17,7 +17,10 @@ using Microsoft.Cci.ILToCodeModel; using Bpl = Microsoft.Boogie;
namespace BytecodeTranslator {
- class MethodTraverser : BaseCodeAndContractTraverser {
+ public class MethodTraverser : BaseCodeAndContractTraverser {
+
+ public readonly TraverserFactory factory;
+
public readonly ClassTraverser ClassTraverser;
private Bpl.Procedure procedure;
@@ -30,7 +33,7 @@ namespace BytecodeTranslator { private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();
- internal class MethodParameter {
+ public class MethodParameter {
public MethodParameter() {
localParameter = null;
inParameterCopy = null;
@@ -65,11 +68,11 @@ namespace BytecodeTranslator { /// Creates a fresh local var of the given Type and adds it to the
/// Bpl Implementation
/// </summary>
- /// <param name="typedef"> The type of the new variable </param>
+ /// <param name="typeReference"> The type of the new variable </param>
/// <returns> A fresh Variable with automatic generated name and location </returns>
- public Bpl.Variable CreateFreshLocal(ITypeDefinition typedef) {
+ public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {
Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(typedef);
+ Bpl.Type t = TranslationHelper.CciTypeToBoogie(typeReference);
Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));
ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie
localVarMap.Add(dummy, v);
@@ -122,13 +125,16 @@ namespace BytecodeTranslator { }
#endregion
- public MethodTraverser(IContractProvider cp, ClassTraverser cTraverser)
+ public MethodTraverser(TraverserFactory factory, IContractProvider cp, ClassTraverser cTraverser)
: base(cp) {
+ this.factory = factory;
HeapVariable = cTraverser.HeapVariable;
procedure = null;
ClassTraverser = cTraverser;
}
+ #region Overrides
+
/// <summary>
///
/// </summary>
@@ -209,7 +215,7 @@ namespace BytecodeTranslator { if (contract != null) {
try {
foreach (IPrecondition pre in contract.Preconditions) {
- ExpressionTraverser exptravers = new ExpressionTraverser(this);
+ ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);
exptravers.Visit(pre.Condition); // TODO
// Todo: Deal with Descriptions
@@ -221,7 +227,7 @@ namespace BytecodeTranslator { }
foreach (IPostcondition post in contract.Postconditions) {
- ExpressionTraverser exptravers = new ExpressionTraverser(this);
+ ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);
exptravers.Visit(post.Condition);
// Todo: Deal with Descriptions
@@ -233,7 +239,7 @@ namespace BytecodeTranslator { }
foreach (IAddressableExpression mod in contract.ModifiedVariables) {
- ExpressionTraverser exptravers = new ExpressionTraverser(this);
+ ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);
exptravers.Visit(mod);
Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
@@ -271,7 +277,7 @@ namespace BytecodeTranslator { throw new NotImplementedException("abstract methods are not yet implemented");
}
- StatementTraverser stmtTraverser = new StatementTraverser(this);
+ StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this, this.HeapVariable);
#region Add assignements from In-Params to local-Params
@@ -289,7 +295,7 @@ namespace BytecodeTranslator { try {
method.ResolvedMethod.Body.Dispatch(stmtTraverser);
} catch (TranslationException te) {
- throw new NotImplementedException("No Errorhandling in Mehtodvisitor / " + te.ToString());
+ throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());
} catch {
throw;
}
@@ -328,5 +334,8 @@ namespace BytecodeTranslator { }
}
+ #endregion
+
}
+
}
diff --git a/BCT/BytecodeTranslator/Prelude.cs b/BCT/BytecodeTranslator/Prelude.cs index 6805a39e..6db620ad 100644 --- a/BCT/BytecodeTranslator/Prelude.cs +++ b/BCT/BytecodeTranslator/Prelude.cs @@ -4,7 +4,7 @@ using System.IO; using System.Text;
namespace BytecodeTranslator {
- class Prelude {
+ public class Prelude {
public static void Emit(Microsoft.Boogie.TokenTextWriter wr) {
wr.Write(@"// Copyright (c) 2010, Microsoft Corp.
// Bytecode Translator prelude
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index f9e46d0d..452cc114 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -61,7 +61,8 @@ namespace BytecodeTranslator { #region Pass 3: Translate the code model to BPL
//tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);
- ToplevelTraverser translator = new ToplevelTraverser(host.GetContractExtractor(module.ModuleIdentity));
+ var factory = new CLRSemantics();
+ ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));
assembly = module as IAssembly;
if (assembly != null)
translator.Visit(assembly);
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index d9c4400a..5ebaea37 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -20,7 +20,10 @@ using System.Diagnostics.Contracts; namespace BytecodeTranslator
{
- internal class StatementTraverser : BaseCodeTraverser {
+ public class StatementTraverser : BaseCodeTraverser {
+
+ public readonly TraverserFactory factory;
+
public readonly MethodTraverser MethodTraverser;
public readonly Bpl.Variable HeapVariable;
@@ -28,12 +31,11 @@ namespace BytecodeTranslator public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
#region Constructors
- public StatementTraverser(MethodTraverser mt) {
- HeapVariable = mt.HeapVariable;
- MethodTraverser = mt;
- }
+ public StatementTraverser(TraverserFactory factory, MethodTraverser mt) :
+ this(factory, mt, mt.HeapVariable) { }
- public StatementTraverser(MethodTraverser mt, Bpl.Variable heapvar) {
+ public StatementTraverser(TraverserFactory factory, MethodTraverser mt, Bpl.Variable heapvar) {
+ this.factory = factory;
HeapVariable = heapvar;
MethodTraverser = mt;
}
@@ -46,7 +48,7 @@ namespace BytecodeTranslator }
Bpl.Expr ExpressionFor(IExpression expression) {
- ExpressionTraverser etrav = new ExpressionTraverser(this);
+ ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);
etrav.Visit(expression);
Contract.Assert(etrav.TranslatedExpressions.Count == 1);
return etrav.TranslatedExpressions.Pop();
@@ -82,10 +84,10 @@ namespace BytecodeTranslator /// <remarks>(mschaef) Works, but still a stub</remarks>
/// <param name="conditionalStatement"></param>
public override void Visit(IConditionalStatement conditionalStatement) {
- StatementTraverser thenTraverser = new StatementTraverser(this.MethodTraverser);
- StatementTraverser elseTraverser = new StatementTraverser(this.MethodTraverser);
+ StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);
+ StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);
- ExpressionTraverser condTraverser = new ExpressionTraverser(this);
+ ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this, this.HeapVariable);
condTraverser.Visit(conditionalStatement.Condition);
thenTraverser.Visit(conditionalStatement.TrueBranch);
elseTraverser.Visit(conditionalStatement.FalseBranch);
@@ -108,7 +110,7 @@ namespace BytecodeTranslator /// <remarks> TODO: might be wrong for the general case</remarks>
public override void Visit(IExpressionStatement expressionStatement) {
- ExpressionTraverser etrav = new ExpressionTraverser(this);
+ ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);
etrav.Visit(expressionStatement.Expression);
}
@@ -150,7 +152,7 @@ namespace BytecodeTranslator #endregion
if (returnStatement.Expression != null) {
- ExpressionTraverser etrav = new ExpressionTraverser(this);
+ ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);
etrav.Visit(returnStatement.Expression);
if (this.MethodTraverser.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {
@@ -202,4 +204,5 @@ namespace BytecodeTranslator #endregion
}
+
}
diff --git a/BCT/BytecodeTranslator/ToplevelTraverser.cs b/BCT/BytecodeTranslator/ToplevelTraverser.cs index 9079b5af..0ba7bffa 100644 --- a/BCT/BytecodeTranslator/ToplevelTraverser.cs +++ b/BCT/BytecodeTranslator/ToplevelTraverser.cs @@ -21,7 +21,9 @@ namespace BytecodeTranslator { /// <summary>
///
/// </summary>
- internal class ToplevelTraverser : BaseCodeAndContractTraverser {
+ public class ToplevelTraverser : BaseCodeAndContractTraverser {
+
+ public readonly TraverserFactory factory;
public readonly IContractProvider ContractProvider;
@@ -29,8 +31,9 @@ namespace BytecodeTranslator { private Dictionary<ITypeDefinition, ClassTraverser> classMap = new Dictionary<ITypeDefinition, ClassTraverser>();
- public ToplevelTraverser(IContractProvider cp)
+ public ToplevelTraverser(TraverserFactory factory, IContractProvider cp)
: base(cp) {
+ this.factory = factory;
ContractProvider = cp;
TranslatedProgram = new Bpl.Program();
}
@@ -38,7 +41,7 @@ namespace BytecodeTranslator { public Bpl.Variable FindOrCreateClassField(ITypeDefinition classtype, IFieldDefinition field) {
ClassTraverser ct;
if (!classMap.TryGetValue(classtype, out ct)) {
- ct = new ClassTraverser(this.ContractProvider, this);
+ ct = this.factory.MakeClassTraverser(this, this.contractProvider);
classMap.Add(classtype, ct);
return ct.FindOrCreateFieldVariable(field);
} else {
@@ -55,8 +58,8 @@ namespace BytecodeTranslator { if (typeDefinition.IsClass) {
ClassTraverser ct;
- if (!classMap.TryGetValue(typeDefinition, out ct)) {
- ct = new ClassTraverser(this.contractProvider, this);
+ if (!classMap.TryGetValue(typeDefinition, out ct)) {
+ ct = this.factory.MakeClassTraverser(this, this.contractProvider);
classMap.Add(typeDefinition, ct);
}
ct.Visit(typeDefinition);
@@ -75,4 +78,5 @@ namespace BytecodeTranslator { }
}
+
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs new file mode 100644 index 00000000..cacc9817 --- /dev/null +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -0,0 +1,27 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+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;
+
+namespace BytecodeTranslator {
+ public abstract class TraverserFactory {
+ public virtual ToplevelTraverser MakeTopLevelTraverser(IContractProvider contractProvider) { return new ToplevelTraverser(this, contractProvider); }
+ public virtual ClassTraverser MakeClassTraverser(ToplevelTraverser parent, IContractProvider contractProvider) { return new ClassTraverser(this, contractProvider, parent); }
+ public virtual MethodTraverser MakeMethodTraverser(ClassTraverser parent, IContractProvider contractProvider) { return new MethodTraverser(this, contractProvider, parent); }
+ public virtual StatementTraverser MakeStatementTraverser(MethodTraverser parent, Bpl.Variable heapVariable) { return new StatementTraverser(this, parent, heapVariable); }
+ public virtual ExpressionTraverser MakeExpressionTraverser(StatementTraverser parent, Bpl.Variable heapVariable) { return new ExpressionTraverser(parent, heapVariable); }
+ }
+}
\ No newline at end of file diff --git a/BCT/Local.testsettings b/BCT/Local.testsettings new file mode 100644 index 00000000..f63e9b16 --- /dev/null +++ b/BCT/Local.testsettings @@ -0,0 +1,31 @@ +<?xml version="1.0" encoding="UTF-8"?>
+<TestSettings name="Local" id="f898dc7f-7e79-4656-a1cd-5ca50fff2b5d" xmlns="http://microsoft.com/schemas/VisualStudio/TeamTest/2010">
+ <Description>These are default test settings for a local test run.</Description>
+ <Execution>
+ <TestTypeSpecific>
+ <UnitTestRunConfig testTypeId="13cdc9d9-ddb5-4fa4-a97d-d965ccfc6d4b">
+ <AssemblyResolution>
+ <TestDirectory useLoadContext="true" />
+ </AssemblyResolution>
+ </UnitTestRunConfig>
+ <WebTestRunConfiguration testTypeId="4e7599fa-5ecb-43e9-a887-cd63cf72d207">
+ <Browser name="Internet Explorer 7.0">
+ <Headers>
+ <Header name="User-Agent" value="Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1)" />
+ <Header name="Accept" value="*/*" />
+ <Header name="Accept-Language" value="{{$IEAcceptLanguage}}" />
+ <Header name="Accept-Encoding" value="GZIP" />
+ </Headers>
+ </Browser>
+ </WebTestRunConfiguration>
+ </TestTypeSpecific>
+ <AgentRule name="LocalMachineDefaultRole">
+ <DataCollectors>
+ <DataCollector uri="datacollector://microsoft/CodeCoverage/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TestTools.CodeCoverage.CoveragePlugIn, Microsoft.VisualStudio.QualityTools.Plugins.CodeCoverage, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Code Coverage">
+ </DataCollector>
+ <DataCollector uri="datacollector://microsoft/TestImpact/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.TestImpactDataCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Test Impact">
+ </DataCollector>
+ </DataCollectors>
+ </AgentRule>
+ </Execution>
+</TestSettings>
\ No newline at end of file diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs new file mode 100644 index 00000000..f537f861 --- /dev/null +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -0,0 +1,15 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+
+namespace RegressionTestInput {
+ public class Class0 {
+ void M(int x) {
+ int y = (5 / x) + (x = 3);
+ Contract.Assert(x == 3 && y <= 8);
+ }
+
+ }
+}
diff --git a/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs b/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..b3cc080a --- /dev/null +++ b/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("RegressionTestInput")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("RegressionTestInput")]
+[assembly: AssemblyCopyright("Copyright © 2010")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("dc8e9afb-ef4e-4954-8f86-1a79bb0d77e4")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj b/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj new file mode 100644 index 00000000..6cf94c40 --- /dev/null +++ b/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj @@ -0,0 +1,54 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>RegressionTestInput</RootNamespace>
+ <AssemblyName>RegressionTestInput</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="Class1.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </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.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs b/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..a0fd3275 --- /dev/null +++ b/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs @@ -0,0 +1,35 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("TranslationTest")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("TranslationTest")]
+[assembly: AssemblyCopyright("Copyright © 2010")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("f448ac99-c5e7-424c-8bdb-243e8276d4d7")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt new file mode 100644 index 00000000..564dd07e --- /dev/null +++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt @@ -0,0 +1,50 @@ +// Copyright (c) 2010, Microsoft Corp.
+// Bytecode Translator prelude
+
+type Ref;
+const null: Ref;
+
+type Field alpha;
+
+type HeapType = <alpha>[Ref, Field alpha]alpha;
+function IsGoodHeap(HeapType): bool;
+
+var $Heap: HeapType where IsGoodHeap($Heap);
+
+procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);
+
+
+
+implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)
+{
+ var __temp_1: int;
+ var $tmp0: int;
+ var __temp_2: int;
+ var __temp_3: int;
+ var local_0: int;
+ var x: int;
+
+ x := x$in;
+ $tmp0 := x;
+ assert $tmp0 != 0;
+ __temp_1 := 5 / $tmp0;
+ __temp_2 := 3;
+ __temp_3 := __temp_2;
+ x := __temp_3;
+ local_0 := __temp_1 + __temp_2;
+ assert x == 3 && local_0 <= 8;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0..ctor$System.Void(this: int);
+
+
+
+implementation RegressionTestInput.Class0..ctor$System.Void(this: int)
+{
+ return;
+}
+
+
diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj new file mode 100644 index 00000000..f0520a8f --- /dev/null +++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj @@ -0,0 +1,111 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>
+ </ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{A112AFBA-D6F6-44A4-A683-C3D458A68D84}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>TranslationTest</RootNamespace>
+ <AssemblyName>TranslationTest</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <ProjectTypeGuids>{3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="Core">
+ <HintPath>..\..\Binaries\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.QualityTools.UnitTestFramework, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="System" />
+ <Reference Include="System.Core">
+ <RequiredTargetFramework>3.5</RequiredTargetFramework>
+ </Reference>
+ </ItemGroup>
+ <ItemGroup>
+ <CodeAnalysisDependentAssemblyPaths Condition=" '$(VS100COMNTOOLS)' != '' " Include="$(VS100COMNTOOLS)..\IDE\PrivateAssemblies">
+ <Visible>False</Visible>
+ </CodeAnalysisDependentAssemblyPaths>
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="UnitTest0.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj">
+ <Project>{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}</Project>
+ <Name>MetadataHelper</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MetadataModel\MetadataModel.csproj">
+ <Project>{33CAB640-0D03-43DF-81BD-22CDC6C0A597}</Project>
+ <Name>MetadataModel</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MutableMetadataModel\MutableMetadataModel.csproj">
+ <Project>{319E151C-8F33-49E7-81C9-30F02F9BA90A}</Project>
+ <Name>MutableMetadataModel</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\PdbReader\PdbReader.csproj">
+ <Project>{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}</Project>
+ <Name>PdbReader</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\PeReader\PeReader.csproj">
+ <Project>{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}</Project>
+ <Name>PeReader</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\SourceModel\SourceModel.csproj">
+ <Project>{4B0054FD-124A-4037-9965-BDB55E6BF389}</Project>
+ <Name>SourceModel</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\CodeModel\CodeModel.csproj">
+ <Project>{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}</Project>
+ <Name>CodeModel</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\ILToCodeModel\ILToCodeModel.csproj">
+ <Project>{27F2A417-B6ED-43AD-A38E-A0B6142216F6}</Project>
+ <Name>ILToCodeModel</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\MutableCodeModel\MutableCodeModel.csproj">
+ <Project>{319E150C-8F33-49E7-81CA-30F02F9BA90A}</Project>
+ <Name>MutableCodeModel</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\BytecodeTranslator\BytecodeTranslator.csproj">
+ <Project>{9C8E4D74-0251-479D-ADAC-A9A469977301}</Project>
+ <Name>BytecodeTranslator</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\RegressionTestInput\RegressionTestInput.csproj">
+ <Project>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</Project>
+ <Name>RegressionTestInput</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <EmbeddedResource Include="RegressionTestInput.txt" />
+ </ItemGroup>
+ <Import Project="$(MSBuildBinPath)\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.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs new file mode 100644 index 00000000..a018797d --- /dev/null +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -0,0 +1,119 @@ +using System;
+using System.Text;
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using System.IO;
+using Microsoft.Cci;
+using Microsoft.Cci.MetadataReader;
+using Microsoft.Cci.MutableCodeModel;
+using Microsoft.Cci.Contracts;
+using Microsoft.Cci.ILToCodeModel;
+using BytecodeTranslator;
+
+namespace TranslationTest {
+ /// <summary>
+ /// Summary description for UnitTest0
+ /// </summary>
+ [TestClass]
+ public class UnitTest0 {
+ public UnitTest0() {
+ //
+ // TODO: Add constructor logic here
+ //
+ }
+
+ private TestContext testContextInstance;
+
+ /// <summary>
+ ///Gets or sets the test context which provides
+ ///information about and functionality for the current test run.
+ ///</summary>
+ public TestContext TestContext {
+ get {
+ return testContextInstance;
+ }
+ set {
+ testContextInstance = value;
+ }
+ }
+
+ #region Additional test attributes
+ //
+ // You can use the following additional attributes as you write your tests:
+ //
+ // Use ClassInitialize to run code before running the first test in the class
+ // [ClassInitialize()]
+ // public static void MyClassInitialize(TestContext testContext) { }
+ //
+ // Use ClassCleanup to run code after all tests in a class have run
+ // [ClassCleanup()]
+ // public static void MyClassCleanup() { }
+ //
+ // Use TestInitialize to run code before running each test
+ // [TestInitialize()]
+ // public void MyTestInitialize() { }
+ //
+ // Use TestCleanup to run code after each test has run
+ // [TestCleanup()]
+ // public void MyTestCleanup() { }
+ //
+ #endregion
+
+ private string ExecuteTest(string assemblyName) {
+
+ var host = new Microsoft.Cci.ILToCodeModel.CodeContractAwareHostEnvironment();
+ BCT.Host = host;
+
+ IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;
+ if (module == null || module == Dummy.Module || module == Dummy.Assembly) {
+ Console.WriteLine(assemblyName + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");
+ Assert.Fail("Failed to read in test assembly for regression test");
+ }
+
+ IAssembly/*?*/ assembly = null;
+
+ PdbReader/*?*/ pdbReader = null;
+ string pdbFile = Path.ChangeExtension(module.Location, "pdb");
+ if (File.Exists(pdbFile)) {
+ Stream pdbStream = File.OpenRead(pdbFile);
+ pdbReader = new PdbReader(pdbStream, host);
+ }
+
+ module = Decompiler.GetCodeAndContractModelFromMetadataModel(host, module, pdbReader);
+
+ #region Pass 3: Translate the code model to BPL
+ var factory = new CLRSemantics();
+ ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));
+ assembly = module as IAssembly;
+ if (assembly != null)
+ translator.Visit(assembly);
+ else
+ translator.Visit(module);
+ #endregion Pass 3: Translate the code model to BPL
+ Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(module.Name + ".bpl");
+ Prelude.Emit(writer);
+ translator.TranslatedProgram.Emit(writer);
+ writer.Close();
+ var fileName = Path.ChangeExtension(assemblyName, "bpl");
+ var s = File.ReadAllText(fileName);
+ return s;
+ }
+
+ [TestMethod]
+ public void TranslationTest() {
+ string dir = TestContext.DeploymentDirectory;
+ var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
+ Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.RegressionTestInput.txt");
+ StreamReader reader = new StreamReader(resource);
+ string expected = reader.ReadToEnd();
+ var result = ExecuteTest(fullPath);
+ if (result != expected) {
+ string resultFile = Path.GetFullPath("RegressionTestOutput.txt");
+ File.WriteAllText(resultFile, result);
+ Assert.Fail("Output didn't match RegressionTestInput.txt: " + resultFile);
+ }
+ }
+ }
+}
+
\ No newline at end of file diff --git a/BCT/TraceAndTestImpact.testsettings b/BCT/TraceAndTestImpact.testsettings new file mode 100644 index 00000000..a6b85f3a --- /dev/null +++ b/BCT/TraceAndTestImpact.testsettings @@ -0,0 +1,21 @@ +<?xml version="1.0" encoding="UTF-8"?>
+<TestSettings name="Trace and Test Impact" id="cadf610f-d4f6-4ea8-9e0b-470bc35c9956" xmlns="http://microsoft.com/schemas/VisualStudio/TeamTest/2010">
+ <Description>These are test settings for Trace and Test Impact.</Description>
+ <Execution>
+ <TestTypeSpecific />
+ <AgentRule name="Execution Agents">
+ <DataCollectors>
+ <DataCollector uri="datacollector://microsoft/SystemInfo/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TestTools.DataCollection.SystemInfo.SystemInfoDataCollector, Microsoft.VisualStudio.TestTools.DataCollection.SystemInfo, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="System Information">
+ </DataCollector>
+ <DataCollector uri="datacollector://microsoft/ActionLog/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TestTools.ManualTest.ActionLog.ActionLogPlugin, Microsoft.VisualStudio.TestTools.ManualTest.ActionLog, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Actions">
+ </DataCollector>
+ <DataCollector uri="datacollector://microsoft/HttpProxy/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.HttpProxyCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="ASP.NET Client Proxy for IntelliTrace and Test Impact">
+ </DataCollector>
+ <DataCollector uri="datacollector://microsoft/TestImpact/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.TestImpactDataCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Test Impact">
+ </DataCollector>
+ <DataCollector uri="datacollector://microsoft/TraceDebugger/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.TraceDebuggerDataCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="IntelliTrace">
+ </DataCollector>
+ </DataCollectors>
+ </AgentRule>
+ </Execution>
+</TestSettings>
\ No newline at end of file |