Add Inhaling expression

src/main/scala/rules/Evaluator.scala

@@ -18,7 +18,7 @@ import viper.silicon.state.terms._
 import viper.silicon.state.terms.implicits._
 import viper.silicon.state.terms.perms.{IsNonNegative, IsPositive}
 import viper.silicon.state.terms.predef.`?r`
-import viper.silicon.utils.toSf
+import viper.silicon.utils.{freshSnap, toSf}
 import viper.silicon.utils.ast.flattenOperator
 import viper.silicon.verifier.Verifier
 import viper.silicon.{Map, TriggerSets}
@@ -910,7 +910,16 @@ object evaluator extends EvaluationRules {
         joiner.join[Term, Term](s, v)((s1, v1, QB) =>
           magicWandSupporter.applyWand(s1, wand, pve, v1)((s2, v2) => {
             eval(s2, eIn, pve, v2)(QB)
-        }))(join(v.symbolConverter.toSort(eIn.typ), "joined_applying", s.relevantQuantifiedVariables, v))(Q)
+          })
+        )(join(v.symbolConverter.toSort(eIn.typ), "joined_applying", s.relevantQuantifiedVariables, v))(Q)
+
+      case ast.Inhaling(a, body) =>
+        joiner.join[Term, Term](s, v)((s1, v1, QB) =>
+          produce(s1, freshSnap, a, pve, v1)((s2, v2) => {
+            v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterInhale)
+            eval(s2, body, pve, v2)(QB)
+          })
+        )(join(v.symbolConverter.toSort(body.typ), "joined_inhaling", s.relevantQuantifiedVariables, v))(Q)
 
       /* Sequences */
 
@@ -1465,6 +1474,17 @@ object evaluator extends EvaluationRules {
     }
   }
 
+  /**
+   * Method that takes a list of [[viper.silicon.rules.JoinDataEntry]] from [[viper.silicon.rules.joiner.join]]
+   * and joins them using a symbolic join function with the given name and arguments.
+   *
+   * @param joinSort         The sort of the result of the join function.
+   * @param joinFunctionName The name of the join function.
+   * @param joinFunctionArgs The arguments of the join function.
+   * @param v                The current verifier.
+   * @param entries          The list of JoinDataEntry to join.
+   * @return A tuple containing the new state and the term resulting from the join.
+   */
   private def join(joinSort: Sort,
                    joinFunctionName: String,
                    joinFunctionArgs: Seq[Term],

src/main/scala/rules/ExecutionFlowController.scala

@@ -49,6 +49,29 @@ trait ExecutionFlowRules extends SymbolicExecutionRules {
 }
 
 object executionFlowController extends ExecutionFlowRules {
+  /**
+   * Execute a local block within its own scope. The continuation Q is invoked
+   * with the result of the local block if the local block succeeded. Changes
+   * to the state and verifier are not propagated outside of the local block.
+   *
+   * Usage example:
+   * {{{
+   * locallyWithResult[Term](s, v)((s1, v1, QL) => {
+   *   eval(s2, exp, pve, v2)((_, tExp, _) => {
+   *     QL(tExp)
+   *   })
+   * })(t => Q(s, t, v))
+   * }}}
+   *
+   * @param s     State to be used for the local block.
+   * @param v     Verifier to be used for the local block.
+   * @param block Local block to be executed. It accepts the current state, verifier, and a
+   *              continuation QL that is invoked with the result of the block.
+   * @param Q     Continuation that is invoked with the result of the local block if the local block
+   *              succeeded.
+   * @tparam R Type of the result of the local block.
+   * @return Verification result after executing the local block and the continuation Q.
+   */
   def locallyWithResult[R](s: State, v: Verifier)
                           (block: (State, Verifier, R => VerificationResult) => VerificationResult)
                           (Q: R => VerificationResult)
@@ -92,6 +115,14 @@ object executionFlowController extends ExecutionFlowRules {
     }
   }
 
+  /**
+   * Execute a local block that is executed within its own scope.
+   *
+   * @param s     State to be used for the local block.
+   * @param v     Verifier to be used for the local block.
+   * @param block Local block to be executed. It accepts a state and a verifier and returns a verification result.
+   * @return      Verification result of executing the local block.
+   */
   def locally(s: State, v: Verifier)
              (block: (State, Verifier) => VerificationResult)
              : VerificationResult =

src/main/scala/rules/Joiner.scala

@@ -36,6 +36,25 @@ trait JoiningRules extends SymbolicExecutionRules {
 }
 
 object joiner extends JoiningRules {
+
+  /**
+   * This method is a higher-order function that handles the joining of different execution
+   * paths in a symbolic execution engine. It records the data collected from each execution path
+   * and merges it into a single data structure. The final data structure is then passed to a
+   * function that performs some final verification step.
+   *
+   * @param s          The current state of the symbolic execution.
+   * @param v          The current verifier.
+   * @param resetState A flag indicating whether the state should be reset after each execution path.
+   * @param block      A function that executes a block of code symbolically and collects data
+   *                   from each feasible execution path.
+   * @param merge      A function that merges the data collected from each feasible execution path.
+   * @param Q          A function that is called after all execution paths have been joined and the data has been merged.
+   *                   It is expected to perform some final verification step.
+   * @tparam D  The generic type parameter for the data collected from each execution path.
+   * @tparam JD The generic type parameter for the merged data.
+   * @return The final result of the join method, which is the result of the Q function.
+   */
   def join[D, JD](s: State, v: Verifier, resetState: Boolean = true)
                  (block: (State, Verifier, (State, D, Verifier) => VerificationResult) => VerificationResult)
                  (merge: Seq[JoinDataEntry[D]] => (State, JD))

src/main/scala/supporters/ExpressionTranslator.scala

@@ -259,6 +259,7 @@ trait ExpressionTranslator {
              | _: ast.Result
              | _: ast.Unfolding
              | _: ast.Applying
+             | _: ast.Inhaling
              | _: ast.InhaleExhaleExp
              | _: ast.PredicateAccess
              | _: ast.FuncApp

src/test/scala/SiliconTests.scala

@@ -20,7 +20,7 @@ class SiliconTests extends SilSuite {
   private val silTestDirectories =
     Seq("all",
         "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations",
-        "wands", "termination", "refute",
+        "wands", "termination", "refute", "inhaling",
         "examples")
 
   val testDirectories: Seq[String] = siliconTestDirectories ++ silTestDirectories