diff options
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 32 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 24 | ||||
-rw-r--r-- | 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<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);
|