From ffb9b41abafa22a101a338a71a46c318bd2f927b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 17:39:50 +0200 Subject: [PATCH 01/10] Asserting read permission only for function preconditions and inside functions --- .../resources/ResourceDescriptions.scala | 28 +++++++---- src/main/scala/rules/ChunkSupporter.scala | 10 +++- src/main/scala/rules/Evaluator.scala | 7 +-- .../rules/MoreCompleteExhaleSupporter.scala | 9 ++-- .../scala/rules/QuantifiedChunkSupport.scala | 46 ++++++++++++++++++- src/main/scala/rules/StateConsolidator.scala | 6 +-- src/main/scala/state/State.scala | 16 ++++--- .../functions/FunctionVerificationUnit.scala | 2 +- 8 files changed, 95 insertions(+), 29 deletions(-) diff --git a/src/main/scala/resources/ResourceDescriptions.scala b/src/main/scala/resources/ResourceDescriptions.scala index 5efb397ae..be8289b98 100644 --- a/src/main/scala/resources/ResourceDescriptions.scala +++ b/src/main/scala/resources/ResourceDescriptions.scala @@ -14,16 +14,18 @@ package viper.silicon.resources *
  • 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 This() literal.
    • *
  • Delayed properties are static properties that are only assumed after a state consolidation.
    • + *
  • The flag withPermUpperBounds determines if properties that set upper bounds for permission amounts should + * be included.
    • * */ 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(withPermUpperBounds: Boolean) = Seq(permAtLeastZero) + override def delayedProperties(withPermUpperBounds: Boolean) = Seq(valNeqImpliesLocNeq) def permAtLeastZero: Property = { val description = "Permissions are non-negative" @@ -47,8 +49,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 +87,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" diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 311063b26..10eae1533 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -155,13 +155,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)) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 943002243..e2c00f8c3 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -918,7 +918,8 @@ object evaluator extends EvaluationRules { * incomplete). */ smDomainNeeded = true, - moreJoins = JoinMode.Off) + moreJoins = JoinMode.Off, + assertReadAccessOnly= 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) @@ -944,8 +945,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 diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 1739866e1..b685553b0 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -208,15 +208,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, ve, v)(Q) else - summariseHeapAndAssertReadAccess(s, h, resource, args, argsExp, ve, v)(Q) + summariseHeapAndAssertReadAccess(s, h, resource, perms, args, argsExp, ve, v)(Q) } private def summariseHeapAndAssertReadAccess(s: State, h: Heap, resource: ast.Resource, + perm: Term, args: Seq[Term], argsExp: Option[Seq[ast.Exp]], ve: VerificationError, @@ -228,7 +229,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val relevantChunks = findChunksWithID[NonQuantifiedChunk](h.values, id).toSeq 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 => @@ -336,7 +337,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) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 37a7a26b8..e6d1c32a2 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1016,7 +1016,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val resourceDescription = Resources.resourceDescriptions(ch.resourceID) val interpreter = new QuantifiedPropertyInterpreter - resourceDescription.instanceProperties.foreach (property => { + resourceDescription.instanceProperties(s.mayAssumeUpperBounds).foreach (property => { v.decider.prover.comment(property.description) val (pcsForChunk, pcsForChunkExp) = interpreter.buildPathConditionForChunk( chunk = ch, @@ -1104,7 +1104,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v) val resourceDescription = Resources.resourceDescriptions(ch.resourceID) - val pcs = interpreter.buildPathConditionsForChunk(ch, resourceDescription.instanceProperties) + val pcs = interpreter.buildPathConditionsForChunk(ch, resourceDescription.instanceProperties(s.mayAssumeUpperBounds)) pcs.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2)))) val resourceIdentifier = resource match { @@ -1517,6 +1517,43 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { } } + def assertReadPermission(s: State, + candidates: Seq[QuantifiedBasicChunk], + codomainQVars: Seq[Var], + condition: Term, + perms: Term, + permsExp: Option[ast.Exp], + v: Verifier) + : ConsumptionResult = { + + var success = false + var permsAvailable: Term = NoPerm + var permsAvailableExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()()) + + var tookEnoughCheck: Term = False + + for (ch <- candidates) { + if (!success) { + permsAvailable = PermPlus(permsAvailable, ch.perm) + permsAvailableExp = permsAvailableExp.map(pae => ast.PermAdd(pae, permsExp.get)()) + + tookEnoughCheck = + Forall(codomainQVars, Implies(condition, Implies(Greater(perms, NoPerm), Greater(permsAvailable, NoPerm))), Nil) + + success = v.decider.check(tookEnoughCheck, Verifier.config.splitTimeout()) + } + } + + // final check + val result = + if (success || v.decider.check(tookEnoughCheck, Verifier.config.assertTimeout.getOrElse(0)) /* This check is a must-check, i.e. an assert */ ) + Complete() + else + Incomplete(PermMinus(permsAvailable, perms), permsAvailableExp.map(pa => ast.PermSub(pa, permsExp.get)())) + + result + } + // TODO: Consider taking a single term λr.q(r) that maps to a permission amount, // as done in my thesis def removePermissions(s: State, @@ -1548,6 +1585,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { else chunkOrderHeuristic(relevantChunks) val constrainPermissions = !consumeExactRead(perms, s.constrainableARPs) + if (s.assertReadAccessOnly) { + val result = assertReadPermission(s, candidates, codomainQVars, condition, perms, permsExp, v) + return (result, s, relevantChunks) + } + var remainingChunks = Vector.empty[QuantifiedBasicChunk] var permsNeeded = perms diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index a8e292100..ca44e08e1 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -98,12 +98,12 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol mergedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => 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)))) } Resources.resourceDescriptions foreach { case (id, desc) => - val pathCond = interpreter.buildPathConditionsForResource(id, desc.delayedProperties) + val pathCond = interpreter.buildPathConditionsForResource(id, desc.delayedProperties(s.mayAssumeUpperBounds)) pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2)))) } @@ -138,7 +138,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) newlyAddedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => 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)))) } diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 25f9e5fdd..2b2a3d6fc 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -17,7 +17,7 @@ import viper.silicon.interfaces.state.GeneralChunk import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms.{Term, Var} import viper.silicon.interfaces.state.Chunk -import viper.silicon.state.terms.{And, Ite, NoPerm} +import viper.silicon.state.terms.{And, Ite} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.ast.BigAnd @@ -64,7 +64,7 @@ final case class State(g: Store = Store(), exhaleExt: Boolean = false, ssCache: SsCache = Map.empty, - hackIssue387DisablePermissionConsumption: Boolean = false, + assertReadAccessOnly: Boolean = false, qpFields: InsertionOrderedSet[ast.Field] = InsertionOrderedSet.empty, qpPredicates: InsertionOrderedSet[ast.Predicate] = InsertionOrderedSet.empty, @@ -88,6 +88,10 @@ final case class State(g: Store = Store(), currentMember.isEmpty || currentMember.get.isInstanceOf[ast.Method] } + val mayAssumeUpperBounds: Boolean = { + currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] + } + val isLastRetry: Boolean = retryLevel == 0 def incCycleCounter(m: ast.Predicate) = @@ -172,7 +176,7 @@ object State { partiallyConsumedHeap1, permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, hackIssue387DisablePermissionConsumption1, + ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins) => @@ -197,7 +201,7 @@ object State { `partiallyConsumedHeap1`, `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, `reserveHeaps1`, `reserveCfgs1`, `conservedPcs1`, `recordPcs1`, `exhaleExt1`, - ssCache2, `hackIssue387DisablePermissionConsumption1`, + ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`) => @@ -322,7 +326,7 @@ object State { partiallyConsumedHeap1, permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, - ssCache1, hackIssue387DisablePermissionConsumption1, + ssCache1, assertReadAccessOnly1, qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins) => @@ -346,7 +350,7 @@ object State { partiallyConsumedHeap2, `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`, reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, - ssCache2, `hackIssue387DisablePermissionConsumption1`, + ssCache2, `assertReadAccessOnly1`, `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`) => diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 7fe942e80..2bfcebb50 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -163,7 +163,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver private def handleFunction(sInit: State, function: ast.Function): VerificationResult = { val data = functionData(function) - val s = sInit.copy(functionRecorder = ActualFunctionRecorder(data), conservingSnapshotGeneration = true) + val s = sInit.copy(functionRecorder = ActualFunctionRecorder(data), conservingSnapshotGeneration = true, assertReadAccessOnly = true) /* Phase 1: Check well-definedness of the specifications */ checkSpecificationWelldefinedness(s, function) match { From f49fee0bac1129185b9851d50048e449d1e11256 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 20:25:30 +0200 Subject: [PATCH 02/10] Assert-read-only function preconditions --- silver | 2 +- .../scala/rules/QuantifiedChunkSupport.scala | 18 ++++++------------ 2 files changed, 7 insertions(+), 13 deletions(-) diff --git a/silver b/silver index f649c0baf..d6d6e65fc 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit f649c0baf2fc133a5d99261dbb567b8a33732588 +Subproject commit d6d6e65fceb454ee6c6e16c8dcbc50d70b7fd481 diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index e6d1c32a2..583e413e0 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1526,27 +1526,21 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v: Verifier) : ConsumptionResult = { - var success = false var permsAvailable: Term = NoPerm var permsAvailableExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()()) - var tookEnoughCheck: Term = False for (ch <- candidates) { - if (!success) { - permsAvailable = PermPlus(permsAvailable, ch.perm) - permsAvailableExp = permsAvailableExp.map(pae => ast.PermAdd(pae, permsExp.get)()) - - tookEnoughCheck = - Forall(codomainQVars, Implies(condition, Implies(Greater(perms, NoPerm), Greater(permsAvailable, NoPerm))), Nil) - - success = v.decider.check(tookEnoughCheck, Verifier.config.splitTimeout()) - } + permsAvailable = PermPlus(permsAvailable, ch.perm) + permsAvailableExp = permsAvailableExp.map(pae => ast.PermAdd(pae, permsExp.get)()) } + val tookEnoughCheck = + Forall(codomainQVars, Implies(condition, Implies(Greater(perms, NoPerm), Greater(permsAvailable, NoPerm))), Nil) + // final check val result = - if (success || v.decider.check(tookEnoughCheck, Verifier.config.assertTimeout.getOrElse(0)) /* This check is a must-check, i.e. an assert */ ) + if (v.decider.check(tookEnoughCheck, Verifier.config.assertTimeout.getOrElse(0)) /* This check is a must-check, i.e. an assert */ ) Complete() else Incomplete(PermMinus(permsAvailable, perms), permsAvailableExp.map(pa => ast.PermSub(pa, permsExp.get)())) From 0ed3647d0edc738b9716ec79560822088cbd8c51 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 13 Oct 2024 21:58:46 +0200 Subject: [PATCH 03/10] Update test annotation --- silver | 2 +- src/test/resources/moreCompleteExhale/0523.vpr | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/silver b/silver index d6d6e65fc..89dce6fde 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d6d6e65fceb454ee6c6e16c8dcbc50d70b7fd481 +Subproject commit 89dce6fde51d0a9bebf6db83c8968a5778be5a1f diff --git a/src/test/resources/moreCompleteExhale/0523.vpr b/src/test/resources/moreCompleteExhale/0523.vpr index 7b0414fb7..13d6e9241 100644 --- a/src/test/resources/moreCompleteExhale/0523.vpr +++ b/src/test/resources/moreCompleteExhale/0523.vpr @@ -9,9 +9,9 @@ function req(x: Ref): Bool method test(x: Ref) { inhale acc(x.f) - //:: ExpectedOutput(application.precondition:insufficient.permission) - assert req(x) // Fails only without --enableMoreCompleteExhale (and should fail) - assert false // Fails even with --enableMoreCompleteExhale (and should fail) + assert req(x) + //:: ExpectedOutput(assert.failed:assertion.false) + assert false } From c6fe45de7427bd29561f239b89f967d34e2c48ef Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Oct 2024 15:14:54 +0200 Subject: [PATCH 04/10] Fix test --- silver | 2 +- src/test/resources/moreCompleteExhale/0523.vpr | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/silver b/silver index 89dce6fde..a0fbf3aa6 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 89dce6fde51d0a9bebf6db83c8968a5778be5a1f +Subproject commit a0fbf3aa6f1d375e2f59a6c350d696856ec7dc5e diff --git a/src/test/resources/moreCompleteExhale/0523.vpr b/src/test/resources/moreCompleteExhale/0523.vpr index 13d6e9241..ea880aaf2 100644 --- a/src/test/resources/moreCompleteExhale/0523.vpr +++ b/src/test/resources/moreCompleteExhale/0523.vpr @@ -33,5 +33,4 @@ predicate SomePredicate_pkg_F(param_pkg_V0: Ref) { method client2_pkg_F(param_pkg_V0: Ref) returns (res_pkg_V0: Int) requires acc(SomePredicate_pkg_F(param_pkg_V0), 1 / 2) ensures acc(SomePredicate_pkg_F(param_pkg_V0), 1 / 2) - //:: ExpectedOutput(application.precondition:insufficient.permission) ensures res_pkg_V0 == getter_pkg_F(param_pkg_V0) \ No newline at end of file From acc2948b7f671bf2d38ce83b41375ed43c7e5254 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Oct 2024 15:37:20 +0200 Subject: [PATCH 05/10] Support command line option to enable old behavior --- src/main/scala/rules/Evaluator.scala | 2 +- src/main/scala/state/State.scala | 2 +- .../scala/supporters/functions/FunctionVerificationUnit.scala | 4 +++- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index fc722b037..bcebdf36e 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -919,7 +919,7 @@ object evaluator extends EvaluationRules { */ smDomainNeeded = true, moreJoins = JoinMode.Off, - assertReadAccessOnly= true) + assertReadAccessOnly = if (Verifier.config.respectFunctionPrecPermAmounts()) 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) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 2b2a3d6fc..5e5d8fc16 100644 --- a/src/main/scala/state/State.scala +++ b/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] + currentMember.isEmpty || !currentMember.get.isInstanceOf[ast.Function] || Verifier.config.respectFunctionPrecPermAmounts() } val isLastRetry: Boolean = retryLevel == 0 diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 2bfcebb50..9c38b34ee 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -163,7 +163,9 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver private def handleFunction(sInit: State, function: ast.Function): VerificationResult = { val data = functionData(function) - val s = sInit.copy(functionRecorder = ActualFunctionRecorder(data), conservingSnapshotGeneration = true, assertReadAccessOnly = true) + val s = sInit.copy(functionRecorder = ActualFunctionRecorder(data), + conservingSnapshotGeneration = true, + assertReadAccessOnly = !Verifier.config.respectFunctionPrecPermAmounts()) /* Phase 1: Check well-definedness of the specifications */ checkSpecificationWelldefinedness(s, function) match { From 1a87e5702290976f3d20bdd0a68c9428ac8059ae Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 15 Oct 2024 15:37:27 +0200 Subject: [PATCH 06/10] Update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index a0fbf3aa6..626437b04 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit a0fbf3aa6f1d375e2f59a6c350d696856ec7dc5e +Subproject commit 626437b04aaa354061246f8d07831ad8effdeb93 From dcb326cfc4236c7f57e4216db1260c56ffa48b5b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 22 Oct 2024 14:35:11 +0200 Subject: [PATCH 07/10] Making permission amounts in access predicates optional --- silver | 2 +- .../ConditionalPermissionRewriter.scala | 25 +++++++++++-------- src/main/scala/rules/Evaluator.scala | 4 +-- src/main/scala/rules/Executor.scala | 6 +++-- src/main/scala/rules/Producer.scala | 6 +++-- 5 files changed, 26 insertions(+), 17 deletions(-) diff --git a/silver b/silver index 10b1b26a2..4509152c3 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 +Subproject commit 4509152c35ae7ceda9441c47dcc25cce962d47c0 diff --git a/src/main/scala/extensions/ConditionalPermissionRewriter.scala b/src/main/scala/extensions/ConditionalPermissionRewriter.scala index 817c5c036..8db3f3237 100644 --- a/src/main/scala/extensions/ConditionalPermissionRewriter.scala +++ b/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(_)), + predicates = noTernaryProgram.predicates.map(nonFunctionRewriter.execute(_)), + methods = noTernaryProgram.methods.map(nonFunctionRewriter.execute(_)))(noTernaryProgram.pos, noTernaryProgram.info, noTernaryProgram.errT) res } @@ -114,7 +118,7 @@ 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) @@ -122,18 +126,19 @@ class ConditionalPermissionRewriter { // 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 => diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 943002243..547cda6e0 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -962,7 +962,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) => { @@ -1015,7 +1015,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) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index a19e85d65..be40c6170 100644 --- a/src/main/scala/rules/Executor.scala +++ b/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) => diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index a80fd7a2f..fda78f5ca 100644 --- a/src/main/scala/rules/Producer.scala +++ b/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) => { From 9ad99ebd16b997b3b4b1a9988c9cd8ac2b32699b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 22 Oct 2024 15:11:32 +0200 Subject: [PATCH 08/10] Fixed two issues --- silver | 2 +- .../scala/extensions/ConditionalPermissionRewriter.scala | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/silver b/silver index 4509152c3..fe1884045 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 4509152c35ae7ceda9441c47dcc25cce962d47c0 +Subproject commit fe188404530dd080d26755228568dd64ca8cf17d diff --git a/src/main/scala/extensions/ConditionalPermissionRewriter.scala b/src/main/scala/extensions/ConditionalPermissionRewriter.scala index 8db3f3237..24120e10c 100644 --- a/src/main/scala/extensions/ConditionalPermissionRewriter.scala +++ b/src/main/scala/extensions/ConditionalPermissionRewriter.scala @@ -105,9 +105,9 @@ class ConditionalPermissionRewriter { val noTernaryProgram: Program = ternaryRewriter.execute(root) 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(_)), - predicates = noTernaryProgram.predicates.map(nonFunctionRewriter.execute(_)), - methods = noTernaryProgram.methods.map(nonFunctionRewriter.execute(_)))(noTernaryProgram.pos, noTernaryProgram.info, noTernaryProgram.errT) + 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 } From f7229cdb7f39616ef98e6eb78e7bad26db24b52d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 22 Oct 2024 17:07:32 +0200 Subject: [PATCH 09/10] Update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 999ef97a1..aac52daab 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 999ef97a18f6d23c3d4a9e7114488b10d5df8540 +Subproject commit aac52daab393e3ce98148e30ed54808aedd3af54 From e6f4a2f4c21ac99f3c79546c9a41dd9653635394 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 2 Dec 2024 14:19:56 +0100 Subject: [PATCH 10/10] Incorporated review comments --- src/main/scala/resources/ResourceDescriptions.scala | 6 ++++-- src/main/scala/rules/Evaluator.scala | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/main/scala/resources/ResourceDescriptions.scala b/src/main/scala/resources/ResourceDescriptions.scala index be8289b98..9153b56e5 100644 --- a/src/main/scala/resources/ResourceDescriptions.scala +++ b/src/main/scala/resources/ResourceDescriptions.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. *
      @@ -24,8 +26,8 @@ trait ResourceDescription { } abstract class BasicDescription extends ResourceDescription { - override def instanceProperties(withPermUpperBounds: Boolean) = Seq(permAtLeastZero) - override def delayedProperties(withPermUpperBounds: Boolean) = 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" diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 01f370115..87e5cf810 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -919,7 +919,8 @@ object evaluator extends EvaluationRules { */ smDomainNeeded = true, moreJoins = JoinMode.Off, - assertReadAccessOnly = if (Verifier.config.respectFunctionPrePermAmounts()) s2.assertReadAccessOnly else true) + 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)