Skip to content

Commit

Permalink
Worked on branching stuff a bunch
Browse files Browse the repository at this point in the history
  • Loading branch information
@rayman2000
rayman2000 committed Nov 15, 2024
1 parent ef5c200 commit afaae51
Show file tree
Hide file tree
Showing 36 changed files with 1,023 additions and 467 deletions.
163 changes: 32 additions & 131 deletions src/main/scala/biabduction/Abduction.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package viper.silicon.biabduction


import viper.silicon
import viper.silicon.interfaces._
import viper.silicon.resources.{FieldID, PredicateID}
Expand All @@ -12,6 +11,7 @@ import viper.silicon.state._
import viper.silicon.state.terms.{SortWrapper, Term, sorts}
import viper.silicon.utils.freshSnap
import viper.silicon.verifier.Verifier
import viper.silver.ast
import viper.silver.ast._
import viper.silver.verifier.{BiAbductionQuestion, DummyReason}

Expand All @@ -22,7 +22,7 @@ object AbductionApplier extends RuleApplier[AbductionQuestion] {

case class AbductionQuestion(s: State, v: Verifier, goal: Seq[Exp],
lostAccesses: Map[Exp, Term] = Map(), foundState: Seq[Exp] = Seq(),
foundStmts: Seq[Stmt] = Seq()) extends BiAbductionQuestion
foundStmts: Seq[Stmt] = Seq(), trigger: Option[Positioned]) extends BiAbductionQuestion

