diff options
author | 2011-05-11 17:32:04 -0700 | |
---|---|---|
committer | 2011-05-11 17:32:04 -0700 | |
commit | a1affe2114ae22816cf72d14fb4ae357a64fe7f2 (patch) | |
tree | bfb5e2a9128646ce4424ab7506172f0fee8deca0 | |
parent | d56c8e6ea80eb5a501bda731fcc0047749df51e7 (diff) | |
parent | b07ef370367ac1e73e35ebc4d89bdc3bb1e9a5fe (diff) |
Merge
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 264 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 7 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 2 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 24 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 8 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/WholeProgram.cs | 4 |
6 files changed, 144 insertions, 165 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 7dbf8d0f..29c0033f 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -424,18 +424,18 @@ namespace BytecodeTranslator /// </summary>
/// <param name="methodCall"></param>
/// <remarks>Stub, This one really needs comments!</remarks>
- public override void Visit(IMethodCall methodCall)
- {
- var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;
+ public override void Visit(IMethodCall methodCall) {
+ var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;
+
if (resolvedMethod == Dummy.Method) {
throw new TranslationException(
ExceptionType.UnresolvedMethod,
MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));
}
-
- #region Translate In Parameters
+ #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;
@@ -443,8 +443,7 @@ namespace BytecodeTranslator List<IFieldDefinition> args = null;
Bpl.Expr arrayExpr = null;
Bpl.Expr indexExpr = null;
- if (!methodCall.IsStaticCall)
- {
+ if (!methodCall.IsStaticCall) {
this.collectStructFields = true;
this.structFields = new List<IFieldDefinition>();
this.arrayExpr = null;
@@ -456,175 +455,145 @@ namespace BytecodeTranslator indexExpr = this.indexExpr;
var e = this.TranslatedExpressions.Pop();
- if (false && methodCall.MethodToCall.ContainingType.IsValueType)
- {
- // then the "this arg" was actually an AddressOf the struct
- // but we are going to ignore that and just get the identifier
- // that it was the address of
- var nAry = e as Bpl.NAryExpr;
- var nAryArgs = nAry.Args;
- e = nAryArgs[0] as Bpl.IdentifierExpr;
- }
inexpr.Add(e);
- if (e is Bpl.NAryExpr)
- {
+ 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++)
- {
+ 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);
}
- //thisExpr = Bpl.Expr.Ident(x);
- //inexpr.Add(thisExpr);
+ }
+ if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
+ outvars.Add(thisExpr);
}
#endregion
- Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();
+ 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 functioncall");
+ 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();
-
- p2eMap.Add(penum.Current, e);
- if (!penum.Current.IsOut)
- {
+ 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
Bpl.IToken cloc = methodCall.Token();
-
- // meeting a constructor is always something special
- if (false && resolvedMethod.IsConstructor)
- {
- // Todo: do something with the constructor call
- }
- else
- {
- // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!
-
- #region Translate Out vars
- var outvars = new List<Bpl.IdentifierExpr>();
- if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
- outvars.Add(thisExpr);
+ 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);
}
- foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)
- {
- if (kvp.Key.IsOut || 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);
- }
+ else {
+ outvars.Add(unboxed);
}
- #endregion
+ TranslatedExpressions.Push(unboxed);
+ }
+ var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
+ string methodname = proc.Name;
- if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void)
- {
- Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
- outvars.Add(new Bpl.IdentifierExpr(cloc, v));
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));
+ 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);
}
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
- string methodname = proc.Name;
+ }
- 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);
- }
+ Bpl.CallCmd call;
+ bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
+ bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
+ if (isEventAdd || isEventRemove) {
+ var mName = resolvedMethod.Name.Value;
+ var eventName = mName.Substring(mName.IndexOf('_') + 1);
+ var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));
+ Contract.Assert(eventDef != Dummy.Event);
+ Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);
+ Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);
+
+ if (methodCall.IsStaticCall) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
+ inexpr.Insert(0, Bpl.Expr.Ident(local));
+ }
+ else {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));
+ inexpr[0] = Bpl.Expr.Ident(local);
}
- Bpl.CallCmd call;
- bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
- bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
- if (isEventAdd || isEventRemove)
- {
- var mName = resolvedMethod.Name.Value;
- var eventName = mName.Substring(mName.IndexOf('_')+1);
- var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));
- Contract.Assert(eventDef != Dummy.Event);
- Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);
- Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);
-
- if (methodCall.IsStaticCall)
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
- inexpr.Insert(0, Bpl.Expr.Ident(local));
- }
- else
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));
- inexpr[0] = Bpl.Expr.Ident(local);
- }
-
- System.Diagnostics.Debug.Assert(outvars.Count == 0);
- outvars.Add(Bpl.Expr.Ident(local));
- string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
- call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
- if (methodCall.IsStaticCall)
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
- }
- 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));
- }
+ System.Diagnostics.Debug.Assert(outvars.Count == 0);
+ outvars.Add(Bpl.Expr.Ident(local));
+ string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
+ call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ if (methodCall.IsStaticCall) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
}
- 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 {
+ 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);
+ }
- if (!methodCall.IsStaticCall) {
- Debug.Assert(args != null && locals != null);
- int count = args.Count;
- Bpl.Variable x = locals[count];
+ foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));
+ }
+
+ if (!methodCall.IsStaticCall) {
+ Debug.Assert(args != null && locals != null);
+ int count = args.Count;
+ Bpl.Variable x = locals[count];
+ count--;
+ while (0 <= count) {
+ IFieldDefinition currField = args[count];
+ Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));
+ Bpl.Variable y = locals[count];
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));
+ x = y;
count--;
- while (0 <= count)
- {
- IFieldDefinition currField = args[count];
- Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));
- Bpl.Variable y = locals[count];
- StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));
- x = y;
- count--;
- }
- if (indexExpr != null) {
- Debug.Assert(arrayExpr != null);
- StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));
- }
}
-
+ if (indexExpr != null) {
+ Debug.Assert(arrayExpr != null);
+ StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));
+ }
}
-
}
#endregion
@@ -756,7 +725,7 @@ namespace BytecodeTranslator /// </summary>
public override void Visit(ICreateObjectInstance createObjectInstance)
{
- TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance.Type, createObjectInstance);
+ TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance);
}
public override void Visit(ICreateArray createArrayInstance)
@@ -788,35 +757,32 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
- private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST)
+ private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)
{
+ var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;
Bpl.IToken token = creationAST.Token();
-
+
var a = this.sink.CreateFreshLocal(creationAST.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(ctor.ResolvedMethod);
+ var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
Bpl.ExprSeq inexpr = new Bpl.ExprSeq();
inexpr.Add(Bpl.Expr.Ident(a));
- IEnumerator<IParameterDefinition> penum = ctor.ResolvedMethod.Parameters.GetEnumerator();
+ IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
penum.MoveNext();
- foreach (IExpression exp in arguments)
- {
- if (penum.Current == null)
- {
+ 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.IsOut)
- {
+ 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();
}
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 812fddb1..6d03ef9f 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -148,6 +148,9 @@ namespace BytecodeTranslator { [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]
public Bpl.Function Real2Box = null;
+ [RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]
+ public Bpl.Function Box2Box = null;
+
public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
Bpl.Function conversion;
if (boogieType == Bpl.Type.Bool)
@@ -160,6 +163,8 @@ namespace BytecodeTranslator { conversion = this.Ref2Box;
else if (boogieType == RealType)
conversion = this.Real2Box;
+ else if (boogieType == BoxType)
+ conversion = this.Box2Box;
else
throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
@@ -183,6 +188,8 @@ namespace BytecodeTranslator { conversion = this.Box2Ref;
else if (boogieType == RealType)
conversion = this.Box2Real;
+ else if (boogieType == BoxType)
+ conversion = this.Box2Box;
else
throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 1fa59767..58bec27f 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -262,7 +262,7 @@ namespace BytecodeTranslator { #region Create Local Vars For Implementation
List<Bpl.Variable> vars = new List<Bpl.Variable>();
foreach (MethodParameter mparam in formalMap.Values) {
- if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))
+ if (!mparam.underlyingParameter.IsByReference)
vars.Add(mparam.outParameterCopy);
}
foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 629e7e54..b8d8334d 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -99,6 +99,9 @@ namespace BytecodeTranslator { return Bpl.Expr.Ident(this.Heap.DefaultStruct);
} else if (bplType == this.Heap.RefType) {
return Bpl.Expr.Ident(this.Heap.NullRef);
+ }
+ else if (bplType == this.Heap.BoxType) {
+ return Bpl.Expr.Ident(this.Heap.DefaultBox);
} else {
throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));
}
@@ -113,9 +116,11 @@ namespace BytecodeTranslator { return heap.RealType;
else if (type.ResolvedType.IsStruct)
return heap.StructType;
- else if (type.IsEnum) {
+ else if (type.IsEnum)
return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer
- } else
+ else if (type is IGenericTypeParameter)
+ return heap.BoxType;
+ else
return heap.RefType;
}
@@ -134,6 +139,14 @@ namespace BytecodeTranslator { return v;
}
+ public Bpl.Variable CreateFreshLocal(Bpl.Type t) {
+ Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
+ 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);
+ return v;
+ }
+
/// <summary>
/// State that gets re-initialized per method
/// </summary>
@@ -335,10 +348,9 @@ namespace BytecodeTranslator { MethodParameter mp;
var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
foreach (IParameterDefinition formal in method.Parameters) {
-
mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));
if (mp.inParameterCopy != null) in_count++;
- if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))
+ if (mp.outParameterCopy != null && formal.IsByReference)
out_count++;
formalMap.Add(formal, mp);
}
@@ -397,7 +409,7 @@ namespace BytecodeTranslator { invars[i++] = mparam.inParameterCopy;
}
if (mparam.outParameterCopy != null) {
- if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)
+ if (mparam.underlyingParameter.IsByReference)
outvars[j++] = mparam.outParameterCopy;
}
}
@@ -563,7 +575,7 @@ namespace BytecodeTranslator { this.FindOrCreateProcedure(method);
return this.declaredMethods[method.InternedKey];
}
- private static IMethodReference Unspecialize(IMethodReference method) {
+ public static IMethodReference Unspecialize(IMethodReference method) {
IMethodReference result = method;
var gmir = result as IGenericMethodInstanceReference;
if (gmir != null) {
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 42b1a4d0..54ed1700 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -37,22 +37,18 @@ namespace BytecodeTranslator { public IParameterDefinition underlyingParameter;
public MethodParameter(IParameterDefinition parameterDefinition, Bpl.Type ptype) {
-
this.underlyingParameter = parameterDefinition;
var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = parameterDefinition.Name.Value;
- if (!parameterDefinition.IsOut) {
- this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
- }
- if (parameterDefinition.IsByReference || parameterDefinition.IsOut) {
+ this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
+ if (parameterDefinition.IsByReference) {
this.outParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$out", ptype), false);
} else {
this.outParameterCopy = new Bpl.LocalVariable(parameterToken, new Bpl.TypedIdent(typeToken, parameterName, ptype));
}
-
}
public override string ToString() {
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index f4cc59af..92154020 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -149,13 +149,11 @@ namespace BytecodeTranslator { Bpl.IToken token = methodCall.Token();
- // TODO: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!
-
#region Translate Out vars
var outvars = new List<Bpl.IdentifierExpr>();
foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {
- if (kvp.Key.IsOut || kvp.Key.IsByReference) {
+ 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");
|