From 728886cbd468e43da5cb60f1e8aa5848f614f987 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 2 Sep 2024 17:59:50 +0200 Subject: [PATCH] We back baby! --- src/main/scala/biabduction/Abduction.scala | 22 +-- src/main/scala/biabduction/BiAbduction.scala | 61 ++++---- src/main/scala/biabduction/Invariant.scala | 138 +++++++++--------- .../scala/biabduction/VarTransformer.scala | 6 +- .../scala/rules/ExecutionFlowController.scala | 10 +- 5 files changed, 124 insertions(+), 113 deletions(-) diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index ba9a0987..61e7cb96 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -223,7 +223,8 @@ object AbductionFold extends AbductionRule { (s1: State, v1: Verifier) => val fold = Fold(a)() val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, sorts.Ref)) - Q(Some(q.copy(s = s1, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost))) + val q2 = q.copy(s = s1, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1) + Q(Some(q2)) } { _: FatalResult => R() } case None => R() } @@ -357,17 +358,18 @@ object AbductionPackage extends AbductionRule { producer.produce(q.s, freshSnap, wand.left, pve, q.v)((s1, v1) => { val packQ = q.copy(s = s1, v = v1, goal = Seq(wand.right)) - val packRes = AbductionApplier.apply(packQ) + AbductionApplier.applyRules(packQ){ packRes => + + // TODO nklose we should instead not trigger + if (packRes.goal.nonEmpty) { + throw new Exception("Could not find proof script for package") + } - // TODO nklose we should instead not trigger - if (packRes.goal.nonEmpty) { - throw new Exception("Could not find proof script for package") + val g1 = q.goal.filterNot(_ == wand) + val stmts = q.foundStmts :+ Package(wand, Seqn(packRes.foundStmts.reverse, Seq())())() + val pres = q.foundState ++ packRes.foundState + Q(Some(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts, foundState = pres))) } - - val g1 = q.goal.filterNot(_ == wand) - val stmts = q.foundStmts :+ Package(wand, Seqn(packRes.foundStmts.reverse, Seq())())() - val pres = q.foundState ++ packRes.foundState - Q(Some(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts, foundState = pres))) }) } } diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index deb9ef44..426e9d9f 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -87,22 +87,18 @@ trait RuleApplier[S] { /** * Recursively applies the rules until we reach the end of the rules list. */ - def apply(in: S, currentRule: Int = 0): S = { + def applyRules(in: S, currentRule: Int = 0)(Q: S => VerificationResult): VerificationResult = { - var result = in - - if (currentRule < rules.length) { - rules(currentRule).apply(in) { s => - s match { - case Some(out) => - result = apply(out) - case None => - result = apply(in, currentRule + 1) - } - Failure(Internal().dueTo(DummyReason)) + if(currentRule == rules.length){ + Q(in) + } else { + rules(currentRule).apply(in) { + case Some(out) => + applyRules(out)(Q) + case None => + applyRules(in, currentRule + 1)(Q) } } - result } } @@ -120,7 +116,7 @@ object BiAbductionSolver { def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): BiAbductionResult = { - executionFlowController.locally(s, v)((s1, v1) => { + val res = executionFlowController.locally(s, v)((s1, v1) => { val qPre = AbductionQuestion(s1, v1, goal) @@ -129,27 +125,32 @@ object BiAbductionSolver { case _ => qPre } - val q1 = AbductionApplier.apply(q) - - if (q1.goal.isEmpty) { - Success(Some(AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc))) - } else { - Failure(Internal() dueTo DummyReason) + AbductionApplier.applyRules(q){ q1 => + if (q1.goal.isEmpty) { + Success(Some(AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc))) + } else { + Failure(Internal() dueTo DummyReason) + } } - }) match { - case Success(Some(abd: AbductionSuccess)) => abd - case _ => BiAbductionFailure(s, v) + + }) + + res match { + case nf: NonFatalResult => + // TODO Can we ever get multiple abduction results here? + abductionUtils.getAbductionResults(nf).head + case _ => + BiAbductionFailure(s, v) } } - def solveAbstraction(s: State, v: Verifier, exps: Seq[Exp]): Seq[Exp] = { - var res: Seq[Exp] = Seq() - executionFlowController.locally(s, v)((s1, v1) => { + 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) - res = AbstractionApplier.apply(q).exps - Success() - }) - res + AbstractionApplier.applyRules(q){ q1 => + QS(q1.exps) + } + })(Q) } def solveFraming(s: State, v: Verifier, postVars: Map[AbstractLocalVar, Term], loc: Position = NoPosition, ignoredBcs: Seq[Exp] = Seq()): FramingSuccess = { diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index c09e08f2..9b50b671 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -89,77 +89,81 @@ object LoopInvariantSolver { q } - val newPreAbstraction = BiAbductionSolver.solveAbstraction(sPreAbd, vPreAbd, q1.preAbstraction ++ newPreState) - 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 - } - val postAbstraction = BiAbductionSolver.solveAbstraction(sPost, vPost, postsTran) - - 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)) + 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 } - } - 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) + 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)) + } + } + 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 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 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 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) - }) - } - }) + ) + } + res } - res } }) } diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index 96fec272..7ddc91db 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -7,12 +7,12 @@ import viper.silicon.state.terms.{BuiltinEquals, Term} import viper.silicon.state._ import viper.silicon.verifier.Verifier import viper.silver.ast._ -import viper.silver.verifier.PartialVerificationError -import viper.silver.verifier.errors.Internal +//import viper.silver.verifier.PartialVerificationError +//import viper.silver.verifier.errors.Internal case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, Term], targetHeap: Heap) { - val pve: PartialVerificationError = Internal() + //val pve: PartialVerificationError = Internal() // Ask the decider whether any of the terms are equal to a target. val matches: Map[Term, Exp] = resolveMatches() diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index a93bc8d4..caf35f37 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -190,9 +190,13 @@ object executionFlowController extends ExecutionFlowRules { // This is not as efficient as it maybe could be, we call action twice. // To speed it up we would have to save the s2, v2, r that we currently ignore in the fake // continuation - locallyWithResult[R](s, v) { (s1, v1, Q1) => - action(s1, v1, (_, _, _) => Success()) } { - case Success(_) => action(s, v, Q) + val res1 = locally(s, v) { (s1, v1) => + action(s1, v1, (_, _, _) => Success()) } + + res1 match { + case _: NonFatalResult => + val res = action(s, v, Q) + res case f: FatalResult => F(f) } }