modeling struct creation by default value

8 files changed, 320 insertions, 1 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 4e04c104..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");

       }

@@ -624,6 +626,35 @@ namespace BytecodeTranslator
     public override void Visit(IAssignment assignment) {

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

 

+      #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;

+      //}

+      #endregion

+

       #region Transform Right Hand Side ...

       this.Visit(assignment.Source);

       Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();

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 bbcc81f5..ba35121d 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -73,6 +73,7 @@ namespace BytecodeTranslator {
         return; // enums just are translated as ints

       } else if (typeDefinition.IsStruct) {

         sink.FindOrCreateType(typeDefinition);

+        //CreateDefaultStructConstructor(typeDefinition);

         base.Visit(typeDefinition);

       } else {

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

@@ -81,6 +82,49 @@ namespace BytecodeTranslator {
       }

     }

 

+    private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {

+      Contract.Requires(typeDefinition.IsStruct);

+

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

+

+      var stmtBuilder = new Bpl.StmtListBuilder();

+

+      foreach (var f in typeDefinition.Fields) {

+        Bpl.Expr e;

+        var bplType = this.sink.CciTypeToBoogie(f.Type);

+        if (bplType == Bpl.Type.Int) {

+          e = Bpl.Expr.Literal(0);

+          e.Type = Bpl.Type.Int;

+        } else if (bplType == Bpl.Type.Bool) {

+          e = Bpl.Expr.False;

+          e.Type = Bpl.Type.Bool;

+        } else {

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

+        }

+

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

+        var o = Bpl.Expr.Ident(proc.OutParams[0]);

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

+        stmtBuilder.Add(c);

+      }

+

+      var attrib = new Bpl.QKeyValue(typeDefinition.Token(), "inline", new List<object>(1), 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;

 

     private void CreateStaticConstructor(ITypeDefinition typeDefinition) {

@@ -290,7 +334,7 @@ namespace BytecodeTranslator {
           foreach (var f in method.ContainingTypeDefinition.Fields) {

             if (f.IsStatic == method.IsStatic) {

               var a = new Assignment() {

-                Source = new DefaultValue() { Type = f.Type, },

+                Source = new DefaultValue() { DefaultValueType = f.Type, Type = f.Type, },

                 Target = new TargetExpression() { Definition = f, Instance = method.IsConstructor ? thisExp : null, Type = f.Type },

                 Type = f.Type,

               };

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 9c20f96a..6e3909ab 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -415,6 +415,40 @@ namespace BytecodeTranslator {
       return procAndFormalMap.Decl;

     }

 

+    /// <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-

+    /// equivalent values. 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 ctor should be returned.</param>

+    /// <returns>A nullary procedure that returns an initialized value 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)) {

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

+        var tok = structType.Token();

+        var selfType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

+        var selfOut = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), false);

+        var outvars = new Bpl.Formal[]{ selfOut };

+        var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#default_ctor",

+          new Bpl.TypeVariableSeq(),

+          new Bpl.VariableSeq(), // in

+          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.declaredMethods.Add(key, procAndFormalMap);

+      }

+      return procAndFormalMap.Decl;

+    }

+

     // TODO: Fix test to return true iff method is marked with the "real" [Pure] attribute

     // also, should it return true for properties and all of the other things the tools

     // consider pure?

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index f2918aa7..40cf9575 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -130,4 +130,25 @@ namespace RegressionTestInput {
       this.y = this.x;

     }

   }

+

+  public struct S {

+    public int x;

+    public bool b;

+  }

+

+  public class CreateStruct {

+    public S Create() {

+      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()

+{

+}

+

+