diff options
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 15 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 3 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 11 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 6 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 6 |
5 files changed, 31 insertions, 10 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 46167ec2..2c25728b 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -744,10 +744,21 @@ namespace BytecodeTranslator this.Traverse(expressionToTraverse);
Bpl.Expr e = this.TranslatedExpressions.Pop();
- if (penum.Current.Type is IGenericParameterReference && this.sink.CciTypeToBoogie(penum.Current.Type) == this.sink.Heap.BoxType)
+ var currentType = penum.Current.Type;
+ if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.BoxType)
inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(expressionToTraverse.Type), e));
- else
+ else {
+ // Need to check if a struct value is being passed as an argument. If so, don't pass the struct,
+ // but pass a copy of it.
+ if (TranslationHelper.IsStruct(currentType)) {
+ var proc = this.sink.FindOrCreateProcedureForStructCopy(currentType);
+ var bplLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(e.Type));
+ var cmd = new Bpl.CallCmd(token, proc.Name, new List<Bpl.Expr> { e, bplLocal, }, new List<Bpl.IdentifierExpr>());
+ this.StmtTraverser.StmtBuilder.Add(cmd);
+ e = bplLocal;
+ }
inexpr.Add(e);
+ }
if (penum.Current.IsByReference) {
Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;
if (unboxed == null) {
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index f6dc7ecf..e6a6fb45 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -224,6 +224,7 @@ namespace BytecodeTranslator { Type = f.Type,
},
};
+ stmts.Add(s);
}
stmtTranslator.Traverse(stmts);
@@ -276,7 +277,7 @@ namespace BytecodeTranslator { var lit = Bpl.Expr.Literal(1);
lit.Type = Bpl.Type.Int;
var args = new List<object> { lit };
- var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", args, null); // TODO: Need to have it be {:inine 1} (and not just {:inline})?
+ var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", args, null);
Bpl.Implementation impl =
new Bpl.Implementation(Bpl.Token.NoToken,
proc.Name,
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index afecc3d5..c3539063 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -66,10 +66,13 @@ namespace BytecodeTranslator { public Bpl.Formal ThisVariable {
get {
- ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);
- return info.ThisVariable;
+ return this.thisVariable;
+ //ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);
+ //return info.ThisVariable;
}
}
+ private Bpl.Formal thisVariable;
+
public Bpl.Formal ReturnVariable {
get {
ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);
@@ -725,7 +728,7 @@ namespace BytecodeTranslator { if (!this.declaredStructDefaultCtors.TryGetValue(procName, out procAndFormalMap)) {
var tok = structType.Token();
var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);
- var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);
+ var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "$this", selfType), true);
var invars = new Bpl.Formal[] { selfIn };
var proc = new Bpl.Procedure(Bpl.Token.NoToken, procName,
new Bpl.TypeVariableSeq(),
@@ -1198,6 +1201,8 @@ namespace BytecodeTranslator { this.localVarMap = new Dictionary<string, Bpl.LocalVariable>();
this.localCounter = 0;
this.methodBeingTranslated = null;
+ var selfType = CciTypeToBoogie(containingType);
+ this.thisVariable = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$this", selfType), true);
}
public Dictionary<IName, int> cciLabels;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index e0498d9d..187ea10b 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -654,7 +654,7 @@ procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: -procedure RegressionTestInput.S.#default_ctor(this: Ref);
+procedure RegressionTestInput.S.#default_ctor($this: Ref);
@@ -1309,8 +1309,10 @@ implementation T$RegressionTestInput.NestedGeneric.#cctor() -implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)
+implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref)
{
+ $Heap := Write($Heap, $this, F$RegressionTestInput.S.x, Int2Box(0));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.S.b, Bool2Box(false));
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 342fd0d6..379413cc 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -640,7 +640,7 @@ procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: -procedure RegressionTestInput.S.#default_ctor(this: Ref);
+procedure RegressionTestInput.S.#default_ctor($this: Ref);
@@ -1295,8 +1295,10 @@ implementation T$RegressionTestInput.NestedGeneric.#cctor() -implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)
+implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref)
{
+ F$RegressionTestInput.S.x[$this] := 0;
+ F$RegressionTestInput.S.b[$this] := false;
}
|