diff --git a/silver b/silver deleted file mode 160000 index 10b1b26a2..000000000 --- a/silver +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7 diff --git a/silver b/silver new file mode 120000 index 000000000..fa266af11 --- /dev/null +++ b/silver @@ -0,0 +1 @@ +../silver \ No newline at end of file diff --git a/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala b/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala index 37621ea33..f7f1e8d81 100644 --- a/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala +++ b/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala @@ -9,12 +9,12 @@ package viper.silicon.resources import viper.silicon.Map import viper.silicon.interfaces.state._ import viper.silicon.state.terms.Term -import viper.silicon.state.{QuantifiedBasicChunk, terms} +import viper.silicon.state.{QuantifiedBasicChunk, State, terms} import viper.silicon.utils.ast.{BigAnd, replaceVarsInExp} import viper.silicon.verifier.Verifier import viper.silver.ast -class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier) extends PropertyInterpreter { +class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier, state: State) extends PropertyInterpreter { protected case class Info(pm: Map[ChunkPlaceholder, GeneralChunk], resourceID: ResourceID) { def addMapping(cp: ChunkPlaceholder, ch: GeneralChunk) = Info(pm + (cp -> ch), resourceID) @@ -114,6 +114,36 @@ class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier } } + protected def buildPrHasUpperBound(chunkPlaceholder: ChunkPlaceholder, info: Info) = { + val chunk = info.pm(chunkPlaceholder) + val pred = state.program.findPredicate(chunk.id.toString) + if (state.predicateData(pred).upperBoundTerm.isDefined) + buildPathCondition(True(), info) + else + buildPathCondition(False(), info) + } + + protected def buildUpperBoundAccess(chunkPlaceholder: ChunkPlaceholder, info: Info) = { + val chunk = info.pm(chunkPlaceholder) + val pred = state.program.findPredicate(chunk.id.toString) + val ubData = (state.predicateData(pred).upperBoundTerm, state.predicateData(pred).upperBoundExp) + require(ubData._1.isDefined) + chunk match { + case _: NonQuantifiedChunk => + if(withExp) + (ubData._1.get, ubData._2) + else + (ubData._1.get, None) + // TODO: remove once singleton quantified chunks are not used anymore + case c: QuantifiedBasicChunk => + val permTerm = ubData._1.get.replace(c.quantifiedVars, c.singletonArguments.get) + if (withExp) + (permTerm, Some(replaceVarsInExp(ubData._2.get, c.quantifiedVarExps.get.map(_.name), c.singletonArgumentExps.get))) + else + (permTerm, None) + } + } + override protected def buildCheck[K <: IteUsableKind] (condition: PropertyExpression[kinds.Boolean], thenDo: PropertyExpression[K], diff --git a/src/main/scala/resources/PropertyExpressions.scala b/src/main/scala/resources/PropertyExpressions.scala index 5932ba72b..d2a66c95d 100644 --- a/src/main/scala/resources/PropertyExpressions.scala +++ b/src/main/scala/resources/PropertyExpressions.scala @@ -90,5 +90,7 @@ case class This() extends ChunkPlaceholder { case class ArgumentAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Argument] case class PermissionAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Permission] case class ValueAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Value] +case class UpperBoundAccess(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Permission] +case class PrHasUpperBound(chunk: ChunkPlaceholder) extends PropertyExpression[kinds.Boolean] case class Null() extends PropertyExpression[kinds.Argument] diff --git a/src/main/scala/resources/PropertyInterpreter.scala b/src/main/scala/resources/PropertyInterpreter.scala index b4b74bd43..c3ec378f8 100644 --- a/src/main/scala/resources/PropertyInterpreter.scala +++ b/src/main/scala/resources/PropertyInterpreter.scala @@ -56,6 +56,8 @@ abstract class PropertyInterpreter { // Chunk accessors case PermissionAccess(cv) => buildPermissionAccess(cv, info) case ValueAccess(cv) => buildValueAccess(cv, info) + case PrHasUpperBound(cv) => buildPrHasUpperBound(cv, info) + case UpperBoundAccess(cv) => buildUpperBoundAccess(cv, info) // decider / heap interaction case Check(condition, thenDo, otherwise) => buildCheck(condition, thenDo, otherwise, info) @@ -72,6 +74,8 @@ abstract class PropertyInterpreter { protected def buildPermissionAccess(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp]) protected def buildValueAccess(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp]) + protected def buildUpperBoundAccess(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp]) + protected def buildPrHasUpperBound(chunkVariable: ChunkPlaceholder, info: Info): (Term, Option[ast.Exp]) /* Assures that if the left-hand side is known to be false without a prover check, the right-hand side is not evaluated. */ diff --git a/src/main/scala/resources/QuantifiedPropertyInterpreter.scala b/src/main/scala/resources/QuantifiedPropertyInterpreter.scala index 09510ad7a..ee2067fa8 100644 --- a/src/main/scala/resources/QuantifiedPropertyInterpreter.scala +++ b/src/main/scala/resources/QuantifiedPropertyInterpreter.scala @@ -55,6 +55,12 @@ class QuantifiedPropertyInterpreter extends PropertyInterpreter { (info.args, info.argsExp) } + override protected def buildUpperBoundAccess(chunkPlaceholder: ChunkPlaceholder, info: Info) = { + sys.error("UpperBoundAccess clauses are not supported in quantified properties.") + } + override protected def buildPrHasUpperBound(chunkPlaceholder: ChunkPlaceholder, info: Info) = buildPathCondition(False(), info) + + override protected def buildCheck[K <: IteUsableKind] (condition: PropertyExpression[kinds.Boolean], thenDo: PropertyExpression[K], diff --git a/src/main/scala/resources/ResourceDescriptions.scala b/src/main/scala/resources/ResourceDescriptions.scala index 5efb397ae..7e5e5fe17 100644 --- a/src/main/scala/resources/ResourceDescriptions.scala +++ b/src/main/scala/resources/ResourceDescriptions.scala @@ -43,7 +43,32 @@ abstract class BasicDescription extends ResourceDescription { } class PredicateDescription extends BasicDescription { + override val instanceProperties = Seq(permAtLeastZero, permAtMostN) + override val delayedProperties = Seq(permUpperBoundDiseq, valNeqImpliesLocNeq) override def toString = "Predicate" + + def permAtMostN: Property = { + val description = "Predicate permissions are at most n" + val name = "permAtMostN" + val cond = PrHasUpperBound(This()) + val thenDo = And(cond, LessThanEquals(PermissionAccess(This()), UpperBoundAccess(This()))) + Property(Or(Not(cond), thenDo), name, description) + } + + def permUpperBoundDiseq: Property = { + val description = "Permission sum greater than n implies non-equal receivers" + val name = "permUpperBoundDiseq" + val c1 = ChunkVariable("c1") + val c2 = ChunkVariable("c2") + val perm1 = PermissionAccess(c1) + val perm2 = PermissionAccess(c2) + val greaterThan = GreaterThan(Plus(perm1, perm2), UpperBoundAccess(c1)) + val neq = Not(Equals(ArgumentAccess(c1), ArgumentAccess(c2))) + val cond = PrHasUpperBound(c1) + val thenDo = And(cond, Check(greaterThan, neq, True())) + Property(ForEach(Seq(c1, c2), Or(Not(cond), thenDo)), name, description) + } + } class FieldDescription extends BasicDescription { diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 311063b26..a4932d842 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -9,7 +9,8 @@ package viper.silicon.rules import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.state._ import viper.silicon.interfaces.{Success, VerificationResult} -import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, Resources} +import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, PredicateID, Resources} +import viper.silicon.Map import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.state.terms.perms.IsPositive @@ -152,8 +153,8 @@ object chunkSupporter extends ChunkSupportRules { val consumeExact = terms.utils.consumeExactRead(perms, s.constrainableARPs) - def assumeProperties(chunk: NonQuantifiedChunk, heap: Heap): Unit = { - val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v) + def assumeProperties(chunk: NonQuantifiedChunk, heap: Heap, s: State): Unit = { + val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v, s) val resource = Resources.resourceDescriptions(chunk.resourceID) val pathCond = interpreter.buildPathConditionsForChunk(chunk, resource.instanceProperties) pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2)))) @@ -170,7 +171,7 @@ object chunkSupporter extends ChunkSupportRules { var newHeap = h - ch if (!v.decider.check(newChunk.perm === NoPerm, Verifier.config.checkTimeout())) { newHeap = newHeap + newChunk - assumeProperties(newChunk, newHeap) + assumeProperties(newChunk, newHeap, s) } val remainingExp = permsExp.map(pe => ast.PermSub(pe, toTakeExp.get)(pe.pos, pe.info, pe.errT)) (ConsumptionResult(PermMinus(perms, toTake), remainingExp, Seq(), v, 0), s, newHeap, takenChunk) @@ -182,7 +183,7 @@ object chunkSupporter extends ChunkSupportRules { val newChunk = ch.withPerm(PermMinus(ch.perm, perms), newPermExp) val takenChunk = ch.withPerm(perms, permsExp) val newHeap = h - ch + newChunk - assumeProperties(newChunk, newHeap) + assumeProperties(newChunk, newHeap, s) (Complete(), s, newHeap, Some(takenChunk)) } else { (Incomplete(perms, permsExp), s, h, None) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 1739866e1..3e5c78e10 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -333,7 +333,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val allChunks = otherChunks ++ newChunks // TODO: Since no permissions were gained, I don't see why the PropertyInterpreter would yield any new assumptions. // See if it can be removed here. - val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v) + val interpreter = new NonQuantifiedPropertyInterpreter(allChunks, v, s) newChunks foreach { ch => val resource = Resources.resourceDescriptions(ch.resourceID) val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index a80fd7a2f..46cc8e6d2 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -354,7 +354,19 @@ object producer extends ProductionRules { val formalArgs = s2.predicateFormalVarMap(predicate) val trigger = (sm: Term) => PredicateTrigger(predicate.name, sm, tArgs) quantifiedChunkSupporter.produceSingleLocation( - s2, predicate, formalArgs, Option.when(withExp)(predicate.formalArgs), tArgs, eArgsNew, snap, gain, gainExp, trigger, v2)(Q) + s2, predicate, formalArgs, Option.when(withExp)(predicate.formalArgs), tArgs, eArgsNew, snap, gain, gainExp, trigger, v2)((s3, v3) => { + val predData = s3.predicateData(predicate) + (predData.upperBoundExp, predData.upperBoundTerm) match { + case (Some(ub), None) => eval(s3, ub, pve, v3)((s4a, tUb, eUbNew, v4a) => { + permissionSupporter.assertNotNegative(s4a, tUb, ub, eUbNew, pve, v4a)((s5, v5) => { + val tmp = s5.predicateData(predicate) + tmp.upperBoundTerm = Some(tUb) + Q(s5.copy(predicateData = s5.predicateData + (predicate -> tmp)), v5) + }) + }) + case (_, _) => Q(s3, v3) + } + }) } else { val snap1 = snap.convert(sorts.Snap) val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgsNew, snap1, gain, gainExp) @@ -365,7 +377,18 @@ object producer extends ProductionRules { val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($argsString))", isInternal_ = true)) v3.decider.assume(App(s3.predicateData(predicate).triggerFunction, snap1 +: tArgs), debugExp) } - Q(s3.copy(h = h3), v3)}) + val predData = s3.predicateData(predicate) + (predData.upperBoundExp, predData.upperBoundTerm) match { + case (Some(ub), None) => eval(s3.copy(h = h3), ub, pve, v3)((s4a, tUb, eUbNew, v4a) => { + permissionSupporter.assertNotNegative(s4a, tUb, ub, eUbNew, pve, v4a)((s5, v5) => { + val tmp = s5.predicateData(predicate) + tmp.upperBoundTerm = Some(tUb) + Q(s5.copy(predicateData = s5.predicateData + (predicate -> tmp)), v5) + }) + }) + case (_, _) => Q(s3.copy(h = h3), v3) + } + }) }}))) case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) => @@ -488,7 +511,19 @@ object producer extends ProductionRules { NegativePermission(acc.perm), QPAssertionNotInjective(acc.loc), v1 - )(Q) + )((s2, v2) => { + val predData = s2.predicateData(predicate) + (predData.upperBoundExp, predData.upperBoundTerm) match { + case (Some(ub), None) => eval(s2, ub, pve, v2)((s4a, tUb, eUbNew, v4a) => { + permissionSupporter.assertNotNegative(s4a, tUb, ub, eUbNew, pve, v4a)((s5, v5) => { + val tmp = s5.predicateData(predicate) + tmp.upperBoundTerm = Some(tUb) + Q(s5.copy(predicateData = s5.predicateData + (predicate -> tmp)), v5) + }) + }) + case (_, _) => Q(s2, v2) + } + }) case (s1, _, _, _, _, None, v1) => Q(s1, v1) } diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 37a7a26b8..a7a17d4ef 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1102,7 +1102,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalQVars, formalQVarsExp, resource, tArgs, eArgs, tPerm, ePerm, sm, s.program) val (fr1, h1) = v.stateConsolidator(s).merge(s.functionRecorder, s, s.h, Heap(Seq(ch)), v) - val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v) + val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v, s) val resourceDescription = Resources.resourceDescriptions(ch.resourceID) val pcs = interpreter.buildPathConditionsForChunk(ch, resourceDescription.instanceProperties) pcs.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2)))) diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index a8e292100..4e91cd29a 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -11,7 +11,8 @@ import viper.silicon.Config import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.interfaces.state._ import viper.silicon.logger.records.data.{CommentRecord, SingleMergeRecord} -import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, Resources} +import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, PredicateID, Resources} +import viper.silicon.Map import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.state.terms.perms._ @@ -31,6 +32,8 @@ trait StateConsolidationRules extends SymbolicExecutionRules { protected def assumeUpperPermissionBoundForQPFields(s: State, v: Verifier): State protected def assumeUpperPermissionBoundForQPFields(s: State, heaps: Seq[Heap], v: Verifier): State + protected def assumeUpperPermissionBoundForQPPredicates(s: State, v: Verifier): State + protected def assumeUpperPermissionBoundForQPPredicates(s: State, heaps: Seq[Heap], v: Verifier): State } /** Performs the minimal work necessary for any consolidator: merging two heaps combines the chunk @@ -51,6 +54,10 @@ class MinimalStateConsolidator extends StateConsolidationRules { protected def assumeUpperPermissionBoundForQPFields(s: State, @unused v: Verifier): State = s protected def assumeUpperPermissionBoundForQPFields(s: State, @unused heaps: Seq[Heap], @unused v: Verifier): State = s + + protected def assumeUpperPermissionBoundForQPPredicates(s: State, @unused v: Verifier): State = s + + protected def assumeUpperPermissionBoundForQPPredicates(s: State, @unused heaps: Seq[Heap], @unused v: Verifier): State = s } /** Default implementation that merges as many known-alias chunks as possible, and deduces various @@ -94,7 +101,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol } while (continue) - val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) + val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v, s) mergedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) @@ -116,8 +123,9 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol reserveHeaps = mergedHeaps.tail) val s2 = assumeUpperPermissionBoundForQPFields(s1, v) + val s3 = assumeUpperPermissionBoundForQPPredicates(s2, v) - s2 + s3 } def consolidateOptionally(s: State, v: Verifier): State = @@ -135,7 +143,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol v.decider.assume(snapEqs, Option.when(withExp)(DebugExp.createInstance("Snapshot", isInternal_ = true)), enforceAssumption = false) - val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v) + val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v, s) newlyAddedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk => val resource = Resources.resourceDescriptions(ch.resourceID) val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties) @@ -199,7 +207,6 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol private def mergeChunks(fr1: FunctionRecorder, chunk1: Chunk, chunk2: Chunk, v: Verifier): Option[(FunctionRecorder, Chunk, Term)] = (chunk1, chunk2) match { case (BasicChunk(rid1, id1, args1, args1Exp, snap1, perm1, perm1Exp), BasicChunk(_, _, _, _, snap2, perm2, perm2Exp)) => val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) - Some(fr2, BasicChunk(rid1, id1, args1, args1Exp, combinedSnap, PermPlus(perm1, perm2), perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())), snapEq) case (l@QuantifiedFieldChunk(id1, fvf1, condition1, condition1Exp, perm1, perm1Exp, invs1, singletonRcvr1, singletonRcvr1Exp, hints1), r@QuantifiedFieldChunk(_, fvf2, _, _, perm2, perm2Exp, _, _, _, hints2)) => @@ -259,7 +266,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val receiver = `?r` val receiverExp = ast.LocalVarDecl(receiver.id.name, ast.Ref)() val args = Seq(receiver) - val chunksPerField: Map[String, Seq[QuantifiedFieldChunk]] = chunks.groupBy(_.id.name) + val chunksPerField: scala.collection.immutable.Map[String, Seq[QuantifiedFieldChunk]] = chunks.groupBy(_.id.name) /* Iterate over all fields f and effectively assume "forall x :: {x.f} perm(x.f) <= write" for each field. Nearly identical to what the evaluator does for perm(x.f) if f is @@ -320,6 +327,86 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol } } + protected def assumeUpperPermissionBoundForQPPredicates(s: State, v: Verifier): State = + assumeUpperPermissionBoundForQPPredicates(s, s.h +: s.reserveHeaps, v) + + protected def assumeUpperPermissionBoundForQPPredicates(s: State, heaps: Seq[Heap], v: Verifier): State = { + heaps.foldLeft(s) { case (si, heap) => + val chunks: Seq[QuantifiedPredicateChunk] = + heap.values.collect({ case ch: QuantifiedPredicateChunk => ch }).to(Seq) + + //val receiver = `?r` + //val receiverExp = ast.LocalVarDecl(receiver.id.name, ast.Ref)() + //val args = Seq(receiver) + val chunksPerPredicate: scala.collection.immutable.Map[String, Seq[QuantifiedPredicateChunk]] = chunks.groupBy(_.id.name) + + /* Iterate over all predicates f with an upperbound and effectively assume "forall x :: f(x) perm(f(x)) <= upperBound" + for each field. */ + chunksPerPredicate.foldLeft(si) { case (si, (predicateName, predicateChunks)) => + val predicate = s.program.findPredicate(predicateName) + val predicateData = s.predicateData(predicate) + val formalVars = s.predicateFormalVarMap(predicate) + val formalVarExps = predicate.formalArgs + val upperBoundTerm = predicateData.upperBoundTerm + val upperBoundExp = predicateData.upperBoundExp + if(upperBoundTerm.isDefined) { + val (sn, smDef, pmDef) = + quantifiedChunkSupporter.heapSummarisingMaps(si, predicate, formalVars, predicateChunks, v) + + if (sn.heapDependentTriggers.exists(r => r.isInstanceOf[ast.Predicate] && r.asInstanceOf[ast.Predicate].name == predicateName)) { + val trigger = PredicateTrigger(predicate.name, smDef.sm, formalVars) + val currentPermAmount = PredicatePermLookup(predicate.name, pmDef.pm, formalVars) + v.decider.prover.comment(s"Assume upper permission bound for predicate ${predicate.name}") + + val debugExp = if (withExp) { + val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.PredicateAccess(formalVarExps.map(v => v.localVar), predicateName)())(), v.getDebugOldLabel(sn))() + val exp = ast.Forall(formalVarExps, Seq(), ast.PermLeCmp(permExp, ast.FullPerm()())())() + Some(DebugExp.createInstance(exp, exp)) + } else { + None + } + v.decider.assume( + Forall(formalVars, PermAtMost(currentPermAmount, upperBoundTerm.get), Trigger(trigger), "qp-pred-prm-bnd"), debugExp) + } else { + /* + If we don't use heap-dependent triggers, the trigger f(x) does not work. Instead, we assume the permission + bound explicitly for each singleton chunk receiver, and for each chunk, triggering on its inverse functions. + That is, we assume + forall r: Ref :: {inv(r)} perm(f(x)) <= upperBound + */ + for (chunk <- predicateChunks) { + if (chunk.singletonArgs.isDefined){ + val debugExp = if (withExp) { + val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.PredicateAccess(chunk.singletonArgExps.get, predicateName)())(), v.getDebugOldLabel(sn))() + val exp = ast.PermLeCmp(permExp, upperBoundExp.get)() + Some(DebugExp.createInstance(exp, exp)) + } else { None } + v.decider.assume(PermAtMost(PredicatePermLookup(predicate.name, pmDef.pm, chunk.singletonArgs.get), upperBoundTerm.get), debugExp) + } else { + val chunkReceivers = chunk.invs.get.inverses.map(i => App(i, chunk.invs.get.additionalArguments ++ chunk.quantifiedVars)) + val triggers = chunkReceivers.map(r => Trigger(r)).toSeq + val currentPermAmount = PredicatePermLookup(predicate.name, pmDef.pm, chunk.quantifiedVars) + v.decider.prover.comment(s"Assume upper permission bound for predicate ${predicate.name}") + val debugExp = if (withExp) { + val chunkReceiverExp = chunk.quantifiedVarExps.get.map(v => v.localVar) + var permExp: ast.Exp = ast.CurrentPerm(ast.PredicateAccess(chunkReceiverExp, predicateName)())() + permExp = ast.DebugLabelledOld(permExp, v.getDebugOldLabel(sn))() + val exp = ast.Forall(chunk.quantifiedVarExps.get, Seq(), ast.PermLeCmp(permExp, upperBoundExp.get)())() + Some(DebugExp.createInstance(exp, exp)) + } else { None } + v.decider.assume( + Forall(chunk.quantifiedVars, PermAtMost(currentPermAmount, upperBoundTerm.get), triggers, "qp-pred-prm-bnd"), debugExp) + } + + } + } + sn + } else + s + } + } + } + @inline private final def partition(h: Heap): (Seq[NonQuantifiedChunk], Seq[Chunk]) = { var nonQuantifiedChunks = Seq[NonQuantifiedChunk]() @@ -390,6 +477,10 @@ class MinimalRetryingStateConsolidator(config: Config) extends RetryingStateCons override protected def assumeUpperPermissionBoundForQPFields(s: State, @unused v: Verifier): State = s override protected def assumeUpperPermissionBoundForQPFields(s: State, @unused heaps: Seq[Heap], @unused v: Verifier): State = s + + override protected def assumeUpperPermissionBoundForQPPredicates(s: State, @unused v: Verifier): State = s + + override protected def assumeUpperPermissionBoundForQPPredicates(s: State, @unused heaps: Seq[Heap], @unused v: Verifier): State = s } /** A variant of [[DefaultStateConsolidator]] that aims to work best when Silicon is run in diff --git a/src/main/scala/supporters/PredicateVerificationUnit.scala b/src/main/scala/supporters/PredicateVerificationUnit.scala index 388c54709..4ce8ef31f 100644 --- a/src/main/scala/supporters/PredicateVerificationUnit.scala +++ b/src/main/scala/supporters/PredicateVerificationUnit.scala @@ -33,6 +33,15 @@ class PredicateData(predicate: ast.Predicate) val triggerFunction = Fun(Identifier(s"${predicate.name}%trigger"), sorts.Snap +: argumentSorts, sorts.Bool) + + val upperBoundExp = { + predicate.upperBound match { + case Some(ub) => require(symbolConvert.toSort(ub.typ) == sorts.Perm, s"Permissions $ub must be of sort Perm, but found ${symbolConvert.toSort(ub.typ)}") + case None => () + } + predicate.upperBound + } + var upperBoundTerm : Option[Term] = None } trait PredicateVerificationUnit @@ -87,10 +96,12 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve openSymbExLogger(predicate) val ins = predicate.formalArgs.map(_.localVar) - val s = sInit.copy(g = Store(ins.map(x => (x, decider.fresh(x)))), + val ubVar = ast.LocalVar("limit", ast.Perm)() + val s = sInit.copy(g = Store(ins.map(x => (x, decider.fresh(x))) ++ Seq((ubVar, decider.fresh(ubVar)))), h = Heap(), oldHeaps = OldHeaps()) val err = PredicateNotWellformed(predicate) + val ubErr = UpperBoundFailed(predicate) val result = predicate.body match { case None => @@ -98,11 +109,25 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve case Some(body) => /* locallyXXX { magicWandSupporter.checkWandsAreSelfFraming(σ.γ, σ.h, predicate, c)} - &&*/ executionFlowController.locally(s, v)((s1, _) => { - produce(s1, freshSnap, body, err, v)((_, _) => - Success())}) + &&*/ + executionFlowController.locally(s, v)((s1, _) => { + produce(s1, freshSnap, body, err, v)((s2, _) => + Success())}) && executionFlowController.locally(s, v)((s1, _) => { + predicate.upperBound match { + case None => + Success() + case Some(ubExp) => + val s3 = s1.scalePermissionFactor(s1.g(ubVar), s1.g.getExp(ubVar)) + produce(s3, freshSnap, ast.And(ast.PermGtCmp(ubVar, ubExp)(), body)(), ubErr, v)((_, _) => + v.decider.assert(terms.False) { + case true => + Success() + case false => + Failure(ubErr.dueTo(InvalidUpperBound(predicate))) + }) + } + }) } - symbExLog.closeMemberScope() Seq(result) }