From de745c755e31856bc054b5ba1a7e26c1156d28c2 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 21 Sep 2023 20:13:02 +0200 Subject: [PATCH 1/8] Simplifying wildcard multiplication --- src/main/scala/decider/Decider.scala | 14 +++++++------- src/main/scala/logger/writer/TermWriter.scala | 9 +++++---- src/main/scala/reporting/Converter.scala | 2 +- src/main/scala/rules/Consumer.scala | 6 +++--- src/main/scala/rules/Evaluator.scala | 4 ++-- src/main/scala/rules/Executor.scala | 2 +- src/main/scala/rules/HavocSupporter.scala | 2 +- src/main/scala/rules/MagicWandSupporter.scala | 2 +- .../rules/MoreCompleteExhaleSupporter.scala | 4 ++-- src/main/scala/rules/Producer.scala | 4 ++-- .../scala/rules/QuantifiedChunkSupport.scala | 2 +- src/main/scala/state/State.scala | 5 +++-- src/main/scala/state/Terms.scala | 19 ++++++++++++------- src/main/scala/state/Triggers.scala | 4 ++-- .../supporters/ExpressionTranslator.scala | 4 ++-- .../supporters/functions/FunctionData.scala | 4 ++-- ...pAccessReplacingExpressionTranslator.scala | 4 ++-- .../qps/PredicateSnapGenerator.scala | 2 +- .../SimpleArithmeticTermSolverTests.scala | 12 ++++++------ src/test/scala/TriggerGeneratorTests.scala | 8 ++++---- src/test/scala/TriggerRewriterTests.scala | 10 +++++----- 21 files changed, 65 insertions(+), 58 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 145fcceb0..785477bfd 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -298,17 +298,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) @@ -333,7 +333,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 @@ -348,7 +348,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 ac1a95edc..d6f6be1b4 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -284,7 +284,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 @@ -407,7 +407,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))){ @@ -421,7 +421,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 610cc514e..e08d54060 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -456,7 +456,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)) @@ -1534,7 +1534,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 d15793a22..8cfcc2115 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -566,7 +566,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 ec2ea7cfe..3f8530945 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -321,7 +321,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 8b509f3a6..68ff99ff4 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -291,7 +291,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 6abf20ff3..1ded4387e 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -57,7 +57,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 @@ -364,7 +364,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 a29672f59..67acaf36f 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -295,7 +295,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) @@ -399,7 +399,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 c1a03b2d4..a75f394e1 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -925,7 +925,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, _) = diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index b56238772..9dd3fab18 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -12,7 +12,7 @@ import viper.silicon.common.Mergeable import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.RecordedPathConditions import viper.silicon.state.State.OldHeaps -import viper.silicon.state.terms.{Term, Var} +import viper.silicon.state.terms.{PermLiteral, Term, Var} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.{Map, Stack} @@ -102,8 +102,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) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 5caefeb45..cd7f4ef5f 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]) @@ -1303,7 +1303,12 @@ object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] { case (t, FullPerm) => t case (NoPerm, _) => NoPerm case (_, NoPerm) => NoPerm + 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 (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal * p1.literal) + case (Ite(c, t1, t2), t3) => Ite(c, PermTimes(t1, t3), PermTimes(t2, t3)) + case (t1, Ite(c, t2, t3)) => Ite(c, PermTimes(t1, t2), PermTimes(t1, t3)) case (_, _) => createIfNonExistent(v0) } @@ -2459,8 +2464,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) diff --git a/src/main/scala/state/Triggers.scala b/src/main/scala/state/Triggers.scala index b03048530..7927c12b5 100644 --- a/src/main/scala/state/Triggers.scala +++ b/src/main/scala/state/Triggers.scala @@ -35,7 +35,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 { @@ -192,7 +192,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 7e0b3cab2..45fd6144a 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 81aa923a1..60ff0e4c1 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -95,7 +95,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 => @@ -116,7 +116,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/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 From dcd17b1dfe7a24f91479183a78c6ae4051f7dfb3 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 22 Sep 2023 13:38:58 +0200 Subject: [PATCH 2/8] Inlining more simplifying multiplications. --- src/main/scala/state/Terms.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index cd7f4ef5f..bdeae6a99 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -1308,6 +1308,10 @@ object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] { case (pl: PermLiteral, v2: Var) if v2.isWildcard && pl.literal > Rational.zero => v2 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) } From b1d5d61b9c0601a1fcaab683bf59ff35e5bf6709 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 9 Oct 2023 22:47:37 +0200 Subject: [PATCH 3/8] Fixing computation of constrainable terms --- src/main/scala/state/Terms.scala | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index bdeae6a99..966f306fd 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -2512,6 +2512,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 } From 3c1c3ce1e7d569c84133bf192b18f6abb77affbc Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 6 Feb 2024 21:15:53 +0100 Subject: [PATCH 4/8] Preventing simplification for resources for which perm is used --- src/main/scala/rules/Consumer.scala | 15 +++++++-- src/main/scala/state/State.scala | 9 +++--- src/main/scala/state/Terms.scala | 12 +++++-- .../scala/verifier/DefaultMainVerifier.scala | 32 +++++++++++++++++++ 4 files changed, 58 insertions(+), 10 deletions(-) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index b10d19468..cc6b38205 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -341,7 +341,10 @@ object consumer extends ConsumptionRules { } else { s2 } - val loss = PermTimes(tPerm, s2.permissionScalingFactor) + val loss = if (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 (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 (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) => { diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 6634c70c1..ff3019b35 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -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, @@ -157,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) => @@ -182,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`) => @@ -307,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) => @@ -331,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 966f306fd..832e31209 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -1297,15 +1297,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 _ => PermTimes(t0, t1) + } +} + object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] { override def apply(v0: (Term, Term)) = v0 match { case (FullPerm, t) => t case (t, FullPerm) => t case (NoPerm, _) => NoPerm case (_, NoPerm) => NoPerm - 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 (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)) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 0db992bea..3bd27b694 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] = 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 + } + State(program = program, functionData = functionData, predicateData = predicateData, qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, qpMagicWands = quantifiedMagicWands, + permLocations = permResources, predicateSnapMap = predSnapGenerator.snapMap, predicateFormalVarMap = predSnapGenerator.formalVarMap, currentMember = Some(member), From 0f55994910a6467ab7ed1e31fa7bb614fa89e2af Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 16 Feb 2024 00:46:18 +0100 Subject: [PATCH 5/8] Added missing cases --- src/main/scala/state/Terms.scala | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index da2979ff1..ed00e5541 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -1330,6 +1330,12 @@ object WildcardSimplifyingPermTimes extends ((Term, Term) => Term) { 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) } } From 329763ec2ae029ff2030694a8e63f9b48d7ab643 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 22 Feb 2024 17:41:48 +0100 Subject: [PATCH 6/8] Also simplifying in producer and QP supporter --- src/main/scala/rules/Producer.scala | 10 ++++++++-- src/main/scala/rules/QuantifiedChunkSupport.scala | 10 ++++++++-- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index 205579e35..d7acb0884 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 (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 (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) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 20a495935..24b8213be 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -794,7 +794,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - val gain = PermTimes(tPerm, s.permissionScalingFactor) + val gain = if (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, @@ -1072,7 +1075,10 @@ 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 (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)) From 7457b7bd06e2d4e6a73fc6fe8b0e2a0f9c4f293e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 26 Feb 2024 12:29:05 +0100 Subject: [PATCH 7/8] Hide simplification behind a new flag --- src/main/scala/Config.scala | 6 ++++++ src/main/scala/rules/Consumer.scala | 6 +++--- src/main/scala/rules/Producer.scala | 4 ++-- src/main/scala/rules/QuantifiedChunkSupport.scala | 6 ++++-- src/main/scala/verifier/DefaultMainVerifier.scala | 4 ++-- 5 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 5c1ef1df0..1b256b770 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", + 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/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index cc6b38205..9658d576a 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -341,7 +341,7 @@ object consumer extends ConsumptionRules { } else { s2 } - val loss = if (s2.permLocations.contains(field)) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field)) PermTimes(tPerm, s2.permissionScalingFactor) else WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) @@ -380,7 +380,7 @@ object consumer extends ConsumptionRules { s2 } - val loss = if (s2.permLocations.contains(loc.loc(s2.program))) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(loc.loc(s2.program))) PermTimes(tPerm, s2.permissionScalingFactor) else WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) @@ -409,7 +409,7 @@ 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 = if (s2.permLocations.contains(locacc.loc(s2.program))) + val loss = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(locacc.loc(s2.program))) PermTimes(tPerm, s2.permissionScalingFactor) else WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index d7acb0884..32e3bfd78 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -319,7 +319,7 @@ 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 = if (s2.permLocations.contains(field)) + val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field)) PermTimes(tPerm, s3.permissionScalingFactor) else WildcardSimplifyingPermTimes(tPerm, s3.permissionScalingFactor) @@ -340,7 +340,7 @@ object producer extends ProductionRules { val snap = sf( predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1) .getOrElse(sorts.Snap), v2) - val gain = if (s2.permLocations.contains(predicate)) + val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(predicate)) PermTimes(tPerm, s2.permissionScalingFactor) else WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 24b8213be..566148f52 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -794,7 +794,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - val gain = if (resource.isInstanceOf[ast.Location] && s.permLocations.contains(resource.asInstanceOf[ast.Location])) + 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) @@ -1075,7 +1076,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs) val chunkOrderHeuristics = qpAppChunkOrderHeuristics(inverseFunctions.invertibles, qvars, hints, v) - val loss = if (resource.isInstanceOf[ast.Location] && s.permLocations.contains(resource.asInstanceOf[ast.Location])) + 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) diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 65be4819e..3d38d87d4 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -325,7 +325,7 @@ 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] = member match { + 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)) @@ -353,7 +353,7 @@ class DefaultMainVerifier(config: Config, }) InsertionOrderedSet(bodyResources.flatten ++ preResources ++ postResources) case _ => InsertionOrderedSet.empty - } + } else InsertionOrderedSet.empty State(program = program, functionData = functionData, From 01d5f505f063d455a23fdac9af3f9c3beb6705b4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 26 Feb 2024 17:11:12 +0100 Subject: [PATCH 8/8] Added reference to PR that explains when the optimization is unsafe --- src/main/scala/Config.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 1b256b770..389592fae 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -684,7 +684,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { } val unsafeWildcardOptimization: ScallopOption[Boolean] = opt[Boolean]("unsafeWildcardOptimization", - descr = "Simplify wildcard terms in a way that is very very rarely unsafe", + descr = "Simplify wildcard terms in a way that is very very rarely unsafe. See Silicon PR #756 for details.", default = Some(false), noshort = true )