/**
* A rule for abduction. A rule is a pair of a check method and an apply method. The check method checks whether the
Expand Down Expand Up @@ -159,6 +159,7 @@ object AbductionFoldBase extends AbductionRule {
safeEval(a.loc.args.head, q.s, q.v, q.lostAccesses) {
case (s2, Some(t), v2) =>
val wildcards = s2.constrainableARPs -- s1.constrainableARPs
// TODO nklose this could branch
predicateSupporter.fold(s1, pred, List(t), None, terms.FullPerm, None, wildcards, pve, v2) { (s3, v3) =>
val fold = Fold(a)()
Q(Some(q.copy(goal = g1, foundStmts = q.foundStmts :+ fold, s = s3, v = v3)))
Expand Down Expand Up @@ -212,16 +213,31 @@ object AbductionFold extends AbductionRule {
// TODO nklose if the predicate is conditional in a weird way, then this might be wrong?
case Some((field, chunk)) =>
val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs
executionFlowController.tryOrElse0(q.s, q.v) {
(sa, va, T) => predicateSupporter.fold(sa, pred, chunk.args.toList, None, terms.FullPerm, None, wildcards, pve, va)(T)
} {
(s1: State, v1: Verifier) =>
val fold = Fold(a)()
val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, sorts.Ref))
val q2 = q.copy(s = s1, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1)
Q(Some(q2))
} { f =>
BiAbductionSolver.solveAbduction(q.s, q.v, f)((s3, v3) => {apply(q.copy(s = s3, v = v3))(Q)})}
val fargs = pred.formalArgs.map(_.localVar)
val eArgs = a.loc.args
val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map)
val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals)
val pveTransformed = pve.withReasonNodeTransformed(reasonTransformer)

val tryFold = predicateSupporter.fold(q.s, pred, chunk.args.toList, None, terms.FullPerm, None, wildcards, pveTransformed, q.v) {
(s1, v1) =>
Success(Some(AbductionSuccess(s1, v1, Seq(v1.decider.pcs.duplicate()), Seq(), Seq(Fold(a)()))))
}
tryFold match {
case nf: NonFatalResult =>
// TODO nklose make sure the pcs are correct here
abductionUtils.getAbductionSuccesses(nf) match {
case Seq(suc) =>
val fold = Fold(a)()
val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, sorts.Ref))
val q2 = q.copy(s = suc.s, v = suc.v, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1)
Q(Some(q2))
}
case f: Failure =>
BiAbductionSolver.solveAbduction(q.s, q.v, f, q.trigger){(s3, res, v3) =>
apply(q.copy(s = s3, v = v3, foundState = res.state ++ q.foundState, foundStmts = res.stmts ++ q.foundStmts))(Q)}
}

case None => {
// If we do not find a chunk, we recurse to try the others by calling this
apply(q.copy(goal = g1)) {
Expand Down Expand Up @@ -361,17 +377,16 @@ object AbductionPackage extends AbductionRule {

val packQ = q.copy(s = s1, v = v1, goal = Seq(wand.right))
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")
}
Q(None)
} else {

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)))
}
}}
})
}
}
Expand All @@ -393,117 +408,3 @@ object AbductionMissing extends AbductionRule {
}
}
}

/*
/**
* Covers the rule fold-base, which removes a predicate instance from the goal if its base case is met
*/
object AbductionListFoldBase extends AbductionRule {
override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = {
val preds = q.goal.collectFirst { case e: PredicateAccessPredicate => e }
preds match {
case None => Q(None)
case Some(a: PredicateAccessPredicate) =>
val g1 = q.goal.filterNot(_ == a)
safeArgEval(a.loc, q) {
case (s1, Some(args), v1) =>
if (v1.decider.check(terms.BuiltinEquals(args.head, terms.Null), Verifier.config.checkTimeout())) {
val fold = Fold(a)()
// Do we have to remove the path condition? How do we do this? Havoc/exhale?
Q(Some(q.copy(goal = g1, foundStmts = q.foundStmts :+ fold)))
} else {
apply(q.copy(goal = g1)) {
case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal)))
case None => Q(None)
}
}
case (_, None, _) => apply(q.copy(goal = g1)) {
case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal)))
case None => Q(None)
}
}
}
}
}
// this does not always do the right thing, see the reassign example
// If we add list(x.next) to our goal, but x.next was assigned to in the method, then we
// find a precondition for the original value of x.next, not for the assigned value.
// We need to add the "old" chunks to the var matching?
// Or do var matching in the context of the current state vs the old state? If so then maybe we do want goals/results as chunks?
object AbductionListFold extends AbductionRule {
override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = {
val preds = q.goal.collectFirst { case e: PredicateAccessPredicate => e }
preds match {
case None => Q(None)
case Some(a: PredicateAccessPredicate) =>
val g1 = q.goal.filterNot(_ == a)
val next = abductionUtils.getNextAccess(q.s.program, a.loc.args.head, a.perm)
checkChunk(next.loc, q) {
case Some(_) =>
val headNext = abductionUtils.getNextAccess(q.s.program, a.loc.args.head, a.perm)
val nextList = abductionUtils.getPredicate(q.s.program, headNext.loc, a.perm)
val g1: Seq[Exp] = q.goal.filterNot(_ == a) :+ nextList
val fold = Fold(a)()
consumer.consume(q.s, headNext, pve, q.v) { (s1, snap, v1) =>
val lost = q.lostAccesses + (headNext.loc -> SortWrapper(snap, sorts.Ref))
Q(Some(q.copy(s = s1, v = v1, goal = g1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost)))
}
case None => apply(q.copy(goal = g1)) {
case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal)))
case None => Q(None)
}
}
}
}
}
object AbductionListUnfold extends AbductionRule {
override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = {
val acc = q.goal.collectFirst { case e: FieldAccessPredicate => e }
acc match {
case None => Q(None)
case Some(a: FieldAccessPredicate) =>
val g1 = q.goal.filterNot(a == _)
val pred = abductionUtils.getPredicate(q.s.program, a.loc.rcv, a.perm)
checkChunk(pred.loc, q) {
case Some(_) =>
val unfold = Unfold(abductionUtils.getPredicate(q.s.program, a.loc.rcv, a.perm))()
val nNl = NeCmp(a.loc.rcv, NullLit()())()
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.foundState else q.foundState :+ nNl
// Exchange list(x) with list(x.next) in the state
// Unfold
unfoldPredicate(q, a.loc.rcv, a.perm) { (s1, v1) =>
// Add x != null to path condition maybe do this first?
produce(s1, freshSnap, nNl, pve, v1)((s2, v2) => {
v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterInhale)
// Remove the access chunk
consumer.consume(s2, a, pve, v2)((s3, snap, v3) => {
val lost = q.lostAccesses + (a.loc -> SortWrapper(snap, sorts.Ref))
Q(Some(q.copy(s = s3, v = v3, goal = g1, foundState = r1, foundStmts = q.foundStmts :+ unfold, lostAccesses = lost)))
})
})
}
}
}
case None => apply(q.copy(goal = g1)) {
case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal)))
case None => Q(None)
}
}
}
}
}
*/
82 changes: 12 additions & 70 deletions src/main/scala/biabduction/Abstraction.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package viper.silicon.biabduction

