Model newly constructed structs as a constant DefaultStruct that has axioms that

define it to return zero-equivalent values for all fields.

7 files changed, 229 insertions, 29 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 53e4ccce..d30202da 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -414,6 +414,8 @@ namespace BytecodeTranslator
         var lit = Bpl.Expr.False;

         lit.Type = Bpl.Type.Bool;

         TranslatedExpressions.Push(lit);

+      } else if (defaultValue.Type.ResolvedType.IsStruct){

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.Heap.DefaultStruct));

       } else {

         throw new NotImplementedException("Don't know how to translate type");

       }

@@ -626,31 +628,31 @@ namespace BytecodeTranslator
 

       #region Special case for s := default(S) when S is a struct

 

-      // The C# source "s = new S()" when S is a struct is compiled

-      // into an "initobj" instruction. That is decompiled into the

-      // assignment: "s = DefaultValue(S)".

-      // We translate it as a call to a pseduo-ctor that is created for S:

-      // "s := S.#default_ctor()".

-

-      if (assignment.Target.Type.ResolvedType.IsStruct &&

-        assignment.Target.Type.TypeCode == PrimitiveTypeCode.NotPrimitive &&

-        assignment.Source is IDefaultValue) {

-

-        this.Visit(assignment.Target);

-        var s = this.TranslatedExpressions.Pop();

-

-        var structType = assignment.Target.Type;

-        Bpl.IToken tok = assignment.Token();

-        var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(structType);

-        string methodname = proc.Name;

-        var inexpr = new List<Bpl.Expr>();

-        var outvars = new List<Bpl.IdentifierExpr>();

-        outvars.Add((Bpl.IdentifierExpr)s);

-        var call = new Bpl.CallCmd(tok, methodname, inexpr, outvars);

-        this.StmtTraverser.StmtBuilder.Add(call);

-

-        return;

-      }

+      //// The C# source "s = new S()" when S is a struct is compiled

+      //// into an "initobj" instruction. That is decompiled into the

+      //// assignment: "s = DefaultValue(S)".

+      //// We translate it as a call to a pseduo-ctor that is created for S:

+      //// "s := S.#default_ctor()".

+

+      //if (assignment.Target.Type.ResolvedType.IsStruct &&

+      //  assignment.Target.Type.TypeCode == PrimitiveTypeCode.NotPrimitive &&

+      //  assignment.Source is IDefaultValue) {

+

+      //  this.Visit(assignment.Target);

+      //  var s = this.TranslatedExpressions.Pop();

+

+      //  var structType = assignment.Target.Type;

+      //  Bpl.IToken tok = assignment.Token();

+      //  var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(structType);

+      //  string methodname = proc.Name;

+      //  var inexpr = new List<Bpl.Expr>();

+      //  var outvars = new List<Bpl.IdentifierExpr>();

+      //  outvars.Add((Bpl.IdentifierExpr)s);

+      //  var call = new Bpl.CallCmd(tok, methodname, inexpr, outvars);

+      //  this.StmtTraverser.StmtBuilder.Add(call);

+

+      //  return;

+      //}

       #endregion

 

       #region Transform Right Hand Side ...

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 81f2b9e9..6bd552fa 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -51,6 +51,13 @@ procedure {:inline 1} Alloc() returns (x: int)
   $Alloc[x] := true;

 }

 

+axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);

+axiom Box2Int($DefaultBox) == 0;

+axiom Box2Bool($DefaultBox) == false;

+

+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );

+

 ";

     private Sink sink;

 

@@ -176,6 +183,13 @@ procedure {:inline 1} Alloc() returns (x: ref)
   $Alloc[x] := true;

 }

 

+axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);

+axiom Box2Int($DefaultBox) == 0;

+axiom Box2Bool($DefaultBox) == false;

+

+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );

+

 ";

     private Sink sink;

 

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index dfdcc609..9c1870c1 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -74,6 +74,11 @@ namespace BytecodeTranslator {
     public Bpl.TypeCtorDecl BoxTypeDecl = null;

     public Bpl.CtorType BoxType;

 

+    [RepresentationFor("$DefaultBox", "const unique $DefaultBox : box;")]

+    public Bpl.Constant DefaultBox;

+    [RepresentationFor("$DefaultStruct", "const unique $DefaultStruct : struct;")]

+    public Bpl.Constant DefaultStruct;

+

     [RepresentationFor("Type", "type Type;")]

     protected Bpl.TypeCtorDecl TypeTypeDecl = null;

     protected Bpl.CtorType TypeType;

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 9482573f..ba35121d 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -73,7 +73,7 @@ namespace BytecodeTranslator {
         return; // enums just are translated as ints

       } else if (typeDefinition.IsStruct) {

         sink.FindOrCreateType(typeDefinition);

-        CreateDefaultStructConstructor(typeDefinition);

+        //CreateDefaultStructConstructor(typeDefinition);

         base.Visit(typeDefinition);

       } else {

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

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index b5fa3582..40cf9575 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -132,14 +132,23 @@ namespace RegressionTestInput {
   }

 

   public struct S {

-    int x;

-    bool b;

+    public int x;

+    public bool b;

   }

 

   public class CreateStruct {

     public S Create() {

-      return new S();

+      var s = new S();

+      Contract.Assert(s.x == 0);

+      Contract.Assert(s.b == false);

+      return s;

     }

+    S AssignThreeToSDotX(S s) {

+      s.x = 3;

+      Contract.Assert(s.x == 3);

+      return s;

+    }

+

   }

 

 }

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index e0102a57..5891b6f5 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -31,6 +31,16 @@ implementation Alloc() returns (x: ref)
 

 

 

+axiom (forall x: Field :: $DefaultStruct[x] == $DefaultBox);

+

+axiom Box2Int($DefaultBox) == 0;

+

+axiom Box2Bool($DefaultBox) == false;

+

+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);

