Skip to content

Commit

Permalink
Branching is better now
Browse files Browse the repository at this point in the history
  • Loading branch information
@rayman2000
rayman2000 committed Jan 24, 2025
1 parent a1349fc commit e2eb54d
Show file tree
Hide file tree
Showing 16 changed files with 298 additions and 137 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/biabduction/Abduction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,7 @@ object AbductionUnfold extends AbductionRule {
case Seq() => checkPredicates(rest, q, goal)(Q)
case Seq(branch) =>
val condTerms = branch.distinct.filterNot(bcsBefore.contains)
val varTran = VarTransformer(s = q.s, v = q.v, targetVars = q.s.g.values, targetHeap = q.s.h)
val varTran = VarTransformer(q.s, q.v, q.s.g.values, q.s.h)
val conds = condTerms.map(varTran.transformTerm(_).get)
Q(Some(pred, predChunk, conds))
case _ => checkPredicates(rest, q, goal)(Q) // Multiple succ branches would require a disjunction. Left out for now
Expand Down Expand Up @@ -424,7 +424,7 @@ object AbductionPackage extends AbductionRule {
case suc: NonFatalResult =>

val abdRes = abductionUtils.getAbductionSuccesses(suc)
val stmts = abdRes.flatMap(_.stmts) //.reverse?
val stmts = abdRes.flatMap(_.stmts)//.reverse
val state = abdRes.flatMap(_.state).reverse

produces(q.s, freshSnap, state.map(_._1), _ => pve, q.v){ (s1, v1) =>
Expand Down
15 changes: 10 additions & 5 deletions src/main/scala/biabduction/Abstraction.scala
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,14 @@
package viper.silicon.biabduction

import viper.silicon.interfaces.{Success, VerificationResult}
import viper.silicon.interfaces.{Failure, Success, VerificationResult}
import viper.silicon.interfaces.state.Chunk
import viper.silicon.resources._
import viper.silicon.rules._
import viper.silicon.state._
import viper.silicon.verifier.Verifier
import viper.silver.ast._
import viper.silver.verifier.DummyReason
import viper.silver.verifier.errors.FoldFailed

import scala.annotation.tailrec

Expand Down Expand Up @@ -43,15 +45,18 @@ object AbstractionFold extends AbstractionRule {
case None => checkChunks(rest, q)(Q)
case Some(eArgs) =>


executionFlowController.tryOrElse0(q.s, q.v) {
(s1, v1, T) =>

val fold = Fold(PredicateAccessPredicate(PredicateAccess(Seq(eArgs), pred.name)(), FullPerm()())())()
executor.exec(s1, fold, v1, None, abdStateAllowed = false)(T)
executor.exec(s1, fold, v1, None, abdStateAllowed = false)((s1a, v1a) =>
//if (v1a.decider.checkSmoke()) {
// Failure(FoldFailed(fold, DummyReason))
//} else {
T(s1a, v1a)
//}
)

// TODO nklose this can branch
//predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pveTransformed, v1)(T)
} {
(s2, v2) => Q(Some(q.copy(s = s2, v = v2)))
} {
Expand Down
24 changes: 12 additions & 12 deletions src/main/scala/biabduction/BiAbduction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,6 @@ trait BiAbductionSuccess extends BiAbductionResult

case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[(Exp, Option[BasicChunk])] = Seq(), stmts: Seq[Stmt] = Seq(), newFieldChunks: Map[BasicChunk, LocationAccess], trigger: Option[Positioned] = None) extends BiAbductionSuccess {

val preTrans = VarTransformer

override def toString: String = {
"Abduced pres " + state.length + ", Abduced statements " + stmts.length
}
Expand Down Expand Up @@ -87,20 +85,21 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat

v.decider.setPcs(pcs)

val varTrans = VarTransformer(s, v, s.g.values, s.h)
val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) }
//val varTrans = VarTransformer(s, v, s.g.values, s.h)
//val preExps = bcExps.map {
// case Some(t) => preTrans.transformExp(t, strict = false)
// case None => None
//}


// If we can express as in vars, then we want to
val ins = s.currentMember.get.asInstanceOf[Method].formalArgs.map(_.localVar)
val preVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) }
val preTrans = VarTransformer(s, v, preVars, s.h)
val preExps = bcExps.map {
case Some(t) => preTrans.transformExp(t, strict = false)
case None => None
}

val varTrans = VarTransformer(s, v, preVars, s.h, otherVars = s.g.values)
val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) }

