diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 5c1ef1df0..389592fae 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -683,6 +683,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { ExhaleMode.Greedy } + val unsafeWildcardOptimization: ScallopOption[Boolean] = opt[Boolean]("unsafeWildcardOptimization", + descr = "Simplify wildcard terms in a way that is very very rarely unsafe. See Silicon PR #756 for details.", + default = Some(false), + noshort = true + ) + val numberOfErrorsToReport: ScallopOption[Int] = opt[Int]("numberOfErrorsToReport", descr = "Number of errors per member before the verifier stops. If this number is set to 0, all errors are reported.", default = Some(1), diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index c6dccdcdc..7cd383851 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -337,17 +337,17 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => /* Fresh symbols */ def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function = - prover_fresh[Fun](id, argSorts, resultSort) + prover_fresh[Fun](id, argSorts, resultSort, false) - def fresh(id: String, sort: Sort): Var = prover_fresh[Var](id, Nil, sort) + def fresh(id: String, sort: Sort): Var = prover_fresh[Var](id, Nil, sort, false) - def fresh(s: Sort): Var = prover_fresh[Var]("$t", Nil, s) + def fresh(s: Sort): Var = prover_fresh[Var]("$t", Nil, s, false) def fresh(v: ast.AbstractLocalVar): Var = - prover_fresh[Var](v.name, Nil, symbolConverter.toSort(v.typ)) + prover_fresh[Var](v.name, Nil, symbolConverter.toSort(v.typ), false) def freshARP(id: String = "$k"): (Var, Term) = { - val permVar = prover_fresh[Var](id, Nil, sorts.Perm) + val permVar = prover_fresh[Var](id, Nil, sorts.Perm, true) val permVarConstraints = IsReadPermVar(permVar) (permVar, permVarConstraints) @@ -373,7 +373,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => } private def prover_fresh[F <: Function : ClassTag] - (id: String, argSorts: Seq[Sort], resultSort: Sort) + (id: String, argSorts: Seq[Sort], resultSort: Sort, isARP: Boolean) : F = { // context.bookkeeper.freshSymbols += 1 @@ -388,7 +388,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => destClass match { case c if c == classOf[Var] => Predef.assert(proverFun.argSorts.isEmpty) - Var(proverFun.id, proverFun.resultSort).asInstanceOf[F] + Var(proverFun.id, proverFun.resultSort, isARP).asInstanceOf[F] case c if c == classOf[Fun] => proverFun.asInstanceOf[F] case c if c == classOf[DomainFun] => DomainFun(proverFun.id, proverFun.argSorts, proverFun.resultSort).asInstanceOf[F] diff --git a/src/main/scala/logger/writer/TermWriter.scala b/src/main/scala/logger/writer/TermWriter.scala index 5b0af880e..f46f2c68b 100644 --- a/src/main/scala/logger/writer/TermWriter.scala +++ b/src/main/scala/logger/writer/TermWriter.scala @@ -6,7 +6,7 @@ package viper.silicon.logger.writer -import spray.json.{JsArray, JsNull, JsObject, JsString, JsValue} +import spray.json.{JsArray, JsBoolean, JsNull, JsObject, JsString, JsValue} import viper.silicon.state.Identifier import viper.silicon.state.terms._ @@ -30,11 +30,12 @@ object TermWriter { "p" -> p ) - private def variable(id: Identifier, sort: Sort) = + private def variable(id: Identifier, sort: Sort, isWildcard: Boolean) = JsObject( "type" -> JsString("variable"), "id" -> JsString(id.name), - "sort" -> toJSON(sort) + "sort" -> toJSON(sort), + "isWildcard" -> JsBoolean(isWildcard) ) def toJSON(sort: Sort): JsValue = { @@ -112,7 +113,7 @@ object TermWriter { "elseBranch" -> toJSON(elseBranch) ) - case Var(id, sort) => variable(id, sort) + case Var(id, sort, arp) => variable(id, sort, arp) case SortWrapper(t, sort) => JsObject( "type" -> JsString("sortWrapper"), diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala index b4e2fedbd..57355b121 100644 --- a/src/main/scala/reporting/Converter.scala +++ b/src/main/scala/reporting/Converter.scala @@ -255,7 +255,7 @@ object Converter { case IntLiteral(x) => LitIntEntry(x) case t: BooleanLiteral => LitBoolEntry(t.value) case Null => VarEntry(model.entries(nullRefId).toString, sorts.Ref) - case Var(_, sort) => + case Var(_, sort, _) => val key: String = term.toString val entry: Option[ModelEntry] = model.entries.get(key) entry diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 0da3269b7..9658d576a 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -294,7 +294,7 @@ object consumer extends ConsumptionRules { case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) val qid = MagicWandIdentifier(wand, s.program).toString val optTrigger = if (forall.triggers.isEmpty) None @@ -341,7 +341,10 @@ object consumer extends ConsumptionRules { } else { s2 } - val loss = PermTimes(tPerm, s2.permissionScalingFactor) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field)) + PermTimes(tPerm, s2.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) quantifiedChunkSupporter.consumeSingleLocation( s2p, h, @@ -377,7 +380,10 @@ object consumer extends ConsumptionRules { s2 } - val loss = PermTimes(tPerm, s2.permissionScalingFactor) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(loc.loc(s2.program))) + PermTimes(tPerm, s2.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) quantifiedChunkSupporter.consumeSingleLocation( s2p, h, @@ -403,7 +409,10 @@ object consumer extends ConsumptionRules { evalLocationAccess(s1, locacc, pve, v1)((s2, _, tArgs, v2) => permissionSupporter.assertNotNegative(s2, tPerm, perm, pve, v2)((s3, v3) => { val resource = locacc.res(s.program) - val loss = PermTimes(tPerm, s3.permissionScalingFactor) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(locacc.loc(s2.program))) + PermTimes(tPerm, s2.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) val ve = pve dueTo InsufficientPermission(locacc) val description = s"consume ${a.pos}: $a" chunkSupporter.consume(s3, h, resource, tArgs, loss, ve, v3, description)((s4, h1, snap1, v4) => { @@ -417,7 +426,7 @@ object consumer extends ConsumptionRules { /* Handle wands */ case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) => val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) evals(s, bodyVars, _ => pve, v)((s1, tArgs, v1) => { val s1p = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program))){ @@ -431,7 +440,7 @@ object consumer extends ConsumptionRules { } else { s1 } - val loss = PermTimes(FullPerm, s1.permissionScalingFactor) + val loss = s1.permissionScalingFactor quantifiedChunkSupporter.consumeSingleLocation( s1p, h, diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index a263b2b64..646798aaa 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -465,7 +465,7 @@ object evaluator extends EvaluationRules { val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](h, identifier) val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ), false)) val (s2, pmDef) = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))) { val (s2, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(s1, wand, formalVars, relevantChunks, v1) v1.decider.assume(PredicateTrigger(identifier.toString, smDef.sm, args)) @@ -1581,7 +1581,7 @@ object evaluator extends EvaluationRules { var mostRecentTrig: PredicateTrigger = null val wandHoles = wand.subexpressionsToEvaluate(s.program) val codomainQVars = - wandHoles.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(wandHoles(i).typ))) + wandHoles.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(wandHoles(i).typ), false)) val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s.h, MagicWandIdentifier(wand, s.program)) val optSmDomainDefinitionCondition = diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index d508cb44f..4f2189d0e 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -624,7 +624,7 @@ object executor extends ExecutionRules { val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedMagicWandChunk](s2.h, ch.id) val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ), false)) val (smDef, smCache) = quantifiedChunkSupporter.summarisingSnapshotMap( s2, wand, formalVars, relevantChunks, v1) diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index f08bf6ba8..b0422750e 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -322,7 +322,7 @@ object havocSupporter extends SymbolicExecutionRules { case w: ast.MagicWand => val bodyVars = w.subexpressionsToEvaluate(s.program) bodyVars.indices.toList.map(i => - Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) } } diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 26d6f6668..fae279da5 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -283,7 +283,7 @@ object magicWandSupporter extends SymbolicExecutionRules { val preMark = v3.decider.setPathConditionMark() if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) { val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) evals(s4, bodyVars, _ => pve, v3)((s5, args, v4) => { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index f7b647dba..53454b10c 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -58,7 +58,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { case _: ast.MagicWand => sorts.Snap } - val `?s` = Var(Identifier("?s"), sort) + val `?s` = Var(Identifier("?s"), sort, false) var summarisingSnapshotDefinitions: Seq[Term] = Vector.empty var permissionSum: Term = NoPerm @@ -386,7 +386,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { } - private val freeReceiver = Var(Identifier("?rcvr"), sorts.Ref) + private val freeReceiver = Var(Identifier("?rcvr"), sorts.Ref, false) def assumeFieldPermissionUpperBounds(h: Heap, v: Verifier): Unit = { // TODO: Instead of "manually" assuming such upper bounds, appropriate PropertyInterpreters diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index a41c11428..32e3bfd78 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -319,7 +319,10 @@ object producer extends ProductionRules { eval(s1, perm, pve, v1)((s2, tPerm, v2) => 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 gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field)) + PermTimes(tPerm, s3.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s3.permissionScalingFactor) 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) @@ -337,7 +340,10 @@ object producer extends ProductionRules { val snap = sf( predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1) .getOrElse(sorts.Snap), v2) - val gain = PermTimes(tPerm, s2.permissionScalingFactor) + val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(predicate)) + PermTimes(tPerm, s2.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) if (s2.qpPredicates.contains(predicate)) { val formalArgs = s2.predicateFormalVarMap(predicate) val trigger = (sm: Term) => PredicateTrigger(predicate.name, sm, tArgs) @@ -356,7 +362,7 @@ object producer extends ProductionRules { case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) => val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) evals(s, bodyVars, _ => pve, v)((s1, args,v1) => { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(sorts.Snap, v1), v1) @@ -460,7 +466,7 @@ object producer extends ProductionRules { case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) => val bodyVars = wand.subexpressionsToEvaluate(s.program) - val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) val optTrigger = if (forall.triggers.isEmpty) None else Some(forall.triggers) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index c7e843681..50c3db82c 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -794,7 +794,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - val gain = PermTimes(tPerm, s.permissionScalingFactor) + val gain = if (!Verifier.config.unsafeWildcardOptimization() || + (resource.isInstanceOf[ast.Location] && s.permLocations.contains(resource.asInstanceOf[ast.Location]))) + PermTimes(tPerm, s.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s.permissionScalingFactor) val (ch: QuantifiedBasicChunk, inverseFunctions) = quantifiedChunkSupporter.createQuantifiedChunk( qvars = qvars, @@ -925,7 +929,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { case p: ast.Predicate => s.predicateFormalVarMap(p) case w: ast.MagicWand => val bodyVars = w.subexpressionsToEvaluate(s.program) - bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ))) + bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false)) } val (relevantChunks, _) = @@ -1072,7 +1076,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs) val chunkOrderHeuristics = qpAppChunkOrderHeuristics(inverseFunctions.invertibles, qvars, hints, v) - val loss = PermTimes(tPerm, s.permissionScalingFactor) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || + (resource.isInstanceOf[ast.Location] && s.permLocations.contains(resource.asInstanceOf[ast.Location]))) + PermTimes(tPerm, s.permissionScalingFactor) + else + WildcardSimplifyingPermTimes(tPerm, s.permissionScalingFactor) val (relevantChunks, otherChunks) = quantifiedChunkSupporter.splitHeap[QuantifiedBasicChunk]( h, ChunkIdentifier(resource, s.program)) diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 0833fffc9..ff3019b35 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -13,7 +13,7 @@ import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.RecordedPathConditions import viper.silicon.interfaces.state.{Chunk, GeneralChunk} import viper.silicon.state.State.OldHeaps -import viper.silicon.state.terms.{And, Ite, NoPerm, SeqAppend, Term, Var} +import viper.silicon.state.terms.{And, Ite, NoPerm, PermLiteral, SeqAppend, Term, Var} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.{Map, Stack} @@ -60,6 +60,7 @@ final case class State(g: Store = Store(), qpFields: InsertionOrderedSet[ast.Field] = InsertionOrderedSet.empty, qpPredicates: InsertionOrderedSet[ast.Predicate] = InsertionOrderedSet.empty, qpMagicWands: InsertionOrderedSet[MagicWandIdentifier] = InsertionOrderedSet.empty, + permLocations: InsertionOrderedSet[ast.Location] = InsertionOrderedSet.empty, smCache: SnapshotMapCache = SnapshotMapCache.empty, pmCache: PmCache = Map.empty, smDomainNeeded: Boolean = false, @@ -104,8 +105,9 @@ final case class State(g: Store = Store(), copy(constrainableARPs = newConstrainableARPs) } - def scalePermissionFactor(p: Term) = + def scalePermissionFactor(p: Term) = { copy(permissionScalingFactor = terms.PermTimes(p, permissionScalingFactor)) + } def merge(other: State): State = State.merge(this, other) @@ -156,7 +158,7 @@ object State { permissionScalingFactor1, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, ssCache1, hackIssue387DisablePermissionConsumption1, - qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1, + qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins) => @@ -181,7 +183,7 @@ object State { `permissionScalingFactor1`, `reserveHeaps1`, `reserveCfgs1`, `conservedPcs1`, `recordPcs1`, `exhaleExt1`, ssCache2, `hackIssue387DisablePermissionConsumption1`, - `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`, + `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`) => @@ -306,7 +308,7 @@ object State { permissionScalingFactor1, reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, ssCache1, hackIssue387DisablePermissionConsumption1, - qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1, + qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1, predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers, moreCompleteExhale, moreJoins) => @@ -330,7 +332,7 @@ object State { `permissionScalingFactor1`, reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, ssCache2, `hackIssue387DisablePermissionConsumption1`, - `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, smDomainNeeded2, + `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2, `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2, `moreJoins`) => diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 433fe88fa..ed00e5541 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -247,8 +247,8 @@ object Macro extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), Macro, override def actualCreate(args: (Identifier, Stack[Sort], Sort)): Macro = new Macro(args._1, args._2, args._3) } -class Var private[terms] (val id: Identifier, val sort: Sort) extends Function with Application[Var] with ConditionalFlyweight[(Identifier, Sort), Var] { - override val equalityDefiningMembers: (Identifier, Sort) = (id, sort) +class Var private[terms] (val id: Identifier, val sort: Sort, val isWildcard: Boolean) extends Function with Application[Var] with ConditionalFlyweight[(Identifier, Sort, Boolean), Var] { + override val equalityDefiningMembers: (Identifier, Sort, Boolean) = (id, sort, isWildcard) val applicable: Var = this val args: Seq[Term] = Seq.empty val argSorts: Seq[Sort] = Seq(sorts.Unit) @@ -256,11 +256,11 @@ class Var private[terms] (val id: Identifier, val sort: Sort) extends Function w override lazy val toString = id.toString - def copy(id: Identifier = id, sort: Sort = sort) = Var(id, sort) + def copy(id: Identifier = id, sort: Sort = sort, isWildcard: Boolean = isWildcard) = Var(id, sort, isWildcard) } -object Var extends CondFlyweightFactory[(Identifier, Sort), Var, Var] { - override def actualCreate(args: (Identifier, Sort)): Var = new Var(args._1, args._2) +object Var extends CondFlyweightFactory[(Identifier, Sort, Boolean), Var, Var] { + override def actualCreate(args: (Identifier, Sort, Boolean)): Var = new Var(args._1, args._2, args._3) } class App private[terms] (val applicable: Applicable, val args: Seq[Term]) @@ -1325,6 +1325,21 @@ class PermTimes private[terms] (val p0: Term, val p1: Term) override val op = "*" } +object WildcardSimplifyingPermTimes extends ((Term, Term) => Term) { + override def apply(t0: Term, t1: Term) = (t0, t1) match { + case (v1: Var, v2: Var) if v1.isWildcard && v2.isWildcard => if (v1.id.name.compareTo(v2.id.name) > 0) v1 else v2 + case (v1: Var, pl: PermLiteral) if v1.isWildcard && pl.literal > Rational.zero => v1 + case (pl: PermLiteral, v2: Var) if v2.isWildcard && pl.literal > Rational.zero => v2 + case (Ite(c, t1, t2), t3) => Ite(c, WildcardSimplifyingPermTimes(t1, t3), WildcardSimplifyingPermTimes(t2, t3)) + case (PermPlus(t1, t2), t3) => PermPlus(WildcardSimplifyingPermTimes(t1, t3), WildcardSimplifyingPermTimes(t2, t3)) + case (t1, PermPlus(t2, t3)) => PermPlus(WildcardSimplifyingPermTimes(t1, t2), WildcardSimplifyingPermTimes(t1, t3)) + case (PermMinus(t1, t2), t3) => PermMinus(WildcardSimplifyingPermTimes(t1, t3), WildcardSimplifyingPermTimes(t2, t3)) + case (t1, PermMinus(t2, t3)) => PermMinus(WildcardSimplifyingPermTimes(t1, t2), WildcardSimplifyingPermTimes(t1, t3)) + case (t1, Ite(c, t2, t3)) => Ite(c, WildcardSimplifyingPermTimes(t1, t2), WildcardSimplifyingPermTimes(t1, t3)) + case _ => PermTimes(t0, t1) + } +} + object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] { override def apply(v0: (Term, Term)) = v0 match { case (FullPerm, t) => t @@ -1332,6 +1347,12 @@ object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] { case (NoPerm, _) => NoPerm case (_, NoPerm) => NoPerm case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal * p1.literal) + case (Ite(c, t1, t2), t3) => Ite(c, PermTimes(t1, t3), PermTimes(t2, t3)) + case (PermPlus(t1, t2), t3) => PermPlus(PermTimes(t1, t3), PermTimes(t2, t3)) + case (t1, PermPlus(t2, t3)) => PermPlus(PermTimes(t1, t2), PermTimes(t1, t3)) + case (PermMinus(t1, t2), t3) => PermMinus(PermTimes(t1, t3), PermTimes(t2, t3)) + case (t1, PermMinus(t2, t3)) => PermMinus(PermTimes(t1, t2), PermTimes(t1, t3)) + case (t1, Ite(c, t2, t3)) => Ite(c, PermTimes(t1, t2), PermTimes(t1, t3)) case (_, _) => createIfNonExistent(v0) } @@ -2507,8 +2528,8 @@ object Let extends CondFlyweightTermFactory[(Map[Var, Term], Term), Let] { /* Predefined terms */ object predef { - val `?s` = Var(Identifier("s@$"), sorts.Snap) // with SnapshotTerm - val `?r` = Var(Identifier("r"), sorts.Ref) + val `?s` = Var(Identifier("s@$"), sorts.Snap, false) // with SnapshotTerm + val `?r` = Var(Identifier("r"), sorts.Ref, false) val Zero = IntLiteral(0) val One = IntLiteral(1) @@ -2551,6 +2572,8 @@ object utils { case PermIntDiv(t0, _) => consumeExactRead(t0, constrainableARPs) case PermPermDiv(t0, t1) => consumeExactRead(t0, constrainableARPs) && consumeExactRead(t1, constrainableARPs) case PermMin(t0 ,t1) => consumeExactRead(t0, constrainableARPs) || consumeExactRead(t1, constrainableARPs) + case Ite(_, t0, NoPerm) => consumeExactRead(t0, constrainableARPs) + case Ite(_, NoPerm, t1) => consumeExactRead(t1, constrainableARPs) case Ite(_, t0, t1) => consumeExactRead(t0, constrainableARPs) || consumeExactRead(t1, constrainableARPs) case _ => true } diff --git a/src/main/scala/state/Triggers.scala b/src/main/scala/state/Triggers.scala index 74f4f92c6..1fba6f6b6 100644 --- a/src/main/scala/state/Triggers.scala +++ b/src/main/scala/state/Triggers.scala @@ -36,7 +36,7 @@ class TriggerGenerator protected def transform[T <: Term](root: T)(f: PartialFunction[Term, Term]) = root.transform(f)() protected def Quantification_vars(q: Quantification) = q.vars protected def Exp_typ(term: Term): Sort = term.sort - protected def Var(id: String, sort: Sort) = terms.Var(Identifier(id), sort) + protected def Var(id: String, sort: Sort) = terms.Var(Identifier(id), sort, false) def generateFirstTriggerGroup(vs: Seq[Var], toSearch: Seq[Term]): Option[(Seq[Trigger], Seq[Var])] = generateFirstTriggerSetGroup(vs, toSearch).map { @@ -193,7 +193,7 @@ class AxiomRewriter(counter: Counter/*, logger: MultiRunLogger*/, protected val solver = SimpleArithmeticSolver protected def fresh(name: String, typ: Type): Var = - Var(Identifier(s"$name@rw${counter.next()}"), typ) + Var(Identifier(s"$name@rw${counter.next()}"), typ, false) protected def log(message: String): Unit = { // logger.println(message) diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 22077d182..914e2911f 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -119,7 +119,7 @@ trait ExpressionTranslator { } Quantification(qantOp, - vars map (v => Var(Identifier(v.name), toSort(v.typ))), + vars map (v => Var(Identifier(v.name), toSort(v.typ), false)), f(body), translatedTriggers, "", @@ -152,7 +152,7 @@ trait ExpressionTranslator { case _: ast.NullLit => Null - case v: ast.AbstractLocalVar => Var(Identifier(v.name), toSort(v.typ)) + case v: ast.AbstractLocalVar => Var(Identifier(v.name), toSort(v.typ), false) case ast.DomainFuncApp(funcName, args, _) => val tArgs = args map f diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala index 1861587c1..d2384dd96 100644 --- a/src/main/scala/supporters/functions/FunctionData.scala +++ b/src/main/scala/supporters/functions/FunctionData.scala @@ -59,10 +59,10 @@ class FunctionData(val programFunction: ast.Function, x = arg.localVar) yield x -> Var(identifierFactory.fresh(x.name), - symbolConverter.toSort(x.typ))) + symbolConverter.toSort(x.typ), false)) val formalResult = Var(identifierFactory.fresh(programFunction.result.name), - symbolConverter.toSort(programFunction.result.typ)) + symbolConverter.toSort(programFunction.result.typ), false) val arguments = Seq(`?s`) ++ formalArgs.values diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index 5235f31de..9b6c75201 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -96,7 +96,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, case v: ast.AbstractLocalVar => data.formalArgs.get(v) match { case Some(t) => t - case None => Var(Identifier(v.name), toSort(v.typ)) + case None => Var(Identifier(v.name), toSort(v.typ), false) } case eQuant: ast.QuantifiedExp => @@ -117,7 +117,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, tQuant.transform({ case v: Var => v.id match { case sid: SuffixedIdentifier if names.contains(sid.prefix.name) => - Var(SimpleIdentifier(sid.prefix.name), v.sort) + Var(SimpleIdentifier(sid.prefix.name), v.sort, false) case _ => v } })() diff --git a/src/main/scala/supporters/qps/PredicateSnapGenerator.scala b/src/main/scala/supporters/qps/PredicateSnapGenerator.scala index 351ce0a35..223f6a6c2 100644 --- a/src/main/scala/supporters/qps/PredicateSnapGenerator.scala +++ b/src/main/scala/supporters/qps/PredicateSnapGenerator.scala @@ -25,7 +25,7 @@ class PredicateSnapGenerator(symbolConverter: SymbolConverter, snapshotSupporter case ast.PredicateAccess(_, predname) => val predicate = program.findPredicate(predname) val sort = predicate -> predicate.body.map(snapshotSupporter.optimalSnapshotSort(_, program)._1).getOrElse(terms.sorts.Snap) - val formalArgs:Seq[Var] = predicate.formalArgs.map(formalArg => Var(Identifier(formalArg.name), symbolConverter.toSort(formalArg.typ))) + val formalArgs:Seq[Var] = predicate.formalArgs.map(formalArg => Var(Identifier(formalArg.name), symbolConverter.toSort(formalArg.typ), false)) formalVarMap += predicate -> formalArgs snapMap += sort } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index c0c39435d..3d38d87d4 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -324,12 +324,44 @@ class DefaultMainVerifier(config: Config, } val moreJoins = Verifier.config.moreJoins() && member.isInstanceOf[ast.Method] + val methodPermCache = mutable.HashMap[String, InsertionOrderedSet[ast.Location]]() + val permResources: InsertionOrderedSet[ast.Location] = if (Verifier.config.unsafeWildcardOptimization()) member match { + case m: ast.Method if m.body.isDefined => + val bodyResources: Iterable[InsertionOrderedSet[ast.Location]] = m.body.get.collect { + case ast.CurrentPerm(la: ast.LocationAccess) => InsertionOrderedSet(la.loc(program)) + case ast.MethodCall(name, _, _) => + if (methodPermCache.contains(name)) + methodPermCache(name) + else { + val calledMethod = program.findMethod(name) + val preResources: Seq[ast.Location] = calledMethod.pres.flatMap(pre => pre.whenExhaling.collect { + case ast.CurrentPerm(la: ast.LocationAccess) => la.loc(program) + }) + val postResources: Seq[ast.Location] = calledMethod.posts.flatMap(post => post.whenInhaling.collect { + case ast.CurrentPerm(la: ast.LocationAccess) => la.loc(program) + }) + val all = InsertionOrderedSet(preResources ++ postResources) + methodPermCache.update(name, all) + all + } + } + val preResources: Seq[ast.Location] = m.pres.flatMap(pre => pre.whenInhaling.collect { + case ast.CurrentPerm(la: ast.LocationAccess) => la.loc(program) + }) + val postResources: Seq[ast.Location] = m.posts.flatMap(post => post.whenExhaling.collect { + case ast.CurrentPerm(la: ast.LocationAccess) => la.loc(program) + }) + InsertionOrderedSet(bodyResources.flatten ++ preResources ++ postResources) + case _ => InsertionOrderedSet.empty + } else InsertionOrderedSet.empty + State(program = program, functionData = functionData, predicateData = predicateData, qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, qpMagicWands = quantifiedMagicWands, + permLocations = permResources, predicateSnapMap = predSnapGenerator.snapMap, predicateFormalVarMap = predSnapGenerator.formalVarMap, currentMember = Some(member), diff --git a/src/test/scala/SimpleArithmeticTermSolverTests.scala b/src/test/scala/SimpleArithmeticTermSolverTests.scala index 77e623906..9afcf2616 100644 --- a/src/test/scala/SimpleArithmeticTermSolverTests.scala +++ b/src/test/scala/SimpleArithmeticTermSolverTests.scala @@ -70,12 +70,12 @@ private[tests] object DSL { def ==>(t2: Term) = Implies(t1, t2) } - val x = Var(Identifier("x"), sorts.Int) - val y = Var(Identifier("y"), sorts.Int) - val z = Var(Identifier("z"), sorts.Int) - val n = Var(Identifier("n"), sorts.Int) - val m = Var(Identifier("m"), sorts.Int) - val b = Var(Identifier("b"), sorts.Int) + val x = Var(Identifier("x"), sorts.Int, false) + val y = Var(Identifier("y"), sorts.Int, false) + val z = Var(Identifier("z"), sorts.Int, false) + val n = Var(Identifier("n"), sorts.Int, false) + val m = Var(Identifier("m"), sorts.Int, false) + val b = Var(Identifier("b"), sorts.Int, false) val `0` = IntLiteral(0) val `1` = IntLiteral(1) diff --git a/src/test/scala/TriggerGeneratorTests.scala b/src/test/scala/TriggerGeneratorTests.scala index 2a7b831b9..68a7acd2f 100644 --- a/src/test/scala/TriggerGeneratorTests.scala +++ b/src/test/scala/TriggerGeneratorTests.scala @@ -21,8 +21,8 @@ class TriggerGeneratorTests extends AnyFunSuite with BeforeAndAfter { } test("Work in simple cases") { - val i = Var(Identifier("i"), sorts.Int) - val s = Var(Identifier("S"), sorts.Seq(sorts.Int)) + val i = Var(Identifier("i"), sorts.Int, false) + val s = Var(Identifier("S"), sorts.Seq(sorts.Int), false) val t = SeqAt(s, i) assert(triggerGenerator.generateTriggerSetGroups(i :: Nil, t) match { @@ -32,8 +32,8 @@ class TriggerGeneratorTests extends AnyFunSuite with BeforeAndAfter { } test("Fail in these cases") { - val i = Var(Identifier("i"), sorts.Int) - val s = Var(Identifier("S"), sorts.Seq(sorts.Int)) + val i = Var(Identifier("i"), sorts.Int, false) + val s = Var(Identifier("S"), sorts.Seq(sorts.Int), false) val t = SeqAt(s, Plus(i, IntLiteral(1))) assert(triggerGenerator.generateTriggerSetGroups(i :: Nil, t).isEmpty) diff --git a/src/test/scala/TriggerRewriterTests.scala b/src/test/scala/TriggerRewriterTests.scala index e9ad7c5fe..c36e4ade1 100644 --- a/src/test/scala/TriggerRewriterTests.scala +++ b/src/test/scala/TriggerRewriterTests.scala @@ -30,14 +30,14 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers with BeforeAndAfter } override protected def fresh(id: String, s: Sort): Var = { - Var(Identifier(s"$id${counter.next()}"), s) + Var(Identifier(s"$id${counter.next()}"), s, false) } } - lazy val x0 = Var(Identifier("x0"), sorts.Int) - lazy val x1 = Var(Identifier("x1"), sorts.Int) - lazy val y0 = Var(Identifier("y0"), sorts.Int) - lazy val z0 = Var(Identifier("z0"), sorts.Int) + lazy val x0 = Var(Identifier("x0"), sorts.Int, false) + lazy val x1 = Var(Identifier("x1"), sorts.Int, false) + lazy val y0 = Var(Identifier("y0"), sorts.Int, false) + lazy val z0 = Var(Identifier("z0"), sorts.Int, false) import rewriter.rewrite