diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index 1bc7a42f..f0ebd9d9 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -22,7 +22,7 @@ object AbductionApplier extends RuleApplier[SiliconAbductionQuestion] { // TODO nklose: cant we just join the check and apply and return either None or Some(AbductionQuestion)? case class SiliconAbductionQuestion(s: State, v: Verifier, goal: Seq[Exp], - lostAccesses: Map[Exp, Term] = Map(), foundPrecons: Seq[Exp] = Seq(), + lostAccesses: Map[Exp, Term] = Map(), foundState: Seq[Exp] = Seq(), foundStmts: Seq[Stmt] = Seq()) extends BiAbductionQuestion /** @@ -226,7 +226,7 @@ object AbductionListUnfold extends AbductionRule[FieldAccessPredicate] { eval(q.s, nNl, pve, q.v) { case (s1, arg, v1) => { val isNl = q.v.decider.check(arg, Verifier.config.checkTimeout()) // Add x != null to result if it does not hold - val r1 = if (isNl) q.foundPrecons else q.foundPrecons :+ nNl + val r1 = if (isNl) q.foundState else q.foundState :+ nNl // Exchange list(x) with list(x.next) in the state // Unfold @@ -239,7 +239,7 @@ object AbductionListUnfold extends AbductionRule[FieldAccessPredicate] { // Remove the access chunk consumer.consume(s2, inst, pve, v2)((s3, snap, v3) => { val lost = q.lostAccesses + (inst.loc -> SortWrapper(snap, sorts.Ref)) - Q(q.copy(s = s3, v = v3, goal = g1, foundPrecons = r1, foundStmts = q.foundStmts :+ unfold, lostAccesses = lost)) + Q(q.copy(s = s3, v = v3, goal = g1, foundState = r1, foundStmts = q.foundStmts :+ unfold, lostAccesses = lost)) }) }) } @@ -323,7 +323,7 @@ object AbductionPackage extends AbductionRule[MagicWand] { val g1 = q.goal.filterNot(_ == inst) val stmts = q.foundStmts :+ Package(inst, Seqn(packRes.foundStmts.reverse, Seq())())() - val pres = q.foundPrecons ++ packRes.foundPrecons + val pres = q.foundState ++ packRes.foundState Q(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts)) }) } @@ -348,6 +348,8 @@ object AbductionMissing extends AbductionRule[Seq[AccessPredicate]] { override protected def apply(q: SiliconAbductionQuestion, inst: Seq[AccessPredicate])(Q: SiliconAbductionQuestion => VerificationResult): VerificationResult = { val g1 = q.goal.filterNot(inst.contains) - Q(q.copy(goal = g1, foundPrecons = q.foundPrecons ++ inst)) + Q(q.copy(goal = g1, foundState = q.foundState ++ inst)) } + + override protected def instanceString(inst: Seq[AccessPredicate]): String = inst.mkString(" && ") } \ No newline at end of file diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index b9c8917e..811abf1a 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -1,22 +1,15 @@ package viper.silicon.biabduction +import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces.{Failure, VerificationResult} import viper.silicon.state._ import viper.silicon.state.terms.Term import viper.silicon.utils.ast.BigAnd import viper.silicon.verifier.Verifier -import viper.silver.ast import viper.silver.ast._ import viper.silver.verifier.errors.Internal import viper.silver.verifier.{AbductionQuestionTransformer, DummyReason, PartialVerificationError, VerificationError} -// TODO we want to continue execution if we abduce successfully. Idea: -// - Hook into the "Try or Fail" methods -// - Instead of actually failing, do bi-abduction -// - track the results somewhere -// - produce the precondition, execute the statements, and continue execution -// - At the end, do abstraction on all the found preconditions. Find the necessary statements for the abstractions - trait BiAbductionResult { def s: State @@ -25,14 +18,43 @@ trait BiAbductionResult { trait BiAbductionSuccess extends BiAbductionResult -case class AbductionSuccess(s: State, v: Verifier, pre: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), loc: Position) extends BiAbductionSuccess { +case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), loc: Position) extends BiAbductionSuccess { + + val line = loc match { + case sp: SourcePosition => sp.start.line.toString + case lc: HasLineColumn => lc.line.toString + case _ => "No Position" + } + override def toString: String = { + "Successful abduction at line " + line + ":\n" + "Abduced state\n" + state.map(_.toString()).mkString("\n") + "\nAbduced statements\n" + stmts.reverse.map(_.toString()).mkString("\n") + } + + def toPrecondition(preVars: Map[AbstractLocalVar, Term], preHeap: Heap): Option[Seq[Exp]] = { + + // We have to use the pcs from the abduction point + val prevPcs = v.decider.pcs + v.decider.setPcs(pcs) + val varTrans = VarTransformer(s, v, preVars, preHeap) + val presTransformed = state.map { varTrans.transformExp } - val line = loc match { - case sp: ast.SourcePosition => sp.start.line - case lc: ast.HasLineColumn => lc.line + if (presTransformed.contains(None)) { // We could not express the state as a precondition + None + } else { + // TODO There is a common case where we add x != null because we know acc(x.next). We want to remove this bc + // If performing the abduction somehow introduces branches, then this could cause problems here. + // TODO for loops, we would like to remove the loop condition from conditions we find. How do we do that? + val bcs = v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformExp(e).isDefined && e != TrueLit()() => varTrans.transformExp(e).get }.toSet + val presFinal = presTransformed.map { e => + if(bcs.isEmpty){ + e.get + } else { + Implies(BigAnd(bcs), e.get)() + } + } + v.decider.setPcs(prevPcs) + Some(presFinal) } - "Successful abduction at line " + line.toString + ":\n" + "Abduced preconditions\n" + pre.map(_.toString()).mkString("\n") + "\nAbduced statements\n" + stmts.reverse.map(_.toString()).mkString("\n") } } @@ -40,13 +62,12 @@ case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), s override def toString: String = "Successful loop invariant abduction" } -case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp]) extends BiAbductionSuccess +case class FramingSuccess(s: State, v: Verifier, pcs: PathConditionStack, posts: Seq[Exp]) extends BiAbductionSuccess case class BiAbductionFailure(s: State, v: Verifier) extends BiAbductionResult { override def toString: String = "Abduction failed" } - object BiAbductionSolver { def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): BiAbductionResult = { @@ -58,55 +79,24 @@ object BiAbductionSolver { case _ => qPre } - val ins = q.s.currentMember match { - case Some(m: Method) => m.formalArgs.map(_.localVar) - case _ => Seq() - } - - val varTrans = VarTransformer(q.s, q.v, q.s.g.values.collect { case (v: AbstractLocalVar, t: Term) if ins.contains(v) => (v, t)}, q.s.oldHeaps.head._2) - val q1 = AbductionApplier.apply(q) if (q1.goal.isEmpty) { - - // TODO it is possible that we want to transform variable in a non-strict way before abstraction - val pres = AbstractionApplier.apply(AbstractionQuestion(q1.foundPrecons, q1.s.program)).exps - - // TODO There is a common case where we add x != null because we know acc(x.next). We want to remove this bc - val bcs = q1.v.decider.pcs.branchConditionExps.collect { case Some(e) if varTrans.transformExp(e).isDefined && e != TrueLit()() => varTrans.transformExp(e).get }.toSet - - // TODO Weak transformation of statements to original variables (Viper encoding can introduce new variables) - val presTransformed = pres.map { varTrans.transformExp } - - if (presTransformed.contains(None)) { - BiAbductionFailure(q1.s, q1.v) - } else { - val presFinal = presTransformed.map { e => - if(bcs.isEmpty){ - e.get - } else { - Implies(BigAnd(bcs), e.get)() - } - } - AbductionSuccess(q1.s, q1.v, presFinal, q1.foundStmts, loc = loc) - } + // TODO if we abstract then the statements may become incorrect + //val state = AbstractionApplier.apply(AbstractionQuestion(q1.foundState, q1.s.program)).exps + AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc) } else { BiAbductionFailure(q1.s, q1.v) } } - def solveFraming(s: State, v: Verifier): FramingSuccess = { + def solveFraming(s: State, v: Verifier, postVars: Map[AbstractLocalVar, Term]): FramingSuccess = { - val formals = s.currentMember match { - case Some(m: Method) => m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar) - case _ => Seq() - } - val tra = VarTransformer(s, v, s.g.values.filter(formals.contains), s.h) + 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 absRes = AbstractionApplier.apply(AbstractionQuestion(res, s.program)).exps - FramingSuccess(s, v, posts = absRes) - //"Abduced postconditions\n" + absRes.map(_.toString()).mkString("\n") + FramingSuccess(s, v, v.decider.pcs.duplicate(), posts = absRes) } } @@ -141,12 +131,14 @@ trait BiAbductionRule[S, T] { def checkAndApply(q: S, rule: Int)(Q: (S, Int) => VerificationResult): VerificationResult = { check(q) { case Some(e) => - println("Applied rule " + this.getClass.getSimpleName) + println("Applied rule " + this.getClass.getSimpleName + " on " + this.instanceString(e)) apply(q, e)(Q(_, 0)) case None => Q(q, rule + 1) } } + protected def instanceString(inst: T): String = inst.toString + protected def check(q: S)(Q: Option[T] => VerificationResult): VerificationResult protected def apply(q: S, inst: T)(Q: S => VerificationResult): VerificationResult diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index ac245db8..909a5acf 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -42,7 +42,7 @@ object LoopInvariantSolver { q: InvariantAbductionQuestion = InvariantAbductionQuestion(Seq(), Map())) (Q: BiAbductionResult => VerificationResult): VerificationResult = { - // Assumme that we have the previous abstraction + // Assume that we have the previous abstraction //producer.produces(s, freshSnap, q.abstraction, pveLam, v) { (s2, v2) => @@ -67,22 +67,24 @@ object LoopInvariantSolver { case nonf: NonFatalResult => val abdReses = (nonf +: nonf.previous).collect { case Success(Some(abd: AbductionSuccess)) => abd } - val newState = abdReses.flatMap(_.pre) + val newStateOpt = abdReses.map { abd => abd.toPrecondition(sPre.g.values, sPre.h)} + if(newStateOpt.contains(None)){ + return Q(BiAbductionFailure(sPre, vPre)) + } + val newState = newStateOpt.flatMap(_.get) // Get the state at the beginning of the loop with with the abduced things added - producer.produces(sPre, freshSnap, abdReses.flatMap(_.pre), pveLam, vPre) { (sPreAbd, vPreAbd) => - - // TODO this is not the way to find the vars, it should be the vars not assigned to in the loop - // TODO nklose this is nonsense now. Think about what should really happen here! - val relVarTrans = VarTransformer(sPreAbd, vPreAbd, sPre.g.values, sPre.h, strict = false) + producer.produces(sPre, freshSnap, abdReses.flatMap(_.state), pveLam, vPre) { (sPreAbd, vPreAbd) => // The framing result contains the state at the end of the loop // TODO we should also track the framed stuff to generate invariants for loops with changing heaps + // TODO branching will lead to multiple of these occuring val framingRes = (nonf +: nonf.previous).collect { case Success(Some(framing: FramingSuccess)) => framing } match { case Seq(res) => res } - // Values of the variables in terms of the beginning of the loop + // Values of the variables at the end of loop in terms of the beginning of the loop + val relVarTrans = VarTransformer(sPre, vPre, sPre.g.values, sPre.h, strict = false) val relValues = framingRes.s.g.values.collect { case (v, t) => (v, relVarTrans.transformTerm(t)) } .collect { case (v, e) if e.isDefined && e.get != v => (v, e.get) } @@ -90,17 +92,17 @@ object LoopInvariantSolver { // The absolute values at the end of the loop, by combining the values before the iteration with the absolute // values from the last iteration - val newAbsValues: Map[AbstractLocalVar, Exp] = relValues.collect { case (v: AbstractLocalVar, e: Exp) => (v, e.transform { + val newAbsValues: Map[AbstractLocalVar, Exp] = relValues.collect { case (v, e) => (v, e.transform { case lv: LocalVar if q.absValues.contains(lv) => q.absValues(lv) }) }.collect { case (v, e) => (v, absVarTran.transformExp(e).get) } // Perform abstraction on the found state for that loop iteration + // TODO nklose this is not working? // TODO there is an assumption here that the re-assignment happens at the end of the loop val newAbsState = newState.map(e => e.transform { case lv: LocalVar if q.absValues.contains(lv) => q.absValues(lv) }).map(absVarTran.transformExp(_).get) - val newAbstraction = AbstractionApplier.apply(AbstractionQuestion(q.abstraction ++ newAbsState, sPre.program)).exps // The re-assignments of this iteration in terms of the absolute values diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index e771ae79..b051d35a 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -1,11 +1,10 @@ package viper.silicon.biabduction -import viper.silicon.interfaces.{Failure, Success} +import viper.silicon.interfaces.state.NonQuantifiedChunk import viper.silicon.resources.{FieldID, PredicateID} -import viper.silicon.rules.{chunkSupporter, evaluator} import viper.silicon.rules.chunkSupporter.findChunk -import viper.silicon.state.terms.{BuiltinEquals, Term, Var, sorts} -import viper.silicon.state.{BasicChunk, ChunkIdentifier, Heap, State, terms} +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 @@ -17,44 +16,31 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa // 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 - val directTargets = targetVars.map(_.swap) - val pointsTargets = targetHeap.values.collect { + private val directTargets = targetVars.map(_.swap) + private val pointsTargets = targetHeap.values.collect { case c: BasicChunk if c.resourceID == FieldID && directTargets.contains(c.args.head) => c.snap -> FieldAccess(directTargets(c.args.head), abductionUtils.getField(c.id, s.program))() }.toMap val targets: Map[Term, Exp] = directTargets ++ pointsTargets - // Current chunks as a map - //val points: Map[Term, Term] = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => c.args.head -> c.snap }.toMap - // All other terms that might be interesting. Currently everything in the store and everything in field chunks - val currentTerms: Seq[Term] = (s.g.values.values ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) }.flatten).toSeq //.collect { case t: Var => t } + private val currentTerms: Seq[Term] = (s.g.values.values ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) }.flatten).toSeq.distinct //.collect { case t: Var => t } // Ask the decider whether any of the terms are equal to a target. + // TODO the decider is an object which changes. So the path conditions go away. We need to do this earlier val matches: Map[Term, Exp] = currentTerms.map { t => t -> targets.collectFirst { case (t1, e) if t.sort == t1.sort && v.decider.check(BuiltinEquals(t, t1), Verifier.config.checkTimeout()) => e } }.collect { case (t2, Some(e)) => t2 -> e }.toMap - // Field Chunks where the snap is equal to a known alias. This is only relevant for expression, not for chunks I think. - //val snaps: Seq[BasicChunk] = s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID && aliases.contains(c.snap) => c }.toSeq - def transformTerm(t: Term): Option[Exp] = { t match { case terms.FullPerm => Some(FullPerm()()) case _ => matches.get(t) - /*/ Check for direct aliases - val direct = matches.get(t) - if (direct.isDefined) { - direct - } else { - // Check for field accesses pointing to the term - points.collectFirst { case (f, v) if v == t && matches.contains(f) => FieldAccess(matches(f), s.program.fields.head)() } - }*/ } } - def onlyTargets(e: Exp): Boolean = { + private def onlyTargets(e: Exp): Boolean = { val vars = e.collect { case lv: LocalVar => lv }.toSeq vars.forall(targetVars.contains(_)) } @@ -71,33 +57,23 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa def transformExp(e: Exp): Option[Exp] = { + // TODO we need to be stricter here. If we can't find a match for a exp which uses + // input vars, then we need to fail (see hidden.vpr) val transformed = e.transform { - case fa: FieldAccess => - var t: Term = terms.Unit - // TODO if we ever call this on state that has been abduced, we might need to access the "lost chunks" here - val res = evaluator.eval(s, fa, pve, v)((_, t2, _) => { - t = t2 - Success() - }) - res match { - case _: Success => transformTerm(t).getOrElse(fa) - case _ => fa + case fa@FieldAccess(lv: LocalVar, _) => + val args = List(s.g.get(lv).get) + val resource = fa.res(s.program) + val id = ChunkIdentifier(resource, s.program) + findChunk[NonQuantifiedChunk](s.h.values, id, args, v) match { + case Some(c) => + transformTerm(c.snap).getOrElse(fa) + case None => fa } + case fa@FieldAccess(rec, _) => + val rcv = transformExp(rec).getOrElse(rec) + FieldAccess(rcv, fa.field)() case lv: LocalVar => transformTerm(s.g(lv)).getOrElse(lv) } - - //val varMap = e.collect { case lc: LocalVar => lc -> transformTerm(s.g(lc)) }.collect { case (k, Some(v)) => k -> v }.toMap - - //val onlyVars = e.transform { - // case lc: LocalVar if !targets.contains(lc) => varMap.getOrElse(lc, lc) - //} - - //val accesses = onlyVars.transform { - // // TODO this will not catch z.next.next -> x - // case fa@FieldAccess(rcv: LocalVar, _) if !onlyTargets(fa) => - // snaps.collectFirst { case c: BasicChunk if c.args.head == s.g(rcv) => matches(c.snap) }.getOrElse(fa) - //} - if (strict && !onlyTargets(transformed)) { None } else { diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 8b7e546d..d17fd52d 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -16,6 +16,7 @@ import viper.silicon.state.terms._ import viper.silicon.state.terms.predef.`?r` import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier +import viper.silver.ast.Method import viper.silver.cfg.silver.SilverCfg import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge} import viper.silver.cfg.{ConditionalEdge, StatementBlock} @@ -329,8 +330,7 @@ object executor extends ExecutionRules { v.decider.prover.comment("Loop head block: Re-establish invariant") consumes(s, invs, e => LoopInvariantNotPreserved(e), v)((s1, _, v1) => { // TODO nklose we may want to limit what kind of posts we can generate here - // TODO loc is very questionable here - val posts = BiAbductionSolver.solveFraming(s1, v1) + val posts = BiAbductionSolver.solveFraming(s1, v1, s1.g.values) Success(Some(posts)) }) } @@ -722,24 +722,24 @@ object executor extends ExecutionRules { | _: ast.While => sys.error(s"Unexpected statement (${stmt.getClass.getName}): $stmt") } - + // TODO this is still wrong: if we are in a loop, then we do not want to go to precondition + // We should just consume locally and return the results in verification successes. + // Then we can collect everything in the methodsupporter to actually translate stuff. executed match { - case Failure(pc: PostconditionViolated, _) => executed // Postconditions are handled later, we do not want to restart for them + case Failure(_: PostconditionViolated, _) => executed // Postconditions are handled elsewhere, we do not want to restart for them case Failure(ve, _) => ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match { - case Some(as@AbductionSuccess(_, _, pre, stmts, _)) => + case Some(as: AbductionSuccess) => // TODO nklose this also breaks if we allow re-assigning to input fields, we consume in the current state // instead of the original state. - println(as.toString()) - println("Continuing verification with abduction results added") - producer.produces(s, freshSnap, pre, ContractNotWellformed, v) { (s1, v1) => - executor.execs(s1, stmts.reverse, v1) { (s2, v2) => - exec(s2, stmt, v2)((s3, v3) => Q(s3, v3) match { - case f: Failure => f - case s: NonFatalResult => s && Success(Some(as)) - }) + //println(as.toString()) + //println("Continuing execution with abduced state and statements added") + producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) => + executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) => + exec(s2, stmt, v2)((s3, v3) => Q(s3, v3) && Success(Some(as))) } } + case Some(_: BiAbductionFailure) => println("Abduction failed") executed diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 2bfb27b0..127d71c5 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -7,20 +7,24 @@ package viper.silicon.supporters import com.typesafe.scalalogging.Logger -import viper.silicon.biabduction.{AbductionSuccess, BiAbductionSolver} +import viper.silicon.biabduction.{AbductionSuccess, BiAbductionSolver, FramingSuccess} import viper.silicon.decider.Decider import viper.silicon.interfaces._ import viper.silicon.logger.records.data.WellformednessCheckRecord import viper.silicon.rules.{consumer, executionFlowController, executor, producer} import viper.silicon.state.State.OldHeaps +import viper.silicon.state.terms.Term import viper.silicon.state.{Heap, State, Store} import viper.silicon.utils.freshSnap import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.{Map, toMap} import viper.silver.ast +import viper.silver.ast.Method import viper.silver.components.StatefulComponent import viper.silver.reporter.AnnotationWarning +import viper.silver.verifier.DummyNode import viper.silver.verifier.errors._ +import viper.silver.verifier.reasons.InternalReason /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */ @@ -117,20 +121,61 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { && { executionFlowController.locally(s2a, v2)((s3, v3) => { exec(s3, body, v3) { (s4, v4) => - consumes(s4, posts, postViolated, v4)((s5, _, v5) => { - val newPosts = BiAbductionSolver.solveFraming(s5, v5) - println("New postconditions for method " + method.name + ":\n" + newPosts.posts.map(_.toString()).mkString("\n")) + // P finds postconditions from the state after consuming existing postconditions + val P = (s: State, _: Term, v: Verifier) => { + val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar) + val vars = s.g.values.collect { case (v, t) if formals.contains(v) => (v, t) } + val newPosts = BiAbductionSolver.solveFraming(s, v, vars) + //println("New postconditions for method " + method.name + ":\n" + newPosts.posts.map(_.toString()).mkString("\n")) Success(Some(newPosts)) - })}})})})}) - - val abdResult = result match { - case f: Failure => - f.message.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match { - case Some(as: AbductionSuccess) => - println("Successful abduction to fulfil postcondition:") - println(as.toString()) - Success(Some(as)) // This is little scary, just returning a success here claiming that we can fulfill the postcondition - case _ => result + } + // Attempt to consume postconditions + consumes(s4, posts, postViolated, v4)(P) match { + // We failed to consume all postconditions + case f@Failure(pcv: PostconditionViolated, _) => + pcv.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match { + // We managed to abduce preconditions so that the post conditions would be fulfilled. So we attempt + // to consume the postconditions and frame again + case Some(as: AbductionSuccess) => + //println("Successful abduction to fulfil postcondition:") + //println(as.toString()) + producer.produces(s4, freshSnap, as.state, ContractNotWellformed, v) { (s6, v6) => + executor.execs(s6, as.stmts.reverse, v6) { (s7, v7) => + consumes(s7, posts, postViolated, v7)(P) && Success(Some(as)) + } + } + // We failed to abduce so that we can fulfil the postconditions + case _ => f + } + // We successfully consumed all postconditions (and then did framing) + case otherRes => otherRes + } + } + }) + }) + }) + }) + + val abdResult: VerificationResult = result match { + case suc: NonFatalResult => + // Collect all the abductions and try to generate preconditions + val ins = method.formalArgs.map(_.localVar) + val inVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) } + val abds = (suc +: suc.previous).collect { case Success(Some(abd: AbductionSuccess)) => abd } + val pres = abds.map {abd => abd.toPrecondition(inVars, abd.s.oldHeaps.head._2)} + // If we fail to generate preconditions somewhere, then we actually fail + if(pres.contains(None)){ + Failure(Internal(reason = InternalReason(DummyNode, "Failed to generate preconditions from abduction results"))) + } else { + // Otherwise we succeed + println("Generated preconditions from abductions: " + pres.flatMap(_.get).mkString(" && ")) + println("Abduced the following statements:\n" + abds.flatMap {abd => abd.stmts.map {stmt => " Line " + abd.line + ": " + stmt.toString() }}.reverse.mkString("\n") ) + // TODO branching can lead to multiple framing results! We need to look at the branching conditions here as well + (suc +: suc.previous).collect { case Success(Some(framing: FramingSuccess)) => framing } match { + case Seq(frame) => println("Generated postconditions: " + frame.posts.mkString(" && ")) + case Seq() => println("No framing result found") + } + result } case _ => result }