Support for quasihavoc

src/main/scala/viper/silver/ast/Statement.scala

@@ -197,6 +197,34 @@ case class Goto(target: String)(val pos: Position = NoPosition, val info: Info =
   */
 case class LocalVarDeclStmt(decl: LocalVarDecl)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Stmt
 
+/** Quasihavoc statement.
+  * Replaces the quasihavocked resource's snapshot with a fresh snapshot.
+  * The optional lhs provides a guard, under which the resource is quasihavocked. For example,
+  *   quasihavoc c ==> Pred(x)
+  * means that we only quasihavoc Pred(x) if the condition c is true.
+  * The quasihavocall variant of this statement allows one to quasihavoc an unbounded number of resources
+  */
+case class Quasihavoc(lhs: Option[Exp], exp: ResourceAccess)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Stmt {
+  override lazy val check: Seq[ConsistencyError] = {
+    // Sanity checks of properties that should be guaranteed by earlier phases of the front end. These checks
+    // are similar to the ones provided by inhale and exhale statements.
+    (if(!Consistency.noResult(this)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)) else Seq()) ++
+    (if (lhs.nonEmpty && !(lhs.get isSubtype Bool)) Seq(ConsistencyError(s"Left side of quasihavoc implication must be of type Bool, but found ${exp.typ}", exp.pos)) else Seq())
+  }
+}
+
+/** Quasihavocall statement (see quasiavoc statement)
+  * Must extend Scope because it declares quantified variables.
+  */
+case class Quasihavocall(vars: Seq[LocalVarDecl], lhs: Option[Exp], exp: ResourceAccess)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Stmt with Scope {
+  val scopedDecls: Seq[Declaration] = vars
+
+  override lazy val check : Seq[ConsistencyError] = {
+    (if(!Consistency.noResult(this)) Seq(ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)) else Seq()) ++
+    (if (lhs.nonEmpty && !(lhs.get isSubtype Bool)) Seq(ConsistencyError(s"Left side of quasihavocall implication must be of type Bool, but found ${exp.typ}", exp.pos)) else Seq())
+  }
+}
+
 
 /** Generic Statement type to use to extend the AST.
   * New statement-typed AST nodes can be defined by creating new case classes extending this trait.

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -690,6 +690,15 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         text("goto") <+> target
       case LocalVarDeclStmt(decl) =>
         text("var") <+> showVar(decl)
+      case Quasihavoc(lhs, exp) =>
+        text("quasihavoc") <+>
+        (if (lhs.nonEmpty) show(lhs.get) <+> "==>" <> space else nil) <>
+        show(exp)
+      case Quasihavocall(vars, lhs, exp) =>
+        text("quasihavocall") <+>
+        ssep(vars map show, char(',') <> space) <+> "::" <+>
+        (if (lhs.nonEmpty) show(lhs.get) <+> "==>" <> space else nil) <>
+        show(exp)
       case e: ExtensionStmt => e.prettyPrint
       case null => uninitialized
     }

src/main/scala/viper/silver/ast/utility/Nodes.scala

@@ -66,6 +66,8 @@ object Nodes {
           case Label(_, invs) => invs
           case Goto(_) => Nil
           case LocalVarDeclStmt(decl) => Seq(decl)
+          case Quasihavoc(lhs, e) => lhs.toSeq :+ e
+          case Quasihavocall(vars, lhs, e) => vars ++ lhs.toSeq :+ e
           case e: ExtensionStmt => e.extensionSubnodes
         }
       case _: LocalVarDecl => Nil

src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala

@@ -227,7 +227,9 @@ object CfgGenerator {
            _: NewStmt |
            _: Assert |
            _: LocalVarDeclStmt |
-           _: Assume =>
+           _: Assume |
+           _: Quasihavoc |
+           _: Quasihavocall =>
         // handle regular, non-control statements
         addStatement(WrappedStmt(stmt))
       case _: ExtensionStmt =>

src/main/scala/viper/silver/parser/FastParser.scala

@@ -77,7 +77,7 @@ object FastParserCompanion {
     // specifications
     "requires", "ensures", "invariant",
     // statements
-    "fold", "unfold", "inhale", "exhale", "new", "assert", "assume", "package", "apply",
+    "fold", "unfold", "inhale", "exhale", "new", "assert", "assume", "package", "apply", "quasihavoc", "quasihavocall",
     // control flow
     "while", "if", "elseif", "else", "goto", "label",
     // sequences
@@ -786,7 +786,6 @@ class FastParser {
 
   lazy val keywords = FastParserCompanion.basicKeywords | ParserExtension.extendedKeywords
 
-
   // Note that `typedFapp` is before `"(" ~ exp ~ ")"` to ensure that the latter doesn't gobble up the brackets for the former
   // and then look like an `fapp` up untill the `: type` part, after which we need to backtrack all the way back (or error if cut)
   def atom(implicit ctx : P[_]) : P[PExp] = P(ParserExtension.newExpAtStart(ctx) | integer | booltrue | boolfalse | nul | old
@@ -1091,11 +1090,13 @@ class FastParser {
 
   def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | macroassign | fieldassign | localassign | fold | unfold | exhale | assertP |
     inhale | assume | ifthnels | whle | varDecl | defineDecl | newstmt | 
-    methodCall | goto | lbl | packageWand | applyWand | macroref | block | ParserExtension.newStmtAtEnd(ctx))
+    methodCall | goto | lbl | packageWand | applyWand | macroref | block |
+    quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
 
   def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fieldassign | localassign | fold | unfold | exhale | assertP |
     inhale | assume | ifthnels | whle | varDecl | newstmt |
-    methodCall | goto | lbl | packageWand | applyWand | macroref | block | ParserExtension.newStmtAtEnd(ctx))
+    methodCall | goto | lbl | packageWand | applyWand | macroref | block |
+    quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
 
   def macroref[_: P]: P[PMacroRef] = FP(idnuse).map { case (pos, a) => PMacroRef(a)(pos) }
 
@@ -1117,6 +1118,28 @@ class FastParser {
 
   def assume[_: P]: P[PAssume] = FP(keyword("assume") ~/ exp).map{ case (pos, e) => PAssume(e)(pos) }
 
+  // Parsing Havoc statements
+  // Havoc statements have two forms:
+  //    1. havoc <resource>
+  //    2. havoc <exp> ==> <resource>
+  // Note that you cannot generalize (2) to something like "<exp1> ==> <exp2> ==> <resource>".
+  // We therefore forbid the lhs of (2) from being an arbitrary expression. Instead,
+  // we enforce that it's a "magicWandExp", which is one level below an implication expression
+  // in the grammar. Note that it is still possible to express "(<exp1> ==> <exp2>) ==> <resource>
+  // using parentheses.
+
+  // Havocall follows a similar pattern to havoc but allows quantifying over variables.
+
+  def quasihavoc[_: P]: P[PQuasihavoc] = FP(keyword("quasihavoc") ~/
+    (magicWandExp ~ "==>").? ~ exp ).map {
+      case (pos, (lhs, rhs)) => PQuasihavoc(lhs, rhs)(pos)
+  }
+
+  def quasihavocall[_: P]: P[PQuasihavocall] = FP(keyword("quasihavocall") ~/
+    nonEmptyFormalArgList ~ "::" ~ (magicWandExp ~ "==>").? ~ exp).map {
+    case (pos, (vars, lhs, rhs)) => PQuasihavocall(vars, lhs, rhs)(pos)
+  }
+
   def ifthnels[_: P]: P[PIf] = FP("if" ~ "(" ~ exp ~ ")" ~ block ~~~ elsifEls).map {
     case (pos, (cond, thn, ele)) => PIf(cond, thn, ele)(pos)
   }

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -1073,6 +1073,8 @@ case class PTypeVarDecl(idndef: PIdnDef)(val pos: (Position, Position)) extends
 case class PMacroRef(idnuse : PIdnUse)(val pos: (Position, Position)) extends PStmt
 case class PDefine(idndef: PIdnDef, parameters: Option[Seq[PIdnDef]], body: PNode)(val pos: (Position, Position)) extends PStmt with PLocalDeclaration
 case class PSkip()(val pos: (Position, Position)) extends PStmt
+case class PQuasihavoc(lhs: Option[PExp], e: PExp)(val pos: (Position, Position)) extends PStmt
+case class PQuasihavocall(vars: Seq[PFormalArgDecl], lhs: Option[PExp], e: PExp)(val pos: (Position, Position)) extends PStmt with PScope
 
 sealed trait PNewStmt extends PStmt {
   def target: PIdnUse
@@ -1326,6 +1328,8 @@ object Nodes {
       case PAxiom(idndef, exp) => (if (idndef.isDefined) Seq(idndef.get) else Nil) ++ Seq(exp)
       case PTypeVarDecl(name) => Seq(name)
       case PDefine(idndef, optArgs, body) => Seq(idndef) ++ optArgs.getOrElse(Nil) ++ Seq(body)
+      case PQuasihavoc(lhs, e) => lhs.toSeq :+ e
+      case PQuasihavocall(vars, lhs, e) => vars ++ lhs.toSeq :+ e
       case t : PExtender => t.getSubnodes()
       case _: PSkip => Nil
       case _: PUnnamedFormalArgDecl => Nil

src/main/scala/viper/silver/parser/Resolver.scala

@@ -271,12 +271,44 @@ case class TypeChecker(names: NameAnalyser) {
       case _: PDefine =>
         /* Should have been removed right after parsing */
         sys.error(s"Unexpected node $stmt found")
