From fad3824179b2db0988601bc3571eb21246b5486c Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 4 Dec 2024 18:46:40 +0100 Subject: [PATCH] Worked on branching --- src/main/scala/biabduction/Abduction.scala | 2 +- src/main/scala/biabduction/BiAbduction.scala | 313 +++++++++++------- src/main/scala/biabduction/Invariant.scala | 38 +-- src/main/scala/rules/Executor.scala | 4 +- .../scala/supporters/MethodSupporter.scala | 49 +-- .../resources/biabduction/nlist/branching.vpr | 3 - .../resources/biabduction/nnlist/loop.vpr | 2 +- 7 files changed, 229 insertions(+), 182 deletions(-) diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index a6b2af90..3d13466f 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -224,7 +224,7 @@ object AbductionFold extends AbductionRule { val tryFold = predicateSupporter.fold(q.s, pred, chunk.args.toList, None, terms.FullPerm, None, wildcards, pveTransformed, q.v) { (s1, v1) => consumer.consume(s1, a, pve, v1) { (s2, _, v2) => - Success(Some(AbductionSuccess(s2, v2, Seq(v2.decider.pcs.duplicate()), Seq(), Seq(Fold(a)())))) + Success(Some(AbductionSuccess(s2, v2, v2.decider.pcs.duplicate(), Seq(), Seq(Fold(a)())))) } } tryFold match { diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index 84c37dd3..1fb10c6d 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -2,8 +2,7 @@ package viper.silicon.biabduction import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces._ -import viper.silicon.interfaces.state.Chunk -import viper.silicon.interfaces.state.NonQuantifiedChunk +import viper.silicon.interfaces.state.{Chunk, NonQuantifiedChunk} import viper.silicon.rules.consumer.consumes import viper.silicon.rules.{executionFlowController, executor, producer} import viper.silicon.state._ @@ -12,7 +11,7 @@ import viper.silicon.utils.ast.BigAnd import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ -import viper.silver.verifier.errors.{Internal, PostconditionViolated} +import viper.silver.verifier.errors.Internal import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotFound} import viper.silver.verifier.{DummyReason, PartialVerificationError, VerificationError} @@ -27,119 +26,169 @@ trait BiAbductionSuccess extends BiAbductionResult // TODO nklose BiAbductionSuccess should be able to provide arbitrary transformations of methods. Then we can just // use this for all cases and need less dummy stuff -case class AbductionSuccess(s: State, v: Verifier, pcs: Seq[PathConditionStack], state: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), trigger: Option[Positioned] = None) extends BiAbductionSuccess { +case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), trigger: Option[Positioned] = None) extends BiAbductionSuccess { - private def bcsExps(pc: PathConditionStack, ignoredBcs: Seq[Term]): Set[Exp] = { - val prevPcs = v.decider.pcs - v.decider.setPcs(pc) - val varTrans = VarTransformer(s, v, s.g.values, s.h) - val bcTerms = v.decider.pcs.branchConditions - val bcExpOpt = bcTerms.collect { - case bc if !ignoredBcs.contains(bc) => varTrans.transformTerm(bc) - } - val bcExp = bcExpOpt.collect { case Some(e) => e }.toSet - v.decider.setPcs(prevPcs) - bcExp + override def toString: String = { + "Abduced pres " + state.length + ", Abduced statements " + stmts.length } - def addToMethod(m: Method): Option[Method] = { + def addToMethod(m: Method, bcsTerms: Seq[Term]): Option[Method] = { val ins = m.formalArgs.map(_.localVar) val preHeap = s.oldHeaps.head._2 - val inVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) } - val pres = toPrecondition(inVars, preHeap) - pres.map { somePres => - + val preVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) } + val prevPcs = v.decider.pcs + v.decider.setPcs(pcs) + val bcExps = getBcExps(bcsTerms) + val pres = getPreconditions(preVars, preHeap, bcExps) + val finalStmts = getStatements(bcExps) + v.decider.setPcs(prevPcs) + if (pres.isEmpty || finalStmts.isEmpty) { + None + } else { + val finalStmt = finalStmts.get val body = m.body.get val newBody: Seqn = trigger match { case None => body - case Some(t: Stmt) if t == abductionUtils.dummyEndStmt => Seqn(body.ss ++ stmts, body.scopedSeqnDeclarations)(body.pos, body.info, body.errT) + case Some(t: Stmt) if t == abductionUtils.dummyEndStmt => Seqn(body.ss ++ finalStmt, body.scopedSeqnDeclarations)(body.pos, body.info, body.errT) case Some(t: Stmt) if abductionUtils.isEndOfLoopStmt(t) => val loop = abductionUtils.getWhile(t.asInstanceOf[Label].invs.head, m) - val newLoopBody = loop.body.copy(ss = loop.body.ss ++ stmts)(pos = loop.body.pos, info = loop.body.info, errT = loop.body.errT) + val newLoopBody = loop.body.copy(ss = loop.body.ss ++ finalStmt)(pos = loop.body.pos, info = loop.body.info, errT = loop.body.errT) val newLoop = loop.copy(body = newLoopBody)(loop.pos, loop.info, loop.errT) body.transform { case stmt if stmt == loop => newLoop } case Some(t: Stmt) => body.transform { case stmt if stmt == t => - Seqn(stmts :+ t, Seq())(t.pos, t.info, t.errT) + Seqn(finalStmt :+ t, Seq())(t.pos, t.info, t.errT) } case Some(e: Exp) => body.transform { case ifStmt: If if ifStmt.cond == e => Seqn(stmts :+ ifStmt, Seq())(ifStmt.pos, ifStmt.info, ifStmt.errT) case whileStmt: While if whileStmt.cond == e => Seqn(stmts :+ whileStmt, Seq())(whileStmt.pos, whileStmt.info, whileStmt.errT) } } - m.copy(pres = m.pres ++ somePres, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT) + Some(m.copy(pres = (m.pres ++ pres.get).distinct, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) } } - override def toString: String = { - "Abduced pres " + state.length + ", Abduced statements " + stmts.length + def getBcExps(bcsTerms: Seq[Term]): Seq[Option[Exp]] = { + val varTrans = VarTransformer(s, v, s.g.values, s.h) + val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) } + bcExps } - def toPrecondition(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], preHeap: Heap, ignoredBcs: Seq[Term] = Seq()): Option[Seq[Exp]] = { + def getStatements(bcExps: Seq[Option[Exp]]): Option[Seq[Stmt]] = { + if (stmts.isEmpty) { + Some(Seq()) + } else if (bcExps.contains(None)) { + None + } else { + val con = BigAnd(bcExps.map { case Some(e) => e }) + con match { + case _: TrueLit => Some(stmts) + case _ => Some(Seq(If(con, Seqn(stmts, Seq())(), Seqn(Seq(), Seq())())())) + } + } + } - val pres = pcs.map { pc => + def getPreconditions(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], preHeap: Heap, bcExps: Seq[Option[Exp]]): Option[Seq[Exp]] = { - // We have to use the pcs from the abduction point - val prevPcs = v.decider.pcs - v.decider.setPcs(pc) + if (state.isEmpty) { + Some(Seq()) + } else { + + // We use the pcs from the abduction point val varTrans = VarTransformer(s, v, preVars, preHeap) val presTransformed = state.map { pre => varTrans.transformExp(pre) } - + val bcPreExps = bcExps.map { + case Some(exp) => varTrans.transformExp(exp) + } + + // If we cannot express the precondition, we have to fail + // If we fail to express some branch conditions, we can overapproximate the precondition if (presTransformed.contains(None)) { - None // We could not express the state as a precondition + None } else { - - val bcs = bcsExps(pc, ignoredBcs).map { exp => varTrans.transformExp(exp) }.collect { case Some(e) => e } - val presFinal = presTransformed.map { e => - if (bcs.isEmpty) { - e.get - } else { - Implies(BigAnd(bcs), e.get)() - } + val pres = presTransformed.collect { case Some(e) => e } + val bcs = BigAnd(bcPreExps.collect { case Some(e) => e }) + bcs match { + case _: TrueLit => Some(pres) + case _ => Some(Seq(Implies(bcs, BigAnd(pres))())) } - v.decider.setPcs(prevPcs) - Some(presFinal) } } - if (pres.contains(None)) { - None - } else { - // TODO nklose we maybe want to combine stuff here - Some(pres.flatMap(_.get).distinct) - } } } -case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), loop: While) extends BiAbductionSuccess { +case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), loop: While, pcs: PathConditionStack) extends BiAbductionSuccess { override def toString: String = "Successful loop invariant abduction" - def addToMethod(m: Method): Method = { - val body = m.body.get - val newBody = body.transform { - case l: While if l.cond == loop.cond => - l.copy(invs = l.invs ++ invs)(pos = l.pos, info = l.info, errT = l.errT) - case other => other + def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = { + + val prevPcs = v.decider.pcs + v.decider.setPcs(pcs) + val bcTran = VarTransformer(s, v, s.g.values, s.h) + val bcExps = bcs.map { t => bcTran.transformTerm(t) } + v.decider.setPcs(prevPcs) + if (bcExps.contains(None)) { + None + } else { + val con = BigAnd(bcExps.map { case Some(e) => e }) + val inv = con match { + case _: TrueLit => BigAnd(invs) + case _ => Implies(con, BigAnd(invs))() + } + val body = m.body.get + val newBody = body.transform { + case l: While if l.cond == loop.cond => + l.copy(invs = l.invs :+ inv)(pos = l.pos, info = l.info, errT = l.errT) + case other => other + } + Some(m.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) } - m.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT) } } -case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], stmts: Seq[Stmt], loc: Positioned, pcs: PathConditionStack, conds: Seq[Exp]) extends BiAbductionSuccess { +case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], stmts: Seq[Stmt], loc: Positioned, pcs: PathConditionStack, varTran: VarTransformer) extends BiAbductionSuccess { override def toString: String = "Successful framing" - def addToMethod(m: Method): Method = { - /*val (newPost, stmt) = if (conds.isEmpty) { - (BigAnd(posts), Seqn(stmts, Seq())()) + def getBcExps(bcsTerms: Seq[Term]): Option[Exp] = { + val varTrans = VarTransformer(s, v, s.g.values, s.h) + val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) } + if (bcExps.contains(None)) { + None } else { - (Implies(BigAnd(conds), BigAnd(posts))(), If(BigAnd(conds), Seqn(stmts, Seq())(), Seqn(Seq(), Seq())())()) - }*/ - val body = m.body.get - val newBody = body.copy(ss = body.ss :+ Seqn(stmts, Seq())())(pos = body.pos, info = body.info, errT = body.errT) - m.copy(posts = m.posts ++ posts, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT) + Some(BigAnd(bcExps.map { case Some(e) => e })) + } + } + + + def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = { + val prevPcs = v.decider.pcs + v.decider.setPcs(pcs) + val bcExpsOpt = getBcExps(bcs) + v.decider.setPcs(prevPcs) + + bcExpsOpt.flatMap { bcExps => + + val bcStmts = (bcExps, stmts) match { + case (_, Seq()) => Seq() + case (_: TrueLit, _) => stmts + case _ => Seq(If(bcExps, Seqn(stmts, Seq())(), Seqn(Seq(), Seq())())()) + } + + val bcPost = (bcExps, posts) match { + case (_, Seq()) => Seq() + case (_: TrueLit, _) => posts + case _ => Seq(Implies(bcExps, BigAnd(posts))()) + } + + val body = m.body.get + val newBody = body.copy(ss = body.ss ++ bcStmts)(pos = body.pos, info = body.info, errT = body.errT) + Some(m.copy(posts = m.posts ++ bcPost, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) + + } } } @@ -227,48 +276,29 @@ object BiAbductionSolver { case SiliconAbductionFailureContext(trafo) if trafo.isDefined => trafo.get } - val reses = executionFlowController.locally(s, v) { (s1, v1) => - val qPre = AbductionQuestion(s1, v1, Seq(abdGoal), trigger = trigger) - val q = tra match { - case Some(trafo) => trafo.f(qPre).asInstanceOf[AbductionQuestion] - case _ => qPre - } - AbductionApplier.applyRules(q) { - q1 => - if (q1.goal.isEmpty) { - Success(Some(AbductionSuccess(q1.s, q1.v, Seq(q1.v.decider.pcs.duplicate()), q1.foundState.reverse, q1.foundStmts.reverse, trigger))) - } else { - f - } - } + //val reses = executionFlowController.locally(s, v) { (s1, v1) => + val qPre = AbductionQuestion(s, v, Seq(abdGoal), trigger = trigger) + val q = tra match { + case Some(trafo) => trafo.f(qPre).asInstanceOf[AbductionQuestion] + case _ => qPre } - reses match { - case f: FatalResult => f - case nf: NonFatalResult => - abductionUtils.getAbductionSuccesses(nf) match { - case Seq(abd) => - producer.produces(s, freshSnap, abd.state, _ => Internal(), v) { - (s2, v2) => - executor.execs(s2, abd.stmts, v2) { - (s3, v3) => - if (v3.decider.checkSmoke()) { - // TODO nklose this result still receives the branch conditions as an implication, which is nonsense - // Easy fix: - // val conds = initPcs.branchConditions.map(initTra.transformTerm).collect({case Some(e) => e}) - Success(Some(BiAbductionFailure(s, v, initPcs))) - } else { - Q(s3, abd.copy(s = s3, v = v3), v3) - } - } - } - case Seq(a, b) if a.state == b.state && a.stmts == b.stmts => - producer.produces(s, freshSnap, a.state, _ => Internal(), v) { - (s2, v2) => - executor.execs(s2, a.stmts, v2) { - (s3, v3) => - Q(s3, a.copy(s = s3, v = v3, pcs = a.pcs ++ b.pcs), v3) - } - } + AbductionApplier.applyRules(q) { + q1 => + if (q1.goal.isEmpty) { + val abd = AbductionSuccess(q1.s, q1.v, q1.v.decider.pcs.duplicate(), q1.foundState.reverse, q1.foundStmts.reverse, trigger) + producer.produces(s, freshSnap, abd.state, _ => Internal(), v) { + (s2, v2) => + executor.execs(s2, abd.stmts, v2) { + (s3, v3) => + if (v3.decider.checkSmoke()) { + Success(Some(BiAbductionFailure(s, v, initPcs))) + } else { + Q(s3, abd.copy(s = s3, v = v3), v3) + } + } + } + } else { + f } } } @@ -297,10 +327,7 @@ object BiAbductionSolver { } { // We consumed all the posts and did not find any new ones. So create a fresh Framing Success with the bcs case Seq() => - val bcsExps = v.decider.pcs.branchConditions - .map { bc => tra.transformTerm(bc) } - .collect{ case Some(e) => e} // TODO we currently just discard bcs we cannot transform. Is this always right? - Q(FramingSuccess(s1, v1, Seq(), Seq(), loc, v.decider.pcs.duplicate(), bcsExps)) // No new state or needed stmts + Q(FramingSuccess(s1, v1, Seq(), Seq(), loc, v.decider.pcs.duplicate(), tra)) // No new state or needed stmts // We consumed the post conditions and found new ones. Handle the new ones and add them to the result case newPosts1 => solveFraming(s1, v1, pvef, tra, loc, newPosts1) { frame => @@ -327,8 +354,49 @@ object BiAbductionSolver { } } + def resolveAbductionResults(m: Method, nf: NonFatalResult): Option[Method] = { + val abdReses = abductionUtils.getAbductionSuccesses(nf) + val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts, res.state)).flatMap { + case (_, reses) => + val unjoined = reses.map(res => (Seq(res), res.pcs.branchConditions)) + val joined = abductionUtils.joinBcs(unjoined) + joined.map { + case (reses, pcs) => + reses.head -> pcs + } + } + abdCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) }) + } + def resolveFramingResults(m: Method, nf: NonFatalResult): Option[Method] = { + val frames = abductionUtils.getFramingSuccesses(nf) + val frameCases = frames.groupBy(f => (f.posts, f.stmts)).flatMap { + case (_, frs) => + val unjoined = frs.map(fr => (Seq(fr), fr.pcs.branchConditions)) + val joined = abductionUtils.joinBcs(unjoined) + joined.map { + case (frs, pcs) => + frs.head -> pcs + } + } + frameCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) }) + } + + def resolveLoopInvResults(m: Method, nf: NonFatalResult): Option[Method] = { + val invs = abductionUtils.getInvariantSuccesses(nf) + val invCases = invs.groupBy(inv => (inv.loop, inv.invs)).flatMap { + case (_, invs) => + val unjoined = invs.map(inv => (Seq(inv), inv.pcs.branchConditions)) + val joined = abductionUtils.joinBcs(unjoined) + joined.map { + case (invs, pcs) => + invs.head -> pcs + } + } + invCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) }) + } + /*/val tra = VarTransformer(s, v, targetVars, s.h) val res = s.h.values.collect { case c: NonQuantifiedChunk => tra.transformChunk(c) }.collect { case Some(e) => e }.toSeq val bcs = v.decider.pcs.branchConditions @@ -342,8 +410,8 @@ object BiAbductionSolver { } } FramingSuccess(s, v, posts = posts, loc) -} -}*/ + } + }*/ } object abductionUtils { @@ -421,4 +489,23 @@ object abductionUtils { }.get } + def joinBcs[T](bcs: Seq[(Seq[T], Seq[Term])]): Seq[(Seq[T], Seq[Term])] = { + bcs.combinations(2).collectFirst { + case Seq((a_res, a_pcs), (b_res, b_pcs)) if canJoin(a_pcs, b_pcs).isDefined => + val rest = bcs.filter { case (c_res, _) => c_res != a_res && c_res != b_res } + val joined = canJoin(a_pcs, b_pcs).get + joinBcs(rest :+ (a_res ++ b_res, joined)) + } match { + case Some(joined) => joined + case None => bcs + } + } + + private def canJoin(a: Seq[Term], b: Seq[Term]): Option[Seq[Term]] = { + (a.diff(b), b.diff(a)) match { + case (Seq(eq: terms.BuiltinEquals), Seq(terms.Not(t))) if eq == t => Some(a.filter(_ != eq)) + case (Seq(terms.Not(t)), Seq(eq: terms.BuiltinEquals)) if eq == t => Some(b.filter(_ != eq)) + case _ => None + } + } } diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index 85752f52..27ce6042 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -49,6 +49,7 @@ object LoopInvariantSolver { abdRes match { case f: Failure => f case abdRes: NonFatalResult => + // TODO nklose we do not guarantee length 1 here anymore val abd = abductionUtils.getAbductionSuccesses(abdRes).head val unfolds = abd.stmts.collect { case Unfold(pa) => (pa.toString -> pa.loc.predicateBody(s.program, Set()).get) }.toMap val unfolded = inverted.map { @@ -94,22 +95,24 @@ object LoopInvariantSolver { loopHead: LoopHeadBlock[Stmt, Exp], loopEdges: Seq[Edge[Stmt, Exp]], joinPoint: Option[SilverBlock], + initialBcs: Seq[Term], q: InvariantAbductionQuestion = InvariantAbductionQuestion(Heap(), Seq(), Seq()), loopConBcs: Seq[Term] = Seq(), iteration: Int = 1): VerificationResult = { + // Produce the already known invariants. They are consumed at the end of the loop body, so we need to do this every iteration produces(s, freshSnap, loopHead.invs, ContractNotWellformed, v) { (sPreInv, vPreInv) => - var loopCondTerm: Option[Term] = None - val oldPcs = vPreInv.decider.pcs.branchConditions + //var loopCondTerm: Option[Term] = None + //val oldPcs = vPreInv.decider.pcs.branchConditions // Run the loop the first time to check whether we abduce any new state 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) { (_, v) => - loopCondTerm = Some(v.decider.pcs.branchConditions.diff(oldPcs).head) + executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint) { (_, _) => + //loopCondTerm = Some(v.decider.pcs.branchConditions.diff(oldPcs).head) Success() } } match { @@ -128,7 +131,7 @@ object LoopInvariantSolver { val abdReses = abductionUtils.getAbductionSuccesses(nonf) val preStateVars = sPreInv.g.values.filter { case (v, _) => origVars.contains(v) } - val newStateOpt = abdReses.collect { case abd => abd.toPrecondition(preStateVars, sPreInv.h, loopConBcs).get }.flatten + val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preStateVars, sPreInv.h, Seq()).get } //val newStateHeadOpt = abdReses.collect { case abd if abd.trigger.contains(loopConExp) => abd.toPrecondition(preStateVars, sPreInv.h) } //if (newStateOpt.contains(None)) { @@ -160,35 +163,18 @@ object LoopInvariantSolver { val newPreState0 = sPreAbd.copy(h = q.preHeap.+(Heap(allChunks))) BiAbductionSolver.solveAbstraction(newPreState0, vPreAbd) { (newPreState, newPreAbstraction0, newPreV) => - //val preState = sPreAbd.copy(h = q.preHeap.+(Heap(allChunks))) - //val tra = VarTransformer(preState, vPreAbd, preStateVars, preState.h) - //BiAbductionSolver.solveFraming(preState, vPreAbd, pveLam, tra, loopConExp, Seq()) { frame => - - //val newPreState = frame.s - //val newPreV = frame.v - //val newPreAbstraction = frame.posts val preTran = VarTransformer(newPreState, newPreV, preStateVars, newPreState.h) val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, strict = false).get) - - //executionFlowController.locally(sPreAbd, vPreAbd) { (sPreAbst2, vPreAbst2) => + executor.follows(sPreAbd, loopEdges, pveLam, vPreAbd, joinPoint)((sPost, vPost) => { - //val postStateVars = sPost.g.values.filter { case (v, _) => origVars.contains(v) } - //val postTran = VarTransformer(sPost, vPost, postStateVars, sPost.h) - //BiAbductionSolver.solveFraming(sPost, vPost, pveLam, postTran, loopConExp, Seq()) { frame => - //val postAbstraction = frame.posts - //val sPostAbs = frame.s - //val vPostAbs = frame.v - 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, strict = false).get) - - - + // If the pushed forward abstraction is the same as the previous one, we are done if (newPreAbstraction == q.preAbstraction && postAbstraction == q.postAbstraction) { getPreInvariant(newPreAbstraction, postAbstraction, loopConExp, sPostAbs, vPostAbs) { preInv => @@ -196,13 +182,13 @@ object LoopInvariantSolver { case Seq() => Success() case res => val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method]) - Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = res, loop))) + Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = res, loop, vPostAbs.decider.pcs.duplicate()))) } } } else { val newLoopCons = loopConBcs :+ loopCondTerm // Else continue with next iteration, using the state from the end of the loop - solveLoopInvariants(sPostAbs, vPostAbs, origVars, loopHead, loopEdges, joinPoint, q.copy(preHeap = newPreState.h, preAbstraction = newPreAbstraction, + solveLoopInvariants(sPostAbs, vPostAbs, origVars, loopHead, loopEdges, joinPoint, initialBcs, q.copy(preHeap = newPreState.h, preAbstraction = newPreAbstraction, postAbstraction = postAbstraction), newLoopCons, iteration = iteration + 1) } } diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 6edaf27f..9fd1b635 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -271,7 +271,7 @@ object executor extends ExecutionRules { val sBody = s.copy(g = gBody, h = Heap()) val invReses = executionFlowController.locally(s, v) ((sAbd, vAbd) => - LoopInvariantSolver.solveLoopInvariants(sAbd, vAbd, sAbd.g.values.keys.toSeq, block, otherEdges, joinPoint) + LoopInvariantSolver.solveLoopInvariants(sAbd, vAbd, sAbd.g.values.keys.toSeq, block, otherEdges, joinPoint, vAbd.decider.pcs.branchConditions) ) invReses match { @@ -281,7 +281,7 @@ object executor extends ExecutionRules { case nfr: NonFatalResult => { val (foundInvs, invSuc) = abductionUtils.getInvariantSuccesses(nfr) match { - case Seq(invSuc) => (invSuc.invs.distinct, Success(Some(LoopInvariantSuccess(s, v, invSuc.invs.distinct, invSuc.loop)))) + case Seq(invSuc) => (invSuc.invs.distinct, Success(Some(LoopInvariantSuccess(s, v, invSuc.invs.distinct, invSuc.loop, v.decider.pcs.duplicate())))) case Seq() => (Seq(), Success()) } val invs = existingInvs ++ foundInvs diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index b25b9fc2..576257b7 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -7,7 +7,7 @@ package viper.silicon.supporters import com.typesafe.scalalogging.Logger -import viper.silicon.biabduction.BiAbductionSolver.solveFraming +import viper.silicon.biabduction.BiAbductionSolver.{resolveAbductionResults, resolveFramingResults, resolveLoopInvResults, solveFraming} import viper.silicon.biabduction.{VarTransformer, abductionUtils} import viper.silicon.decider.Decider import viper.silicon.interfaces._ @@ -120,12 +120,12 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { }) val ex = executionFlowController.locally(s2a, v2)((s3, v3) => { exec(s3, body, v3) { (s4, v4) => { - val postViolated = (offendingNode: ast.Exp) => PostconditionViolated(offendingNode, method) val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar) val vars = s4.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) } val tra = VarTransformer(s4, v4, vars, s4.h) solveFraming(s4, v4, postViolated, tra, abductionUtils.dummyEndStmt, posts) { - frame => Success(Some(frame)) + frame => Success(Some(frame.copy(s = s4, v = v4)) + ) } } } @@ -137,40 +137,16 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { val abdResult: VerificationResult = result match { case suc: NonFatalResult if method.body.isDefined => val abdFails = abductionUtils.getAbductionFailures(suc) - val mFail = abdFails.foldLeft(method){case (m1, fail) => fail.addToMethod(m1)} - - val abdReses = abductionUtils.getAbductionSuccesses(suc) - // TODO we are generating duplicate statements - // Maybe try to generate bcs and if that fails then merge? - val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts)) - abdReses.foldLeft[Option[Method]](Some(mFail))((m1, res) => m1.flatMap{mm => res.addToMethod(mm)}) - // Collect all the abductions and try to generate preconditions - match { - case None => Failure(Internal(reason = InternalReason(DummyNode, "Failed to generate preconditions from abduction results"))) + + val mFail = abdFails.foldLeft(method) { case (m1, fail) => fail.addToMethod(m1) } + val mAbd = resolveAbductionResults(mFail, suc) + val mInv = mAbd.flatMap(m2 => resolveLoopInvResults(m2, suc)) + val mFrame = mInv.flatMap(someM => resolveFramingResults(someM, suc)) + + mFrame match { + case None => Failure(Internal(reason = InternalReason(DummyNode, "Resolving Biabduction results failed"))) case Some(m) => - val invReses = abductionUtils.getInvariantSuccesses(suc) - val mInv = invReses.foldLeft[Method](m)((m1, res) => res.addToMethod(m1)) - - val frames = abductionUtils.getFramingSuccesses(suc) - //val frameBcs = frames.map{frame => frame.pcs.branchConditions} - - // We can remove bcs that are present in all frames - //val toRemove = frameBcs.reduceLeft(_ intersect _) - - //val toKeep = frames.zip(frameBcs.map{frame => frame.diff(toRemove)}).toMap - - val frameCases = frames.groupBy(f => (f.posts, f.stmts)) - - val mPosts = frameCases.values.toSeq match { - case Seq(singleCase) => { - singleCase.head.addToMethod(mInv) - } - } - - //val mPosts = frames.foldLeft(mInv){case (m1, frame) => frame.addToMethod(m1)} - - //val abducedMethod = mPosts.copy(pres = mPosts.pres.distinct, posts = mPosts.posts.distinct)(mPosts.pos, mPosts.info, mPosts.errT) - println("Original method: \n" + method.toString + "\nAbduced method: \n" + mPosts.toString) + println("Original method: \n" + method.toString + "\nAbduced method: \n" + m.toString) result } case _ => result @@ -192,6 +168,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { def stop(): Unit = {} } } + /* private def handlePostConditions(s: State, method: ast.Method, posts: Seq[ast.Exp], v: Verifier): VerificationResult = { val postViolated = (offendingNode: ast.Exp) => PostconditionViolated(offendingNode, method) diff --git a/src/test/resources/biabduction/nlist/branching.vpr b/src/test/resources/biabduction/nlist/branching.vpr index 7a7a8b72..807150f0 100644 --- a/src/test/resources/biabduction/nlist/branching.vpr +++ b/src/test/resources/biabduction/nlist/branching.vpr @@ -14,6 +14,3 @@ method test(x: Ref, cond: Bool) reverse(x.next) } } - - - diff --git a/src/test/resources/biabduction/nnlist/loop.vpr b/src/test/resources/biabduction/nnlist/loop.vpr index c0ea150b..4367585f 100644 --- a/src/test/resources/biabduction/nnlist/loop.vpr +++ b/src/test/resources/biabduction/nnlist/loop.vpr @@ -25,7 +25,7 @@ method loop(this: Ref) //package list(x) --* list(this){ // fold list(x_old) // apply list(x_old) --* list(this) - // } + //} } // fold list(x) // apply list(x) --* list(this)