+

+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);

+

 procedure DelegateAdd(a: int, b: int) returns (c: int);

 

 

@@ -204,6 +214,10 @@ type Field;
 

 type box;

 

+const unique $DefaultBox: box;

+

+const unique $DefaultStruct: struct;

+

 type Type;

 

 function Box2Int(box) : int;

@@ -720,6 +734,12 @@ implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
 

 

 

+const unique RegressionTestInput.S: Type;

+

+const unique RegressionTestInput.S.x: Field;

+

+const unique RegressionTestInput.S.b: Field;

+

 const unique RegressionTestInput.AsyncAttribute: Type;

 

 procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);

@@ -747,3 +767,68 @@ implementation RegressionTestInput.AsyncAttribute.#cctor()
 }

 

 

+

+const unique RegressionTestInput.CreateStruct: Type;

+

+procedure RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box);

+

+

+

+implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box)

+{

+  var local_0: [Field]box;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 141} true;

+    local_0 := $DefaultStruct;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 142} true;

+    assert Box2Int(local_0[RegressionTestInput.S.x]) == 0;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 143} true;

+    assert !Box2Bool(local_0[RegressionTestInput.S.b]);

+    assert {:sourceFile "Class1.cs"} {:sourceLine 145} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box);

+

+

+

+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box)

+{

+  var s: [Field]box;

+

+    s := s$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 147} true;

+    s := s[RegressionTestInput.S.x := Int2Box(3)];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 148} true;

+    assert Box2Int(s[RegressionTestInput.S.x]) == 3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 150} true;

+    $result := s;

+    return;

+}

+

+

+

+procedure RegressionTestInput.CreateStruct.#ctor(this: int);

+

+

+

+implementation RegressionTestInput.CreateStruct.#ctor(this: int)

+{

+    call System.Object.#ctor(this);

+    return;

+}

+

+

+

+procedure RegressionTestInput.CreateStruct.#cctor();

+

+

+

+implementation RegressionTestInput.CreateStruct.#cctor()

+{

+}

+

+

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 872da3ae..b6df83bc 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -33,6 +33,16 @@ implementation Alloc() returns (x: int)
 

 

 

+axiom (forall x: Field :: $DefaultStruct[x] == $DefaultBox);

+

+axiom Box2Int($DefaultBox) == 0;

+

+axiom Box2Bool($DefaultBox) == false;

+

+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);

+

+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);

+

 procedure DelegateAdd(a: int, b: int) returns (c: int);

 

 

@@ -194,6 +204,10 @@ type Field;
 

 type box;

 

+const unique $DefaultBox: box;

+

+const unique $DefaultStruct: struct;

+

 type Type;

 

 function Box2Int(box) : int;

@@ -710,6 +724,12 @@ implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
 

 

 

+const unique RegressionTestInput.S: Type;

+

+var RegressionTestInput.S.x: [int]int;

+

+var RegressionTestInput.S.b: [int]bool;

+

 const unique RegressionTestInput.AsyncAttribute: Type;

 

 procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);

@@ -737,3 +757,68 @@ implementation RegressionTestInput.AsyncAttribute.#cctor()
 }

 

 

+

+const unique RegressionTestInput.CreateStruct: Type;

+

+procedure RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box);

+

+

+

+implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box)

+{

+  var local_0: [Field]box;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 141} true;

+    local_0 := $DefaultStruct;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 142} true;

+    assert local_0[RegressionTestInput.S.x] == 0;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 143} true;

+    assert !local_0[RegressionTestInput.S.b];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 145} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box);

+

+

+

+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box)

+{

+  var s: [Field]box;

+

+    s := s$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 147} true;

+    s[RegressionTestInput.S.x] := 3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 148} true;

+    assert s[RegressionTestInput.S.x] == 3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 150} true;

+    $result := s;

+    return;

+}

+

+

+

+procedure RegressionTestInput.CreateStruct.#ctor(this: int);

+

+

+

+implementation RegressionTestInput.CreateStruct.#ctor(this: int)

+{

+    call System.Object.#ctor(this);

+    return;

+}

+

+

+

+procedure RegressionTestInput.CreateStruct.#cctor();

+

+

+

+implementation RegressionTestInput.CreateStruct.#cctor()

+{

+}

+

+