Skip to content

Commit

Permalink
add permissionScalingFactorExp
Browse files Browse the repository at this point in the history
  • Loading branch information
@AndreaKe
AndreaKe committed Oct 29, 2023
1 parent 18442f3 commit 33d89e6
Show file tree
Hide file tree
Showing 5 changed files with 27 additions and 17 deletions.
3 changes: 2 additions & 1 deletion src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -399,9 +399,10 @@ object consumer extends ConsumptionRules {
permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => {
val resource = locacc.res(s.program)
val loss = PermTimes(tPerm, s3.permissionScalingFactor)
val lossExp = ast.PermMul(perm, s3.permissionScalingFactorExp)(perm.pos, perm.info, perm.errT)
val ve = pve dueTo InsufficientPermission(locacc)
val description = s"consume ${a.pos}: $a"
chunkSupporter.consume(s3, h, resource, tArgs, eArgs, loss, perm, ve, v3, description)((s4, h1, snap1, v4) => { // FIXME ake: scalingFactor
chunkSupporter.consume(s3, h, resource, tArgs, eArgs, loss, lossExp, ve, v3, description)((s4, h1, snap1, v4) => {
val s5 = s4.copy(partiallyConsumedHeap = Some(h1),
constrainableARPs = s.constrainableARPs)
Q(s5, h1, snap1, v4)})})))
Expand Down
7 changes: 4 additions & 3 deletions src/main/scala/rules/Evaluator.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -504,7 +504,7 @@ object evaluator extends EvaluationRules {
s1, predicate, s1.predicateFormalVarMap(predicate), relevantChunks, v1)
if (s2.heapDependentTriggers.contains(predicate)){
val trigger = PredicateTrigger(predicate.name, smDef.sm, args)
val argsString = predicate.formalArgs.map(s2.substituteVarsInExp(_)).mkString(", ")
val argsString = predicate.formalArgs.mkString(", ") // TODO ake: substitution
val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
v1.decider.assume(trigger, debugExp)
}
Expand Down Expand Up @@ -835,14 +835,15 @@ object evaluator extends EvaluationRules {
v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs), debugExp)
}
val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
val s7 = s6.scalePermissionFactor(tPerm)
val s7 = s6.scalePermissionFactor(tPerm, ePerm)
val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip tArgs)
val s7a = s7.copy(g = insg)
produce(s7a, toSf(snap), body, pve, v4)((s8, v5) => {
val s9 = s8.copy(g = s7.g,
functionRecorder = s8.functionRecorder.changeDepthBy(-1),
recordVisited = s3.recordVisited,
permissionScalingFactor = s6.permissionScalingFactor)
permissionScalingFactor = s6.permissionScalingFactor,
permissionScalingFactorExp = s6.permissionScalingFactorExp)
.decCycleCounter(predicate)
val s10 = v5.stateConsolidator.consolidateIfRetrying(s9, v5)
v5.decider.finishDebugSubExp(s"unfolded(${predicate.name})")
Expand Down
16 changes: 10 additions & 6 deletions src/main/scala/rules/PredicateSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ object predicateSupporter extends PredicateSupportRules {
val gIns = s.g + Store(predicate.formalArgs map (_.localVar) zip tArgs)
val s1 = s.copy(g = gIns,
smDomainNeeded = true)
.scalePermissionFactor(tPerm)
.scalePermissionFactor(tPerm, ePerm)
consume(s1, body, pve, v)((s1a, snap, v1) => {
if (!Verifier.config.disableFunctionUnfoldTrigger()) {
val predTrigger = App(s1a.predicateData(predicate).triggerFunction,
Expand Down Expand Up @@ -104,13 +104,15 @@ object predicateSupporter extends PredicateSupportRules {
h = h3,
smCache = smCache,
permissionScalingFactor = s.permissionScalingFactor,
permissionScalingFactorExp = s.permissionScalingFactorExp,
functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef))
Q(s3, v1)
} else {
val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap.convert(sorts.Snap), tPerm, ePerm)
val s3 = s2.copy(g = s.g,
smDomainNeeded = s.smDomainNeeded,
permissionScalingFactor = s.permissionScalingFactor)
permissionScalingFactor = s.permissionScalingFactor,
permissionScalingFactorExp = s.permissionScalingFactorExp)
chunkSupporter.produce(s3, s3.h, ch, v1)((s4, h1, v2) =>
Q(s4.copy(h = h1), v2))
}
Expand All @@ -132,7 +134,7 @@ object predicateSupporter extends PredicateSupportRules {

val gIns = s.g + Store(predicate.formalArgs map (_.localVar) zip tArgs)
val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
val s1 = s.scalePermissionFactor(tPerm)
val s1 = s.scalePermissionFactor(tPerm, ePerm)
if (s1.qpPredicates.contains(predicate)) {
val formalVars = s1.predicateFormalVarMap(predicate)
quantifiedChunkSupporter.consumeSingleLocation(
Expand All @@ -158,13 +160,14 @@ object predicateSupporter extends PredicateSupportRules {
v2.decider.assume(predicateTrigger, new DebugExp(s"Predicate Trigger ${predicate.name}($eargs)"))
}
Q(s4.copy(g = s.g,
permissionScalingFactor = s.permissionScalingFactor),
permissionScalingFactor = s.permissionScalingFactor,
permissionScalingFactorExp = s.permissionScalingFactorExp),
v2)})
})
} else {
val ve = pve dueTo InsufficientPermission(pa)
val description = s"consume ${pa.pos}: $pa"
chunkSupporter.consume(s1, s1.h, predicate, tArgs, eArgs, s1.permissionScalingFactor, ast.FullPerm()(), ve, v, description)((s2, h1, snap, v1) => { // FIXME ake: scalingFactor
chunkSupporter.consume(s1, s1.h, predicate, tArgs, eArgs, s1.permissionScalingFactor, s1.permissionScalingFactorExp, ve, v, description)((s2, h1, snap, v1) => {
val s3 = s2.copy(g = gIns, h = h1)
.setConstrainable(constrainableWildcards, false)
produce(s3, toSf(snap), body, pve, v1)((s4, v2) => {
Expand All @@ -176,7 +179,8 @@ object predicateSupporter extends PredicateSupportRules {
v2.decider.assume(predicateTrigger, new DebugExp(s"Predicate Trigger ${pa.predicateName}($eargs)"))
}
val s5 = s4.copy(g = s.g,
permissionScalingFactor = s.permissionScalingFactor)
permissionScalingFactor = s.permissionScalingFactor,
permissionScalingFactorExp = s.permissionScalingFactorExp)
Q(s5, v2)})})
}
}
Expand Down
6 changes: 4 additions & 2 deletions src/main/scala/rules/Producer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -261,11 +261,12 @@ object producer extends ProductionRules {
permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => {
val snap = sf(v3.symbolConverter.toSort(field.typ), v3)
val gain = PermTimes(tPerm, s3.permissionScalingFactor)
val gainExp = ast.PermMul(perm, s3.permissionScalingFactorExp)(perm.pos, perm.info, perm.errT)
if (s3.qpFields.contains(field)) {
val trigger = (sm: Term) => FieldTrigger(field.name, sm, tRcvr)
quantifiedChunkSupporter.produceSingleLocation(s3, field, Seq(`?r`), Seq(tRcvr), snap, gain, trigger, v3)(Q)
} else {
val ch = BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), Seq(eRcvr), snap, gain, perm) // TODO ake: scaling factor
val ch = BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), Seq(eRcvr), snap, gain, gainExp)
chunkSupporter.produce(s3, s3.h, ch, v3)((s4, h4, v4) =>
Q(s4.copy(h = h4), v4))
}})))
Expand All @@ -279,14 +280,15 @@ object producer extends ProductionRules {
predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
.getOrElse(sorts.Snap), v2)
val gain = PermTimes(tPerm, s2.permissionScalingFactor)
val gainExp = ast.PermMul(perm, s2.permissionScalingFactorExp)(perm.pos, perm.info, perm.errT)
if (s2.qpPredicates.contains(predicate)) {
val formalArgs = s2.predicateFormalVarMap(predicate)
val trigger = (sm: Term) => PredicateTrigger(predicate.name, sm, tArgs)
quantifiedChunkSupporter.produceSingleLocation(
s2, predicate, formalArgs, tArgs, snap, gain, trigger, v2)(Q)
} else {
val snap1 = snap.convert(sorts.Snap)
val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap1, gain, perm) // FIXME ake: scalingFactor
val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap1, gain, gainExp)
chunkSupporter.produce(s2, s2.h, ch, v2)((s3, h3, v3) => {
if (Verifier.config.enablePredicateTriggersOnInhale() && s3.functionRecorder == NoopFunctionRecorder
&& !Verifier.config.disableFunctionUnfoldTrigger()) {
Expand Down
12 changes: 7 additions & 5 deletions src/main/scala/state/State.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,8 @@ final case class State(g: Store = Store(),
retryLevel: Int = 0,
/* ast.Field, ast.Predicate, or MagicWandIdentifier */
heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty,
moreCompleteExhale: Boolean = false)
moreCompleteExhale: Boolean = false,
permissionScalingFactorExp: ast.Exp = ast.FullPerm()())
extends Mergeable[State] {

val isMethodVerification: Boolean = {
Expand Down Expand Up @@ -104,8 +105,9 @@ final case class State(g: Store = Store(),
copy(constrainableARPs = newConstrainableARPs)
}

def scalePermissionFactor(p: Term) =
copy(permissionScalingFactor = terms.PermTimes(p, permissionScalingFactor))
def scalePermissionFactor(p: Term, exp: ast.Exp) =
copy(permissionScalingFactor = terms.PermTimes(p, permissionScalingFactor),
permissionScalingFactorExp = ast.PermMul(exp, permissionScalingFactorExp)(exp.pos, exp.info, exp.errT))

def merge(other: State): State =
State.merge(this, other)
Expand Down Expand Up @@ -170,7 +172,7 @@ object State {
ssCache1, hackIssue387DisablePermissionConsumption1,
qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
moreCompleteExhale) =>
moreCompleteExhale, permissionScalingFactorExp1) =>

/* Decompose state s2: most values must match those of s1 */
s2 match {
Expand All @@ -195,7 +197,7 @@ object State {
ssCache2, `hackIssue387DisablePermissionConsumption1`,
`qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`,
`predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
moreCompleteExhale2) =>
moreCompleteExhale2, `permissionScalingFactorExp1`) =>

val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
val triggerExp3 = triggerExp1 && triggerExp2
Expand Down

0 comments on commit 33d89e6

Please sign in to comment.