Checking only read permissions when asserting function preconditions

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

@@ -159,4 +159,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 setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean
+
+  def assumePermUpperBounds: 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 oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(!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.setCheckReadPermissionOnlyState(oldPermOnlyState)
     env = null
     ErrorMemberMapping.currentMember = null
     res
@@ -665,7 +668,7 @@ 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 ++ permModule.assumePermUpperBounds ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
     )
 
     val predicateBody = p.body.get
@@ -871,12 +874,17 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
                     * contain permission introspection.
                     */
                   val curState = stateModule.state
+                  val oldReadState = permModule.setCheckReadPermissionOnlyState(true)
                   defState.setDefState()
                   val res = executeExhale()
+                  permModule.setCheckReadPermissionOnlyState(oldReadState)
                   stateModule.replaceState(curState)
                   res
                 case None =>
-                  executeExhale()
+                  val oldReadState = permModule.setCheckReadPermissionOnlyState(true)
+                  val res = executeExhale()
+                  permModule.setCheckReadPermissionOnlyState(oldReadState)
+                  res
               }
             }
           ) ++
@@ -961,7 +969,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
             wandModule.translatingStmtsInWandInit()
           }
           (checkDefinedness(acc, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
-            checkDefinedness(perm, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
+            checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
             foldFirst, foldLast)
         }
       }
@@ -998,7 +1006,7 @@ 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)) ++
+          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,7 @@ 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 ++ permModule.assumePermUpperBounds ++ 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 +269,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")
       }
 

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

@@ -103,6 +103,9 @@ class QuantifiedPermModule(val verifier: Verifier)
   private val predicateMaskFieldName = Identifier("PredicateMaskField")
   private val wandMaskFieldName = Identifier("WandMaskField")
 
+  private val assumePermUpperBoundName = Identifier("AssumePermUpperBound")
+  private val assumePermUpperBound: Const = Const(assumePermUpperBoundName)
+
 
   private val resultMask = LocalVarDecl(Identifier("ResultMask"),maskType)
   private val summandMask1 = LocalVarDecl(Identifier("SummandMask1"),maskType)
@@ -122,6 +125,8 @@ class QuantifiedPermModule(val verifier: Verifier)
   private var rangeFuncs: ListBuffer[Func] = new ListBuffer[Func](); //list of inverse functions used for inhale/exhale qp
   private var triggerFuncs: ListBuffer[Func] = new ListBuffer[Func](); //list of inverse functions used for inhale/exhale qp
 
+  private var assertReadPermOnly: Boolean = false
+
   private val readMaskName = Identifier("readMask")
   private val updateMaskName = Identifier("updMask")
 
@@ -159,6 +164,7 @@ class QuantifiedPermModule(val verifier: Verifier)
         Seq(obj, field),
         Trigger(permInZeroPMask),
         permInZeroPMask === FalseLit())) ::
+      ConstDecl(assumePermUpperBoundName, Bool) ::
       // predicate mask function
       Func(predicateMaskFieldName,
         Seq(LocalVarDecl(Identifier("f"), predicateVersionFieldType())),
@@ -192,13 +198,13 @@ class QuantifiedPermModule(val verifier: Verifier)
         Trigger(Seq(staticGoodState)),
         staticGoodState ==> staticGoodMask)) ++ {
       val perm = currentPermission(obj.l, field.l)
+      val shouldAssumePermUpperBound = if (verifier.respectFunctionPrecPermAmounts) TrueLit() else assumePermUpperBound
       Axiom(Forall(staticStateContributions(true, true) ++ obj ++ field,
         Trigger(Seq(staticGoodMask, perm)),
         // permissions are non-negative
         (staticGoodMask ==> ( perm >= noPerm &&
-          // permissions for fields which aren't predicates are smaller than 1
           // permissions for fields which aren't predicates or wands are smaller than 1
-          ((staticGoodMask && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm )))
+          ((staticGoodMask && shouldAssumePermUpperBound && heapModule.isPredicateField(field.l).not && heapModule.isWandField(field.l).not) ==> perm <= fullPerm )))
       ))    } ++ {
       val obj = LocalVarDecl(Identifier("o")(axiomNamespace), refType)
       val field = LocalVarDecl(Identifier("f")(axiomNamespace), fieldType)
@@ -240,6 +246,10 @@ class QuantifiedPermModule(val verifier: Verifier)
 
   def permType = NamedType(permTypeName)
 
+  override def assumePermUpperBounds: Stmt = {
+    Assume(assumePermUpperBound)
+  }
+
   def staticStateContributions(withHeap: Boolean, withPermissions: Boolean): Seq[LocalVarDecl] = if (withPermissions) Seq(LocalVarDecl(maskName, maskType)) else Seq()
   def currentStateContributions: Seq[LocalVarDecl] = Seq(LocalVarDecl(mask.name, maskType))
   def currentStateVars : Seq[Var] = Seq(mask)
@@ -259,6 +269,13 @@ class QuantifiedPermModule(val verifier: Verifier)
     inverseFuncs = new ListBuffer[Func]();
     rangeFuncs = new ListBuffer[Func]();
     triggerFuncs = new ListBuffer[Func]();
+    assertReadPermOnly = false
+  }
+
+  override def setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean = {
+    val oldState = assertReadPermOnly
+    assertReadPermOnly = readOnly
+    oldState
   }
 
   override def usingOldState = stateModuleIsUsingOldState
