Include definedness checks during exhale (#457)

src/main/scala/viper/carbon/modules/ExhaleModule.scala

@@ -6,7 +6,7 @@
 
 package viper.carbon.modules
 
-import components.{ComponentRegistry, ExhaleComponent}
+import components.{ComponentRegistry, DefinednessState, ExhaleComponent}
 import viper.silver.{ast => sil}
 import viper.carbon.boogie.Stmt
 import viper.silver.verifier.PartialVerificationError
@@ -25,7 +25,10 @@ import viper.silver.verifier.PartialVerificationError
 trait ExhaleModule extends Module with ExhaleComponent with ComponentRegistry[ExhaleComponent] {
 
   /**
-    * @param exp         the expression to be exhaled and the error to be raised if the exhale fails.
+    * @param exp         A sequence of triples where the conjunction of the corresponding expressions (projection on the
+    *                    the first element) is to be exhaled. The triple includes the error to be raised if the exhale fails and
+    *                    the error to be raised if a well-definedness check fails during the exhale (if the latter is set
+    *                    to [[None]], then no well-definedness checks are performed).
     * @param havocHeap   A boolean used to allow or prevent havocing the heap after the exhale.
     *                    For example, the heap is not havoced after the exhale when translating a fold statement.
     * @param isAssert    A boolean that tells whether the exhale method is being called during an exhale statement or an assert statement
@@ -38,6 +41,25 @@ trait ExhaleModule extends Module with ExhaleComponent with ComponentRegistry[Ex
     * The 'statesStackForPackageStmt' and 'insidePackageStmt' are used when translating statements during packaging a wand.
     * For more details refer to the note in the wand module.
     */
-  def exhale(exp: Seq[(sil.Exp, PartialVerificationError)], havocHeap: Boolean = true, isAssert: Boolean = false
-             , statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
-}
+  def exhale(exp: Seq[(sil.Exp, PartialVerificationError, Option[PartialVerificationError])], havocHeap: Boolean = true,
+             isAssert: Boolean = false, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
+
+  /** convenience methods */
+
+  def exhaleWithoutDefinedness(exp: Seq[(sil.Exp, PartialVerificationError)], havocHeap: Boolean = true,
+                               isAssert: Boolean = false, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
+    exhale(exp.map(eError => (eError._1, eError._2, None)), havocHeap = havocHeap, isAssert = isAssert, statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)
+  }
+
+  def exhaleSingleWithoutDefinedness(exp: sil.Exp, exhaleError: PartialVerificationError, havocHeap: Boolean = true,
+                                     isAssert: Boolean = false, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
+    exhale(Seq((exp, exhaleError, None)), havocHeap = havocHeap, isAssert = isAssert, statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)
+  }
+
+  def exhaleSingleWithDefinedness(exp: sil.Exp, exhaleError: PartialVerificationError, definednessError: PartialVerificationError,
+                                  havocHeap: Boolean = true, isAssert: Boolean = false, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false) = {
+    exhale(Seq((exp, exhaleError, Some(definednessError))), havocHeap = havocHeap, isAssert = isAssert,
+      statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)
+  }
+
+}

src/main/scala/viper/carbon/modules/ExpModule.scala

@@ -8,7 +8,7 @@ package viper.carbon.modules
 
 import viper.silver.{ast => sil}
 import viper.carbon.boogie.{Exp, LocalVar, Stmt}
-import viper.carbon.modules.components.{ComponentRegistry, DefinednessComponent}
+import viper.carbon.modules.components.{ComponentRegistry, DefinednessComponent, DefinednessState}
 import viper.silver.verifier.PartialVerificationError
 
 /**
@@ -30,30 +30,27 @@ trait ExpModule extends Module with ComponentRegistry[DefinednessComponent] {
    */
   def allFreeAssumptions(e: sil.Exp): Stmt
 
-    /**
-      * Check definedness of Viper expressions as they occur in the program.
-      *
-      * makeChecks provides the possibility of switching off most checks, to get
-      * only the side-effects (unfoldings) of unravelling the expression. Note that
-      * the parameter should be passed down through recursive calls (default true)
-      *
-      * ignoreIfInWand gives the option to ignore the definedness check if it is called during a package statement
-      *
-      * inWand distinguish when check definedness is called during a package statement.
-      */
+  /***
+    * Check well-definedness of Viper expressions. This method should only be invoked on pure Viper expressions or
+    * impure *atomic* Viper assertions (e.g., accessibility predicates, quantified permissions).
+    * For other kinds of impure assertions such as separating conjunctions where one conjunct is impure, well-definedness
+    * is always tied to an inhale or exhale (or assert) operation. In those cases, the corresponding inhale and exhale
+    * methods should be invoked, which permit switching on well-definedness checks.
+    *
+    * @param e
+    * @param error
+    * @param makeChecks provides the possibility of switching off most checks, to get only the side-effects (unfoldings)
+    *                   of unravelling the expression. Note that the parameter should be passed down through recursive
+    *                   calls (default true)
+    * @param definednessStateOpt If defined, then represents the state in which permission checks that are part of the definedness
+    *                            check should be made, otherwise these checks should be made in the currently active state.
+    *                            Expressions should be evaluated in the currently active state.
+    * @param insidePackageStmt true if call is made during a package statement
+    * @param ignoreIfInWand gives the option to ignore the definedness check if it is called during a package statement
+    * @return
+    */
   def checkDefinedness(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean = true,
+                       definednessStateOpt: Option[DefinednessState] = None,
                        insidePackageStmt: Boolean = false, ignoreIfInWand: Boolean = false): Stmt
 
-  /**
-   * Check definedness of Viper assertions such as pre-/postconditions or invariants.
-   * The implementation works by exhaling 'e' and checking the necessary properties
-   * along the way.
-   *
-   * statesStackForPackageStmt stack of states used in translating statements during packaging a wand (carries currentState and LHS of wands)
-   * insidePackageStmt      Boolean that represents whether this method is being called during packaging a wand or not.
-   * The 'statesStackForPackageStmt' and 'insidePackageStmt' are used when translating statements during packaging a wand.
-   * For more details refer to the general note in 'wandModule'.
-   */
-  def checkDefinednessOfSpecAndExhale(e: sil.Exp, definednessError: PartialVerificationError, exhaleError: PartialVerificationError,
-                                      statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
 }

src/main/scala/viper/carbon/modules/components/DefinednessComponent.scala

@@ -26,14 +26,19 @@ trait DefinednessComponent extends Component {
     * the well-definedness checks for `e`'s subnodes.
     * If `makeChecks` is set to false, then no definedness checks should be emitted. See [[partialCheckDefinedness]]
     * for the purpose of `makeChecks`.
+    * If `definednessStateOpt` is defined, then it represents the state in which permission checks that are part of the
+    * definedness check should be made, otherwise these checks should be done in the currently active state.
+    * Expressions should be evaluated in the currently active state.
    */
-  def simplePartialCheckDefinednessBefore(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean): Stmt = Statements.EmptyStmt
+  def simplePartialCheckDefinednessBefore(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean,
+                                          definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
 
   /**
     * Same as [[simplePartialCheckDefinednessBefore]], except that this well-definedness check is invoked and emitted
     * *after* the well-definedness checks of `e`'s subnodes are invoked and emitted.
     */
-  def simplePartialCheckDefinednessAfter(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean): Stmt = Statements.EmptyStmt
+  def simplePartialCheckDefinednessAfter(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean,
+                                         definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
 
   /**
    * Proof obligations for a given expression.  The first part of the result is used before
@@ -43,7 +48,21 @@ trait DefinednessComponent extends Component {
    * The makeChecks argument can be set to false to cause the expression to be explored (and
    * corresponding unfoldings to be executed), but no other checks to actually be made. Note that this method
    * must be overridden for this parameter to be used.
+   * If `definednessStateOpt` is defined, then it represents the state in which permission checks that are part of the
+   * definedness check should be made, otherwise these checks should be done in the currently active state.
+   * Expressions should be evaluated in the currently active state.
    */
-  def partialCheckDefinedness(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean): (() => Stmt, () => Stmt) =
-    (() => simplePartialCheckDefinednessBefore(e, error, makeChecks), () => simplePartialCheckDefinednessAfter(e, error, makeChecks))
+  def partialCheckDefinedness(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean,
+                              definednessStateOpt: Option[DefinednessState]): (() => Stmt, () => Stmt) =
+    (
+      () => simplePartialCheckDefinednessBefore(e, error, makeChecks, definednessStateOpt),
+      () => simplePartialCheckDefinednessAfter(e, error, makeChecks, definednessStateOpt)
+    )
+
 }
+
+/**
+  * Wrapper for representing the definedness state.
+  * @param setDefState Running this should set the currently active state to the definedness state.
+  */
+case class DefinednessState(var setDefState: () => Unit)

src/main/scala/viper/carbon/modules/components/ExhaleComponent.scala

@@ -19,13 +19,24 @@ trait ExhaleComponent extends Component {
   /**
    * Exhale a single expression.
    */
-  def exhaleExp(e: sil.Exp, error: PartialVerificationError): Stmt = Statements.EmptyStmt
+  def exhaleExp(e: sil.Exp, error: PartialVerificationError, definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
 
   /**
+    */
+
+  /***
+    * Method that allows components to contribute to exhaling an expression.
     * The first part of the result is used before exhaling the expression, and finally after exhaling the expression
     * the second part of the result is used.
+    * @param e expression to be exhaled.
+    * @param error exhale error
+    * @param definednessStateOpt If defined, then this expresses the current state in which definedness checks are performed
+    *                            ("definedness state"). If defined and if the implementing component is responsible for the
+    *                            top-level operator in @{code e}, then the component must ensure that that the definedness
+    *                            state is updated (and restored) correctly.
+    * @return
     */
-  def exhaleExpBeforeAfter(e: sil.Exp, error: PartialVerificationError): (() => Stmt, () => Stmt) =
-    (() => exhaleExp(e, error), () => Statements.EmptyStmt)
+  def exhaleExpBeforeAfter(e: sil.Exp, error: PartialVerificationError, definednessStateOpt: Option[DefinednessState]): (() => Stmt, () => Stmt) =
+    (() => exhaleExp(e, error, definednessStateOpt), () => Statements.EmptyStmt)
 
 }