Removed the method DefaultValue from the sink: if a default value of a type

is desired, then the CCI nodes must be created and an expression/statement
traverser used to translate it.

7 files changed, 89 insertions, 54 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 4456c860..0925bc7c 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -350,7 +350,8 @@ namespace BytecodeTranslator
 

       var typ = defaultValue.Type;

 

-      if (typ.IsValueType && typ.TypeCode == PrimitiveTypeCode.NotPrimitive) {

+      #region Struct

+      if (TranslationHelper.IsStruct(typ)) {

         // then it is a struct and gets special treatment

         // translate it as if it were a call to the nullary ctor for the struct type

         // (which doesn't actually exist, but gets generated for each struct type

@@ -383,8 +384,28 @@ namespace BytecodeTranslator
         this.TranslatedExpressions.Push(locExpr);

         return;

       }

+      #endregion

 

-      TranslatedExpressions.Push(this.sink.DefaultValue(typ));

+      Bpl.Expr e;

+      var bplType = this.sink.CciTypeToBoogie(typ);

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

+        var lit = Bpl.Expr.Literal(0);

+        lit.Type = Bpl.Type.Int;

+        e = lit;

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

+        var lit = Bpl.Expr.False;

+        lit.Type = Bpl.Type.Bool;

+        e = lit;

+      } else if (bplType == this.sink.Heap.RefType) {

+        e = Bpl.Expr.Ident(this.sink.Heap.NullRef);

+      } else if (bplType == this.sink.Heap.BoxType) {

+        e = Bpl.Expr.Ident(this.sink.Heap.DefaultBox);

+      } else {

+        throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(typ)));

+      }

+

+      TranslatedExpressions.Push(e);

+      return;

     }

 

     #endregion

@@ -614,7 +635,7 @@ namespace BytecodeTranslator
       Contract.Assert(TranslatedExpressions.Count == 0);

 

       var typ = source.Type;

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

+      var structCopy = TranslationHelper.IsStruct(typ) && !(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;

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 5c78298b..2458d27c 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -104,29 +104,47 @@ namespace BytecodeTranslator {
 

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

 

-      var stmtBuilder = new Bpl.StmtListBuilder();

+      this.sink.BeginMethod();

+      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+      var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

-        var e = this.sink.DefaultValue(f.Type);

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

-        var o = Bpl.Expr.Ident(proc.InParams[0]);

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

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

-        stmtBuilder.Add(c);

+        if (f.IsStatic) continue;

+        var s = new ExpressionStatement() {

+          Expression = new Assignment() {

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

+            Target = new TargetExpression() {

+              Definition = f,

+              Instance = new ThisReference() { Type = typeDefinition, },

+              Type = f.Type,

+            },

+            Type = f.Type,

+          },

+        };

       }

 

+      stmtTranslator.Visit(stmts);

+      var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);

+

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

+

+      List<Bpl.Variable> vars = new List<Bpl.Variable>();

+      foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

+        vars.Add(v);

+      }

+      Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

+

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

+        vseq,

+        translatedStatements,

         attrib,

         new Bpl.Errors()

         );

@@ -143,6 +161,7 @@ namespace BytecodeTranslator {
       var stmtBuilder = new Bpl.StmtListBuilder();

 

       foreach (var f in typeDefinition.Fields) {

+        if (f.IsStatic) continue;

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

@@ -187,32 +206,49 @@ namespace BytecodeTranslator {
 

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

 

-      var stmtBuilder = new Bpl.StmtListBuilder();

+      this.sink.BeginMethod();

+

+      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+      var stmts = new List<IStatement>();

+

       foreach (var f in typeDefinition.Fields) {

-        if (f.IsStatic) {

-

-          var e = this.sink.DefaultValue(f.Type);

-          stmtBuilder.Add(

-            TranslationHelper.BuildAssignCmd(

-            Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(f)), 

-            e

-            ));

-        }

+        if (!f.IsStatic) continue;

+        stmts.Add(

+          new ExpressionStatement() {

+            Expression = new Assignment() {

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

+              Target = new TargetExpression() {

+                Definition = f,

+                Instance = null,

+                Type = f.Type,

+              },

+              Type = f.Type,

+            }

+          });

       }

+

+      stmtTranslator.Visit(stmts);

+      var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);

+

+      List<Bpl.Variable> vars = new List<Bpl.Variable>();

+      foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

+        vars.Add(v);

+      }