v.decider.setPcs(prevPcs)
preExps
bcExps
}

def getStatements(bcExps: Seq[Exp]): Option[Seq[Stmt]] = {
Expand Down Expand Up @@ -330,6 +329,7 @@ object BiAbductionSolver {

if (q1.v.decider.checkSmoke()) {
Success(Some(BiAbductionFailure(s, v, initPcs)))
//Unreachable()
} else {
val newChunks = newState.collect { case (_, c: Some[BasicChunk]) => c.get }
val newOldHeaps = q1.s.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks)) }
Expand Down Expand Up @@ -414,7 +414,7 @@ object BiAbductionSolver {
// That is why we do as much as possible on term level to avoid this as much as possible
val expUnjoined = termJoined.map {
case (reses, bcTerms) =>
reses -> reses.head.getBcExps(bcTerms).distinct.collect { case Some(bc) => bc }
reses -> reses.head.getBcExps(bcTerms).collect { case Some(bc) => bc }.flatMap(_.topLevelConjuncts).distinct
}
expUnjoined.groupBy(_._2).map { case (bcs, list) => list.head._1.head -> bcs }
}
Expand Down
163 changes: 93 additions & 70 deletions src/main/scala/biabduction/Invariant.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ package viper.silicon.biabduction
import viper.silicon.interfaces._
import viper.silicon.rules.producer.produces
import viper.silicon.rules.{evaluator, executionFlowController, executor, producer}
import viper.silicon.state.terms.Term
import viper.silicon.state.terms.{False, Term, True}
import viper.silicon.state.{Heap, State}
import viper.silicon.utils.ast.BigAnd
import viper.silicon.utils.freshSnap
Expand Down Expand Up @@ -35,11 +35,10 @@ object LoopInvariantSolver {
case _ => true
} ++ posts).distinct

