summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs93
-rw-r--r--BCT/BytecodeTranslator/Heap.cs53
-rw-r--r--BCT/BytecodeTranslator/HeapFactory.cs67
-rw-r--r--BCT/BytecodeTranslator/Sink.cs4
4 files changed, 142 insertions, 75 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index a19bbedc..851dc20b 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 (args != null) {
+ 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 (args != null) {
+ args.Add(field.ResolvedField);
+ }
+ else {
+ Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
+ TranslatedExpressions.Push(this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct));
+ }
}
return;
}
@@ -468,7 +482,7 @@ namespace BytecodeTranslator
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)));
+ outMap = new Bpl.IdentifierExpr(methodCall.Token(), sink.CreateFreshLocal(sink.Heap.StructType));
outvars.Add(outMap);
}
foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)
@@ -562,13 +576,7 @@ namespace BytecodeTranslator
}
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);
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd((Bpl.IdentifierExpr)thisExpr, outMap));
}
}
@@ -577,6 +585,7 @@ namespace BytecodeTranslator
#endregion
#region Translate Assignments
+ private List<IFieldDefinition> args = null;
/// <summary>
///
@@ -592,6 +601,7 @@ namespace BytecodeTranslator
#endregion
var target = assignment.Target;
+ var fieldReference = target.Definition as IFieldReference;
this.assignmentSourceExpr = sourceexp;
this.Visit(target);
@@ -605,22 +615,47 @@ 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 = this.sink.CreateFreshLocal(instanceExpr.Type);
+ locals.Add(x);
+ StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(x), instanceExpr));
+ 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));
+ locals.Add(y);
+ 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;
+ }
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(assignment.Token(), Bpl.Expr.Ident(x), f, sourceexp, fieldReference.ResolvedField.ContainingType.ResolvedType.IsStruct));
+
+ IFieldDefinition currField = fieldReference.ResolvedField;
+ int count = args.Count;
+ x = locals[count];
+ count--;
+ while (true) {
+ if (count < 0) {
+ if (instanceExpr.Type == this.sink.Heap.StructType) {
+ StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(instanceExpr, Bpl.Expr.Ident(x)));
+ }
+ break;
+ }
+ if (currField.ContainingType.ResolvedType.IsClass) break;
+ 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(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;
}
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 c6fadd5f..9c20f96a 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++;
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-20 21:43:24 +0000