Skip to content

Commit

Permalink
Worked on branching
Browse files Browse the repository at this point in the history
  • Loading branch information
@rayman2000
rayman2000 committed Dec 4, 2024
1 parent 344578b commit fad3824
Show file tree
Hide file tree
Showing 7 changed files with 229 additions and 182 deletions.
2 changes: 1 addition & 1 deletion src/main/scala/biabduction/Abduction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
313 changes: 200 additions & 113 deletions src/main/scala/biabduction/BiAbduction.scala
View file

Large diffs are not rendered by default.

38 changes: 12 additions & 26 deletions src/main/scala/biabduction/Invariant.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand All @@ -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)) {
Expand Down Expand Up @@ -160,49 +163,32 @@ 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 =>
preInv ++ postAbstraction match {
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)
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/rules/Executor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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
Expand Down
49 changes: 13 additions & 36 deletions src/main/scala/supporters/MethodSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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._
Expand Down Expand Up @@ -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))
)
}
}
}
Expand All @@ -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
Expand All @@ -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)
Expand Down
3 changes: 0 additions & 3 deletions src/test/resources/biabduction/nlist/branching.vpr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,3 @@ method test(x: Ref, cond: Bool)
reverse(x.next)
}
}



2 changes: 1 addition & 1 deletion src/test/resources/biabduction/nnlist/loop.vpr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit fad3824

Please sign in to comment.