Fixed array construction

Added a couple more stubs

3 files changed, 41 insertions, 19 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index d1708608..052d8bf4 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -883,7 +883,21 @@ namespace BytecodeTranslator
 

     public override void Visit(ICreateArray createArrayInstance)

     {

-      TranslateArrayCreation(createArrayInstance);

+      Bpl.IToken cloc = createArrayInstance.Token();

+      var a = this.sink.CreateFreshLocal(createArrayInstance.Type);

+

+      Debug.Assert(createArrayInstance.Rank > 0); 

+      Bpl.Expr lengthExpr = Bpl.Expr.Literal(1);

+      foreach (IExpression expr in createArrayInstance.Sizes) {

+        this.Visit(expr);

+        lengthExpr = Bpl.Expr.Mul(lengthExpr, TranslatedExpressions.Pop());

+      }

+      

+      // First generate an Alloc() call

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

+      Bpl.Expr assumeExpr = Bpl.Expr.Eq(new Bpl.NAryExpr(cloc, new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(Bpl.Expr.Ident(a))), lengthExpr);

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.AssumeCmd(cloc, assumeExpr));

+      TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

     

     public override void Visit(ICreateDelegateInstance createDelegateInstance)

@@ -898,18 +912,6 @@ namespace BytecodeTranslator
       TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);

     }

 

-    private void TranslateArrayCreation(IExpression creationAST)

-    {

-      Bpl.IToken cloc = creationAST.Token();

-

-      var a = this.sink.CreateFreshLocal(creationAST.Type);

-

-      // First generate an Alloc() call

-      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

-

-      TranslatedExpressions.Push(Bpl.Expr.Ident(a));

-    }

-

     private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)

     {

       var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;

@@ -1287,9 +1289,7 @@ namespace BytecodeTranslator
     public override void Visit(IVectorLength vectorLength) {

       base.Visit(vectorLength.Vector);

       var e = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(

-        Bpl.Expr.Select(new Bpl.IdentifierExpr(vectorLength.Token(), this.sink.Heap.ArrayLengthVariable), new Bpl.Expr[] { e })

-        );

+      TranslatedExpressions.Push(new Bpl.NAryExpr(vectorLength.Token(), new Bpl.FunctionCall(this.sink.Heap.ArrayLengthFunction), new Bpl.ExprSeq(e)));

     }

 

     #endregion

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 7ab72e82..28964c15 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -63,6 +63,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
 axiom (forall t: Type :: $DynamicType($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;

@@ -71,6 +72,17 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
 {

   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 Sink sink;

@@ -87,7 +99,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
         this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());

         this.RefType = new Bpl.CtorType(this.RefTypeDecl.tok, this.RefTypeDecl, new Bpl.TypeSeq());

         this.RealType = new Bpl.CtorType(this.RealTypeDecl.tok, this.RealTypeDecl, new Bpl.TypeSeq());

-      }

+      } 

       return b;

     }

 

@@ -225,7 +237,17 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
 {

   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 Sink sink;

 

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 6d03ef9f..004d4224 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -68,8 +68,8 @@ namespace BytecodeTranslator {
   {

     [RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Box;")]

     public Bpl.Variable ArrayContentsVariable = null;

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

-    public Bpl.Variable ArrayLengthVariable = null;

+    [RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]

+    public Bpl.Function ArrayLengthFunction = null;

 

     public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);