Skip to content

Commit

Permalink
Line number and postconditions for loops.
Browse files Browse the repository at this point in the history
  • Loading branch information
@rayman2000
rayman2000 committed Oct 18, 2024
1 parent 0d56642 commit ef5c200
Show file tree
Hide file tree
Showing 5 changed files with 46 additions and 29 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/biabduction/BiAbduction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ trait BiAbductionRule[S] {

object BiAbductionSolver {

def solveAbduction(s: State, v: Verifier, f: Failure)(Q: (State, Verifier) => VerificationResult): VerificationResult = {
def solveAbduction(s: State, v: Verifier, f: Failure, loc: Option[Position] = None)(Q: (State, Verifier) => VerificationResult): VerificationResult = {

val abdGoal: Option[AccessPredicate] = f.message.reason match {
case reason: InsufficientPermission =>
Expand All @@ -142,7 +142,7 @@ object BiAbductionSolver {
if (q1.goal.isEmpty) {
producer.produces(s, freshSnap, q1.foundState, _ => Internal(), v) { (s2, v2) =>
executor.execs(s2, q1.foundStmts.reverse, v2) { (s3, v3) =>
Success(Some(AbductionSuccess(s, v, v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = f.message.pos))) && Q(s3, v3)
Success(Some(AbductionSuccess(s, v, v.decider.pcs.duplicate(), q1.foundState, q1.foundStmts, loc = loc.getOrElse(f.message.pos)))) && Q(s3, v3)
}
}
} else {
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/biabduction/Invariant.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ object LoopInvariantSolver {
locs match {
case Seq() => Q(Seq())
case loc +: rest =>
findChunkFromExp(loc, s, v){
findChunkFromExp(loc, s, v) {
case Some(chunk) => findChunks(rest, s, v) { chunks => Q(chunk +: chunks) }
}
}
Expand Down
9 changes: 5 additions & 4 deletions src/main/scala/biabduction/VarTransformer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,13 +50,14 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa

t match {
case t if matches.contains(t) => matches.get(t)
//case BuiltinEquals(t1, t2) => (transformTerm(t1), transformTerm(t2)) match {
// case (Some(e1), Some(e2)) => Some(EqCmp(e1, e2)())
// case _ => None
//}
case BuiltinEquals(t1, t2) => (transformTerm(t1), transformTerm(t2)) match {
case (Some(e1), Some(e2)) => Some(EqCmp(e1, e2)())
case _ => None
}
case terms.FractionPermLiteral(r) => Some(FractionalPerm(IntLit(r.numerator)(), IntLit(r.denominator)())())
case terms.FullPerm => Some(FullPerm()())
case terms.Null => Some(NullLit()())
case terms.Not(t) => transformTerm(t).map(Not(_)())
case _ => None
}
}
Expand Down
21 changes: 14 additions & 7 deletions src/main/scala/rules/Executor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import viper.silicon.state.terms.predef.`?r`
import viper.silicon.utils.ast.{BigAnd, extractPTypeFromExp, simplifyVariableName}
import viper.silicon.utils.freshSnap
import viper.silicon.verifier.Verifier
import viper.silver.ast.{Exp, Stmt, VirtualPosition}
import viper.silver.ast.{Exp, Position, Stmt, VirtualPosition}
import viper.silver.cfg.silver.SilverCfg
import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge}
import viper.silver.cfg.{ConditionalEdge, StatementBlock}
Expand Down Expand Up @@ -228,6 +228,10 @@ object executor extends ExecutionRules {
sys.error(s"Unexpected block: $block")

case block@cfg.LoopHeadBlock(existingInvs, stmts, _) =>

val invLoc = s.methodCfg.outEdges(block).head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition.pos
val endPos = VirtualPosition("End of loop at " + invLoc.toString)

incomingEdgeKind match {
case cfg.Kind.In =>
/* We've reached a loop head block via an in-edge. Steps to perform:
Expand All @@ -250,6 +254,7 @@ object executor extends ExecutionRules {
map.updated(x, xNew)}))
val sBody = s.copy(g = gBody, h = Heap())


val edges = s.methodCfg.outEdges(block)
val (outEdges, otherEdges) = edges partition (_.kind == cfg.Kind.Out)
val sortedEdges = otherEdges ++ outEdges
Expand All @@ -275,11 +280,13 @@ object executor extends ExecutionRules {

type PhaseData = (State, RecordedPathConditions, Set[FunctionDecl])
var phase1data: Vector[PhaseData] = Vector.empty



val invSuc = if (newInvs.isEmpty) {
Success()
} else {
Success(Some(LoopInvariantSuccess(s, v, foundInvs, otherEdges.head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition.pos)))
Success(Some(LoopInvariantSuccess(s, v, foundInvs, invLoc)))
}

val wfi = executionFlowController.locally(sBody, v)((s0, v0) => {
Expand All @@ -295,7 +302,7 @@ object executor extends ExecutionRules {

val con = executionFlowController.locally(s, v) ((s0, v0) => {
v0.decider.prover.comment("Loop head block: Establish invariant")
checkInvariants(s0, v0, invs)((sLeftover, v1) => {
checkInvariants(s0, v0, invs, invLoc)((sLeftover, v1) => {
v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")
phase1data.foldLeft(Success(): VerificationResult) {
case (result, _) if !result.continueVerification => result
Expand All @@ -322,7 +329,7 @@ object executor extends ExecutionRules {
executionFlowController.locally(s4, v3)((s5, v5) => {
follows(s5, otherEdges, WhileFailed, v5, joinPoint)((s6, v6) => {
// TODO nklose check that no new state is abduced, this would be incorrect
checkInvariants(s6, v6, foundInvs)((_, _) => Success())
checkInvariants(s6, v6, foundInvs, endPos)((_, _) => Success())
}
)
}) combine
Expand Down Expand Up @@ -350,16 +357,16 @@ object executor extends ExecutionRules {
*/
v.decider.prover.comment("Loop head block: Re-establish invariant")
// TODO nklose check that no new state is abduced, this would be incorrect
checkInvariants(s, v, existingInvs)(Q)
checkInvariants(s, v, existingInvs, endPos)(Q)
}
}

}

private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp])(Q: (State, Verifier) => VerificationResult): VerificationResult = {
private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], loc: Position)(Q: (State, Verifier) => VerificationResult): VerificationResult = {
executionFlowController.tryOrElse1[Term](s, v){(s1, v1, QS) => consumes(s1, invs, LoopInvariantNotPreserved, v1)(QS) }
{(s1, _, v1) => Q(s1, v1)}
{f => BiAbductionSolver.solveAbduction(s, v, f)((s3, v3) => checkInvariants(s3, v3, invs)(Q))}
{f => BiAbductionSolver.solveAbduction(s, v, f, Some(loc))((s3, v3) => checkInvariants(s3, v3, invs, loc)(Q))}
}

def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier)
Expand Down
39 changes: 24 additions & 15 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, abductionUtils}
import viper.silicon.biabduction.{BiAbductionSolver, FramingSuccess, VarTransformer, abductionUtils}
import viper.silicon.decider.Decider
import viper.silicon.interfaces._
import viper.silicon.logger.records.data.WellformednessCheckRecord
Expand Down Expand Up @@ -122,34 +122,39 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
executionFlowController.locally(s2a, v2)((s3, v3) => {
exec(s3, body, v3) { (s4, v4) => {
handlePostConditions(s4, method, posts, v3)
}}})})})})
}
}
})
})
})
})

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 = abductionUtils.getAbductionSuccesses(suc)
val pres = abds.map {abd => abd.toPrecondition(inVars, abd.s.oldHeaps.head._2)}
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)){
if (pres.contains(None)) {
Failure(Internal(reason = InternalReason(DummyNode, "Failed to generate preconditions from abduction results")))
} else {
// Otherwise we succeed
val presTra = pres.flatMap(_.get).distinct
if(presTra.nonEmpty){
println("Generated preconditions from abductions: " + presTra.mkString(" && "))
if (presTra.nonEmpty) {
println("Generated preconditions from abductions: " + presTra.mkString(" && "))
}
val stmtStrs = abds.flatMap {abd => abd.stmts.map {stmt => " Line " + abd.line + ": " + stmt.toString() }}.distinct
if(stmtStrs.nonEmpty) {
val stmtStrs = abds.flatMap { abd => abd.stmts.map { stmt => " Line " + abd.line + ": " + stmt.toString() } }.distinct
if (stmtStrs.nonEmpty) {
println("Abduced the following statements:\n" + stmtStrs.reverse.mkString("\n"))
}
val invs = abductionUtils.getInvariantSuccesses(suc).map(invSuc => " Line " + invSuc.line + ": " + invSuc.invs.mkString(" && ")).distinct
if(invs.nonEmpty){
if (invs.nonEmpty) {
println("Generated invariants::\n" + invs.mkString("\n"))
}
val posts = abductionUtils.getFramingSuccesses(suc).flatMap(_.posts).distinct
if(posts.nonEmpty){
if (posts.nonEmpty) {
println("Generated postconditions: " + posts.mkString(" && "))
}
result
Expand Down Expand Up @@ -179,11 +184,15 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
} {
(s1: State, _: Term, v1: Verifier) => {
// TODO nklose We want to do abstraction, but that might require adding folds and such...
val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar)
val vars = s1.g.values.collect { case (v2, t) if formals.contains(v2) => (v2, t) }
val newPosts = BiAbductionSolver.solveFraming(s1, v1, vars, method.pos)
val newRes = if(newPosts.posts.isEmpty) Success() else handlePostConditions(s1, method, newPosts.posts, v1)
newRes && Success(Some(newPosts))
BiAbductionSolver.solveAbstraction(s1, v1) { (s2, framedPosts, v2) =>
val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar)
val vars = s2.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) }
//val newPosts = BiAbductionSolver.solveFraming(s1, v1, vars, method.pos)
val varTran = VarTransformer(s2, v2, vars, s2.h)
val newPosts = framedPosts.map { e => varTran.transformExp(e) }.collect { case Some(e) => e }
val newRes = if (newPosts.isEmpty) Success() else handlePostConditions(s1, method, newPosts, v1)
newRes && Success(Some(FramingSuccess(s2, v2, newPosts, method.pos)))
}
}
} {
f =>
Expand Down

0 comments on commit ef5c200

Please sign in to comment.