From 0d566427c26f30a1e947e31c7972d6ae002785ce Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 17 Oct 2024 17:24:14 +0200 Subject: [PATCH] Revamped loops for new abstraction --- src/main/scala/Config.scala | 2 +- src/main/scala/biabduction/Abduction.scala | 4 +- src/main/scala/biabduction/Abstraction.scala | 22 +- src/main/scala/biabduction/BiAbduction.scala | 18 +- src/main/scala/biabduction/Invariant.scala | 234 ++++++++++-------- .../scala/biabduction/VarTransformer.scala | 2 +- src/main/scala/rules/Executor.scala | 3 +- .../MagicWandSnapFunctionsContributor.scala | 3 +- 8 files changed, 166 insertions(+), 122 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index a21ad4ca5..b0fd1cfb6 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(true), // Set to true for biabduction testing + default = Some(false), noshort = true ) diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index 33e813a4f..ec9397191 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -116,7 +116,7 @@ object AbductionRemove extends AbductionRule { private def consumeChunks(chunks: Seq[BasicChunk], q: AbductionQuestion)(Q: AbductionQuestion => VerificationResult): VerificationResult = { chunks match { case Seq() => Q(q) - case c :: cs => + case c +: cs => val c1 = findChunk[BasicChunk](q.s.h.values, c.id, c.args, q.v).get val resource: Resource = c.resourceID match { case PredicateID => q.s.program.predicates.head @@ -191,7 +191,7 @@ object AbductionFold extends AbductionRule { protected def findFirstFieldChunk(locs: Seq[FieldAccess], q: AbductionQuestion)(Q: Option[(FieldAccess, BasicChunk)] => VerificationResult): VerificationResult = { locs match { case Seq() => Q(None) - case loc :: rest => + case loc +: rest => checkChunk(loc, q.s, q.v, q.lostAccesses) { case Some(chunk) => Q(Some(loc, chunk)) case None => findFirstFieldChunk(rest, q)(Q) diff --git a/src/main/scala/biabduction/Abstraction.scala b/src/main/scala/biabduction/Abstraction.scala index b4da43a5a..54af98a5e 100644 --- a/src/main/scala/biabduction/Abstraction.scala +++ b/src/main/scala/biabduction/Abstraction.scala @@ -7,6 +7,8 @@ import viper.silicon.state._ import viper.silicon.verifier.Verifier import viper.silver.ast._ +import scala.annotation.tailrec + object AbstractionApplier extends RuleApplier[AbstractionQuestion] { override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply) } @@ -16,7 +18,7 @@ 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 varTran: VarTransformer = VarTransformer(s, v, s.g.values, Heap()) def isTriggerField(bc: BasicChunk): Boolean = { bc.resourceID match { @@ -33,7 +35,7 @@ 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 => + 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) { @@ -52,16 +54,16 @@ object AbstractionFold extends AbstractionRule { } -// 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 { + @tailrec 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 chunk +: rest => + q.varTran.transformTerm(chunk.snap) match { case None => findWandFieldChunk(rest, q) - case Some(lhs) => Some((lhs, chunk)) + case Some(snap) => Some((snap, chunk)) } } } @@ -86,7 +88,7 @@ object AbstractionPackage extends AbstractionRule { object AbstractionJoin extends AbstractionRule { override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.toSeq + val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect{case Some(wand: MagicWand) => wand}.toSeq val pairs = wands.combinations(2).toSeq pairs.collectFirst { case wands if wands(0).right == wands(1).left => (wands(0), wands(1)) @@ -94,8 +96,8 @@ object AbstractionJoin extends AbstractionRule { } match { case None => Q(None) 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))) + magicWandSupporter.packageWand(q.s, MagicWand(w1.left, w2.right)(), Seqn(Seq(Apply(w1)(), Apply(w2)()), Seq())(), pve, q.v) { + (s1, wandChunk, v1) => Q(Some(q.copy(s = s1.copy(h = s1.h.+(wandChunk)), v = v1))) } } } @@ -111,7 +113,7 @@ object AbstractionApply extends AbstractionRule { 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)) + (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 1c6ea6283..b8bfd1123 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -2,6 +2,7 @@ package viper.silicon.biabduction import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces._ +import viper.silicon.interfaces.state.NonQuantifiedChunk import viper.silicon.rules.{executionFlowController, executor, producer} import viper.silicon.state._ import viper.silicon.state.terms.Term @@ -152,23 +153,22 @@ object BiAbductionSolver { - 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)) + def solveAbstraction(s: State, v: Verifier)(Q: (State, Seq[Exp], Verifier) => VerificationResult): VerificationResult = { + val q = AbstractionQuestion(s, v) + AbstractionApplier.applyRules(q) { q1 => + Success(Some(solveFraming(q1.s, q1.v, q1.s.g.values))) } match { - case NonFatalResult => + case res: NonFatalResult => val exps = abductionUtils.getFramingSuccesses(res).head - Q(exps.s, exps.v, exps.posts) + Q(exps.s, exps.posts, exps.v) } } - // 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. + // This does not do abstraction, but just transforms state back into expressions. 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) - val res = s.h.values.collect { case c: BasicChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq + val res = s.h.values.collect { case c: NonQuantifiedChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq val bcs = v.decider.pcs.branchConditions.map { term => tra.transformTerm(term) }.collect { case Some(e) if e != TrueLit()() && !ignoredBcs.contains(e) => e }.toSet val posts = res.map { e => if (bcs.isEmpty) { diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index 71215fb43..e9701c63b 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -1,27 +1,29 @@ package viper.silicon.biabduction import viper.silicon.interfaces._ +import viper.silicon.interfaces.state.Chunk +import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.rules.producer.produces -import viper.silicon.rules.{executionFlowController, executor, producer} -import viper.silicon.state.State +import viper.silicon.rules.{evaluator, executionFlowController, executor, producer} +import viper.silicon.state.{BasicChunk, ChunkIdentifier, Heap, State} import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ import viper.silver.cfg.silver.SilverCfg.SilverBlock import viper.silver.cfg.{ConditionalEdge, Edge, LoopHeadBlock} -import viper.silver.verifier.{DummyReason, PartialVerificationError} import viper.silver.verifier.errors.{ContractNotWellformed, Internal} +import viper.silver.verifier.{DummyReason, PartialVerificationError} // Many things are either in relation to the current loop iteration (which we call relative) or the total state/the state // before the loop (which we call absolute). -case class InvariantAbductionQuestion(preAbstraction: Seq[Exp], postAbstraction: Seq[Exp], absValues: Map[AbstractLocalVar, Exp]) +case class InvariantAbductionQuestion(preHeap: Heap, preAbstraction: Seq[Exp], postAbstraction: Seq[Exp]) //, absValues: Map[AbstractLocalVar, Exp]) object LoopInvariantSolver { private val pve: PartialVerificationError = Internal() - private def pveLam(exp: Exp) = pve + private def pveLam(exp: Exp): PartialVerificationError = pve // TODO this is oversimplified, we actually should solve a proper abduction question with the other invariant. // In particular, we need to ensure that permissions are not doubled between the two. Whenever the two invariants describe the same @@ -34,31 +36,55 @@ object LoopInvariantSolver { } } - // TODO do we need to check well-definedness of the loop condition + private def findChunkFromExp(loc: LocationAccess, s: State, v: Verifier)(Q: Option[BasicChunk] => VerificationResult): VerificationResult = { + + // TODO Currently we assume only one arg, which may be wrong for arbitrary predicates + val arg = loc match { + case FieldAccess(rcv, _) => rcv + case PredicateAccess(args, _) => args.head + } + evaluator.eval(s, arg, pve, v) { (s2, term, _, v2) => + val resource = loc.res(s2.program) + val id = ChunkIdentifier(resource, s2.program) + val chunk = findChunk[BasicChunk](s2.h.values, id, Seq(term), v2) + Q(chunk) + } + } + + protected def findChunks(locs: Seq[LocationAccess], s: State, v: Verifier)(Q: Seq[BasicChunk] => VerificationResult): VerificationResult = { + locs match { + case Seq() => Q(Seq()) + case loc +: rest => + findChunkFromExp(loc, s, v){ + case Some(chunk) => findChunks(rest, s, v) { chunks => Q(chunk +: chunks) } + } + } + } + + // TODO do we need to check well-definedness of the loop condition? def solveLoopInvariants(sPre: State, vPre: Verifier, origVars: Seq[AbstractLocalVar], loopHead: LoopHeadBlock[Stmt, Exp], loopEdges: Seq[Edge[Stmt, Exp]], joinPoint: Option[SilverBlock], - q: InvariantAbductionQuestion = InvariantAbductionQuestion(Seq(), Seq(), Map()), + q: InvariantAbductionQuestion = InvariantAbductionQuestion(Heap(), Seq(), Seq()), iteration: Int = 1): VerificationResult = { // We want to remove the loop condition from many inferred expressions - // TODO we are assuming there is only one loop edge. Is this true for all loops we care about? + // We assuming there is only one loop edge. val loopCondition = loopEdges.head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition - val wvs = sPre.methodCfg.writtenVars(loopHead).filter(origVars.contains) - val absVars = origVars.filterNot(wvs.contains) + //val wvs = sPre.methodCfg.writtenVars(loopHead).filter(origVars.contains) + //val absVars = origVars.filterNot(wvs.contains) - // TODO nklose actually we probably do want to consume/produce the invariants in between iterations, but just check them - // TODO (and maybe just fail if they do not hold). Maybe? Actually I am not so sure this is correct // Produce the already known invariants. They are consumed at the end of the loop body, so we need to do this every iteration produces(sPre, freshSnap, loopHead.invs, ContractNotWellformed, vPre)((sPreInv, vPreInv) => // Run the loop the first time to check whether we abduce any new state - executionFlowController.locally(sPreInv, vPreInv)((sFP, vFP) => + executionFlowController.locally(sPreInv, vPreInv) { (sFP, vFP) => // TODO nklose follows should be private. We can exec the statement block instead? - executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint)((_, _) => Success())) match { + executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint)((_, _) => Success()) + } match { // Abduction has failed so we fail case f: Failure => f @@ -66,103 +92,117 @@ object LoopInvariantSolver { case nonf: NonFatalResult => val abdReses = abductionUtils.getAbductionSuccesses(nonf) - val preStateVars = sPreInv.g.values.filter { case (v, _) => absVars.contains(v) } + val preStateVars = sPreInv.g.values.filter { case (v, _) => origVars.contains(v) } val newStateOpt = abdReses.map { abd => abd.toPrecondition(preStateVars, sPreInv.h, Seq(loopCondition)) } if (newStateOpt.contains(None)) { return Failure(pve dueTo DummyReason) } - val newPreState = newStateOpt.flatMap(_.get) + val abductionResults = newStateOpt.flatMap(_.get) // Do the second pass so that we can compare the state at the end of the loop with the state at the beginning - // Get the state at the beginning of the loop with with the abduced things added - producer.produces(sPreInv, freshSnap, newPreState, pveLam, vPreInv) { (sPreAbd, vPreAbd) => - - // First iteration - val q1 = if (iteration == 1) { - // Transform things at the beginning of the loop to only use the variables existing before the loop - // This is required to calculate 'absolute' values - val firstVarTrans = VarTransformer(sPreAbd, vPreAbd, preStateVars, sPreAbd.h) - val firstAbsValues: Map[AbstractLocalVar, Exp] = wvs.collect { case v => v -> firstVarTrans.transformExp(v) } - .collect { case (v, v1) if v1.isDefined => (v, v1.get) }.toMap - q.copy(absValues = firstAbsValues) - } else { - q - } - - BiAbductionSolver.solveAbstraction(sPreAbd, vPreAbd, q1.preAbstraction ++ newPreState) { newPreAbstraction => - val res = executionFlowController.locally(sPreAbd, vPreAbd) { (sPreAbd2, vPreAbd2) => - executor.follows(sPreAbd2, loopEdges, pveLam, vPreAbd2, joinPoint)((sPost, vPost) => { - - // Values of the variables at the end of loop in terms of the beginning of the loop - val relVarTrans = VarTransformer(sPost, vPost, sPreAbd2.g.values.filter { case (v, _) => origVars.contains(v) }, sPreAbd2.h) - val relPreValues = sPost.g.values.collect { case (v, (t, _)) if wvs.contains(v) => (v, relVarTrans.transformTerm(t)) } - .collect { case (v, e) if e.isDefined => (v, e.get) } - - - // We would like to transform as much as possible to the absVars. - // However, if state is created, then this my not be possible. Then we are willing to transform things to - // wvs as well - val postTranAbs = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => absVars.contains(v) }, sPost.h) - val postTranOrig = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => origVars.contains(v) }, sPost.h) - val postsRaw = BiAbductionSolver.solveFraming(sPost, vPost, sPost.g.values, NoPosition, Seq(loopCondition)).posts - val postsTran = postsRaw.map { exp => - val wvsPost = postTranOrig.transformExp(exp) - postTranAbs.transformExp(wvsPost.get, strict = false).get - } - BiAbductionSolver.solveAbstraction(sPost, vPost, postsTran) { postAbstraction => - - val newAbsPostValues: Map[AbstractLocalVar, Exp] = relPreValues.collect { case (v, e) => (v, e.transform { - case lv: LocalVar if q1.absValues.contains(lv) => q1.absValues(lv) - }) - } - - // To check whether we are done, we take the previous abstractions and "push them forward" an iteration - val relPreAssigns: Map[Exp, Exp] = { - q1.absValues.collect { - case (v, e) if newAbsPostValues.contains(v) => (e, newAbsPostValues(v)) + // Get the state at the beginning of the loop with the abduced things added + producer.produces(sPreInv, freshSnap, abductionResults, pveLam, vPreInv) { (sPreAbd, vPreAbd) => + findChunks(abductionResults.collect { + case loc: FieldAccessPredicate => loc.loc + case loc: PredicateAccessPredicate => loc.loc + }, sPreAbd, vPreAbd) { chunks => + + //val totalAbduced = q.preChunks ++ chunks + BiAbductionSolver.solveAbstraction(sPreAbd.copy(h = q.preHeap.+(Heap(chunks))), vPreAbd) { (newPreState, newPreAbstraction0, newPreV) => + + val preTran = VarTransformer(newPreState, newPreV, preStateVars, newPreState.h) + val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, false).get) + // First iteration + //val q1 = if (iteration == 1) { + // Transform things at the beginning of the loop to only use the variables existing before the loop + // This is required to calculate 'absolute' values + // val firstVarTrans = VarTransformer(sPreAbd, vPreAbd, preStateVars, sPreAbd.h) + // val firstAbsValues: Map[AbstractLocalVar, Exp] = wvs.collect { case v => v -> firstVarTrans.transformExp(v) } + // .collect { case (v, v1) if v1.isDefined => (v, v1.get) }.toMap + // q.copy(absValues = firstAbsValues) + // } else { + // q + // } + + val res = executionFlowController.locally(sPreAbd, vPreAbd) { (sPreAbst2, vPreAbst2) => + executor.follows(sPreAbst2, loopEdges, pveLam, vPreAbst2, joinPoint)((sPost, vPost) => { + + // Values of the variables at the end of loop in terms of the beginning of the loop + //val relVarTrans = VarTransformer(sPost, vPost, sPreAbst2.g.values.filter { case (v, _) => origVars.contains(v) }, sPreAbst2.h) + //val relPreValues = sPost.g.values.collect { case (v, (t, _)) if wvs.contains(v) => (v, relVarTrans.transformTerm(t)) } + // .collect { case (v, e) if e.isDefined => (v, e.get) } + + + // We would like to transform as much as possible to the absVars. + // However, if state is created, then this my not be possible. Then we are willing to transform things to + // wvs as well + //val postTranAbs = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => absVars.contains(v) }, sPost.h) + //val postTranOrig = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => origVars.contains(v) }, sPost.h) + //val postsRaw = BiAbductionSolver.solveFraming(sPost, vPost, sPost.g.values, NoPosition, Seq(loopCondition)).posts + //val postsTran = postsRaw.map { exp => + // val wvsPost = postTranOrig.transformExp(exp) + // postTranAbs.transformExp(wvsPost.get, strict = false).get + //} + BiAbductionSolver.solveAbstraction(sPost, vPost) { (sPostAbs, postAbstraction0, vPostAbs) => + val postStateVars = sPostAbs.g.values.filter { case (v, _) => origVars.contains(v) } + val postTran = VarTransformer(sPostAbs, vPostAbs, postStateVars, sPostAbs.h) + val postAbstraction = postAbstraction0.map(e => postTran.transformExp(e, false).get) + + //val newAbsPostValues: Map[AbstractLocalVar, Exp] = relPreValues.collect { case (v, e) => (v, e.transform { + // case lv: LocalVar if q1.absValues.contains(lv) => q1.absValues(lv) + //}) + //} + + /* + // To check whether we are done, we take the previous abstractions and "push them forward" an iteration + val relPreAssigns: Map[Exp, Exp] = { + q1.absValues.collect { + case (v, e) if newAbsPostValues.contains(v) => (e, newAbsPostValues(v)) + } } - } - val prevPreAbstTrans = q1.preAbstraction.map(_.transform { - case exp: Exp if relPreAssigns.contains(exp) => relPreAssigns(exp) - }) - - val relPostAssigns: Map[Exp, Exp] = { - newAbsPostValues.collect { - case (v, e) if q1.absValues.contains(v) => (q1.absValues(v), e) - } - } - val prevPostAbstTrans = q1.postAbstraction.map(_.transform { - case exp: Exp if relPostAssigns.contains(exp) => - relPostAssigns(exp) - }) - - // If the pushed forward abstraction is the same as the previous one, we are done - if (newPreAbstraction.diff(prevPreAbstTrans).isEmpty && postAbstraction.diff(prevPostAbstTrans).isEmpty) { - - // Swap in the assigned to variables again instead of the absolute values - val newAbsSwapped = newAbsPostValues.collect { case (v, e) if origVars.contains(v) => (e, v) } - val relPreAbstraction = newPreAbstraction.map(_.transform { - case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp) - }) - val postInv = postAbstraction.map(_.transform { - case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp) + val prevPreAbstTrans = q1.preAbstraction.map(_.transform { + case exp: Exp if relPreAssigns.contains(exp) => relPreAssigns(exp) }) - val preInv = relPreAbstraction.flatMap(getPreInvariant) - Success(Some(LoopInvariantSuccess(sPost, vPost, invs = preInv ++ postInv, loopCondition.pos))) - } else { - // Else continue with next iteration, using the state from the end of the loop - executionFlowController.locally(sPost, vPost)((sNext, vNext) => { - solveLoopInvariants(sNext, vNext, origVars, loopHead, loopEdges, joinPoint, q1.copy(preAbstraction = newPreAbstraction, - postAbstraction = postAbstraction, absValues = newAbsPostValues), iteration = iteration + 1) + val relPostAssigns: Map[Exp, Exp] = { + newAbsPostValues.collect { + case (v, e) if q1.absValues.contains(v) => (q1.absValues(v), e) + } + } + val prevPostAbstTrans = q1.postAbstraction.map(_.transform { + case exp: Exp if relPostAssigns.contains(exp) => + relPostAssigns(exp) + })*/ + + // If the pushed forward abstraction is the same as the previous one, we are done + if (newPreAbstraction.diff(q.preAbstraction).isEmpty && postAbstraction.diff(q.postAbstraction).isEmpty) { + + // Swap in the assigned to variables again instead of the absolute values + /* + val newAbsSwapped = newAbsPostValues.collect { case (v, e) if origVars.contains(v) => (e, v) } + val relPreAbstraction = newPreAbstraction.map(_.transform { + case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp) + }) + val postInv = postAbstraction.map(_.transform { + case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp) + })*/ + + val preInv = newPreAbstraction.flatMap(getPreInvariant) + Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = preInv ++ postAbstraction, loopCondition.pos))) + } else { + // Else continue with next iteration, using the state from the end of the loop + //executionFlowController.locally(sPost, vPost)((sNext, vNext) => { + solveLoopInvariants(sPostAbs, vPostAbs, origVars, loopHead, loopEdges, joinPoint, q.copy(preHeap = newPreState.h, preAbstraction = newPreAbstraction, + postAbstraction = postAbstraction), iteration = iteration + 1) + //} + //) } - ) } } + ) } - ) + res } - res } } }) diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index 771681840..029e4abc4 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -76,7 +76,7 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa 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 expBindings = mwc.bindings.collect { case (lv, (term, _)) if rcvs.contains(term) => lv -> rcvs(term).get} val instantiated = shape.replace(expBindings) Some(instantiated) //Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get)) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 88c44e203..ce983ba75 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -734,7 +734,8 @@ object executor extends ExecutionRules { exhaleExt = false, reserveHeaps = Nil) } - assert(s2.reserveHeaps.length == s.reserveHeaps.length) + // TODO nklose figure out what is going on here + //assert(s2.reserveHeaps.length == s.reserveHeaps.length) val smCache3 = chWand match { case ch: QuantifiedMagicWandChunk if s2.heapDependentTriggers.contains(MagicWandIdentifier(wand, s2.program)) => diff --git a/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala index c2b925c6a..b124566e5 100644 --- a/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala +++ b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala @@ -40,7 +40,8 @@ class MagicWandSnapFunctionsContributor(preambleReader: PreambleReader[String, S */ override def analyze(program: Program): Unit = { // If there are not magic wands, do not add any definitions or axioms - if (!program.existsDefined { case ast.MagicWand(_, _) => true }) return + // Removed for abduction + //if (!program.existsDefined { case ast.MagicWand(_, _) => true }) return collectedSorts = InsertionOrderedSet(sorts.MagicWandSnapFunction) collectedFunctionDecls = preambleReader.readPreamble(FILE_DECLARATIONS)