Chalice: add specification statement ( ghost? (const|var) (x (:T)?)+ [P(x)] )

5 files changed, 83 insertions, 48 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 4f63f57b..570a527c 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -147,25 +147,23 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci
   var SCC: List[Function] = Nil;

 }

 case class Condition(id: String, where: Option[Expression]) extends NamedMember(id)

-class Variable(name: String, typ: Type) extends ASTNode {

+class Variable(name: String, typ: Type, isGhost: Boolean, isImmutable: Boolean) extends ASTNode {

   val id = name

   val t = typ

-  val IsGhost: Boolean = false

-  val IsImmutable: Boolean = false

+  val IsGhost = isGhost

+  val IsImmutable = isImmutable

   val UniqueName = {

     val n = Variable.VariableCount

     Variable.VariableCount = Variable.VariableCount + 1

     name + "#" + n

   }

+  def this(name: String, typ: Type) = this(name,typ,false,false);

+  override def toString = (if (IsGhost) "ghost " else "") + (if (IsImmutable) "const " else "var ") + id;

 }

 object Variable { var VariableCount = 0 }

-class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {

-  override val IsImmutable: Boolean = true

-}

-class SpecialVariable(name: String, typ: Type) extends Variable(name, typ) {

+class SpecialVariable(name: String, typ: Type) extends Variable(name, typ, false, false) {

   override val UniqueName = name

 }

-

 sealed abstract class Specification extends ASTNode

 case class Precondition(e: Expression) extends Specification

 case class Postcondition(e: Expression) extends Specification

@@ -193,19 +191,13 @@ case class WhileStmt(guard: Expression,
 case class Assign(lhs: VariableExpr, rhs: RValue) extends Statement

 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 =

-    if (const)

-      new ImmutableVariable(id, t){override val IsGhost = ghost}

-    else

-      new Variable(id, t){override val IsGhost = ghost}

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

 }

 case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expression, id: String, args: List[Expression]) extends Statement {

   var locals = List[Variable]()

   var m: Method = null

 }

-case class Spec(declaresLocal: List[Boolean], lhs: List[VariableExpr], pred: Expression) extends Statement {

-  var locals = List[Variable]()

-}

+case class SpecStmt(lhs: List[VariableExpr], locals:List[Variable], expr: 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/Parser.scala b/Chalice/src/Parser.scala
index b57a5ea4..d04746bc 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -65,8 +65,8 @@ class Parser extends StandardTokenParsers {
 

   def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl)

   def fieldDecl =

-        ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, false) }

-        | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, true) }

+        ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }

+        | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }

         )

   def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)

   def methodDecl = {

@@ -95,18 +95,15 @@ class Parser extends StandardTokenParsers {
   def formalList(immutable: Boolean) = repsep(formal(immutable), ",")  

   def formal(immutable: Boolean): Parser[Variable] =

     idType ^^ {case (id,t) =>

-      currentLocalVariables = currentLocalVariables + id;

-      if (immutable) new ImmutableVariable(id,t)

-      else new Variable(id,t) 

+      currentLocalVariables = currentLocalVariables + id.v;

+      new Variable(id.v,t,false,immutable) 

     }

-

   def Ident = positioned(ident ^^ PositionedString)

-  def idType =

-    idTypeOpt ^^ {

+  def idType = idTypeOpt ^^ {

       case (id, None) => (id, Type("int", Nil))

       case (id, Some(t)) => (id, t) }

   def idTypeOpt =

-    ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }

+    Ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }

   def typeDecl: Parser[Type] =

       positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }

       | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }

@@ -138,7 +135,8 @@ class Parser extends StandardTokenParsers {
     | blockStatement ^^ BlockStmt

     | "var" ~> localVarStmt(false, false)

     | "const" ~> localVarStmt(true, false)

-    | "ghost" ~> ( "const" ~> localVarStmt(true, true) | "var" ~> localVarStmt(false, true))

+    | "ghost" ~> "const" ~> localVarStmt(true, true)

+    | "ghost" ~> "var" ~> localVarStmt(false, true)

     | "call" ~> callStmt

     | "if" ~> ifStmtThen

     | "while" ~> "(" ~> expression ~ ")" ~ loopSpec ~ blockStatement ^^ {

@@ -225,10 +223,20 @@ class Parser extends StandardTokenParsers {
           Receive(declareImplicitLocals(lhs), e, lhs) }

     )

   def localVarStmt(const: Boolean, ghost: Boolean) =

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

+    ( (rep1sep(idType, ",") into {decls:List[(PositionedString,Type)] => {

+        val locals = for ((id, t) <- decls; if (! currentLocalVariables.contains(id.v))) yield {

+          currentLocalVariables = currentLocalVariables + id.v

+          new Variable(id.v, t, ghost, const)

+        }

+        val lhs = for ((id, _) <- decls) yield {

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

+        }

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

+     } })

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

         case (id,optT) ~ rhs =>

-          currentLocalVariables = currentLocalVariables + id

-          LocalVar(id,

+          currentLocalVariables = currentLocalVariables + id.v

+          LocalVar(id.v,

                    optT match {

                      case Some(t) => t

                      case None =>

@@ -240,8 +248,8 @@ class Parser extends StandardTokenParsers {
                          case _ => Type("int", Nil)

                        }

                    },

-                   const, ghost, rhs)

-      }

+                   const, ghost, rhs) }