@@ -367,15 +384,20 @@ class QuantifiedPermModule(val verifier: Verifier)
           (if (!usingOldState) currentMaskAssignUpdate(loc, permSub(curPerm, permToExhale)) else Nil)
 
         val permVar = LocalVar(Identifier("perm"), permType)
-        if (!p.isInstanceOf[sil.WildcardPerm]) {
-          val prmTranslated = translatePerm(p)
-
+        if (assertReadPermOnly || !p.isInstanceOf[sil.WildcardPerm]) {
+          val prmTranslated = if (p.isInstanceOf[sil.WildcardPerm]) fullPerm else translatePerm(p)
+          if (assertReadPermOnly) {
+            (permVar := prmTranslated) ++
+              Assert(permissionPositiveInternal(permVar, Some(p), true), error.dueTo(reasons.NegativePermission(p))) ++
+              Assert(permLt(noPerm, permVar) ==> permLt(noPerm, curPerm), error.dueTo(reasons.InsufficientPermission(loc)))
+          } else {
             (permVar := prmTranslated) ++
               Assert(permissionPositiveInternal(permVar, Some(p), true), error.dueTo(reasons.NegativePermission(p))) ++
-            If(permVar !== noPerm,
-              Assert(permLe(permVar, curPerm), error.dueTo(reasons.InsufficientPermission(loc))),
-              Nil) ++
-            subtractFromMask(permVar)
+              If(permVar !== noPerm,
+                Assert(permLe(permVar, curPerm), error.dueTo(reasons.InsufficientPermission(loc))),
+                Nil) ++
+              subtractFromMask(permVar)
+          }
         } else {
           val curPerm = currentPermission(loc)
           val wildcard = LocalVar(Identifier("wildcard"), Real)
@@ -389,9 +411,13 @@ class QuantifiedPermModule(val verifier: Verifier)
       case w@sil.MagicWand(_,_) =>
         val wandRep = wandModule.getWandRepresentation(w)
         val curPerm = currentPermission(translateNull, wandRep)
+        val sufficientPermExp = if (assertReadPermOnly)
+          curPerm > noPerm
+        else
+          permLe(fullPerm, curPerm)
         Comment("permLe")++
-          Assert(permLe(fullPerm, curPerm), error.dueTo(reasons.MagicWandChunkNotFound(w))) ++
-          (if (!usingOldState) currentMaskAssignUpdate(translateNull, wandRep, permSub(curPerm, fullPerm)) else Nil)
+          Assert(sufficientPermExp, error.dueTo(reasons.MagicWandChunkNotFound(w))) ++
+          (if (!usingOldState && !assertReadPermOnly) currentMaskAssignUpdate(translateNull, wandRep, permSub(curPerm, fullPerm)) else Nil)
 
       case fa@sil.Forall(v, cond, expr) =>
 
@@ -470,13 +496,14 @@ class QuantifiedPermModule(val verifier: Verifier)
         val vs = forall.variables
 
         val res = expr match {
-          case sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), perms) =>
+          case accPred@sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), _) =>
             // alpha renaming, to avoid clashes in context, use vFresh instead of v
             val vsFresh = vs.map(v => {
               val vFresh = env.makeUniquelyNamed(v)
               env.define(vFresh.localVar)
               vFresh
             })
+            val perms = accPred.perm
 
             var isWildcard = false
             def renaming[E <: sil.Exp] = (e:E) => Expressions.renameVariables(e, vs.map(v => v.localVar), vsFresh.map(v => v.localVar))
@@ -546,8 +573,10 @@ class QuantifiedPermModule(val verifier: Verifier)
 
             //define permission requirement
             val permNeeded =
-              if(isWildcard) {
-            currentPermission(translatedRecv, translatedLocation) > noPerm
+              if(assertReadPermOnly) {
+                translatedPerms > noPerm ==> currentPermission(translatedRecv, translatedLocation) > noPerm
+              } else if (isWildcard) {
+                currentPermission(translatedRecv, translatedLocation) > noPerm
               } else {
                 currentPermission(translatedRecv, translatedLocation) >= translatedPerms
               }
@@ -607,16 +636,19 @@ class QuantifiedPermModule(val verifier: Verifier)
             }
             val injectiveAssertion = Assert(is_injective, err)
 