import viper.silicon.interfaces.VerificationResult
import viper.silicon.interfaces.state.Chunk
import viper.silicon.resources._
import viper.silicon.rules._
import viper.silicon.state._
Expand All @@ -13,7 +14,7 @@ object AbstractionApplier extends RuleApplier[AbstractionQuestion] {
override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply)
}

case class AbstractionQuestion(s: State, v: Verifier) {
case class AbstractionQuestion(s: State, v: Verifier, fixedChunks: Seq[Chunk]) {

// 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
Expand All @@ -22,7 +23,7 @@ case class AbstractionQuestion(s: State, v: Verifier) {

def isTriggerField(bc: BasicChunk): Boolean = {
bc.resourceID match {
case FieldID => fields.contains(abductionUtils.getField(bc.id, s.program))
case FieldID => fields.contains(abductionUtils.getField(bc.id, s.program)) && !fixedChunks.contains(bc)
case _ => false
}
}
Expand All @@ -40,6 +41,7 @@ object AbstractionFold extends AbstractionRule {
val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs
executionFlowController.tryOrElse0(q.s, q.v) {
(s1, v1, T) =>
// TODO nklose this can branch
predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pve, v1)(T)
} { (s2, v2) => Q(Some(q.copy(s = s2, v = v2))) } {
_ => checkChunks(rest, q)(Q)
Expand All @@ -57,30 +59,31 @@ object AbstractionFold extends AbstractionRule {
object AbstractionPackage extends AbstractionRule {

@tailrec
private def findWandFieldChunk(chunks: Seq[BasicChunk], q: AbstractionQuestion): Option[(Exp, BasicChunk)] = {
private def findWandFieldChunk(chunks: Seq[Chunk], q: AbstractionQuestion): Option[(Exp, BasicChunk)] = {
chunks match {
case Seq() => None
case chunk +: rest =>
case (chunk: BasicChunk) +: rest if q.isTriggerField(chunk) =>
q.varTran.transformTerm(chunk.snap) match {
case None => findWandFieldChunk(rest, q)
case Some(snap) => Some((snap, chunk))
}
case _ +: rest => findWandFieldChunk(rest, q)
}
}

override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {

val candChunks = q.s.h.values.collect { case bc: BasicChunk if q.isTriggerField(bc) => bc }.toSeq

findWandFieldChunk(candChunks, q) match {
findWandFieldChunk(q.s.h.values.toSeq, q) match {
case None => Q(None)
case Some((lhsArg, chunk)) =>
val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program))
val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
val rhsArg = q.varTran.transformTerm(chunk.args.head).get
val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())()
val wand = MagicWand(lhs, rhs)()
executor.exec(q.s, Assert(wand)(), q.v) { (s1, sv) => Q(Some(q.copy(s = s1, v = sv)))}
executor.exec(q.s, Assert(wand)(), q.v) {
(s1, sv) =>
Q(Some(q.copy(s = s1, v = sv)))}
}
}
}
Expand All @@ -107,7 +110,7 @@ object AbstractionApply 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) }.collect {case Some(wand: MagicWand) => wand}
val targets = q.s.h.values.collect { case c: BasicChunk => q.varTran.transformChunk(c) }.collect {case Some(exp) => exp}.toSeq
val targets = q.s.h.values.collect { case c: BasicChunk if !q.fixedChunks.contains(c) => q.varTran.transformChunk(c) }.collect {case Some(exp) => exp}.toSeq

wands.collectFirst{case wand if targets.contains(wand.left) => wand } match {
case None => Q(None)
Expand All @@ -118,64 +121,3 @@ object AbstractionApply extends AbstractionRule {
}
}
}

/*
object AbstractionListFold extends AbstractionRule {
override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
val lists = q.exps.collect({ case pa: PredicateAccessPredicate => pa.loc.args.head -> pa }).toMap
q.exps.collectFirst { case acc: FieldAccessPredicate => acc } match {
case None => Q(None)
case Some(acc) if (lists.contains(acc.loc)) =>
val exps1 = q.exps.filterNot(exp => exp == acc || exp == lists(acc.loc)) :+ abductionUtils.getPredicate(q.s.program, acc.loc.rcv)
Q(Some(q.copy(exps = exps1)))
case Some(acc) =>
val check = EqCmp(acc.loc, NullLit()())()
evaluator.eval(q.s, check, pve, q.v) { (_, b, _) =>
b match {
case True =>
val exps1 = q.exps.filterNot(_ == acc) :+ abductionUtils.getPredicate(q.s.program, acc.loc.rcv)
Q(Some(q.copy(exps = exps1)))
case _ => apply(q.copy(exps = q.exps.filterNot(_ == acc))) {
case Some(q1) => Q(Some(q1.copy(exps = q1.exps :+ acc)))
case None => Q(None)
}
}
}
}
}
}
// This should trigger on:
// - Two connected nexts
// - A wand and a next on the rhs of the wand
// - A wand and a next on the lhs of the wand
object AbstractionListPackage extends AbstractionRule {
override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = {
// TODO there must be a better way to do this
// TODO There also may be a level of .nexts that we can remove in the wand case
q.exps.combinations(2).collectFirst {
case Seq(first: FieldAccessPredicate, second@FieldAccessPredicate(FieldAccess(next: FieldAccess, _), _))
if next == first.loc => Seq(MagicWand(abductionUtils.getPredicate(q.s.program, second.loc), abductionUtils.getPredicate(q.s.program, first.loc.rcv))(), first, second)
case Seq(second@FieldAccessPredicate(FieldAccess(next: FieldAccess, _), _), first: FieldAccessPredicate)
if next == first.loc => Seq(MagicWand(abductionUtils.getPredicate(q.s.program, second.loc), abductionUtils.getPredicate(q.s.program, first.loc.rcv))(), first, second)
case Seq(wand@MagicWand(left: PredicateAccessPredicate, _: PredicateAccessPredicate), next: FieldAccessPredicate)
if left.loc.args.head == next.loc.rcv => Seq(MagicWand(abductionUtils.getPredicate(q.s.program, next.loc), wand.right)(), wand, next)
case Seq(next: FieldAccessPredicate, wand@MagicWand(left: PredicateAccessPredicate, _: PredicateAccessPredicate))
if left.loc.args.head == next.loc.rcv => Seq(MagicWand(abductionUtils.getPredicate(q.s.program, next.loc), wand.right)(), wand, next)
case Seq(wand@MagicWand(_: PredicateAccessPredicate, second: PredicateAccessPredicate), first: FieldAccessPredicate)
if second.loc.args.head == first.loc => Seq(MagicWand(wand.left, abductionUtils.getPredicate(q.s.program, first.loc.rcv))(), wand, first)
case Seq(first: FieldAccessPredicate, wand@MagicWand(_: PredicateAccessPredicate, second: PredicateAccessPredicate))
if second.loc.args.head == first.loc => Seq(MagicWand(wand.left, abductionUtils.getPredicate(q.s.program, first.loc.rcv))(), wand, first)
} match {
case None => Q(None)
case Some((wand: MagicWand) :: gs) =>
val exp1: Seq[Exp] = q.exps.filterNot(gs.contains) :+ wand
Q(Some(q.copy(exps = exp1)))
}
}
}
*/
Loading

0 comments on commit afaae51

Please sign in to comment.