Chalice:

* support multi-step refinement (convert refinement blocks into normal sequences of statements)
* added tests

9 files changed, 108 insertions, 44 deletions

diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
new file mode 100644
index 00000000..52a7d06b
--- /dev/null
+++ b/Chalice/refinements/Answer
@@ -0,0 +1,21 @@
+Processing LoopSqRoot.chalice
+

+Boogie program verifier finished with 9 verified, 0 errors

+Processing RecSqRoot.chalice
+

+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

+Processing SumCubes.chalice
+

+Boogie program verifier finished with 6 verified, 0 errors

+Processing TestTransform.chalice
+

+Boogie program verifier finished with 10 verified, 0 errors

+Processing TestRefines.chalice
+

+Boogie program verifier finished with 9 verified, 0 errors

diff --git a/Chalice/refinements/LoopSqRoot.chalice b/Chalice/refinements/LoopSqRoot.chalice
index e14fe4d6..4ea9434d 100644
--- a/Chalice/refinements/LoopSqRoot.chalice
+++ b/Chalice/refinements/LoopSqRoot.chalice
@@ -27,25 +27,17 @@ class A1 refines A0 {
     }
   }
 }
-/*
-  method compute2(n: int) returns (x: int)
-    requires n >= 0;
-  { 
-    var l := 0;
-    var r := n + 1;
-    while (l + 1 != r)
-      invariant l >= 0 && r > l;
-      invariant l*l <= n && n < r*r;
-    {
-      var p [2*p <= l+r && l+r < 2*(p+1)];
-      assert l < p && p < r;
-      if (p*p <= n) {
-        l := p;
-      } else {
-        r := p;
+
+class A2 refines A1 {
+  transforms sqroot(n) returns (x)
+  {
+    _
+    while {
+      replaces k by {
+        var k [2*k <= l+r && l+r < 2*(k+1)]        
       }
+      *
     }
-    // no need to reverify
+    _
   }
 }
-*/
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
new file mode 100644
index 00000000..9cc84d90
--- /dev/null
+++ b/Chalice/refinements/test.sh
@@ -0,0 +1,29 @@
+#!/usr/bin/bash
+
+TESTS="
+  LoopSqRoot.chalice
+  RecSqRoot.chalice
+  SpecStmt.chalice
+  SumCubes.chalice
+  TestTransform.chalice
+  TestRefines.chalice
+"
+if [ -f Output ]
+then
+  rm -f Output
+fi
+
+for f in $TESTS 
+do
+  echo "Processing $f" | tee -a Output
+  scala -cp ../bin chalice.Chalice -nologo $f >> Output 2>&1
+done
+
+if diff Output Answer
+then
+  echo Success
+else
+  echo Failure
+fi
+
+  
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 8059284c..cbb2ac85 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -190,10 +190,25 @@ sealed abstract class Refinement(id: String) extends Callable(id) {
 case class MethodTransform(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], trans: Transform) extends Refinement(id) {

   var body = null:List[Statement];

   def Spec = {assert(refines != null); refines.Spec ++ spec}

-  def Body = {assert(body != null); body}   // TODO: get rid of refinement blocks (that is make sure variables match)

+  def Body = {

+    assert(body != null);

+    // make sure the body appears as if it is from a normal method

+    def concretize(ss: List[Statement]): List[Statement] = ss flatMap {

+      case r @ RefinementBlock(con, abs) =>

+        con :::

+        (for ((a,c) <- (r.during._1 zip r.during._2)) yield LocalVar(a, Some(new VariableExpr(c))))

+      case BlockStmt(ss) => List(BlockStmt(concretize(ss)))

+      case IfStmt(guard, BlockStmt(thn), None) => List(IfStmt(guard, BlockStmt(concretize(thn)), None))

+      case IfStmt(guard, BlockStmt(thn), Some(els)) => List(IfStmt(guard, BlockStmt(concretize(thn)), Some(BlockStmt(concretize(List(els))))))

+      case WhileStmt(guard, oi, ni, lks, BlockStmt(ss)) => List(WhileStmt(guard, oi ++ ni, Nil, lks, BlockStmt(concretize(ss))))

+      case s => List(s)

+    }

+    concretize(body)

+  }

   def Ins = {assert(refines != null); refines.Ins}

   def Outs = {assert(refines != null); refines.Outs ++ outs.drop(refines.Outs.size)}

 }

