Skip to content

Commit ff4d359

Browse files
marcoeilersmarcoeilers
authored
Fixing issues #410 and #338 (#899)
1 parent ecb4a1a commit ff4d359

7 files changed

Lines changed: 42 additions & 19 deletions

File tree

‎silver‎

‎src/main/scala/rules/ChunkSupporter.scala‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,12 @@ object chunkSupporter extends ChunkSupportRules {
256256
case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) =>
257257
Q(s, ch.snap, v)
258258
case _ if v.decider.checkSmoke(true) =>
259-
Success() // TODO: Mark branch as dead?
259+
if (s.isInPackage) {
260+
val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
261+
Q(s, snap, v)
262+
} else {
263+
Success() // TODO: Mark branch as dead?
264+
}
260265
case _ =>
261266
createFailure(ve, v, s, "looking up chunk", true)
262267
}

‎src/main/scala/rules/Executor.scala‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -494,7 +494,7 @@ object executor extends ExecutionRules {
494494
consume(s, a, false, pve, v)((s1, _, v1) =>
495495
Q(s1, v1))
496496

497-
case assert @ ast.Assert(a: ast.FalseLit) =>
497+
case assert @ ast.Assert(a: ast.FalseLit) if !s.isInPackage =>
498498
/* "assert false" triggers a smoke check. If successful, we backtrack. */
499499
executionFlowController.tryOrFail0(s.copy(h = magicWandSupporter.getEvalHeap(s)), v)((s1, v1, QS) => {
500500
if (v1.decider.checkSmoke(true))
@@ -653,7 +653,7 @@ object executor extends ExecutionRules {
653653

654654
case pckg @ ast.Package(wand, proofScript) =>
655655
val pve = PackageFailed(pckg)
656-
magicWandSupporter.packageWand(s, wand, proofScript, pve, v)((s1, chWand, v1) => {
656+
magicWandSupporter.packageWand(s.copy(isInPackage = true), wand, proofScript, pve, v)((s1, chWand, v1) => {
657657

658658
val hOps = s1.reserveHeaps.head + chWand
659659
assert(s.exhaleExt || s1.reserveHeaps.length == 1)
@@ -692,7 +692,7 @@ object executor extends ExecutionRules {
692692
case _ => s2.smCache
693693
}
694694

695-
continuation(s2.copy(smCache = smCache3), v1)
695+
continuation(s2.copy(smCache = smCache3, isInPackage = s.isInPackage), v1)
696696
})
697697

698698
case apply @ ast.Apply(e) =>

‎src/main/scala/rules/MoreCompleteExhaleSupporter.scala‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ import viper.silicon.utils.ast.{BigAnd, buildMinExp, removeKnownToBeTrueExp, rep
1919
import viper.silicon.verifier.Verifier
2020
import viper.silicon.{MList, MMap}
2121
import viper.silver.ast
22-
import viper.silver.parser.{PKw, PPrimitiv, PReserved}
22+
import viper.silver.parser.PUnknown
2323
import viper.silver.verifier.VerificationError
2424

2525
import scala.collection.mutable.ListBuffer
@@ -204,7 +204,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
204204

205205
if (relevantChunks.isEmpty) {
206206
if (v.decider.checkSmoke(true)) {
207-
Success() // TODO: Mark branch as dead?
207+
if (s.isInPackage) {
208+
val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
209+
Q(s, snap, v)
210+
} else {
211+
Success() // TODO: Mark branch as dead?
212+
}
208213
} else {
209214
createFailure(ve, v, s, False, "branch is dead")
210215
}

‎src/main/scala/rules/Producer.scala‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -323,7 +323,7 @@ object producer extends ProductionRules {
323323
eval(s1, perm, pve, v1)((s2, tPerm, ePermNew, v2) =>
324324
permissionSupporter.assertNotNegative(s2, tPerm, perm, ePermNew, pve, v2)((s2a, v3) => {
325325
val s3 = s2a.copy(constrainableARPs = s.constrainableARPs)
326-
val snap = sf(v3.symbolConverter.toSort(field.typ), v3)
326+
val snap = sf(v3.snapshotSupporter.optimalSnapshotSort(field, s3, v3), v3)
327327
val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field))
328328
PermTimes(tPerm, s3.permissionScalingFactor)
329329
else
@@ -350,9 +350,7 @@ object producer extends ProductionRules {
350350
eval(s1, perm, pve, v1)((s1a, tPerm, ePermNew, v1a) =>
351351
permissionSupporter.assertNotNegative(s1a, tPerm, perm, ePermNew, pve, v1a)((s1b, v2) => {
352352
val s2 = s1b.copy(constrainableARPs = s.constrainableARPs)
353-
val snap = sf(
354-
predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
355-
.getOrElse(sorts.Snap), v2)
353+
val snap = sf(v2.snapshotSupporter.optimalSnapshotSort(predicate, s2, v2), v2)
356354
val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(predicate))
357355
PermTimes(tPerm, s2.permissionScalingFactor)
358356
else
@@ -382,7 +380,7 @@ object producer extends ProductionRules {
382380
val formalVarExps = Option.when(withExp)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)()))
383381
evals(s, bodyVars, _ => pve, v)((s1, args, bodyVarsNew, v1) => {
384382
val (sm, smValueDef) =
385-
quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(sorts.Snap, v1), v1)
383+
quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(v1.snapshotSupporter.optimalSnapshotSort(wand, s1, v1), v1), v1)
386384
v1.decider.prover.comment("Definitional axioms for singleton-SM's value")
387385
val definitionalAxiomMark = v1.decider.setPathConditionMark()
388386
val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true))
@@ -416,7 +414,7 @@ object producer extends ProductionRules {
416414
Q(s2, v1)})
417415

418416
case wand: ast.MagicWand =>
419-
val snap = sf(sorts.MagicWandSnapFunction, v)
417+
val snap = sf(v.snapshotSupporter.optimalSnapshotSort(wand, s, v), v)
420418
magicWandSupporter.createChunk(s, wand, MagicWandSnapshot(snap), pve, v)((s1, chWand, v1) =>
421419
chunkSupporter.produce(s1, s1.h, chWand, v1)((s2, h2, v2) =>
422420
Q(s2.copy(h = h2), v2)))
@@ -431,7 +429,7 @@ object producer extends ProductionRules {
431429
else Some(forall.triggers)
432430
evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) {
433431
case (s1, qvars, qvarExps, Seq(tCond), eCondNew, Some((Seq(tRcvr, tPerm), rcvrPerm, tTriggers, (auxGlobals, auxNonGlobals), auxExps)), v1) =>
434-
val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1)
432+
val tSnap = sf(sorts.FieldValueFunction(v1.snapshotSupporter.optimalSnapshotSort(acc.loc.field, s1, v1), acc.loc.field.name), v1)
435433
val s1a = s1.copy(constrainableARPs = s.constrainableARPs)
436434
quantifiedChunkSupporter.produce(
437435
s1a,

‎src/main/scala/state/State.scala‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ final case class State(g: Store = Store(),
6262
conservedPcs: Stack[Vector[RecordedPathConditions]] = Stack(),
6363
recordPcs: Boolean = false,
6464
exhaleExt: Boolean = false,
65+
isInPackage: Boolean = false,
6566

6667
ssCache: SsCache = Map.empty,
6768
assertReadAccessOnly: Boolean = false,
@@ -175,7 +176,7 @@ object State {
175176
triggerExp1,
176177
partiallyConsumedHeap1,
177178
permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld,
178-
reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
179+
reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, isInPackage1,
179180
ssCache1, assertReadAccessOnly1,
180181
qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1,
181182
predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
@@ -200,7 +201,7 @@ object State {
200201
triggerExp2,
201202
`partiallyConsumedHeap1`,
202203
`permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`,
203-
`reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
204+
`reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, `isInPackage1`,
204205
ssCache2, `assertReadAccessOnly1`,
205206
`qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`,
206207
`predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
@@ -331,7 +332,7 @@ object State {
331332
triggerExp1,
332333
partiallyConsumedHeap1,
333334
permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld,
334-
reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
335+
reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, isInPackage1,
335336
ssCache1, assertReadAccessOnly1,
336337
qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1,
337338
predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
@@ -355,7 +356,7 @@ object State {
355356
triggerExp2,
356357
partiallyConsumedHeap2,
357358
`permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`,
358-
reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
359+
reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, `isInPackage1`,
359360
ssCache2, `assertReadAccessOnly1`,
360361
`qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2,
361362
`predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,

‎src/main/scala/supporters/SnapshotSupporter.scala‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,17 +8,20 @@ package viper.silicon.supporters
88

99
import viper.silicon.debugger.DebugExp
1010
import viper.silicon.state.terms.{Combine, First, Second, Sort, Term, Unit, sorts}
11-
import viper.silicon.state.{State, SymbolConverter}
11+
import viper.silicon.state.{MagicWandIdentifier, State, SymbolConverter}
1212
import viper.silicon.utils.toSf
1313
import viper.silicon.verifier.Verifier
1414
import viper.silver.ast
15+
import viper.silver.ast.Resource
1516
import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
1617

1718
import scala.annotation.unused
1819

1920
trait SnapshotSupporter {
2021
def optimalSnapshotSort(a: ast.Exp, program: ast.Program): (Sort, Boolean)
2122

23+
def optimalSnapshotSort(r: ast.Resource, s: State, v: Verifier): Sort
24+
2225
def createSnapshotPair(s: State,
2326
sf: (Sort, Verifier) => Term,
2427
a0: ast.Exp,
@@ -31,6 +34,17 @@ class DefaultSnapshotSupporter(symbolConverter: SymbolConverter) extends Snapsho
3134
def optimalSnapshotSort(a: ast.Exp, program: ast.Program): (Sort, Boolean) =
3235
optimalSnapshotSort(a, program, Nil)
3336

37+
def optimalSnapshotSort(r: Resource, s: State, v: Verifier): Sort = r match {
38+
case f: ast.Field => v.symbolConverter.toSort(f.typ)
39+
case p: ast.Predicate if s.predicateSnapMap.contains(p) => s.predicateSnapMap(p)
40+
case p: ast.Predicate =>
41+
p.body.map(v.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
42+
.getOrElse(sorts.Snap)
43+
case mw: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(mw, s.program)) =>
44+
sorts.Snap
45+
case _: ast.MagicWand => sorts.MagicWandSnapFunction
46+
}
47+
3448
private def optimalSnapshotSort(a: ast.Exp, program: ast.Program, visited: Seq[String])
3549
: (Sort, Boolean) =
3650

0 commit comments

Comments
 (0)
⚡