diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 000000000..32cfc61d2 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,5 @@ +{ + "files.watcherExclude": { + "**/target": true + } +} \ No newline at end of file diff --git a/silver b/silver index e2b64333a..fe91024e7 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit e2b64333a1b05d9450148a826daf4ede1704e4ca +Subproject commit fe91024e7e310bba79000b31179e968f3fb9282e diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index faa56d350..4f0564833 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -2,21 +2,25 @@ package viper.silicon.biabduction import viper.silicon import viper.silicon.interfaces._ +import viper.silicon.interfaces.state.Chunk import viper.silicon.rules._ import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.rules.evaluator.{eval, evals} import viper.silicon.rules.producer.produces import viper.silicon.state._ -import viper.silicon.state.terms.{SortWrapper, Term} +import viper.silicon.state.terms.{FractionPermLiteral, PermLiteral, PermTimes, Permissions, SortWrapper, Term} import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ +import viper.silver.utility.Common.Rational import viper.silver.verifier.errors.Internal +import viper.silver.verifier.reasons.AssertionFalse import viper.silver.verifier.{BiAbductionQuestion, DummyReason} +import scala.collection.concurrent.TrieMap + object AbductionApplier extends RuleApplier[AbductionQuestion] { - override val rules: Seq[AbductionRule] = Seq(AbductionRemove, AbductionFoldBase, - AbductionFold, AbductionUnfold, AbductionApply, AbductionPackage, AbductionMissing) + override val rules: Seq[AbductionRule] = Seq(AbductionBase, AbductionApply, AbductionFoldBase, AbductionFold, AbductionUnfold, AbductionPackage, AbductionMissing) } case class AbductionQuestion(s: State, v: Verifier, goal: Seq[Exp], @@ -30,54 +34,8 @@ case class AbductionQuestion(s: State, v: Verifier, goal: Seq[Exp], * If the rule was applied, then we have to return to the start of the rule list, otherwise we increment the rule index. */ trait AbductionRule extends BiAbductionRule[AbductionQuestion] { - - - /** - * Does a couple of things to ensure evalution works properly: - * - * Check the lost accesses to see if the access is there - * Evaluate sub-expressions safely to ensure that a missing chunk will not cause the evaluation to silently abort - */ - protected def safeEval(e: Exp, s: State, v: Verifier, lostAccesses: Map[Exp, Term])(Q: (State, Option[Term], Verifier) => VerificationResult): VerificationResult = { - - if (!e.contains[LocationAccess]) { - eval(s, e, pve, v)((s1, t, _, v1) => Q(s1, Some(t), v1)) - } else { - - // If the arg was lost, we have it in the map - if (lostAccesses.contains(e)) { - Q(s, Some(lostAccesses(e)), v) - } else { - e match { - // If the arg is a location access, we have to recursively check it - case loc: LocationAccess => checkChunk(loc, s, v, lostAccesses) { - case Some(c) => Q(s, Some(c.snap), v) - case None => Q(s, None, v) - } - //case lv: AbstractLocalVar => Q(s, Some(s.g(lv)), v) - case _ => eval(s, e, pve, v)((s, t, _, v) => Q(s, Some(t), v)) - //case _ => evalLocationAccess(q.s, loc, pve, q.v) { (s2, _, tArgs, v2) => Q(s2, Some(tArgs), v2) } - } - } - } - } - - protected def checkChunk(loc: LocationAccess, s: State, v: Verifier, lostAccesses: Map[Exp, Term])(Q: Option[BasicChunk] => VerificationResult): VerificationResult = { - val arg = loc match { - case FieldAccess(rcv, _) => rcv - case PredicateAccess(args, _) => args.head - } - safeEval(arg, s, v, lostAccesses) { (s2, terms, v2) => - terms match { - case Some(term) => - val resource = loc.res(s2.program) - val id = ChunkIdentifier(resource, s2.program) - val chunk = findChunk[BasicChunk](s2.h.values, id, Seq(term), v2) - Q(chunk) - case None => Q(None) - } - } - } + // This helps us not to compute the field map of a predicate every time + val predFieldsCache = TrieMap.empty[(Predicate, PredicateAccessPredicate), Map[FieldAccess, Rational]] } /** @@ -85,7 +43,7 @@ trait AbductionRule extends BiAbductionRule[AbductionQuestion] { * Remove predicate and fields accesses which are both in the goal and in the current state */ // TODO this should add to lostAccesses -object AbductionRemove extends AbductionRule { +object AbductionBase extends AbductionRule { // TODO we should also remove magic wands, so all access predicates override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = { @@ -94,15 +52,75 @@ object AbductionRemove extends AbductionRule { case e: PredicateAccessPredicate => e } acc match { - case None => Q(None) - case Some(g@AccessPredicate(loc: LocationAccess, _)) => + case None => + Q(None) + case Some(g@AccessPredicate(loc: LocationAccess, _: WildcardPerm)) => val g1 = q.goal.filterNot(g == _) - checkChunk(loc, q.s, q.v, q.lostAccesses) { - case Some(_) => Q(Some(q.copy(goal = g1))) - case None => apply(q.copy(goal = g1)) { - case Some(q2) => Q(Some(q2.copy(goal = g +: q2.goal))) - case None => Q(None) - } + abductionUtils.permsTo(loc, q.s, q.v, q.lostAccesses) { + case Some(_: NoPerm) => + Q(None) + case _ => + Q(Some(q.copy(goal = g1))) + } + case Some(g@AccessPredicate(loc: LocationAccess, permG: Exp)) => + val g1 = q.goal.filterNot(g == _) + abductionUtils.permsTo(loc, q.s, q.v, q.lostAccesses) { + // If we have fullperm, we can just remove the goal + case Some(_: FullPerm) => + Q(Some(q.copy(goal = g1))) + // No perm, keep going + case Some(_: NoPerm) => + Q(None) + case Some(permH: FractionalPerm) => + // pH >= pG, we can just remove the goal + val varTrans = VarTransformer(q.s, q.v, q.s.g.values, q.s.h) + if (q.v.decider.check(terms.AtLeast(varTrans.permExpToTerm(permH), varTrans.permExpToTerm(permG)), Verifier.config.checkTimeout())) { + Q(Some(q.copy(goal = g1))) + } + // pH < pG, reduce the goal and keep going + else { + Q(None) + // This was moved into the AbdMissing rule when the Base rule was modified, left here for completeness + /*val newP = abductionUtils.clampSubPerm(Some(permG), Some(permH)) + val g2 = abductionUtils.accWithPerm(g, Some(newP)) + val toConsume = abductionUtils.accWithPerm(g, Some(permH)) + consumer.consume(q.s, toConsume, false, pve, q.v) { + (s1, _, v1) => + val q1 = q.copy(s = s1, v = v1, goal = Seq(g2)) + AbductionApplier.applyRules(q1) { baseRes => + if (baseRes.goal.nonEmpty) { + Q(None) + } else { + // val state = q.foundState ++ baseRes.foundState + producer.produce(baseRes.s, freshSnap, abductionUtils.accWithPerm(g, Some(permH)), pve, baseRes.v) { + (s2, v2) => + abductionUtils.findChunkFromExp(loc, s2, v2, Internal()) { newChunk => + val state = (q.foundState ++ baseRes.foundState) + /*.map { + case (exp@FieldAccessPredicate(loc, _), chunk) => + if (loc == g.loc) (g, newChunk) + else (exp, chunk) + case (exp@PredicateAccessPredicate(loc, _), chunk) => + if (loc == g.loc) (g, newChunk) + else (exp, chunk) + }*/ + val lost = q.lostAccesses ++ baseRes.lostAccesses + Q(Some(AbductionQuestion(s2, v2, g1, lost, state, q.foundStmts , q.trigger, q.stateAllowed))) + } + } + } + + } + }*/ + } + // This means we can't determine what the perms are + // Happens for example with variables + case None => + Q(None) + // This should hopefully never happen? + // Here for debugging + case e => + Q(None) } } } @@ -133,14 +151,16 @@ object AbductionFoldBase extends AbductionRule { case Some(cond) => val g1 = q.goal.filterNot(_ == a) val concCond = cond.transform { case lv: AbstractLocalVar if lv == pred.formalArgs.head.localVar => a.loc.args.head } - safeEval(concCond, q.s, q.v, q.lostAccesses) { + abductionUtils.safeEval(concCond, q.s, q.v, q.lostAccesses) { case (s1, Some(term), v1) => if (v1.decider.check(term, Verifier.config.checkTimeout())) { - safeEval(a.loc.args.head, q.s, q.v, q.lostAccesses) { + abductionUtils.safeEval(a.loc.args.head, q.s, q.v, q.lostAccesses) { case (s2, Some(t), v2) => val wildcards = s2.constrainableARPs -- s1.constrainableARPs // TODO nklose this could branch - predicateSupporter.fold(s1, pred, List(t), None, terms.FullPerm, None, wildcards, pve, v2) { (s3, v3) => + val varTrans = VarTransformer(q.s, q.v, q.s.g.values, q.s.h) + val permToFold = varTrans.permExpToTerm(a.permExp.getOrElse(FullPerm()())) + predicateSupporter.fold(s1, pred, List(t), None, permToFold, None, wildcards, pve, v2) { (s3, v3) => //consumer.consume(s3, a, pve, v3) { (s4, _, v4) => val fold = Fold(a)() Q(Some(q.copy(goal = g1, foundStmts = q.foundStmts :+ fold, s = s3, v = v3))) @@ -175,9 +195,11 @@ object AbductionFold extends AbductionRule { locs match { case Seq() => Q(None) case loc +: rest => - checkChunk(loc, q.s, q.v, q.lostAccesses) { - case Some(chunk) => Q(Some(loc, chunk)) - case None => findFirstFieldChunk(rest, q)(Q) + abductionUtils.checkChunk(loc, q.s, q.v, q.lostAccesses) { + case Some(chunk) => + Q(Some(loc, chunk)) + case None => + findFirstFieldChunk(rest, q)(Q) } } } @@ -187,81 +209,248 @@ object AbductionFold extends AbductionRule { preds match { case None => Q(None) case Some(a: PredicateAccessPredicate) => + if (a.permExp.isEmpty) { + Q(None) + } val g1 = q.goal.filterNot(_ == a) val pred = a.loc.loc(q.s.program) - val fields = pred.body.get.transform { case lc: AbstractLocalVar if pred.formalArgs.head.localVar == lc => a.loc.args.head }.collect { case e: FieldAccessPredicate => e.loc }.toSeq + val fieldsM = predFieldsCache.getOrElseUpdate((pred, a), abductionUtils.fieldsMap(pred, a)) + val fields: Seq[FieldAccess] = fieldsM.keys.toSeq + findFirstFieldChunk(fields, q) { - // If we find a chunk, then we definitely have to fold. So we attempt to and abduce anything else that might be missing. - // TODO nklose if the predicate is conditional in a weird way, then this might be wrong? case Some((field, chunk)) => - val fold = Fold(a)() - executor.exec(q.s, fold, q.v, q.trigger, q.stateAllowed) { (s1, v1) => - val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, chunk.snap.sort)) - val q2 = q.copy(s = s1, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1) - Q(Some(q2)) + val shouldSkipForInvariant = q.s.reservedForInvariants.exists { + case fap: FieldAccessPredicate => + fap.loc.field == field.field && fap.loc.rcv == field.rcv + case _ => false + } + val shouldSkipForFoldUnfold = q.s.reservedForFoldUnfold.lastOption.exists { + case (_, seq) => seq.exists { + case fap: FieldAccessPredicate => + fap.loc.field == field.field && fap.loc.rcv == field.rcv + case _ => false + } + } + + if (shouldSkipForInvariant || shouldSkipForFoldUnfold) { + apply(q.copy(goal = g1)) { + case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal))) + case None => Q(None) + } + } else { + val foldS = q.s.copy(abdPermScalingFactorExp = a.perm) + val fold = Fold(a)() + executionFlowController.tryOrElse0(foldS, q.v) { + (s1, v1, T) => + executor.exec(s1, fold, v1, q.trigger, q.stateAllowed) { (s2, v2) => + T(s2, v2) + } + } { + (s1, v1) => + val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, chunk.snap.sort)) + // If we succeeded a fold we can remove (fold, _) from our stack. + val sFoldSucceeded = s1.copy(abdPermScalingFactorExp = FullPerm()(), + reservedForFoldUnfold = s1.reservedForFoldUnfold filter { + case (exp, _) => exp != fold.acc + }) + // Then, if we folded but we're not done (we're inside a nested fold, for example) we need to reserve + // the thing we just folded so that it does not get unfolded + val s2ReserveForFoldUnfold = if (sFoldSucceeded.reservedForFoldUnfold.nonEmpty) + sFoldSucceeded.copy(reservedForFoldUnfold = + q.s.reservedForFoldUnfold.init :+ (q.s.reservedForFoldUnfold.last._1, q.s.reservedForFoldUnfold.last._2 :+ fold.acc) + ) else sFoldSucceeded + val q2 = q.copy(s = s2ReserveForFoldUnfold, v = v1, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1) + Q(Some(q2)) + } { + // Fold failed + _ => + Q(None) + } } - case None => { - // If we do not find a chunk, we recurse to try the others by calling this + case None => apply(q.copy(goal = g1)) { case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal))) case None => Q(None) } - } + case _ => + Q(None) } + } } - } } object AbductionUnfold extends AbductionRule { - private def checkPredicates(pres: Seq[PredicateAccess], q: AbductionQuestion, goal: FieldAccess)(Q: Option[(PredicateAccess, BasicChunk, Seq[Exp])] => VerificationResult): VerificationResult = { + private def checkUnfoldingWand(q: AbductionQuestion, pred: PredicateAccess)(Q: Boolean => VerificationResult): VerificationResult = { + q.s.packaging match { + case Some(exp: Exp) => + val allPreds = exp.collect { case pap: PredicateAccessPredicate => pap.loc } + .filter(_.predicateName == pred.predicateName) + + if (allPreds.isEmpty) { + Q(false) + } else { + // Check if any predicate contained in the wand is the one we're attempting to unfold + def checkAny(remaining: Seq[PredicateAccess]): VerificationResult = { + remaining match { + case Seq() => + Q(false) + case loc +: rest => + // println(s"\tWill check loc $loc (${loc.args.head} == ${pred.args.head})") + abductionUtils.safeEval(loc.args.head, q.s, q.v, q.lostAccesses) { (s1, t1, v1) => + abductionUtils.safeEval(pred.args.head, s1, v1, q.lostAccesses) { (_, t2, v2) => + (t1, t2) match { + case (Some(t1v), Some(t2v)) if t1v == t2v || v2.decider.check(terms.Equals(t1v, t2v), Verifier.config.checkTimeout()) => + Q(true) + case _ => checkAny(rest) + } + } + } + } + } + checkAny(allPreds.toSeq) + } + case _ => + Q(false) + } + } + + private def checkPredicates(pres: Seq[PredicateAccess], q: AbductionQuestion, goal: FieldAccess) + (Q: Option[(PredicateAccess, BasicChunk, Seq[Exp], Term)] => VerificationResult): VerificationResult = { pres match { case Seq() => Q(None) case pred :: rest => - checkChunk(pred, q.s, q.v, q.lostAccesses) { - case None => checkPredicates(rest, q, goal)(Q) + abductionUtils.checkChunk(pred, q.s, q.v, q.lostAccesses) { + case None => + checkPredicates(rest, q, goal)(Q) case Some(predChunk) => - val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs - val bcsBefore = q.v.decider.pcs.branchConditions - var failedBranches: Seq[silicon.Stack[Term]] = Seq() - var succBranches: Seq[silicon.Stack[Term]] = Seq() - val tryUnfold = predicateSupporter.unfold(q.s, pred.loc(q.s.program), predChunk.args.toList, None, terms.FullPerm, None, wildcards, pve, q.v, pred) { - (s1, v1) => - checkChunk(goal, s1, v1, q.lostAccesses) { - case None => - failedBranches = failedBranches :+ v1.decider.pcs.branchConditions - Failure(pve dueTo DummyReason) - case Some(_) => - succBranches = succBranches :+ v1.decider.pcs.branchConditions - Success() - } + // We need to make sure that we do not unfold stuff that we do not want to + val currPap = PredicateAccessPredicate(pred, Some(q.s.abdPermScalingFactorExp))() + + // Check if this predicate is reserved because we're currently folding it (to avoid infinite unfold/fold loop) + val shouldSkip = q.s.reservedForFoldUnfold.lastOption.exists { + case (_, seq) => seq.exists { + case p: PredicateAccessPredicate => + p.loc == currPap.loc && abductionUtils.asRational(p.permExp) == abductionUtils.asRational(currPap.permExp) + case _ => false + } } - tryUnfold match { - case _: NonFatalResult => Q(Some(pred, predChunk, Seq())) - case _: FatalResult => - succBranches match { - case Seq() => checkPredicates(rest, q, goal)(Q) - case Seq(branch) => - val condTerms = branch.distinct.filterNot(bcsBefore.contains) - val varTran = VarTransformer(q.s, q.v, q.s.g.values, q.s.h) - val conds = condTerms.map(varTran.transformTerm(_).get) - Q(Some(pred, predChunk, conds)) - case _ => checkPredicates(rest, q, goal)(Q) // Multiple succ branches would require a disjunction. Left out for now - } + // Check if this predicate is part of a loop invariant we're trying to preserve — unfolding it would break the invariant + val shouldSkipInvariant = q.s.reservedForInvariants.exists { + case p: PredicateAccessPredicate => + p.loc == currPap.loc && abductionUtils.asRational(p.permExp) == abductionUtils.asRational(currPap.permExp) + case _ => false + } + // This is a bit more involved: if the trigger of our abduction is ``fold pred(x)`` then we do NOT want + // to unfold ``pred(x)``, no matter what the goal is. This issue arises when we could theoretically + // hold multiple instances of a predicate (e.g. because one field apears with 1/2) but already hold one (or more) + val shouldSkipSamePred = q.trigger match { + case Some(fold: Fold) => fold.acc.loc == currPap.loc + case _ => false + } + + if (shouldSkip || shouldSkipInvariant || shouldSkipSamePred) { + // println(s"AbdUnfold -- Skipping $currPap to avoid re-unfolding${if (shouldSkipInvariant) " (invariant)" else if (shouldSkipSamePred) " same predicate" else ""}") + Q(None) + } else { + // We do not ever want to unfold the LHS of a wand when we're trying to infer the RHS + // We also do not want to unfold any fraction of the RHS that might already be in the state + checkUnfoldingWand(q, pred) { + case true => + Q(None) + case false => + val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs + val bcsBefore = q.v.decider.pcs.branchConditions + var failedBranches: Seq[silicon.Stack[Term]] = Seq() + var succBranches: Seq[silicon.Stack[Term]] = Seq() + + // This is outdated, here for completeness, we now unfold all we have and check that we made progress + // + // val pH = varTrans.transformTerm(predChunk.perm) + // val pGExp = varTrans.transformTerm(pG) + // if we are here, it means that there are no permissions to the goal on the heap + // (otherwise the base rule would have applied) + // this means that to check of many permissions to the (goal) field there are in + // the predicate body, we can unfold it and check, then discard the vUnfolded state + // permsTo(goal, sUnfolded, vUnfolded, q.lostAccesses) { pField => + /*val p: terms.Term = pGExp match { + case Some(_: WildcardPerm) => + predChunk.perm + case _ => + val pTemp = abductionUtils.asRational(pGExp.getOrElse(FullPerm()())) / + (abductionUtils.asRational(pH.getOrElse(FullPerm()())) * abductionUtils.asRational(pField.getOrElse(FullPerm()()))) + varTrans.permExpToTerm(abductionUtils.asPerm(abductionUtils.permMin( + abductionUtils.asPerm(pTemp), + pH.getOrElse(FullPerm()()))), q.v).getOrElse(terms.FullPerm) + }*/ + val tryUnfold = predicateSupporter.unfold(q.s, pred.loc(q.s.program), predChunk.args.toList, None, predChunk.perm, None, wildcards, pve, q.v, pred) { + (s1, v1) => + def fail() = { + failedBranches = failedBranches :+ v1.decider.pcs.branchConditions + Failure(pve dueTo DummyReason) + } + + abductionUtils.permsTo(goal, q.s, q.v, q.lostAccesses) { + case None => + fail() + case prevPerm => + abductionUtils.permsTo(goal, s1, v1, q.lostAccesses) { + case None => + fail() + case currPerm => + if (abductionUtils.asRational(currPerm) > abductionUtils.asRational(prevPerm) + // && (abductionUtils.asRational(prevPerm) < Rational(1, 1)) + ) { + succBranches = succBranches :+ v1.decider.pcs.branchConditions + Success() + } + else { + fail() + } + } + } + } + // We must make sure we try to match chunks to their value in the store + // Otherwise if we for example unfold nodes(curr) to get ocurr.next.prev because we know + // ocurr.next == curr then we should try to use cur, and not ocurr.next + // Otherwise, if we do not hold permissions to ocurr.next, unfolding will fail + val newPred = q.s.g.values.collectFirst { + case (localVar, (term, _)) if term == predChunk.args.head => localVar + } match { + case Some(localVar) => pred.copy(args = Seq(localVar))(pred.pos, pred.info, pred.errT) + case None => pred + } + tryUnfold match { + case _: NonFatalResult => + Q(Some(newPred, predChunk, Seq(), predChunk.perm)) + case _: FatalResult => + succBranches match { + case Seq() => checkPredicates(rest, q, goal)(Q) + case Seq(branch) => + val condTerms = branch.distinct.filterNot(bcsBefore.contains) + val varTran = VarTransformer(q.s, q.v, q.s.g.values, q.s.h) + val conds = condTerms.map(varTran.transformTerm(_).get) + Q(Some(newPred, predChunk, conds, predChunk.perm)) + case _ => checkPredicates(rest, q, goal)(Q) // Multiple succ branches would require a disjunction. Left out for now + } + } + } } } } } override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = { + val acc = q.goal.collectFirst { case e: FieldAccessPredicate => e } acc match { case None => Q(None) case Some(a: FieldAccessPredicate) => + /*if (a.permExp.isEmpty) { + Q(None) + }*/ val g1 = q.goal.filterNot(a == _) - - // If we fail for a, then we recurse and try for other fields val R = () => apply(q.copy(goal = g1)) { case Some(q2) => Q(Some(q2.copy(goal = a +: q2.goal))) @@ -270,13 +459,17 @@ object AbductionUnfold extends AbductionRule { val preds = abductionUtils.getContainingPredicates(a.loc, q.s.program).filter(abductionUtils.isValidPredicate) val predAccs = preds.map { pred => PredicateAccess(Seq(a.loc.rcv), pred)(NoPosition, NoInfo, NoTrafos) } + // val varTrans = VarTransformer(q.s, q.v, q.s.g.values, q.s.h) + // val pG = varTrans.permExpToTerm(a.permExp.getOrElse(FullPerm()()), q.v).getOrElse(terms.FullPerm) checkPredicates(predAccs, q, a.loc) { case None => R() - case Some((pred, predChunk, conds)) => + case Some((pred, predChunk, conds, p)) => produces(q.s, freshSnap, conds, _ => pve, q.v)((s1, v1) => { val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs - predicateSupporter.unfold(s1, pred.loc(q.s.program), predChunk.args.toList, None, terms.FullPerm, None, wildcards, pve, v1, pred) { (s2, v2) => - Q(Some(q.copy(s = s2, v = v2, foundStmts = q.foundStmts :+ Unfold(PredicateAccessPredicate(pred, Some(FullPerm()()))())(), foundState = q.foundState ++ conds.map(c => c -> None)))) + predicateSupporter.unfold(s1, pred.loc(q.s.program), predChunk.args.toList, None, p, None, wildcards, pve, v1, pred) { (s2, v2) => + val varTrans2 = VarTransformer(s2, v2, s2.g.values, s2.h) + Q(Some(q.copy(s = s2, v = v2, foundStmts = q.foundStmts :+ Unfold(PredicateAccessPredicate(pred, varTrans2.transformTerm(p))())(), + foundState = q.foundState ++ conds.map(c => c -> None)))) } }) } @@ -290,46 +483,61 @@ object AbductionApply extends AbductionRule { q.goal.headOption match { case None => Q(None) case Some(g) => - val goalWand = MagicWand(TrueLit()(), g)() - val goalStructure = goalWand.structure(q.s.program) + val goalWand = abductionUtils.transformWithAliasing(MagicWand(TrueLit()(), g)(), q).asInstanceOf[MagicWand] + val goalStructure = abductionUtils.correctStructure(goalWand.structure(q.s.program)) // We drop the first element, because it is the true lit of the lhs val subexps = goalWand.subexpressionsToEvaluate(q.s.program).tail + // val varTran = VarTransformer(q.s, q.v, q.s.g.values, q.s.h) + // val aliasedWand = abductionUtils.transformWithAliasing(goalWand, q) // If the args of the magic wand chunk match the evaluated subexpressions, then the right hand of the magic wand // chunk is our goal, so the rule can be applied evals(q.s, subexps, _ => pve, q.v)((s1, args, _, v1) => { + val varTrans1 = VarTransformer(s1, v1, s1.g.values, s1.h) val matchingWand = s1.h.values.collect { // If the wand in the state contains our goal in the right-hand-side, then we would like to apply the wand - case m: MagicWandChunk if m.id.ghostFreeWand.structure(s1.program).right.contains(goalStructure.right) && m.args.takeRight(args.length) == args => + case m: MagicWandChunk if abductionUtils.correctStructure(m.id.ghostFreeWand.structure(s1.program)).right.contains(goalStructure.right) + // Here we need to: + // - Check for aliasing + // - Remove all permission values + && m.args.takeRight(args.length).filter(!_.isInstanceOf[Permissions]).map(varTrans1.transformTerm) + == args.filter(!_.isInstanceOf[Permissions]).map(varTrans1.transformTerm) => // If we find a matching wand, we have to find an expression representing the left hand side of the wand val lhsTerms = m.args.dropRight(args.length) - val varTransformer = VarTransformer(s1, v1, s1.g.values, s1.h) - val lhsArgs = lhsTerms.map(t => varTransformer.transformTerm(t)) + val lhsArgs = lhsTerms.map(varTrans1.transformTerm) if (lhsArgs.contains(None)) { None } else { val formalLhsArgs = m.id.ghostFreeWand.subexpressionsToEvaluate(s1.program).dropRight(args.length) val wand = m.id.ghostFreeWand.transform { + // TODO: The assumption (see comment) might not hold for fractional permissions case n if formalLhsArgs.contains(n) => lhsArgs(formalLhsArgs.indexOf(n)).get // I am assuming that the subexpressions are unique, which should hold } Some(wand) } + case m: MagicWandChunk => + None }.collectFirst { case c if c.isDefined => c.get } matchingWand match { case Some(wand) => val q1 = q.copy(goal = Seq(wand.left)) + // We can't apply a wand that has the same term on the LHS and RHS + if (wand.left == wand.right) { + Q(None) + } AbductionApplier.applyRules(q1) { lhsRes => - if (lhsRes.goal.nonEmpty) { Q(None) } else { magicWandSupporter.applyWand(lhsRes.s, wand, pve, lhsRes.v) { (s2, v2) => val g1 = q.goal.filterNot(_ == wand.right) - val stmts: Seq[Stmt] = ((q.foundStmts :+ Apply(wand)()) ++ lhsRes.foundStmts ).distinct // TODO there is a weird duplication here sometimes + // FIXME: I [Amos] had to remove the distinct (see TODO), because if we end up with two identical fractions + // we might want to keep both + val stmts: Seq[Stmt] = ((q.foundStmts :+ Apply(wand)()) ++ lhsRes.foundStmts)//.distinct // TODO there is a weird duplication here sometimes val state = q.foundState ++ lhsRes.foundState val lost = q.lostAccesses ++ lhsRes.lostAccesses Q(Some(AbductionQuestion(s2, v2, g1, lost, state, stmts, q.trigger, q.stateAllowed))) } - } + } } case None => @@ -347,67 +555,118 @@ object AbductionApply extends AbductionRule { // TODO nklose this should actually do a package after simulating it. Then we do not have issues with the correct state at the end object AbductionPackage extends AbductionRule { + private def assertLHS(s: State, v: Verifier, wand: MagicWand, q: AbductionQuestion) + (Q: (State, Verifier) => VerificationResult): VerificationResult = { + executionFlowController.tryOrElse0(s, v) { (s1, v1, T) => + executor.exec(s1, Assert(wand.left)(), v1) { (s2, v2) => + T(s2, v2) + } + } { + (s1a, v1a) => Q(s1a, v1a) + } { + f => + f.message.reason match { + // In case we fail to abductively asser the LHS because of an assertion, we try to simply produce it + // and reattempt the fold + case AssertionFalse(assertion) => + producer.produce(s, freshSnap, assertion, pve, v) { (s1r, v1r) => + assertLHS(s1r, v1r, wand, q)(Q) + } + case _ => + f + } + } + } + override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = { q.goal.collectFirst { case a: MagicWand => a } match { case None => Q(None) case Some(wand) => - executionFlowController.locally(q.s, q.v) { (s0, v0) => - - // TODO This may produce things that are already in the state - producer.produce(s0, freshSnap, wand.left, pve, v0) { (s1, v1) => - val packQ = q.copy(s = s1, v = v1, goal = wand.right.topLevelConjuncts) - AbductionApplier.applyRules(packQ) { packRes => - if (packRes.goal.nonEmpty) { - Failure(pve dueTo (DummyReason)) - } else { - val newState = packRes.foundState - val newStmts = packRes.foundStmts - Success(Some(AbductionSuccess(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate(), newState, newStmts, Map(), Seq(), None))) + // We need to "remember" that we are packaging a wand, so we will not try to unfold + // predicates that are part of the RHS when inferring the LHS and vice-versa + val sReservedWand = q.s.copy(packaging = Some(wand)) + executionFlowController.locally(sReservedWand, q.v) { (s1, v1) => + assertLHS(s1, v1, wand, q) { (s2, v2) => + // We need to make sure we do not try producing a value constraint when inferring the RHS + val packQ = q.copy(s = s2, v = v2, goal = wand.right.topLevelConjuncts) + AbductionApplier.applyRules(packQ) { packRes => + if (packRes.goal.nonEmpty) { + Failure(pve dueTo DummyReason) + } else { + val newState = packRes.foundState + val newStmts = packRes.foundStmts + // Small hack: To flag these results to keep, we use a TrueLit as trigger (it will never be an actual trigger) + // .copy(produceableAssertions = s2.produceableAssertions) + Success(Some(AbductionSuccess(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate(), newState, newStmts, Map(), Seq(), Some(TrueLit()())))) + } } } - } - } match { - case _: FatalResult => Q(None) - case suc: NonFatalResult => - - val abdRes = abductionUtils.getAbductionSuccesses(suc) - val stmts = abdRes.flatMap(_.stmts).reverse - val state = abdRes.flatMap(_.state).reverse - - - - produces(q.s, freshSnap, state.map(_._1), _ => pve, q.v) { (s1, v1) => - val locs: Seq[LocationAccess] = state.map { - case (p: FieldAccessPredicate, _) => p.loc - case (p: PredicateAccessPredicate, _) => p.loc - } - abductionUtils.findChunks(locs, s1, v1, Internal()) { newChunks => - - val newOldHeaps = s1.oldHeaps.map{ case (s, h) => (s, h + Heap(newChunks.keys))} - val sPack = s1.copy(oldHeaps = newOldHeaps) - - // TODO the script needs to be self-framing (so field accesses need to be resolved to vars) - val script = Seqn(stmts, Seq())() - val tran = VarTransformer(sPack, v1, sPack.g.values, sPack.h) - script.transform{ - case e: FieldAccess => - val lv = tran.transformExp(e, strict = false) - lv.get + } match { + case fail: FatalResult => + Q(None) + case suc: NonFatalResult => + val abdRes = abductionUtils.getAbductionSuccesses(suc) + // We need to filter out those abdRes that come from asserting the LHS of the wand + // And then pick a branch to keep if there are multiples that are all correct + val picked = abductionUtils.pickBranch(abdRes).filter(res => res.trigger != Some(Assert(wand.left)())) + // We also need to filter out those statements that are a biproduct of assuming the LHS of the wand + val truelit = abductionUtils.pickBranch(abdRes).filter( res => res.trigger match { + case Some(TrueLit()) => true + case _ => false + }) + val stmts = truelit.flatMap(_.stmts).reverse + val state = picked.flatMap(_.state).reverse + val assertions = picked.flatMap(_.assertions) + // val produceableAssertions = abdRes.flatMap(res => res.s.produceableAssertions).distinct + // .copy(produceableAssertions = produceableAssertions) + produces(sReservedWand, freshSnap, state.map(_._1) ++ assertions, _ => pve, q.v) { (s1, v1) => + val locs: Seq[LocationAccess] = state.map { + case (p: FieldAccessPredicate, _) => p.loc + case (p: PredicateAccessPredicate, _) => p.loc } - - magicWandSupporter.packageWand(sPack, wand, script, pve, v1) { - (s2, wandChunk, v2) => - val g1 = q.goal.filterNot(_ == wand) - val finalStmts = q.foundStmts :+ Package(wand, script)() - val finalState = q.foundState ++ state - //val lost = q.lostAccesses ++ packRes.lostAccesses - Q(Some(q.copy(s = s2.copy(h = s2.reserveHeaps.head.+(wandChunk)), v = v2, goal = g1, foundStmts = finalStmts, foundState = finalState))) + abductionUtils.findChunks(locs, s1, v1, Internal()) { newChunks => + val newOldHeaps = s1.oldHeaps.map { case (s, h) => (s, h + Heap(newChunks.keys)) } + val sPack = s1.copy(oldHeaps = newOldHeaps) + // TODO the script needs to be self-framing (so field accesses need to be resolved to vars) + val script = Seqn(stmts, Seq())() + val tran = VarTransformer(sPack, v1, sPack.g.values, sPack.h) + script.transform { + case e: FieldAccess => + val lv = tran.transformExp(e, strict = false) + lv.get + } + val aliasedWand = abductionUtils.transformWithAliasing(wand, q).asInstanceOf[MagicWand] + // Because we produce asssertions when packaging the wand, it might happen that we fail to package + // the wand because the assertion does not hold. In that case, we fail + executionFlowController.tryOrElse1[Chunk](sPack, v1) { + (sT, vT, T) => + magicWandSupporter.packageWand(sT, aliasedWand, script, pve, vT)(T) + } { + (s2, wandChunk, v2) => + val g1 = q.goal.filterNot(_ == wand) + val finalStmts = q.foundStmts :+ Package(aliasedWand, script)() + val finalState = q.foundState ++ state + Q(Some(q.copy(s = s2.copy(h = s2.reserveHeaps.head.+(wandChunk), packaging = None) + , v = v2, goal = g1, foundStmts = finalStmts, foundState = finalState))) + } { + f => + Q(None) + } + // Legacy code, here for completeness + /*magicWandSupporter.packageWand(sPack, aliasedWand, script, pve, v1) { + (s2, wandChunk, v2) => + val g1 = q.goal.filterNot(_ == wand) + val finalStmts = q.foundStmts :+ Package(aliasedWand, script)() + val finalState = q.foundState ++ state + // println(s"AbdPackage -- Packaged wand from ${sPack.h.values.mkString("\n\t")} to \n\t${s2.reserveHeaps.head.+(wandChunk).values.mkString("\n\t")}") + Q(Some(q.copy(s = s2.copy(h = s2.reserveHeaps.head.+(wandChunk), packaging = None) + , v = v2, goal = g1, foundStmts = finalStmts, foundState = finalState))) + }*/ } } - } + } } } - } } /** @@ -421,19 +680,35 @@ object AbductionMissing extends AbductionRule { case e: FieldAccessPredicate => e case e: PredicateAccessPredicate => e } + if (!q.stateAllowed || accs.isEmpty) { Q(None) } else { val g1 = q.goal.filterNot(accs.contains) - producer.produces(q.s, freshSnap, accs, _ => pve, q.v) { (s1, v1) => - val locs: Map[LocationAccess, Exp] = accs.map { p => p.loc -> p }.toMap - abductionUtils.findChunks(locs.keys.toSeq, s1, v1, Internal()) { newChunks => - - val newOldHeaps = s1.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks.keys)) } - val s2 = s1.copy(oldHeaps = newOldHeaps) - - val newState = newChunks.map { case (c, loc) => (locs(loc), Some(c)) } - Q(Some(q.copy(s = s2, v = v1, goal = g1, foundState = q.foundState ++ newState))) + abductionUtils.concretizeAccs(accs, q) { cAccs => + /*val scaledCAccs = cAccs.map { + case fa: FieldAccessPredicate => + FieldAccessPredicate(fa.loc, Some(PermMul(fa.permExp.getOrElse(FullPerm()()), q.s.abdPermScalingFactorExp)()))() + case pa: PredicateAccessPredicate => + PredicateAccessPredicate(pa.loc, Some(PermMul(pa.permExp.getOrElse(FullPerm()()), q.s.abdPermScalingFactorExp)()))() + }*/ + producer.produces(q.s, freshSnap, cAccs, _ => pve, q.v) { (s1, v1) => + val locs: Map[LocationAccess, Exp] = cAccs.map { p => p.loc.asInstanceOf[LocationAccess] -> p }.toMap + abductionUtils.findChunks(locs.keys.toSeq, s1, v1, Internal()) { newChunks => + val newOldHeaps = s1.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks.keys)) } + val s2 = s1.copy(oldHeaps = newOldHeaps) + + val newState = + newChunks.flatMap { + case (c, loc) => + locs.get(loc).map(l => (l, Some(c))) + } + val s2ReserveForFoldUnfold = if (s2.reservedForFoldUnfold.nonEmpty) + s2.copy(reservedForFoldUnfold = + q.s.reservedForFoldUnfold.init :+ (q.s.reservedForFoldUnfold.last._1, q.s.reservedForFoldUnfold.last._2 ++ accs) + ) else s2 + Q(Some(q.copy(s = s2ReserveForFoldUnfold, v = v1, goal = g1, foundState = q.foundState ++ newState))) + } } } } diff --git a/src/main/scala/biabduction/Abstraction.scala b/src/main/scala/biabduction/Abstraction.scala index 8604a27dc..be3edf24c 100644 --- a/src/main/scala/biabduction/Abstraction.scala +++ b/src/main/scala/biabduction/Abstraction.scala @@ -1,12 +1,19 @@ package viper.silicon.biabduction -import viper.silicon.interfaces.VerificationResult +import viper.silicon.interfaces.{Failure, Success, VerificationResult} import viper.silicon.interfaces.state.Chunk -import viper.silicon.resources._ +import viper.silicon.resources.FieldID import viper.silicon.rules._ import viper.silicon.state._ +import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ +import viper.silver.utility.Common.Rational +import viper.silver.verifier.PartialVerificationError +import viper.silver.verifier.errors.Internal +import viper.silver.verifier.reasons.InsufficientPermission + +import scala.collection.mutable object AbstractionApplier extends RuleApplier[AbstractionQuestion] { override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply) @@ -14,13 +21,17 @@ object AbstractionApplier extends RuleApplier[AbstractionQuestion] { case class AbstractionQuestion(s: State, v: Verifier) { - def varTran: VarTransformer = VarTransformer(s, v, s.g.values, s.h) + val pve: PartialVerificationError = Internal() + val predPermMap = abductionUtils.buildPredicatePermissionsMap(s, v) + def varTran: VarTransformer = VarTransformer(s, v, s.g.values, s.h) } -trait AbstractionRule extends BiAbductionRule[AbstractionQuestion] +trait AbstractionRule extends BiAbductionRule[AbstractionQuestion] {} object AbstractionFold extends AbstractionRule { + + private val wildcardPredicates: mutable.Set[Predicate] = mutable.Set.empty[Predicate] // TODO we assume each field only appears in at most one predicate private def getFieldPredicate(bc: BasicChunk, q: AbstractionQuestion): Option[Predicate] = { @@ -32,31 +43,139 @@ object AbstractionFold extends AbstractionRule { } private def checkChunks(chunks: Seq[(BasicChunk, Predicate)], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { + + def retryFold(fold: Fold, currentQ: AbstractionQuestion, previousFailure: Failure, rest: Seq[(BasicChunk, Predicate)]): VerificationResult = { + val reason = previousFailure.message.reason match { + case reason: InsufficientPermission => + val perm = previousFailure.message.offendingNode match { + case _: Fold => Some(PermMul(currentQ.s.abdPermScalingFactorExp, reason.permExp.getOrElse(FullPerm()()))()) + case _ => reason.permExp + } + val acc = reason.offendingNode match { + case n: FieldAccess => Some(FieldAccessPredicate(n, perm)()) + case n: PredicateAccess => Some(PredicateAccessPredicate(n, perm)()) + case _ => None + } + acc + case _ => None + } + reason match { + // We ONLY want to reattempt fold if we're missing a field + // TODO: This should NOT be a field of a recursive predicate + case Some(acc: FieldAccessPredicate) => + abductionUtils.permsTo(acc.loc, currentQ.s, currentQ.v, Map.empty) { + // We only reattempt the fold if we have some permissions to the other field + case Some(_: NoPerm) => + checkChunks(rest, q)(Q) + case permH@Some(p) => + val newPerm = abductionUtils.clampSubPerm(acc.permExp, permH) + val toProd = abductionUtils.accWithPerm(acc, Some(newPerm)) + producer.produce(currentQ.s, freshSnap, toProd, pve, currentQ.v) { (s1p, v1p) => + executionFlowController.tryOrElse0(s1p, v1p) { + (s1, v1, T) => + val permToFold = fold.acc.permExp.getOrElse(FullPerm()()) + executor.exec(s1.copy(abdPermScalingFactorExp = permToFold), fold, v1, None, abdStateAllowed = false)((s1a, v1a) => { + T(s1a, v1a) + }) + } { + (s2, v2) => + val sFoldSucceeded = s2.copy( + abdPermScalingFactorExp = FullPerm()(), + reservedForFoldUnfold = s2.reservedForFoldUnfold filter { + case (exp, _) => exp != fold.acc + }) + Q(Some(currentQ.copy(s = sFoldSucceeded, v = v2))) + } { + f2 => retryFold(fold, currentQ.copy(s = s1p, v = v1p), f2, rest) + } + } + case _ => + checkChunks(rest, q)(Q) + } + case _ => + // Failure was not due to insufficient permissions to a field, give up and check rest + checkChunks(rest, q)(Q) + } + } + chunks match { - case _ if chunks.isEmpty => Q(None) + case _ if chunks.isEmpty => + Q(None) case (chunk, pred) +: rest => q.varTran.transformTerm(chunk.args.head) match { case None => checkChunks(rest, q)(Q) case Some(eArgs) => - + // Here we need to do a bit of magic to check for the permissions that any given + // predicate would give us on the field + val (accLoc, accPerm) = q.varTran.transformChunk(chunk) match { + case Some(FieldAccessPredicate(loc, p)) => (loc, p) + case Some(PredicateAccessPredicate(loc, p)) => (loc, p) + } + val pField = pred.body.get.collectFirst { + case fap: FieldAccessPredicate if (accLoc match { + case FieldAccess(_, field) => fap.loc.field == field + case _ => false + }) => fap.loc + } match { + case None => FullPerm()() + case Some(loc) => q.predPermMap(pred)(loc.field) + } + val permToFold = accPerm match { + case Some(WildcardPerm()) => WildcardPerm()() + case _ => abductionUtils.minPerm( + abductionUtils.simplifyPermission(PermPermDiv(accPerm.getOrElse(FullPerm()()), pField)()), + FullPerm()(), q.v, q.varTran) + } + val fold = Fold(PredicateAccessPredicate(PredicateAccess(Seq(eArgs), pred.name)(), Some(permToFold))())() executionFlowController.tryOrElse0(q.s, q.v) { (s1, v1, T) => - val fold = Fold(PredicateAccessPredicate(PredicateAccess(Seq(eArgs), pred.name)(), Some(FullPerm()()))())() - executor.exec(s1, fold, v1, None, abdStateAllowed = false)((s1a, v1a) => + executor.exec(s1.copy(abdPermScalingFactorExp = permToFold), fold, v1, None, abdStateAllowed = false)((s1a, v1a) => { T(s1a, v1a) + } ) + } { - (s2, v2) => Q(Some(q.copy(s = s2, v = v2))) + (s2, v2) => + // If we succeeded a fold we can remove (fold, _) from our stack. + // Ideally it will always be at the top of the stack, but I am not 100% sure so I filter, + // better safe than sorry + val sFoldSucceeded = s2.copy( + abdPermScalingFactorExp = FullPerm()(), + reservedForFoldUnfold = s2.reservedForFoldUnfold filter { + case (exp, _) => exp != fold.acc + }) + Q(Some(q.copy(s = sFoldSucceeded, v = v2))) } { f => - checkChunks(rest, q)(Q) + // The idea here is, before checking other chunks, if we failed to fold because of + // insufficient permissions to another field, and we have a smaller fraction fo this field, then + // we can just add the field and keep going + // If we have acc(x.next, 1/1) && acc(x.data, 1/4), then it just means that x.data was never accesses + // for write permissions BUT we can just over-approximate and add them + + // checkChunks(rest, q)(Q) + retryFold(fold, q.copy(s = q.s.copy(abdPermScalingFactorExp = permToFold)), f, rest) } } } } override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - val candChunks = q.s.h.values.collect { case bc: BasicChunk => (bc, getFieldPredicate(bc, q)) }.collect { case (c, Some(pred)) => (c, pred) }.toSeq + //val candChunks = q.s.h.values.collect { case bc: BasicChunk => (bc, getFieldPredicate(bc, q)) }.collect { case (c, Some(pred)) => (c, pred) }.toSeq + val candChunks = q.s.h.values + .collect { case bc: BasicChunk => (bc, getFieldPredicate(bc, q)) } + .collect { case (c, Some(pred)) => (c, pred) } + .toSeq + // We need to sort the chunks from biggest to smallest (in term of permissions) because otherwise if we have + // x.next -> 1/4 and x.data -> 1/1, and we check first x.next, we will end up with + // list(x, 1/4) and x.data -> 3/4 and retryFold will fail + .sortWith { case ((c1, _), (c2, _)) => + q.v.decider.check( + terms.Greater(c1.perm, c2.perm), + Verifier.config.checkTimeout() + ) + } + checkChunks(candChunks, q)(Q) } } @@ -72,7 +191,6 @@ object AbstractionPackage extends AbstractionRule { q.s.g.termValues.collectFirst { case (lv, term) if term.sort == bc.snap.sort && q.v.decider.check(terms.Equals(term, bc.snap), Verifier.config.checkTimeout()) => lv } match { case None => Q(None) case Some(lhsArgExp) => - // Now we check whether the predicate contains a predicate call on the field val field = abductionUtils.getField(bc.id, q.s.program) // TODO we assume each field only appears in at most one predicate @@ -80,21 +198,32 @@ object AbstractionPackage extends AbstractionRule { case None => Q(None) case Some(pred) => pred.collectFirst { - case recPred@PredicateAccess(Seq(FieldAccess(_, field2)), _) if field == field2 => recPred + case recPred@PredicateAccess(Seq(fa@FieldAccess(_, field2)), _) if field == field2 => (fa, recPred) } match { case None => Q(None) - case Some(recPred) => - val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArgExp), recPred.predicateName)(NoPosition, NoInfo, NoTrafos), Some(FullPerm()()))() + case Some((fa, recPred)) => + val lhsLoc = PredicateAccess(Seq(lhsArgExp), recPred.predicateName)(NoPosition, NoInfo, NoTrafos) // We only want to create the wand if the inner predicate is not present in the current state. - abductionUtils.findChunkFromExp(lhs.loc, q.s, q.v, pve) { - case Some(_) => Q(None) + abductionUtils.findChunkFromExp(lhsLoc, q.s, q.v, pve) { + case Some(_) => + Q(None) case None => q.varTran.transformTerm(bc.args.head) match { case None => Q(None) case Some(rhsArg) => - val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), Some(FullPerm()()))() - Q(Some(MagicWand(lhs, rhs)())) + val rhsLoc = PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos) + val pH = q.varTran.transformTerm(bc.perm).getOrElse(FullPerm()()) + val pF = q.predPermMap(pred)(fa.field) + val pP = q.predPermMap(pred)(recPred.predicateName) + val factor = PermPermDiv(pH, pF)() + val lhsPerm = abductionUtils.simplifyPermission(PermMul(pP, factor)()) + val rhsPerm = abductionUtils.simplifyPermission(factor) + val lhs = PredicateAccessPredicate(lhsLoc, Some(lhsPerm))() + val rhs = PredicateAccessPredicate(rhsLoc, Some(rhsPerm))() + val wand = MagicWand(lhs, rhs)() + Q(Some(wand)) + } } } @@ -115,14 +244,27 @@ object AbstractionPackage extends AbstractionRule { } override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - findWand(q.s.h.values.toSeq, q) { - case None => Q(None) - case Some(wand) => - executor.exec(q.s, Assert(wand)(), q.v) { + // case None => Q(None) + case Some(wand) => + // Asserting the wand might fail: The fact that we can attempt packaging it does nto imply that packaging + // it will succees + executionFlowController.tryOrElse0(q.s, q.v) { (s1, v1, T) => + executor.exec(s1, Assert(wand)(), v1) { (s2, v2) => + T(s2, v2) + } + } { + (s1a, v1a) => + Q(Some(q.copy(s = s1a, v = v1a))) + } { + f => + Q(None) + } + /*executor.exec(q.s, Assert(wand)(), q.v) { (s1, v1) => Q(Some(q.copy(s = s1, v = v1))) - } + }*/ + case _ => Q(None) } } } @@ -132,12 +274,13 @@ object AbstractionJoin extends AbstractionRule { override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect { case Some(wand: MagicWand) => wand }.toSeq val pairs = wands.combinations(2).toSeq + pairs.collectFirst { - case wands if wands(0).right == wands(1).left => (wands(0), wands(1)) - case wands if wands(1).right == wands(0).left => (wands(1), wands(0)) + case wands if abductionUtils.expMatchWithPermissions(wands(0).right, wands(1).left, q.v, q.varTran) => (wands(0), wands(1)) + case wands if abductionUtils.expMatchWithPermissions(wands(1).right, wands(0).left, q.v, q.varTran) => (wands(1), wands(0)) } match { case None => Q(None) - case (Some((w1, w2))) => + case Some((w1, w2)) => magicWandSupporter.packageWand(q.s, MagicWand(w1.left, w2.right)(), Seqn(Seq(Apply(w1)(), Apply(w2)()), Seq())(), pve, q.v) { (s1, wandChunk, v1) => Q(Some(q.copy(s = s1.copy(h = s1.reserveHeaps.head.+(wandChunk)), v = v1))) @@ -151,8 +294,9 @@ object AbstractionApply extends AbstractionRule { override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { val wands = q.s.h.values.collect { case wand: MagicWandChunk => q.varTran.transformChunk(wand) }.collect { case Some(wand: MagicWand) => wand } val targets = q.s.h.values.collect { case c: BasicChunk => q.varTran.transformChunk(c) }.collect { case Some(exp) => exp }.toSeq - - wands.collectFirst { case wand if targets.contains(wand.left) => wand } match { + wands.collectFirst { + case wand if targets.exists(target => abductionUtils.expMatchWithPermissions(wand.left, target, q.v, q.varTran)) => wand + } match { case None => Q(None) case Some(wand) => magicWandSupporter.applyWand(q.s, wand, pve, q.v) { diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index b18bea16f..bde461bc3 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -1,17 +1,23 @@ package viper.silicon.biabduction +import viper.silicon +import viper.silicon.biabduction.abductionUtils.pve import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces._ -import viper.silicon.rules.chunkSupporter.findChunk +import viper.silicon.interfaces.state.Chunk +import viper.silicon.rules.chunkSupporter.{findChunk, findChunksWithID} import viper.silicon.rules.consumer.consumes -import viper.silicon.rules.{evaluator, executionFlowController} +import viper.silicon.rules.evaluator.eval +import viper.silicon.rules.{evaluator, executionFlowController, executor, producer} import viper.silicon.state._ import viper.silicon.state.terms.{Term, True} import viper.silicon.utils.ast.{BigAnd, BigOr} +import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ -import viper.silver.verifier.errors.Internal -import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotFound} +import viper.silver.utility.Common.Rational +import viper.silver.verifier.errors.{Internal, LoopInvariantNotPreserved} +import viper.silver.verifier.reasons.{AssertionFalse, InsufficientPermission, MagicWandChunkNotFound} import viper.silver.verifier.{DummyReason, PartialVerificationError, VerificationError} import scala.annotation.tailrec @@ -27,10 +33,10 @@ trait BiAbductionSuccess extends BiAbductionResult // TODO nklose BiAbductionSuccess should be able to provide arbitrary transformations of methods. Then we can just // use this for all cases and need less dummy stuff -case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[(Exp, Option[BasicChunk])] = Seq(), stmts: Seq[Stmt] = Seq(), newFieldChunks: Map[BasicChunk, LocationAccess], allNewChunks: Seq[BasicChunk], trigger: Option[Positioned] = None) extends BiAbductionSuccess { +case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[(Exp, Option[BasicChunk])] = Seq(), stmts: Seq[Stmt] = Seq(), newFieldChunks: Map[BasicChunk, LocationAccess], allNewChunks: Seq[BasicChunk], trigger: Option[Positioned] = None, assertions: Seq[Exp] = Seq.empty) extends BiAbductionSuccess { override def toString: String = { - "Abduced pres " + state.length + ", Abduced statements " + stmts.length + s"Abduced ${state.length} pres: $state triggered by ${trigger.getOrElse("{}")},\n\tAbduced ${stmts.length} statements $stmts,\n\tAbduced ${assertions.length} assertions $assertions" } def getBcExps(bcsTerms: Seq[Term]): Seq[Option[Exp]] = { @@ -38,21 +44,23 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat v.decider.setPcs(pcs) - //val varTrans = VarTransformer(s, v, s.g.values, s.h) + //val varTran = VarTransformer(s, v, s.g.values, s.h) //val preExps = bcExps.map { // case Some(t) => preTrans.transformExp(t, strict = false) // case None => None //} - // If we can express as in vars, then we want to val ins = s.currentMember.get.asInstanceOf[Method].formalArgs.map(_.localVar) val preVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) } val otherVars: Map[AbstractLocalVar, (Term, Option[Exp])] = s.g.values - val varTrans = VarTransformer(s, v, preVars, s.h, otherVars = otherVars) - val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) } - + val varTran = VarTransformer(s, v, preVars, s.h, otherVars = otherVars) + val bcExps = bcsTerms.map { t => + val t1 = varTran.transformTerm(t) + t1 + } + v.decider.setPcs(prevPcs) bcExps } @@ -72,27 +80,32 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat } } - def getPreconditions(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], preHeap: Heap, bcExps: Seq[Exp], newFieldChunks: Map[BasicChunk, LocationAccess]): Option[Seq[Exp]] = { + def getPreconditions(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], + preHeap: Heap, bcExps: Seq[Exp], newFieldChunks: Map[BasicChunk, LocationAccess]): Option[Seq[Exp]] = { - if (state.isEmpty) { - Some(Seq()) - } else { + val varTran = VarTransformer(s, v, preVars, preHeap, newFieldChunks) - val varTrans = VarTransformer(s, v, preVars, preHeap, newFieldChunks) - val presTransformed = state.collect { - case (pre, Some(ch)) => varTrans.transformChunk(ch) - //case (pre, None) => varTrans.transformExp(pre) - } - val bcPreExps = bcExps.collect { - case exp => varTrans.transformExp(exp) - } + val presTransformed = state.collect { + case (pre, Some(ch)) => + pre match { + case ap: AccessPredicate => + varTran.transformChunk(ch.copy(perm = varTran.permExpToTerm(ap.perm))) + } + } + + val assertionsTransformed = assertions.map { assert => varTran.transformExp(assert, onlyInner = true) } + val bcPreExps = bcExps.collect { + case exp => varTran.transformExp(exp) + } - // If we cannot express the precondition, we have to fail - // If we fail to express some branch conditions, we can overapproximate the precondition - if (presTransformed.contains(None)) { - None + // If we cannot express the precondition or assertions, we have to fail + if (presTransformed.contains(None) || assertionsTransformed.contains(None)) { + None + } else { + val pres = presTransformed.collect { case Some(e) => e } ++ assertionsTransformed.collect { case Some(e) => e } + if (pres.isEmpty) { + Some(Seq()) } else { - val pres = presTransformed.collect { case Some(e) => e } val bcs = BigAnd(bcPreExps.collect { case Some(e) => e }) bcs match { case _: TrueLit => Some(pres) @@ -117,11 +130,12 @@ case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), l } case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], loc: Positioned, pcs: PathConditionStack, varTran: VarTransformer) extends BiAbductionSuccess { - override def toString: String = "Successful framing" - + override def toString: String = { + s"Succesfull framing with posts $posts" + } def getBcExps(bcsTerms: Seq[Term], prefVars: Map[AbstractLocalVar, (Term, Option[Exp])], otherVars: Map[AbstractLocalVar, (Term, Option[Exp])]): Seq[Exp] = { - val varTrans = VarTransformer(s, v, prefVars, s.h, otherVars = otherVars) - val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) } + val varTran = VarTransformer(s, v, prefVars, s.h, otherVars = otherVars) + val bcExps = bcsTerms.map { t => varTran.transformTerm(t) } bcExps.collect { case Some(e) => e.topLevelConjuncts }.flatten.distinct } } @@ -129,16 +143,17 @@ case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], loc: Positione case class BiAbductionFailure(s: State, v: Verifier, pcs: PathConditionStack) extends BiAbductionResult { override def toString: String = "Abduction failed" - def addToMethod(m: Method): Method = { + def + addToMethod(m: Method): Method = { val ins = m.formalArgs.map(_.localVar) val preHeap = s.oldHeaps.head._2 val inVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) } val prevPcs = v.decider.pcs v.decider.setPcs(pcs) - val varTrans = VarTransformer(s, v, inVars, preHeap) + val varTran = VarTransformer(s, v, inVars, preHeap) val bcTerms = v.decider.pcs.branchConditions val bcExpOpt = bcTerms.map { - bc => varTrans.transformTerm(bc) + bc => varTran.transformTerm(bc) } v.decider.setPcs(prevPcs) @@ -162,7 +177,6 @@ trait RuleApplier[S] { * Recursively applies the rules until we reach the end of the rules list. */ def applyRules(in: S, currentRule: Int = 0)(Q: S => VerificationResult): VerificationResult = { - if (currentRule == rules.length) { Q(in) } else { @@ -188,27 +202,59 @@ trait BiAbductionRule[S] { object BiAbductionSolver { def solveAbductionForError(s: State, v: Verifier, f: Failure, stateAllowed: Boolean, trigger: Option[Positioned] = None)(Q: (State, Verifier) => VerificationResult): VerificationResult = { - if (!s.doAbduction) { f } else { val initPcs = v.decider.pcs.duplicate() - //val initTra = VarTransformer(s, v, s.g.values, s.h) - val reason = f.message.reason match { case reason: InsufficientPermission => + val perm = f.message.offendingNode match { + case _: Fold => + Some(PermMul(s.abdPermScalingFactorExp, reason.permExp.getOrElse(FullPerm()()))()) + case _ => reason.permExp + } val acc = reason.offendingNode match { - case n: FieldAccess => FieldAccessPredicate(n, Some(FullPerm()()))() - case n: PredicateAccess => PredicateAccessPredicate(n, Some(FullPerm()()))() + case n: FieldAccess => + FieldAccessPredicate(n, perm)() + case n: PredicateAccess => + PredicateAccessPredicate(n, perm)() } Some(acc) - case reason: MagicWandChunkNotFound => Some(reason.offendingNode) - case _ => None + case reason: MagicWandChunkNotFound => + Some(reason.offendingNode) + // If we fail a fold because of an assertion, we might want to reattempt it with the assertion produced + case AssertionFalse(assert) => + f.message.offendingNode match { + case _: Fold => Some(Assert(assert)()) + case _ => None + } + case _ => + None } reason match { case None => f - case Some(abdGoal) => + case Some(Assert(assertion)) if s.packaging.isDefined => + // If we failed to fold a predicate because of an assertion while packaging a wand, + // we try producing the assertion in the state and continuing + executionFlowController.tryOrElse0(s, v) { (s1, v1, T) => + val sProd = s1.reserveHeaps.length match { + // This means that we are inside package... right? + // if we are in a pakcage stmt we must record all permissions added by previously executed statements + case 4 => s1.copy(h=s1.reserveHeaps(1)) + case _ => s1 + } + producer.produce(sProd, freshSnap, assertion, pve, v1) { (s2, v2) => + T(s2, v2) + } + } { + (s1a, v1a) => + val abd = AbductionSuccess(s1a, v1a, v1a.decider.pcs.duplicate(), Seq.empty, Seq.empty, Map.empty, Seq.empty, trigger, Seq(assertion)) + Success(Some(abd)) && Q(s1a, v1a) + } { + f => f + } + case Some(abdGoal: Exp) => val tra = f.message.failureContexts.collectFirst { case SiliconAbductionFailureContext(trafo) if trafo.isDefined => trafo.get @@ -219,9 +265,32 @@ object BiAbductionSolver { case Some(trafo) => trafo.f(qPre).asInstanceOf[AbductionQuestion] case _ => qPre } + // We need to save in the state if we're failing because of a fold + val qFold = f.message.offendingNode match { + case fold: Fold => + q.copy(s = s.copy(reservedForFoldUnfold = + if (q.s.reservedForFoldUnfold.exists { case (exp, _) => exp == fold.acc }) q.s.reservedForFoldUnfold + else q.s.reservedForFoldUnfold :+ (fold.acc -> Seq.empty) + )) + case _ => q + } + // We also need to check if we're failing because of an invariant and, if yes, save it + // amherz: we now handle this differently, here for completeness + /*val qInvariant = f.message match { + case LoopInvariantNotPreserved(invariant, _, _) => + val predAccesses: Seq[Exp] = invariant.collect { case pap: PredicateAccessPredicate => pap }.toSeq + qFold.copy(s = qFold.s.copy(reservedForInvariants = qFold.s.reservedForInvariants ++ predAccesses)) + case _ => qFold + }*/ + + // NOTE: Without fractional permissions, the comment below is true + // With fractional permissions, we HAVE to start with rule one because if we hold a fraction smaller + // than the goal, we must subtract it from the goal + // amherz: THIS IS NO LONGER TURE. We now start at 1, because all math is performed in the missing (last) rule + // // We skip the first rule because we know that an error occured, so we cannot be done // This allows us to fold on null references multiple times, as is required for e.g. trees. - AbductionApplier.applyRules(q, currentRule = 1) { + AbductionApplier.applyRules(qFold, currentRule = 1) { q1 => if (q1.goal.isEmpty) { val newState = q1.foundState.reverse @@ -232,9 +301,10 @@ object BiAbductionSolver { //Unreachable() } else { val newChunks = newState.collect { case (_, c: Some[BasicChunk]) => c.get } - //val newOldHeaps = q1.s.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks)) } - //val s1 = q1.s.copy(oldHeaps = newOldHeaps) + // val newOldHeaps = q1.s.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks)) } + // val s1 = q1.s.copy(oldHeaps = newOldHeaps) val fieldChunks = newState.collect { case (fa: FieldAccessPredicate, c) => (c.get, fa.loc) }.toMap + val abd = AbductionSuccess(q1.s, q1.v, q1.v.decider.pcs.duplicate(), newState, newStmts, fieldChunks, newChunks, trigger) Success(Some(abd)) && Q(q1.s, q1.v) } @@ -242,6 +312,11 @@ object BiAbductionSolver { f } } + case _ => + // This will only happen if we fail with an assertion (value constraint) AND + // we're not packaging + // In that case, we fail + f } } } @@ -256,15 +331,14 @@ object BiAbductionSolver { } def solveFraming(s: State, v: Verifier, pvef: Exp => PartialVerificationError, tra: VarTransformer, loc: Positioned, knownPosts: Seq[Exp], stateAllowed: Boolean)(Q: FramingSuccess => VerificationResult): VerificationResult = { - - //val tra = VarTransformer(s, v, targetVars, s.h) executionFlowController.tryOrElse1[Option[Term]](s, v) { (s, v, QS) => consumes(s, knownPosts, false, pvef, v)(QS) } { (s1: State, _: Option[Term], v1: Verifier) => executionFlowController.locallyWithResult[Seq[Exp]](s1, v1) { (s1a, v1a, T) => BiAbductionSolver.solveAbstraction(s1a, v1a) { (s2, framedPosts, v2) => + // val tra2 = VarTransformer(s, v, s.g.values, s.h) val newPosts = framedPosts.map { e => tra.transformExp(e) }.collect { case Some(e) => e } - T(newPosts) + T(abductionUtils.sortExps(newPosts)) } } { // We consumed all the posts and did not find any new ones. So create a fresh Framing Success with the bcs @@ -273,7 +347,8 @@ object BiAbductionSolver { // We consumed the post conditions and found new ones. Handle the new ones and add them to the result case newPosts1 => solveFraming(s1, v1, pvef, tra, loc, newPosts1, stateAllowed) { frame => - val newFrame = frame.copy(posts = frame.posts ++ newPosts1) + val sortedPost = abductionUtils.sortExps(newPosts1) + val newFrame = frame.copy(posts = frame.posts ++ sortedPost) Q(newFrame) } } @@ -282,17 +357,6 @@ object BiAbductionSolver { f => BiAbductionSolver.solveAbductionForError(s, v, f, stateAllowed, Some(loc))((s3, v3) => { solveFraming(s3, v3, pvef, tra, loc, knownPosts, stateAllowed)(Q) - - /*{ - frame => - val newAbdRes = if (res.state.nonEmpty) { - Success(Some(res.copy(stmts = Seq()))) - } else { - Success() - } - //val newFrame = frame.copy(stmts = frame.stmts ++ res.stmts) - Q(frame) - }*/ } ) } @@ -301,9 +365,8 @@ object BiAbductionSolver { def resolveAbductionResults(m: Method, nf: NonFatalResult): Option[Method] = { val abdReses = abductionUtils.getAbductionSuccesses(nf) val newMatches = abdReses.flatMap(_.newFieldChunks).toMap - val abdCases = abdReses.groupBy(res => (res.trigger.get, res.trigger.get.pos, res.stmts, res.state)) + val abdCases = abdReses.groupBy(res => (res.trigger.get.pos, res.stmts, res.state.map({ case (e, _) => e }))) - // Try to join by bc terms val joinedCases = abdCases.map { case (_, reses) => val unjoined = reses.map(res => @@ -313,7 +376,6 @@ object BiAbductionSolver { case term => Seq(term) }.distinct.filter(_ != True))) val termJoined = abductionUtils.joinBcsTerms(unjoined) - // Now transform to exp, remove Nones and join again. TODO: Removing Nones here might be unsound // That is why we do as much as possible on term level to avoid this as much as possible val expUnjoined = termJoined.map { @@ -321,16 +383,18 @@ object BiAbductionSolver { reses -> reses.head.getBcExps(bcTerms).collect { case Some(bc) => bc }.flatMap(_.topLevelConjuncts).distinct } val expJoined = abductionUtils.joinBcsExps(expUnjoined) - val abdRes = expJoined.head._1.head val finalBcs = BigOr(expJoined.map(e => BigAnd(e._2))) (abdRes -> finalBcs) } - // We want to add things in the reverse order of the abduction results. abdReses.reverse.foldLeft[Option[Method]](Some(m)) { (mOpt, res) => mOpt match { - case Some(m1) if joinedCases.contains(res) => addToMethod(m1, Seq(joinedCases(res)), newMatches, res) + case Some(m1) if joinedCases.contains(res) => + addToMethod(m1, Seq(joinedCases(res)), newMatches, res) match { + case Some(m2) => Some(m2) + case None => mOpt + } case _ => mOpt } } @@ -340,7 +404,6 @@ object BiAbductionSolver { val s = abdRes.s val v = abdRes.v - val ins = m.formalArgs.map(_.localVar) val preHeap = s.oldHeaps.head._2 val preVars = s.g.values.collect { case (v, t) if ins.contains(v) => (v, t) } @@ -374,8 +437,8 @@ object BiAbductionSolver { case whileStmt: While if whileStmt.cond == e && whileStmt.cond.pos == e.pos => Seqn(abdRes.stmts :+ whileStmt, Seq())(whileStmt.pos, whileStmt.info, whileStmt.errT) } } - - Some(m.copy(pres = abductionUtils.sortExps(pres.get ++ m.pres).distinct, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) + val newPres = abductionUtils.sortExps(abductionUtils.normalizePreconditions(pres.get ++ m.pres, s, v)) + Some(m.copy(pres = newPres, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) } } @@ -391,14 +454,11 @@ object BiAbductionSolver { def resolveFramingResults(m: Method, nf: NonFatalResult): Option[Method] = { val frames = abductionUtils.getFramingSuccesses(nf) - // We get a framing result for every branch. // So postconditions that are in every branch can just be added without any bcs val everyPosts = frames.head.posts.filter { p => frames.forall(_.posts.contains(p)) } - - //val formals = m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar) - //val bcs = frames.map(_.pcs.branchConditions) - + // val formals = m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar) + // val bcs = frames.map(_.pcs.branchConditions) val cases = frames.map { f => val prefVars = f.s.g.values.collect { case (var2, t) if m.formalArgs.map(_.localVar).contains(var2) => (var2, t) } val otherVars = f.s.g.values.collect { case (var2, t) if m.formalReturns.map(_.localVar).contains(var2) => (var2, t) } @@ -408,7 +468,6 @@ object BiAbductionSolver { }.distinct.filter(_ != True) (f.posts.diff(everyPosts), f.getBcExps(bcs, prefVars, otherVars)) }.distinct - // We can remove bcs that hold in every branch val everyTerms = cases.head._2.filter { t => cases.forall(_._2.contains(t)) } @@ -416,22 +475,11 @@ object BiAbductionSolver { case (posts, bcs) if posts.nonEmpty && bcs.diff(everyTerms).nonEmpty => Implies(BigAnd(bcs.diff(everyTerms)), BigAnd(posts))() case (posts, _) if posts.nonEmpty => BigAnd(posts) } ++ everyPosts - Some(m.copy(posts = m.posts ++ res)(pos = m.pos, info = m.info, errT = m.errT)) - - /* - val frameCases = frames.groupBy(f => f.posts.diff(everyPosts)).flatMap { - case (_, frs) => - val unjoined = frs.map(fr => (Seq(fr), fr.pcs.branchConditions.distinct.filter(_ != True))) - val joined = abductionUtils.joinBcs(unjoined) - joined.map { - case (frs, pcs) => - frs.head -> pcs - } - } - - frameCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2.diff(alwaysTerms)) }) - */ + // we still need to sort the posts + val sortedPosts = abductionUtils.sortExps(m.posts ++ res) + val newM = m.copy(posts = sortedPosts)(pos = m.pos, info = m.info, errT = m.errT) + Some(newM) } @@ -504,6 +552,8 @@ object BiAbductionSolver { object abductionUtils { + val pve: PartialVerificationError = Internal() + def isValidPredicate(pred: Predicate): Boolean = { pred.formalArgs.size == 1 && pred.body.isDefined } @@ -666,4 +716,545 @@ object abductionUtils { fields ++ preds ++ others } + // We need to normalize conditions, that includes: performing airhtmetic on the permissions to the same lcoation, + // clamp the permissions. + def normalizePreconditions(expressions: Seq[Exp], s: State, v: Verifier): Seq[Exp] = { + val varTran = VarTransformer(s, v, s.g.values, s.h) + + def normalizePermissions(exp: Exp): Exp = { + exp.transform({ + case fap: FieldAccessPredicate => + fap.copy(permExp = None)(fap.pos, fap.info, fap.errT) + case pap: PredicateAccessPredicate => + pap.copy(permExp = None)(pap.pos, pap.info, pap.errT) + }) + } + + def extractPerm(exp: Exp): Exp = exp match { + case fap: FieldAccessPredicate => fap.perm + case pap: PredicateAccessPredicate => pap.perm + case Implies(_, fap: FieldAccessPredicate) => fap.perm + case Implies(_, pap: PredicateAccessPredicate) => pap.perm + case e => e + } + + def clampPerm(permSum: Exp): Exp = { + try { + val r = asRational(Some(permSum)) + if (r > Rational(1, 1)) asPerm(Rational(1, 1)) + else asPerm(r) + } catch { + case _: IllegalStateException => permSum + } + } + + expressions.groupBy(normalizePermissions).values.map { group => + if (group.size == 1) { + group.head + } else { + val ap = group.head + val permSum = clampPerm( + group + .map(extractPerm) + .reduceLeft((p1, p2) => PermAdd(p1, p2)(p1.pos, p1.info, p1.errT)) + ) + + ap match { + case fap: FieldAccessPredicate => + fap.copy(permExp = Some(permSum))(fap.pos, fap.info, fap.errT) + case pap: PredicateAccessPredicate => + pap.copy(permExp = Some(permSum))(pap.pos, pap.info, pap.errT) + case Implies(lhs, fap: FieldAccessPredicate) => + Implies(lhs, fap.copy(permExp = Some(permSum))(fap.pos, fap.info, fap.errT))(ap.pos, ap.info, ap.errT) + case Implies(lhs, pap: PredicateAccessPredicate) => + Implies(lhs, pap.copy(permExp = Some(permSum))(pap.pos, pap.info, pap.errT))(ap.pos, ap.info, ap.errT) + case other => other + } + } + }.toSeq + } + + + def accWithPerm(ap: AccessPredicate, newPerm: Option[Exp]): AccessPredicate = { + ap match { + case fap: FieldAccessPredicate => FieldAccessPredicate(fap.loc, newPerm)(fap.pos, fap.info, fap.errT) + case pap: PredicateAccessPredicate => PredicateAccessPredicate(pap.loc, newPerm)(pap.pos, pap.info, pap.errT) + } + } + + def asRational(p: Option[Exp]): Rational = p match { + case Some(p2) => p2 match { + case _: FullPerm => Rational(1, 1) + case _: NoPerm => Rational(0, 1) + case FractionalPerm(IntLit(l), IntLit(r)) => Rational(l, r) + case PermMul(e1, e2) => asRational(Some(e1)) * asRational(Some(e2)) + case PermSub(e1, e2) => asRational(Some(e1)) - asRational(Some(e2)) + case PermAdd(e1, e2) => asRational(Some(e1)) + asRational(Some(e2)) + case PermDiv(e1, e2) => asRational(Some(e1)) / asRational(Some(e2)) + case PermPermDiv(e1, e2) => asRational(Some(e1)) / asRational(Some(e2)) + case WildcardPerm() => Rational(0, 1) + case e => + throw new IllegalStateException(s"Impossible by invariant: $p") + } + case None => Rational(1, 1) + } + + def asPerm(r: Rational): Exp = { + FractionalPerm(IntLit(r.numerator)(), IntLit(r.denominator)())() + } + + // This does max(a - b, 0) + def clampSubPerm(a: Option[Exp], b: Option[Exp]): FractionalPerm = { + val sub = asRational(a) - asRational(b) + FractionalPerm( + IntLit(if (sub.compare(Rational(0, 1)) < 0) 0 else sub.numerator)(), + IntLit(sub.denominator)() + )() + } + + def maxPerm(p1: Exp, p2: Exp, v: Verifier, varTran: VarTransformer): Exp = { + (p1, p2) match { + case (Implies(lhs1, inner1), Implies(lhs2, inner2)) if lhs1 == lhs2 => + val term1 = varTran.permExpToTerm(inner1 match { case fap: FieldAccessPredicate => fap.perm case pap: PredicateAccessPredicate => pap.perm }) + val term2 = varTran.permExpToTerm(inner2 match { case fap: FieldAccessPredicate => fap.perm case pap: PredicateAccessPredicate => pap.perm }) + if (v.decider.check(terms.AtLeast(term1, term2), Verifier.config.checkTimeout())) p1 else p2 + case (Implies(_, _), _) | (_, Implies(_, _)) => + p1 + case _ => + val term1 = varTran.permExpToTerm(p1) + val term2 = varTran.permExpToTerm(p2) + if (v.decider.check(terms.AtLeast(term1, term2), Verifier.config.checkTimeout())) p1 else p2 + } + } + + def minPerm(p1: Exp, p2: Exp, v: Verifier, varTran: VarTransformer): Exp = { + (p1, p2) match { + case (Implies(lhs1, inner1), Implies(lhs2, inner2)) if lhs1 == lhs2 => + val term1 = varTran.permExpToTerm(inner1 match { case fap: FieldAccessPredicate => fap.perm case pap: PredicateAccessPredicate => pap.perm }) + val term2 = varTran.permExpToTerm(inner2 match { case fap: FieldAccessPredicate => fap.perm case pap: PredicateAccessPredicate => pap.perm }) + if (v.decider.check(terms.AtMost(term1, term2), Verifier.config.checkTimeout())) p1 else p2 + case (Implies(_, _), _) | (_, Implies(_, _)) => + p1 + case _ => + val term1 = varTran.permExpToTerm(p1) + val term2 = varTran.permExpToTerm(p2) + if (v.decider.check(terms.AtMost(term1, term2), Verifier.config.checkTimeout())) p1 else p2 + } + } + + def maxPermRational(a: Option[Exp], b: Option[Exp]): Rational = { + val aRational = asRational(a) + val bRational = asRational(b) + if (aRational.compare(bRational) >= 0) aRational else bRational + } + + def minPermRational(a: Option[Exp], b: Option[Exp]): Rational = { + val aRational = asRational(a) + val bRational = asRational(b) + if (aRational.compare(bRational) < 0) aRational else bRational + } + + def fieldsMap(pred: Predicate, a: PredicateAccessPredicate): Map[FieldAccess, Rational] = { + pred.body.get.transform { + case lc: AbstractLocalVar if pred.formalArgs.head.localVar == lc => a.loc.args.head + }.collect { + // Need to make sure that for pred(x) we only include fields x.f and not x.f.g + case fap: FieldAccessPredicate if fap.loc.rcv == a.loc.args.head => fap.permExp match { + case None => fap.loc -> Rational(1, 1) + case Some(_: FullPerm) => fap.loc -> Rational(1, 1) + case Some(_: NoPerm) => fap.loc -> Rational(0, 1) + case Some(FractionalPerm(IntLit(a), IntLit(b))) => fap.loc -> Rational(a, b) + } + }.toMap/*.filter { case (fa, _) => + // We need ot filter out things like curr.next.prev + !fa.rcv.isInstanceOf[FieldAccess] + }.toMap*/ + } + + // If the wand contains acc(list(x)) the structure has ", write" instead of ", Perm", + // need to correct it to semantically compare wands with fractions + def correctStructure(structure: MagicWandStructure.MagicWandStructure): MagicWandStructure.MagicWandStructure = { + def transPerm(perm: Option[Exp], fap: AccessPredicate) = Some(perm match { + case None => LocalVar ("Perm", Perm)(fap.pos, fap.info, fap.errT) + case Some(_: FullPerm) => LocalVar ("Perm", Perm)(fap.pos, fap.info, fap.errT) + case Some(p) => p + }) + structure.transform{ + case fap@FieldAccessPredicate(loc, perm) => + FieldAccessPredicate(loc, transPerm(perm, fap))(fap.pos, fap.info, fap.errT) + case pap@PredicateAccessPredicate(loc, perm) => + PredicateAccessPredicate(loc, transPerm(perm, pap))(pap.pos, pap.info, pap.errT) + } + } + + def checkChunk(loc: LocationAccess, s: State, v: Verifier, lostAccesses: Map[Exp, Term]) + (Q: Option[BasicChunk] => VerificationResult): VerificationResult = { + val arg = loc match { + case FieldAccess(rcv, _) => rcv + case PredicateAccess(args, _) => args.head + } + safeEval(arg, s, v, lostAccesses) { (s2, terms, v2) => + terms match { + case Some(term) => + val resource = loc.res(s2.program) + val id = ChunkIdentifier(resource, s2.program) + val chunk = findChunk[BasicChunk](s2.h.values, id, Seq(term), v2) + Q(chunk) + case None => Q(None) + } + } + } + + /** + * Does a couple of things to ensure evalution works properly: + * + * Check the lost accesses to see if the access is there + * Evaluate sub-expressions safely to ensure that a missing chunk will not cause the evaluation to silently abort + */ + def safeEval(e: Exp, s: State, v: Verifier, lostAccesses: Map[Exp, Term]) + (Q: (State, Option[Term], Verifier) => VerificationResult): VerificationResult = { + + if (!e.contains[LocationAccess]) { + eval(s, e, pve, v)((s1, t, _, v1) => Q(s1, Some(t), v1)) + } else { + + // If the arg was lost, we have it in the map + if (lostAccesses.contains(e)) { + Q(s, Some(lostAccesses(e)), v) + } else { + e match { + // If the arg is a location access, we have to recursively check it + case loc: LocationAccess => checkChunk(loc, s, v, lostAccesses) { + case Some(c) => Q(s, Some(c.snap), v) + case None => Q(s, None, v) + } + //case lv: AbstractLocalVar => Q(s, Some(s.g(lv)), v) + case _ => eval(s, e, pve, v)((s, t, _, v) => Q(s, Some(t), v)) + //case _ => evalLocationAccess(q.s, loc, pve, q.v) { (s2, _, tArgs, v2) => Q(s2, Some(tArgs), v2) } + } + } + } + } + + // Computes permissions to a location + // We need the (rather expensive) verifier check to minimize the amoutn of aliased locations that we could miss on + // This is the _definitelyEqual_ variable. + def permsTo(loc: LocationAccess, s: State, v: Verifier, lostAccesses: Map[Exp, Term]) + (Q: Option[Exp] => VerificationResult) = { + val arg = loc match { + case FieldAccess(rcv, _) => rcv + case PredicateAccess(args, _) => args.head + } + + safeEval(arg, s, v, lostAccesses) { (s2, terms, v2) => + terms match { + case Some(term) => + val resource = loc.res(s2.program) + val id = ChunkIdentifier(resource, s2.program) + val h = s2.partiallyConsumedHeap.getOrElse(s2.h) + val chs = findChunksWithID[BasicChunk](h.values, id) + val currentPermAmount = + chs.foldLeft(NoPerm()(): Exp)((q, ch) => { + val definitelyEqual = ch.args.zip(Seq(term)).forall { + case (a1, a2) => v2.decider.check(a1 === a2, Verifier.config.checkTimeout()) + } + if (definitelyEqual) { + val varTran = VarTransformer(s, v, s.g.values, s.h) + PermAdd(q, varTran.transformTerm(ch.perm).getOrElse(NoPerm()()))() + } else q + }) + val rationalPerm = asRational(Some(currentPermAmount)) + if (rationalPerm == Rational(0, 1)) { + Q(Some(NoPerm()())) + } + else { + Q(Some(FractionalPerm(IntLit(rationalPerm.numerator)(), IntLit(rationalPerm.denominator)())())) + } + case None => + Q(Some(NoPerm()())) + } + } + } + + def expMatchWithPermissions(exp1: Exp, exp2: Exp, v: Verifier, varTran: VarTransformer): Boolean = { + (exp1, exp2) match { + case (fap1: FieldAccessPredicate, fap2: FieldAccessPredicate) => + fap1.loc == fap2.loc && + ((fap1.permExp, fap2.permExp) match { + case (Some(perm1), Some(perm2)) => + v.decider.check(terms.Equals(varTran.permExpToTerm(perm1), varTran.permExpToTerm(perm2)), Verifier.config.checkTimeout()) + case (None, None) => true + case (None, Some(FullPerm())) => true + case (Some(FullPerm()), None) => true + case _ => false + }) + case (pap1: PredicateAccessPredicate, pap2: PredicateAccessPredicate) => + pap1.loc == pap2.loc && + ((pap1.permExp, pap2.permExp) match { + case (Some(perm1), Some(perm2)) => + v.decider.check(terms.Equals(varTran.permExpToTerm(perm1), varTran.permExpToTerm(perm2)), Verifier.config.checkTimeout()) + case (None, None) => true + case (None, Some(FullPerm())) => true + case (Some(FullPerm()), None) => true + case _ => false + }) + case _ => false + } + } + + def simplifyPermission(e: Exp): Exp = { + if (!e.isInstanceOf[PermExp] || e.isInstanceOf[WildcardPerm]) return e + val rational = abductionUtils.asRational(Some(e)) + if (rational.numerator == 1 && rational.denominator == 1) { + FullPerm()() + } else if (rational.numerator == 0) { + NoPerm()() + } else { + FractionalPerm(IntLit(rational.numerator)(), IntLit(rational.denominator)())() + } + } + + // This is the fucntion that takes care of cocnretizing (i.e. turning into concrete values that we can work with) permissions + // It currently turns wildcard (i.e. read) permissions into an exact fraction that can be modified. + def concretizeAccs(accs: Seq[AccessPredicate], q: AbductionQuestion) + (Q: Seq[AccessPredicate] => VerificationResult): VerificationResult = { + def go(remaining: List[AccessPredicate], + accumulated: List[AccessPredicate]): VerificationResult = { + remaining match { + case Nil => + Q(accumulated.reverse) + + case (fap@FieldAccessPredicate(_, Some(WildcardPerm()))) :: tail => + go(tail, abductionUtils.accWithPerm(fap, Some(FractionalPerm(IntLit(1)(), IntLit(4)())())) :: accumulated) + /*findMinPerm(loc, q.s, q.v, q.lostAccesses) { permOpt => + val perm = permOpt.getOrElse(FullPerm()()) + go(tail, abductionUtils.accWithPerm(fap, Some(perm)) :: accumulated) + }*/ + + case (pap@PredicateAccessPredicate(_, Some(WildcardPerm()))) :: tail => + go(tail, abductionUtils.accWithPerm(pap, Some(FractionalPerm(IntLit(1)(), IntLit(4)())())) :: accumulated) + /*findMinPerm(loc, q.s, q.v, q.lostAccesses) { permOpt => + val perm = permOpt.getOrElse(FullPerm()()) + go(tail, abductionUtils.accWithPerm(pap, Some(perm)) :: accumulated) + }*/ + + case acc :: tail => + acc match { + case g @ AccessPredicate(loc: LocationAccess, permG) => + abductionUtils.permsTo(loc, q.s, q.v, q.lostAccesses) { permH => + val newP = abductionUtils.clampSubPerm(Some(permG), permH) + val g2 = abductionUtils.accWithPerm(g, Some(newP)) + go(tail, g2 :: accumulated) + } + + /*case _ => + go(tail, acc :: accumulated)*/ + } + } + } + + go(accs.toList, Nil) + } + + def buildPredicatePermissionsMap(s: State, v: Verifier): Map[Predicate, Map[Object, FractionalPerm]] = { + + var result: Map[Predicate, Map[Object, FractionalPerm]] = Map.empty + + def processLocation(bS: State, bV: Verifier, eS: State, loc: LocationAccess) + (Q: FractionalPerm => VerificationResult): VerificationResult = { + + abductionUtils.permsTo(loc, eS, v, Map.empty) { prevPerm => + abductionUtils.permsTo(loc, bS, bV, Map.empty) { currPerm => + val gainedPerm = abductionUtils.clampSubPerm(currPerm, prevPerm) + Q(gainedPerm) + } + } + + } + + def processPredicates(remaining: List[Predicate], acc: Map[Predicate, Map[Object, FractionalPerm]]): VerificationResult = remaining match { + case Nil => + result = acc + Success() + case pred :: rest => + processPredicate(pred) { locationPermMap => + processPredicates(rest, acc + (pred -> locationPermMap)) + } + } + + def processPredicate(pred: Predicate) + (Q: Map[Object, FractionalPerm] => VerificationResult): VerificationResult = { + + def innermostFA(loc: LocationAccess): Option[FieldAccess] = loc match { + case fa @ FieldAccess(rcv, _) => + rcv match { + case innerRcv: FieldAccess => innermostFA(innerRcv) + case _ => Some(fa) + } + case _ => None + } + + val locations: Seq[LocationAccess] = pred.body.get.flatMap { + case PredicateAccessPredicate(loc, _) => Some(loc) + case FieldAccessPredicate(loc, _) => innermostFA(loc) + case _ => None + }.toSeq.distinct + + val freshVars = pred.formalArgs.map(arg => LocalVar(arg.name, arg.typ)()) + val varDecls = freshVars.map { + fv => LocalVarDeclStmt(LocalVarDecl(fv.name, fv.typ)())() + } + + // Helper to merge two maps taking max permission for each key + def mergeMaxPerms(acc1: Map[Object, FractionalPerm], + acc2: Map[Object, FractionalPerm]): Map[Object, FractionalPerm] = { + val allKeys = acc1.keySet ++ acc2.keySet + allKeys.map { key => + val perm1 = acc1.get(key).orElse(Some(NoPerm()())) + val perm2 = acc2.get(key).orElse(Some(NoPerm()())) + val maxP = abductionUtils.maxPermRational(perm1, perm2) + key -> FractionalPerm(IntLit(maxP.numerator)(), IntLit(maxP.denominator)())() + }.toMap + } + + var accumulatedPerms: Map[Object, FractionalPerm] = Map.empty + + def processLocations(bS: State, bV: Verifier, eS: State, remaining: Seq[LocationAccess], acc: Map[Object, FractionalPerm]): VerificationResult = remaining match { + case Nil => + accumulatedPerms = mergeMaxPerms(accumulatedPerms, acc) + Success() + case loc :: rest => + processLocation(bS, bV, eS, loc) { perm => + loc match { + case PredicateAccess(_, name) => processLocations(bS, bV, eS, rest, acc + (name -> perm)) + case FieldAccess(_, field) => processLocations(bS, bV, eS, rest, acc + (field -> perm)) + } + } + } + + val result = executor.exec(s, Seqn(varDecls, Seq.empty)(), v) { (eS, _) => + executor.exec(s, Seqn(varDecls :+ Inhale(pred.body.get)(), Seq.empty)(), v) { (bS, bV) => + processLocations(bS, bV, eS, locations, Map.empty) + } + } + + result && Q(accumulatedPerms) + } + + processPredicates(s.program.predicates.toList, Map.empty) + result + } + + /*def retryOnFailedAssertion( + s: State, + v: Verifier, + exec: (State, Verifier, (State, Verifier) => VerificationResult) => VerificationResult + )(Q: (State, Verifier) => VerificationResult): VerificationResult = { + executionFlowController.tryOrElse0(s, v) { (s1, v1, T) => + exec(s1, v1, T) + } { + (s1a, v1a) => + // println(s"Attempt successful") + Q(s1a, v1a) + } { + f => + f.message.reason match { + case AssertionFalse(assertion) => + // println(s"exec failed with ${f.message.reason}") + producer.produce(s, freshSnap, assertion, pve, v) { (s1r, v1r) => + // println(s"Produced, will reattempt") + retryOnFailedAssertion(s1r, v1r, exec)(Q) + } + case _ => + f + } + } + }*/ + + def pickBranch( + results: Seq[AbductionSuccess] + ): Seq[AbductionSuccess] = { + val grouped = results.groupBy(_.pcs.branchConditions) + if (grouped.isEmpty) return Seq.empty + + val minSize = grouped.keys.map(_.size).min + var current = grouped.filter(_._1.size == minSize).maxBy(_._2.size)._1 + val selectedBcs = collection.mutable.Set(current) + + var searching = true + while (searching) { + val extensions = grouped.filter { case (bcs, _) => + bcs.size == current.size + 1 && bcs.tail == current + } + if (extensions.isEmpty) { + searching = false + } else { + val (nextBcs, _) = extensions.maxBy(_._2.size) + selectedBcs += nextBcs + current = nextBcs + } + } + + results.filter(r => selectedBcs.contains(r.pcs.branchConditions)) + } + + + // Here we try to match for aliasing, so if we have a situation like + // g: + // this -> (this@1@10,None) + // x -> ($t@3@10,None) + // h: + // this@1@10.next -> $t@3@10 + // We try to change list(this.next) --* list(this) to list(x) --* list(this) + // + // This also needs to work if we have + // g: + // list -> (list@1@10,None) + // head1 -> (head1@7@10,None) + // h: + // this@1@10.next -> First:($t@3@10) + // and in the decider assumptions: + // head1@7@10 == First:($t@3@10) + def transformWithAliasing(exp: Exp, q: AbductionQuestion): Exp = { + exp.transform { + case pred: PredicateAccessPredicate => + val newArgs = pred.loc.args.map { + case fa: FieldAccess => + resolveToVar(fa, q).getOrElse(fa) + case arg => arg + } + val newLoc = pred.loc.copy(args = newArgs)(pred.loc.pos, pred.loc.info, pred.loc.errT) + pred.copy(loc = newLoc)(pred.pos, pred.info, pred.errT) + } + } + + + private def resolveToVar(fa: FieldAccess, q: AbductionQuestion): Option[AbstractLocalVar] = { + val receiverTerm = fa.rcv match { + case lv: LocalVar => q.s.g.values.collectFirst { + case (v, (term, _)) if v.name == lv.name => term + } + case _ => None + } + + val valueTerm = receiverTerm.flatMap { rcvTerm => + q.s.h.values.collectFirst { + case chunk: BasicChunk if chunk.args.head == rcvTerm && chunk.id.name == fa.field.name => + chunk.snap + } + } + + valueTerm.flatMap { valTerm => + // First try exact syntactic match + q.s.g.values.collectFirst { + case (localVar, (term, _)) if term == valTerm => localVar + }.orElse { + // Fall back to semantic equality via the decider, but only if sorts match + q.s.g.values.collectFirst { + case (localVar, (term, _)) if term.sort == valTerm.sort && q.v.decider.check(terms.Equals(term, valTerm), Verifier.config.checkTimeout()) => localVar + } + } + } + } + } diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index 7054d0736..3d47396cb 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -3,7 +3,7 @@ package viper.silicon.biabduction import viper.silicon.interfaces._ import viper.silicon.rules.producer.produces import viper.silicon.rules.{evaluator, executionFlowController, executor, producer} -import viper.silicon.state.terms.{False, Term, True} +import viper.silicon.state.terms.{False, Term, True, AtLeast} import viper.silicon.state.{Heap, State} import viper.silicon.utils.ast.BigAnd import viper.silicon.utils.freshSnap @@ -34,13 +34,12 @@ object LoopInvariantSolver { val rest = (pres.filter { case _: MagicWand => false - case _ => true + case _ => false //true? } ++ posts).distinct var res: Seq[Exp] = Seq() executionFlowController.locally(s.copy(h = Heap()), v) { (s1, v1) => - producer.produces(s1, freshSnap, rest ++ existingInvs, pveLam, v1) { (s2, v2) => // There are case where there is some overlap between lefts and rests, we remove this using abduction @@ -70,7 +69,7 @@ object LoopInvariantSolver { case abdRes: NonFatalResult => // TODO nklose we do not guarantee length 1 here anymore abductionUtils.getAbductionSuccesses(abdRes) match { - case Seq(AbductionSuccess(s5, v5, _, _, _, _, _, _)) => + case Seq(AbductionSuccess(s5, v5, _, _, _, _, _, _, _)) => val unfolded = VarTransformer(s5, v5, s5.g.values, s5.h).transformState(s5) res = unfolded Success() @@ -118,94 +117,85 @@ object LoopInvariantSolver { //} executionFlowController.locally(s, v) { (s1, v1) => - - // Produce the already known invariants. They are consumed at the end of the loop body, so we need to do this every iteration - /*val invSubFields = loopHead.invs.flatMap(_.topLevelConjuncts).flatMap { inv => inv.flatMap { - case _: FieldAccess => Seq() - case other => other.collect {case fa: FieldAccess => fa} - }}.distinct*/ - - //val check = Seqn(Seq(Assert(BigAnd(perms))(), Inhale(BigAnd(funcs))()), Seq())() producer.produce(s1, freshSnap, BigAnd(loopHead.invs), pve, v1, withAbduction = true) { (s2, v2) => - //executor.exec(s1, check, v1, None) { (s2, v2) => - //evaluator.evalsWithAbduction(s1, invSubFields, _ => pve, v1) { (s2, _, _, v2) => - //produces(s2, freshSnap, loopHead.invs, ContractNotWellformed, v2) { (s3, v3) => - executor.follows(s2, loopEdges, pveLam, v2, joinPoint) { (s3, v3) => - - // To find a fixed point, we are only interested in branches where the loop condition can remains true - var nextCon = false - executionFlowController.locally(s3, v3) { (s4, v4) => - - //val conSubFields = loopConExp.topLevelConjuncts.flatMap { con => con.flatMap { - // case _: FieldAccess => Seq() - // case other => other.collect {case fa: FieldAccess => fa} - //}}.distinct - //executor.exec(s4, check, v4, None) { (s5, v5) => - //evaluator.evalsWithAbduction(s4, conSubFields, _ => pve, v4) { (sCon, _, _, vCon) => - producer.produce(s4, freshSnap, loopConExp, pve, v4, withAbduction = true) { (s5, v5) => - nextCon = !v5.decider.checkSmoke() - //.check(conTerm, Verifier.config.checkTimeout()) - Success() + + executionFlowController.locally(s2, v2) { (sF, vF) => + // edges have condition that is assumed by verifier + executor.follows(sF, loopEdges, pveLam, vF, joinPoint) { (s3, v3) => + // To find a fixed point we are only interested in branches where the loop condition can remains true + var nextCon = false + /*// println(s"Will produce loopConExp")*/ + executionFlowController.locally(s3, v3) { (s4, v4) => + producer.produce(s4, freshSnap, loopConExp, pve, v4, withAbduction = true) { (s5, v5) => + nextCon = !v5.decider.checkSmoke() + Success() } - //} - } - if (!nextCon) { - Success() - } else { - val endStmt = abductionUtils.getEndOfLoopStmt(loop) - val postTran = VarTransformer(s3, v3, s3.g.values, s3.h) - val postState = postTran.transformState(s3) - Success(Some(FramingSuccess(s3, v3, postState, endStmt, v3.decider.pcs.duplicate(), postTran))) + } + if (!nextCon) { + Success() + } else { + val endStmt = abductionUtils.getEndOfLoopStmt(loop) + val postTran = VarTransformer(s3, v3, s3.g.values, s3.h) + val postState = postTran.transformState(s3) + Success(Some(FramingSuccess(s3, v3, postState, endStmt, v3.decider.pcs.duplicate(), postTran))) + } } } - //} } } match { case f: Failure => f case nonf: NonFatalResult => - val abdReses = abductionUtils.getAbductionSuccesses(nonf).reverse + val abdReses = abductionUtils.getAbductionSuccesses(nonf).reverse.groupBy(_.trigger.get.pos) + // We need ot make sure that any branching in the loop body does not lead ot us generating twice the same + // abdres due to if conditions and their negation + .flatMap { case (_, grouped) => + grouped.distinctBy(abd => abd.state.map { case (e, _) => e }) + } + .toSeq // TODO nklose do we want to join branches properly here like we do for preconditions? + // [amherz] I think the above does it? val newMatches = abdReses.flatMap(_.newFieldChunks).toMap val preLoopVars = s.g.values.filter { case (v, _) => origVars.contains(v) } - val newStateOpt = abdReses.flatMap(abd => abd.getPreconditions(preLoopVars, s.h, Seq(), newMatches).get).distinct - + val preState = s.copy(h = q.preHeap) + val preTran = VarTransformer(preState, v, preLoopVars, preState.h) + // We need to normalize the state otherwise we might have fragmented chunks + val newStateOpt = abductionUtils.normalizePreconditions( + abdReses.flatMap(abd => + abd.getPreconditions(preLoopVars, s.h, Seq(), newMatches).toSeq.flatten + ), s, v) // We still need to remove the current loop condition val newState = abductionUtils.sortExps(newStateOpt.map(_.transform { case im: Implies if im.left == loopConExp => im.right })) //if (loopConExp == loopCons.head) { + println("-------------------------------------------------------------------") println("New state:\n " + newState.mkString("\n ")) + println("-------------------------------------------------------------------") //} - val preState = s.copy(h = q.preHeap) - val preTran = VarTransformer(preState, v, preLoopVars, preState.h) - val accs = loopHead.invs.flatMap(_.topLevelConjuncts).collect { case fa: FieldAccessPredicate => fa.loc case pa: PredicateAccessPredicate => pa.loc } - abductionUtils.findOptChunks(accs, preState, v, pve) { chunks => val toKeep = chunks.keys val toAbs = preState.copy(h= Heap(preState.h.values.toSeq.diff(toKeep.toSeq))) - - BiAbductionSolver.solveAbstraction(toAbs, v) { (newPreState0, newPreAbstraction0, _) => - // Now we add back the things we removed before abstraction. Or not I guess? val newPreState = newPreState0.copy(h = newPreState0.h + Heap(toKeep)) val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, strict = false).get) //++ chunks.values //if (loopConExp == loopCons.head) { + println("-------------------------------------------------------------------") println("New pre abstraction:\n " + newPreAbstraction.mkString("\n ")) + println("-------------------------------------------------------------------") //} // Consolidate the framing successes val posts = abductionUtils.getFramingSuccesses(nonf).groupBy(_.posts) - // We take the frame with the most posts val chosenFrame = posts.maxBy { case (exps, _) => exps.size }._2.head //posts.head._2.head chosenFrame.v.decider.setPcs(chosenFrame.pcs) @@ -217,24 +207,46 @@ object LoopInvariantSolver { val newPostAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get) //if (loopConExp == loopCons.head) { + println("-------------------------------------------------------------------") println("New post abstraction:\n " + newPostAbstraction.mkString("\n ")) + println("-------------------------------------------------------------------") //} // If the pushed forward abstraction is the same as the previous one, we are done if (iteration > 2 && newPreAbstraction.toSet == q.preAbstraction.toSet && newPostAbstraction.toSet == q.postAbstraction.toSet) { val existingInvs = loop.invs - val res = getInvariants(newPreAbstraction, newPostAbstraction, loopConExp, existingInvs, sPostAbs, vPostAbs) + // Need to distinct otherwise we get some weird duplication + val res = getInvariants(newPreAbstraction, newPostAbstraction, loopConExp, existingInvs, sPostAbs, vPostAbs).distinctBy(_.toString) //if (loopConExp == loopCons.head) { + println("-------------------------------------------------------------------") println("Invariants:\n " + res.mkString("\n ")) + println("-------------------------------------------------------------------") //} 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 - val allNewChunks = abdReses.map(abd => (abd.allNewChunks, abd.pcs.branchConditions)) - val matchingPreChunks = allNewChunks.collect { case (chunks, bcs) if bcs.diff(vPostAbs.decider.pcs.branchConditions).isEmpty => chunks }.flatten - solveLoopInvariants(sPostAbs, vPostAbs, origVars, loopHead, loopEdges, joinPoint, initialBcs, q.copy(preHeap = newPreState.h + Heap(matchingPreChunks), preAbstraction = newPreAbstraction, + // val allNewChunks = abdReses.map(abd => (abd.allNewChunks, abd.pcs.branchConditions)) + // val matchingPreChunks = allNewChunks.collect { case (chunks, bcs) if bcs.diff(vPostAbs.decider.pcs.branchConditions).isEmpty => chunks }.flatten + + // We need to merge chunks that refer to the same value but have different snaps (?) + val preChunks = abdReses + .map(abd => (abd.allNewChunks, abd.pcs.branchConditions)) + .flatMap { case (chunks, bcs) => chunks.map(chunk => (chunk, bcs)) } + .filter { case (_, bcs) => bcs.diff(vPostAbs.decider.pcs.branchConditions).isEmpty } + .groupBy { case (chunk, _) => (chunk.id, chunk.args) } + .map { case (_, grouped) => + val (bestChunk, _) = grouped.tail.foldLeft(grouped.head) { case ((accChunk, accPcs), (chunk, pcs)) => + if (vPostAbs.decider.check(AtLeast(accChunk.perm, chunk.perm), Verifier.config.checkTimeout())) + (accChunk, accPcs) + else + (chunk, pcs) + } + bestChunk + } + .toList + solveLoopInvariants(sPostAbs, vPostAbs, origVars, loopHead, loopEdges, joinPoint, initialBcs, q.copy(preHeap = newPreState.h + Heap(preChunks), preAbstraction = newPreAbstraction, postAbstraction = newPostAbstraction), iteration = iteration + 1) } } diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index 0d367eaab..cdf50dedb 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -1,45 +1,61 @@ package viper.silicon.biabduction +import org.checkerframework.checker.units.qual.m import viper.silicon.interfaces.state.NonQuantifiedChunk import viper.silicon.resources.{FieldID, PredicateID} import viper.silicon.rules.chunkSupporter.findChunk -import viper.silicon.state.terms.{BuiltinEquals, Null, Term, Var} +import viper.silicon.state.terms.{BuiltinEquals, Combine, Null, SortWrapper, Term, Var, Unit} import viper.silicon.state._ +import viper.silicon.state.terms.sorts.Perm import viper.silicon.utils.ast.{BigAnd, BigOr} import viper.silicon.verifier.Verifier import viper.silver.ast +import viper.silver.ast.{AbstractLocalVar, Exp, Field, FieldAccess, FieldAccessPredicate, FractionalPerm, LocationAccess, PermExp, PredicateAccessPredicate} import scala.annotation.tailrec +import scala.collection.immutable.TreeSeqMap -case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap, newFieldChunks: Map[BasicChunk, ast.LocationAccess] = Map(), otherVars: Map[ast.AbstractLocalVar, (Term, Option[ast.Exp])] = Map()) { +case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocalVar, (Term, Option[ast.Exp])], + targetHeap: Heap, newFieldChunks: Map[BasicChunk, ast.LocationAccess] = Map(), + otherVars: Map[ast.AbstractLocalVar, (Term, Option[ast.Exp])] = Map()) { - //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, ast.Exp] = resolveMatches() + var matches: Map[Term, ast.Exp] = resolveMatches() val newChunkBySnap = newFieldChunks.map { case (c, fa: ast.FieldAccess) => c.snap -> (c, fa) } private def resolveMatches(): Map[Term, ast.Exp] = { + def extractSnapTerms(snap: Term): Seq[Term] = snap match { + case Combine(s1, s2) => + extractSnapTerms(s1) ++ extractSnapTerms(s2) + case SortWrapper(t, _) => + extractSnapTerms(t) + case terms.Unit => + Seq.empty + case t => + Seq(t) + } + val allTerms: Seq[Term] = (s.g.values.values.map { case (t1, _) => t1 } ++ s.h.values.collect { case c: BasicChunk if c.resourceID == FieldID => Seq(c.args.head, c.snap) - case c: BasicChunk if c.resourceID == PredicateID => c.args + case c: BasicChunk if c.resourceID == PredicateID => c.args ++ extractSnapTerms(c.snap) }.flatten ++ prefVars.values.map(_._1) ++ otherVars.values.map(_._1) - ++ v.decider.pcs.branchConditions.collect { case t => t.subterms.collect { case tVar: Var => tVar } }.flatten).toSeq.distinct + ++ v.decider.pcs.branchConditions.collect { case t => t.subterms.collect { case tVar: Var => tVar } }.flatten + ).toSeq.distinct + // The symbolic values of the target vars in the store. Everything else is an attempt to match things to these terms - //val targetMap: Map[Term, AbstractLocalVar] = targets.view.map(localVar => s.g.get(localVar).get -> localVar).toMap + // val targetMap: Map[Term, AbstractLocalVar] = targets.view.map(localVar => s.g.get(localVar).get -> localVar).toMap val directPrefTargets = prefVars.map{case (lv, (t, _)) => t -> lv} //++ Map(terms.Null -> ast.NullLit()()) - val directTargets = directPrefTargets ++ otherVars.map{case (lv, (t, _)) => t -> lv}.filter { case (t, _) => !directPrefTargets.contains(t) } - val directAliases = allTerms.map { t => t -> directTargets.collectFirst { case (t1, e) if t.sort == t1.sort && v.decider.check(BuiltinEquals(t, t1), Verifier.config.checkTimeout()) => e } }.collect { case (t2, Some(e)) => t2 -> e }.toMap - val chunksToResolve = targetHeap.values.collect { case c: BasicChunk if c.resourceID == FieldID && !(directAliases.contains(c.args.head) && directAliases.contains(c.snap)) && c.snap != Null => c }.toSeq @@ -58,17 +74,117 @@ case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocal } } + def permExpToTerm(permExp: Exp): Term = { + + def binPermOp(e1: Exp, e2: Exp, op: (Term, Term) => Term): Term = { + op(permExpToTerm(e1), permExpToTerm(e2)) + } + + val ret = permExp match { + case ast.IntLit(n) => + terms.IntLiteral(n) + case ast.FullPerm() => + terms.FullPerm + case ast.NoPerm() => + terms.NoPerm + case ast.WildcardPerm() => + val arp = v.decider.freshARP("abductionWC") + v.decider.assume(arp._2, None, None) + arp._1 + case ast.FractionalPerm(ast.IntLit(e1), ast.IntLit(e2)) => + terms.FractionPerm((terms.IntLiteral(e1), terms.IntLiteral(e2))) + case ast.PermMul(e1, e2) => + binPermOp(e1, e2, terms.PermTimes(_, _)) + case ast.PermSub(e1, e2) => + binPermOp(e1, e2, terms.PermMinus(_, _)) + case ast.PermAdd(e1, e2) => + binPermOp(e1, e2, terms.PermPlus(_, _)) + case ast.PermDiv(e1, e2) => + binPermOp(e1, e2, terms.PermPermDiv(_, _)) + case ast.PermPermDiv(e1, e2) => + binPermOp(e1, e2, terms.PermPermDiv(_, _)) + case _ => throw new IllegalStateException(s"permExpToTerm can't transform $permExp") + } + ret + } + + // This function assumes that prefVars are the Vars in the precondition(s) and + // targetHeap is the heap in the precondition(s) + // prefVars: Map[ast.AbstractLocalVar, (Term, Option[ast.Exp])] + /*def mergePreconditions(oldPres: Seq[Exp], newPres: Seq[Exp]): Seq[Exp] = { + + def resolveAlias(rcv: Exp): Option[Exp] = + rcv match { + case v: AbstractLocalVar => + prefVars + .get(v) + .flatMap { case (t, _) => matches.get(t) } + case _ => None + } + + val fapInNewPres: Set[(Exp, Field)] = newPres.collect { + case FieldAccessPredicate(FieldAccess(rcv, field), _) => (rcv, field) + }.toSet + + val filteredOldPres = + oldPres.filterNot { + case FieldAccessPredicate(FieldAccess(rcvB, fieldB), _) => + resolveAlias(rcvB) + .exists { aliasedRcv => + fapInNewPres.contains((aliasedRcv, fieldB)) + } + case e => + false + } + + + + val merged: Seq[Exp] = newPres ++ filteredOldPres + merged + }*/ + def transformTerm(t: Term): Option[ast.Exp] = { - t match { - case t if matches.contains(t) => matches.get(t) + def binPermOp(t1: terms.Term, t2: terms.Term, identity: ast.Exp, op: (ast.Exp, ast.Exp) => ast.Exp): Option[ast.Exp] = { + val exp1 = transformTerm(t1).getOrElse(ast.FullPerm()()) + val exp2 = transformTerm(t2).getOrElse(ast.FullPerm()()) + + (exp1, exp2) match { + case (ast.WildcardPerm(), _) => + Some(ast.WildcardPerm()()) + case (_, ast.WildcardPerm()) => + Some(ast.WildcardPerm()()) + case _ => + Some(op(exp1, exp2)) + } + } + + (t match { + case terms.Null => + Some(ast.NullLit()()) + case t if matches.contains(t) => + matches.get(t) case BuiltinEquals(t1, t2) => (transformTerm(t1), transformTerm(t2)) match { case (Some(e1), Some(e2)) => Some(ast.EqCmp(e1, e2)()) case _ => None } + case v@terms.Var(_) if v.isWildcard => Some(ast.WildcardPerm()()) + // FIXME: This is probably wrong + case terms.PermMin(t1, t2) => + val e1 = transformTerm(t1) + val e2 = transformTerm(t2) + val minP = abductionUtils.minPermRational(e1, e2) + Some(ast.FractionalPerm(ast.IntLit(minP.numerator)(), ast.IntLit(minP.denominator)())()) + case terms.FractionPermLiteral(r) => Some(ast.FractionalPerm(ast.IntLit(r.numerator)(), ast.IntLit(r.denominator)())()) case terms.FullPerm => Some(ast.FullPerm()()) + case terms.NoPerm => Some(ast.NoPerm()()) + case terms.PermTimes(t1, t2) => binPermOp(t1, t2, ast.FullPerm()(), ast.PermMul(_, _)()) + case terms.PermPermDiv(t1, t2) => binPermOp(t1, t2, ast.FullPerm()(), ast.PermPermDiv(_, _)()) + case terms.FractionPerm(t1, t2) => binPermOp(t1, t2, ast.FullPerm()(), ast.PermDiv(_, _)()) + case terms.PermMinus(t1, t2) => binPermOp(t1, t2, ast.NoPerm()(), ast.PermSub(_, _)()) + case terms.PermPlus(t1, t2) => binPermOp(t1, t2, ast.NoPerm()(), ast.PermAdd(_, _)()) case terms.Null => Some(ast.NullLit()()) case terms.Not(t1) => transformTerm(t1).flatMap(e1 => Some(ast.Not(e1)())) case terms.Not(BuiltinEquals(t1, t2)) => (transformTerm(t1), transformTerm(t2)) match { @@ -86,34 +202,45 @@ case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocal case or: terms.Or => val subs = or.ts.map(transformTerm) if (subs.contains(None)) None else Some(BigOr(subs.map(_.get))) - /* - case app: terms.App => - app.applicable match { - case df: terms.DomainFun => - val args = app.args.map(transformTerm) - if (args.contains(None)) None else { - val funcName = df.id.name.split('[').head - val domFunc = s.program.domainFunctionsByName.get(funcName) - Some(ast.DomainFuncApp(domFunc.get, args.map(_.get), Map())()) - } - - case _ => - val args = app.args.tail.map(transformTerm) - if (args.contains(None)) None else { - val funcName = app.applicable.id.name - val func = s.program.functionsByName.get(funcName) - Some(ast.FuncApp(func.get, args.map(_.get))()) - } - } - */ case sl: terms.SeqLength => transformTerm(sl.p).flatMap(e => Some(ast.SeqLength(e)())) case sa: terms.SeqAt => (transformTerm(sa.p0), transformTerm(sa.p1)) match { case (Some(e0), Some(e1)) => Some(ast.SeqIndex(e0, e1)()) case _ => None } case terms.IntLiteral(n) => Some(ast.IntLit(n)()) - case _ => None - } + case terms.Greater(t1, t2) =>(transformTerm(t1), transformTerm(t2)) match { + case (Some(e1), Some(e2)) => + Some(ast.GtCmp(e1, e2)()) + case (_, None) => None + case (None, _) => None + } + case terms.AtLeast(t1, t2) =>(transformTerm(t1), transformTerm(t2)) match { + case (Some(e1), Some(e2)) => + Some(ast.GeCmp(e1, e2)()) + case (_, None) => None + case (None, _) => None + } + case terms.AtMost(t1, t2) =>(transformTerm(t1), transformTerm(t2)) match { + case (Some(e1), Some(e2)) => + Some(ast.LeCmp(e1, e2)()) + case (_, None) => None + case (None, _) => None + } + case terms.Less(t1, t2) =>(transformTerm(t1), transformTerm(t2)) match { + case (Some(e1), Some(e2)) => + Some(ast.LtCmp(e1, e2)()) + case (_, None) => None + case (None, _) => None + } + // Delay this case as much as possible as it is expensive + /*case t if matches.exists { case (key, _) => key.sort == t.sort && v.decider.check(key === t, Verifier.config.checkTimeout()) } => + matches.collectFirst { + case (key, value) if key.sort == t.sort && v.decider.check(key === t, Verifier.config.checkTimeout()) => value + }*/ + case e => + None + }).map(abductionUtils.simplifyPermission) + } def transformState(s: State): Seq[ast.Exp] = { @@ -146,7 +273,7 @@ case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocal val expBindings = mwc.bindings.collect { case (lv, (term, _)) if rcvs.contains(term) => lv -> rcvs(term).get } val instantiated = shape.replace(expBindings) Some(instantiated) - //Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get)) + // Some(abductionUtils.getPredicate(s.program, rcv.get, transformTerm(b.perm).get)) } } } @@ -169,11 +296,11 @@ case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocal } } - def transformExp(e: ast.Exp, strict: Boolean = true): Option[ast.Exp] = { + def transformExp(e: ast.Exp, strict: Boolean = true, onlyInner: Boolean = false): Option[ast.Exp] = { try { val res = e.transform { - // We do not want to resolve things to fields accesses for wands, as that would not be self-framing + // We do not want to resolve things to fields accesses for wands, as that would not be self-framing case ast.MagicWand(left: ast.AbstractLocalVar, right: ast.AbstractLocalVar) => val leftT = s.g.values(left)._1 val rightT = s.g.values(right)._1 @@ -184,35 +311,30 @@ case class VarTransformer(s: State, v: Verifier, prefVars: Map[ast.AbstractLocal ast.MagicWand(leftE, rightE)() case ast.FieldAccessPredicate(fa, perm) => - // We do not want to transform the entire field access, this would resolve the snap! val newRcv = transformExp(fa.rcv).get ast.FieldAccessPredicate(ast.FieldAccess(newRcv, fa.field)(), perm)() case fa@ast.FieldAccess(target, field) => - // We do not get the guarantee that the chunks exist in the current state, so we can not evaluate them - // directly - safeEval(fa) match { - // If the chunk exists in the current state, then we want to match the snap term - case Some(term) => - val existingChunkTerm = transformTerm(term) - existingChunkTerm match { - case Some(nfa: ast.FieldAccess) => nfa - - case Some(ast.NullLit()) | Some(ast.LocalVar(_, _)) | None => - val rvcExp = transformExp(target) - ast.FieldAccess(rvcExp.get, field)() - - // TODO nklose this wrong sometimes? - // Specifically I think if we are transforming "in-place" then this is fine, - // but if we are transforming "into the past" then this can be wrong because the - // old value of the field is not necessarily equal to the new value - - } - // Else we want to recurse and try to match the target - case None => - val rvcExp = transformExp(target) - ast.FieldAccess(rvcExp.get, field)() + if (onlyInner && target.isInstanceOf[ast.FieldAccess]) { + val rvcExp = transformExp(target) + ast.FieldAccess(rvcExp.get, field)() + } else { + safeEval(fa) match { + case Some(term) => + val existingChunkTerm = transformTerm(term) + existingChunkTerm match { + case Some(nfa: ast.FieldAccess) => + nfa + + case Some(ast.NullLit()) | Some(ast.LocalVar(_, _)) | None => + val rvcExp = transformExp(target) + ast.FieldAccess(rvcExp.get, field)() + } + case None => + val rvcExp = transformExp(target) + ast.FieldAccess(rvcExp.get, field)() + } } case lv: ast.LocalVar => { val term: Term = s.g.values.getOrElse(lv, (prefVars ++ otherVars)(lv))._1 diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index fae549871..2b9f711ac 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -243,6 +243,7 @@ object consumer extends ConsumptionRules { * and producer. Try to unify the code. */ case QuantifiedPermissionAssertion(forall, cond, acc: ast.FieldAccessPredicate) => + println(s"EVALUATING QP $acc") val field = acc.loc.field val qid = BasicChunkIdentifier(acc.loc.field.name) val optTrigger = @@ -276,12 +277,13 @@ object consumer extends ConsumptionRules { pve = pve, negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), - insufficientPermissionReason = InsufficientPermission(acc.loc), + insufficientPermissionReason = InsufficientPermission(acc.loc, Some(acc.permExp.getOrElse(ast.FullPerm()(acc.pos, acc.info, acc.errT)))), v1)((s2, h2, snap, v2) => Q(s2.copy(constrainableARPs = s.constrainableARPs), h2, snap, v2)) case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) => + println(s"EVALUATING QP $acc") val predicate = s.program.findPredicate(acc.loc.predicateName) /* TODO: Quantified codomain variables are used in axioms and chunks (analogous to `?r`) * and need to be instantiated in several places. Hence, they need to be known, @@ -322,7 +324,7 @@ object consumer extends ConsumptionRules { pve = pve, negativePermissionReason = NegativePermission(acc.perm), notInjectiveReason = QPAssertionNotInjective(acc.loc), - insufficientPermissionReason = InsufficientPermission(acc.loc), + insufficientPermissionReason = InsufficientPermission(acc.loc, Some(acc.permExp.getOrElse(ast.FullPerm()(acc.pos, acc.info, acc.errT)))), v1)((s2, h2, snap, v2) => Q(s2.copy(constrainableARPs = s.constrainableARPs), h2, snap, v2)) case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1) } @@ -471,7 +473,7 @@ object consumer extends ConsumptionRules { else WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor) val lossExp = permNew.map(p => ast.PermMul(p, s3.permissionScalingFactorExp.get)(p.pos, p.info, p.errT)) - val ve = pve dueTo InsufficientPermission(locacc) + val ve = pve dueTo InsufficientPermission(locacc, Some(perm)) val description = s"consume ${a.pos}: $a" chunkSupporter.consume(s3, h, resource, tArgs, eArgs, loss, lossExp, returnSnap, ve, v3, description)((s4, h1, snap1, v4) => { val s5 = s4.copy(partiallyConsumedHeap = Some(h1), diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 7e4db4a22..39535035f 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -23,7 +23,7 @@ import viper.silicon.utils.toSf import viper.silicon.verifier.Verifier import viper.silicon.{Map, TriggerSets} import viper.silver.ast -import viper.silver.ast.{AnnotationInfo, LocalVarWithVersion, TrueLit, WeightedQuantifier} +import viper.silver.ast.{AnnotationInfo, LocalVarWithVersion, TrueLit, WeightedQuantifier, WildcardPerm} import viper.silver.reporter.{AnnotationWarning, WarningsDuringVerification} import viper.silver.utility.Common.Rational import viper.silver.verifier.errors.{ErrorWrapperWithTransformers, PreconditionInAppFalse} @@ -272,7 +272,7 @@ object evaluator extends EvaluationRules { val toAssert = IsPositive(totalPermissions.replace(`?r`, tRcvr)) v1.decider.assert(toAssert) { case false => - createFailure(pve dueTo InsufficientPermission(fa), v1, s1, toAssert, Option.when(withExp)(perms.IsPositive(ast.CurrentPerm(fa)())())) + createFailure(pve dueTo InsufficientPermission(fa, Some(WildcardPerm()(fa.pos, fa.info, fa.errT))), v1, s1, toAssert, Option.when(withExp)(perms.IsPositive(ast.CurrentPerm(fa)())())) case true => val fvfLookup = Lookup(fa.field.name, fvfDef.sm, tRcvr) val fr1 = s1.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, fvfLookup).recordFvfAndDomain(fvfDef) @@ -302,7 +302,7 @@ object evaluator extends EvaluationRules { } v1.decider.assert(permCheck) { case false => - createFailure(pve dueTo InsufficientPermission(fa), v1, s1, permCheck, permCheckExp) + createFailure(pve dueTo InsufficientPermission(fa, Some(WildcardPerm()(fa.pos, fa.info, fa.errT))), v1, s1, permCheck, permCheckExp) case true => val smLookup = Lookup(fa.field.name, relevantChunks.head.fvf, tRcvr) val fr2 = @@ -334,7 +334,7 @@ object evaluator extends EvaluationRules { } v1.decider.assert(permCheck) { case false => - createFailure(pve dueTo InsufficientPermission(fa), v1, s2, permCheck, permCheckExp) + createFailure(pve dueTo InsufficientPermission(fa, Some(WildcardPerm()(fa.pos, fa.info, fa.errT))), v1, s2, permCheck, permCheckExp) case true => val smLookup = Lookup(fa.field.name, smDef1.sm, tRcvr) val fr2 = @@ -348,7 +348,7 @@ object evaluator extends EvaluationRules { case fa: ast.FieldAccess => evalLocationAccess(s, fa, pve, v)((s1, _, tArgs, eArgs, v1) => { - val ve = pve dueTo InsufficientPermission(fa) + val ve = pve dueTo InsufficientPermission(fa, Some(WildcardPerm()(fa.pos, fa.info, fa.errT))) val resource = fa.res(s.program) chunkSupporter.lookup(s1, s1.h, resource, tArgs, eArgs, ve, v1)((s2, h2, tSnap, v2) => { val fr = s2.functionRecorder.recordSnapshot(fa, v2.decider.pcs.branchConditions, tSnap) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 414be524c..142d634e7 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -70,7 +70,6 @@ object executor extends ExecutionRules { val s1 = handleOutEdge(s, edge, v) //executionFlowController.tryOrElse2[Term, Option[Exp]](s1, v) {(s1a, va, R) => evalWithAbduction(s1, ce.condition, IfFailed(ce.condition), v) {(s2, tCond, condNew, v1) => - /* Using branch(...) here ensures that the edge condition is recorded * as a branch condition on the pathcondition stack. */ @@ -114,12 +113,12 @@ object executor extends ExecutionRules { } def follows(s: State, - edges: Seq[SilverEdge], - @unused pvef: ast.Exp => PartialVerificationError, - v: Verifier, - joinPoint: Option[SilverBlock]) - (Q: (State, Verifier) => VerificationResult) - : VerificationResult = { + edges: Seq[SilverEdge], + @unused pvef: ast.Exp => PartialVerificationError, + v: Verifier, + joinPoint: Option[SilverBlock]) + (Q: (State, Verifier) => VerificationResult) + : VerificationResult = { // If joining branches is enabled, find join point if it exists. val jp: Option[SilverBlock] = if (s.moreJoins.id >= JoinMode.All.id) { @@ -300,7 +299,8 @@ object executor extends ExecutionRules { (allInvs, Success(Some(LoopInvariantSuccess(s, v, allInvs, invSucs.head.loop, v.decider.pcs.duplicate())))) case Seq() if !s.doAbduction => (Seq(), Success()) } - val invs = abductionUtils.sortExps(foundInvs ++ existingInvs) + // We need the distinct here because there is some duplication of existing Invariants otherwise + val invs = abductionUtils.sortExps(foundInvs ++ existingInvs).distinctBy(_.toString) type PhaseData = (State, RecordedPathConditions, Set[FunctionDecl]) var phase1data: Vector[PhaseData] = Vector.empty @@ -392,8 +392,9 @@ object executor extends ExecutionRules { Q(s2, v2) } { f => - BiAbductionSolver.solveAbductionForError(s, v, f, stateAllowed, Some(location))((s3, v3) => - checkInvariants(s3, v3, invs, location, stateAllowed)(Q)) + BiAbductionSolver.solveAbductionForError(s, v, f, stateAllowed, Some(location)) { (s3, v3) => + checkInvariants(s3, v3, invs, location, stateAllowed)(Q) + } } } } @@ -531,7 +532,7 @@ object executor extends ExecutionRules { val s5 = if (withExp) s4.copy(oldHeaps = s4.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s4))) else s4 Q(s5, v2) case (Incomplete(_, _), s3, _) => - createFailure(pve dueTo InsufficientPermission(fa), v2, s3, "sufficient permission")}})) + createFailure(pve dueTo InsufficientPermission(fa, Some(ast.FullPerm()(fa.pos, fa.info, fa.errT))), v2, s3, "sufficient permission")}})) case ass @ ast.FieldAssign(fa @ ast.FieldAccess(eRcvr, field), rhs) => assert(!s.exhaleExt) @@ -539,7 +540,7 @@ object executor extends ExecutionRules { eval(s, eRcvr, pve, v)((s1, tRcvr, eRcvrNew, v1) => eval(s1, rhs, pve, v1)((s2, tRhs, rhsNew, v2) => { val resource = fa.res(s.program) - val ve = pve dueTo InsufficientPermission(fa) + val ve = pve dueTo InsufficientPermission(fa, Some(ast.FullPerm()(fa.pos, fa.info, fa.errT))) val description = s"consume ${ass.pos}: $ass" chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), eRcvrNew.map(Seq(_)), FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), false, ve, v2, description)((s3, h3, _, v3) => { val (tSnap, _) = ssaifyRhs(tRhs, rhs, rhsNew, field.name, field.typ, v3, s3) @@ -728,7 +729,10 @@ object executor extends ExecutionRules { val wildcards = s3.constrainableARPs -- s1.constrainableARPs predicateSupporter.fold(s3, predicate, tArgs, eArgsNew, tPerm, ePermNew, wildcards, pveFoldTransformed, v3)((s4, v4) => { v3.decider.finishDebugSubExp(s"folded ${predAcc.toString}") - Q(s4, v4) + val s5 = s4.copy(reservedForFoldUnfold = + s4.reservedForFoldUnfold.filterNot { case (exp, _) => exp == pap } + ) + Q(s5, v4) } )}))) diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 0dee65344..c0bc8dc37 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -392,6 +392,8 @@ object magicWandSupporter extends SymbolicExecutionRules { */ assert(stackSize == s2.reserveHeaps.length) + // Execute proof script, i.e. the part written after the magic wand wrapped by curly braces. + // The proof script should transform the current state such that we can consume the wand's RHS. // Execute proof script, i.e. the part written after the magic wand wrapped by curly braces. // The proof script should transform the current state such that we can consume the wand's RHS. executor.exec(s2, proofScriptCfg, v2)((proofScriptState, proofScriptVerifier) => { @@ -405,6 +407,31 @@ object magicWandSupporter extends SymbolicExecutionRules { createWandChunkAndRecordResults(s3.copy(exhaleExt = false, oldHeaps = s.oldHeaps, doAbduction = s.doAbduction), freshSnapRoot, snapRhs.get, v3) }) }) + // We attempt executing the stmts one by one, this way if we fail for an assertion we will capture it and + // produce it? + /*def execStmtsWithAbd(stmts: Seq[Stmt], s: State, v: Verifier)(Q: (State, Verifier) => VerificationResult): VerificationResult = { + stmts match { + case Nil => Q(s, v) + case stmt +: rest => + println(s"Will execute $stmt") + println(s"Before stmt: \n${s.reserveHeaps.zipWithIndex.map { case (h, i) => s"[$i] ${h.values.mkString(", ")}" }.mkString("\n")}") + executor.exec(s.copy(doAbduction = true), stmt, v) { (s1, v1) => + println(s"After stmt: \n${s1.reserveHeaps.zipWithIndex.map { case (h, i) => s"[$i] ${h.values.mkString(", ")}" }.mkString("\n")}") + execStmtsWithAbd(rest, s1, v1)(Q) + } + } + }*/ + /*execStmtsWithAbd(proofScript.ss, s2, v2)((proofScriptState, proofScriptVerifier) => { + // Consume the wand's RHS and produce a snapshot which records all the values of variables on the RHS. + // This part indirectly calls the methods `this.transfer` and `this.consumeFromMultipleHeaps`. + consume( + proofScriptState.copy(oldHeaps = s2.oldHeaps, reserveCfgs = proofScriptState.reserveCfgs.tail), + wand.right, true, pve, proofScriptVerifier + )((s3, snapRhs, v3) => { + + createWandChunkAndRecordResults(s3.copy(exhaleExt = false, oldHeaps = s.oldHeaps, doAbduction = s.doAbduction), freshSnapRoot, snapRhs.get, v3) + }) + })*/ }) }) diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala index 7a0f814c1..7e94f5208 100644 --- a/src/main/scala/rules/PredicateSupporter.scala +++ b/src/main/scala/rules/PredicateSupporter.scala @@ -178,7 +178,7 @@ object predicateSupporter extends PredicateSupportRules { v2)}) }) } else { - val ve = pve dueTo InsufficientPermission(pa) + val ve = pve dueTo InsufficientPermission(pa, Some(ePerm.getOrElse(ast.FullPerm()(pa.pos, pa.info, pa.errT)))) val description = s"consume ${pa.pos}: $pa" chunkSupporter.consume(s1, s1.h, predicate, tArgs, eArgs, s1.permissionScalingFactor, s1.permissionScalingFactorExp, true, ve, v, description)((s2, h1, snap, v1) => { val s3 = s2.copy(g = gIns, h = h1) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index 084dbf72f..b7809944d 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -110,7 +110,7 @@ object producer extends ProductionRules { : VerificationResult = { if(!withAbduction){ - produceR(s, sf, a.whenInhaling, pve, v)(Q) + produceR(s, sf, a.whenInhaling, pve, v)(Q) } else { executionFlowController.tryOrElse0(s, v) { (s1, v1, T) => produceR(s1, sf, a.whenInhaling, pve, v1)(T) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 3637b49e4..bc4f974df 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1430,7 +1430,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { if (s.exhaleExt) { val failure = resourceAccess match { - case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s, "single QP consume inside package") + + case locAcc: ast.LocationAccess => + println(s"ERROR AT $locAcc") + createFailure(pve dueTo InsufficientPermission(locAcc, Some(permissionsExp.getOrElse(ast.FullPerm()(locAcc.pos, locAcc.info, locAcc.errT)))), v, s, "single QP consume inside package") case wand: ast.MagicWand => createFailure(pve dueTo MagicWandChunkNotFound(wand), v, s, "single QP consume inside package") case _ => sys.error(s"Found resource $resourceAccess, which is not yet supported as a quantified resource.") } @@ -1522,7 +1525,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { } case (Incomplete(_, _), _, _) => resourceAccess match { - case locAcc: ast.LocationAccess => createFailure(pve dueTo InsufficientPermission(locAcc), v, s, "single QP consume") + case locAcc: ast.LocationAccess => + println(s"ERROR AT $locAcc") + createFailure(pve dueTo InsufficientPermission(locAcc, Some(permissionsExp.getOrElse(ast.FullPerm()(locAcc.pos, locAcc.info, locAcc.errT)))), v, s, "single QP consume") case wand: ast.MagicWand => createFailure(pve dueTo MagicWandChunkNotFound(wand), v, s, "single QP consume") case _ => sys.error(s"Found resource $resourceAccess, which is not yet supported as a quantified resource.") } diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 222939308..444170e12 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -38,6 +38,31 @@ final case class State(g: Store = Store(), doAbduction: Boolean = false, abductionResults: Seq[BiAbductionResult] = Seq(), + // Needed for tracking in fractional abduction + abdPermScalingFactorExp: ast.Exp = ast.FullPerm()(), + // This we need for a tricky problem: + // When we try to package a wand like pkg X --* Y { unfold U fold F } + // And to fold F we need an assertion that we previously (when producing X in the state) + // produced into the state + // and this assertion needs some permissions that are obtained by unfolding U + // then we must track that we can produce this assertion while executing the pkg script + // We needed this because the pkg script was executed as one singular cfg + // We must "remember" that we can produce it + // OUTDATED BECAUSE I [amherz] modified package to execute stmt by stmt + // produceableAssertions: Seq[ast.Exp] = Seq.empty, + + // We need to keep track of the predicate that we are reserved and of what we have produced while reserved + // it. This way, if we fold nodes(curr.next) by folding away curr.next.prev, we will not try to unfold it when + // trying to abduce curr.next.prev again. + // The same thing happens the other way around: if we produce curr.next.prev + reservedForFoldUnfold: Seq[(ast.Exp, Seq[ast.Exp])] = Seq.empty, + // A similar problem as above can rise when checking invariants as well + // If we need an invariant nodes(curr + reservedForInvariants: Seq[ast.Exp] = Seq.empty, + // Here we store the LHS of a wand we might be trying to package in abstraction, we need to + // not unfold it if we're looking for a field. Would this ever happen in practice? + packaging: Option[ast.Exp] = None, + recordVisited: Boolean = false, visited: List[ast.Predicate] = Nil, /* TODO: Use a multiset instead of a list */ @@ -126,6 +151,10 @@ final case class State(g: Store = Store(), copy(permissionScalingFactor = terms.PermTimes(p, permissionScalingFactor), permissionScalingFactorExp = permissionScalingFactorExp.map(psf => ast.PermMul(exp.get, psf)(exp.get.pos, exp.get.info, exp.get.errT))) + def scalePermissionFactorAbd(exp: ast.Exp) = + copy( + abdPermScalingFactorExp = ast.PermMul(exp, abdPermScalingFactorExp)()) + def merge(other: State): State = State.merge(this, other) @@ -169,6 +198,7 @@ object State { parallelizeBranches1, doAbduction1, abductionResults1, + abdPermScalingFactorExp1, reservedForUnfold1, reservedForInvariants1, packaging1, recordVisited1, visited1, methodCfg1, invariantContexts1, constrainableARPs1, @@ -196,6 +226,7 @@ object State { `parallelizeBranches1`, `doAbduction1`, `abductionResults1`, + `abdPermScalingFactorExp1`, `reservedForUnfold1`, `reservedForInvariants1`, `packaging1`, `recordVisited1`, `visited1`, `methodCfg1`, `invariantContexts1`, constrainableARPs2, @@ -329,6 +360,7 @@ object State { parallelizeBranches1, doAbduction1, abductionResults1, + abdPermScalingFactorExp1, reservedForUnfold1, reservedForInvariants1, packaging1, recordVisited1, visited1, methodCfg1, invariantContexts1, constrainableARPs1, @@ -355,6 +387,7 @@ object State { `parallelizeBranches1`, `doAbduction1`, `abductionResults1`, + `abdPermScalingFactorExp1`, `reservedForUnfold1`, `reservedForInvariants1`, `packaging1`, `recordVisited1`, `visited1`, `methodCfg1`, invariantContexts2, constrainableARPs2, diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index ebc12318a..af2a6e728 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -126,6 +126,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { } val ex = executionFlowController.locally(s2a, v2)((s3, v3) => { exec(s3, body, v3) { (s4, v4) => { + if(sInit.doAbduction) { 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) } @@ -148,7 +149,8 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { BiAbductionSolver.solveAbductionForError(s1, v1, f, stateAllowed = true, None)((_, _) => { Success() }) match { - case _: FatalResult => f + case _: FatalResult => + f case nf: NonFatalResult => val reses = abductionUtils.getAbductionSuccesses(nf) // We can't abduce statement for preconditions @@ -171,13 +173,11 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { 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 mAbd = resolveAbductionResults(mFail, suc) val mInv = mAbd.flatMap(m2 => resolveLoopInvResults(m2, suc)) val mFrame = mInv.flatMap(someM => resolveFramingResults(someM, suc)) - mFrame match { case None => Seq(Failure(Internal(reason = InternalReason(DummyNode, "Resolving Biabduction results failed")))) case Some(m) => diff --git a/src/test/resources/fractionalAbduction/dl/dl.vpr b/src/test/resources/fractionalAbduction/dl/dl.vpr new file mode 100644 index 000000000..b23f747ff --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl.vpr @@ -0,0 +1,22 @@ +field next: Ref +field prev: Ref + +predicate nodes(this: Ref) { + acc(this.next) && acc(this.prev, 1/2) && + (this.next != null ==> + nodes(this.next) && + acc(this.next.prev, 1/2) && + this.next.prev == this + ) +} + +field head: Ref + +predicate dllist(this: Ref) { + acc(this.head) && + (this.head != null ==> + acc(this.head.prev, 1/2) && + this.head.prev == null && + nodes(this.head) + ) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_concat.vpr b/src/test/resources/fractionalAbduction/dl/dl_concat.vpr new file mode 100644 index 000000000..14d148da9 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_concat.vpr @@ -0,0 +1,107 @@ +import "dl.vpr" + +// method dl_concat(list1: Ref, list2: Ref) returns (res: Ref) +// requires dllist(list1) +// requires dllist(list2) +// ensures dllist(res) +// { +// unfold dllist(list2) +// if (list2.head == null) { +// fold dllist(list2) +// res := list1 +// } +// else { +// unfold nodes(list2.head) +// unfold dllist(list1) +// if (list1.head == null) { +// list2.head.prev := null +// fold nodes(list2.head) +// fold dllist(list2) +// res := list2 +// } +// else { +// var curr: Ref := list1.head +// package nodes(curr) --* dllist(list1) { +// fold dllist(list1) +// } +// unfold nodes(curr) +// while (curr.next != null) +// invariant acc(curr.next) && acc(curr.prev, 1/2) +// invariant curr.next != null ==> acc(curr.next.prev, 1/2) && curr.next.prev == curr && nodes(curr.next) +// invariant nodes(curr) --* dllist(list1) +// { +// var ocurr: Ref := curr +// curr := curr.next + +// package nodes(curr) --* dllist(list1) { +// fold nodes(ocurr) +// apply nodes(ocurr) --* dllist(list1) +// } +// unfold nodes(curr) +// } +// curr.next := list2.head +// list2.head.prev := curr + +// fold nodes(list2.head) +// fold nodes(curr) + +// apply nodes(curr) --* dllist(list1) + +// res := list1 +// } +// } +// } + +method dl_concat(list1: Ref, list2: Ref) returns (res: Ref) +requires dllist(list1) +requires dllist(list2) +// ensures dllist(res) +{ + // unfold dllist(list1) + var head1: Ref := list1.head + // unfold dllist(list2) + var head2: Ref := list2.head + var curr: Ref := head1 + + if (head1 == null) { + res := list2 + // fold dllist(res) + } else { + + if (head2 == null) { + res := list1 + // fold dllist(res) + } else { + + // package nodes(curr) --* nodes(head1) + // unfold nodes(curr) + + while (curr.next != null) // unfolding acc(nodes(curr), 1/4) in curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev, 1/2) + invariant curr.next != null ==> acc(nodes(curr.next)) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + // invariant nodes(curr) --* nodes(head1) + { + var ocurr: Ref := curr + curr := curr.next + + // unfold nodes(curr) + // package acc(nodes(curr)) --* acc(nodes(head1)) { + // fold acc(nodes(ocurr)) + // apply acc(nodes(ocurr)) --* acc(nodes(head1)) + // } + } + curr.next := list2.head + // unfold nodes(list2.head) + list2.head.prev := curr + res := list1 + // fold nodes(list2.head) + // fold nodes(curr) + // apply acc(nodes(curr)) --* acc(nodes(head1)) + // fold dllist(res) + list2.head := null + } + } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_copy.vpr b/src/test/resources/fractionalAbduction/dl/dl_copy.vpr new file mode 100644 index 000000000..ce024d245 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_copy.vpr @@ -0,0 +1,111 @@ +import "dl.vpr" + +method copy(list: Ref) returns (cp_list: Ref) +requires dllist(list) +// requires acc(list.head) && acc(list.head.prev) && (list.head.prev == null) +// requires acc(list.head.next) && acc(list.head.next.prev, 1/2) && list.head.next.prev == list.head +// requires acc(dllist(list), 1/4) +// ensures acc(dllist(list), 1/4) && dllist(cp_list) +{ + cp_list := new(head) + // unfold acc(dllist(list), 1/4) + var list_head: Ref := list.head + if (list.head == null) { + // fold acc(dllist(list), 1/4) + cp_list.head := null + // fold dllist(cp_list) + } else { + var curr: Ref := list_head + + var cp: Ref := new(next, prev) + cp.next := null + cp.prev := null + + var cp_head: Ref := cp + cp_list.head := cp_head + + fold nodes(cp) + package nodes(cp) --* nodes(cp_head) + + // package acc(nodes(curr), 1/4) --* acc(nodes(list_head), 1/4) + // unfold acc(nodes(curr), 1/4) + + while (curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev, 1/2) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + invariant curr.next != null ==> acc(nodes(curr.next)) + // invariant nodes(cp) + invariant nodes(cp) --* nodes(cp_head) + // invariant acc(nodes(curr), 1/4) --* acc(nodes(list_head), 1/4) + { + + var ocp: Ref := cp + cp := new(next, prev) + // unfold nodes(ocp) + ocp.next := cp + cp.next := null + cp.prev := ocp + + var ocurr: Ref := curr + curr := curr.next + + // package acc(nodes(curr), 1/4) --* acc(nodes(list_head), 1/4) { + // fold acc(nodes(ocurr), 1/4) + // apply acc(nodes(ocurr), 1/4) --* acc(nodes(list_head), 1/4) + // } + // unfold acc(nodes(curr), 1/4) + + // fold nodes(cp) + package nodes(cp) --* nodes(cp_head) { + fold nodes(ocp) + apply nodes(ocp) --* nodes(cp_head) + } + } + // fold acc(nodes(curr), 1/4) + // apply acc(nodes(curr), 1/4) --* acc(nodes(list_head), 1/4) + // fold acc(dllist(list), 1/4) + // apply nodes(cp) --* nodes(cp_head) + // fold dllist(cp_list) + } + +} + +// var list_head: Ref := list.head +// var curr: Ref := list_head + +// // var cp: Ref := new(*) +// // cp.next := null +// // cp.prev := null + +// // fold nodes(cp) +// package acc(nodes(curr), 1/4) --* acc(nodes(list_head), 1/4) +// unfold acc(nodes(curr), 1/4) + +// while (curr.next != null) +// invariant acc(curr.next, 1/4) +// invariant acc(curr.prev, 1/8) +// invariant curr.next != null ==> acc(curr.next.prev, 1/8) +// invariant curr.next != null ==> curr.next.prev == curr +// invariant curr.next != null ==> acc(nodes(curr.next), 1/4) +// // invariant nodes(cp) +// invariant acc(nodes(curr), 1/4) --* acc(nodes(list_head), 1/4) +// { +// // var ocp: Ref := cp +// // cp := new(*) +// // unfold nodes(ocp) +// // ocp.next := cp +// // cp.next := null +// // cp.prev := ocp + +// var ocurr: Ref := curr +// curr := curr.next + +// package acc(nodes(ocurr), 1/4) --* acc(nodes(list_head), 1/4) { +// fold acc(nodes(ocurr), 1/4) +// apply acc(nodes(ocurr), 1/4) --* acc(nodes(list_head), 1/4) +// } +// // fold nodes(cp) +// unfold acc(nodes(curr), 1/4) +// } \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_dispose.vpr b/src/test/resources/fractionalAbduction/dl/dl_dispose.vpr new file mode 100644 index 000000000..bc7df6653 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_dispose.vpr @@ -0,0 +1,33 @@ +import "dl.vpr" + +method dl_dispose(list: Ref) + // requires acc(dllist(list)) +{ + var ocurr: Ref := new(next, prev) + ocurr.next := null + + // unfold acc(dllist(list)) + var curr: Ref := list.head + + while (curr != null) + // Need the invariant + invariant curr != null ==> acc(nodes(curr)) + { + // unfold acc(nodes(curr)) + ocurr := curr + curr := curr.next + + free(ocurr) + } + + free_head(list) +} + +method free(this: Ref) + requires acc(this.next) && acc(this.prev, 1/2) && + (this.next != null ==> + acc(this.next.prev, 1/2) && + this.next.prev == this) + +method free_head(this: Ref) + requires acc(this.head) \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_filter.vpr b/src/test/resources/fractionalAbduction/dl/dl_filter.vpr new file mode 100644 index 000000000..d392fbaca --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_filter.vpr @@ -0,0 +1,67 @@ +import "dl.vpr" + +method dl_filter(list: Ref) returns (res: Ref) + requires acc(dllist(list)) + // ensures dllist(res) +{ + // unfold acc(dllist(list)) + var list_head: Ref := list.head + + if (list_head == null) { + res := list + // fold dllist(list) + } + else { + // unfold nodes(list_head) + if (list_head.next == null) { + res := list + // fold nodes(list_head) + // fold dllist(res) + } else { + var p: Ref := list_head + var curr: Ref := list_head.next + // unfold nodes(curr) + // package acc(nodes(p)) --* acc(nodes(list_head)) + + while (curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev, 1/2) + invariant curr.next != null ==> acc(nodes(curr.next)) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + invariant acc(p.next) + invariant p.next == curr + // invariant acc(nodes(p)) --* acc(nodes(list_head)) + { + var ocurr: Ref := curr + var old_p: Ref := p + curr := curr.next + // unfold nodes(curr) + + var nondet: Bool + if(nondet) { + p.next := curr; + curr.prev := p + free(ocurr) + } else { + p := ocurr + } + + // if(!nondet){ + // package nodes(p) --* nodes(list_head) { + // fold nodes(old_p) + // apply nodes(old_p) --* nodes(list_head) + // } + // } + } + // fold nodes(curr) + // fold nodes(p) + // apply acc(nodes(p)) --* acc(nodes(list_head)) + res := list + // fold dllist(res) + } + } +} + +method free(this: Ref) + requires acc(this.next) && acc(this.prev) \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_insert.vpr b/src/test/resources/fractionalAbduction/dl/dl_insert.vpr new file mode 100644 index 000000000..3f9b02074 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_insert.vpr @@ -0,0 +1,64 @@ +import "./dl.vpr" + +method insert(list: Ref, elt: Ref) returns (res: Ref) + requires dllist(list) + // ensures dllist(res) +{ + // unfold dllist(list) + var list_head: Ref := list.head + + if (list_head == null) { + res := new(*) + res.prev := null + res.next := null + } else { + var curr: Ref := list_head + var nondet: Bool + + // package nodes(curr) --* nodes(list_head) + // unfold nodes(curr) + + while (nondet && curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev, 1/2) + invariant curr.next != null ==> acc(nodes(curr.next)) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + // invariant acc(nodes(curr)) --* acc(nodes(list_head)) + { + var ocurr: Ref := curr + nondet := havoc() + curr := curr.next + + // unfold nodes(curr) + // package nodes(curr) --* nodes(list_head) { + // fold nodes(ocurr) + // apply nodes(ocurr) --* nodes(list_head) + // } + } + + if (curr.next != null) { + // unfold nodes(elt) + elt.next := curr.next + curr.next := elt + elt.prev := curr + // unfold nodes(elt.next) + elt.next.prev := elt + // fold nodes(elt.next) + // fold nodes(elt) + // fold nodes(curr) + } else { + // unfold nodes(elt) + elt.next := null + curr.next := elt + elt.prev := curr + // fold nodes(elt) + // fold nodes(curr) + } + // apply nodes(curr) --* nodes(list_head) + } + res := list + // fold dllist(res) +} + +method havoc() returns (res: Bool) \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_remove.vpr b/src/test/resources/fractionalAbduction/dl/dl_remove.vpr new file mode 100644 index 000000000..25eea78a1 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_remove.vpr @@ -0,0 +1,47 @@ +import "./dl.vpr" + +method remove(lst: Ref) returns (res: Ref) + requires dllist(lst) +{ + var curr: Ref + var tmp: Ref + var nondet: Bool + // unfold dllist(lst) + var lst_head: Ref := lst.head + + if(lst_head == null){ + res := null + } else { + curr := lst_head + + // package nodes(curr) --* nodes(lst_head) + + while (nondet && curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev, 1/2) + invariant curr.next != null ==> acc(nodes(curr.next)) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + // invariant acc(nodes(curr)) --* acc(nodes(lst_head)) + { + var ocurr: Ref := curr + nondet := havoc() + curr := curr.next + + // package nodes(curr) --* nodes(lst_head) { + // fold nodes(ocurr) + // apply nodes(ocurr) --* nodes(lst_head) + // } + } + tmp := curr.next + if (tmp != null) { + // unfold nodes(tmp) + curr.next := tmp.next + } + // fold nodes(curr) + // apply nodes(curr) --* nodes(lst_head) + res := lst_head + } +} + +method havoc() returns (res: Bool) \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_reverse.vpr b/src/test/resources/fractionalAbduction/dl/dl_reverse.vpr new file mode 100644 index 000000000..d60cd9fc0 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_reverse.vpr @@ -0,0 +1,51 @@ +import "./dl.vpr" + +method dl_reverse(list: Ref) returns (res: Ref) + requires dllist(list) + // ensures dllist(res) +{ + // unfold dllist(list) + var list_head: Ref := list.head + var curr: Ref := list_head + var res_head: Ref := new(next, prev) + res_head.next := null + res_head.prev := null + + if (list_head == null) { + res := list + // fold dllist(res) + } else { + // fold nodes(res_head) + // unfold nodes(curr) + + while (curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev) + invariant curr.next != null ==> acc(nodes(curr.next)) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + // invariant nodes(res_head) + invariant acc(res_head.prev, 1/2) + invariant res_head.prev == null + { + var tmp: Ref := curr + curr := curr.next + + tmp.next := res_head + // unfold nodes(res_head) + res_head.prev := tmp + // fold nodes(res_head) + + res_head := tmp + tmp.prev := null + + fold nodes(res_head) + // unfold nodes(curr) + } + + res := new(head) + res.head := res_head + list.head := null + // fold dllist(res) + } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/dl/dl_traverse.vpr b/src/test/resources/fractionalAbduction/dl/dl_traverse.vpr new file mode 100644 index 000000000..811721401 --- /dev/null +++ b/src/test/resources/fractionalAbduction/dl/dl_traverse.vpr @@ -0,0 +1,38 @@ +import "./dl.vpr" + +method dl_traverse(list: Ref) + // requires dllist(list) + requires acc(list.head) && acc(list.head.prev) && (list.head.prev == null) + requires acc(list.head.next) && acc(list.head.next.prev, 1/2) && list.head.next.prev == list.head + // ensures dllist(list) +{ + var list_head: Ref := list.head + var curr: Ref := list_head + + if (list_head == null) { + // fold dllist(list) + } else { + while (curr.next != null) + invariant acc(curr.next) + // invariant acc(curr.prev, 1/2) + invariant curr.next != null ==> acc(nodes(curr.next)) + invariant curr.next != null ==> acc(curr.next.prev, 1/2) + invariant curr.next != null ==> curr.next.prev == curr + // invariant nodes(curr) --* nodes(list_head) + { + var ocurr: Ref := curr + curr := curr.next + + // unfold nodes(curr) + // package acc(nodes(curr)) --* acc(nodes(list_head)) { + // fold acc(nodes(ocurr)) + // apply acc(nodes(ocurr)) --* acc(nodes(list_head)) + // } + } + + // fold nodes(list2.head) + // fold nodes(curr) + // apply acc(nodes(curr)) --* acc(nodes(list_head)) + // fold dllist(res) + } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/doublelinkedlist.vpr b/src/test/resources/fractionalAbduction/doublelinkedlist.vpr new file mode 100644 index 000000000..a13e69cd6 --- /dev/null +++ b/src/test/resources/fractionalAbduction/doublelinkedlist.vpr @@ -0,0 +1,22 @@ +field next: Ref +field prev: Ref + +predicate nodes(this: Ref) { + acc(this.next) && acc(this.prev, 1/2) && + (this.next != null ==> + acc(this.next.prev, 1/2) && + this.next.prev == this && + nodes(this.next) + ) +} + +field head: Ref + +predicate dlist(this: Ref) { + acc(this.head) && + (this.head != null ==> + acc(this.head.prev, 1/2) && + this.head.prev == null && + nodes(this.head) + ) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test.vpr b/src/test/resources/fractionalAbduction/test.vpr new file mode 100644 index 000000000..04990f0c2 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test.vpr @@ -0,0 +1,12 @@ +field next: Ref + +/* predicate list(x: Ref) { + x != null ==> acc(x.next, 1/2) && acc(list(x.next), 1/2) +} */ + +method foo(x: Ref) + requires acc(x.next, 1/6) + requires acc(x.next, 1/6) +{ + assert acc(x.next, 1/2) +} diff --git a/src/test/resources/fractionalAbduction/test1.vpr b/src/test/resources/fractionalAbduction/test1.vpr new file mode 100644 index 000000000..c9c2c2c77 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test1.vpr @@ -0,0 +1,13 @@ +field next: Ref + +predicate list(x: Ref) { + x != null ==> acc(x.next, 1/2) && acc(list(x.next), 1/2) +} + +method foo(x: Ref) + requires acc(x.next, 1/2) //wilcard) + //requires acc(list(x.next), 1/4) +{ + // fold acc(list(x), 1/2) + assert acc(list(x), 1/2) +} diff --git a/src/test/resources/fractionalAbduction/test10.vpr b/src/test/resources/fractionalAbduction/test10.vpr new file mode 100644 index 000000000..bca67025b --- /dev/null +++ b/src/test/resources/fractionalAbduction/test10.vpr @@ -0,0 +1,25 @@ +import "doublelinkedlist.vpr" + +method main() { + var x: Ref := new(*) + var y: Ref := new(*) + var z: Ref := new(*) + + var list: Ref := new(*) + + x.prev := null + x.next := y + + y.prev := x + y.next := z + + z.prev := y + z.next := null + + fold nodes(z) + fold nodes(y) + fold nodes(x) + + list.head := x + fold dlist(list) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test11.vpr b/src/test/resources/fractionalAbduction/test11.vpr new file mode 100644 index 000000000..43af1fc31 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test11.vpr @@ -0,0 +1,12 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +method foo(x: Ref) + requires acc(x.f, wildcard) +{ + // fold acc(pred(x), 1/2) + assert acc(pred(x), 1/2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test12.vpr b/src/test/resources/fractionalAbduction/test12.vpr new file mode 100644 index 000000000..b171b7e3c --- /dev/null +++ b/src/test/resources/fractionalAbduction/test12.vpr @@ -0,0 +1,13 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + + +method foo(x: Ref, p: Perm) + // requires p == 1/2 +{ + fold acc(pred(x), p) + assert acc(pred(x), 1/2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test13.vpr b/src/test/resources/fractionalAbduction/test13.vpr new file mode 100644 index 000000000..ad90eea9c --- /dev/null +++ b/src/test/resources/fractionalAbduction/test13.vpr @@ -0,0 +1,13 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f, 1/2) +} + + +method foo(x: Ref) + requires acc(x.f, 1/4) +{ + fold acc(pred(x), 1/2) + assert acc(pred(x), 1/2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test14.vpr b/src/test/resources/fractionalAbduction/test14.vpr new file mode 100644 index 000000000..a2d013bf9 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test14.vpr @@ -0,0 +1,12 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +method foo(x: Ref, p: Perm) + requires acc(pred(x), 1/2) + requires 0/1 < p && p < 1/1 +{ + assert acc(pred(x), p) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test15.vpr b/src/test/resources/fractionalAbduction/test15.vpr new file mode 100644 index 000000000..38b65d6aa --- /dev/null +++ b/src/test/resources/fractionalAbduction/test15.vpr @@ -0,0 +1,15 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +method foo(x: Ref, p: Perm, q: Perm) + requires 0/1 < q && q < 1/1 + requires acc(x.f, 1/2) + // requires 0/1 < p && p < 1/1 + // requires acc(x.f, p) +{ + fold acc(pred(x), 1/2) + assert acc(pred(x), p) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test16.vpr b/src/test/resources/fractionalAbduction/test16.vpr new file mode 100644 index 000000000..890208d71 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test16.vpr @@ -0,0 +1,15 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +method foo(x: Ref) + requires acc(pred(x), wildcard) + ensures acc(pred(x), wildcard) + ensures acc(x.f, wildcard) +{ + unfold acc(pred(x), wildcard) + var y : Ref := x.f + fold acc(pred(x), wildcard) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test19.vpr b/src/test/resources/fractionalAbduction/test19.vpr new file mode 100644 index 000000000..d863ad352 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test19.vpr @@ -0,0 +1,25 @@ +field f: Ref + +predicate pred(x: Ref) { + (x != null) ==> acc(x.f, 1/4) +} + +predicate predpred(x: Ref) { + (x != null) ==> acc(x.f, 1/4) +} + +method bar(x: Ref) + requires x != null + requires acc(pred(x), write) + requires acc(predpred(x), write) + // ensures acc(pred(x), 2/1) +{ + // if (!(x == null)) { + // unfold acc(predpred(x), write) + // unfold acc(pred(x), write) + // } + assert acc(x.f, 1 / 2) + // if (!(x == null)) { + // fold acc(pred(x), 1 / 2 / (1 / 4)) + // } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test2.vpr b/src/test/resources/fractionalAbduction/test2.vpr new file mode 100644 index 000000000..6f1cebf43 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test2.vpr @@ -0,0 +1,19 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +// If we were to fold 1/2 instead of 1/3, +// we would nto have to perform the unfold and second fold +method foo(x: Ref) + // requires acc(x.f, 1/3) + // requires x.f == null +{ + // fold acc(pred(x), 1/3) + assert acc(pred(x), 1/3) + // unfold acc(pred(x), 1/3) + assert x.f == null + // fold acc(pred(x), 1/3) + assert acc(pred(x), 1/3) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test20.vpr b/src/test/resources/fractionalAbduction/test20.vpr new file mode 100644 index 000000000..68ccbc2ba --- /dev/null +++ b/src/test/resources/fractionalAbduction/test20.vpr @@ -0,0 +1,12 @@ +field f: Ref +field g: Ref + +predicate pred(x: Ref) { + acc(x.f) && acc(x.g) +} + +method foo(x: Ref) + requires acc(x.f, 1/2) +{ + assert pred(x) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test21.vpr b/src/test/resources/fractionalAbduction/test21.vpr new file mode 100644 index 000000000..7d8188a19 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test21.vpr @@ -0,0 +1,11 @@ +field f: Ref + +method bar(x: Ref) + // requires acc(x.f, 1/4) +{ + if (x.f == null) { + assert acc(x.f, 2/4) + } else { + assert acc(x.f, 1/4) + } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test22.vpr b/src/test/resources/fractionalAbduction/test22.vpr new file mode 100644 index 000000000..914d5e330 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test22.vpr @@ -0,0 +1,20 @@ +field f: Ref + +method foo(x: Ref) + requires acc(x.f, 1/2) + +method foo2(x: Ref) + requires acc(x.f, 3/4) + +method bar(x: Ref) +{ + assert acc(x.f, 1/2) + assert acc(x.f, 3/4) +} + +method bar2(x: Ref) +{ + foo(x) + foo2(x) +} + diff --git a/src/test/resources/fractionalAbduction/test23.vpr b/src/test/resources/fractionalAbduction/test23.vpr new file mode 100644 index 000000000..18a6531f4 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test23.vpr @@ -0,0 +1,15 @@ +field f: Int +field g: Ref + +method foo(x: Ref) +{ + if (x.f > 2) { + assert acc(x.g, 1/4) + } elseif (x.f < -2) { + assert acc(x.g, 1/4) + } + if (x.f > 0) { + assert acc(x.g, 1/4) + } +} + diff --git a/src/test/resources/fractionalAbduction/test24.vpr b/src/test/resources/fractionalAbduction/test24.vpr new file mode 100644 index 000000000..90b12f93b --- /dev/null +++ b/src/test/resources/fractionalAbduction/test24.vpr @@ -0,0 +1,11 @@ +field f: Int +field g: Ref + +method foo(x: Ref) +{ + if (x.f > 2) { + assert acc(x.g, 1/4) + } + // assert acc(x.f, 2/4) +} + diff --git a/src/test/resources/fractionalAbduction/test25.vpr b/src/test/resources/fractionalAbduction/test25.vpr new file mode 100644 index 000000000..afc1dd5ff --- /dev/null +++ b/src/test/resources/fractionalAbduction/test25.vpr @@ -0,0 +1,14 @@ +field f: Int +field g: Ref + +method foo(x: Ref) +{ + if (x.f > 2) { + assert acc(x.g, 1/4) + if (x.f > 5) { + assert acc(x.g, 2/4) + } + } + // assert acc(x.f, 2/4) +} + diff --git a/src/test/resources/fractionalAbduction/test26.vpr b/src/test/resources/fractionalAbduction/test26.vpr new file mode 100644 index 000000000..3ca1adb19 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test26.vpr @@ -0,0 +1,32 @@ +field f: Ref + +predicate pred(x: Ref) { + x != null ==> acc(x.f) +} + +method foo(x: Ref) returns (y: Ref) +{ + if (x.f == null) { + y := null + } else { + y := x + } +} + + +/* method foo(x: Ref) returns (y: Ref) + requires acc(x.f, write) + ensures !(x == null) && !(x.f == null) ==> acc(pred(y), write) + ensures !(x == y) && x.f == y ==> acc(pred(x), write) +{ + if (x.f == null) { + y := null + } else { + y := x} + if (!(x == y) && y == y) { + fold acc(pred(x), write) + } + if (!(x == null)) { + fold acc(pred(y), write) + } +} */ \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test27.vpr b/src/test/resources/fractionalAbduction/test27.vpr new file mode 100644 index 000000000..4b74d260e --- /dev/null +++ b/src/test/resources/fractionalAbduction/test27.vpr @@ -0,0 +1,14 @@ +field f: Int +field g: Bool +field b: Bool + +method test1(x: Ref, bo: Bool) + //requires b ? acc(x.f) : acc(x.g) + //ensures b ? acc(x.f) && x.f == 0 : acc(x.g) && x.g +{ + if (bo) { + x.f := 0 + } else { + x.g := true + } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test28.vpr b/src/test/resources/fractionalAbduction/test28.vpr new file mode 100644 index 000000000..23b3bf2bf --- /dev/null +++ b/src/test/resources/fractionalAbduction/test28.vpr @@ -0,0 +1,11 @@ +field f: Int +predicate pred(x: Ref) { acc(x.f) } +predicate pred2(x: Ref) { acc(pred(x), 1/2) && acc(x.f, 1/2) } + +method failure (x: Ref) + requires acc(x.f, 1/2) +{ + // Folding pred2 (x) might fail . + // There might be insufficient permission to access pred (x) + assert acc(pred2(x), 1/2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test29.vpr b/src/test/resources/fractionalAbduction/test29.vpr new file mode 100644 index 000000000..d5e073158 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test29.vpr @@ -0,0 +1,16 @@ +field f: Int +field v: Int +field g: Ref + +method foo(x: Ref) +{ + if (x.f > 2) { + if (x.v > 3) { + assert acc(x.g, 1/4) + if (x.f > 5) { + assert acc(x.g, 2/4) + } + } + } + // assert acc(x.f, 2/4) +} diff --git a/src/test/resources/fractionalAbduction/test2_5.vpr b/src/test/resources/fractionalAbduction/test2_5.vpr new file mode 100644 index 000000000..daf8f1bd3 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test2_5.vpr @@ -0,0 +1,16 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +method foo(x: Ref) + requires x.f == null +{ + // fold acc(pred(x), 1/3) + assert acc(pred(x), 1/3) + // unfold acc(pred(x), 1/3) + assert x.f == null + // fold acc(pred(x), 1/3) + assert acc(pred(x), 1/3) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test3.vpr b/src/test/resources/fractionalAbduction/test3.vpr new file mode 100644 index 000000000..2554ce8ac --- /dev/null +++ b/src/test/resources/fractionalAbduction/test3.vpr @@ -0,0 +1,20 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +// Here, ideally, we only infer 2/3 +// Furthermore, if possible, we could +// directly fold 2/3 at the beginning +method foo(x: Ref) + //requires acc(pred(x), 1/2) + //requires acc(pred(x), 1/6) +{ + // fold acc(pred(x), 1/2) + assert acc(pred(x), 1/2) + // unfold acc(pred(x), 1/2) + // fold acc(pred(x), 2/3) + assert acc(pred(x), 2/3) + assert acc(pred(x), 1/2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test30.vpr b/src/test/resources/fractionalAbduction/test30.vpr new file mode 100644 index 000000000..84e7724fc --- /dev/null +++ b/src/test/resources/fractionalAbduction/test30.vpr @@ -0,0 +1,12 @@ +field next: Ref + +predicate list(x: Ref) { + x != null ==> (acc(x.next) && list(x.next)) +} + +method foo(x: Ref) + requires acc(x.next) + requires x.next == null +{ + assert list(x) +} diff --git a/src/test/resources/fractionalAbduction/test31.vpr b/src/test/resources/fractionalAbduction/test31.vpr new file mode 100644 index 000000000..d4971eb47 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test31.vpr @@ -0,0 +1,15 @@ +field next: Ref +field data: Int + +predicate list(x: Ref) { + x != null ==> (acc(x.next) && acc(x.data) && list(x.next)) +} +method assign(x: Ref, elem: Ref) +{ + var curr: Ref := x + while (curr != null) { + var old_curr: Ref := curr + curr := curr.next + } + curr.next := elem +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test32.vpr b/src/test/resources/fractionalAbduction/test32.vpr new file mode 100644 index 000000000..43472b423 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test32.vpr @@ -0,0 +1,8 @@ +field f: Ref +field v: Int + +method foo(x: Ref) { + if (x.f != null) { + assert acc(x.f, 1/2) + } +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test4.vpr b/src/test/resources/fractionalAbduction/test4.vpr new file mode 100644 index 000000000..ad1b22fcc --- /dev/null +++ b/src/test/resources/fractionalAbduction/test4.vpr @@ -0,0 +1,21 @@ +field f: Ref + +predicate pred(x: Ref) { + acc(x.f) +} + +// The unfold is not really neecessary here, maybe we can +// do a second pass to remove unnecessary statements? +// Or keep iterating until we reach a fixed point? +method foo(x: Ref) + requires acc(x.f, 1/4) + // requires acc(x.f, 1/4) + // requires acc(x.f, 1/4) +{ + // fold acc(pred(x), 1/4) + assert acc(pred(x), 1/4) + // unfold acc(pred(x), 1/4) + assert acc(x.f, 1/4) + assert acc(x.f, 1/2) + +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test5.vpr b/src/test/resources/fractionalAbduction/test5.vpr new file mode 100644 index 000000000..93f901856 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test5.vpr @@ -0,0 +1,18 @@ +field f1: Ref +field f2: Ref + +predicate pred1(x: Ref) { + acc(x.f1) +} + +predicate pred2(x: Ref) { + acc(x.f2) +} + +method foo(x: Ref) + requires acc(x.f1, 1 / 2) +{ + assert acc(pred1(x), 1 / 4) + assert acc(pred2(x), 1 / 4) + assert acc(x.f2, 1 / 2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test6.vpr b/src/test/resources/fractionalAbduction/test6.vpr new file mode 100644 index 000000000..1bd7ed76f --- /dev/null +++ b/src/test/resources/fractionalAbduction/test6.vpr @@ -0,0 +1,26 @@ +field next: Ref + +predicate list(x: Ref) { + x != null ==> acc(x.next) && acc(list(x.next)) +} + +method iter_read(x: Ref) + requires acc(list(x), 1/2) + ensures acc(list(x), 1/2) +{ + var curr: Ref := x + package acc(list(curr), 1/2) --* acc(list(x), 1/2) + while(curr != null) + invariant acc(list(curr), 1/2) + invariant acc(list(curr), 1/2) --* acc(list(x), 1/2) + { + var curr0: Ref := curr + unfold acc(list(curr), 1/2) + curr := curr.next + package acc(list(curr), 1/2) --* acc(list(x), 1/2) { + fold acc(list(curr0), 1/2) + apply acc(list(curr0), 1/2) --* acc(list(x), 1/2) + } + } + apply acc(list(curr), 1/2) --* acc(list(x), 1/2) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test7.vpr b/src/test/resources/fractionalAbduction/test7.vpr new file mode 100644 index 000000000..cebd72f11 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test7.vpr @@ -0,0 +1,9 @@ +field f: Ref + +method example(x: Ref) + requires acc(x.f) +{ + package acc(x.f, 1/2) --* acc(x.f) + // apply acc(x.f, 1/2) --* acc(x.f) + assert acc(x.f) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test8.vpr b/src/test/resources/fractionalAbduction/test8.vpr new file mode 100644 index 000000000..2b4b5ed20 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test8.vpr @@ -0,0 +1,9 @@ +field f: Ref + +method example(x: Ref) + requires acc(x.f, 3/4) + requires acc(x.f, 1/4) --* acc(x.f, 1/2) +{ + apply acc(x.f, 1/4) --* acc(x.f, 1/2) + assert acc(x.f) +} \ No newline at end of file diff --git a/src/test/resources/fractionalAbduction/test9.vpr b/src/test/resources/fractionalAbduction/test9.vpr new file mode 100644 index 000000000..143c96034 --- /dev/null +++ b/src/test/resources/fractionalAbduction/test9.vpr @@ -0,0 +1,17 @@ +field f: Ref + +method example(x: Ref) + requires acc(x.f, 1/4) +{ + package acc(x.f, 1/2) --* acc(x.f, 1/4) + //apply acc(x.f, 1/2) --* acc(x.f, 1/4) + //assert acc(x.f, 1/2) --* acc(x.f, 1/4) +} + + +method foo(x: Ref, y: Ref) +requires acc(y.f) +//requires acc(x.f) +{ + package acc(x.f) --* acc(y.f) +} \ No newline at end of file