diff options
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 7 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 27 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 2 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 2 |
4 files changed, 35 insertions, 3 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 316e3faa..b4a258ad 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -640,7 +640,12 @@ namespace BytecodeTranslator this.Visit(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));
+ if (structCopy) {
+ cmd = new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { e, bplParam, }, new List<Bpl.IdentifierExpr>());
+ } else {
+ cmd = Bpl.Cmd.SimpleAssign(tok, bplParam, e);
+ }
+ StmtTraverser.StmtBuilder.Add(cmd);
return;
}
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 22cc8cb8..7e6ddcff 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -473,6 +473,24 @@ namespace BytecodeTranslator { #endregion
+ #region Add disjointness contracts for any struct values passed by value
+ var paramList = new List<IParameterDefinition>(method.Parameters);
+ for (int p1index = 0; p1index < method.ParameterCount; p1index++) {
+ var p1 = paramList[p1index];
+ if (p1.IsByReference) continue;
+ if (!(p1.Type.IsValueType && p1.Type.TypeCode == PrimitiveTypeCode.NotPrimitive)) continue;
+ for (int p2index = p1index + 1; p2index < method.ParameterCount; p2index++) {
+ var p2 = paramList[p2index];
+ if (p2.IsByReference) continue;
+ if (!(p2.Type.IsValueType && p2.Type.TypeCode == PrimitiveTypeCode.NotPrimitive)) continue;
+ if (!TypeHelper.TypesAreEquivalent(p1.Type, p2.Type)) continue;
+ var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq,
+ Bpl.Expr.Ident(formalMap[p1].inParameterCopy), Bpl.Expr.Ident(formalMap[p2].inParameterCopy)));
+ boogiePrecondition.Add(req);
+ }
+ }
+ #endregion
+
var tok = method.Token();
Bpl.DeclWithFormals decl;
if (IsPure(method)) {
@@ -573,13 +591,18 @@ namespace BytecodeTranslator { var otherIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "other", selfType), false);
var invars = new Bpl.Formal[] { selfIn, otherIn, };
var outvars = new Bpl.Formal[0];
+ var selfInExpr = Bpl.Expr.Ident(selfIn);
+ var otherInExpr = Bpl.Expr.Ident(otherIn);
+ var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, selfInExpr, otherInExpr));
+ var ens = new Bpl.Ensures(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, selfInExpr, otherInExpr));
+
var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#copy_ctor",
new Bpl.TypeVariableSeq(),
new Bpl.VariableSeq(invars),
new Bpl.VariableSeq(outvars),
- new Bpl.RequiresSeq(),
+ new Bpl.RequiresSeq(req),
new Bpl.IdentifierExprSeq(), // modifies
- new Bpl.EnsuresSeq()
+ new Bpl.EnsuresSeq(ens)
);
this.TranslatedProgram.TopLevelDeclarations.Add(proc);
procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 98dcbca4..93f3a127 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -692,6 +692,8 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref) procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);
+ free requires this != other;
+ free ensures this != other;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 58085075..48d2c942 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -682,6 +682,8 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref) procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);
+ free requires this != other;
+ free ensures this != other;
|