From c480f60896deff835fcac9cdda4b4ecea0fcc395 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 3 Oct 2024 19:27:43 +0200 Subject: [PATCH] Started reworking abstraction --- src/main/scala/Config.scala | 2 +- src/main/scala/biabduction/Abstraction.scala | 96 +++++++++++++++---- src/main/scala/biabduction/BiAbduction.scala | 18 ++-- .../scala/biabduction/VarTransformer.scala | 43 +++++---- .../scala/supporters/MethodSupporter.scala | 2 +- 5 files changed, 115 insertions(+), 46 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index b0fd1cfb6..a21ad4ca5 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -820,7 +820,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { val enableDebugging: ScallopOption[Boolean] = opt[Boolean]("enableDebugging", descr = "Enable debugging mode", - default = Some(false), + default = Some(true), // Set to true for biabduction testing noshort = true ) diff --git a/src/main/scala/biabduction/Abstraction.scala b/src/main/scala/biabduction/Abstraction.scala index 45f7192a3..b4da43a5a 100644 --- a/src/main/scala/biabduction/Abstraction.scala +++ b/src/main/scala/biabduction/Abstraction.scala @@ -1,9 +1,9 @@ package viper.silicon.biabduction import viper.silicon.interfaces.VerificationResult -import viper.silicon.rules.evaluator -import viper.silicon.state.State -import viper.silicon.state.terms.True +import viper.silicon.resources._ +import viper.silicon.rules._ +import viper.silicon.state._ import viper.silicon.verifier.Verifier import viper.silver.ast._ @@ -11,37 +11,92 @@ object AbstractionApplier extends RuleApplier[AbstractionQuestion] { override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply) } -case class AbstractionQuestion(exps: Seq[Exp], s: State, v: Verifier) +case class AbstractionQuestion(s: State, v: Verifier) { + + // TODO we assume each field only appears in at most one predicate + def fields: Map[Field, Predicate] = s.program.predicates.flatMap { pred => pred.body.get.collect { case fa: FieldAccessPredicate => (fa.loc.field, pred) } }.toMap + + def varTran = VarTransformer(s, v, s.g.values, Heap()) + + def isTriggerField(bc: BasicChunk): Boolean = { + bc.resourceID match { + case FieldID => fields.contains(abductionUtils.getField(bc.id, s.program)) + case _ => false + } + } +} trait AbstractionRule extends BiAbductionRule[AbstractionQuestion] object AbstractionFold extends AbstractionRule { - + + private def checkChunks(chunks: Seq[BasicChunk], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { + chunks match { + case Seq() => Q(None) + case chunk :: rest => + val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program)) + val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs + executionFlowController.tryOrElse0(q.s, q.v) { + (s1, v1, T) => + predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pve, v1)(T) + } { (s2, v2) => Q(Some(q.copy(s = s2, v = v2))) } { + _ => checkChunks(rest, q)(Q) + } + } + } + override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - Q(None) + val candChunks = q.s.h.values.collect { case bc: BasicChunk if q.isTriggerField(bc) => bc }.toSeq + checkChunks(candChunks, q)(Q) } } + +// TODO nklose Never fold. Instead, check if there exists a var in the state so that the field access is equal to it. If so, then we can package where the var gives us the lhs. object AbstractionPackage extends AbstractionRule { + private def findWandFieldChunk(chunks: Seq[BasicChunk], q: AbstractionQuestion): Option[(Exp, BasicChunk)] = { + chunks match { + case Seq() => None + case chunk :: rest => + q.varTran.transformChunk(chunk) match { + case None => findWandFieldChunk(rest, q) + case Some(lhs) => Some((lhs, chunk)) + } + } + } + override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - Q(None) + + val candChunks = q.s.h.values.collect { case bc: BasicChunk if q.isTriggerField(bc) => bc }.toSeq + + findWandFieldChunk(candChunks, q) match { + case None => Q(None) + case Some((lhsArg, chunk)) => + val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program)) + val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())() + val rhsArg = q.varTran.transformTerm(chunk.args.head).get + val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())() + val wand = MagicWand(lhs, rhs)() + executor.exec(q.s, Assert(wand)(), q.v) { (s1, sv) => Q(Some(q.copy(s = s1, v = sv)))} + } } } object AbstractionJoin extends AbstractionRule { override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - val wands = q.exps.collect { case wand: MagicWand => wand } + val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.toSeq val pairs = wands.combinations(2).toSeq pairs.collectFirst { case wands if wands(0).right == wands(1).left => (wands(0), wands(1)) case wands if wands(1).right == wands(0).left => (wands(1), wands(0)) } match { case None => Q(None) - case (Some(inst)) => - val exps1 = q.exps.filterNot(exp => inst._1 == exp || inst._2 == exp) :+ MagicWand(inst._1.left, inst._2.right)() - Q(Some(q.copy(exps = exps1))) + case (Some((w1, w2))) => + magicWandSupporter.packageWand(q.s, MagicWand(w1.left, w2.right)(), Seq(Apply(w1), Apply(w2)), pve, q.v) { + (s1, v1) => Q(Some(q.copy(s = s1, v = v1))) + } } } } @@ -49,16 +104,15 @@ object AbstractionJoin extends AbstractionRule { object AbstractionApply extends AbstractionRule { override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - val wands = q.exps.collect { case wand: MagicWand => wand } - val matches = wands.filter(wand => q.exps.contains(wand.left)) - if (matches.isEmpty) { - Q(None) - } else { - val lefts = matches.map(_.left) - val rights = matches.map(_.right) - - val exps1 = q.exps.filterNot(matches.contains).filter(lefts.contains(_)) ++ rights - Q(Some(q.copy(exps = exps1))) + val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect {case Some(wand: MagicWand) => wand} + val targets = q.s.h.values.collect { case c: BasicChunk => q.varTran.transformChunk(c) }.collect {case Some(exp) => exp}.toSeq + + wands.collectFirst{case wand if targets.contains(wand.left) => wand } match { + case None => Q(None) + case Some(wand) => + magicWandSupporter.applyWand(q.s, wand, pve, q.v) { + (s1, v1) => Q(Some(q.copy(s = s1, v = v1)) + } } } } diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index 6ab73c3be..1c6ea6283 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -152,15 +152,19 @@ object BiAbductionSolver { - def solveAbstraction(s: State, v: Verifier, exps: Seq[Exp])(Q: Seq[Exp] => VerificationResult): VerificationResult = { - executionFlowController.locallyWithResult[Seq[Exp]](s, v)((s1, v1, QS) => { - val q = AbstractionQuestion(exps, s1, v1) - AbstractionApplier.applyRules(q){ q1 => - QS(q1.exps) - } - })(Q) + def solveAbstraction(s: State, v: Verifier)(Q: (State, Verifier, Seq[Exp]) => VerificationResult): VerificationResult = { + val q = AbstractionQuestion(s1, v1) + val res = AbstractionApplier.applyRules(q) { q1 => + Success(solveFraming(q1.s, q1.v, q1.s.g.values)) + } match { + case NonFatalResult => + val exps = abductionUtils.getFramingSuccesses(res).head + Q(exps.s, exps.v, exps.posts) + } } + // TODO nklose we would like to abstract postconditions, but we cannot do it here anymore! We call this from an abstraction rule + // So we have to do this only where we generate the postconditions. def solveFraming(s: State, v: Verifier, postVars: Map[AbstractLocalVar, (Term, Option[Exp])], loc: Position = NoPosition, ignoredBcs: Seq[Exp] = Seq()): FramingSuccess = { val tra = VarTransformer(s, v, postVars, s.h) diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index e36d3d9d3..771681840 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -8,8 +8,6 @@ import viper.silicon.state._ import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast._ -//import viper.silver.verifier.PartialVerificationError -//import viper.silver.verifier.errors.Internal case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap) { @@ -20,10 +18,10 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa private def resolveMatches(): Map[Term, Exp] = { - val allTerms: Seq[Term] = (s.g.values.values.map{case (t1, _) => t1} + val allTerms: Seq[Term] = (s.g.values.values.map { case (t1, _) => t1 } ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) }.flatten ++ targetVars.values.map(_._1) - ++ v.decider.pcs.branchConditions.collect{ case t => t.subterms.collect{case tVar: Var => tVar}}.flatten).toSeq.distinct + ++ v.decider.pcs.branchConditions.collect { case t => t.subterms.collect { case tVar: Var => tVar } }.flatten).toSeq.distinct // The symbolic values of the target vars in the store. Everything else is an attempt to match things to these terms //val targetMap: Map[Term, AbstractLocalVar] = targets.view.map(localVar => s.g.get(localVar).get -> localVar).toMap @@ -34,15 +32,16 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa }.collect { case (t2, Some(e)) => t2 -> e }.toMap resolveChunks(directAliases, targetHeap.values.collect { case c: BasicChunk - if c.resourceID == FieldID && !(directAliases.contains(c.args.head) && directAliases.contains(c.snap)) => c }.toSeq, allTerms.filter(!directAliases.contains(_))) + if c.resourceID == FieldID && !(directAliases.contains(c.args.head) && directAliases.contains(c.snap)) => c + }.toSeq, allTerms.filter(!directAliases.contains(_))) } private def resolveChunks(currentMatches: Map[Term, Exp], remainingChunks: Seq[BasicChunk], remainingTerms: Seq[Term]): Map[Term, Exp] = { - remainingChunks.collectFirst { case c if currentMatches.contains(c.args.head) => c} match { + remainingChunks.collectFirst { case c if currentMatches.contains(c.args.head) => c } match { case None => currentMatches case Some(c) => val newExp = FieldAccess(currentMatches(c.args.head), abductionUtils.getField(c.id, s.program))() - val newMatches = currentMatches ++ remainingTerms.collect{ case t if t.sort == c.snap.sort && v.decider.check(BuiltinEquals(t, c.snap), Verifier.config.checkTimeout()) => t -> newExp } + val newMatches = currentMatches ++ remainingTerms.collect { case t if t.sort == c.snap.sort && v.decider.check(BuiltinEquals(t, c.snap), Verifier.config.checkTimeout()) => t -> newExp } resolveChunks(newMatches, remainingChunks.filter(_ != c), remainingTerms.filter(!newMatches.contains(_))) } } @@ -62,14 +61,26 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa } } - def transformChunk(b: BasicChunk): Option[Exp] = { + def transformChunk(b: NonQuantifiedChunk): Option[Exp] = { - val rcv = transformTerm(b.args.head) - (b, rcv) match { - case (_, None) => None - case (BasicChunk(FieldID, _, _, _, _, _, _), rcv) => Some(FieldAccessPredicate(FieldAccess(rcv.get, abductionUtils.getField(b.id, s.program))(), transformTerm(b.perm).get)()) - case (BasicChunk(PredicateID, id, _, _, _, _, _), rcv) => Some(PredicateAccessPredicate(PredicateAccess(Seq(rcv.get), id.name)(), transformTerm(b.perm).get)()) - //Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get)) + b match { + case bc: BasicChunk => + val rcv = transformTerm(bc.args.head) + (bc, rcv) match { + case (_, None) => None + case (BasicChunk(FieldID, _, _, _, _, _, _), rcv) => Some(FieldAccessPredicate(FieldAccess(rcv.get, abductionUtils.getField(bc.id, s.program))(), transformTerm(b.perm).get)()) + case (BasicChunk(PredicateID, id, _, _, _, _, _), rcv) => Some(PredicateAccessPredicate(PredicateAccess(Seq(rcv.get), id.name)(), transformTerm(b.perm).get)()) + + } + case mwc: MagicWandChunk => + val rcvs = mwc.args.map(a => a -> transformTerm(a)).toMap + if (rcvs.values.toSeq.contains(None)) None else { + val shape = mwc.id.ghostFreeWand + val expBindings = mwc.bindings.map(b => b._1 -> rcvs(b._2._1).get) + val instantiated = shape.replace(expBindings) + Some(instantiated) + //Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get)) + } } } @@ -122,12 +133,12 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa } case lv: LocalVar => { val term: Term = s.g.values.getOrElse(lv, targetVars(lv))._1 - transformTerm(term).get + transformTerm(term).get } } Some(res) } catch { - case _: NoSuchElementException => if(strict) None else Some(e) + case _: NoSuchElementException => if (strict) None else Some(e) } } } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index b53383e14..9166f4452 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -178,7 +178,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { consumes(s, posts, postViolated, v)(QS) } { (s1: State, _: Term, v1: Verifier) => { - // TODO nklose This fails to generate statements if we do abstraction + // TODO nklose We want to do abstraction, but that might require adding folds and such... val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar) val vars = s1.g.values.collect { case (v2, t) if formals.contains(v2) => (v2, t) } val newPosts = BiAbductionSolver.solveFraming(s1, v1, vars, method.pos)