merge changes with shaz's checkin.

5 files changed, 121 insertions, 2 deletions

diff --git a/.hgignore b/.hgignore
index 1905d88e..6852779f 100644
--- a/.hgignore
+++ b/.hgignore
@@ -4,7 +4,7 @@ syntax: regexp
 ^(Source|BCT|Jennisys)/.*\.(user|suo|cache)$

 ^Source/(Core|Dafny)/(Parser|Scanner).cs.old$

 ^Binaries/.*\.(dll|pdb|exe|manifest|config)$

-^.*(bin|obj)/([^/]*/)?(Debug|Release)/.*$

+^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked)/.*$

 ^Binaries/BytecodeTranslator$

 ^BCT/Binaries/.*$

 Test/([^/]*)/Output

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 4e04c104..53e4ccce 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -624,6 +624,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/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index bbcc81f5..9482573f 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..b5fa3582 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -130,4 +130,16 @@ namespace RegressionTestInput {
       this.y = this.x;

     }

   }

+

+  public struct S {

+    int x;

+    bool b;

+  }

+

+  public class CreateStruct {

+    public S Create() {

+      return new S();

+    }

+  }

+

 }