diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index 31e0edd5..aec63979 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -109,11 +109,10 @@ case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), l def addToMethod(m: Method): Option[Method] = { val body = m.body.get val newBody = body.transform { - case l: While if l == loop => + case l: While if l.cond == loop.cond => l.copy(invs = l.invs ++ invs)(pos = l.pos, info = l.info, errT = l.errT) case other => other } - //val newBody = body.copy(ss = newSs)(pos = body.pos, info = body.info, errT = body.errT) Some(m.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) } } @@ -124,7 +123,6 @@ case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], loc: Position) def addToMethod(m: Method): Option[Method] = { Some(m.copy(posts = m.posts ++ posts)(pos = m.pos, info = m.info, errT = m.errT)) } - } case class BiAbductionFailure(s: State, v: Verifier) extends BiAbductionResult { @@ -298,7 +296,11 @@ object abductionUtils { } def getContainingPredicates(f: FieldAccess, p: Program): Seq[Predicate] = { - p.predicates.filter(_.body.get.contains(f)) + + p.predicates.filter{ pred => + val absAcc = f.copy(rcv = pred.formalArgs.head.localVar)(f.pos, f.info, f.errT) + pred.body.get.contains(absAcc) + } } def checkBc(v: Verifier, bc: Term, ignoredBcs: Seq[Term]): Boolean = { diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index eb7e9249..8df35678 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -360,7 +360,7 @@ object executor extends ExecutionRules { } } - private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], stmt: Stmt)(Q: (State, Verifier) => VerificationResult): VerificationResult = { + private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], location: Stmt)(Q: (State, Verifier) => VerificationResult): VerificationResult = { if (invs.isEmpty) { Q(s, v) } else { @@ -372,7 +372,7 @@ object executor extends ExecutionRules { } { f => // There are cases where it is incorrect to abduce state here, but only some cases and it is hard to distinguish them - BiAbductionSolver.solveAbduction(s, v, f, Some(stmt))((s3, res, v3) => Success(Some(res)) && checkInvariants(s3, v3, invs, stmt)(Q)) + BiAbductionSolver.solveAbduction(s, v, f, Some(location))((s3, res, v3) => Success(Some(res)) && checkInvariants(s3, v3, invs, location)(Q)) } } } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 3f8f8a73..3e243e7f 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -132,12 +132,12 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { val abdResult: VerificationResult = result match { case suc: NonFatalResult if method.body.isDefined => + // Collect all the abductions and try to generate preconditions val abdReses = abductionUtils.getBiAbductionSuccesses(suc) - - - val pres = abductionUtils.getAbductionSuccesses(suc).filter{_.state.nonEmpty} - + val pres = abductionUtils.getAbductionSuccesses(suc).collect{ case abd if abd.state.nonEmpty => abd} + val states = pres.map(_.state.head) + val triggers = pres.map(_.trigger) val newMethod = abdReses.foldLeft[Option[Method]](Some(method))( (m, res) => m match { case None => None @@ -177,7 +177,6 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { consumes(s, posts, postViolated, v)(QS) } { (s1: State, _: Term, v1: Verifier) => { - // TODO nklose We want to do abstraction, but that might require adding folds and such... 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) }