diff options
| -rw-r--r-- | .hgignore | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 133 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 53 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 67 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 4 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 22 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 18 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 4 |
8 files changed, 208 insertions, 95 deletions
@@ -4,7 +4,7 @@ syntax: regexp ^(Source|BCT|Jennisys)/.*\.(user|suo|cache)$
^Source/(Core|Dafny)/(Parser|Scanner).cs.old$
^Binaries/.*\.(dll|pdb|exe|manifest|config)$
-^.*(bin|obj)/([^/]*/)?(Debug|Release)/.*$
+^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked)/.*$
^Binaries/BytecodeTranslator$
^BCT/Binaries/.*$
Test/([^/]*)/Output
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index b189b4eb..53e4ccce 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -86,9 +86,22 @@ namespace BytecodeTranslator return;
}
IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;
- if (field != null)
- {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field.ResolvedField)));
+ if (field != null) {
+ var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field.ResolvedField));
+ var instance = addressableExpression.Instance;
+ if (instance == null) {
+ TranslatedExpressions.Push(f);
+ }
+ else {
+ this.Visit(instance);
+ if (this.args != null) {
+ this.args.Add(field.ResolvedField);
+ }
+ else {
+ Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
+ TranslatedExpressions.Push(this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct));
+ }
+ }
return;
}
IArrayIndexer/*?*/ arrayIndexer = addressableExpression.Definition as IArrayIndexer;
@@ -240,16 +253,12 @@ namespace BytecodeTranslator IFieldReference field = targetExpression.Definition as IFieldReference;
if (field != null)
{
- //ProcessFieldVariable(field, targetExpression.Instance, false);
- //return;
- var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field.ResolvedField));
- TranslatedExpressions.Push(f);
var instance = targetExpression.Instance;
if (instance != null) {
+ this.args = new List<IFieldDefinition>();
this.Visit(instance);
}
return;
-
}
#endregion
@@ -296,8 +305,13 @@ namespace BytecodeTranslator }
else {
this.Visit(instance);
- Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct));
+ if (this.args != null) {
+ this.args.Add(field.ResolvedField);
+ }
+ else {
+ Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
+ TranslatedExpressions.Push(this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct));
+ }
}
return;
}
@@ -422,11 +436,29 @@ namespace BytecodeTranslator var inexpr = new List<Bpl.Expr>();
#region Create the 'this' argument for the function call
- Bpl.Expr thisExpr = null;
+ Bpl.IdentifierExpr thisExpr = null;
+ List<Bpl.Variable> locals = null;
+ List<IFieldDefinition> args = null;
if (!methodCall.IsStaticCall)
{
+ Debug.Assert(this.args == null);
+ this.args = new List<IFieldDefinition>();
this.Visit(methodCall.ThisArgument);
- thisExpr = this.TranslatedExpressions.Pop();
+ args = this.args;
+ this.args = null;
+
+ thisExpr = this.TranslatedExpressions.Pop() 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(this.sink.CciTypeToBoogie(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)));
+ x = y;
+ locals.Add(y);
+ }
+ thisExpr = Bpl.Expr.Ident(x);
inexpr.Add(thisExpr);
}
#endregion
@@ -465,11 +497,9 @@ namespace BytecodeTranslator // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!
#region Translate Out vars
- Bpl.IdentifierExpr outMap = null;
var outvars = new List<Bpl.IdentifierExpr>();
if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
- outMap = new Bpl.IdentifierExpr(methodCall.Token(), sink.CreateFreshLocal(new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(sink.Heap.FieldType), sink.Heap.BoxType)));
- outvars.Add(outMap);
+ outvars.Add(thisExpr);
}
foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)
{
@@ -560,16 +590,23 @@ namespace BytecodeTranslator call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
this.StmtTraverser.StmtBuilder.Add(call);
}
- if (outMap != null) {
- Debug.Assert(thisExpr != null);
- Bpl.AssignLhs lhs = new Bpl.SimpleAssignLhs(Bpl.Token.NoToken, (Bpl.IdentifierExpr) thisExpr);
- List<Bpl.AssignLhs> lhss = new List<Bpl.AssignLhs>();
- lhss.Add(lhs);
- List<Bpl.Expr> rhss = new List<Bpl.Expr>();
- rhss.Add(outMap);
- Bpl.AssignCmd acmd = new Bpl.AssignCmd(methodCall.Token(), lhss, rhss);
- this.StmtTraverser.StmtBuilder.Add(acmd);
+
+ 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];
+ if (currField.Type.ResolvedType.IsClass) break;
+ 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));
+ x = y;
+ count--;
+ }
}
+
}
}
@@ -577,6 +614,7 @@ namespace BytecodeTranslator #endregion
#region Translate Assignments
+ private List<IFieldDefinition> args = null;
/// <summary>
///
@@ -621,9 +659,14 @@ namespace BytecodeTranslator #endregion
var target = assignment.Target;
+ var fieldReference = target.Definition as IFieldReference;
this.assignmentSourceExpr = sourceexp;
+ List<IFieldDefinition> args = null;
+ Debug.Assert(this.args == null);
this.Visit(target);
+ args = this.args;
+ this.args = null;
this.assignmentSourceExpr = null;
if (target.Definition is IArrayIndexer) {
@@ -634,22 +677,39 @@ namespace BytecodeTranslator return;
}
- var fieldReference = target.Definition as IFieldReference;
if (fieldReference != null) {
- Bpl.Expr o = null;
- if (target.Instance != null)
- o = TranslatedExpressions.Pop();
- Bpl.IdentifierExpr f = this.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
- Bpl.Cmd c;
+ Bpl.IdentifierExpr f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(fieldReference.ResolvedField));
if (target.Instance == null) {
- c = Bpl.Cmd.SimpleAssign(assignment.Token(), f, sourceexp);
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(), f, sourceexp));
}
else {
- c = this.sink.Heap.WriteHeap(assignment.Token(), o, f, sourceexp, fieldReference.ContainingType.ResolvedType.IsStruct);
+ Debug.Assert(args != null);
+ List<Bpl.Variable> locals = new List<Bpl.Variable>();
+ Bpl.IdentifierExpr instanceExpr = TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
+ Bpl.Variable x = instanceExpr.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(this.sink.CciTypeToBoogie(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)));
+ x = y;
+ locals.Add(y);
+ }
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(assignment.Token(), Bpl.Expr.Ident(x), f, sourceexp, fieldReference.ResolvedField.ContainingType.ResolvedType.IsStruct));
+
+ int count = args.Count;
+ x = locals[count];
+ count--;
+ while (0 <= count) {
+ IFieldDefinition currField = args[count];
+ if (currField.Type.ResolvedType.IsClass) break;
+ Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));
+ Bpl.Variable y = locals[count];
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(assignment.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct));
+ x = y;
+ count--;
+ }
}
- // In the struct case, I am making the assumption that we only see a single field dereference on the left side of the assignment
- //var c = (fieldReference.ContainingType.ResolvedType.IsStruct) ? this.sink.WriteStruct((Bpl.IdentifierExpr)o, f, sourceexp) : this.sink.Heap.WriteHeap(assignment.Token(), o, f, sourceexp);
- StmtTraverser.StmtBuilder.Add(c);
return;
}
@@ -963,8 +1023,7 @@ namespace BytecodeTranslator return;
}
- public override void Visit(IConversion conversion)
- {
+ public override void Visit(IConversion conversion) {
var tok = conversion.ValueToConvert.Token();
Visit(conversion.ValueToConvert);
var boogieTypeOfValue = this.sink.CciTypeToBoogie(conversion.ValueToConvert.Type);
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index ba06b454..81f2b9e9 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -34,6 +34,8 @@ namespace BytecodeTranslator { /// </summary>
private readonly string InitialPreludeText =
@"const null: int;
+type ref = int;
+type struct = [Field]box;
type HeapType = [int,int]int;
var $Heap: HeapType where IsGoodHeap($Heap);
function IsGoodHeap(HeapType): bool;
@@ -49,7 +51,6 @@ procedure {:inline 1} Alloc() returns (x: int) $Alloc[x] := true;
}
-type ref = int;
";
private Sink sink;
@@ -147,19 +148,7 @@ type ref = int; [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
private Bpl.Variable HeapVariable = null;
-
- [RepresentationFor("Box2Int", "function Box2Int(box): int;")]
- private Bpl.Function Box2Int = null;
-
- [RepresentationFor("Box2Bool", "function Box2Bool(box): bool;")]
- private Bpl.Function Box2Bool = null;
-
- [RepresentationFor("Int2Box", "function Int2Box(int): box;")]
- private Bpl.Function Int2Box = null;
-
- [RepresentationFor("Bool2Box", "function Bool2Box(bool): box;")]
- private Bpl.Function Bool2Box = null;
-
+
[RepresentationFor("Read", "function {:inline true} Read(H:HeapType, o:ref, f:Field): box { H[o, f] }")]
private Bpl.Function Read = null;
@@ -172,6 +161,7 @@ type ref = int; private readonly string InitialPreludeText =
@"const null: ref;
type ref = int;
+type struct = [Field]box;
type HeapType = [ref,Field]box;
function IsGoodHeap(HeapType): bool;
var $ArrayContents: [int][int]int;
@@ -185,6 +175,7 @@ procedure {:inline 1} Alloc() returns (x: ref) assume $Alloc[x] == false;
$Alloc[x] := true;
}
+
";
private Sink sink;
@@ -269,23 +260,10 @@ procedure {:inline 1} Alloc() returns (x: ref) );
// wrap it in the right conversion function
- Bpl.Function conversion;
var originalType = this.underlyingTypes[f.Decl];
var boogieType = sink.CciTypeToBoogie(originalType);
- if (boogieType == Bpl.Type.Bool)
- conversion = this.Box2Bool;
- else if (boogieType == Bpl.Type.Int)
- conversion = this.Box2Int;
- else
- throw new InvalidOperationException("Unknown Boogie type");
- var callExpr = new Bpl.NAryExpr(
- f.tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(callRead)
- );
- callExpr.Type = boogieType;
+ var callExpr = Unbox(f.tok, boogieType, callRead);
return callExpr;
-
}
/// <summary>
@@ -295,25 +273,12 @@ procedure {:inline 1} Alloc() returns (x: ref) public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value, bool isStruct) {
Debug.Assert(o != null);
- // wrap it in the right conversion function
- Bpl.Function conversion;
+ Bpl.IdentifierExpr h;
+ Bpl.NAryExpr callWrite;
var originalType = this.underlyingTypes[f.Decl];
var boogieType = sink.CciTypeToBoogie(originalType);
- if (boogieType == Bpl.Type.Bool)
- conversion = this.Bool2Box;
- else if (boogieType == Bpl.Type.Int)
- conversion = this.Int2Box;
- else
- throw new InvalidOperationException("Unknown Boogie type");
-
- var callConversion = new Bpl.NAryExpr(
- f.tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(value)
- );
+ var callConversion = Box(f.tok, boogieType, value);
- Bpl.IdentifierExpr h;
- Bpl.NAryExpr callWrite;
if (isStruct) {
h = (Bpl.IdentifierExpr)o;
callWrite = Bpl.Expr.Store(h, f, callConversion);
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 23a7de80..dfdcc609 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -77,6 +77,73 @@ namespace BytecodeTranslator { [RepresentationFor("Type", "type Type;")]
protected Bpl.TypeCtorDecl TypeTypeDecl = null;
protected Bpl.CtorType TypeType;
+
+ private Bpl.Type structType = null;
+ public Bpl.Type StructType {
+ get {
+ if (structType == null) {
+ structType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(FieldType), BoxType);
+ }
+ return structType;
+ }
+ }
+
+ [RepresentationFor("Box2Int", "function Box2Int(box): int;")]
+ public Bpl.Function Box2Int = null;
+
+ [RepresentationFor("Box2Bool", "function Box2Bool(box): bool;")]
+ public Bpl.Function Box2Bool = null;
+
+ [RepresentationFor("Box2Struct", "function Box2Struct(box): struct;")]
+ public Bpl.Function Box2Struct = null;
+
+ [RepresentationFor("Int2Box", "function Int2Box(int): box;")]
+ public Bpl.Function Int2Box = null;
+
+ [RepresentationFor("Bool2Box", "function Bool2Box(bool): box;")]
+ public Bpl.Function Bool2Box = null;
+
+ [RepresentationFor("Struct2Box", "function Struct2Box(struct): box;")]
+ public Bpl.Function Struct2Box = null;
+
+ public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
+ Bpl.Function conversion;
+ if (boogieType == Bpl.Type.Bool)
+ conversion = this.Bool2Box;
+ else if (boogieType == Bpl.Type.Int)
+ conversion = this.Int2Box;
+ else if (boogieType == StructType)
+ conversion = this.Struct2Box;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+
+ var callConversion = new Bpl.NAryExpr(
+ tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(expr)
+ );
+ return callConversion;
+ }
+
+ public Bpl.Expr Unbox(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
+ Bpl.Function conversion = null;
+ if (boogieType == Bpl.Type.Bool)
+ conversion = this.Box2Bool;
+ else if (boogieType == Bpl.Type.Int)
+ conversion = this.Box2Int;
+ else if (boogieType == StructType)
+ conversion = this.Box2Struct;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+
+ var callExpr = new Bpl.NAryExpr(
+ tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(expr)
+ );
+ callExpr.Type = boogieType;
+ return callExpr;
+ }
/// <summary>
/// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 488edb9f..6e3909ab 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -103,7 +103,7 @@ namespace BytecodeTranslator { else if (TypeHelper.IsPrimitiveInteger(type))
return Bpl.Type.Int;
else if (type.ResolvedType.IsStruct)
- return new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.heap.FieldType), this.heap.BoxType);
+ return heap.StructType;
return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type
}
@@ -287,7 +287,7 @@ namespace BytecodeTranslator { if (!method.IsStatic) {
Bpl.Type selfType;
if (method.ContainingType.ResolvedType.IsStruct) {
- selfType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);
+ selfType = Heap.StructType;
in_count++;
self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "thisIn", selfType), true);
out_count++;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 87514ae9..e0102a57 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -5,6 +5,8 @@ const null: ref; type ref = int;
+type struct = [Field]box;
+
type HeapType = [ref,Field]box;
function IsGoodHeap(HeapType) : bool;
@@ -188,14 +190,6 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) var $Heap: HeapType where IsGoodHeap($Heap);
-function Box2Int(box) : int;
-
-function Box2Bool(box) : bool;
-
-function Int2Box(int) : box;
-
-function Bool2Box(bool) : box;
-
function {:inline true} Read(H: HeapType, o: ref, f: Field) : box
{
H[o, f]
@@ -212,6 +206,18 @@ type box; type Type;
+function Box2Int(box) : int;
+
+function Box2Bool(box) : bool;
+
+function Box2Struct(box) : struct;
+
+function Int2Box(int) : box;
+
+function Bool2Box(bool) : box;
+
+function Struct2Box(struct) : box;
+
function $DynamicType(ref) : Type;
function $TypeOf(Type) : ref;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index e6d6e7fd..872da3ae 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -3,6 +3,10 @@ const null: int;
+type ref = int;
+
+type struct = [Field]box;
+
type HeapType = [int,int]int;
var $Heap: HeapType where IsGoodHeap($Heap);
@@ -29,8 +33,6 @@ implementation Alloc() returns (x: int) -type ref = int;
-
procedure DelegateAdd(a: int, b: int) returns (c: int);
@@ -194,6 +196,18 @@ type box; type Type;
+function Box2Int(box) : int;
+
+function Box2Bool(box) : bool;
+
+function Box2Struct(box) : struct;
+
+function Int2Box(int) : box;
+
+function Bool2Box(bool) : box;
+
+function Struct2Box(struct) : box;
+
function $DynamicType(ref) : Type;
function $TypeOf(Type) : ref;
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index c6184e63..87b48740 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -247,7 +247,9 @@ namespace Microsoft.Boogie { private void ComputeAllLabels(StmtList stmts) {
if (stmts == null) return;
foreach (BigBlock bb in stmts.BigBlocks) {
- allLabels.Add(bb.LabelName);
+ if (bb.LabelName != null) {
+ allLabels.Add(bb.LabelName);
+ }
ComputeAllLabels(bb.ec);
}
}
|