Assert-read-only function preconditions

viperproject · Oct 13, 2024 · 6a7280c · 6a7280c
1 parent 8638bfa
commit 6a7280c
Show file tree

Hide file tree

Showing 5 changed files with 74 additions and 26 deletions.
diff --git a/silver b/silver
diff --git a/src/main/scala/viper/carbon/modules/PermModule.scala b/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
+
 }
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/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(true)
     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
@@ -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
               }
             }
           ) ++

diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala b/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)

diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/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())),
@@ -195,7 +201,7 @@ class QuantifiedPermModule(val verifier: Verifier)
       Axiom(Forall(staticStateContributions(true, true) ++ obj ++ field,
         Trigger(Seq(staticGoodMask, perm)),
         // permissions are non-negative
-        (staticGoodMask ==> ( perm >= noPerm &&
+        ((staticGoodMask && assumePermUpperBound) ==> ( 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 )))
@@ -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))) ++
-            If(permVar !== noPerm,
-              Assert(permLe(permVar, curPerm), error.dueTo(reasons.InsufficientPermission(loc))),
-              Nil) ++
-            subtractFromMask(permVar)
+              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)
+          }
         } 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) =>
 
@@ -546,8 +572,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 +635,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 +742,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 +832,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,7 +1045,7 @@ 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
@@ -1171,7 +1207,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)
+2 −1		src/main/scala/viper/silver/ast/Program.scala
+17 −0		src/main/scala/viper/silver/ast/utility/Consistency.scala
+5 −2		src/main/scala/viper/silver/frontend/SilFrontend.scala
+5 −0		src/main/scala/viper/silver/reporter/Message.scala
+7 −0		src/main/scala/viper/silver/reporter/Reporter.scala
+2 −2		src/main/scala/viper/silver/verifier/VerificationResult.scala
+300 −0		src/test/resources/all/functions/function_precondition_perms.vpr
+8 −8		src/test/resources/all/issues/carbon/0196.vpr
+1 −1		src/test/resources/all/issues/carbon/0223.vpr
+2 −9		src/test/resources/all/issues/silicon/0030.vpr
+5 −5		src/test/resources/all/issues/silicon/0240.vpr
+1 −0		src/test/resources/all/issues/silicon/0376.vpr