+      Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

+

       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)

+        vseq,

+        translatedStatements

         );

 

       impl.Proc = proc;

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

 

-

     }

 

     /// <summary>

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 7e6ddcff..093233cb 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -85,28 +85,6 @@ namespace BytecodeTranslator {
     

     public readonly Bpl.Program TranslatedProgram;

 

-    public Bpl.Expr DefaultValue(ITypeReference type) {

-      var bplType = CciTypeToBoogie(type);

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

-        var lit = Bpl.Expr.Literal(0);

-        lit.Type = Bpl.Type.Int;

-        return lit;

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

-        var lit = Bpl.Expr.False;

-        lit.Type = Bpl.Type.Bool;

-        return lit;

-      } else if (type.ResolvedType.IsStruct) {

-        return Bpl.Expr.Ident(this.Heap.DefaultStruct);

-      } else if (bplType == this.Heap.RefType) {

-        return Bpl.Expr.Ident(this.Heap.NullRef);

-      }

-      else if (bplType == this.Heap.BoxType) {

-        return Bpl.Expr.Ident(this.Heap.DefaultBox);

-      } else {

-        throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));

-      }

-    }

-

     public Bpl.Type CciTypeToBoogie(ITypeReference type) {

       if (TypeHelper.TypesAreEquivalent(type, type.PlatformType.SystemBoolean))

         return Bpl.Type.Bool;

@@ -478,11 +456,11 @@ namespace BytecodeTranslator {
         for (int p1index = 0; p1index < method.ParameterCount; p1index++) {

           var p1 = paramList[p1index];

           if (p1.IsByReference) continue;

-          if (!(p1.Type.IsValueType && p1.Type.TypeCode == PrimitiveTypeCode.NotPrimitive)) continue;

+          if (!TranslationHelper.IsStruct(p1.Type)) continue;

           for (int p2index = p1index + 1; p2index < method.ParameterCount; p2index++) {

             var p2 = paramList[p2index];

             if (p2.IsByReference) continue;

-            if (!(p2.Type.IsValueType && p2.Type.TypeCode == PrimitiveTypeCode.NotPrimitive)) continue;

+            if (!TranslationHelper.IsStruct(p2.Type)) continue;

             if (!TypeHelper.TypesAreEquivalent(p1.Type, p2.Type)) continue;

             var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq,

               Bpl.Expr.Ident(formalMap[p1].inParameterCopy), Bpl.Expr.Ident(formalMap[p2].inParameterCopy)));

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index afe6a959..f03894a2 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -183,7 +183,7 @@ namespace BytecodeTranslator
       var e = ExpressionFor(initVal);

 

       var typ = initVal.Type;

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

+      var structCopy = TranslationHelper.IsStruct(typ) && !(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;

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 54ed1700..fde776f9 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -122,6 +122,10 @@ namespace BytecodeTranslator {
       return s;

     }

 

+    public static bool IsStruct(ITypeReference typ) {

+      return typ.IsValueType && !typ.IsEnum && typ.TypeCode == PrimitiveTypeCode.NotPrimitive;

+    }

+

     #region Temp Stuff that must be replaced as soon as there is real code to deal with this

 

     public static Bpl.Variable TempThisVar() {

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 93f3a127..98583054 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -685,8 +685,6 @@ implementation RegressionTestInput.RefParameters.#cctor()
 

 implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)

 {

-    $Heap := Write($Heap, this, RegressionTestInput.S.x, Int2Box(0));

-    $Heap := Write($Heap, this, RegressionTestInput.S.b, Bool2Box(false));

 }

 

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 48d2c942..c292fb90 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -675,8 +675,6 @@ implementation RegressionTestInput.RefParameters.#cctor()
 

 implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)

 {

-    this[RegressionTestInput.S.x] := Int2Box(0);

-    this[RegressionTestInput.S.b] := Bool2Box(false);

 }