Skip to content

Commit

Permalink
We back baby!
Browse files Browse the repository at this point in the history
  • Loading branch information
@rayman2000
rayman2000 committed Sep 2, 2024
1 parent 8836fa4 commit 728886c
Show file tree
Hide file tree
Showing 5 changed files with 124 additions and 113 deletions.
22 changes: 12 additions & 10 deletions src/main/scala/biabduction/Abduction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,8 @@ object AbductionFold extends AbductionRule {
(s1: State, v1: Verifier) =>
val fold = Fold(a)()
val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, sorts.Ref))
Q(Some(q.copy(s = s1, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost)))
val q2 = q.copy(s = s1, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1)
Q(Some(q2))
} { _: FatalResult => R() }
case None => R()
}
Expand Down Expand Up @@ -357,17 +358,18 @@ object AbductionPackage extends AbductionRule {
producer.produce(q.s, freshSnap, wand.left, pve, q.v)((s1, v1) => {

val packQ = q.copy(s = s1, v = v1, goal = Seq(wand.right))
val packRes = AbductionApplier.apply(packQ)
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")
}

// TODO nklose we should instead not trigger
if (packRes.goal.nonEmpty) {
throw new Exception("Could not find proof script for package")
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)))
}

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 Down
61 changes: 31 additions & 30 deletions src/main/scala/biabduction/BiAbduction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,22 +87,18 @@ trait RuleApplier[S] {
/**
* Recursively applies the rules until we reach the end of the rules list.
*/
def apply(in: S, currentRule: Int = 0): S = {
def applyRules(in: S, currentRule: Int = 0)(Q: S => VerificationResult): VerificationResult = {

var result = in

if (currentRule < rules.length) {
rules(currentRule).apply(in) { s =>
s match {
case Some(out) =>
result = apply(out)
case None =>
result = apply(in, currentRule + 1)
}
Failure(Internal().dueTo(DummyReason))
if(currentRule == rules.length){
Q(in)
} else {
rules(currentRule).apply(in) {
case Some(out) =>
applyRules(out)(Q)
case None =>
applyRules(in, currentRule + 1)(Q)
}
}
result
}
}

Expand All @@ -120,7 +116,7 @@ object BiAbductionSolver {

def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): BiAbductionResult = {

executionFlowController.locally(s, v)((s1, v1) => {
val res = executionFlowController.locally(s, v)((s1, v1) => {

val qPre = AbductionQuestion(s1, v1, goal)

Expand All @@ -129,27 +125,32 @@ object BiAbductionSolver {
case _ => qPre
}

val q1 = AbductionApplier.apply(q)

if (q1.goal.isEmpty) {
Success(Some(AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc)))
} else {
Failure(Internal() dueTo DummyReason)
AbductionApplier.applyRules(q){ q1 =>
if (q1.goal.isEmpty) {
Success(Some(AbductionSuccess(q.s, q.v, q.v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc)))
} else {
Failure(Internal() dueTo DummyReason)
}
}
}) match {
case Success(Some(abd: AbductionSuccess)) => abd
case _ => BiAbductionFailure(s, v)

})

res match {
case nf: NonFatalResult =>
// TODO Can we ever get multiple abduction results here?
abductionUtils.getAbductionResults(nf).head
case _ =>
BiAbductionFailure(s, v)
}
}

def solveAbstraction(s: State, v: Verifier, exps: Seq[Exp]): Seq[Exp] = {
var res: Seq[Exp] = Seq()
executionFlowController.locally(s, v)((s1, v1) => {
def solveAbstraction(s: State, v: Verifier, exps: Seq[Exp])(Q: Seq[Exp] => VerificationResult): VerificationResult = {
executionFlowController.locallyWithResult[Seq[Exp]](s, v)((s1, v1, QS) => {
val q = AbstractionQuestion(exps, s1, v1)
res = AbstractionApplier.apply(q).exps
Success()
})
res
AbstractionApplier.applyRules(q){ q1 =>
QS(q1.exps)
}
})(Q)
}

def solveFraming(s: State, v: Verifier, postVars: Map[AbstractLocalVar, Term], loc: Position = NoPosition, ignoredBcs: Seq[Exp] = Seq()): FramingSuccess = {
Expand Down
138 changes: 71 additions & 67 deletions src/main/scala/biabduction/Invariant.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,77 +89,81 @@ object LoopInvariantSolver {
q
}

val newPreAbstraction = BiAbductionSolver.solveAbstraction(sPreAbd, vPreAbd, q1.preAbstraction ++ newPreState)
val res = executionFlowController.locally(sPreAbd, vPreAbd) { (sPreAbd2, vPreAbd2) =>
executor.follows(sPreAbd2, loopEdges, pveLam, vPreAbd2, joinPoint)((sPost, vPost) => {

// Values of the variables at the end of loop in terms of the beginning of the loop
val relVarTrans = VarTransformer(sPost, vPost, sPreAbd2.g.values.filter { case (v, _) => origVars.contains(v)}, sPreAbd2.h)
val relPreValues = sPost.g.values.collect { case (v, t) if wvs.contains(v) => (v, relVarTrans.transformTerm(t)) }
.collect { case (v, e) if e.isDefined => (v, e.get) }


// We would like to transform as much as possible to the absVars.
// However, if state is created, then this my not be possible. Then we are willing to transform things to
// wvs as well
val postTranAbs = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => absVars.contains(v) }, sPost.h)
val postTranOrig = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => origVars.contains(v) }, sPost.h)
val postsRaw = BiAbductionSolver.solveFraming(sPost, vPost, sPost.g.values, NoPosition, Seq(loopCondition)).posts
val postsTran = postsRaw.map{exp =>
val wvsPost = postTranOrig.transformExp(exp)
postTranAbs.transformExp(wvsPost.get, strict=false).get
}
val postAbstraction = BiAbductionSolver.solveAbstraction(sPost, vPost, postsTran)

val newAbsPostValues: Map[AbstractLocalVar, Exp] = relPreValues.collect { case (v, e) => (v, e.transform {
case lv: LocalVar if q1.absValues.contains(lv) => q1.absValues(lv)
})
}

// To check whether we are done, we take the previous abstractions and "push them forward" an iteration
val relPreAssigns: Map[Exp, Exp] = {
q1.absValues.collect {
case (v, e) if newAbsPostValues.contains(v) => (e, newAbsPostValues(v))
BiAbductionSolver.solveAbstraction(sPreAbd, vPreAbd, q1.preAbstraction ++ newPreState) { newPreAbstraction =>
val res = executionFlowController.locally(sPreAbd, vPreAbd) { (sPreAbd2, vPreAbd2) =>
executor.follows(sPreAbd2, loopEdges, pveLam, vPreAbd2, joinPoint)((sPost, vPost) => {

// Values of the variables at the end of loop in terms of the beginning of the loop
val relVarTrans = VarTransformer(sPost, vPost, sPreAbd2.g.values.filter { case (v, _) => origVars.contains(v) }, sPreAbd2.h)
val relPreValues = sPost.g.values.collect { case (v, t) if wvs.contains(v) => (v, relVarTrans.transformTerm(t)) }
.collect { case (v, e) if e.isDefined => (v, e.get) }


// We would like to transform as much as possible to the absVars.
// However, if state is created, then this my not be possible. Then we are willing to transform things to
// wvs as well
val postTranAbs = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => absVars.contains(v) }, sPost.h)
val postTranOrig = VarTransformer(sPost, vPost, sPost.g.values.filter { case (v, _) => origVars.contains(v) }, sPost.h)
val postsRaw = BiAbductionSolver.solveFraming(sPost, vPost, sPost.g.values, NoPosition, Seq(loopCondition)).posts
val postsTran = postsRaw.map { exp =>
val wvsPost = postTranOrig.transformExp(exp)
postTranAbs.transformExp(wvsPost.get, strict = false).get
}
}
val prevPreAbstTrans = q1.preAbstraction.map(_.transform {
case exp: Exp if relPreAssigns.contains(exp) => relPreAssigns(exp)
})

val relPostAssigns: Map[Exp, Exp] = {
newAbsPostValues.collect {
case (v, e) if q1.absValues.contains(v) => (q1.absValues(v), e)
BiAbductionSolver.solveAbstraction(sPost, vPost, postsTran) { postAbstraction =>

val newAbsPostValues: Map[AbstractLocalVar, Exp] = relPreValues.collect { case (v, e) => (v, e.transform {
case lv: LocalVar if q1.absValues.contains(lv) => q1.absValues(lv)
})
}

// To check whether we are done, we take the previous abstractions and "push them forward" an iteration
val relPreAssigns: Map[Exp, Exp] = {
q1.absValues.collect {
case (v, e) if newAbsPostValues.contains(v) => (e, newAbsPostValues(v))
}
}
val prevPreAbstTrans = q1.preAbstraction.map(_.transform {
case exp: Exp if relPreAssigns.contains(exp) => relPreAssigns(exp)
})

val relPostAssigns: Map[Exp, Exp] = {
newAbsPostValues.collect {
case (v, e) if q1.absValues.contains(v) => (q1.absValues(v), e)
}
}
val prevPostAbstTrans = q1.postAbstraction.map(_.transform {
case exp: Exp if relPostAssigns.contains(exp) =>
relPostAssigns(exp)
})

// If the pushed forward abstraction is the same as the previous one, we are done
if (newPreAbstraction.diff(prevPreAbstTrans).isEmpty && postAbstraction.diff(prevPostAbstTrans).isEmpty) {

// Swap in the assigned to variables again instead of the absolute values
val newAbsSwapped = newAbsPostValues.collect { case (v, e) if origVars.contains(v) => (e, v) }
val relPreAbstraction = newPreAbstraction.map(_.transform {
case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp)
})
val postInv = postAbstraction.map(_.transform {
case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp)
})

val preInv = relPreAbstraction.flatMap(getPreInvariant)
Success(Some(LoopInvariantSuccess(sPost, vPost, invs = preInv ++ postInv, loopCondition.pos)))
} else {
// Else continue with next iteration, using the state from the end of the loop
executionFlowController.locally(sPost, vPost)((sNext, vNext) => {
solveLoopInvariants(sNext, vNext, origVars, loopHead, loopEdges, joinPoint, q1.copy(preAbstraction = newPreAbstraction,
postAbstraction = postAbstraction, absValues = newAbsPostValues), iteration = iteration + 1)
}
)
}
}
}
val prevPostAbstTrans = q1.postAbstraction.map(_.transform {
case exp: Exp if relPostAssigns.contains(exp) =>
relPostAssigns(exp)
})

// If the pushed forward abstraction is the same as the previous one, we are done
if (newPreAbstraction.diff(prevPreAbstTrans).isEmpty && postAbstraction.diff(prevPostAbstTrans).isEmpty) {

// Swap in the assigned to variables again instead of the absolute values
val newAbsSwapped = newAbsPostValues.collect { case (v, e) if origVars.contains(v) => (e, v) }
val relPreAbstraction = newPreAbstraction.map(_.transform {
case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp)
})
val postInv = postAbstraction.map(_.transform {
case exp: Exp if newAbsSwapped.contains(exp) => newAbsSwapped(exp)
})

val preInv = relPreAbstraction.flatMap(getPreInvariant)
Success(Some(LoopInvariantSuccess(sPost, vPost, invs = preInv ++ postInv, loopCondition.pos)))
} else {
// Else continue with next iteration, using the state from the end of the loop
executionFlowController.locally(sPost, vPost)((sNext, vNext) => {
solveLoopInvariants(sNext, vNext, origVars, loopHead, loopEdges, joinPoint, q1.copy(preAbstraction = newPreAbstraction,
postAbstraction = postAbstraction, absValues = newAbsPostValues), iteration = iteration + 1)
})
}
})
)
}
res
}
res
}
})
}
Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/biabduction/VarTransformer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@ 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
import viper.silver.verifier.errors.Internal
//import viper.silver.verifier.PartialVerificationError
//import viper.silver.verifier.errors.Internal

case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, Term], targetHeap: Heap) {

val pve: PartialVerificationError = Internal()
//val pve: PartialVerificationError = Internal()

// Ask the decider whether any of the terms are equal to a target.
val matches: Map[Term, Exp] = resolveMatches()
Expand Down
10 changes: 7 additions & 3 deletions src/main/scala/rules/ExecutionFlowController.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,9 +190,13 @@ object executionFlowController extends ExecutionFlowRules {
// This is not as efficient as it maybe could be, we call action twice.
// To speed it up we would have to save the s2, v2, r that we currently ignore in the fake
// continuation
locallyWithResult[R](s, v) { (s1, v1, Q1) =>
action(s1, v1, (_, _, _) => Success()) } {
case Success(_) => action(s, v, Q)
val res1 = locally(s, v) { (s1, v1) =>
action(s1, v1, (_, _, _) => Success()) }

res1 match {
case _: NonFatalResult =>
val res = action(s, v, Q)
res
case f: FatalResult => F(f)
}
}
Expand Down

0 comments on commit 728886c

Please sign in to comment.