Translate assignments of structs as a call to a (default) copy constructor

that does the field-by-field copy.

6 files changed, 145 insertions, 7 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 887792be..316e3faa 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -595,7 +595,8 @@ namespace BytecodeTranslator
     /// <param name="assignment"></param>

     public override void Visit(IAssignment assignment) {

       Contract.Assert(TranslatedExpressions.Count == 0);

-      TranslateAssignment(assignment.Token(), assignment.Target.Definition, assignment.Target.Instance, assignment.Source);

+      var tok = assignment.Token();

+      TranslateAssignment(tok, assignment.Target.Definition, assignment.Target.Instance, assignment.Source);

       return;

 

     }

@@ -608,13 +609,28 @@ namespace BytecodeTranslator
     private void TranslateAssignment(Bpl.IToken tok, object container, IExpression/*?*/ instance, IExpression source) {

       Contract.Assert(TranslatedExpressions.Count == 0);

 

+      var typ = source.Type;

+      var structCopy = typ.IsValueType && typ.TypeCode == PrimitiveTypeCode.NotPrimitive && !(source is IDefaultValue);

+      // then a struct value of type S is being assigned: "lhs := s"

+      // model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying

+      Bpl.DeclWithFormals proc = null;

+      if (structCopy) {

+        proc = this.sink.FindOrCreateProcedureForStructCopy(typ);

+      }

+      Bpl.Cmd cmd;

+

       var/*?*/ local = container as ILocalDefinition;

       if (local != null) {

         Contract.Assume(instance == null);

         this.Visit(source);

         var e = this.TranslatedExpressions.Pop();

         var bplLocal = Bpl.Expr.Ident(this.sink.FindOrCreateLocalVariable(local));

-        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplLocal, e));

+        if (structCopy) {

+          cmd = new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr>{ e, bplLocal, }, new List<Bpl.IdentifierExpr>());

+        } else {

+          cmd = Bpl.Cmd.SimpleAssign(tok, bplLocal, e);

+        }

+        StmtTraverser.StmtBuilder.Add(cmd);

         return;

       }

 

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index f65c4732..5c78298b 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -85,6 +85,7 @@ namespace BytecodeTranslator {
       } else if (typeDefinition.IsStruct) {

         sink.FindOrCreateType(typeDefinition);

         CreateDefaultStructConstructor(typeDefinition);

+        CreateStructCopyConstructor(typeDefinition);

         base.Visit(typeDefinition);

       } else {

         Console.WriteLine("Unknown kind of type definition '{0}' was found",

@@ -133,6 +134,42 @@ namespace BytecodeTranslator {
       impl.Proc = (Bpl.Procedure) proc; // TODO: get rid of cast

       this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

     }

+    

+    private void CreateStructCopyConstructor(ITypeDefinition typeDefinition) {

+      Contract.Requires(typeDefinition.IsStruct);

+

+      var proc = this.sink.FindOrCreateProcedureForStructCopy(typeDefinition);

+

+      var stmtBuilder = new Bpl.StmtListBuilder();

+

+      foreach (var f in typeDefinition.Fields) {

+        var boogieType = sink.CciTypeToBoogie(f.Type);

+        var fExp = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f));

+        var e = this.sink.Heap.ReadHeap(Bpl.Expr.Ident(proc.InParams[0]), fExp, AccessType.Struct, boogieType);

+        var o = Bpl.Expr.Ident(proc.InParams[1]);

+        var c = this.sink.Heap.WriteHeap(Bpl.Token.NoToken, o, fExp, e, AccessType.Struct, boogieType);

+        stmtBuilder.Add(c);

+      }

+

+      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})?

+      Bpl.Implementation impl =

+        new Bpl.Implementation(Bpl.Token.NoToken,

+        proc.Name,

+        new Bpl.TypeVariableSeq(),

+        proc.InParams,

+        proc.OutParams,

+        new Bpl.VariableSeq(),

+        stmtBuilder.Collect(Bpl.Token.NoToken),

+        attrib,

+        new Bpl.Errors()

+        );

+

+      impl.Proc = (Bpl.Procedure)proc; // TODO: get rid of cast

+      this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

+    }

 

     private bool sawCctor = false;

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index a40e067d..22cc8cb8 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -512,6 +512,7 @@ namespace BytecodeTranslator {
       return procAndFormalMap.Decl;

     }

 

+    private Dictionary<uint, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<uint, ProcedureInfo>();

     /// <summary>

     /// Struct "creation" (source code that looks like "new S()" for a struct type S) is modeled

     /// by a call to the nullary "ctor" that initializes all of the structs fields to zero-