// If the loop condition requires permissions which are folded away in the invariant, we need to partially unfold it.
executionFlowController.locallyWithResult[Seq[Exp]](s.copy(h = Heap()), v) { (s1, v1, Q1) =>
producer.produces(s1, freshSnap, rest ++ existingInvs, pveLam, v1) { (s2, v2) =>


// There are case where there is some overlap between lefts and rests, we remove this using abduction
val leftRes = executor.exec(s2, Assert(BigAnd(lefts))(), v2, None) {
(_, _) => Success()
}
Expand All @@ -48,6 +47,7 @@ object LoopInvariantSolver {
case nf: NonFatalResult =>
val leftsAbd = abductionUtils.getAbductionSuccesses(nf).flatMap(_.state).map(_._1)

// If the loop condition requires permissions which are folded away in the invariant, we need to partially unfold it.
producer.produces(s2, freshSnap, leftsAbd, pveLam, v2) { (s2a, v2a) =>
executionFlowController.tryOrElse0(s2a, v2a) { (s3, v3, T) =>
evaluator.eval(s3, loopCon, pve, v3)((s4, _, _, v4) => T(s4, v4))
Expand All @@ -56,7 +56,7 @@ object LoopInvariantSolver {
(_, _) => Q1(res)
} {
f =>
val abd = BiAbductionSolver.solveAbductionForError(s2, v2, f, stateAllowed = false, Some(loopCon)) { (_, _) =>
val abd = BiAbductionSolver.solveAbductionForError(s2a, v2a, f, stateAllowed = false, Some(loopCon)) { (_, _) =>
Success()
}
abd match {
Expand All @@ -71,8 +71,6 @@ object LoopInvariantSolver {
}

}


}
}
}
Expand All @@ -92,98 +90,123 @@ object LoopInvariantSolver {
iteration: Int = 1): VerificationResult = {


// TODO if the loop condition (and maybe also the loop invs) contain permissions which require statements from the starting state, then this will fail.
// I need thought out way to eval / assume / check all of these things each iteration.

println("\nIteration: " + iteration)

// We assume there is only one loop internal edge
val loopConExp = loopEdges.head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition
val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method])

// 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) =>

// Run the loop the first time to check whether we abduce any new state
executionFlowController.locally(sPreInv, vPreInv) { (sFP, vFP) =>
// Run the loop the first time to check whether we abduce any new state
executionFlowController.locally(s, v) { (s1, v1) =>

// TODO nklose follows should be private. We can exec the statement block instead?
executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint) {
(_, _) => Success()
//(s1, v1) =>
// We evaluate the loop condition at the end of loop so that we can start the next iteration from a valid state
//evaluator.evalWithAbduction(s1, loopConExp, pve, v1){(_, _, _, _) => Success()}
// Produce the already known invariants. They are consumed at the end of the loop body, so we need to do this every iteration
evaluator.evalWithAbduction(s1, BigAnd(loopHead.invs), pve, v1) { (s2, _, _, v2) =>
produces(s2, freshSnap, loopHead.invs, ContractNotWellformed, v2) { (s3, v3) =>
executor.follows(s3, loopEdges, pveLam, v3, joinPoint) {
(_, _) => Success()
}
}
} match {
}
} match {

// Abduction has failed so we fail
case f: Failure => f
case nonf: NonFatalResult =>
// Abduction has failed so we fail
case f: Failure => f
case nonf: NonFatalResult =>

val abdReses = abductionUtils.getAbductionSuccesses(nonf).reverse
// TODO nklose do we want to join branches properly here like we do for preconditions?
val newMatches = abdReses.flatMap(_.newFieldChunks).toMap
val preStateVars = sPreInv.g.values.filter { case (v, _) => origVars.contains(v) }
val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preStateVars, sPreInv.h, Seq(), newMatches).get }.distinct
val abdReses = abductionUtils.getAbductionSuccesses(nonf).reverse
// TODO nklose do we want to join branches properly here like we do for preconditions?
val newMatches = abdReses.flatMap(_.newFieldChunks).toMap
val preLoopVars = s.g.values.filter { case (v, _) => origVars.contains(v) }
val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preLoopVars, s.h, Seq(), newMatches).get }.distinct

// We still need to remove the current loop condition
val newState = abductionUtils.sortExps(newStateOpt.map(_.transform {
case im: Implies if im.left == loopConExp => im.right
}))
// We still need to remove the current loop condition
val newState = abductionUtils.sortExps(newStateOpt.map(_.transform {
case im: Implies if im.left == loopConExp => im.right
}))

println("New state:\n " + newState.mkString("\n "))
println("New state:\n " + newState.mkString("\n "))

// 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 the abduced things added
producer.produces(sPreInv, freshSnap, newState, pveLam, vPreInv) { (sPreAbd, vPreAbd) =>
// 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 the abduced things added
producer.produces(s, freshSnap, newState ++ loopHead.invs, pveLam, v) { (sPreAbd, vPreAbd) =>

abductionUtils.findChunks(newState.collect {
case loc: FieldAccessPredicate => loc.loc
case loc: PredicateAccessPredicate => loc.loc
}, sPreAbd, vPreAbd, pve) { chunks =>
abductionUtils.findChunks(newState.collect {
case loc: FieldAccessPredicate => loc.loc
case loc: PredicateAccessPredicate => loc.loc
}, sPreAbd, vPreAbd, pve) { chunks =>

val allChunks = chunks.keys
val allNewChunks = chunks.keys

val newPreState0 = sPreAbd.copy(h = q.preHeap.+(Heap(allChunks)))
BiAbductionSolver.solveAbstraction(newPreState0, vPreAbd) {
(newPreState, newPreAbstraction0, newPreV) =>
val newPreHeap = sPreAbd.copy(h = q.preHeap)
BiAbductionSolver.solveAbstraction(newPreHeap, vPreAbd) {
(newPreState, newPreAbstraction0, newPreV) =>

val preTran = VarTransformer(newPreState, newPreV, preStateVars, newPreState.h)
val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, strict = false).get)
val preTran = VarTransformer(newPreState, newPreV, preLoopVars, newPreState.h)
val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, strict = false).get)
println("New pre abstraction:\n " + newPreAbstraction.mkString("\n "))

println("New pre abstraction:\n " + newPreAbstraction.mkString("\n "))
executor.follows(sPreAbd, loopEdges, pveLam, vPreAbd, joinPoint)((sPost, vPost) => {

executor.follows(sPreAbd, loopEdges, pveLam, vPreAbd, joinPoint)((sPost, vPost) => {
sPreAbd
// To find a fixed point, we are only interested in branches where the conditions remains true
var nextCon = false
executionFlowController.locally(sPost, vPost) { (sPost1, vPost1) =>
evaluator.evalWithAbduction(sPost1, loopConExp, pve, vPost1) { (sCon, conTerm, _, vCon) =>
nextCon = conTerm != False
Success()
}
}
if (!nextCon) {
Success()
} else {

val ins = s.currentMember.get.asInstanceOf[Method].formalArgs.map(_.localVar)
val inVars = sPost.g.values.collect { case (v, t) if ins.contains(v) => (v, t) }
val preLoopVars = sPost.g.values.filter { case (v, _) => origVars.contains(v) }
val postTran = VarTransformer(sPost, vPost, inVars, sPost.h, otherVars = preLoopVars)

BiAbductionSolver.solveAbstraction(sPost, vPost) { (sPostAbs, postAbstraction0, vPostAbs) =>
val newPostAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get)
val endStmt = abductionUtils.getEndOfLoopStmt(loop)
Success(Some(FramingSuccess(sPostAbs, vPostAbs, newPostAbstraction, endStmt, vPostAbs.decider.pcs.duplicate(), postTran)))
}
}
}) match {
case f: FatalResult => f
case nf: NonFatalResult =>

val posts = abductionUtils.getFramingSuccesses(nf).groupBy(_.posts).toSeq

posts match {

val postStateVars = sPostAbs.g.values.filter { case (v, _) => origVars.contains(v) }
val postTran = VarTransformer(sPostAbs, vPostAbs, postStateVars, sPostAbs.h)
val newpostAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get)
case Seq((posts, frames)) =>

println("New post abstraction:\n " + newpostAbstraction.mkString("\n "))
val newPostAbstraction = posts

// If the pushed forward abstraction is the same as the previous one, we are done
if (newPreAbstraction.toSet == q.preAbstraction.toSet && newpostAbstraction.toSet == q.postAbstraction.toSet) {
// TODO this is unprecise
val fr = frames.head
println("New post abstraction:\n " + newPostAbstraction.mkString("\n "))

val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method])
val existingInvs = loop.invs
getInvariants(newPreAbstraction, newpostAbstraction, loopConExp, existingInvs, sPostAbs, vPostAbs) { res =>
println("Invariants:\n " + res.mkString("\n "))
Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = res, loop, vPostAbs.decider.pcs.duplicate())))
// If the pushed forward abstraction is the same as the previous one, we are done
if (iteration > 1 && newPreAbstraction.toSet == q.preAbstraction.toSet && newPostAbstraction.toSet == q.postAbstraction.toSet) {

val existingInvs = loop.invs
getInvariants(newPreAbstraction, newPostAbstraction, loopConExp, existingInvs, fr.s, fr.v) { res =>
println("Invariants:\n " + res.mkString("\n "))
Success(Some(LoopInvariantSuccess(fr.s, fr.v, invs = res, loop, fr.v.decider.pcs.duplicate())))
}
} else {
//val newLoopCons = loopConBcs :+ loopCondTerm
// Else continue with next iteration, using the state from the end of the loop
fr.v.decider.setPcs(fr.pcs)
solveLoopInvariants(fr.s, fr.v, origVars, loopHead, loopEdges, joinPoint, initialBcs, q.copy(preHeap = newPreState.h + Heap(allNewChunks), preAbstraction = newPreAbstraction,
postAbstraction = newPostAbstraction), iteration = iteration + 1)
}
} 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, initialBcs, q.copy(preHeap = newPreState.h, preAbstraction = newPreAbstraction,
postAbstraction = newpostAbstraction), iteration = iteration + 1)
}
}
})
}
}
}
//}
}
}
}
}
}
}
Loading

0 comments on commit e2eb54d

Please sign in to comment.