Translate assignments to parameters that are of a struct type correctly. Note

that this means all methods with such parameters (where the parameter is passed
by value) must have free preconditions expressing that the parameters are
disjoint (since we are representing structs as Ref).

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;