@@ -519,13 +520,15 @@ namespace BytecodeTranslator {
     /// is defined in an assembly that is not being translated, then its behavior is unspecified.

     /// </summary>

     /// <param name="structType">A type reference to the value type for which the ctor should be returned.</param>

-    /// <returns>A nullary procedure that returns an initialized value of type <paramref name="structType"/>.</returns>

+    /// <returns>A unary procedure (i.e., it takes the struct value as its parameter) that initializes

+    /// its parameter of type <paramref name="structType"/>.

+    /// </returns>

     public Bpl.DeclWithFormals FindOrCreateProcedureForDefaultStructCtor(ITypeReference structType) {

       Contract.Requires(structType.IsValueType);

-     

+

       ProcedureInfo procAndFormalMap;

       var key = structType.InternedKey;

-      if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {

+      if (!this.declaredStructDefaultCtors.TryGetValue(key, out procAndFormalMap)) {

         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

         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);

@@ -541,7 +544,46 @@ namespace BytecodeTranslator {
           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

         procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);

-        this.declaredMethods.Add(key, procAndFormalMap);

+        this.declaredStructDefaultCtors.Add(key, procAndFormalMap);

+      }

+      return procAndFormalMap.Decl;

+    }

+

+    private Dictionary<uint, ProcedureInfo> declaredStructCopyCtors = new Dictionary<uint, ProcedureInfo>();

+    private Dictionary<uint, ProcedureInfo> declaredStructEqualityOperators = new Dictionary<uint, ProcedureInfo>();

+    /// <summary>

+    /// The assignment of one struct value to another is modeled by a method that makes a field-by-field

+    /// copy of the source of the assignment.

+    /// Note that the generated procedure has no contract. So if the struct

+    /// is defined in an assembly that is not being translated, then its behavior is unspecified.

+    /// </summary>

+    /// <param name="structType">A type reference to the value type for which the procedure should be returned.</param>

+    /// <returns>A binary procedure (i.e., it takes the two struct values as its parameters).

+    /// </returns>

+    public Bpl.DeclWithFormals FindOrCreateProcedureForStructCopy(ITypeReference structType) {

+      Contract.Requires(structType.IsValueType);

+

+      ProcedureInfo procAndFormalMap;

+      var key = structType.InternedKey;

+      if (!this.declaredStructCopyCtors.TryGetValue(key, out procAndFormalMap)) {

+        var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+        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), false);

+        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 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.IdentifierExprSeq(), // modifies

+          new Bpl.EnsuresSeq()

+          );

+        this.TranslatedProgram.TopLevelDeclarations.Add(proc);

+        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);

+        this.declaredStructCopyCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

     }

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 06029204..afe6a959 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -178,9 +178,28 @@ namespace BytecodeTranslator
       var initVal = localDeclarationStatement.InitialValue;

       if (initVal == null) return;

       var boogieLocal = this.sink.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

+      var boogieLocalExpr = Bpl.Expr.Ident(boogieLocal);

       var tok = localDeclarationStatement.Token();

       var e = ExpressionFor(initVal);

-      StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, boogieLocal), e));

+

+      var typ = initVal.Type;

+      var structCopy = typ.IsValueType && typ.TypeCode == PrimitiveTypeCode.NotPrimitive && !(initVal is IDefaultValue);

+      // then a struct value of type S is being assigned: "lhs := s"

+      // model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying

+      Bpl.DeclWithFormals proc = null;

+      if (structCopy) {

+        var defaultValue = new DefaultValue() {

+          DefaultValueType = typ,

+          Locations = new List<ILocation>(localDeclarationStatement.Locations),

+          Type = typ,

+        };

+        var e2 = ExpressionFor(defaultValue);

+        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2));

+        proc = this.sink.FindOrCreateProcedureForStructCopy(typ);

+        StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { e, boogieLocalExpr, }, new List<Bpl.IdentifierExpr>()));

+      } else {

+        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e));

+      }

       return;

     }

 

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 429419de..98dcbca4 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -691,6 +691,18 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)
 

 

 

+procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);

+

+

+

+implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref)

+{

+    $Heap := Write($Heap, other, RegressionTestInput.S.x, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x))));

+    $Heap := Write($Heap, other, RegressionTestInput.S.b, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b))));

+}

+

+

+

 const unique RegressionTestInput.Class0: Type;

 

 var RegressionTestInput.Class0.StaticInt: int;

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 78d4112c..58085075 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -681,6 +681,18 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)
 

 

 

+procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);

+

+

+

+implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref)

+{

+    other[RegressionTestInput.S.x] := Int2Box(Box2Int(this[RegressionTestInput.S.x]));

+    other[RegressionTestInput.S.b] := Bool2Box(Box2Bool(this[RegressionTestInput.S.b]));

+}

+

+

+

 const unique RegressionTestInput.Class0: Type;

 

 var RegressionTestInput.Class0.StaticInt: int;