From f90a2fd212c8e4893b37aa9bfa5e6ed70d882702 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 17 May 2011 23:01:04 -0700 Subject: Fixed array construction Added a couple more stubs --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 32 +++++++++++++-------------- BCT/BytecodeTranslator/Heap.cs | 24 +++++++++++++++++++- BCT/BytecodeTranslator/HeapFactory.cs | 4 ++-- 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 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); -- cgit v1.2.3