+      case PQuasihavoc(lhs, e) =>
+        checkHavoc(stmt, lhs, e)
+      case havoc@PQuasihavocall(vars, lhs, e) =>
+        vars foreach (v => check(v.typ))
+        // update the curMember, which contains quantified variable information
+        val oldCurMember = curMember
+        curMember = havoc
+        // Actually type check the havoc
+        checkHavoc(stmt, lhs, e)
+        // restore the previous curMember
+        curMember = oldCurMember
+
       case t:PExtender => t.typecheck(this, names).getOrElse(Nil) foreach(message =>
                               messages ++= FastMessaging.message(t, message))
       case _: PSkip =>
     }
   }
 
+  def checkHavoc(stmt: PStmt, lhs: Option[PExp], e: PExp): Unit = {
+    // If there is a condition, make sure that it is a Bool
+    if (lhs.nonEmpty) {
+      check(lhs.get, Bool)
+    }
+    // Make sure that the rhs is a resource
+    val havocError = "Havoc statement must take a field access, predicate, or wand"
+    e match {
+      case _: PFieldAccess => checkTopTyped(e, None)
+      case pc: PCall =>
+        check(e, Bool)
+        // make sure that this is in fact a predicate
+        if (pc.extfunction == null) {
+          messages ++= FastMessaging.message(stmt, havocError)
+        }
+      case _: PMagicWandExp => check(e, Bool)
+      case _ => messages ++= FastMessaging.message(stmt, havocError)
+    }
+  }
+
   def acceptNonAbstractPredicateAccess(exp: PExp, messageIfAbstractPredicate: String): Unit = {
     exp match {
       case PAccPred(PPredicateAccess(_, idnuse), _) =>

src/main/scala/viper/silver/parser/Transformer.scala

@@ -113,6 +113,8 @@ object Transformer {
         case p@PAssert(e) => PAssert(go(e))(p.pos)
         case p@PAssume(e) => PAssume(go(e))(p.pos)
         case p@PInhale(e) => PInhale(go(e))(p.pos)
+        case p@PQuasihavoc(lhs, e) => PQuasihavoc(lhs map go, go(e))(p.pos)
+        case p@PQuasihavocall(vars, lhs, e) => PQuasihavocall(vars map go, lhs map go, go(e))(p.pos)
           // MAPS:
         //case PExplicitMultiset(elems) => PExplicitMultiset(elems map go)
         case p@PEmptyMap(keyType, valueType) => PEmptyMap(go(keyType), go(valueType))(p.pos)

src/main/scala/viper/silver/parser/Translator.scala

@@ -238,12 +238,35 @@ case class Translator(program: PProgram) {
         If(exp(cond), stmt(thn).asInstanceOf[Seqn], stmt(els).asInstanceOf[Seqn])(pos)
       case PWhile(cond, invs, body) =>
         While(exp(cond), invs map exp, stmt(body).asInstanceOf[Seqn])(pos)
+      case PQuasihavoc(lhs, e) =>
+        val (newLhs, newE) = havocStmtHelper(lhs, e)
+        Quasihavoc(newLhs, newE)(pos)
+      case PQuasihavocall(vars, lhs, e) =>
+        val newVars = vars map liftVarDecl
+        val (newLhs, newE) = havocStmtHelper(lhs, e)
+        Quasihavocall(newVars, newLhs, newE)(pos)
       case t: PExtender =>   t.translateStmt(this)
       case _: PDefine | _: PSkip =>
         sys.error(s"Found unexpected intermediate statement $s (${s.getClass.getName}})")
     }
   }
 
+  /** Helper function that translates subexpressions common to a Havoc or Havocall statement */
+  def havocStmtHelper(lhs: Option[PExp], e: PExp): (Option[Exp], ResourceAccess) = {
+    val newLhs = lhs.map(exp)
+    exp(e) match {
+      case exp: FieldAccess => (newLhs, exp)
+      case PredicateAccessPredicate(predAccess, perm) =>
+        // A PrediateAccessPredicate is a PredicateResourceAccess combined with
+        // a Permission. Havoc expects a ResourceAccess. To make types match,
+        // we must extract the PredicateResourceAccess.
+        assert(perm.isInstanceOf[FullPerm])
+        (newLhs, predAccess)
+      case exp: MagicWand => (newLhs, exp)
+      case _ => sys.error("Can't havoc this kind of expression")
+    }
+  }
+
   /** Takes a `PExp` and turns it into an `Exp`. */
   def exp(pexp: PExp): Exp = {
     val pos = pexp

src/main/scala/viper/silver/verifier/VerificationError.scala

@@ -530,6 +530,31 @@ object errors {
   def LetWandFailed(offendingNode: LocalVarAssign): PartialVerificationError =
     PartialVerificationError((reason: ErrorReason) => LetWandFailed(offendingNode, reason))
 
+  case class QuasihavocFailed(offendingNode: Quasihavoc, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
+    val id = "quasihavoc.failed"
+    val text = "Quasihavoc might fail."
+
+    override val pos = offendingNode.exp.pos
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = QuasihavocFailed(offendingNode.asInstanceOf[Quasihavoc], this.reason, this.cached)
+    def withReason(r: ErrorReason) = QuasihavocFailed(offendingNode, r, cached)
+  }
+
+  def QuasihavocFailed(offendingNode: Quasihavoc): PartialVerificationError =
+    PartialVerificationError((reason: ErrorReason) => QuasihavocFailed(offendingNode, reason))
+
+  case class HavocallFailed(offendingNode: Quasihavocall, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
+    val id = "quasihavocall.failed"
+    val text = "Quasihavocall might fail."
+
+    override val pos = offendingNode.exp.pos
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = HavocallFailed(offendingNode.asInstanceOf[Quasihavocall], this.reason, this.cached)
+    def withReason(r: ErrorReason) = HavocallFailed(offendingNode, r, cached)
+  }
+
+  def HavocallFailed(offendingNode: Quasihavocall): PartialVerificationError =
+    PartialVerificationError((reason: ErrorReason) => HavocallFailed(offendingNode, reason))
+
+
   case class HeuristicsFailed(offendingNode: ErrorNode, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
     val id = "heuristics.failed"
     val text = "Applying heuristics failed."
@@ -648,6 +673,13 @@ object reasons {
     def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = QPAssertionNotInjective(offendingNode.asInstanceOf[ResourceAccess])
   }
 
+  case class QuasihavocallNotInjective(offendingNode: Quasihavocall) extends AbstractErrorReason {
+    val id = "quasihavocall.not.injective"
+    val readableMessage = s"Quasihavocall statement $offendingNode might not be injective."
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = QuasihavocallNotInjective(offendingNode.asInstanceOf[Quasihavocall])
+  }
+
   case class LabelledStateNotReached(offendingNode: LabelledOld) extends AbstractErrorReason {
     val id = "labelled.state.not.reached"
     val lbl = offendingNode.oldLabel