asserting in expressions (take 2)

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

@@ -483,17 +483,22 @@ case class CondExp(cond: Exp, thn: Exp, els: Exp)(val pos: Position = NoPosition
 }
 
 // --- Prover hint expressions
-
-case class Unfolding(acc: PredicateAccessPredicate, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+/** Prover hint expressions. eg unfolding in */
+sealed trait HintExp extends Exp {
+  val body: Exp
   override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(body)
-  lazy val typ = body.typ
+  lazy val typ: Type = body.typ
+}
+
+case class Unfolding(acc: PredicateAccessPredicate, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends HintExp {
 }
 
-case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends HintExp {
   override lazy val check : Seq[ConsistencyError] = (if(!(wand isSubtype Wand)) Seq(ConsistencyError(s"Expected wand but found ${wand.typ} ($wand)", wand.pos)) else Seq()) ++ Consistency.checkPure(body)
-  lazy val typ = body.typ
 }
 
+case class Asserting(assertion: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends HintExp {}
+
 // --- Old expressions
 
 sealed trait OldExp extends UnExp {

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

@@ -741,6 +741,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       group(parens(text("unfolding") <+> nest(defaultIndent, show(acc)) <+> "in" <> nest(defaultIndent, line <> show(exp))))
     case Applying(wand, exp) =>
       parens(text("applying") <+> nest(defaultIndent, show(wand)) <+> "in" <> nest(defaultIndent, line <> show(exp)))
+    case Asserting(assertion, exp) =>
+      parens(text("asserting") <+> nest(defaultIndent, parens(show(assertion))) <+> "in" <+> show(exp))
     case Old(exp) =>
       text("old") <> parens(show(exp))
     case LabelledOld(exp,label) =>

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

@@ -221,8 +221,7 @@ object Consistency {
   }
 
   def noGhostOperations(n: Node) = !n.existsDefined {
-    case u: Unfolding if !u.isPure =>
-    case a: Applying if !a.isPure =>
+    case h: HintExp if !h.isPure =>
   }
 
   /** Returns true iff the given expression is a valid trigger. */

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

@@ -23,8 +23,7 @@ object Expressions {
     case InhaleExhaleExp(in, ex) => isPure(in) && isPure(ex)
     case BinExp(e0, e1) => isPure(e0) && isPure(e1)
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
-    case unf: Unfolding => isPure(unf.body)
-    case app: Applying => isPure(app.body)
+    case h: HintExp => isPure(h.body)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure

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

@@ -83,6 +83,7 @@ object Nodes {
           case PredicateAccessPredicate(pred_acc, perm) => Seq(pred_acc, perm)
           case Unfolding(acc, body) => Seq(acc, body)
           case Applying(wand, body) => Seq(wand, body)
+          case Asserting(assertion, body) => Seq(assertion, body)
           case Old(exp) => Seq(exp)
           case CondExp(cond, thn, els) => Seq(cond, thn, els)
           case Let(v, exp, body) => Seq(v, exp, body)

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

@@ -93,7 +93,7 @@ object FastParserCompanion {
     // maps
     "Map", "range",
     // prover hint expressions
-    "unfolding", "in", "applying",
+    "unfolding", "in", "applying", "asserting",
     // old expression
     "old", "lhs",
     // other expressions
@@ -796,7 +796,7 @@ class FastParser {
   // 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
     | result | unExp | typedFapp
-    | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying
+    | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying | asserting
     | setTypedEmpty | explicitSetNonEmpty | multiSetTypedEmpty | explicitMultisetNonEmpty | seqTypedEmpty
     | size | explicitSeqNonEmpty | seqRange
     | mapTypedEmpty | explicitMapNonEmpty | mapDomain | mapRange
@@ -1210,6 +1210,9 @@ class FastParser {
 
   def applying[_: P]: P[PExp] = FP(keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PApplying(a, b)(pos) }
 
+
+  def asserting[_: P]: P[PExp] = FP(keyword("asserting") ~/ "(" ~ exp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PAsserting(a, b)(pos) }
+
   def programDecl(implicit ctx : P[_]) : P[PProgram] = P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | domainDecl | fieldDecl | functionDecl | predicateDecl | methodDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map {
     case (pos, decls) => {
       PProgram(

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

@@ -717,6 +717,13 @@ case class PApplying(wand: PExp, exp: PExp)(val pos: (Position, Position)) exten
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
+case class PAsserting(assertion: PExp, exp: PExp)(val pos: (Position, Position)) extends POpApp {
+  override val opName = "applying"
+  override val args = Seq(assertion, exp)
+  override val signatures : List[PTypeSubstitution] =
+    List(Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> POpApp.pArg(1)))
+}
+
 sealed trait PBinder extends PExp{
   def body:PExp
   var _typeSubstitutions : List[PTypeSubstitution] =  null
@@ -1255,6 +1262,7 @@ object Nodes {
       case PCall(func, args, optType) => Seq(func) ++ args ++ (optType match { case Some(t) => Seq(t) case None => Nil})
       case PUnfolding(acc, exp) => Seq(acc, exp)
       case PApplying(wand, exp) => Seq(wand, exp)
+      case PAsserting(assertion, exp) => Seq(assertion, exp)
       case PExists(vars, triggers, exp) => vars ++ triggers ++ Seq(exp)
       case PLabelledOld(id, e) => Seq(id, e)
       case po: POldExp => Seq(po.e)

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

@@ -61,6 +61,7 @@ object Transformer {
 
         case p@PUnfolding(acc, exp) => PUnfolding(go(acc), go(exp))(p.pos)
         case p@PApplying(wand, exp) => PApplying(go(wand), go(exp))(p.pos)
+        case p@PAsserting(assertion, exp) => PAsserting(go(assertion), go(exp))(p.pos)
 
         case p@PExists(vars, triggers, exp) => PExists(vars map go, triggers map go, go(exp))(p.pos)
         case p@PForall(vars, triggers, exp) => PForall(vars map go, triggers map go, go(exp))(p.pos)

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

@@ -442,6 +442,8 @@ case class Translator(program: PProgram) {
         Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos)
       case PApplying(wand, e) =>
         Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos)
+      case PAsserting(a, e) =>
+        Asserting(exp(a), exp(e))(pos)
       case PLet(exp1, PLetNestedScope(variable, body)) =>
         Let(liftVarDecl(variable), exp(exp1), exp(body))(pos)
       case _: PLetNestedScope =>

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -6,26 +6,26 @@
 
 package viper.silver.plugin.standard.termination
 
+import fastparse._
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
-import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
+import viper.silver.ast.{Assert, CondExp, CurrentPerm, Exp, Function, HintExp, InhaleExhaleExp, MagicWand, Method, Node, Program, While}
+import viper.silver.parser.FastParserCompanion.whitespace
 import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.PPredicateInstance
 import viper.silver.plugin.standard.termination.transformation.Trafo
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
-import viper.silver.verifier.errors.{AssertFailed, PreconditionInAppFalse}
-import viper.silver.verifier._
-import fastparse._
-import viper.silver.parser.FastParserCompanion.whitespace
 import viper.silver.reporter.Entity
+import viper.silver.verifier._
+import viper.silver.verifier.errors.AssertFailed
 
 import scala.annotation.unused
 
 class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
                         @unused logger: ch.qos.logback.classic.Logger,
                         config: viper.silver.frontend.SilFrontendConfig,
                         fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
-  import fp.{FP, keyword, exp, ParserExtension}
+  import fp.{FP, ParserExtension, exp, keyword}
 
   private def deactivated: Boolean = config != null && config.terminationPlugin.toOption.getOrElse(false)
 
@@ -246,8 +246,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     case _ =>
   }).recurseFunc({
     case CondExp(_, e1, e2) => Seq(e1, e2)
-    case Applying(_, exp) => Seq(exp)
-    case Unfolding(_, exp) => Seq(exp)
+    case h: HintExp => Seq(h.body)
     case CurrentPerm(_) => Nil
   })
 }

src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala

@@ -167,9 +167,8 @@ trait ExpTransformer extends ProgramManager with ErrorReporter {
   }
 
   private val toPureBooleanExpRecursion: PartialFunction[Node, Seq[Node]] = {
-    case Unfolding(_, body) => Seq(body)
+    case h: HintExp => Seq(h.body)
     case _: AccessPredicate | _: MagicWand => Nil
-    case Applying(_, b) => Seq(b)
     case Forall(_, _, exp) => Seq(exp)
   }
 

src/test/resources/all/asserting-in/other-fail.vpr

@@ -0,0 +1,16 @@
+field x: Int
+
+method test1() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (1 / 0 == 0) in true
+}
+
+method test2() {
+  //:: ExpectedOutput(assert.failed:division.by.zero)
+  assert asserting (true) in (1 / 0 == 0)
+}
+
+method test3(r: Ref) {
+  //:: ExpectedOutput(assert.failed:insufficient.permission)
+  assert asserting (true && acc(r.x)) in true
+}

src/test/resources/all/asserting-in/pass.vpr

@@ -0,0 +1,7 @@
+field x: Int
+
+method test1(r: Ref) returns (y: Int)
+requires acc(r.x)
+ensures acc(r.x) && y == r.x {
+  y := asserting (acc(r.x)) in r.x
+}

src/test/resources/all/asserting-in/simple-fail.vpr

@@ -0,0 +1,15 @@
+method assign() {
+//:: ExpectedOutput(assignment.failed:assertion.false)
+  var x: Int := asserting (false) in 0
+}
+
+method pres()
+//:: ExpectedOutput(not.wellformed:assertion.false)
+requires asserting (false) in false {
+  assert false
+}
+
+//:: ExpectedOutput(function.not.wellformed:assertion.false)
+function fun(): Int {
+  asserting (false) in 0
+}

src/test/resources/all/asserting-in/wand.vpr

@@ -0,0 +1,5 @@
+field f: Int
+
+method test0(x: Ref) {
+    package acc(x.f) && (asserting (acc(x.f)) in (x.f == 0)) --* acc(x.f) {}
+}