+

 sealed abstract class Transform extends ASTNode

 /** Pattern matching within a block (zero or more) over deterministic statements */

 case class BlockPat() extends Transform {

@@ -226,7 +241,14 @@ 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;

-  var locals: List[Variable] = null;

+  // existing local variables before the block

+  var before: List[Variable] = null;

+  // shared declared local variables

+  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

+    (a,c)

+  }         

   override def Declares = con flatMap {_.Declares}

 }

 

@@ -257,8 +279,7 @@ case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement {
   override def Targets = if (lhs.v != null) Set(lhs.v) else Set()

 }

 case class FieldUpdate(lhs: MemberAccess, rhs: RValue) extends Statement

-case class LocalVar(id: String, t: Type, const: Boolean, ghost: Boolean, rhs: Option[RValue]) extends Statement {

-  val v = new Variable(id, t, ghost, const);

+case class LocalVar(v: Variable, rhs: Option[RValue]) extends Statement {

   override def Declares = List(v)

   override def Targets = rhs match {case None => Set(); case Some(_) => Set(v)}

 }

@@ -520,7 +541,7 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[
 

 object AST {

   /**

-   * Flattens sequences of transforms and merges consecutive blocks

+   * Flattens sequences of transforms and merges consecutive block patterns

    */

   def normalize(trans: Transform): Transform = trans match {

     case IfPat(thn, Some(els)) => IfPat(normalize(thn), Some(normalize(els)))

@@ -548,7 +569,7 @@ object AST {
   /**

    * Matches a proper block to a transform.

    * Effects: some statements might be replaced by refinements blocks; Loops might have new invariants.

-   * Requires: in transform, a sequence pattern should not contain a sequence pattern.

+   * Requires: transform is normalized

    */

   def refine:(List[Statement], Transform) => TransformMatch = {

     // order is important!

diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 98258e97..21c9bd0c 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -106,9 +106,9 @@ class ChaliceToCSharp {
       case BlockStmt(ss) => indent + "{" + nl + (indentMore { rep(ss map convertStatement) }) + indent + "}" + nl

       case IfStmt(guard, thn, els) => indent + "if (" + convertExpression(guard) + ")" + nl + convertStatement(thn) + 

         (if(els.isDefined) (indent + "else" + nl + convertStatement(els.get)) else { "" }) + nl

-      case LocalVar(id, tp, const, ghost, rhs) =>

-        indent + convertType(tp) + " " + id + " = " +

-        (if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(tp)) + 

+      case LocalVar(v, rhs) =>

+        indent + convertType(v.t) + " " + v.id + " = " +

+        (if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(v.t)) + 

         ";" + nl

       case FieldUpdate(MemberAccess(target, f), rhs) =>

         indent + convertExpression(target) + "." + f + " = " + convertExpression(rhs) + ";" + nl

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index bffcfb00..b8390405 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -256,7 +256,7 @@ class Parser extends StandardTokenParsers {
     | idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {

         case (id,optT) ~ rhs =>

           currentLocalVariables = currentLocalVariables + id.v

-          LocalVar(id.v,

+          val v = Variable(id.v,

                    optT match {

                      case Some(t) => t

                      case None =>

@@ -267,8 +267,8 @@ class Parser extends StandardTokenParsers {
                          case Some(x:BinaryExpr) if x.ResultType != null => new Type(x.ResultType);

                          case _ => Type("int", Nil)

                        }

-                   },

-                   const, ghost, rhs) }

+                   }, ghost, const)

+          LocalVar(v, rhs) }

     )

   def ifStmtThen: Parser[IfStmt] =

     "(" ~> expression ~ ")" ~ blockStatement ~ ("else" ~> ifStmtElse ?) ^^ {

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 6a408b45..30cfb66f 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -89,10 +89,14 @@ object PrintProgram {
       }

     case w @ WhileStmt(guard, _, _, lkch, body) =>

       print("while ("); Expr(guard); println(")")

-      for (inv <- w.Invs) {

+      for (inv <- w.oldInvs) {

         Spaces(indent+2)

         print("invariant "); Expr(inv); println(Semi)

       }

+      for (inv <- w.newInvs) {

+        Spaces(indent+2)

+        print("invariant "); Expr(inv); print(" // refined"); println(Semi)

+      }

       for (l <- lkch) {

         Spaces(indent+2)

         print("lockchange "); Expr(l); println(Semi)

@@ -102,10 +106,8 @@ object PrintProgram {
       Expr(lhs); print(" := "); Rhs(rhs); println(Semi)

     case FieldUpdate(lhs,rhs) =>

       Expr(lhs); print(" := "); Rhs(rhs); println(Semi)

-    case LocalVar(id,t,c,g,rhs) =>

-      if (g) print("ghost ")

-      if (c) print("const ") else print("var ")

-      print(id + ": " + t.FullName)

+    case LocalVar(v,rhs) =>

+      print(v + ": " + v.t.FullName)

       rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }

       println(Semi)

     case SpecStmt(lhs, locals, pre, post) =>

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index e50cc7ab..9a0b830d 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -291,14 +291,14 @@ object Resolver {
    case BlockStmt(ss) =>

      var ctx = context

      for (s <- ss) s match {

-       case l @ LocalVar(id, t, c, g, rhs) =>

-         ResolveType(l.v.t, ctx)

+       case l @ LocalVar(v, rhs) =>

+         ResolveType(v.t, ctx)

          val oldCtx = ctx

-         ctx = ctx.AddVariable(l.v)

+         ctx = ctx.AddVariable(v)

          rhs match {

            case None =>

            case Some(rhs) =>

-             val lhs = VariableExpr(id)

+             val lhs = VariableExpr(v.id)

              lhs.pos = l.pos;

              ResolveExpr(lhs, ctx, false, false)(false)

              ResolveAssign(lhs, rhs, oldCtx)

@@ -1097,7 +1097,7 @@ object Resolver {
        s match {

          case r @ RefinementBlock(c, a) =>

            // abstract globals available at this point in the program

-           r.locals = locals

+           r.before = locals

            ResolveStmt(BlockStmt(c), ctx)

            val vs = c flatMap {s => s.Declares};

            for (v <- a flatMap {s => s.Declares}; if (! vs.contains(v)))

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index f4fd1108..1ae56ca2 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -347,7 +347,7 @@ class Translator {
           DefinePreInitialState :::

           Inhale(Preconditions(mt.Spec), "precondition") :::

           DefineInitialState :::

-          translateStatements(mt.Body) :::

+          translateStatements(mt.body) :::

           Exhale(Postconditions(mt.refines.Spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "postcondition") :::

           tag(

             Exhale(Postconditions(mt.spec) map {p => (p, ErrorMessage(p.pos, "The postcondition at " + p.pos + " might not hold."))}, "refinement postcondition"),

@@ -1040,10 +1040,9 @@ class Translator {
     val conGlobals = etran.FreshGlobals("concrete")

     val conTran = new ExpressionTranslator(conGlobals map {v => new VarExpr(v)}, etran.oldEtran.Globals, currentClass);

     // shared locals before block (excluding immutable)

-    val before = for (v <- r.locals; if (! v.isImmutable)) yield v;

+    val before = for (v <- r.before; if (! v.isImmutable)) yield v;

     // shared locals in block

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

-    val duringC = for (v <- duringA) yield r.con.flatMap(s => s.Declares).find(_ == v).get

+    val (duringA, duringC) = r.during;

     // save locals before (to restore for abstract block)

     val beforeV = for (v <- before) yield new Variable(v.id, v.t)

     // save locals after (to compare with abstract block)