Adapting to renamed config field

src/main/scala/extensions/ConditionalPermissionRewriter.scala

@@ -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/rules/Evaluator.scala

@@ -919,7 +919,7 @@ object evaluator extends EvaluationRules {
                                  */
                              smDomainNeeded = true,
                              moreJoins = JoinMode.Off,
-                             assertReadAccessOnly = if (Verifier.config.respectFunctionPrecPermAmounts()) s2.assertReadAccessOnly else true)
+                             assertReadAccessOnly = if (Verifier.config.respectFunctionPrePermAmounts()) s2.assertReadAccessOnly else true)
             consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
@@ -963,7 +963,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) => {
@@ -1016,7 +1016,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/Executor.scala

@@ -596,8 +596,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) =>
@@ -610,8 +611,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/Producer.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) => {
@@ -337,8 +338,9 @@ object producer extends ProductionRules {
                   Q(s4.copy(h = h4), 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) => {

src/main/scala/state/State.scala

@@ -89,7 +89,7 @@ final case class State(g: Store = Store(),
   }
 
   val mayAssumeUpperBounds: Boolean = {
-    currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || Verifier.config.respectFunctionPrecPermAmounts()
+    currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || Verifier.config.respectFunctionPrePermAmounts()
   }
 
   val isLastRetry: Boolean = retryLevel == 0

src/main/scala/supporters/functions/FunctionVerificationUnit.scala

@@ -165,7 +165,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
       val data = functionData(function)
       val s = sInit.copy(functionRecorder = ActualFunctionRecorder(data),
         conservingSnapshotGeneration = true,
-        assertReadAccessOnly = !Verifier.config.respectFunctionPrecPermAmounts())
+        assertReadAccessOnly = !Verifier.config.respectFunctionPrePermAmounts())
 
       /* Phase 1: Check well-definedness of the specifications */
       checkSpecificationWelldefinedness(s, function) match {