Chalice: fix a bug where output variables of a method were not decoupled.

4 files changed, 59 insertions, 36 deletions

diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index 42767bfd..8bd8a24b 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -1,44 +1,45 @@
 Processing LoopSqRoot.chalice
-

-Boogie program verifier finished with 9 verified, 0 errors

+
+Boogie program verifier finished with 9 verified, 0 errors
 Processing RecSqRoot.chalice
-

-Boogie program verifier finished with 11 verified, 0 errors

+
+Boogie program verifier finished with 11 verified, 0 errors
 Processing SpecStmt.chalice
-  12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.

-  25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.

-  33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.

-

-Boogie program verifier finished with 4 verified, 3 errors

+  12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true.
+  25.5: Assertion might not hold. The expression at 25.12 might not evaluate to true.
+  33.5: Assertion might not hold. The expression at 33.12 might not evaluate to true.
+
+Boogie program verifier finished with 4 verified, 3 errors
 Processing SumCubes.chalice
-

-Boogie program verifier finished with 6 verified, 0 errors

+
+Boogie program verifier finished with 6 verified, 0 errors
 Processing TestTransform.chalice
-

-Boogie program verifier finished with 10 verified, 0 errors

+
+Boogie program verifier finished with 10 verified, 0 errors
 Processing TestRefines.chalice
-

-Boogie program verifier finished with 9 verified, 0 errors

+  28.5: Refinement may produce different value for pre-state local variable: c
+
+Boogie program verifier finished with 14 verified, 1 error
 Processing RecFiniteDiff.chalice
-

-Boogie program verifier finished with 9 verified, 0 errors

+
+Boogie program verifier finished with 9 verified, 0 errors
 Processing LoopFiniteDiff.chalice
-

-Boogie program verifier finished with 12 verified, 0 errors

+
+Boogie program verifier finished with 12 verified, 0 errors
 Processing Pick.chalice
-  26.25: Sequence index might be larger than or equal to the length of the sequence.

-

-Boogie program verifier finished with 11 verified, 1 error

+  26.25: Sequence index might be larger than or equal to the length of the sequence.
+
+Boogie program verifier finished with 11 verified, 1 error
 Processing TestCoupling.chalice
-  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.

-  62.38: Location might not be readable.

-  66.5: Location might not be writable

-

-Boogie program verifier finished with 17 verified, 3 errors

+  35.13: The postcondition at 35.13 might not hold. Insufficient fraction at 35.13 for A1.y.
+  62.38: Location might not be readable.
+  66.5: Location might not be writable
+
+Boogie program verifier finished with 17 verified, 3 errors
 Processing Calculator.chalice
-

-Boogie program verifier finished with 15 verified, 0 errors

+
+Boogie program verifier finished with 15 verified, 0 errors
 Processing AngelicExec.chalice
-  14.5: Refinement may produce different value for a declared local variable: x

-

-Boogie program verifier finished with 11 verified, 1 error

+  14.5: Refinement may produce different value for a declared local variable: x
+
+Boogie program verifier finished with 11 verified, 1 error
diff --git a/Chalice/refinements/TestRefines.chalice b/Chalice/refinements/TestRefines.chalice
index 2cfc19b2..3081eb90 100644
--- a/Chalice/refinements/TestRefines.chalice
+++ b/Chalice/refinements/TestRefines.chalice
@@ -9,5 +9,22 @@ class A {
 class B refines C {}
 class C refines D {}
 class D refines A {
-  transforms m(i:int) returns (j:int, k:int) {*} 
+  transforms m(i:int) returns (j:int, k:int) 
+  {
+  *
+  } 
+}
+
+class X {
+  method m() returns (c: bool) 
+  {
+    c := true;
+  }
+}
+
+class Y refines X {
+  refines m() returns (c: bool, d: bool)
+  {
+    c := false;
+  }
 }
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index edeb52ba..bd524ec3 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -260,11 +260,16 @@ case class SeqPat(pats: List[Transform]) extends Transform {
 case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends Statement {

   if (con.size > 0) pos = con.first.pos

   // local variables in context at the beginning of the block

+

   var before: List[Variable] = null

   // shared declared local variables (mapping between abstract and concrete)

+  // should be called after resolution

   lazy val during: (List[Variable], List[Variable]) = {

-    val a = for (v <- abs.flatMap(s => s.Declares)) yield v;

-    val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v).get

+    val a = abs.flatMap(s => s.Declares);

+    val c = for (v <- a) yield con.flatMap(s => s.Declares).find(_ == v) match {

+      case Some(w) => w;

+      case None => v;

+    }

     (a,c)

   }         

   override def Declares = con flatMap {_.Declares}

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 7ccfe7e3..0c4ae979 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -1127,7 +1127,7 @@ object Resolver {
        }

      }

    }

-   resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), Nil)

+   resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), mt.refines.Outs)

  }

 

  def ResolveCouplingInvariant(ci: CouplingInvariant, cl: Class, context: ProgramContext) {