WIP: Function axiomatization fix using uninterpreted guard function

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

@@ -38,6 +38,6 @@ 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)], havocHeap: Boolean = true, isAssert: Boolean = false,
+             addFreeAssumptionBefore: Boolean = false, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt
 }

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

@@ -59,4 +59,18 @@ trait FuncPredModule extends Module {
 
   def translateBackendFuncApp(fa: sil.BackendFuncApp): Exp
   def translateBackendFunc(f: sil.BackendFunc): Seq[Decl]
+
+  /***
+    * Returns a Boolean Boogie expression that expresses the conditions one gets for free for function calls in e, if
+    * e is well-defined. If result is None, then there are no such free conditions.
+    * @param e must be a pure expression
+    * @return
+    */
+  def allFreeFunctionAssumptions(e: sil.Exp) : Stmt
+
+  /***
+    * Same as freeFunctionAssumptions(e: sil.Exp) except that the input expects a Boogie translation of a pure Viper expression
+    */
+  def allFreeFunctionAssumptions(e: Exp) : Stmt
+
 }

src/main/scala/viper/carbon/modules/impls/DefaultExhaleModule.scala

@@ -35,8 +35,8 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
     register(this)
   }
 
-  override def exhale(exps: Seq[(sil.Exp, PartialVerificationError)], havocHeap: Boolean = true, isAssert: Boolean = false
-                      , statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
+  override def exhale(exps: Seq[(sil.Exp, PartialVerificationError)], havocHeap: Boolean = true, isAssert: Boolean = false,
+                      addFreeAssumptionBefore: Boolean = false, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
 
     // creating a new temp state if we are inside a package statement
     val curState = stateModule.state
@@ -48,7 +48,7 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
     }
     val tempState: StateRep = wandModule.tempCurState.asInstanceOf[StateRep]
 
-    val exhaleStmt = exps map (e => exhaleConnective(e._1.whenExhaling, e._2, havocHeap,
+    val exhaleStmt = exps map (e => exhaleConnective(e._1.whenExhaling, e._2, havocHeap, addFreeAssumptionBefore,
       statesStackForPackageStmt, insidePackageStmt, isAssert = isAssert, currentStateForPackage = tempState))
 
     val assumptions = MaybeCommentBlock("Free assumptions (exhale module)",
@@ -77,43 +77,66 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
     *                  Access to the current state is needed during translation of an exhale during packaging a wand
    */
   private def exhaleConnective(e: sil.Exp, error: PartialVerificationError, havocHeap: Boolean = true,
+                               addFreeAssumptionBefore: Boolean = false,
                                statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false,
                                isAssert: Boolean , currentStateForPackage: StateRep): Stmt = {
 
     // creating union of current state and ops state to be used in translating exps
     val currentState = stateModule.state
 
+    def maybeFuncAssumptionsSil(eDef: sil.Exp) : Stmt = {
+      if(addFreeAssumptionBefore)
+        MaybeCommentBlock("ExhaleModule function assumptions", funcPredModule.allFreeFunctionAssumptions(eDef))
+      else Statements.EmptyStmt
+    }
+
+    def maybeFuncAssumptions(eDef: Exp) : Stmt = {
+      if(addFreeAssumptionBefore)
+        MaybeCommentBlock("ExhaleModule function assumptions", funcPredModule.allFreeFunctionAssumptions(eDef))
+      else Statements.EmptyStmt
+    }
+
     e match {
       case sil.And(e1, e2) =>
-        exhaleConnective(e1, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
-          exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
+        exhaleConnective(e1, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
+          exhaleConnective(e2, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
           Nil
       case sil.Implies(e1, e2) =>
+        val e1TranslatedInWand = translateExpInWand(e1)
         if(insidePackageStmt){
-          val res = If(wandModule.getCurOpsBoolvar() ==> translateExpInWand(e1), exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
+          val res = If(wandModule.getCurOpsBoolvar() ==> e1TranslatedInWand, exhaleConnective(e2, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
           val unionStmt = wandModule.updateUnion()
           res ++ unionStmt
         }
-        else
-          If(translateExpInWand(e1), exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
+        else {
+          maybeFuncAssumptions(e1TranslatedInWand) ++
+          If(e1TranslatedInWand, exhaleConnective(e2, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage), Statements.EmptyStmt)
+        }
       case sil.CondExp(c, e1, e2) =>
-        if(insidePackageStmt)
+        val cTranslatedInWand = translateExpInWand(c)
+        if(insidePackageStmt) {
+          maybeFuncAssumptions(cTranslatedInWand) ++
           If(wandModule.getCurOpsBoolvar(),
-            If(translateExpInWand(c), exhaleConnective(e1, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
-              exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage)),
+            If(cTranslatedInWand,
+              exhaleConnective(e1, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
+              exhaleConnective(e2, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage)),
             Statements.EmptyStmt) ++
             // The union state should be updated because the union state calculated inside exhaleExt (let's call it state U') is inside the then part of if(c){}
             // and outside the if condition c is not satisfied we still evaluate expressions and check definedness in U' without knowing any assumption about it
           wandModule.updateUnion()
-        else
-          If(translateExpInWand(c), exhaleConnective(e1, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
-            exhaleConnective(e2, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage))
+        } else {
+          maybeFuncAssumptions(cTranslatedInWand) ++
+          If(cTranslatedInWand, exhaleConnective(e1, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage),
+            exhaleConnective(e2, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage))
+        }
       case sil.Let(declared,boundTo,body) if !body.isPure =>
       {
         val u = env.makeUniquelyNamed(declared) // choose a fresh binder
+        val boundToTranslatedInWand = translateExpInWand(boundTo)
         env.define(u.localVar)
-        Assign(translateLocalVar(u.localVar),translateExpInWand(boundTo)) ::
-          exhaleConnective(body.replace(declared.localVar, u.localVar),error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
+        Assign(translateLocalVar(u.localVar), boundToTranslatedInWand) ::
+          maybeFuncAssumptions(boundToTranslatedInWand) ::
+          exhaleConnective(body.replace(declared.localVar, u.localVar),error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage) ::
           {
             env.undefine(u.localVar)
             Nil
@@ -128,33 +151,39 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
 
         val renamedBody = Expressions.instantiateVariables(body, vars.map(_.localVar), varsFresh.map(_.localVar))
 
-        val exhaleStmt : Stmt = exhaleConnective(renamedBody, error, havocHeap, statesStackForPackageStmt,
+        val exhaleStmt : Stmt = exhaleConnective(renamedBody, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt,
           insidePackageStmt, isAssert, currentStateForPackage = currentStateForPackage)
 
+        val translatedExp : Exp = translateExp(e)
+        varsFresh.foreach(vFresh => env.undefine(vFresh.localVar))
+
         Seqn(Seq (
           NondetIf(Seqn(Seq(exhaleStmt, Assume(FalseLit())))),
           //GP: in the non-deterministic branch we checked the assertion, hence we assume the assertion in the main branch
-          Assume(translateExp(e)),
-          {
-            varsFresh.foreach(vFresh => env.undefine(vFresh.localVar))
-            Nil
-          }
-        ))
+          Assume(translatedExp)
+          ) ++
+          (
+            /* we need to assume the function call assumptions again, since previously they are made within the non-deterministic
+               branch within which assertions are checked
+             */
+            maybeFuncAssumptions(translatedExp)
+          )
+        )
       }
       case sil.Unfolding(_, body) if !insidePackageStmt => {
         val checks = components map (_.exhaleExpBeforeAfter(e, error))
         val stmtBefore = (checks map (_._1())).toList
 
         val stmtBody =
-            exhaleConnective(body, error, havocHeap, statesStackForPackageStmt, insidePackageStmt, isAssert,
+            exhaleConnective(body, error, havocHeap, addFreeAssumptionBefore, statesStackForPackageStmt, insidePackageStmt, isAssert,
               currentStateForPackage = currentStateForPackage)
 
         val stmtAfter = (checks map (_._2())).toList
 
         (stmtBefore ++ stmtBody ++ stmtAfter)
       }
       case _ => {
-        if(insidePackageStmt){  // handling exhales during packaging a wand
+        if(insidePackageStmt) {  // handling exhales during packaging a wand
           // currently having wild cards and 'constraining' expressions are not supported during packaging a wand.
           if(!permModule.getCurrentAbstractReads().isEmpty) {
             sys.error("Abstract reads cannot be used during packaging a wand.")  // AG: To be changed to unsupportedFeatureException
@@ -182,20 +211,26 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
           else
             exhaleExtStmt ++ addAssumptions ++ assertTransfer
         } else {
-          invokeExhaleOnComponents(e, error)
+          invokeExhaleOnComponents(e, error, addFreeAssumptionBefore)
         }
       }
     }
   }
 
-  private def invokeExhaleOnComponents(e: sil.Exp, error: PartialVerificationError) : Stmt = {
+  private def invokeExhaleOnComponents(e: sil.Exp, error: PartialVerificationError, addFreeAssumptionsBefore: Boolean) : Stmt = {
+    val maybeFunctionAssms : Stmt =
+      if(addFreeAssumptionsBefore) {
+        MaybeCommentBlock("ExhaleModule function assumptions", funcPredModule.allFreeFunctionAssumptions(e))
+      } else {
+        Statements.EmptyStmt
+      }
     val checks = components map (_.exhaleExpBeforeAfter(e, error))
     val stmtBefore = checks map (_._1())
     // some implementations may rely on the order of these calls
 
     val stmtAfter = checks map (_._2())
 
-    stmtBefore ++ stmtAfter
+    maybeFunctionAssms ++ stmtBefore ++ stmtAfter
   }
 
   /**