+            val maskUpdateStmt = if (assertReadPermOnly) Nil else
+              CommentBlock("assume permission updates for field " + f.name, Assume(Forall(obj, triggersForPermissionUpdateAxiom, condTrueLocations && condFalseLocations))) ++
+              CommentBlock("assume permission updates for independent locations", independentLocations) ++
+              (mask := qpMask)
+
             val res1 = Havoc(qpMask) ++
               MaybeComment("wild card assumptions", stmts ++
               wildcardAssms) ++
               CommentBlock("check that the permission amount is positive", permPositive) ++
               CommentBlock("check if receiver " + recv.toString + " is injective",injectiveAssertion) ++
               CommentBlock("check if sufficient permission is held", enoughPerm) ++
               CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
-              CommentBlock("assume permission updates for field " + f.name, Assume(Forall(obj,triggersForPermissionUpdateAxiom, condTrueLocations && condFalseLocations ))) ++
-              CommentBlock("assume permission updates for independent locations", independentLocations) ++
-              (mask := qpMask)
+              maskUpdateStmt
 
             vsFresh.foreach(v => env.undefine(v.localVar))
 
@@ -711,8 +743,10 @@ class QuantifiedPermModule(val verifier: Verifier)
 
             //check that sufficient permission is held
             val permNeeded =
-              if(isWildcard) {
-                (currentPermission(translateNull, translatedResource) > RealLit(0))
+              if(assertReadPermOnly) {
+                translatedPerms > noPerm ==> (currentPermission(translateNull, translatedResource) > noPerm)
+              } else if (isWildcard) {
+                (currentPermission(translateNull, translatedResource) > noPerm)
               } else {
                 (currentPermission(translateNull, translatedResource) >= translatedPerms)
               }
@@ -799,17 +833,20 @@ class QuantifiedPermModule(val verifier: Verifier)
             }
             val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err)
 
+            val maskUpdateStmts = if (assertReadPermOnly) Nil else
+              CommentBlock("assume permission updates", permissionsMap ++
+              independentResource) ++
+              CommentBlock("assume permission updates for independent locations ", independentLocations) ++
+              (mask := qpMask)
+
             val res1 = Havoc(qpMask) ++
               MaybeComment("wildcard assumptions", stmts ++
               wildcardAssms) ++
               CommentBlock("check that the permission amount is positive", permPositive) ++
               CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion) ++
               CommentBlock("check if sufficient permission is held", enoughPerm) ++
               CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
-              CommentBlock("assume permission updates", permissionsMap ++
-              independentResource) ++
-              CommentBlock("assume permission updates for independent locations ", independentLocations) ++
-              (mask := qpMask)
+              maskUpdateStmts
 
             vsFresh.foreach(vFresh => env.undefine(vFresh.localVar))
             freshFormalDecls.foreach(x => env.undefine(x.localVar))
@@ -1009,11 +1046,12 @@ class QuantifiedPermModule(val verifier: Verifier)
    */
   def translateInhale(e: sil.Forall, error: PartialVerificationError): Stmt = e match{
     case SourceQuantifiedPermissionAssertion(forall, Implies(cond, expr)) =>
-      val vs = forall.variables // TODO: Generalise to multiple quantified variables
+      val vs = forall.variables
 
        val res = expr match {
          //Quantified Field Permission
-         case sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), perms) =>
+         case accPred@sil.FieldAccessPredicate(fieldAccess@sil.FieldAccess(recv, f), _) =>
+           val perms = accPred.perm
            // alpha renaming, to avoid clashes in context, use vFresh instead of v
            var isWildcard = false
            val vsFresh = vs.map(v => env.makeUniquelyNamed(v))
@@ -1171,7 +1209,7 @@ class QuantifiedPermModule(val verifier: Verifier)
              (if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", permPositive) else Nil) ++
              CommentBlock("Assume set of fields is nonNull", nonNullAssumptions) ++
             // CommentBlock("Assume injectivity", injectiveAssumption) ++
-             CommentBlock("Define permissions", Assume(Forall(obj,triggerForPermissionUpdateAxiom, condTrueLocations&&condFalseLocations )) ++
+             CommentBlock("Define permissions", Assume(Forall(obj, triggerForPermissionUpdateAxiom, condTrueLocations && condFalseLocations)) ++
                independentLocations) ++
              (mask := qpMask)
 
@@ -1489,7 +1527,13 @@ class QuantifiedPermModule(val verifier: Verifier)
       case sil.FullPerm() =>
         fullPerm
       case sil.WildcardPerm() =>
-        sys.error("cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)")
+        if (assertReadPermOnly) {
+          // We are in a context where permission amounts do not matter, so we can safely translate a wildcard to
+          // a full permission.
+          fullPerm
+        } else {
+          sys.error("cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)")
+        }
       case sil.EpsilonPerm() =>
         sys.error("epsilon permissions are not supported by this permission module")
       case sil.CurrentPerm(res: ResourceAccess) =>

src/main/scala/viper/carbon/verifier/Verifier.scala

@@ -80,4 +80,6 @@ trait Verifier {
 
   def usePolyMapsInEncoding: Boolean
 
+  def respectFunctionPrecPermAmounts: Boolean
+
 }