Checking only read permissions when asserting function preconditions (#877)

Author: marcoeilers

silver

@@ -20,7 +20,7 @@ import scala.collection.mutable
   *
   */
 class ConditionalPermissionRewriter {
-  private def rewriter(implicit p: Program, alreadySeen: mutable.HashSet[Exp]) = ViperStrategy.Context[Condition]({
+  private def rewriter(implicit p: Program, isFunction: Boolean, alreadySeen: mutable.HashSet[Exp]) = ViperStrategy.Context[Condition]({
     // Does NOT rewrite ternary expressions; those have to be transformed to implications in advance
     // using the ternaryRewriter below.
     //
@@ -32,8 +32,8 @@ class ConditionalPermissionRewriter {
       // Transformation causes issues if the permission involve a wildcard, so we avoid that case.
       // Also, we cannot push perm and forperm expressions further in, since their value may be different at different
       // places in the same assertion.
-      val res = if (!acc.perm.contains[WildcardPerm] && !Expressions.containsPermissionIntrospection(cond))
-        (conditionalize(acc, cc.c &*& cond), cc) // Won't recurse into acc's children (see recurseFunc below)
+      val res = if ((isFunction || !acc.perm.contains[WildcardPerm]) && !Expressions.containsPermissionIntrospection(cond))
+        (conditionalize(acc, cc.c &*& cond, isFunction), cc) // Won't recurse into acc's children (see recurseFunc below)
       else
         (Implies(And(cc.c.exp, cond)(), acc)(i.pos, i.info, i.errT), cc)
       alreadySeen.add(res._1)
@@ -61,8 +61,8 @@ class ConditionalPermissionRewriter {
     case (acc: AccessPredicate, cc) if cc.c.optExp.nonEmpty =>
       // Found an accessibility predicate nested under some conditionals
       // Wildcards may cause issues, see above.
-      val res = if (!acc.perm.contains[WildcardPerm])
-        (conditionalize(acc, cc.c), cc) // Won't recurse into acc's children
+      val res = if (isFunction || !acc.perm.contains[WildcardPerm])
+        (conditionalize(acc, cc.c, isFunction), cc) // Won't recurse into acc's children
       else
         (Implies(cc.c.exp, acc)(acc.pos, acc.info, acc.errT), cc)
       alreadySeen.add(res._1)
@@ -103,7 +103,11 @@ class ConditionalPermissionRewriter {
     */
   def rewrite(root: Program): Program = {
     val noTernaryProgram: Program = ternaryRewriter.execute(root)
-    val res: Program = rewriter(root, new mutable.HashSet[Exp]()).execute(noTernaryProgram)
+    val functionRewriter = rewriter(root, true, new mutable.HashSet[Exp]())
+    val nonFunctionRewriter = rewriter(root, false, new mutable.HashSet[Exp]())
+    val res = noTernaryProgram.copy(functions = noTernaryProgram.functions.map(functionRewriter.execute[Function](_)),
+      predicates = noTernaryProgram.predicates.map(nonFunctionRewriter.execute[Predicate](_)),
+      methods = noTernaryProgram.methods.map(nonFunctionRewriter.execute[Method](_)))(noTernaryProgram.pos, noTernaryProgram.info, noTernaryProgram.errT)
     res
   }
 
@@ -114,26 +118,27 @@ class ConditionalPermissionRewriter {
 
   /** Makes `acc`'s permissions conditional w.r.t. `cond`.
     */
-  private def conditionalize(acc: AccessPredicate, cond: Condition)(implicit p: Program): Exp = {
+  private def conditionalize(acc: AccessPredicate, cond: Condition, isFunction: Boolean)(implicit p: Program): Exp = {
     // We have to be careful not to introduce well-definedness issues when conditionalizing.
     // For example, if we transform
     // i >= 0 && i < |s| ==> acc(s[i].f)
     // to
     // acc(s[i].f, i >= 0 && i < |s| ? write : none)
     // then backends may complain that s[i].f is not well-defined. Thus, we only perform the
     // transformation if receiver/argument expressions are always well-defined.
+    val defaultPerm = if (isFunction) WildcardPerm()() else FullPerm()()
     acc match {
       case FieldAccessPredicate(loc, perm) =>
         if (Expressions.proofObligations(loc.rcv)(p).isEmpty) {
-          FieldAccessPredicate(loc, makeCondExp(cond.exp, perm))(acc.pos, acc.info, acc.errT)
+          FieldAccessPredicate(loc, Some(makeCondExp(cond.exp, perm.getOrElse(defaultPerm))))(acc.pos, acc.info, acc.errT)
         } else {
           // Hack: use a conditional null as the receiver, that's always well-defined.
           val fieldAccess = loc.copy(rcv = makeCondExp(cond.exp, loc.rcv, NullLit()()))(loc.pos, loc.info, loc.errT)
-          FieldAccessPredicate(fieldAccess, makeCondExp(cond.exp, perm))(acc.pos, acc.info, acc.errT)
+          FieldAccessPredicate(fieldAccess, Some(makeCondExp(cond.exp, perm.getOrElse(defaultPerm))))(acc.pos, acc.info, acc.errT)
         }
       case PredicateAccessPredicate(loc, perm) =>
         if (!loc.args.exists(a => Expressions.proofObligations(a)(p).nonEmpty))
-          PredicateAccessPredicate(loc, makeCondExp(cond.exp, perm))(acc.pos, acc.info, acc.errT)
+          PredicateAccessPredicate(loc, Some(makeCondExp(cond.exp, perm.getOrElse(defaultPerm))))(acc.pos, acc.info, acc.errT)
         else
           Implies(cond.exp, acc)(acc.pos, acc.info, acc.errT)
       case wand: MagicWand =>

src/main/scala/extensions/ConditionalPermissionRewriter.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.resources
 
+import scala.annotation.unused
+
 /**
   * A resource description contains the assumptions that are added at several points during verificaton.
   * <ul>
@@ -14,16 +16,18 @@ package viper.silicon.resources
   *   <li>Static properties are also assumed when a new chunk is added to the heap. They descripe properties of the whole heap
   *   and are not allowed to contain the <code>This()</code> literal.</li>
   *   <li>Delayed properties are static properties that are only assumed after a state consolidation.</li>
+  *   <li>The flag withPermUpperBounds determines if properties that set upper bounds for permission amounts should
+  *   be included.</li>
   *  </ul>
   */
 trait ResourceDescription {
-  val instanceProperties: Seq[Property]
-  val delayedProperties: Seq[Property]
+  def instanceProperties(withPermUpperBounds: Boolean): Seq[Property]
+  def delayedProperties(withPermUpperBounds: Boolean): Seq[Property]
 }
 
 abstract class BasicDescription extends ResourceDescription {
-  override val instanceProperties = Seq(permAtLeastZero)
-  override val delayedProperties = Seq(valNeqImpliesLocNeq)
+  override def instanceProperties(@unused withPermUpperBounds: Boolean) = Seq(permAtLeastZero)
+  override def delayedProperties(@unused withPermUpperBounds: Boolean) = Seq(valNeqImpliesLocNeq)
 
   def permAtLeastZero: Property = {
     val description = "Permissions are non-negative"
@@ -47,8 +51,18 @@ class PredicateDescription extends BasicDescription {
 }
 
 class FieldDescription extends BasicDescription {
-  override val instanceProperties = Seq(permAtLeastZero, permAtMostOne, permImpliesNonNull)
-  override val delayedProperties = Seq(permUpperBoundDiseq, valNeqImpliesLocNeq)
+  override def instanceProperties(withPermUpperBounds: Boolean) = {
+    if (withPermUpperBounds)
+      Seq(permAtLeastZero, permAtMostOne, permImpliesNonNull)
+    else
+      Seq(permAtLeastZero, permImpliesNonNull)
+  }
+  override def delayedProperties(withPermUpperBounds: Boolean) = {
+    if (withPermUpperBounds)
+      Seq(permUpperBoundDiseq, valNeqImpliesLocNeq)
+    else
+      Seq(valNeqImpliesLocNeq)
+  }
 
   def permAtMostOne: Property = {
     val description = "Field permissions are at most one"
@@ -75,8 +89,8 @@ class FieldDescription extends BasicDescription {
 }
 
 class MagicWandDescription extends ResourceDescription {
-  override val instanceProperties = Seq(permAtLeastZero)
-  override val delayedProperties = Seq[Property]()
+  override def instanceProperties(withPermUpperBounds: Boolean) = Seq(permAtLeastZero)
+  override def delayedProperties(withPermUpperBounds: Boolean) = Seq[Property]()
 
   def permAtLeastZero: Property = {
     val description = "Permissons are non-negative"

src/main/scala/resources/ResourceDescriptions.scala

@@ -163,13 +163,19 @@ object chunkSupporter extends ChunkSupportRules {
     def assumeProperties(chunk: NonQuantifiedChunk, heap: Heap): Unit = {
       val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v)
       val resource = Resources.resourceDescriptions(chunk.resourceID)
-      val pathCond = interpreter.buildPathConditionsForChunk(chunk, resource.instanceProperties)
+      val pathCond = interpreter.buildPathConditionsForChunk(chunk, resource.instanceProperties(s.mayAssumeUpperBounds))
       pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
     }
 
     findChunk[NonQuantifiedChunk](h.values, id, args, v) match {
       case Some(ch) =>
-        if (consumeExact) {
+        if (s.assertReadAccessOnly) {
+          if (v.decider.check(Implies(IsPositive(perms), IsPositive(ch.perm)), Verifier.config.assertTimeout.getOrElse(0))) {
+            (Complete(), s, h, Some(ch))
+          } else {
+            (Incomplete(perms, permsExp), s, h, None)
+          }
+        } else if (consumeExact) {
           val toTake = PermMin(ch.perm, perms)
           val toTakeExp = permsExp.map(pe => buildMinExp(Seq(ch.permExp.get, pe), ast.Perm))
           val newPermExp = permsExp.map(pe => ast.PermSub(ch.permExp.get, toTakeExp.get)(pe.pos, pe.info, pe.errT))

src/main/scala/rules/ChunkSupporter.scala

@@ -924,7 +924,9 @@ object evaluator extends EvaluationRules {
                                  * incomplete).
                                  */
                              smDomainNeeded = true,
-                             moreJoins = JoinMode.Off)
+                             moreJoins = JoinMode.Off,
+                             assertReadAccessOnly = if (Verifier.config.respectFunctionPrePermAmounts())
+                               s2.assertReadAccessOnly /* should currently always be false */ else true)
             consumes(s3, pres, true, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.get.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
@@ -950,8 +952,8 @@ object evaluator extends EvaluationRules {
                                recordVisited = s2.recordVisited,
                                functionRecorder = fr5,
                                smDomainNeeded = s2.smDomainNeeded,
-                               hackIssue387DisablePermissionConsumption = s.hackIssue387DisablePermissionConsumption,
-                               moreJoins = s2.moreJoins)
+                               moreJoins = s2.moreJoins,
+                               assertReadAccessOnly = s2.assertReadAccessOnly)
               val funcAppNew = eArgsNew.map(args => ast.FuncApp(funcName, args)(fapp.pos, fapp.info, fapp.typ, fapp.errT))
               QB(s5, (tFApp, funcAppNew), v3)})
             /* TODO: The join-function is heap-independent, and it is not obvious how a
@@ -968,7 +970,7 @@ object evaluator extends EvaluationRules {
         if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) {
           v.decider.startDebugSubExp()
           evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
-            eval(s1, ePerm, pve, v1)((s2, tPerm, ePermNew, v2) =>
+            eval(s1, ePerm.getOrElse(ast.FullPerm()()), pve, v1)((s2, tPerm, ePermNew, v2) =>
               v2.decider.assert(IsPositive(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative
                 case true =>
                   joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s2, v2)((s3, v3, QB) => {
@@ -1021,7 +1023,7 @@ object evaluator extends EvaluationRules {
                     Q(s12, r12._1, r12._2, v7)})
                 case false =>
                   v2.decider.finishDebugSubExp(s"unfolded(${predicate.name})")
-                  createFailure(pve dueTo NonPositivePermission(ePerm), v2, s2, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}))
+                  createFailure(pve dueTo NonPositivePermission(ePerm.get), v2, s2, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}))
         } else {
           val unknownValue = v.decider.appliedFresh("recunf", v.symbolConverter.toSort(eIn.typ), s.relevantQuantifiedVariables.map(_._1))
           Q(s, unknownValue, Option.when(withExp)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)

src/main/scala/rules/Evaluator.scala

@@ -601,8 +601,9 @@ object executor extends ExecutionRules {
               v3.symbExLog.closeScope(sepIdentifier)
               Q(s6, v3)})})})
 
-      case fold @ ast.Fold(ast.PredicateAccessPredicate(predAcc @ ast.PredicateAccess(eArgs, predicateName), ePerm)) =>
+      case fold @ ast.Fold(pap @ ast.PredicateAccessPredicate(predAcc @ ast.PredicateAccess(eArgs, predicateName), _)) =>
         v.decider.startDebugSubExp()
+        val ePerm = pap.perm
         val predicate = s.program.findPredicate(predicateName)
         val pve = FoldFailed(fold)
         evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
@@ -615,8 +616,9 @@ object executor extends ExecutionRules {
                 }
               )})))
 
-      case unfold @ ast.Unfold(ast.PredicateAccessPredicate(pa @ ast.PredicateAccess(eArgs, predicateName), ePerm)) =>
+      case unfold @ ast.Unfold(pap @ ast.PredicateAccessPredicate(pa @ ast.PredicateAccess(eArgs, predicateName), _)) =>
         v.decider.startDebugSubExp()
+        val ePerm = pap.perm
         val predicate = s.program.findPredicate(predicateName)
         val pve = UnfoldFailed(unfold)
         evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>

src/main/scala/rules/Executor.scala

@@ -233,16 +233,16 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                      (Q: (State, Heap, Option[Term], Verifier) => VerificationResult)
                      : VerificationResult = {
 
-    if (!s.hackIssue387DisablePermissionConsumption)
+    if (!s.assertReadAccessOnly)
       actualConsumeComplete(s, h, resource, args, argsExp, perms, permsExp, returnSnap, ve, v)(Q)
-    else {
-      summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, returnSnap, ve, v)(Q)
-    }
+    else
+      summariseHeapAndAssertReadAccess(s, h, resource, perms, args, argsExp, returnSnap, ve, v)(Q)
   }
 
   private def summariseHeapAndAssertReadAccess(s: State,
                                                h: Heap,
                                                resource: ast.Resource,
+                                               perm: Term,
                                                args: Seq[Term],
                                                argsExp: Option[Seq[ast.Exp]],
                                                returnSnap: Boolean,
@@ -253,17 +253,18 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     val id = ChunkIdentifier(resource, s.program)
     val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq
+
     if (returnSnap) {
       summarise(s, relevantChunks, resource, args, argsExp, None, v)((s1, snap, permSum, permSumExp, v1) =>
-        v.decider.assert(IsPositive(permSum)) {
+        v.decider.assert(Implies(IsPositive(perm), IsPositive(permSum))) {
           case true =>
             Q(s1, h, Some(snap), v1)
           case false =>
             createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)()))
         })
     } else {
       val (s1, permSum, permSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp)
-      v.decider.assert(IsPositive(permSum)) {
+      v.decider.assert(Implies(IsPositive(perm), IsPositive(permSum))) {
         case true =>
           Q(s1, h, None, v)
         case false =>
@@ -374,7 +375,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v)
         newChunks foreach { ch =>
           val resource = Resources.resourceDescriptions(ch.resourceID)
-          val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)
+          val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties(s.mayAssumeUpperBounds))
           pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
         }
         val newHeap = Heap(allChunks)

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -317,7 +317,8 @@ object producer extends ProductionRules {
         letSupporter.handle[ast.Exp](s, let, pve, v)((s1, g1, body, v1) =>
           produceR(s1.copy(g = s1.g + g1), sf, body, pve, v1)(Q))
 
-      case accPred@ast.FieldAccessPredicate(ast.FieldAccess(eRcvr, field), perm) =>
+      case accPred@ast.FieldAccessPredicate(ast.FieldAccess(eRcvr, field), _) =>
+        val perm = accPred.perm
         eval(s, eRcvr, pve, v)((s1, tRcvr, eRcvrNew, v1) =>
           eval(s1, perm, pve, v1)((s2, tPerm, ePermNew, v2) =>
             permissionSupporter.assertNotNegative(s2, tPerm, perm, ePermNew, pve, v2)((s3, v3) => {
@@ -341,8 +342,9 @@ object producer extends ProductionRules {
                   Q(s6, v4)
                 })}})))
 
-      case ast.PredicateAccessPredicate(ast.PredicateAccess(eArgs, predicateName), perm) =>
+      case accPred @ ast.PredicateAccessPredicate(ast.PredicateAccess(eArgs, predicateName), _) =>
         val predicate = s.program.findPredicate(predicateName)
+        val perm = accPred.perm
         evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
           eval(s1, perm, pve, v1)((s1a, tPerm, ePermNew, v1a) =>
             permissionSupporter.assertNotNegative(s1a, tPerm, perm, ePermNew, pve, v1a)((s2, v2) => {