Chalice: add pre-conditions to specification statements; semantically spec statement is just like a call statement now

6 files changed, 29 insertions, 14 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 570a527c..5ca0f98a 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -197,7 +197,7 @@ case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expr
   var locals = List[Variable]()

   var m: Method = null

 }

-case class SpecStmt(lhs: List[VariableExpr], locals:List[Variable], expr: Expression) extends Statement

+case class SpecStmt(lhs: List[VariableExpr], locals:List[Variable], pre: Expression, post: Expression) extends Statement

 case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

 case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement

 case class Unshare(obj: Expression) extends Statement

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 449db023..3f2a7e43 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -59,7 +59,7 @@ object Chalice {
    " [-boogie:path]" +

    " [-defaults:int]" +

    " [<boogie option>]*" +

-   " <file.chalice>";

+   " <file.chalice>*";

 

    for (a <- args) {

      if (options contains a) options(a)()

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index d04746bc..101d6eb0 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -231,7 +231,10 @@ class Parser extends StandardTokenParsers {
         val lhs = for ((id, _) <- decls) yield {

           val v = VariableExpr(id.v); v.pos = id.pos; v

         }

-        "[" ~> expression <~ "]" <~ Semi ^^ {e => SpecStmt(lhs, locals, e)};

+        "[" ~> opt(expression <~ ",") ~ expression <~ "]" <~ Semi ^^ {

+          case Some(pre) ~ post => SpecStmt(lhs, locals, pre, post)

+          case None ~ post => SpecStmt(lhs, locals, BoolLiteral(true), post)

+        };

      } })

     | idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {

         case (id,optT) ~ rhs =>

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 6f99db2c..5ec898c5 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -95,7 +95,7 @@ object PrintProgram {
       print(id + ": " + t.FullName)

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

       println(Semi)

-    case SpecStmt(lhs, locals, expr) =>

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

       if (locals.size > 0) {

         if (locals(0).IsGhost) print("ghost ");

         if (locals(0).IsImmutable) print("const ") else print("var ")

@@ -108,7 +108,7 @@ object PrintProgram {
           if (first) first = false else print(", ");

           print(l.id);

         }

-      print(" ["); Expr(expr); print("]"); println(Semi);

+      print(" ["); Expr(pre); print(", "); Expr(post); print("]"); println(Semi);

     case Call(_, outs, obj, id, args) =>

       print("call ")

       outs match {

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index c1740c61..360146f5 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -277,7 +277,8 @@ object Resolver {
            if (v.v != null && !s.locals.contains(v.v) && v.v.IsImmutable)

              context.Error(s.pos, "Immutable variable cannot be updated by a spec statement: " + v.id);           

          }

-         ResolveExpr(s.expr, ctx, true, true)(false)

+         ResolveExpr(s.pre, ctx, false, true)(false)

+         ResolveExpr(s.post, ctx, true, true)(false)

        case s =>

          ResolveStmt(s, ctx)

      }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index aae392fd..cf9c422e 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -429,14 +429,8 @@ class Translator {
           //update the local, provided a rhs was provided

           case None => Nil

           case Some(rhs) => translateStatement(Assign(new VariableExpr(lv.v), rhs)) }}

-      case SpecStmt(lhs, locals, expr) =>

-        locals.flatMap(v => translateLocalVarDecl(v, true)) :::

-        Comment("spec statement") ::

-        lhs.map(l => Boogie.Havoc(l)) :::

-        isDefined(expr) :::

-        bassume(expr)

-      case c: Call =>

-        translateCall(c)

+      case s: SpecStmt => translateSpecStmt(s)

+      case c: Call => translateCall(c)

       case Install(obj, lowerBounds, upperBounds) =>

         Comment("install") ::

         isDefined(obj) :::

@@ -865,6 +859,23 @@ class Translator {
     etran.Heap.store(o, "rdheld", false)

   }

 

+  def translateSpecStmt(s: SpecStmt): List[Stmt] = {

+    val preGlobals = etran.FreshGlobals("pre")

+

+    // declare new local variables

+    s.locals.flatMap(v => translateLocalVarDecl(v, true)) :::

+    Comment("spec statement") ::

+    (for (v <- preGlobals) yield BLocal(v)) :::

+    // remember values of globals

+    (for ((o,g) <- preGlobals zip etran.Globals) yield (new Boogie.VarExpr(o) := g)) :::

+    // exhale preconditions

+    etran.Exhale(List((s.pre, ErrorMessage(s.pos, "The specification statement precondition at " + s.pos + " might not hold."))), "precondition", true) :::

+    // havoc locals

+    (s.lhs.map(l => Boogie.Havoc(l))) :::

+    // inhale postconditions (using the state before the call as the "old" state)

+    etran.FromPreGlobals(preGlobals).Inhale(List(s.post), "postcondition", true)

+  }

+

   def translateCall(c: Call): List[Stmt] = {

     val obj = c.obj;

     val lhs = c.lhs;