diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index b8bfd1123..e133a13d3 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -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 => @@ -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 { diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index e9701c63b..5a88f95a0 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -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) } } } diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index 029e4abc4..34703a92f 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -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 } } diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index ce983ba75..881148d2a 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -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} @@ -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: @@ -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 @@ -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) => { @@ -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 @@ -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 @@ -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) diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 9166f4452..5005ed60d 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -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 @@ -122,7 +122,12 @@ 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 => @@ -130,26 +135,26 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { 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 @@ -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 =>