refactored the prelude, added thread_local attribute to $Exception variable

3 files changed, 73 insertions, 189 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 3067975d..410b9eb3 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -291,16 +291,6 @@ namespace BytecodeTranslator
     public override void Visit(IAddressOf addressOf)

     {

       Visit(addressOf.Expression);

-      //if (addressOf.Expression.Type.IsValueType)

-      //{

-      //  var e = this.TranslatedExpressions.Pop();

-      //  var callBox = new Bpl.NAryExpr(

-      //    addressOf.Token(),

-      //  new Bpl.FunctionCall(this.sink.Heap.Struct2Ref),

-      //  new Bpl.ExprSeq(e)

-      //  );

-      //  TranslatedExpressions.Push(callBox);

-      //}

     }

     #endregion

 

@@ -728,23 +718,14 @@ namespace BytecodeTranslator
         if (instance == null) {

           // static fields are not kept in the heap

           StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, f, e));

-        } else {

-          if (false && field.ContainingType.ResolvedType.IsStruct) {

-            //var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);

-            //var s_prime_expr = Bpl.Expr.Ident(s_prime);

-            //var boogieType = sink.CciTypeToBoogie(field.Type);

-            //StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,

-            //  field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

-            //  boogieType));

-            UpdateStruct(tok, instance, field, e);

-          } else {

-            this.Visit(instance);

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

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

-            StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,

-              field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

-              boogieType));

-          }

+        }

+        else {

+          this.Visit(instance);

+          var x = this.TranslatedExpressions.Pop();

+          var boogieType = sink.CciTypeToBoogie(field.Type);

+          StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,

+            field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

+            boogieType));

         }

         return;

       }

@@ -805,34 +786,7 @@ namespace BytecodeTranslator
 

       Contract.Assume(false);

     }

-

-    private void UpdateStruct(Bpl.IToken tok, IExpression iExpression, IFieldReference field, Bpl.Expr e) {

-      var addrOf = iExpression as IAddressOf;

-      if (addrOf == null) return;

-      var addressableExpression = addrOf.Expression as IAddressableExpression;

-      if (addressableExpression == null) return;

-

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

-

-      if (addressableExpression.Instance == null) {

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

-        this.Visit(addressableExpression);

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

-        StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, def, f, e,

-          AccessType.Struct,

-          boogieType));

-      } else {

-        var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);

-        var s_prime_expr = Bpl.Expr.Ident(s_prime);

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

-        StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,

-          AccessType.Struct,

-          boogieType));

-        UpdateStruct(tok, addressableExpression.Instance, addressableExpression.Definition as IFieldReference, s_prime_expr);

-      }

-    }

-

-

+    

     #endregion

 

     #region Translate Object Creation

@@ -1388,7 +1342,7 @@ namespace BytecodeTranslator
               func = this.sink.Heap.Int2Ref;

           } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.NotPrimitive) {

             // REVIEW: Do we need to check to make sure that conversion.ValueToConvert.Type.IsValueType?

-            func = this.sink.Heap.Struct2Ref;

+            func = this.sink.Heap.Box2Ref;

           } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float32 ||

             conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float64) {

               func = this.sink.Heap.Real2Ref;

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 8da78bca..74121074 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -32,67 +32,15 @@ namespace BytecodeTranslator {
     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

-    private readonly string InitialPreludeText =

-      @"type Struct = [Field]Box;

-type HeapType = [Ref,Field]Box;

-var $Heap: HeapType;

-

-var $Alloc: [Ref] bool;

-procedure {:inline 1} Alloc() returns (x: Ref)

-  modifies $Alloc;

-{

-  assume $Alloc[x] == false && x != null;

-  $Alloc[x] := true;

-}

-

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

-axiom Box2Int($DefaultBox) == 0;

-axiom Box2Bool($DefaultBox) == false;

-axiom Box2Ref($DefaultBox) == null;

-//axiom Box2Struct($DefaultBox) == $DefaultStruct;

-

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

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

-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

-axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );

-

-procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

-{

-  $result := $TypeOf($DynamicType(this));

-}

-function $TypeOfInv(Ref): Type;

-axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

-

-function $ThreadDelegate(Ref) : Ref;

-

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

-{

-  call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);

-}

-procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);

-

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) 

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start(this: Ref) 

-{

-  call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));

-}

-procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);

+    private readonly string InitialPreludeText = @"";

 

-";

     private Sink sink;

 

     public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {

       heap = this;

       program = null;

       this.sink = sink;

-      string prelude = this.InitialPreludeText + this.DelegateEncodingText;

+      string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

         this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

@@ -201,57 +149,8 @@ procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

     private readonly string InitialPreludeText =

-      @"//type Struct = [Field]Box;

-type Struct = Ref;

-type HeapType = [Ref][Field]Box;

-

-var $Alloc: [Ref] bool;

-procedure {:inline 1} Alloc() returns (x: Ref)

-  modifies $Alloc;

-{

-  assume $Alloc[x] == false && x != null;

-  $Alloc[x] := true;

-}

-

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

-//axiom (forall h : HeapType, f : Field :: { Read(h, $DefaultStruct, f) } Read(h, $DefaultStruct, f) == $DefaultBox);

-axiom Box2Int($DefaultBox) == 0;

-axiom Box2Bool($DefaultBox) == false;

-axiom Box2Ref($DefaultBox) == null;

-//axiom Box2Struct($DefaultBox) == $DefaultStruct;

-

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

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

-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

-axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );

-

-procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

-{

-  $result := $TypeOf($DynamicType(this));

-}

-function $TypeOfInv(Ref): Type;

-axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

-

-function $ThreadDelegate(Ref) : Ref;

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

-{

-  call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);

-}

-procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);

-

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) 

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start(this: Ref) 

-{

-  call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));

-}

-procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);

+      @"type HeapType = [Ref][Field]Box;

+

 ";

     private Sink sink;

 

@@ -261,7 +160,7 @@ procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
       this.sink = sink;

       heap = this;

       program = null;

-      string prelude = this.InitialPreludeText + this.DelegateEncodingText;

+      string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

         this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index c63791e2..3404c190 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -96,18 +96,6 @@ namespace BytecodeTranslator {
     public Bpl.TypeCtorDecl TypeTypeDecl = null;

     public Bpl.CtorType TypeType;

 

-    private Bpl.Type structType = null;

-    public Bpl.Type StructType {

-      get {

-        if (structType == null) {

-          structType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(FieldType), BoxType);

-        }

-        return structType;

-      }

-    }

-    [RepresentationFor("$DefaultStruct", "const unique $DefaultStruct : [Field]Box;")]

-    public Bpl.Constant DefaultStruct;

-

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

     protected Bpl.TypeCtorDecl RealTypeDecl = null;

     public Bpl.CtorType RealType;

@@ -126,9 +114,6 @@ namespace BytecodeTranslator {
     [RepresentationFor("Box2Bool", "function Box2Bool(Box): bool;")]

     public Bpl.Function Box2Bool = null;

 

-    [RepresentationFor("Box2Struct", "function Box2Struct(Box): Struct;")]

-    public Bpl.Function Box2Struct = null;

-

     [RepresentationFor("Box2Ref", "function Box2Ref(Box): Ref;")]

     public Bpl.Function Box2Ref = null;

 

@@ -141,9 +126,6 @@ namespace BytecodeTranslator {
     [RepresentationFor("Bool2Box", "function Bool2Box(bool): Box;")]

     public Bpl.Function Bool2Box = null;

 

-    [RepresentationFor("Struct2Box", "function Struct2Box(Struct): Box;")]

-    public Bpl.Function Struct2Box = null;

-

     [RepresentationFor("Ref2Box", "function Ref2Box(Ref): Box;")]

     public Bpl.Function Ref2Box = null;

 

@@ -159,8 +141,6 @@ namespace BytecodeTranslator {
         conversion = this.Bool2Box;

       else if (boogieType == Bpl.Type.Int)

         conversion = this.Int2Box;

-      else if (boogieType == StructType)

-        conversion = this.Struct2Box;

       else if (boogieType == RefType)

         conversion = this.Ref2Box;

       else if (boogieType == RealType)

@@ -184,8 +164,6 @@ namespace BytecodeTranslator {
         conversion = this.Box2Bool;

       else if (boogieType == Bpl.Type.Int)

         conversion = this.Box2Int;

-      else if (boogieType == StructType)

-        conversion = this.Box2Struct;

       else if (boogieType == RefType)

         conversion = this.Box2Ref;

       else if (boogieType == RealType)

@@ -210,8 +188,6 @@ namespace BytecodeTranslator {
     /// <summary>

     /// Used to represent "boxing" as it is done in the CLR.

     /// </summary>

-    [RepresentationFor("Struct2Ref", "function Struct2Ref(Struct): Ref;")]

-    public Bpl.Function Struct2Ref = null;

     [RepresentationFor("Int2Ref", "function Int2Ref(int): Ref;")]

     public Bpl.Function Int2Ref = null;

     [RepresentationFor("Bool2Ref", "function Bool2Ref(bool): Ref;")]

@@ -327,8 +303,63 @@ namespace BytecodeTranslator {
     [RepresentationFor("$As", "function $As(Ref, Type): Ref;")]

     public Bpl.Function AsFunction = null;

 

-    protected readonly string DelegateEncodingText =

-      @"procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

+    protected readonly string CommonText =

+      @"var $Alloc: [Ref] bool;

+

+procedure {:inline 1} Alloc() returns (x: Ref)

+  modifies $Alloc;

+{

+  assume $Alloc[x] == false && x != null;

+  $Alloc[x] := true;

+}

+

+function $TypeOfInv(Ref): Type;

+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

+

+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

+{

+  $result := $TypeOf($DynamicType(this));

+}

+

+axiom Box2Int($DefaultBox) == 0;

+axiom Box2Bool($DefaultBox) == false;

+axiom Box2Ref($DefaultBox) == null;

+

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

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

+axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

+

+function $ThreadDelegate(Ref) : Ref;

+

+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

+{

+  assume $ThreadDelegate(this) == start$in;

+}

+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

+{

+  call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);

+}

+procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref) {

+  $Exception := null;

+  call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);

+}

+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);

+

+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) 

+{

+  assume $ThreadDelegate(this) == start$in;

+}

+procedure {:inline 1} System.Threading.Thread.Start(this: Ref) 

+{

+  call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));

+}

+procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref) {

+  $Exception := null;

+  call System.Threading.ThreadStart.Invoke(this);

+}

+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);

+

+procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

 {

   var m: int;

   var o: Ref;

@@ -453,7 +484,7 @@ procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref)
     [RepresentationFor("$Receiver", "var $Receiver: [Ref][Ref]Ref;")]

     public Bpl.GlobalVariable DelegateReceiver = null;

 

-    [RepresentationFor("$Exception", "var $Exception: Ref;")]

+    [RepresentationFor("$Exception", "var {:thread_local} $Exception: Ref;")]

     public Bpl.GlobalVariable ExceptionVariable = null;

   }