diff options
author | 2011-05-16 14:21:35 -0700 | |
---|---|---|
committer | 2011-05-16 14:21:35 -0700 | |
commit | 9026ac103f2e5ca9be7617de99c7d4a1fc1d9e0e (patch) | |
tree | 6c93972963e3adc04081da301ff30624df95838f | |
parent | 3628ed3ac55bc79515c0cb2c1bec9a21470c9d54 (diff) |
Merge
-rw-r--r-- | BCT/BytecodeTranslator/BytecodeTranslator.csproj | 12 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 294 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 21 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 45 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 31 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 32 |
6 files changed, 362 insertions, 73 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index 86fc4a5d..e4575480 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -32,6 +32,7 @@ <UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
<TargetFrameworkProfile />
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -41,7 +42,7 @@ <DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsCustomRewriterAssembly>
</CodeContractsCustomRewriterAssembly>
<CodeContractsCustomRewriterClass>
@@ -67,6 +68,15 @@ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
<CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 29c0033f..77050c46 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -138,6 +138,16 @@ namespace BytecodeTranslator }
public override void Visit(IArrayIndexer arrayIndexer) {
+
+#if EXPERIMENTAL
+ if (!IsAtomicInstance(arrayIndexer.IndexedObject)) {
+ // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
+ var se = ExpressionSimplifier.Simplify(this.sink, arrayIndexer);
+ this.Visit(se);
+ return;
+ }
+#endif
+
this.Visit(arrayIndexer.IndexedObject);
Bpl.Expr arrayExpr = TranslatedExpressions.Pop();
this.Visit(arrayIndexer.Indices);
@@ -155,6 +165,9 @@ namespace BytecodeTranslator indexExpr = new Bpl.NAryExpr(arrayIndexer.Token(), new Bpl.FunctionCall(f), new Bpl.ExprSeq(indexExprs));
}
+#if EXPERIMENTAL
+ this.TranslatedExpressions.Push(arrayExpr);
+#else
Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(arrayIndexer.Type));
Bpl.Expr selectExpr = sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, temp.Type);
this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, selectExpr));
@@ -162,10 +175,22 @@ namespace BytecodeTranslator this.arrayExpr = arrayExpr;
this.indexExpr = indexExpr;
+#endif
}
public override void Visit(ITargetExpression targetExpression)
{
+#if EXPERIMENTAL
+ Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");
+
+ if (targetExpression.Instance != null && !IsAtomicInstance(targetExpression.Instance)) {
+ //// Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
+ var se = ExpressionSimplifier.Simplify(this.sink, targetExpression);
+ this.Visit(se);
+ return;
+ }
+#endif
+
#region ArrayIndexer
IArrayIndexer/*?*/ indexer = targetExpression.Definition as IArrayIndexer;
if (indexer != null)
@@ -252,11 +277,14 @@ namespace BytecodeTranslator public override void Visit(IBoundExpression boundExpression)
{
- //if (boundExpression.Instance != null)
- //{
- // this.Visit(boundExpression.Instance);
- // // TODO: (mschaef) look where it's bound and do something
- //}
+
+ if (boundExpression.Instance != null && !IsAtomicInstance(boundExpression.Instance)) {
+ // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.
+ var se = ExpressionSimplifier.Simplify(this.sink, boundExpression);
+ this.Visit(se);
+ return;
+ }
+
#region Local
ILocalDefinition local = boundExpression.Definition as ILocalDefinition;
if (local != null)
@@ -290,9 +318,9 @@ namespace BytecodeTranslator }
else {
Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
- Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(field.ResolvedField.Type));
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, temp.Type)));
- TranslatedExpressions.Push(temp);
+ var bplType = this.sink.CciTypeToBoogie(field.Type);
+ var e = this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, bplType);
+ this.TranslatedExpressions.Push(e);
}
}
return;
@@ -339,6 +367,14 @@ namespace BytecodeTranslator #endregion
}
+ internal static bool IsAtomicInstance(IExpression expression) {
+ var thisInst = expression as IThisReference;
+ if (thisInst != null) return true;
+ var be = expression as IBoundExpression;
+ if (be == null) return false;
+ return be.Instance == null;
+ }
+
public override void Visit(IPopValue popValue) {
var locExpr = this.StmtTraverser.operandStack.Pop();
this.TranslatedExpressions.Push(locExpr);
@@ -604,6 +640,7 @@ namespace BytecodeTranslator private Bpl.Expr arrayExpr = null;
private Bpl.Expr indexExpr = null;
+#if EXPERIMENTAL
/// <summary>
///
/// </summary>
@@ -612,9 +649,108 @@ namespace BytecodeTranslator public override void Visit(IAssignment assignment) {
Contract.Assert(TranslatedExpressions.Count == 0);
+ var tok = assignment.Token();
+
+ object container = assignment.Target.Definition;
+
+ var/*?*/ local = container as ILocalDefinition;
+ if (local != null) {
+ Contract.Assume(assignment.Target.Instance == null);
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ var bplLocal = Bpl.Expr.Ident(this.sink.FindOrCreateLocalVariable(local));
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplLocal, e));
+ return;
+ }
+
+ var/*?*/ parameter = container as IParameterDefinition;
+ if (parameter != null) {
+ Contract.Assume(assignment.Target.Instance == null);
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ var bplParam = Bpl.Expr.Ident(this.sink.FindParameterVariable(parameter, this.contractContext));
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplParam, e));
+ return;
+ }
+
+ var/*?*/ field = container as IFieldReference;
+ if (field != null) {
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));
+ if (assignment.Target.Instance == null) {
+ // static fields are not kept in the heap
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, f, e));
+ } else {
+ if (field.ContainingType.ResolvedType.IsStruct) {
+ //var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);
+ //var s_prime_expr = Bpl.Expr.Ident(s_prime);
+ //var boogieType = sink.CciTypeToBoogie(field.Type);
+ //StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,
+ // field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,
+ // boogieType));
+ UpdateStruct(tok, assignment.Target.Instance, field, e);
+ } else {
+ this.Visit(assignment.Target.Instance);
+ var x = this.TranslatedExpressions.Pop();
+ var boogieType = sink.CciTypeToBoogie(field.Type);
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,
+ field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,
+ boogieType));
+ }
+ }
+ return;
+ }
+
+ var/*?*/ arrayIndexer = container as IArrayIndexer;
+ if (arrayIndexer != null) {
+ this.Visit(assignment.Target.Instance);
+ var x = this.TranslatedExpressions.Pop();
+ this.Visit(arrayIndexer.Indices);
+ var indices_prime = this.TranslatedExpressions.Pop();
+ this.Visit(assignment.Source);
+ var e = this.TranslatedExpressions.Pop();
+ StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, x, indices_prime, e, AccessType.Array, sink.CciTypeToBoogie(arrayIndexer.Type)));
+ return;
+ }
+
+ Contract.Assume(false);
+ }
+
+ private void UpdateStruct(Bpl.IToken tok, IExpression iExpression, IFieldReference field, Bpl.Expr e) {
+ var addrOf = iExpression as IAddressOf;
+ if (addrOf == null) return;
+ var addressableExpression = addrOf.Expression as IAddressableExpression;
+ if (addressableExpression == null) return;
+
+ var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));
+
+ if (addressableExpression.Instance == null) {
+ var boogieType = sink.CciTypeToBoogie(field.Type);
+ this.Visit(addressableExpression);
+ var def = this.TranslatedExpressions.Pop();
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, def, f, e,
+ AccessType.Struct,
+ boogieType));
+ } else {
+ var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);
+ var s_prime_expr = Bpl.Expr.Ident(s_prime);
+ var boogieType = sink.CciTypeToBoogie(field.Type);
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,
+ AccessType.Struct,
+ boogieType));
+ UpdateStruct(tok, addressableExpression.Instance, addressableExpression.Definition as IFieldReference, s_prime_expr);
+ }
+ }
+
+#else
+
+ public override void Visit(IAssignment assignment) {
+ Contract.Assert(TranslatedExpressions.Count == 0);
+
#region Transform Right Hand Side ...
this.Visit(assignment.Source);
- Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();
+ var sourceexp = this.TranslatedExpressions.Pop();
#endregion
// Simplify the LHS so that all nested dereferences and method calls are broken
@@ -643,8 +779,7 @@ namespace BytecodeTranslator Bpl.IdentifierExpr f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(fieldReference.ResolvedField));
if (target.Instance == null) {
StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(), f, sourceexp));
- }
- else {
+ } else {
Debug.Assert(args != null);
List<Bpl.Variable> locals = new List<Bpl.Variable>();
Bpl.IdentifierExpr instanceExpr = TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
@@ -715,6 +850,8 @@ namespace BytecodeTranslator return;
}
+#endif
+
#endregion
#region Translate Object Creation
@@ -1161,74 +1298,123 @@ namespace BytecodeTranslator }
#endregion
+ public override void Visit(IBlockExpression blockExpression) {
+ this.StmtTraverser.Visit(blockExpression.BlockStatement);
+ this.Visit(blockExpression.Expression);
+ }
+
/// <summary>
/// This is a rewriter so it must be used on a mutable Code Model!!!
/// </summary>
- private class AssignmentSimplifier : CodeRewriter {
+ private class ExpressionSimplifier : CodeRewriter {
Sink sink;
- private List<IStatement> localDeclarations = new List<IStatement>();
- private AssignmentSimplifier(Sink sink)
+ private ExpressionSimplifier(Sink sink)
: base(sink.host) {
this.sink = sink;
}
- public static IBlockExpression Simplify(Sink sink, ITargetExpression targetExpression) {
- var a = new AssignmentSimplifier(sink);
- var leftOverExpression = a.Rewrite(targetExpression);
- return new BlockExpression() {
- BlockStatement = new BlockStatement() { Statements = a.localDeclarations, },
- Expression = leftOverExpression,
- Type = targetExpression.Type,
- };
+ public static IExpression Simplify(Sink sink, IExpression expression) {
+ var a = new ExpressionSimplifier(sink);
+ return a.Rewrite(expression);
}
public override IExpression Rewrite(IBoundExpression boundExpression) {
- if (boundExpression.Instance == null)
- return base.Rewrite(boundExpression); // REVIEW: Maybe just stop the rewriting and return boundExpression?
- var e = base.Rewrite(boundExpression);
- boundExpression = e as IBoundExpression;
- if (boundExpression == null) return e;
+
+ if (ExpressionTraverser.IsAtomicInstance(boundExpression.Instance)) return boundExpression;
+
+ // boundExpression == BE(inst, def), i.e., inst.def
+ // return { loc := e; [assert loc != null;] | BE(BE(null,loc), def) }, i.e., "loc := e; loc.def"
+ // where e is the rewritten inst
+
+ var e = base.Rewrite(boundExpression.Instance);
+
var loc = new LocalDefinition() {
- Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()), // TODO: should make the name unique within the method containing the assignment
+ Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),
Type = boundExpression.Type,
};
- this.localDeclarations.Add(
- new LocalDeclarationStatement() {
- InitialValue = boundExpression,
- LocalVariable = loc,
- }
- );
- return new BoundExpression() {
- Definition = loc,
- Instance = null,
- Type = boundExpression.Type,
+ var locDecl = new LocalDeclarationStatement() {
+ InitialValue = e,
+ LocalVariable = loc,
};
+ return new BlockExpression() {
+ BlockStatement = new BlockStatement() {
+ Statements = new List<IStatement> { locDecl },
+ },
+ Expression = new BoundExpression() {
+ Definition = boundExpression.Definition,
+ Instance = new BoundExpression() {
+ Definition = loc,
+ Instance = null,
+ Type = loc.Type,
+ },
+ Type = boundExpression.Type,
+ },
+ };
+
}
- public override IExpression Rewrite(IMethodCall methodCall) {
+ public override IExpression Rewrite(IArrayIndexer arrayIndexer) {
+ if (ExpressionTraverser.IsAtomicInstance(arrayIndexer.IndexedObject)) return arrayIndexer;
- var e = base.Rewrite(methodCall); // simplify anything deeper in the tree
- methodCall = e as IMethodCall;
- if (methodCall == null) return e;
+ // arrayIndexer == AI(inst, [index]), i.e., inst[index0, index1,...]
+ // return { loc := e; [assert loc != null;] | AI(BE(null,loc), [index]) }
+ // where e is the rewritten array instance
+
+ var e = base.Rewrite(arrayIndexer.IndexedObject);
var loc = new LocalDefinition() {
- Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment
- Type = methodCall.Type,
+ Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),
+ Type = arrayIndexer.Type,
};
- this.localDeclarations.Add(
- new LocalDeclarationStatement() {
- InitialValue = methodCall,
- LocalVariable = loc,
- }
- );
- return new BoundExpression() {
- Definition = loc,
- Instance = null,
- Type = methodCall.Type,
+ var locDecl = new LocalDeclarationStatement() {
+ InitialValue = e,
+ LocalVariable = loc,
+ };
+ return new BlockExpression() {
+ BlockStatement = new BlockStatement() {
+ Statements = new List<IStatement> { locDecl },
+ },
+ Expression = new ArrayIndexer() {
+ IndexedObject = new BoundExpression() {
+ Definition = loc,
+ Instance = null,
+ Type = loc.Type,
+ },
+ Indices = new List<IExpression>(arrayIndexer.Indices),
+ Type = arrayIndexer.Type,
+ },
};
}
+
+ public override ITargetExpression Rewrite(ITargetExpression targetExpression) {
+ Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");
+ return null;
+ }
+
+ //public override IExpression Rewrite(IMethodCall methodCall) {
+
+ // var e = base.Rewrite(methodCall); // simplify anything deeper in the tree
+ // methodCall = e as IMethodCall;
+ // if (methodCall == null) return e;
+
+ // var loc = new LocalDefinition() {
+ // Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment
+ // Type = methodCall.Type,
+ // };
+ // this.localDeclarations.Add(
+ // new LocalDeclarationStatement() {
+ // InitialValue = methodCall,
+ // LocalVariable = loc,
+ // }
+ // );
+ // return new BoundExpression() {
+ // Definition = loc,
+ // Instance = null,
+ // Type = methodCall.Type,
+ // };
+ //}
}
}
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 58bec27f..b1be6294 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -46,7 +46,12 @@ namespace BytecodeTranslator { }
public override void Visit(IAssembly assembly) {
- base.Visit(assembly);
+ this.sink.BeginAssembly(assembly);
+ try {
+ base.Visit(assembly);
+ } finally {
+ this.sink.EndAssembly(assembly);
+ }
}
/// <summary>
@@ -55,6 +60,9 @@ namespace BytecodeTranslator { ///
public override void Visit(ITypeDefinition typeDefinition) {
+ var savedPrivateTypes = this.privateTypes;
+ this.privateTypes = new List<ITypeDefinition>();
+
if (typeDefinition.IsClass) {
bool savedSawCctor = this.sawCctor;
this.sawCctor = false;
@@ -80,7 +88,12 @@ namespace BytecodeTranslator { TypeHelper.GetTypeName(typeDefinition));
throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition)));
}
+ this.Visit(typeDefinition.PrivateHelperMembers);
+ foreach (var t in this.privateTypes) {
+ this.Visit(t);
+ }
}
+ List<ITypeDefinition> privateTypes = new List<ITypeDefinition>();
private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {
Contract.Requires(typeDefinition.IsStruct);
@@ -256,7 +269,11 @@ namespace BytecodeTranslator { #endregion
#region Translate body
- method.Body.Dispatch(stmtTraverser);
+ var helperTypes = stmtTraverser.TranslateMethod(method);
+ if (helperTypes != null) {
+ this.privateTypes.AddRange(helperTypes);
+ }
+ //method.Body.Dispatch(stmtTraverser);
#endregion
#region Create Local Vars For Implementation
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index f42c34d9..471b3431 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -132,12 +132,19 @@ namespace BytecodeTranslator { var copier = new CodeDeepCopier(host);
var mutableModule = copier.Copy(module);
- var mutator = new ReparentModule(host,
- TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType),
- mutableModule);
- module = mutator.Rewrite(mutableModule);
+ var mscorlib = TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType);
+
+ //var mutator = new ReparentModule(host, mscorlib, mutableModule);
+ //module = mutator.Rewrite(mutableModule);
+ //modules.Add(Tuple.Create(module, pdbReader));
+
+ RewriteUnitReferences renamer = new RewriteUnitReferences(host, mutableModule);
+ var mscorlibAssembly = (IAssembly)mscorlib;
+ renamer.targetAssembly = mscorlibAssembly;
+ renamer.originalAssemblyIdentity = mscorlibAssembly.AssemblyIdentity;
+ renamer.RewriteChildren(mutableModule);
+ modules.Add(Tuple.Create((IModule)mutableModule, pdbReader));
- modules.Add(Tuple.Create(module, pdbReader));
}
}
if (modules.Count == 0) {
@@ -340,6 +347,34 @@ namespace BytecodeTranslator { // Maybe this is a good place to add the procedure to the toplevel declarations
}
}
+
+ private class RewriteUnitReferences : MetadataRewriter {
+ private UnitIdentity sourceUnitIdentity = null;
+ internal IAssembly/*?*/ targetAssembly = null;
+ internal AssemblyIdentity/*?*/ originalAssemblyIdentity = null;
+
+ Dictionary<uint, bool> internedKeys = new Dictionary<uint, bool>();
+
+ public RewriteUnitReferences(IMetadataHost host, Module sourceUnit)
+ : base(host) {
+ this.sourceUnitIdentity = sourceUnit.UnitIdentity;
+ }
+
+ public override IModuleReference Rewrite(IModuleReference moduleReference) {
+ if (this.sourceUnitIdentity.Equals(moduleReference.UnitIdentity)) {
+ return this.targetAssembly;
+ }
+ return base.Rewrite(moduleReference);
+ }
+ public override IAssemblyReference Rewrite(IAssemblyReference assemblyReference) {
+ if (this.sourceUnitIdentity.Equals(assemblyReference.UnitIdentity)) {
+ return this.targetAssembly;
+ }
+ return base.Rewrite(assemblyReference);
+ }
+
+ }
+
}
}
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index b8d8334d..852c3986 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -118,7 +118,7 @@ namespace BytecodeTranslator { return heap.StructType;
else if (type.IsEnum)
return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer
- else if (type is IGenericTypeParameter)
+ else if (type is IGenericTypeParameter)
return heap.BoxType;
else
return heap.RefType;
@@ -167,7 +167,9 @@ namespace BytecodeTranslator { Bpl.IToken tok = local.Token();
Bpl.Type t = CciTypeToBoogie(local.Type.ResolvedType);
if (!localVarMap.TryGetValue(local, out v)) {
- v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));
+ var name = local.Name.Value;
+ name = TranslationHelper.TurnStringIntoValidIdentifier(name);
+ v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, t));
localVarMap.Add(local, v);
}
return v;
@@ -334,6 +336,7 @@ namespace BytecodeTranslator { ProcedureInfo procAndFormalMap;
var key = method.InternedKey;
+
if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {
string MethodName = TranslationHelper.CreateUniqueMethodName(method);
@@ -375,7 +378,7 @@ namespace BytecodeTranslator { Bpl.Formal selfOut = null;
#region Create 'this' parameter
if (!method.IsStatic) {
- Bpl.Type selfType = CciTypeToBoogie(method.ContainingType);
+ var selfType = CciTypeToBoogie(method.ContainingType);
if (method.ContainingType.ResolvedType.IsStruct) {
//selfType = Heap.StructType;
in_count++;
@@ -470,15 +473,16 @@ namespace BytecodeTranslator { #endregion
+ var tok = method.Token();
Bpl.DeclWithFormals decl;
if (IsPure(method)) {
- var func = new Bpl.Function(method.Token(),
+ var func = new Bpl.Function(tok,
MethodName,
new Bpl.VariableSeq(invars),
this.RetVariable);
decl = func;
} else {
- var proc = new Bpl.Procedure(method.Token(),
+ var proc = new Bpl.Procedure(tok,
MethodName,
new Bpl.TypeVariableSeq(),
new Bpl.VariableSeq(invars),
@@ -488,7 +492,10 @@ namespace BytecodeTranslator { boogiePostcondition);
decl = proc;
}
-
+ if (!TypeHelper.GetDefiningUnitReference(method.ContainingType).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity)) {
+ var attrib = new Bpl.QKeyValue(tok, "extern", new List<object>(1), null);
+ decl.Attributes = attrib;
+ }
string newName = null;
if (IsStubMethod(method, out newName)) {
@@ -573,7 +580,8 @@ namespace BytecodeTranslator { public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method) {
this.FindOrCreateProcedure(method);
- return this.declaredMethods[method.InternedKey];
+ var key = method.InternedKey;
+ return this.declaredMethods[key];
}
public static IMethodReference Unspecialize(IMethodReference method) {
IMethodReference result = method;
@@ -634,6 +642,15 @@ namespace BytecodeTranslator { this.localCounter = 0;
}
+ public void BeginAssembly(IAssembly assembly) {
+ this.assemblyBeingTranslated = assembly;
+ }
+
+ public void EndAssembly(IAssembly assembly) {
+ this.assemblyBeingTranslated = null;
+ }
+ private IAssembly assemblyBeingTranslated;
+
public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();
public void AddDelegate(ITypeDefinition type, IMethodDefinition defn)
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 24b4b2ca..0e13c510 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -50,13 +50,37 @@ namespace BytecodeTranslator return etrav.TranslatedExpressions.Pop();
}
+ public ICollection<ITypeDefinition>/*?*/ TranslateMethod(IMethodDefinition method) {
+ var methodBody = method.Body as ISourceMethodBody;
+ if (methodBody == null) return null;
+ var block = methodBody.Block as BlockStatement;
+ // TODO: Error if cast fails?
+
+ ICollection<ITypeDefinition> newTypes = null;
+ if (block != null) {
+ var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);
+ newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);
+ }
+ this.Visit(methodBody);
+ return newTypes;
+ }
+
#endregion
- public override void Visit(IBlockStatement block) {
- Bpl.StmtListBuilder slb = new Bpl.StmtListBuilder();
+ //public override void Visit(ISourceMethodBody methodBody) {
+ // var block = methodBody.Block as BlockStatement;
+ // // TODO: Error if cast fails?
+
+ // if (block != null) {
+ // var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);
+ // var newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);
+ // }
+ // base.Visit(methodBody);
+ //}
- foreach (IStatement st in block.Statements) {
- this.Visit(st);
+ public override void Visit(IBlockStatement block) {
+ foreach (var s in block.Statements) {
+ this.Visit(s);
}
}
|