summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator
diff options
context:
space:
mode:
Diffstat (limited to 'BCT/BytecodeTranslator')
-rw-r--r--BCT/BytecodeTranslator/BytecodeTranslator.csproj12
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs641
-rw-r--r--BCT/BytecodeTranslator/Heap.cs71
-rw-r--r--BCT/BytecodeTranslator/HeapFactory.cs4
-rw-r--r--BCT/BytecodeTranslator/MetadataTraverser.cs50
-rw-r--r--BCT/BytecodeTranslator/Program.cs93
-rw-r--r--BCT/BytecodeTranslator/Sink.cs35
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs34
-rw-r--r--BCT/BytecodeTranslator/TraverserFactory.cs6
-rw-r--r--BCT/BytecodeTranslator/WholeProgram.cs88
10 files changed, 694 insertions, 340 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..08e32248 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);
@@ -433,102 +469,26 @@ namespace BytecodeTranslator
MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));
}
- #region Translate In and Out Parameters
- var inexpr = new List<Bpl.Expr>();
- var outvars = new List<Bpl.IdentifierExpr>();
-
- #region Create the 'this' argument for the function call
- Bpl.IdentifierExpr thisExpr = null;
- List<Bpl.Variable> locals = null;
- List<IFieldDefinition> args = null;
- Bpl.Expr arrayExpr = null;
- Bpl.Expr indexExpr = null;
- if (!methodCall.IsStaticCall) {
- this.collectStructFields = true;
- this.structFields = new List<IFieldDefinition>();
- this.arrayExpr = null;
- this.indexExpr = null;
- this.Visit(methodCall.ThisArgument);
- this.collectStructFields = false;
- args = this.structFields;
- arrayExpr = this.arrayExpr;
- indexExpr = this.indexExpr;
-
- var e = this.TranslatedExpressions.Pop();
- inexpr.Add(e);
- if (e is Bpl.NAryExpr) {
- e = ((Bpl.NAryExpr)e).Args[0];
- }
- thisExpr = e as Bpl.IdentifierExpr;
- locals = new List<Bpl.Variable>();
- Bpl.Variable x = thisExpr.Decl;
- locals.Add(x);
- for (int i = 0; i < args.Count; i++) {
- Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));
- Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);
- StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));
- x = y;
- locals.Add(y);
- }
- }
- if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
- outvars.Add(thisExpr);
- }
- #endregion
+ Bpl.IToken cloc = methodCall.Token();
- Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();
- Dictionary<IParameterDefinition, Bpl.IdentifierExpr> p2eMap = new Dictionary<IParameterDefinition, Bpl.IdentifierExpr>();
- IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
- penum.MoveNext();
- foreach (IExpression exp in methodCall.Arguments) {
- if (penum.Current == null) {
- throw new TranslationException("More arguments than parameters in method call");
- }
- this.Visit(exp);
- Bpl.Expr e = this.TranslatedExpressions.Pop();
- if (penum.Current.Type is IGenericTypeParameter)
- inexpr.Add(sink.Heap.Box(methodCall.Token(), this.sink.CciTypeToBoogie(exp.Type), e));
- else
- inexpr.Add(e);
- if (penum.Current.IsByReference) {
- Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;
- if (unboxed == null) {
- throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");
- }
- if (penum.Current.Type is IGenericTypeParameter) {
- Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));
- toBoxed[unboxed] = boxed;
- outvars.Add(boxed);
- }
- else {
- outvars.Add(unboxed);
- }
- }
- penum.MoveNext();
- }
- #endregion
+ List<Bpl.Expr> inexpr;
+ List<Bpl.IdentifierExpr> outvars;
+ Bpl.IdentifierExpr thisExpr;
+ List<Bpl.Variable> locals;
+ List<IFieldDefinition> args;
+ Bpl.Expr arrayExpr;
+ Bpl.Expr indexExpr;
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
+ var proc = TranslateArgumentsAndReturnProcedure(cloc, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);
- Bpl.IToken cloc = methodCall.Token();
- if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
- Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);
- if (resolvedMethod.Type is IGenericTypeParameter) {
- Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));
- toBoxed[unboxed] = boxed;
- outvars.Add(boxed);
- }
- else {
- outvars.Add(unboxed);
- }
- TranslatedExpressions.Push(unboxed);
- }
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
string methodname = proc.Name;
-
+ var translateAsFunctionCall = proc is Bpl.Function;
Bpl.QKeyValue attrib = null;
- foreach (var a in resolvedMethod.Attributes) {
- if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
- attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);
+ if (!translateAsFunctionCall) {
+ foreach (var a in resolvedMethod.Attributes) {
+ if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
+ attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);
+ }
}
}
@@ -563,13 +523,24 @@ namespace BytecodeTranslator
else {
this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));
}
- }
- else {
- if (attrib != null)
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
- else
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
+ } else {
+ if (translateAsFunctionCall) {
+ var func = proc as Bpl.Function;
+ var exprSeq = new Bpl.ExprSeq();
+ foreach (var e in inexpr) {
+ exprSeq.Add(e);
+ }
+ var callFunction = new Bpl.NAryExpr(cloc, new Bpl.FunctionCall(func), exprSeq);
+ this.TranslatedExpressions.Push(callFunction);
+ return;
+
+ } else {
+ if (attrib != null)
+ call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
+ else
+ call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ }
}
foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {
@@ -596,6 +567,99 @@ namespace BytecodeTranslator
}
}
+ protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out List<Bpl.Variable> locals, out List<IFieldDefinition> args, out Bpl.Expr arrayExpr, out Bpl.Expr indexExpr, out Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed) {
+ inexpr = new List<Bpl.Expr>();
+ outvars = new List<Bpl.IdentifierExpr>();
+
+ #region Create the 'this' argument for the function call
+ thisExpr = null;
+ locals = null;
+ args = null;
+ arrayExpr = null;
+ indexExpr = null;
+ if (thisArg != null) {
+ this.collectStructFields = true;
+ this.structFields = new List<IFieldDefinition>();
+ this.arrayExpr = null;
+ this.indexExpr = null;
+ this.Visit(thisArg);
+ this.collectStructFields = false;
+ args = this.structFields;
+ arrayExpr = this.arrayExpr;
+ indexExpr = this.indexExpr;
+
+ var e = this.TranslatedExpressions.Pop();
+ inexpr.Add(e);
+ if (e is Bpl.NAryExpr) {
+ e = ((Bpl.NAryExpr)e).Args[0];
+ }
+ thisExpr = e as Bpl.IdentifierExpr;
+ locals = new List<Bpl.Variable>();
+ Bpl.Variable x = thisExpr.Decl;
+ locals.Add(x);
+ for (int i = 0; i < args.Count; i++) {
+ Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));
+ Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);
+ StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));
+ x = y;
+ locals.Add(y);
+ }
+ }
+ if (thisArg != null && methodToCall.ContainingType.ResolvedType.IsStruct) {
+ outvars.Add(thisExpr);
+ }
+ #endregion
+
+ toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();
+ IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
+ penum.MoveNext();
+ foreach (IExpression exp in arguments) {
+ if (penum.Current == null) {
+ throw new TranslationException("More arguments than parameters in method call");
+ }
+ this.Visit(exp);
+ Bpl.Expr e = this.TranslatedExpressions.Pop();
+ if (penum.Current.Type is IGenericTypeParameter)
+ inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(exp.Type), e));
+ else
+ inexpr.Add(e);
+ if (penum.Current.IsByReference) {
+ Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;
+ if (unboxed == null) {
+ throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");
+ }
+ if (penum.Current.Type is IGenericTypeParameter) {
+ Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));
+ toBoxed[unboxed] = boxed;
+ outvars.Add(boxed);
+ } else {
+ outvars.Add(unboxed);
+ }
+ }
+ penum.MoveNext();
+ }
+
+ var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
+
+ var translateAsFunctionCall = proc is Bpl.Function;
+ if (!translateAsFunctionCall) {
+ if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
+ Bpl.Variable v = this.sink.CreateFreshLocal(resolvedMethod.Type.ResolvedType);
+ Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);
+ if (resolvedMethod.Type is IGenericTypeParameter) {
+ Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));
+ toBoxed[unboxed] = boxed;
+ outvars.Add(boxed);
+ } else {
+ outvars.Add(unboxed);
+ }
+ TranslatedExpressions.Push(unboxed);
+ }
+ }
+
+ return proc;
+ }
+
#endregion
#region Translate Assignments
@@ -604,6 +668,7 @@ namespace BytecodeTranslator
private Bpl.Expr arrayExpr = null;
private Bpl.Expr indexExpr = null;
+#if EXPERIMENTAL
/// <summary>
///
/// </summary>
@@ -612,18 +677,119 @@ 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
// up into separate assignments to locals.
- var blockExpression = AssignmentSimplifier.Simplify(this.sink, assignment.Target);
- foreach (var s in blockExpression.BlockStatement.Statements) {
- this.StmtTraverser.Visit(s);
- }
- var target = blockExpression.Expression as ITargetExpression;
+ //var blockExpression = ExpressionSimplifier.Simplify(this.sink, assignment.Target) as IBlockExpression;
+ //foreach (var s in blockExpression.BlockStatement.Statements) {
+ // this.StmtTraverser.Visit(s);
+ //}
+ //var target = blockExpression.Expression as ITargetExpression;
+
+ var target = assignment.Target;
List<IFieldDefinition> args = null;
Bpl.Expr arrayExpr = null;
@@ -643,8 +809,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 +880,8 @@ namespace BytecodeTranslator
return;
}
+#endif
+
#endregion
#region Translate Object Creation
@@ -725,77 +892,35 @@ namespace BytecodeTranslator
/// </summary>
public override void Visit(ICreateObjectInstance createObjectInstance)
{
- TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance);
- }
-
- public override void Visit(ICreateArray createArrayInstance)
- {
- TranslateArrayCreation(createArrayInstance);
- }
-
- public override void Visit(ICreateDelegateInstance createDelegateInstance)
- {
- if (createDelegateInstance.Instance == null) {
- TranslatedExpressions.Push(Bpl.Expr.Literal(0));
- }
- else {
- this.Visit(createDelegateInstance.Instance);
- }
-
- TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);
- }
-
- private void TranslateArrayCreation(IExpression creationAST)
- {
- Bpl.IToken cloc = creationAST.Token();
-
- var a = this.sink.CreateFreshLocal(creationAST.Type);
-
- // First generate an Alloc() call
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
-
- TranslatedExpressions.Push(Bpl.Expr.Ident(a));
- }
-
- private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)
- {
+ var ctor = createObjectInstance.MethodToCall;
var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;
- Bpl.IToken token = creationAST.Token();
-
- var a = this.sink.CreateFreshLocal(creationAST.Type);
+ Bpl.IToken token = createObjectInstance.Token();
+
+ var a = this.sink.CreateFreshLocal(createObjectInstance.Type);
// First generate an Alloc() call
this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
// Second, generate the call to the appropriate ctor
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
- Bpl.ExprSeq inexpr = new Bpl.ExprSeq();
- inexpr.Add(Bpl.Expr.Ident(a));
- IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
- penum.MoveNext();
- foreach (IExpression exp in arguments) {
- if (penum.Current == null) {
- throw new TranslationException("More Arguments than Parameters in functioncall");
- }
- this.Visit(exp);
- Bpl.Expr e = this.TranslatedExpressions.Pop();
- if (penum.Current.Type is IGenericTypeParameter)
- inexpr.Add(sink.Heap.Box(ctor.Token(), this.sink.CciTypeToBoogie(exp.Type), e));
- else
- inexpr.Add(e);
- penum.MoveNext();
- }
- Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();
+ List<Bpl.Expr> inexpr;
+ List<Bpl.IdentifierExpr> outvars;
+ Bpl.IdentifierExpr thisExpr;
+ List<Bpl.Variable> locals;
+ List<IFieldDefinition> args;
+ Bpl.Expr arrayExpr;
+ Bpl.Expr indexExpr;
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
+ var proc = TranslateArgumentsAndReturnProcedure(token, ctor, resolvedMethod, null, createObjectInstance.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);
this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, proc.Name, inexpr, outvars));
// Generate assumption about the dynamic type of the just allocated object
this.StmtTraverser.StmtBuilder.Add(
- new Bpl.AssumeCmd(token,
+ new Bpl.AssumeCmd(token,
Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
this.sink.Heap.DynamicType(inexpr[0]),
- Bpl.Expr.Ident(this.sink.FindOrCreateType(creationAST.Type))
+ Bpl.Expr.Ident(this.sink.FindOrCreateType(createObjectInstance.Type))
)
)
);
@@ -803,6 +928,37 @@ namespace BytecodeTranslator
TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
+ public override void Visit(ICreateArray createArrayInstance)
+ {
+ Bpl.IToken cloc = createArrayInstance.Token();
+ var a = this.sink.CreateFreshLocal(createArrayInstance.Type);
+
+ Debug.Assert(createArrayInstance.Rank > 0);
+ Bpl.Expr lengthExpr = Bpl.Expr.Literal(1);
+ foreach (IExpression expr in createArrayInstance.Sizes) {
+ this.Visit(expr);
+ lengthExpr = Bpl.Expr.Mul(lengthExpr, TranslatedExpressions.Pop());
+ }
+
+ // First generate an Alloc() call
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
+ Bpl.Expr assumeExpr = Bpl.Expr.Eq(new Bpl.NAryExpr(cloc, new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(Bpl.Expr.Ident(a))), lengthExpr);
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.AssumeCmd(cloc, assumeExpr));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(a));
+ }
+
+ public override void Visit(ICreateDelegateInstance createDelegateInstance)
+ {
+ if (createDelegateInstance.Instance == null) {
+ TranslatedExpressions.Push(Bpl.Expr.Literal(0));
+ }
+ else {
+ this.Visit(createDelegateInstance.Instance);
+ }
+
+ TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);
+ }
+
private void TranslateDelegateCreation(IMethodReference methodToCall, ITypeReference type, IExpression creationAST)
{
Bpl.IToken cloc = creationAST.Token();
@@ -1134,9 +1290,7 @@ namespace BytecodeTranslator
public override void Visit(IVectorLength vectorLength) {
base.Visit(vectorLength.Vector);
var e = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(
- Bpl.Expr.Select(new Bpl.IdentifierExpr(vectorLength.Token(), this.sink.Heap.ArrayLengthVariable), new Bpl.Expr[] { e })
- );
+ TranslatedExpressions.Push(new Bpl.NAryExpr(vectorLength.Token(), new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(e)));
}
#endregion
@@ -1161,74 +1315,125 @@ 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;
+
+ // 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(methodCall); // simplify anything deeper in the tree
- methodCall = e as IMethodCall;
- if (methodCall == null) return e;
+ 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,
+ },
+ };
+ }
+
+#if EXPERIMENTAL
+ 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;
}
+#endif
+
+ //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/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 283a59a3..87d950c4 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -56,6 +56,35 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );
axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
+{
+ $result := $TypeOf($DynamicType(this));
+}
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start(this: Ref)
+{
+ call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
+}
+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
+
";
private Sink sink;
@@ -71,7 +100,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());
this.RefType = new Bpl.CtorType(this.RefTypeDecl.tok, this.RefTypeDecl, new Bpl.TypeSeq());
this.RealType = new Bpl.CtorType(this.RealTypeDecl.tok, this.RealTypeDecl, new Bpl.TypeSeq());
- }
+ }
return b;
}
@@ -82,6 +111,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = field.Token();
Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);
@@ -100,6 +130,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
string eventName = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ eventName = TranslationHelper.TurnStringIntoValidIdentifier(eventName);
Bpl.IToken tok = e.Token();
Bpl.Type t = this.sink.CciTypeToBoogie(e.Type.ResolvedType);
@@ -108,7 +139,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
v = new Bpl.GlobalVariable(tok, tident);
}
else {
- Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);
+ Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.RefType), t);
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, mt);
v = new Bpl.GlobalVariable(tok, tident);
}
@@ -125,11 +156,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
/// </param>
public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType) {
if (accessType == AccessType.Struct)
- return Bpl.Expr.Select(o, f);
+ return Unbox(f.tok, unboxType, Bpl.Expr.Select(o, f));
else if (accessType == AccessType.Heap)
return Bpl.Expr.Select(f, o);
else
- return Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f);
+ return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));
}
/// <summary>
@@ -139,11 +170,11 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType) {
Debug.Assert(o != null);
if (accessType == AccessType.Struct)
- return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, value);
+ return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, Box(f.tok, boxType, value));
else if (accessType == AccessType.Heap)
return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)f, o, value);
else
- return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, value)));
+ return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, Box(f.tok, boxType, value))));
}
}
@@ -192,6 +223,33 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );
axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
+{
+ $result := $TypeOf($DynamicType(this));
+}
+function $TypeOfInv(Ref): Type;
+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
+
+function $ThreadDelegate(Ref) : Ref;
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
+{
+ call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
+}
+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+
+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
+{
+ assume $ThreadDelegate(this) == start$in;
+}
+procedure {:inline 1} System.Threading.Thread.Start(this: Ref)
+{
+ call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
+}
+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
";
private Sink sink;
@@ -239,6 +297,7 @@ axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );
public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = e.Token();
if (e.Adder.ResolvedMethod.IsStatic) {
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 6d03ef9f..004d4224 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -68,8 +68,8 @@ namespace BytecodeTranslator {
{
[RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Box;")]
public Bpl.Variable ArrayContentsVariable = null;
- [RepresentationFor("$ArrayLength", "var $ArrayLength: [Ref]int;")]
- public Bpl.Variable ArrayLengthVariable = null;
+ [RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]
+ public Bpl.Function ArrayLengthFunction = null;
public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 58bec27f..75601140 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -30,23 +30,31 @@ namespace BytecodeTranslator {
public readonly TraverserFactory factory;
- public readonly PdbReader/*?*/ PdbReader;
+ public readonly IDictionary<IUnit, PdbReader> PdbReaders;
+ public PdbReader/*?*/ PdbReader;
- public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader)
+ public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
: base() {
this.sink = sink;
this.factory = sink.Factory;
- this.PdbReader = pdbReader;
+ this.PdbReaders = pdbReaders;
}
#region Overrides
public override void Visit(IModule module) {
+ this.PdbReaders.TryGetValue(module, out this.PdbReader);
base.Visit(module);
}
public override void Visit(IAssembly assembly) {
- base.Visit(assembly);
+ this.PdbReaders.TryGetValue(assembly, out this.PdbReader);
+ this.sink.BeginAssembly(assembly);
+ try {
+ base.Visit(assembly);
+ } finally {
+ this.sink.EndAssembly(assembly);
+ }
}
/// <summary>
@@ -55,6 +63,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 +91,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 +272,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
@@ -272,6 +292,8 @@ namespace BytecodeTranslator {
Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());
#endregion
+ var translatedBody = stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken);
+
#region Add implementation to Boogie program
if (proc != null) {
Bpl.Implementation impl =
@@ -281,13 +303,14 @@ namespace BytecodeTranslator {
decl.InParams,
decl.OutParams,
vseq,
- stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));
+ translatedBody);
impl.Proc = proc;
this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
} else { // method is translated as a function
- //Bpl.Function func = decl as Bpl.Function;
- //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), new List<Bpl.Block>{ new Bpl.Block(
+ //var func = decl as Bpl.Function;
+ //Contract.Assume(func != null);
+ //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), translatedBody.BigBlocks);
}
#endregion
@@ -366,6 +389,15 @@ namespace BytecodeTranslator {
#endregion
+ #region Public API
+ public virtual void TranslateAssemblies(IEnumerable<IUnit> assemblies) {
+ foreach (var a in assemblies) {
+ a.Dispatch(this);
+ }
+ }
+ #endregion
+
+ #region Helpers
private class FindCtorCall : BaseCodeTraverser {
private bool isDeferringCtor = false;
public ITypeReference containingType;
@@ -387,5 +419,7 @@ namespace BytecodeTranslator {
base.Visit(methodCall);
}
}
+ #endregion
+
}
} \ No newline at end of file
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index f42c34d9..50ac68cf 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -25,6 +25,9 @@ namespace BytecodeTranslator {
[OptionDescription("The names of the assemblies to use as input", ShortForm = "a")]
public List<string> assemblies = null;
+ [OptionDescription("Break into debugger", ShortForm = "break")]
+ public bool breakIntoDebugger = false;
+
[OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
@@ -36,7 +39,7 @@ namespace BytecodeTranslator {
public bool wholeProgram = false;
[OptionDescription("Stub assembly", ShortForm = "s")]
- public List<string>/*?*/ stubAssemblies = null;
+ public List<string>/*?*/ stub = null;
}
@@ -47,14 +50,21 @@ namespace BytecodeTranslator {
static int Main(string[] args)
{
int result = 0;
+ int errorReturnValue = -1;
#region Parse options
var options = new Options();
options.Parse(args);
+ if (options.HelpRequested) {
+ options.PrintOptions("");
+ return errorReturnValue;
+ }
if (options.HasErrors) {
- if (options.HelpRequested)
- options.PrintOptions("");
- return 1;
+ options.PrintErrorsAndExit(Console.Out);
+ }
+
+ if (options.breakIntoDebugger) {
+ System.Diagnostics.Debugger.Break();
}
#endregion
@@ -81,7 +91,7 @@ namespace BytecodeTranslator {
return 1;
}
- result = TranslateAssembly(assemblyNames, heap, options.libpaths, options.wholeProgram, options.stubAssemblies);
+ result = TranslateAssembly(assemblyNames, heap, options.libpaths, options.wholeProgram, options.stub);
} catch (Exception e) { // swallow everything and just return an error code
Console.WriteLine("The byte-code translator failed: {0}", e.Message);
@@ -98,7 +108,9 @@ namespace BytecodeTranslator {
var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
- var modules = new List<Tuple<IModule,PdbReader/*?*/>>();
+ var modules = new List<IModule>();
+ var contractExtractors = new Dictionary<IUnit, IContractProvider>();
+ var pdbReaders = new Dictionary<IUnit, PdbReader>();
foreach (var a in assemblyNames) {
var module = host.LoadUnitFrom(a) as IModule;
if (module == null || module == Dummy.Module || module == Dummy.Assembly) {
@@ -112,7 +124,9 @@ namespace BytecodeTranslator {
pdbReader = new PdbReader(pdbStream, host);
}
module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
- modules.Add(Tuple.Create(module, pdbReader));
+ modules.Add(module);
+ contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
+ pdbReaders.Add(module, pdbReader);
}
if (stubAssemblies != null) {
foreach (var s in stubAssemblies) {
@@ -132,12 +146,21 @@ 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((IModule)mutableModule);
+ contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));
+ pdbReaders.Add(module, pdbReader);
- modules.Add(Tuple.Create(module, pdbReader));
}
}
if (modules.Count == 0) {
@@ -145,7 +168,7 @@ namespace BytecodeTranslator {
return -1;
}
- var primaryModule = modules[0].Item1;
+ var primaryModule = modules[0];
TraverserFactory traverserFactory;
if (wholeProgram)
@@ -156,20 +179,8 @@ namespace BytecodeTranslator {
var sink = new Sink(host, traverserFactory, heapFactory);
TranslationHelper.tmpVarCounter = 0;
- foreach (var tup in modules) {
-
- var module = tup.Item1;
- var pdbReader = tup.Item2;
-
- IAssembly/*?*/ assembly = null;
- MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, host.GetContractExtractor(module.ModuleIdentity), pdbReader);
- assembly = module as IAssembly;
- if (assembly != null)
- translator.Visit(assembly);
- else
- translator.Visit(module);
-
- }
+ MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
+ translator.TranslateAssemblies(modules);
foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys) {
CreateDispatchMethod(sink, type);
@@ -340,6 +351,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..97fd4441 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 (this.assemblyBeingTranslated != null && !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;
@@ -609,6 +617,10 @@ namespace BytecodeTranslator {
t = this.Heap.CreateTypeVariable(type);
this.declaredTypes.Add(key, t);
this.TranslatedProgram.TopLevelDeclarations.Add(t);
+ if (this.assemblyBeingTranslated != null && !TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity)) {
+ var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);
+ t.Attributes = attrib;
+ }
}
return t;
}
@@ -634,6 +646,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..d26f540d 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);
}
}
@@ -73,7 +97,7 @@ namespace BytecodeTranslator
if (this.PdbReader != null) {
var slocs = this.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);
foreach (var sloc in slocs) {
- fileName = sloc.Document.Name.Value;
+ fileName = sloc.Document.Location;
lineNumber = sloc.StartLine;
break;
}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index cdc1c8a3..78c818bd 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -18,9 +18,11 @@ using Bpl = Microsoft.Boogie;
namespace BytecodeTranslator {
public abstract class TraverserFactory {
- public virtual MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader/*?*/ pdbReader)
+ public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
+ IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
+ IDictionary<IUnit, PdbReader> sourceLocationProviders)
{
- return new MetadataTraverser(sink, pdbReader);
+ return new MetadataTraverser(sink, sourceLocationProviders);
}
public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
return new StatementTraverser(sink, pdbReader, contractContext);
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index 92154020..dd00768b 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -16,8 +16,7 @@ namespace BytecodeTranslator {
class WholeProgram : TraverserFactory {
/// <summary>
- /// Table to be filled by the metadata traverser when it first gets to an assembly.
- /// [TODO: It should be full set of assemblies that are being translated (CUA).]
+ /// Table to be filled by the metadata traverser before visiting any assemblies.
///
/// The table lists the direct supertypes of all type definitions that it encounters during the
/// traversal. (But the table is organized so that subTypes[T] is the list of type definitions
@@ -25,8 +24,10 @@ namespace BytecodeTranslator {
/// </summary>
readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes = new Dictionary<ITypeReference, List<ITypeReference>>();
- public override MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader pdbReader) {
- return new WholeProgramMetadataSemantics(this, sink, pdbReader);
+ public override MetadataTraverser MakeMetadataTraverser(Sink sink,
+ IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
+ IDictionary<IUnit, PdbReader> pdbReaders) {
+ return new WholeProgramMetadataSemantics(this, sink, pdbReaders);
}
public class WholeProgramMetadataSemantics : MetadataTraverser {
@@ -34,27 +35,23 @@ namespace BytecodeTranslator {
readonly WholeProgram parent;
readonly Sink sink;
- /// <summary>
- /// TODO: Need to have this populated before any of the assemblies in the CUA are traversed.
- /// </summary>
- readonly Dictionary<IAssembly, bool> codeUnderAnalysis = new Dictionary<IAssembly, bool>();
+ readonly Dictionary<IUnit, bool> codeUnderAnalysis = new Dictionary<IUnit, bool>();
- public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, PdbReader/*?*/ pdbReader)
- : base(sink, pdbReader) {
+ public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
+ : base(sink, pdbReaders) {
this.parent = parent;
this.sink = sink;
}
- public override void Visit(IAssembly assembly) {
-
- #region When doing whole-program analysis, traverse the assembly gathering type information
- this.codeUnderAnalysis.Add(assembly, true);
+ public override void TranslateAssemblies(IEnumerable<IUnit> assemblies) {
+ #region traverse all of the units gathering type information
var typeRecorder = new RecordSubtypes(this.parent.subTypes);
- typeRecorder.Visit(assembly);
+ foreach (var a in assemblies) {
+ this.codeUnderAnalysis.Add(a, true);
+ typeRecorder.Visit(a);
+ }
#endregion
-
- base.Visit(assembly);
-
+ base.TranslateAssemblies(assemblies);
}
class RecordSubtypes : BaseMetadataTraverser {
@@ -120,54 +117,18 @@ namespace BytecodeTranslator {
return;
}
- #region Translate In Parameters
-
- var inexpr = new List<Bpl.Expr>();
- #region Create the 'this' argument for the function call
- this.Visit(methodCall.ThisArgument);
- inexpr.Add(this.TranslatedExpressions.Pop());
- #endregion
-
- Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();
- IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
- penum.MoveNext();
- foreach (IExpression exp in methodCall.Arguments) {
- if (penum.Current == null) {
- throw new TranslationException("More Arguments than Parameters in functioncall");
- }
- this.Visit(exp);
- Bpl.Expr e = this.TranslatedExpressions.Pop();
-
- p2eMap.Add(penum.Current, e);
- if (!penum.Current.IsOut) {
- inexpr.Add(e);
- }
-
- penum.MoveNext();
- }
- #endregion
-
Bpl.IToken token = methodCall.Token();
- #region Translate Out vars
- var outvars = new List<Bpl.IdentifierExpr>();
+ List<Bpl.Expr> inexpr;
+ List<Bpl.IdentifierExpr> outvars;
+ Bpl.IdentifierExpr thisExpr;
+ List<Bpl.Variable> locals;
+ List<IFieldDefinition> args;
+ Bpl.Expr arrayExpr;
+ Bpl.Expr indexExpr;
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
+ var proc = TranslateArgumentsAndReturnProcedure(token, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);
- foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {
- if (kvp.Key.IsByReference) {
- Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;
- if (iexp == null) {
- throw new TranslationException("Trying to pass complex expression as out in functioncall");
- }
- outvars.Add(iexp);
- }
- }
- #endregion
-
- if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
- outvars.Add(new Bpl.IdentifierExpr(token, v));
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(token, v));
- }
Bpl.QKeyValue attrib = null;
foreach (var a in resolvedMethod.Attributes) {
@@ -179,7 +140,6 @@ namespace BytecodeTranslator {
var elseBranch = new Bpl.StmtListBuilder();
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
var methodname = proc.Name;
Bpl.CallCmd call;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 05:41:01 +0000