Fix call to struct copy ctor.

3 files changed, 176 insertions, 38 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 3a8deab3..723b90ca 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -752,8 +752,8 @@ namespace BytecodeTranslator
           // 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, }, new List<Bpl.IdentifierExpr>{ bplLocal, });

+            var bplLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(currentType));

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

             this.StmtTraverser.StmtBuilder.Add(cmd);

             e = bplLocal;

           }

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 75e77da9..92438297 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -442,12 +442,98 @@ var {:thread_local} $Exception: Ref;
 

 

 

-function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

+function {:constructor} T$RegressionTestInput.StructContainingStruct() : Type;

+

+function {:constructor} {:extern} T$System.ValueType() : Type;

 

 function {:constructor} {:extern} T$System.Object() : Type;

 

 axiom (forall $T: Type :: { $Subtype(T$System.Object(), $T) } $Subtype(T$System.Object(), $T) <==> T$System.Object() == $T);

 

+axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T));

+

+axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) } $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) <==> T$RegressionTestInput.StructContainingStruct() == $T || $Subtype(T$System.ValueType(), $T));

+

+procedure RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref);

+

+

+

+const unique F$RegressionTestInput.StructContainingStruct.d: Field;

+

+procedure RegressionTestInput.S.#default_ctor($this: Ref);

+

+

+

+function {:constructor} T$RegressionTestInput.S() : Type;

+

+axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T));

+

+const unique F$RegressionTestInput.StructContainingStruct.s: Field;

+

+implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref)

+{

+  var $tmp0: Ref;

+

+    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.d, Real2Box($DefaultReal));

+    call $tmp0 := Alloc();

+    call RegressionTestInput.S.#default_ctor($tmp0);

+    assume $DynamicType($tmp0) == T$RegressionTestInput.S();

+    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.s, Ref2Box($tmp0));

+}

+

+

+

+procedure RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref);

+  free ensures this != other;

+

+

+

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

+  free ensures this != other;

+

+

+

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

+{

+  var $tmp1: Ref;

+

+    call other := Alloc();

+    assume $DynamicType(other) == T$RegressionTestInput.StructContainingStruct();

+    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.d, Real2Box(Box2Real(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.d))));

+    call $tmp1 := RegressionTestInput.S.#copy_ctor(Box2Ref(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.s)));

+    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.s, Ref2Box($tmp1));

+}

+

+

+

+procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref);

+

+

+

+implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref)

+{

+  var s: Ref;

+  var t_Ref: Ref;

+  var $tmp0: Ref;

+  var $localExc: Ref;

+  var $label: int;

+

+    s := s$in;

+    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 206} true;

+    call $tmp0 := Alloc();

+    call RegressionTestInput.StructContainingStruct.#default_ctor($tmp0);

+    assume $DynamicType($tmp0) == T$RegressionTestInput.StructContainingStruct();

+    t_Ref := $tmp0;

+    call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s);

+    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 208} true;

+    $result := t_Ref;

+    return;

+}

+

+

+

+function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

+

 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

@@ -654,18 +740,6 @@ procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result:
 

 

 

-procedure RegressionTestInput.S.#default_ctor($this: Ref);

-

-

-

-function {:constructor} T$RegressionTestInput.S() : Type;

-

-function {:constructor} {:extern} T$System.ValueType() : Type;

-

-axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T));

-

-axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T));

-

 const unique F$RegressionTestInput.S.x: Field;

 

 const unique F$RegressionTestInput.S.b: Field;

@@ -1317,11 +1391,6 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref)
 

 

 

-procedure RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref);

-  free ensures this != other;

-

-

-

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

 {

     call other := Alloc();

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index acc6970a..d7848c0c 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -428,12 +428,98 @@ var {:thread_local} $Exception: Ref;
 

 

 

-function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

+function {:constructor} T$RegressionTestInput.StructContainingStruct() : Type;

+

+function {:constructor} {:extern} T$System.ValueType() : Type;

 

 function {:constructor} {:extern} T$System.Object() : Type;

 

 axiom (forall $T: Type :: { $Subtype(T$System.Object(), $T) } $Subtype(T$System.Object(), $T) <==> T$System.Object() == $T);

 

+axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T));

+

+axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) } $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) <==> T$RegressionTestInput.StructContainingStruct() == $T || $Subtype(T$System.ValueType(), $T));

+

+procedure RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref);

+

+

+

+var F$RegressionTestInput.StructContainingStruct.d: [Ref]Real;

+

+procedure RegressionTestInput.S.#default_ctor($this: Ref);

+

+

+

+function {:constructor} T$RegressionTestInput.S() : Type;

+

+axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T));

+

+var F$RegressionTestInput.StructContainingStruct.s: [Ref]Ref;

+

+implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref)

+{

+  var $tmp0: Ref;

+

+    F$RegressionTestInput.StructContainingStruct.d[$this] := $DefaultReal;

+    call $tmp0 := Alloc();

+    call RegressionTestInput.S.#default_ctor($tmp0);

+    assume $DynamicType($tmp0) == T$RegressionTestInput.S();

+    F$RegressionTestInput.StructContainingStruct.s[$this] := $tmp0;

+}

+

+

+

+procedure RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref);

+  free ensures this != other;

+

+

+

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

+  free ensures this != other;

+

+

+

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

+{

+  var $tmp1: Ref;

+

+    call other := Alloc();

+    assume $DynamicType(other) == T$RegressionTestInput.StructContainingStruct();

+    F$RegressionTestInput.StructContainingStruct.d[other] := F$RegressionTestInput.StructContainingStruct.d[this];

+    call $tmp1 := RegressionTestInput.S.#copy_ctor(F$RegressionTestInput.StructContainingStruct.s[this]);

+    F$RegressionTestInput.StructContainingStruct.s[other] := $tmp1;

+}

+

+

+

+procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref);

+

+

+

+implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref)

+{

+  var s: Ref;

+  var t_Ref: Ref;

+  var $tmp0: Ref;

+  var $localExc: Ref;

+  var $label: int;

+

+    s := s$in;

+    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 206} true;

+    call $tmp0 := Alloc();

+    call RegressionTestInput.StructContainingStruct.#default_ctor($tmp0);

+    assume $DynamicType($tmp0) == T$RegressionTestInput.StructContainingStruct();

+    t_Ref := $tmp0;

+    call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s);

+    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 208} true;

+    $result := t_Ref;

+    return;

+}

+

+

+

+function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

+

 axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T));

 

 procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

@@ -640,18 +726,6 @@ procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result:
 

 

 

-procedure RegressionTestInput.S.#default_ctor($this: Ref);

-

-

-

-function {:constructor} T$RegressionTestInput.S() : Type;

-

-function {:constructor} {:extern} T$System.ValueType() : Type;

-

-axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T));

-

-axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T));

-

 var F$RegressionTestInput.S.x: [Ref]int;

 

 var F$RegressionTestInput.S.b: [Ref]bool;

@@ -1303,11 +1377,6 @@ implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref)
 

 

 

-procedure RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref);

-  free ensures this != other;

-

-

-

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

 {

     call other := Alloc();