Checking only read permissions when asserting function preconditions (#…

…532)

src/main/scala/viper/carbon/CarbonVerifier.scala

@@ -94,6 +94,12 @@ case class CarbonVerifier(override val reporter: Reporter,
   }
   else false
 
+  def respectFunctionPrecPermAmounts: Boolean = if (config != null) config.respectFunctionPrePermAmounts.toOption match {
+    case Some(b) => b
+    case None => false
+  }
+  else false
+
   override def usePolyMapsInEncoding =
     if (config != null) {
       config.desugarPolymorphicMaps.toOption match {

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

@@ -8,7 +8,6 @@ package viper.carbon.modules
 
 import viper.carbon.boogie._
 import viper.carbon.modules.components.CarbonStateComponent
-import viper.carbon.utility.PolyMapRep
 import viper.silver.{ast => sil}
 
 case class PMaskDesugaredRep(selectId: Identifier, storeId: Identifier)
@@ -159,4 +158,8 @@ trait PermModule extends Module with CarbonStateComponent {
   // removes permission to w#ft (footprint of the magic wand) (See Heap module for w#ft description)
   def exhaleWandFt(w: sil.MagicWand): Stmt
 
+  def setCheckReadPermissionOnly(readOnly: Boolean): Boolean
+
+  def assumePermUpperBounds(doAssume: Boolean): Stmt
+
 }

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

@@ -190,6 +190,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     override def translateFunction(f: sil.Function, names: Option[mutable.Map[String, String]]): Seq[Decl] = {
     env = Environment(verifier, f)
     ErrorMemberMapping.currentMember = f
+
+    val oldCheckReadPermOnly = permModule.setCheckReadPermissionOnly(!verifier.respectFunctionPrecPermAmounts)
     val res = MaybeCommentedDecl(s"Translation of function ${f.name}",
       MaybeCommentedDecl("Uninterpreted function definitions", functionDefinitions(f), size = 1) ++
         (if (f.isAbstract) Nil else
@@ -207,6 +209,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
       names.get ++= usedNames
     }
 
+    permModule.setCheckReadPermissionOnly(oldCheckReadPermOnly)
     env = null
     ErrorMemberMapping.currentMember = null
     res
@@ -642,7 +645,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     val args = f.formalArgs map translateLocalVarDecl
     val res = sil.Result(f.typ)()
     val init : Stmt = MaybeCommentBlock("Initializing the state",
-      stateModule.initBoogieState ++ (f.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ++ assumeFunctionsAt(heights(f.name)))
+      stateModule.initBoogieState ++ (if (verifier.respectFunctionPrecPermAmounts) Nil else permModule.assumePermUpperBounds(false)) ++
+        (f.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ++ assumeFunctionsAt(heights(f.name)))
     val checkPre : Stmt = checkFunctionPreconditionDefinedness(f)
     val checkExp : Stmt = if (f.isAbstract) MaybeCommentBlock("(no definition for abstract function)",Nil) else
       MaybeCommentBlock("Check definedness of function body",
@@ -665,7 +669,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
     val args = p.formalArgs map translateLocalVarDecl
     val init : Stmt = MaybeCommentBlock("Initializing the state",
-      stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
+      stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++
+        (if (verifier.respectFunctionPrecPermAmounts) Nil else permModule.assumePermUpperBounds(true)) ++
+        (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
     )
 
     val predicateBody = p.body.get
@@ -871,12 +877,17 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
                     * contain permission introspection.
                     */
                   val curState = stateModule.state
+                  val oldCheckReadPermOnly = permModule.setCheckReadPermissionOnly(!verifier.respectFunctionPrecPermAmounts)
                   defState.setDefState()
                   val res = executeExhale()
+                  permModule.setCheckReadPermissionOnly(oldCheckReadPermOnly)
                   stateModule.replaceState(curState)
                   res
                 case None =>
-                  executeExhale()
+                  val oldCheckReadPermOnly = permModule.setCheckReadPermissionOnly(!verifier.respectFunctionPrecPermAmounts)
+                  val res = executeExhale()
+                  permModule.setCheckReadPermissionOnly(oldCheckReadPermOnly)
+                  res
               }
             }
           ) ++
@@ -961,7 +972,10 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
             wandModule.translatingStmtsInWandInit()
           }
           (checkDefinedness(acc, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
-            checkDefinedness(perm, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
+            // If no permission amount is supplied explicitly, we always use the default FullPerm; this is
+            // okay even if we are inside a function and only want to check for some positive amount, because permission
+            // amounts do not matter in this context.
+            checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
             foldFirst, foldLast)
         }
       }
@@ -998,7 +1012,10 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     unfold match {
       case sil.Unfold(acc@sil.PredicateAccessPredicate(pa@sil.PredicateAccess(_, _), perm)) =>
         checkDefinedness(acc, errors.UnfoldFailed(unfold), insidePackageStmt = insidePackageStmt) ++
-          checkDefinedness(perm, errors.UnfoldFailed(unfold)) ++
+          // If no permission amount is supplied explicitly, we always use the default FullPerm; this is
+          // okay even if we are inside a function and only want to check for some positive amount, because permission
+          // amounts do not matter in this context.
+          checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.UnfoldFailed(unfold)) ++
           unfoldPredicate(acc, errors.UnfoldFailed(unfold), false, statesStackForPackageStmt, insidePackageStmt)
     }
   }

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

@@ -137,7 +137,8 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles
             val initOldStateComment = "Initializing of old state"
             val ins: Seq[LocalVarDecl] = formalArgs map translateLocalVarDecl
             val outs: Seq[LocalVarDecl] = formalReturns map translateLocalVarDecl
-            val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ stmtModule.initStmt(method.bodyOrAssumeFalse))
+            val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++
+              (if (verifier.respectFunctionPrecPermAmounts) Nil else permModule.assumePermUpperBounds(true)) ++ stmtModule.initStmt(method.bodyOrAssumeFalse))
             val initOld = MaybeCommentBlock("Initializing the old state", stateModule.initOldState)
             val paramAssumptions = mWithLoopInfo.formalArgs map (a => allAssumptionsAboutValue(a.typ, translateLocalVarDecl(a), true))
             val inhalePre = translateMethodDeclPre(pres)
@@ -269,9 +270,9 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles
     val resourceCurPerm =
       q.exp match {
         case r : sil.FieldAccess =>
-          sil.FieldAccessPredicate(r, curPermVar)()
+          sil.FieldAccessPredicate(r, Some(curPermVar))()
         case r: sil.PredicateAccess =>
-          sil.PredicateAccessPredicate(r, curPermVar)()
+          sil.PredicateAccessPredicate(r, Some(curPermVar))()
         case _ => sys.error("Not supported resource in quasihavoc")
       }