Add Inhaling expression

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

@@ -495,6 +495,12 @@ case class Applying(wand: MagicWand, body: Exp)(val pos: Position = NoPosition,
   lazy val typ = body.typ
 }
 
+case class Inhaling(exp: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp {
+  override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(body) ++
+    (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Assertion to inhale must be of type Bool, but found ${exp.typ}", exp.pos)) else Seq())
+  lazy val typ: Type = body.typ
+}
+
 // --- Old expressions
 
 sealed trait OldExp extends UnExp {

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

@@ -770,7 +770,9 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case Unfolding(acc, exp) =>
         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)))
+        parens(text("applying") <+> parens(nest(defaultIndent, show(wand))) <+> "in" <> nest(defaultIndent, line <> show(exp)))
+      case Inhaling(exp, body) =>
+        parens(text("inhaling") <+> parens(nest(defaultIndent, show(exp))) <+> "in" <> nest(defaultIndent, line <> show(body)))
       case Old(exp) =>
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>

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

@@ -25,6 +25,7 @@ object Expressions {
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
     case unf: Unfolding => isPure(unf.body)
     case app: Applying => isPure(app.body)
+    case inh: Inhaling => isPure(inh.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 Inhaling(exp, body) => Seq(exp, 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

@@ -365,7 +365,7 @@ class FastParser {
   def atomReservedKw[$: P]: P[PExp] = {
     reservedKwMany(
       StringIn("true", "false", "null", "old", "result", "acc", "none", "wildcard", "write", "epsilon", "perm", "let", "forall", "exists", "forperm",
-        "unfolding", "applying", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
+        "unfolding", "applying", "inhaling", "Set", "Seq", "Multiset", "Map", "range", "domain", "new"),
       str => pos => str match {
         case "true" => Pass.map(_ => PBoolLit(PReserved(PKw.True)(pos))(_))
         case "false" => Pass.map(_ => PBoolLit(PReserved(PKw.False)(pos))(_))
@@ -384,6 +384,7 @@ class FastParser {
         case "forperm" => forperm.map(_(PReserved(PKw.Forperm)(pos)))
         case "unfolding" => unfolding.map(_(PReserved(PKwOp.Unfolding)(pos)))
         case "applying" => applying.map(_(PReserved(PKwOp.Applying)(pos)))
+        case "inhaling" => inhaling.map(_(PReserved(PKwOp.Inhaling)(pos)))
         case "Set" => setConstructor.map(_(PReserved(PKwOp.Set)(pos)))
         case "Seq" => seqConstructor.map(_(PReserved(PKwOp.Seq)(pos)))
         case "Multiset" => multisetConstructor.map(_(PReserved(PKwOp.Multiset)(pos)))
@@ -652,6 +653,10 @@ class FastParser {
       PApplying(_, wand.inner, op, b)
   }
 
+  def inhaling[$: P]: P[PKwOp.Inhaling => Pos => PExp] = P(exp.parens ~ PKwOp.In ~ exp).map {
+    case (exp, in, body) => PInhaling(_, exp.inner, in, body)
+  }
+
   def predicateAccessAssertion[$: P]: P[PAccAssertion] = P(accessPred | predAcc)
 
   def setConstructor[$: P]: P[PKwOp.Set => Pos => PExp] =

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

@@ -1064,6 +1064,14 @@ case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PE
     List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
+case class PInhaling(inhaling: PKwOp.Inhaling, exp: PExp, in: PKwOp.In, body: PExp)(val pos: (Position, Position)) extends PHeapOpApp {
+  override val args = Seq(exp, body)
+  override val signatures: List[PTypeSubstitution] = List(
+    Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> POpApp.pArg(1)),
+    Map(POpApp.pArgS(0) -> Impure, POpApp.pResS -> POpApp.pArg(1)),
+  )
+}
+
 sealed trait PBinder extends PExp with PScope {
   def boundVars: Seq[PLogicalVarDecl]
 

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

@@ -494,6 +494,8 @@ object PKwOp {
   type Unfolding = PReserved[Unfolding.type]
   case object Applying    extends PKwOp("applying")                 with PKeywordAtom with RightSpace
   type Applying = PReserved[Applying.type]
+  case object Inhaling    extends PKwOp("inhaling")                 with PKeywordAtom with RightSpace
+  type Inhaling = PReserved[Inhaling.type]
   case object Let         extends PKwOp("let")                      with PKeywordAtom with RightSpace
   type Let = PReserved[Let.type]
 

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

@@ -707,6 +707,8 @@ case class TypeChecker(names: NameAnalyser) {
               case PApplying(_, wand, _, _) =>
                 checkMagicWand(wand)
 
+              case PInhaling(_, _, _, _) =>
+
               // We checked that the `rcv` is valid above with `poa.args.foreach(checkInternal)`
               case PFieldAccess(_, _, idnref) =>
                 if (idnref.decls.isEmpty)

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

@@ -507,6 +507,8 @@ case class Translator(program: PProgram) {
         Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info)
       case PApplying(_, wand, _, e) =>
         Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info)
+      case PInhaling(_, e, _, body) =>
+        Inhaling(exp(e), exp(body))(pos, info)
       case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) =>
         Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info)
       case _: PLetNestedScope =>

src/test/resources/inhaling/README.md

@@ -0,0 +1,13 @@
+# Test Cases for inhaling expressions
+
+| Filename                 | Description                                                            |
+|--------------------------|------------------------------------------------------------------------|
+| [test1.vpr](./test1.vpr) | Inhaling magic wand's LHS to inspect its snapshot.                     |
+| [test2.vpr](./test2.vpr) | Inhaling single fields and inspect its values.                         |
+| [test3.vpr](./test3.vpr) | Inhaling predicates and inspect its values.                            |
+| [test4.vpr](./test4.vpr) | Inhaling fields and return some values.                                |
+| [test5.vpr](./test5.vpr) | Inhaling in a method's precondition to define a magic wand's snapshot. |
+| [test6.vpr](./test6.vpr) | Invalid inhaling leads to a inconsistent state.                        |           
+| [test7.vpr](./test7.vpr) | Inhaling fields with conditionals.                                     |
+| [test8.vpr](./test8.vpr) | Inhaling fields with value conditions.                                 |
+| [test9.vpr](./test9.vpr) | Inhaling does not leak any permissions.                                |

src/test/resources/inhaling/test1.vpr

@@ -0,0 +1,13 @@
+field f: Int
+
+method test1(x: Ref, y: Ref)
+    requires acc(x.f) && acc(y.f)
+{
+    y.f := 42
+
+    package acc(x.f) --* acc(y.f)
+    exhale acc(x.f)
+
+    assert inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+    assert acc(x.f, none)
+}

src/test/resources/inhaling/test2.vpr

@@ -0,0 +1,14 @@
+field f: Int
+
+method test2(x: Ref, y: Ref)
+    requires acc(x.f) && acc(y.f)
+{
+    x.f := 10
+    y.f := 42
+
+    exhale acc(x.f)
+
+    assert inhaling (acc(x.f)) in y.f == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (acc(x.f)) in x.f == 10
+}

src/test/resources/inhaling/test3.vpr

@@ -0,0 +1,15 @@
+field f: Int
+
+predicate foo(x: Ref) { acc(x.f) }
+
+method test3(x: Ref, y: Ref)
+    requires foo(x) && foo(y)
+    requires unfolding foo(x) in x.f == 10
+    requires unfolding foo(y) in y.f == 42
+{
+    exhale foo(x)
+
+    assert inhaling (foo(x)) in unfolding foo(y) in y.f == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (foo(x)) in unfolding foo(x) in x.f == 10
+}

src/test/resources/inhaling/test4.vpr

@@ -0,0 +1,18 @@
+field f: Int
+
+method test4(x: Ref, y: Ref)
+    requires acc(x.f) && acc(y.f)
+{
+    x.f := 42
+    y.f := 10
+
+    package acc(x.f) --* acc(y.f)
+    exhale acc(x.f)
+
+    var p: Int := inhaling (acc(x.f)) in x.f
+    var q: Int := inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f
+
+    assert q == 10
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert p == 42
+}

src/test/resources/inhaling/test5.vpr

@@ -0,0 +1,12 @@
+field f: Int
+
+method test5(x: Ref, y: Ref)
+    requires true --* acc(x.f)
+    requires acc(x.f) --* acc(y.f)
+    requires inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 10
+{
+    apply true --* acc(x.f)
+    apply acc(x.f) --* acc(y.f)
+
+    assert y.f == 10
+}

src/test/resources/inhaling/test6.vpr

@@ -0,0 +1,27 @@
+field f: Int
+
+predicate P(x: Ref) {
+    acc(x.f) && x.f == 1
+}
+
+method test6a(x: Ref)
+    requires acc(x.f)
+{
+    assert inhaling (acc(x.f)) in true
+    assert false
+}
+
+method test6b(x: Ref)
+    requires acc(x.f)
+{
+    assert inhaling (acc(x.f)) in false
+}
+
+method test6c(x: Ref)
+    requires acc(x.f) && x.f == 0
+{
+    assert inhaling (P(x)) in x.f == 0
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (P(x)) in false
+    assert inhaling (P(x)) in unfolding P(x) in false
+}

src/test/resources/inhaling/test7.vpr

@@ -0,0 +1,27 @@
+field f: Int
+
+method test7a(x: Ref, y: Ref, i: Int)
+    requires acc(x.f) && acc(y.f)
+    requires y.f == 42
+{
+    package acc(x.f) --* acc(y.f)
+
+    if (i < 0) {
+        exhale acc(x.f)
+        assert inhaling (i < 0 ? acc(x.f) : true) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+    } else {
+        assert inhaling (i < 0 ? acc(x.f) : true) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+    }
+}
+
+method test7b(x: Ref, y: Ref, i: Int)
+    requires acc(x.f) && acc(y.f)
+    requires y.f == 42
+{
+    package acc(x.f) --* acc(y.f)
+    if (i < 0) {
+        exhale acc(x.f)
+    }
+
+    assert inhaling (i < 0 ? acc(x.f) : true) in applying (acc(x.f) --* acc(y.f)) in y.f == 42
+}

src/test/resources/inhaling/test8.vpr

@@ -0,0 +1,15 @@
+field f: Int
+
+method test8a(x: Ref)
+    requires acc(x.f)
+{
+    assert inhaling (x.f == 1) in x.f == 1
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (x.f == 1) in x.f == 0
+}
+
+method test8b(x: Ref) {
+    assert inhaling (acc(x.f) && x.f == 1) in x.f == 1
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert inhaling (acc(x.f) && x.f == 1) in x.f == 0
+}

src/test/resources/inhaling/test9.vpr

@@ -0,0 +1,14 @@
+field f: Int
+
+method test9a(x: Ref) {
+    assert inhaling (acc(x.f) && x.f == 0) in x.f == 0
+    assert acc(x.f, none)
+}
+
+method test9b(x: Ref, p: Perm)
+    requires none <= p
+    requires acc(x.f, p)
+{
+    assert inhaling (acc(x.f, write - p) && x.f == 0) in x.f == 0
+    assert acc(x.f, p)
+}