Trying to fix the bound expression simplifier.

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;