+    )

   def ifStmtThen: Parser[IfStmt] =

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

       case guard ~ _ ~ thenClause ~ elseClause => IfStmt(guard, BlockStmt(thenClause), elseClause) }

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

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

       println(Semi)

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

+      if (locals.size > 0) {

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

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

+      } else

+        print("var ");

+      VarList(locals);

+      var first = (locals.size == 0);

+      for (l <- lhs)

+        if (! locals.exists(v => v.id == l.id)) {

+          if (first) first = false else print(", ");

+          print(l.id);

+        }

+      print(" ["); Expr(expr); 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 7365bfc8..c1740c61 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -6,6 +6,7 @@
 package chalice;

 import scala.util.parsing.input.Position

 import scala.util.parsing.input.Positional

+import collection.mutable.ListBuffer

 

 object Resolver {

  sealed abstract class ResolverOutcome

@@ -268,7 +269,15 @@ object Resolver {
          for (v <- c.locals) { ctx = ctx.AddVariable(v) } 

        case r: Receive =>

          ResolveStmt(r, ctx)

-         for (v <- r.locals) { ctx = ctx.AddVariable(v) } 

+         for (v <- r.locals) { ctx = ctx.AddVariable(v) }

+       case s: SpecStmt =>

+         for (v <- s.locals) { ResolveType(v.t, ctx); ctx = ctx.AddVariable(v) }

+         for (v <- s.lhs) {

+           ResolveExpr(v, ctx, true, true)(false)

+           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)

        case s =>

          ResolveStmt(s, ctx)

      }

@@ -308,7 +317,8 @@ object Resolver {
      ResolveExpr(rhs, context, false, false)(false)

      if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)

      if (! lhs.isPredicate && lhs.f != null && !lhs.f.isGhost) CheckNoGhost(rhs, context)

-   case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")

+   case _:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")

+   case _:SpecStmt => throw new Exception("should have been handled before")

    case c @ Call(declaresLocal, lhs, obj, id, args) =>

      ResolveExpr(obj, context, false, false)(false)

      CheckNoGhost(obj, context)

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index d5ddfdcd..aae392fd 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -390,7 +390,7 @@ class Translator {
         translateWhile(w)

       case Assign(lhs, rhs) =>

         def assignOrAssumeEqual(r: Boogie.Expr): List[Boogie.Stmt] = {

-          if (lhs.v.isInstanceOf[ImmutableVariable]) {

+          if (lhs.v.IsImmutable) {

             // this must be a "ghost const"

             val name = lhs.v.UniqueName

             bassert(! VarExpr("assigned$" + name), lhs.pos, "Const variable can be assigned to only once.") ::

@@ -423,21 +423,18 @@ class Translator {
         isDefined(target) :::

         bassert(CanWrite(target, lhs.f), s.pos, "Location might not be writable") ::

         statements ::: etran.Heap.store(target, lhs.f, toStore) :: bassume(wf(VarExpr(HeapName), VarExpr(MaskName)))

-      case lv @ LocalVar(id, t, const, ghost, rhs) =>

-        val bv = Variable2BVarWhere(lv.v)

-        val isAssignedVar = if (const) new Boogie.BVar("assigned$" + bv.id, BoolClass) else null

-        Comment("local " + (if (ghost) "ghost " else "") + (if (const) "const " else "var ") + id) ::

-        BLocal(bv) :: 

-        { if (const)

-            // havoc x; var assigned$x: bool; assigned$x := false; 

-            Havoc(new Boogie.VarExpr(bv)) ::

-            BLocal(isAssignedVar) :: (new Boogie.VarExpr(isAssignedVar) := false)

-          else

-            List() } :::

-        { rhs match {

+      case lv : LocalVar =>

+        translateLocalVarDecl(lv.v, false) :::

+        { lv.rhs match {

           //update the local, provided a rhs was provided

-          case None => List()

+          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 Install(obj, lowerBounds, upperBounds) =>

@@ -756,6 +753,20 @@ class Translator {
     }

   }

 

+  def translateLocalVarDecl(v: Variable, assignConst: Boolean) = {

+    val bv = Variable2BVarWhere(v)

+    Comment("local " + v) ::

+    BLocal(bv) ::

+    { if (v.IsImmutable) {

+        val isAssignedVar = new Boogie.BVar("assigned$" + bv.id, BoolClass)

+        // havoc x; var assigned$x: bool; assigned$x := false;

+        Havoc(new Boogie.VarExpr(bv)) ::

+        BLocal(isAssignedVar) ::

+        (new Boogie.VarExpr(isAssignedVar) := assignConst)

+      } else

+        Nil }

+  }

+

   def translateAllocation(cl: Class, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression], pos: Position): (Boogie.BVar, List[Boogie.Stmt]) = {

     val (nw, nwe) = NewBVar("nw", cl, true)

     val (ttV,tt) = Boogie.NewTVar("T")

@@ -933,7 +944,7 @@ class Translator {
       (new VariableExpr(sv) := new VariableExpr(v))) :::

     // havoc local-variable loop targets

     (w.LoopTargets :\ List[Boogie.Stmt]()) ( (v,vars) => (v match {

-      case v: ImmutableVariable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))

+      case v: Variable if v.IsImmutable => Boogie.Havoc(Boogie.VarExpr("assigned$" + v.id))

       case _ => Boogie.Havoc(Boogie.VarExpr(v.UniqueName)) }) :: vars) :::

     Boogie.If(null,

     // 1. CHECK  DEFINEDNESS OF INVARIANT