diff options
author | 2011-05-12 10:09:55 -0700 | |
---|---|---|
committer | 2011-05-12 10:09:55 -0700 | |
commit | d608e9c2390fbd5e3e49685d5dd9fdeaeccf8f5a (patch) | |
tree | 414b504b8d36136731d862d4e8c888db2fe3efc1 | |
parent | 0a0f91fdc3ce6917e9ceaec54de72cc19b1e480a (diff) |
Trying to fix the bound expression simplifier.
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 131 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 2 | ||||
-rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 24 | ||||
-rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 24 |
4 files changed, 129 insertions, 52 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 7dbf8d0f..e4f8d1ff 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -644,17 +644,23 @@ namespace BytecodeTranslator Contract.Assert(TranslatedExpressions.Count == 0);
#region Transform Right Hand Side ...
- this.Visit(assignment.Source);
- Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();
+ // Simplify the RHS so that all nested dereferences and method calls are broken
+ // up into separate assignments to locals.
+ var sourceExpression = ExpressionSimplifier.Simplify(this.sink, assignment.Source);
+ this.Visit(sourceExpression);
+ var sourceexp = this.TranslatedExpressions.Pop();
#endregion
// Simplify the LHS so that all nested dereferences and method calls are broken
// up into separate assignments to locals.
- var blockExpression = AssignmentSimplifier.Simplify(this.sink, assignment.Target);
- foreach (var s in blockExpression.BlockStatement.Statements) {
- this.StmtTraverser.Visit(s);
- }
- var target = blockExpression.Expression as ITargetExpression;
+ var targetExpression = ExpressionSimplifier.Simplify(this.sink, assignment.Target);
+ //var targetBlockExpression = targetExpression as IBlockExpression;
+ //if (targetBlockExpression != null){
+ //foreach (var s in targetBlockExpression.BlockStatement.Statements) {
+ // this.StmtTraverser.Visit(s);
+ //}
+
+ var target = targetExpression as ITargetExpression;
List<IFieldDefinition> args = null;
Bpl.Expr arrayExpr = null;
@@ -1198,71 +1204,108 @@ namespace BytecodeTranslator /// <summary>
/// This is a rewriter so it must be used on a mutable Code Model!!!
/// </summary>
- private class AssignmentSimplifier : CodeRewriter {
+ private class ExpressionSimplifier : CodeRewriter {
Sink sink;
- private List<IStatement> localDeclarations = new List<IStatement>();
- private AssignmentSimplifier(Sink sink)
+ private ExpressionSimplifier(Sink sink)
: base(sink.host) {
this.sink = sink;
}
- public static IBlockExpression Simplify(Sink sink, ITargetExpression targetExpression) {
- var a = new AssignmentSimplifier(sink);
- var leftOverExpression = a.Rewrite(targetExpression);
- return new BlockExpression() {
- BlockStatement = new BlockStatement() { Statements = a.localDeclarations, },
- Expression = leftOverExpression,
- Type = targetExpression.Type,
- };
+ public static IExpression Simplify(Sink sink, IExpression expression) {
+ var a = new ExpressionSimplifier(sink);
+ return a.Rewrite(expression);
}
public override IExpression Rewrite(IBoundExpression boundExpression) {
if (boundExpression.Instance == null)
return base.Rewrite(boundExpression); // REVIEW: Maybe just stop the rewriting and return boundExpression?
+ var thisInst = boundExpression.Instance as IThisReference;
+ if (thisInst != null) return boundExpression;
+ var p = boundExpression.Instance as IParameterDefinition;
+ if (p != null) return boundExpression;
+ var existingLocal = boundExpression.Instance as ILocalDefinition;
+ if (existingLocal != null) return boundExpression;
+
var e = base.Rewrite(boundExpression);
boundExpression = e as IBoundExpression;
if (boundExpression == null) return e;
+
var loc = new LocalDefinition() {
- Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()), // TODO: should make the name unique within the method containing the assignment
+ Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),
Type = boundExpression.Type,
};
- this.localDeclarations.Add(
- new LocalDeclarationStatement() {
- InitialValue = boundExpression,
- LocalVariable = loc,
- }
- );
- return new BoundExpression() {
- Definition = loc,
- Instance = null,
+ var locDecl = new LocalDeclarationStatement() {
+ InitialValue = boundExpression,
+ LocalVariable = loc,
+ };
+ return new BlockExpression() {
+ BlockStatement = new BlockStatement() {
+ Statements = new List<IStatement>{ locDecl },
+ },
+ Expression = new BoundExpression() {
+ Definition = loc,
+ Instance = null,
+ Type = boundExpression.Type,
+ },
Type = boundExpression.Type,
};
+
}
- public override IExpression Rewrite(IMethodCall methodCall) {
+ public override ITargetExpression Rewrite(ITargetExpression targetExpression) {
+ var be = targetExpression.Instance as IBoundExpression;
+ if (be == null) return targetExpression;
- var e = base.Rewrite(methodCall); // simplify anything deeper in the tree
- methodCall = e as IMethodCall;
- if (methodCall == null) return e;
+ var e = this.Rewrite(be);
var loc = new LocalDefinition() {
- Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment
- Type = methodCall.Type,
+ Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),
+ Type = be.Type,
};
- this.localDeclarations.Add(
- new LocalDeclarationStatement() {
- InitialValue = methodCall,
- LocalVariable = loc,
- }
- );
- return new BoundExpression() {
- Definition = loc,
- Instance = null,
- Type = methodCall.Type,
+ var locDecl = new LocalDeclarationStatement() {
+ InitialValue = e,
+ LocalVariable = loc,
+ };
+ return new TargetExpression() {
+ Definition = targetExpression.Definition,
+ Instance = new BlockExpression() {
+ BlockStatement = new BlockStatement() {
+ Statements = new List<IStatement> { locDecl, },
+ },
+ Expression = new BoundExpression() {
+ Definition = loc,
+ Instance = null,
+ },
+ Type = loc.Type,
+ },
+ Type = targetExpression.Type,
};
}
+
+ //public override IExpression Rewrite(IMethodCall methodCall) {
+
+ // var e = base.Rewrite(methodCall); // simplify anything deeper in the tree
+ // methodCall = e as IMethodCall;
+ // if (methodCall == null) return e;
+
+ // var loc = new LocalDefinition() {
+ // Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment
+ // Type = methodCall.Type,
+ // };
+ // this.localDeclarations.Add(
+ // new LocalDeclarationStatement() {
+ // InitialValue = methodCall,
+ // LocalVariable = loc,
+ // }
+ // );
+ // return new BoundExpression() {
+ // Definition = loc,
+ // Instance = null,
+ // Type = methodCall.Type,
+ // };
+ //}
}
}
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 283a59a3..f38e0093 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -39,6 +39,7 @@ var $Heap: HeapType; var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
+ free ensures x != null;
modifies $Alloc;
{
assume $Alloc[x] == false && x != null;
@@ -175,6 +176,7 @@ type HeapType = [Ref,Field]Box; var $Alloc: [Ref] bool;
procedure {:inline 1} Alloc() returns (x: Ref)
+ free ensures x != null;
modifies $Alloc;
{
assume $Alloc[x] == false && x != null;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 98d25303..430474d2 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -5,8 +5,6 @@ type Struct = [Field]Box; type HeapType = [Ref,Field]Box;
-function IsGoodHeap(HeapType) : bool;
-
var $Alloc: [Ref]bool;
procedure {:inline 1} Alloc() returns (x: Ref);
@@ -17,7 +15,7 @@ procedure {:inline 1} Alloc() returns (x: Ref); implementation Alloc() returns (x: Ref)
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
@@ -29,10 +27,18 @@ 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 DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
@@ -190,7 +196,7 @@ implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) -var $Heap: HeapType where IsGoodHeap($Heap);
+var $Heap: HeapType;
function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Box
{
@@ -220,6 +226,8 @@ type Type; const unique $DefaultStruct: Struct;
+type Real;
+
function Box2Int(Box) : int;
function Box2Bool(Box) : bool;
@@ -228,6 +236,8 @@ function Box2Struct(Box) : Struct; function Box2Ref(Box) : Ref;
+function Box2Real(Box) : Real;
+
function Int2Box(int) : Box;
function Bool2Box(bool) : Box;
@@ -236,12 +246,18 @@ function Struct2Box(Struct) : Box; function Ref2Box(Ref) : Box;
+function Real2Box(Real) : Box;
+
function Struct2Ref(Struct) : Ref;
function Int2Ref(int) : Ref;
function Bool2Ref(bool) : Ref;
+function Int2Real(int, Type, Type) : Real;
+
+function Real2Int(Real, Type, Type) : Real;
+
function $DynamicType(Ref) : Type;
function $TypeOf(Type) : Ref;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 6e450f38..629a241c 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -5,9 +5,7 @@ type Struct = [Field]Box; type HeapType = [Ref,Field]Box;
-var $Heap: HeapType where IsGoodHeap($Heap);
-
-function IsGoodHeap(HeapType) : bool;
+var $Heap: HeapType;
var $Alloc: [Ref]bool;
@@ -19,7 +17,7 @@ procedure {:inline 1} Alloc() returns (x: Ref); implementation Alloc() returns (x: Ref)
{
- assume $Alloc[x] == false;
+ assume $Alloc[x] == false && x != null;
$Alloc[x] := true;
}
@@ -31,10 +29,18 @@ 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 DelegateAdd(a: Ref, b: Ref) returns (c: Ref);
@@ -210,6 +216,8 @@ type Type; const unique $DefaultStruct: Struct;
+type Real;
+
function Box2Int(Box) : int;
function Box2Bool(Box) : bool;
@@ -218,6 +226,8 @@ function Box2Struct(Box) : Struct; function Box2Ref(Box) : Ref;
+function Box2Real(Box) : Real;
+
function Int2Box(int) : Box;
function Bool2Box(bool) : Box;
@@ -226,12 +236,18 @@ function Struct2Box(Struct) : Box; function Ref2Box(Ref) : Box;
+function Real2Box(Real) : Box;
+
function Struct2Ref(Struct) : Ref;
function Int2Ref(int) : Ref;
function Bool2Ref(bool) : Ref;
+function Int2Real(int, Type, Type) : Real;
+
+function Real2Int(Real, Type, Type) : Real;
+
function $DynamicType(Ref) : Type;
function $TypeOf(Type) : Ref;
|