From 97353cd13101645b8cf0d6fb67317bafd14e697d Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Wed, 15 Jan 2025 23:31:29 +0100 Subject: [PATCH] You know like major changes to how the whole thing works I guess --- src/main/scala/biabduction/Abduction.scala | 149 ++++++----- src/main/scala/biabduction/Abstraction.scala | 2 +- src/main/scala/biabduction/BiAbduction.scala | 245 ++++++++++++------ src/main/scala/biabduction/Invariant.scala | 63 ++--- .../scala/biabduction/VarTransformer.scala | 22 +- src/main/scala/rules/Executor.scala | 54 ++-- .../scala/supporters/MethodSupporter.scala | 1 - .../checksum1.vpr} | 5 +- .../checksum2.vpr} | 9 +- .../dafny/{ => checksum}/exercises-16.0.vpr | 13 +- .../dafny/{ => coffee}/examples-16.2.vpr | 0 .../dafny/{ => coffee}/exercises-16.2.vpr | 16 +- .../biabduction/dafny/exercises-16.3.vpr | 16 -- .../dafny/{ => tokenizer}/exercises-16.1.vpr | 5 - .../tokenizer1.vpr} | 5 +- .../tokenizer2.vpr} | 54 ++-- .../biabduction/grasshopper/sl/sl_concat.vpr | 12 +- .../biabduction/grasshopper/sl/sl_dispose.vpr | 8 +- .../grasshopper/sl/sl_double_all.vpr | 30 +-- .../biabduction/grasshopper/sl/sl_filter.vpr | 37 +-- .../biabduction/grasshopper/sl/sl_insert.vpr | 35 +-- .../grasshopper/sl/sl_pairwise_sum.vpr | 49 ++-- .../biabduction/grasshopper/sl/sl_reverse.vpr | 1 - .../biabduction/mytests/nlist/chain.vpr | 10 + .../vipertests/basic/disjunction_fast_20.vpr | 200 +++++++------- .../vipertests/basic/disjunction_slow_20.vpr | 192 +++++++------- .../biabduction/vipertests/basic/funcpred.vpr | 8 +- .../vipertests/functions/linkedlists.vpr | 30 +-- .../functions/recursive_unrolling.vpr | 35 ++- 29 files changed, 676 insertions(+), 630 deletions(-) rename src/test/resources/biabduction/dafny/{examples-16.0.0.vpr => checksum/checksum1.vpr} (63%) rename src/test/resources/biabduction/dafny/{examples-16.0.1.vpr => checksum/checksum2.vpr} (52%) rename src/test/resources/biabduction/dafny/{ => checksum}/exercises-16.0.vpr (86%) rename src/test/resources/biabduction/dafny/{ => coffee}/examples-16.2.vpr (100%) rename src/test/resources/biabduction/dafny/{ => coffee}/exercises-16.2.vpr (55%) delete mode 100644 src/test/resources/biabduction/dafny/exercises-16.3.vpr rename src/test/resources/biabduction/dafny/{ => tokenizer}/exercises-16.1.vpr (99%) rename src/test/resources/biabduction/dafny/{examples-16.1.0.vpr => tokenizer/tokenizer1.vpr} (79%) rename src/test/resources/biabduction/dafny/{examples-16.1.1.vpr => tokenizer/tokenizer2.vpr} (64%) create mode 100644 src/test/resources/biabduction/mytests/nlist/chain.vpr diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index aa8aae50c..77467728b 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -8,7 +8,7 @@ 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, sorts} +import viper.silicon.state.terms.{SortWrapper, Term} import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast @@ -64,7 +64,6 @@ trait AbductionRule extends BiAbductionRule[AbductionQuestion] { } protected def checkChunk(loc: LocationAccess, s: State, v: Verifier, lostAccesses: Map[Exp, Term])(Q: Option[BasicChunk] => VerificationResult): VerificationResult = { - // TODO Currently we assume only one arg, which may be wrong for arbitrary predicates val arg = loc match { case FieldAccess(rcv, _) => rcv case PredicateAccess(args, _) => args.head @@ -100,8 +99,8 @@ object AbductionRemove extends AbductionRule { case Some(g@AccessPredicate(loc: LocationAccess, _)) => val g1 = q.goal.filterNot(g == _) checkChunk(loc, q.s, q.v, q.lostAccesses) { - case Some(c) => - consumeChunks(Seq(c), q.copy(goal = g1))(q2 => Q(Some(q2))) + case Some(_) => Q(Some(q.copy(goal = g1))) + //consumeChunks(Seq(c), q.copy(goal = g1))(q2 => Q(Some(q2))) case None => apply(q.copy(goal = g1)) { case Some(q2) => Q(Some(q2.copy(goal = g +: q2.goal))) case None => Q(None) @@ -112,19 +111,19 @@ object AbductionRemove extends AbductionRule { /** * This will crash if the chunks do not exist. This is by design. Only call this if you are sure that the chunks exist. - */ - private def consumeChunks(chunks: Seq[BasicChunk], q: AbductionQuestion)(Q: AbductionQuestion => VerificationResult): VerificationResult = { - chunks match { - case Seq() => Q(q) - case c +: cs => - val c1 = findChunk[BasicChunk](q.s.h.values, c.id, c.args, q.v).get - val resource: Resource = c.resourceID match { - case PredicateID => q.s.program.predicates.head - case FieldID => q.s.program.fields.head - } - chunkSupporter.consume(q.s, q.s.h, resource, c1.args, None, c1.perm, None, ve, q.v, "")((s1, _, _, v1) => consumeChunks(cs, q.copy(s = s1, v = v1))(Q)) - } - } + * + * private def consumeChunks(chunks: Seq[BasicChunk], q: AbductionQuestion)(Q: AbductionQuestion => VerificationResult): VerificationResult = { + * chunks match { + * case Seq() => Q(q) + * case c +: cs => + * val c1 = findChunk[BasicChunk](q.s.h.values, c.id, c.args, q.v).get + * val resource: Resource = c.resourceID match { + * case PredicateID => q.s.program.predicates.head + * case FieldID => q.s.program.fields.head + * } + * chunkSupporter.consume(q.s, q.s.h, resource, c1.args, None, c1.perm, None, ve, q.v, "")((s1, _, _, v1) => consumeChunks(cs, q.copy(s = s1, v = v1))(Q)) + * } + * } */ } @@ -161,10 +160,10 @@ object AbductionFoldBase extends AbductionRule { 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) => - consumer.consume(s3, a, pve, v3) { (s4, _, v4) => - val fold = Fold(a)() - Q(Some(q.copy(goal = g1, foundStmts = q.foundStmts :+ fold, s = s4, v = v4))) - } + //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))) + //} } } } else { @@ -214,35 +213,43 @@ object AbductionFold extends AbductionRule { // 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 wildcards = q.s.constrainableARPs -- q.s.constrainableARPs - - val fargs = pred.formalArgs.map(_.localVar) - val eArgs = a.loc.args - val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map) - val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals) - val pveTransformed = pve.withReasonNodeTransformed(reasonTransformer) - - val tryFold = predicateSupporter.fold(q.s, pred, chunk.args.toList, None, terms.FullPerm, None, wildcards, pveTransformed, q.v) { - (s1, v1) => - consumer.consume(s1, a, pve, v1) { (s2, _, v2) => - Success(Some(AbductionSuccess(s2, v2, v2.decider.pcs.duplicate(), Seq(), Seq(Fold(a)())))) - } + //val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs + + //val fargs = pred.formalArgs.map(_.localVar) + //val eArgs = a.loc.args + //val formalsToActuals: Map[ast.LocalVar, ast.Exp] = fargs.zip(eArgs).to(Map) + //val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals) + //val pveTransformed = pve.withReasonNodeTransformed(reasonTransformer) + + val fold = Fold(a)() + executor.exec(q.s, fold, q.v, doAbduction = true, q.trigger) { (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)) } - tryFold match { - case nf: NonFatalResult => - // TODO nklose make sure the pcs are correct here - abductionUtils.getAbductionSuccesses(nf) match { - case Seq(suc) => - val fold = Fold(a)() - val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, sorts.Ref)) - val q2 = q.copy(s = suc.s, v = suc.v, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1) - Q(Some(q2)) - } - case f: Failure => - BiAbductionSolver.solveAbduction(q.s, q.v, f, q.trigger){(s3, res, v3) => - apply(q.copy(s = s3, v = v3, foundState = res.state ++ q.foundState, foundStmts = res.stmts ++ q.foundStmts))(Q)} + + /* + val tryFold = predicateSupporter.fold(q.s, pred, chunk.args.toList, None, terms.FullPerm, None, wildcards, pveTransformed, q.v) { + (s1, v1) => + consumer.consume(s1, a, pve, v1) { (s2, _, v2) => + Success(Some(AbductionSuccess(s1, v1, v1.decider.pcs.duplicate(), Seq(), Seq(Fold(a)()), newFieldChunks=Map()))) } - + } + tryFold match { + case nf: NonFatalResult => + // TODO nklose make sure the pcs are correct here + abductionUtils.getAbductionSuccesses(nf) match { + case Seq(suc) => + val fold = Fold(a)() + val lost = q.lostAccesses + (field -> SortWrapper(chunk.snap, chunk.snap.sort)) + val q2 = q.copy(s = suc.s, v = suc.v, foundStmts = q.foundStmts :+ fold, lostAccesses = lost, goal = g1) + Q(Some(q2)) + } + case f: Failure => + BiAbductionSolver.solveAbduction(q.s, q.v, f, q.trigger){(s3, res, v3) => + apply(q.copy(s = s3, v = v3, foundState = res.state ++ q.foundState, foundStmts = res.stmts ++ q.foundStmts))(Q)} + }*/ + case None => { // If we do not find a chunk, we recurse to try the others by calling this apply(q.copy(goal = g1)) { @@ -336,7 +343,7 @@ object AbductionApply extends AbductionRule { // We drop the first element, because it is the true lit of the lhs val subexps = goalWand.subexpressionsToEvaluate(q.s.program).tail // 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 applieed + // chunk is our goal, so the rule can be applied evals(q.s, subexps, _ => pve, q.v)((s1, args, _, v1) => { val matchingWand = s1.h.values.collect { case m: MagicWandChunk if m.id.ghostFreeWand.structure(s1.program).right == goalStructure.right && m.args.takeRight(args.length) == args => @@ -356,10 +363,26 @@ object AbductionApply extends AbductionRule { }.collectFirst { case c if c.isDefined => c.get } matchingWand match { case Some(wand) => - val g1 = q.goal.filterNot(_ == wand.right) :+ wand.left - consumer.consume(s1, wand, pve, v1)((s2, _, v2) => { - Q(Some(q.copy(s = s2, v = v2, goal = g1, foundStmts = q.foundStmts :+ Apply(wand)()))) - }) + val q1 = q.copy(goal = Seq(wand.left)) + 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 = q.foundStmts ++ lhsRes.foundStmts :+ Apply(wand)() + val state = q.foundState ++ lhsRes.foundState + val lost = q.lostAccesses ++ lhsRes.lostAccesses + Q(Some(AbductionQuestion(s2, v2, g1, lost, state, stmts, q.trigger))) + /*val g1 = q.goal.filterNot(_ == wand.right) :+ wand.left + consumer.consume(s1, wand, pve, v1)((s2, _, v2) => + Q(Some(q.copy(s = s2, v = v2, goal = g1, foundStmts = q.foundStmts :+ Apply(wand)()))) + )*/ + } + } + } + case None => val g1 = q.goal.filterNot(_ == g) apply(q.copy(goal = g1)) { @@ -382,17 +405,19 @@ object AbductionPackage extends AbductionRule { producer.produce(q.s, freshSnap, wand.left, pve, q.v)((s1, v1) => { val packQ = q.copy(s = s1, v = v1, goal = Seq(wand.right)) - AbductionApplier.applyRules(packQ){ packRes => - + AbductionApplier.applyRules(packQ) { packRes => + if (packRes.goal.nonEmpty) { Q(None) } else { - val g1 = q.goal.filterNot(_ == wand) - val stmts = q.foundStmts :+ Package(wand, Seqn(packRes.foundStmts.reverse, Seq())())() - val pres = q.foundState ++ packRes.foundState - Q(Some(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts, foundState = pres))) - }} + val g1 = q.goal.filterNot(_ == wand) + val stmts = q.foundStmts :+ Package(wand, Seqn(packRes.foundStmts.reverse, Seq())())() + val pres = q.foundState ++ packRes.foundState + //val lost = q.lostAccesses ++ packRes.lostAccesses + Q(Some(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts, foundState = pres))) + } + } }) } } @@ -410,7 +435,9 @@ object AbductionMissing extends AbductionRule { Q(None) } else { val g1 = q.goal.filterNot(accs.contains) - Q(Some(q.copy(goal = g1, foundState = q.foundState ++ accs))) + producer.produces(q.s, freshSnap, accs, _ => pve, q.v) { (s1, v1) => + Q(Some(q.copy(s = s1, v = v1, goal = g1, foundState = q.foundState ++ accs))) + } } } } diff --git a/src/main/scala/biabduction/Abstraction.scala b/src/main/scala/biabduction/Abstraction.scala index 1eef2f2c8..d9b7013eb 100644 --- a/src/main/scala/biabduction/Abstraction.scala +++ b/src/main/scala/biabduction/Abstraction.scala @@ -19,7 +19,7 @@ case class AbstractionQuestion(s: State, v: Verifier, fixedChunks: Seq[Chunk]) { // TODO we assume each field only appears in at most one predicate def fields: Map[Field, Predicate] = s.program.predicates.flatMap { pred => pred.body.get.collect { case fa: FieldAccessPredicate => (fa.loc.field, pred) } }.toMap - def varTran: VarTransformer = VarTransformer(s, v, s.g.values, Heap()) + def varTran: VarTransformer = VarTransformer(s, v, s.g.values, s.h) def isTriggerField(bc: BasicChunk): Boolean = { bc.resourceID match { diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index f21644023..71c96abc7 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -2,9 +2,10 @@ package viper.silicon.biabduction import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces._ -import viper.silicon.interfaces.state.{Chunk, NonQuantifiedChunk} +import viper.silicon.interfaces.state.Chunk +import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.rules.consumer.consumes -import viper.silicon.rules.{executionFlowController, executor, producer} +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 @@ -26,20 +27,20 @@ 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] = Seq(), stmts: Seq[Stmt] = Seq(), trigger: Option[Positioned] = None) extends BiAbductionSuccess { +case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, state: Seq[Exp] = Seq(), stmts: Seq[Stmt] = Seq(), newFieldChunks: Map[BasicChunk, LocationAccess], trigger: Option[Positioned] = None) extends BiAbductionSuccess { override def toString: String = { "Abduced pres " + state.length + ", Abduced statements " + stmts.length } - def addToMethod(m: Method, bcsTerms: Seq[Term]): Option[Method] = { + def addToMethod(m: Method, bcsTerms: Seq[Term], newFieldChunks: Map[BasicChunk, LocationAccess]): Option[Method] = { 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) } val prevPcs = v.decider.pcs v.decider.setPcs(pcs) val bcExps = getBcExps(bcsTerms) - val pres = getPreconditions(preVars, preHeap, bcExps) + val pres = getPreconditions(preVars, preHeap, bcExps, newFieldChunks) val finalStmts = getStatements(bcExps) v.decider.setPcs(prevPcs) if (pres.isEmpty || finalStmts.isEmpty) { @@ -49,7 +50,9 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat val body = m.body.get val newBody: Seqn = trigger match { case None => body - case Some(t: Stmt) if t == abductionUtils.dummyEndStmt => Seqn(body.ss ++ finalStmt, body.scopedSeqnDeclarations)(body.pos, body.info, body.errT) + case Some(t: Stmt) if t == abductionUtils.dummyEndStmt => + Seqn(body.ss ++ finalStmt, body.scopedSeqnDeclarations)(body.pos, body.info, body.errT) + case Some(t: Stmt) if abductionUtils.isEndOfLoopStmt(t) => val loop = abductionUtils.getWhile(t.asInstanceOf[Label].invs.head, m) val newLoopBody = loop.body.copy(ss = loop.body.ss ++ finalStmt)(pos = loop.body.pos, info = loop.body.info, errT = loop.body.errT) @@ -80,8 +83,8 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat if (stmts.isEmpty) { Some(Seq()) // TODO nklose we are over approximating here, this is probably wrong in general but good in practise - //} else if (bcExps.contains(None)) { - // None + //} else if (bcExps.contains(None)) { + // None } else { val con = BigAnd(bcExps.collect { case Some(e) => e }) con match { @@ -91,21 +94,20 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat } } - def getPreconditions(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], preHeap: Heap, bcExps: Seq[Option[Exp]]): Option[Seq[Exp]] = { + def getPreconditions(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], preHeap: Heap, bcExps: Seq[Option[Exp]], newFieldChunks: Map[BasicChunk, LocationAccess]): Option[Seq[Exp]] = { if (state.isEmpty) { Some(Seq()) } else { - - // We use the pcs from the abduction point - val varTrans = VarTransformer(s, v, preVars, preHeap) + + val varTrans = VarTransformer(s, v, preVars, preHeap, newFieldChunks) val presTransformed = state.map { pre => varTrans.transformExp(pre) } - val bcPreExps = bcExps.map { - case Some(exp) => varTrans.transformExp(exp) + val bcPreExps = bcExps.collect { + case Some(exp) => varTrans.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)) { @@ -125,13 +127,19 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), loop: While, pcs: PathConditionStack) extends BiAbductionSuccess { override def toString: String = "Successful loop invariant abduction" - def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = { - + def getBcsExps(bcs: Seq[Term]): Seq[Exp] = { val prevPcs = v.decider.pcs v.decider.setPcs(pcs) val bcTran = VarTransformer(s, v, s.g.values, s.h) - val bcExps = bcs.map { t => bcTran.transformTerm(t) } + val bcExps = bcs.map { t => bcTran.transformTerm(t) }.collect { case Some(e) => e } v.decider.setPcs(prevPcs) + bcExps + } + + /* + def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = { + + val bcExps = getBcsExps(bcs) if (bcExps.contains(None)) { None } else { @@ -148,18 +156,18 @@ case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), l } Some(m.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) } - } + }*/ } -case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], stmts: Seq[Stmt], loc: Positioned, pcs: PathConditionStack, varTran: VarTransformer) extends BiAbductionSuccess { +case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], loc: Positioned, pcs: PathConditionStack, varTran: VarTransformer) extends BiAbductionSuccess { override def toString: String = "Successful framing" - def getBcExps(bcsTerms: Seq[Term], targetVars: Map[AbstractLocalVar, (Term, Option[Exp])]): Option[Exp] = { + def getBcExps(bcsTerms: Seq[Term], targetVars: Map[AbstractLocalVar, (Term, Option[Exp])]): Seq[Exp] = { val varTrans = VarTransformer(s, v, targetVars, s.h) val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) } // TODO this is possibly unsound but better in practise - Some(BigAnd(bcExps.collect { case Some(e) => e })) + bcExps.collect { case Some(e) => e } /* if (bcExps.contains(None)) { None @@ -168,35 +176,33 @@ case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], stmts: Seq[Stm }*/ } + /* + def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = { + val prevPcs = v.decider.pcs + v.decider.setPcs(pcs) + val formals = m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar) + val vars = s.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) } + val bcExps = getBcExps(bcs, vars) + v.decider.setPcs(prevPcs) - def addToMethod(m: Method, bcs: Seq[Term]): Option[Method] = { - val prevPcs = v.decider.pcs - v.decider.setPcs(pcs) - val formals = m.formalArgs.map(_.localVar) ++ m.formalReturns.map(_.localVar) - val vars = s.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) } - val bcExpsOpt = getBcExps(bcs, vars) - v.decider.setPcs(prevPcs) - - bcExpsOpt.flatMap { bcExps => - + /* val bcStmts = (bcExps, stmts) match { case (_, Seq()) => Seq() case (_: TrueLit, _) => stmts case _ => Seq(If(bcExps, Seqn(stmts, Seq())(), Seqn(Seq(), Seq())())()) - } + }*/ val bcPost = (bcExps, posts) match { case (_, Seq()) => Seq() - case (_: TrueLit, _) => posts - case _ => Seq(Implies(bcExps, BigAnd(posts))()) + case (Seq(), _) => posts + case _ => Seq(Implies(BigAnd(bcExps), BigAnd(posts))()) } - val body = m.body.get - val newBody = body.copy(ss = body.ss ++ bcStmts)(pos = body.pos, info = body.info, errT = body.errT) - Some(m.copy(posts = m.posts ++ bcPost, body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT)) + //val body = m.body.get + //val newBody = body.copy(ss = body.ss ++ bcStmts)(pos = body.pos, info = body.info, errT = body.errT) + Some(m.copy(posts = m.posts ++ bcPost)(pos = m.pos, info = m.info, errT = m.errT)) - } - } + }*/ } case class BiAbductionFailure(s: State, v: Verifier, pcs: PathConditionStack) extends BiAbductionResult { @@ -292,18 +298,28 @@ object BiAbductionSolver { AbductionApplier.applyRules(q) { q1 => if (q1.goal.isEmpty) { - val abd = AbductionSuccess(q1.s, q1.v, q1.v.decider.pcs.duplicate(), q1.foundState.reverse, q1.foundStmts.reverse, trigger) - producer.produces(s, freshSnap, abd.state, _ => Internal(), v) { - (s2, v2) => - executor.execs(s2, abd.stmts, v2) { - (s3, v3) => - if (v3.decider.checkSmoke()) { - Success(Some(BiAbductionFailure(s, v, initPcs))) - } else { - Q(s3, abd.copy(s = s3, v = v3), v3) - } - } + val newState = q1.foundState.reverse + val newStmts = q1.foundStmts.reverse + //producer.produces(s, freshSnap, newState, _ => Internal(), v) { (s2, v2) => + val newLocs = newState.collect { + case fa: FieldAccessPredicate => fa.loc + case pa: PredicateAccessPredicate => pa.loc + } + abductionUtils.findChunks(newLocs, q1.s, q1.v, Internal()) { newChunks => + //val newMatches = fieldsTerms.zip(newFields).toMap + //executor.execs(s2, newStmts, v2, doAbduction = false) { (s3, v3) => + if (q1.v.decider.checkSmoke()) { + Success(Some(BiAbductionFailure(s, v, initPcs))) + } else { + val newOldHeaps = q1.s.oldHeaps.map { case (label, heap) => (label, heap + Heap(newChunks.keys)) } + val s1 = q1.s.copy(oldHeaps = newOldHeaps) + val fieldChunks = newChunks.collect { case (c, fa: FieldAccess) => (c, fa) } + val abd = AbductionSuccess(s1, q1.v, q1.v.decider.pcs.duplicate(), newState, newStmts, fieldChunks, trigger) + Q(s1, abd, q1.v) + } + //} } + //} } else { f } @@ -333,7 +349,7 @@ object BiAbductionSolver { } { // We consumed all the posts and did not find any new ones. So create a fresh Framing Success with the bcs case Seq() => - Q(FramingSuccess(s1, v1, Seq(), Seq(), loc, v.decider.pcs.duplicate(), tra)) // No new state or needed stmts + Q(FramingSuccess(s1, v1, Seq(), loc, v.decider.pcs.duplicate(), tra)) // No new state or needed stmts // 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) { frame => @@ -347,13 +363,14 @@ object BiAbductionSolver { BiAbductionSolver.solveAbduction(s, v, f, Some(loc))((s3, res, v3) => { solveFraming(s3, v3, pvef, tra, loc, knownPosts) { frame => - val newAbdRes = if (res.state.nonEmpty) { + /*val newAbdRes = if (res.state.nonEmpty) { Success(Some(res.copy(stmts = Seq()))) } else { Success() - } - val newFrame = frame.copy(stmts = frame.stmts ++ res.stmts) - newAbdRes && Q(newFrame) + }*/ + val newAbdRes = Success(Some(res)) + //val newFrame = frame.copy(stmts = frame.stmts ++ res.stmts) + newAbdRes && Q(frame) } } ) @@ -362,7 +379,9 @@ object BiAbductionSolver { def resolveAbductionResults(m: Method, nf: NonFatalResult): Option[Method] = { val abdReses = abductionUtils.getAbductionSuccesses(nf) - val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts, res.state)).flatMap { + val newMatches = abdReses.flatMap(_.newFieldChunks).toMap + val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts, res.state)) + val joinedCases = abdCases.flatMap { case (_, reses) => val unjoined = reses.map(res => (Seq(res), res.pcs.branchConditions.distinct.filter(_ != True))) val joined = abductionUtils.joinBcs(unjoined) @@ -371,13 +390,39 @@ object BiAbductionSolver { reses.head -> pcs } } - abdCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) }) + // 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) => res.addToMethod(m1, joinedCases(res), newMatches) + case _ => mOpt + }} + //joinedCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2, newMatches) }) } def resolveFramingResults(m: Method, nf: NonFatalResult): Option[Method] = { val frames = abductionUtils.getFramingSuccesses(nf) - val frameCases = frames.groupBy(f => (f.posts, f.stmts)).flatMap { + + // 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 vars = frames.head.s.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) } + + + val cases = frames.map(f => (f.posts.diff(everyPosts), f.getBcExps(f.pcs.branchConditions.distinct.filter(_ != True), vars))) + + // We can remove bcs that hold in every branch + val everyTerms = cases.head._2.filter { t => cases.forall(_._2.contains(t)) } + + val res = cases.collect { + 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) @@ -387,16 +432,48 @@ object BiAbductionSolver { } } - // We get a framing result for every branch that reaches the end. So we can remove bcs that hold in every case, as they - // are guaranteed to hold. - val allTerms = frameCases.values - val alwaysTerms = allTerms.head.filter {t => allTerms.forall(_.contains(t))} - frameCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2.diff(alwaysTerms)) }) + */ + } + def resolveLoopInvResults(m: Method, nf: NonFatalResult): Option[Method] = { - val invs = abductionUtils.getInvariantSuccesses(nf) + + val invsSuccs = abductionUtils.getInvariantSuccesses(nf) + + val reses = invsSuccs.groupBy(inv => inv.loop).map { + case (loop, cases) => + + // We get an invariant for each time we reach a loop. So if an invariant holds every time we get there + // we can ignore the bcs + val everyInv = cases.head.invs.filter { i => cases.forall(_.invs.contains(i)) } + val everyBcs = cases.head.pcs.branchConditions.filter { t => cases.forall(_.pcs.branchConditions.contains(t)) } :+ True + + val invsWithBcs = cases.map { inv => + val bcs = inv.getBcsExps(inv.pcs.branchConditions.distinct.filter(!everyBcs.contains(_))) + (inv.invs.diff(everyInv), bcs.diff(everyBcs)) + } + + val res = invsWithBcs.collect { + case (is, bcs) if is.nonEmpty && bcs.nonEmpty => Implies(BigAnd(bcs.diff(everyBcs)), BigAnd(is))() + case (is, _) if is.nonEmpty => BigAnd(is) + } ++ everyInv + + (loop, res) + } + + Some(reses.foldLeft(m) { case (m1, (loop, inv)) => + val body = m1.body.get + val newBody = body.transform { + case l: While if l.cond == loop.cond => + l.copy(invs = l.invs ++ inv)(pos = l.pos, info = l.info, errT = l.errT) + case other => other + } + m1.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT) + }) + + /* val invCases = invs.groupBy(inv => (inv.loop, inv.invs)).flatMap { case (_, invs) => val unjoined = invs.map(inv => (Seq(inv), inv.pcs.branchConditions.distinct.filter(_ != True))) @@ -406,7 +483,7 @@ object BiAbductionSolver { invs.head -> pcs } } - invCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) }) + invCases.foldLeft[Option[Method]](Some(m))((m1, res) => m1.flatMap { mm => res._1.addToMethod(mm, res._2) })*/ } /*/val tra = VarTransformer(s, v, targetVars, s.h) @@ -429,15 +506,7 @@ object BiAbductionSolver { object abductionUtils { def isValidPredicate(pred: Predicate): Boolean = { - pred.formalArgs.size == 1 && (pred.body match { - case None => false - case Some(body) => - !body.topLevelConjuncts.exists { - case _: FieldAccessPredicate => false - case _: Implies => false - case _ => true - } - }) + pred.formalArgs.size == 1 && pred.body.isDefined } def getVars(t: Term, g: Store): Seq[AbstractLocalVar] = { @@ -517,8 +586,34 @@ object abductionUtils { (a.diff(b), b.diff(a)) match { case (Seq(eq: terms.BuiltinEquals), Seq(terms.Not(t))) if eq == t => Some(a.filter(_ != eq)) case (Seq(terms.Not(t)), Seq(eq: terms.BuiltinEquals)) if eq == t => Some(b.filter(_ != eq)) + case (Seq(), _) => Some(a) + case (_, Seq()) => Some(b) case _ => None } } + private def findChunkFromExp(loc: LocationAccess, s: State, v: Verifier, pve: PartialVerificationError)(Q: Option[BasicChunk] => VerificationResult): VerificationResult = { + + val arg = loc match { + case FieldAccess(rcv, _) => rcv + case PredicateAccess(args, _) => args.head + } + evaluator.eval(s, arg, pve, v) { (s2, term, _, v2) => + 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) + } + } + + def findChunks(locs: Seq[LocationAccess], s: State, v: Verifier, pve: PartialVerificationError)(Q: Map[BasicChunk, LocationAccess] => VerificationResult): VerificationResult = { + locs match { + case Seq() => Q(Map()) + case loc +: rest => + findChunkFromExp(loc, s, v, pve) { + case Some(chunk) => findChunks(rest, s, v, pve) { chunks => Q(chunks + (chunk -> loc)) } + } + } + } + } diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index 03ed96e87..f84a04890 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -51,9 +51,10 @@ object LoopInvariantSolver { case abdRes: NonFatalResult => // TODO nklose we do not guarantee length 1 here anymore abductionUtils.getAbductionSuccesses(abdRes) match { - case Seq(AbductionSuccess(s5, v5, _, Seq(), _, _)) => + case Seq(AbductionSuccess(s5, v5, _, Seq(), _, _, _)) => val unfolded = VarTransformer(s5, v5, s5.g.values, s5.h).transformState(s5) Q(unfolded) + case _ => Q(inverted) } /* val unfolds = abd.stmts.collect { case Unfold(pa) => (pa.toString -> pa.loc.predicateBody(s.program, Set()).get) }.toMap @@ -69,31 +70,6 @@ object LoopInvariantSolver { }(Q) } - private def findChunkFromExp(loc: LocationAccess, s: State, v: Verifier)(Q: Option[BasicChunk] => VerificationResult): VerificationResult = { - - // TODO Currently we assume only one arg, which may be wrong for arbitrary predicates - val arg = loc match { - case FieldAccess(rcv, _) => rcv - case PredicateAccess(args, _) => args.head - } - evaluator.eval(s, arg, pve, v) { (s2, term, _, v2) => - 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) - } - } - - protected def findChunks(locs: Seq[LocationAccess], s: State, v: Verifier)(Q: Map[BasicChunk, LocationAccess] => VerificationResult): VerificationResult = { - locs match { - case Seq() => Q(Map()) - case loc +: rest => - findChunkFromExp(loc, s, v) { - case Some(chunk) => findChunks(rest, s, v) { chunks => Q(chunks + (chunk -> loc)) } - } - } - } - // TODO do we need to check well-definedness of the loop condition? def solveLoopInvariants(s: State, v: Verifier, @@ -106,6 +82,7 @@ object LoopInvariantSolver { loopConBcs: Seq[Term] = Seq(), iteration: Int = 1): VerificationResult = { + println("\nIteration: " + iteration) // Produce the already known invariants. They are consumed at the end of the loop body, so we need to do this every iteration produces(s, freshSnap, loopHead.invs, ContractNotWellformed, v) { (sPreInv, vPreInv) => @@ -113,39 +90,39 @@ object LoopInvariantSolver { executionFlowController.locally(sPreInv, vPreInv) { (sFP, vFP) => // TODO nklose follows should be private. We can exec the statement block instead? - executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint) { (_, _) => - //loopCondTerm = Some(v.decider.pcs.branchConditions.diff(oldPcs).head) - Success() - } + executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint) { (_, _) => Success()} } match { // Abduction has failed so we fail case f: Failure => f - case nonf: NonFatalResult => // We assume there is only one loop internal edge val loopConExp = loopEdges.head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition - val abdReses = abductionUtils.getAbductionSuccesses(nonf) + val abdReses = abductionUtils.getAbductionSuccesses(nonf).reverse + // TODO nklose do we want to join branches here like we do for preconditions? + val newMatches = abdReses.flatMap(_.newFieldChunks).toMap val preStateVars = sPreInv.g.values.filter { case (v, _) => origVars.contains(v) } - val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preStateVars, sPreInv.h, Seq()).get } + val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preStateVars, sPreInv.h, Seq(), newMatches).get } // We still need to remove the current loop condition val newState = newStateOpt.map(_.transform { case im: Implies if im.left == loopConExp => im.right }) + println("New state:\n " + newState.mkString("\n ")) + // Do the second pass so that we can compare the state at the end of the loop with the state at the beginning // Get the state at the beginning of the loop with the abduced things added producer.produces(sPreInv, freshSnap, newState, pveLam, vPreInv) { (sPreAbd0, vPreAbd0) => evaluator.eval(sPreAbd0, loopConExp, pve, vPreAbd0) { (sPreAbd, loopCondTerm, _, vPreAbd) => - findChunks(newState.collect { + abductionUtils.findChunks(newState.collect { case loc: FieldAccessPredicate => loc.loc case loc: PredicateAccessPredicate => loc.loc - }, sPreAbd, vPreAbd) { chunks => + }, sPreAbd, vPreAbd, pve) { chunks => val allChunks = chunks.keys @@ -156,8 +133,8 @@ object LoopInvariantSolver { val preTran = VarTransformer(newPreState, newPreV, preStateVars, newPreState.h) val newPreAbstraction = newPreAbstraction0.map(e => preTran.transformExp(e, strict = false).get) + println("New pre abstraction:\n " + newPreAbstraction.mkString("\n ")) - executor.follows(sPreAbd, loopEdges, pveLam, vPreAbd, joinPoint)((sPost, vPost) => { BiAbductionSolver.solveAbstraction(sPost, vPost) { (sPostAbs, postAbstraction0, vPostAbs) => @@ -166,20 +143,14 @@ object LoopInvariantSolver { val postTran = VarTransformer(sPostAbs, vPostAbs, postStateVars, sPostAbs.h) val postAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get) - println("\nIteration: " + iteration) - println("New state:\n " + newState.mkString("\n ")) - println("New pre abstraction:\n " + newPreAbstraction.mkString("\n ")) println("New post abstraction:\n " + postAbstraction.mkString("\n ")) // If the pushed forward abstraction is the same as the previous one, we are done - if (newPreAbstraction == q.preAbstraction && postAbstraction == q.postAbstraction) { + if (newPreAbstraction.toSet == q.preAbstraction.toSet && postAbstraction.toSet == q.postAbstraction.toSet) { getPreInvariant(newPreAbstraction, postAbstraction, loopConExp, sPostAbs, vPostAbs) { preInv => - preInv ++ postAbstraction match { - case Seq() => Success() - case res => - val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method]) - Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = res, loop, vPostAbs.decider.pcs.duplicate()))) - } + + val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method]) + Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = preInv ++ postAbstraction, loop, vPostAbs.decider.pcs.duplicate()))) } } else { val newLoopCons = loopConBcs :+ loopCondTerm diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index 14ad5fd78..47faf70d5 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -11,13 +11,15 @@ import viper.silver.ast._ import scala.annotation.tailrec -case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap) { +case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap, newFieldChunks: Map[BasicChunk, LocationAccess] = Map()) { //val pve: PartialVerificationError = Internal() // Ask the decider whether any of the terms are equal to a target. val matches: Map[Term, Exp] = resolveMatches() + val newChunkBySnap = newFieldChunks.map { case (c, fa: FieldAccess) => c.snap -> (c, fa) } + private def resolveMatches(): Map[Term, Exp] = { val allTerms: Seq[Term] = (s.g.values.values.map { case (t1, _) => t1 } @@ -69,6 +71,10 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa case _ => None } case terms.True => Some(TrueLit()()) + case t if newChunkBySnap.contains(t) => + val c = newChunkBySnap(t) + val rcv = transformTerm(c._1.args.head) + Some(FieldAccess(rcv.get, c._2.field)()) case _ => None } } @@ -126,16 +132,17 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa } } - // This is kinda tricky if the expression contains field accesses. - // We do not get the guarantee that the chunks exist in the current state, so we can not evaluate them - // directly def transformExp(e: Exp, strict: Boolean = true): Option[Exp] = { try { val res = e.transform { case FieldAccessPredicate(fa, perm) => + // We do not want to transform the entire field access, this would resolve the snap! val newRcv = transformExp(fa.rcv).get FieldAccessPredicate(FieldAccess(newRcv, fa.field)(), perm)() case fa@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) => @@ -143,8 +150,7 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa existingChunkTerm match { case Some(nfa: FieldAccess) => nfa - // Due to heap representation this can sometimes happen - case Some(NullLit()) | Some(LocalVar(_, _)) => + case Some(NullLit()) | Some(LocalVar(_, _)) | None => val rvcExp = transformExp(target) FieldAccess(rvcExp.get, field)() @@ -152,9 +158,7 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa // 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 - case None => - val rvcExp = transformExp(target) - FieldAccess(rvcExp.get, field)() + } // Else we want to recurse and try to match the target case None => diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index d0a6f9c28..95d6340e1 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -38,11 +38,11 @@ trait ExecutionRules extends SymbolicExecutionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult - def exec(s: State, stmt: ast.Stmt, v: Verifier) + def exec(s: State, stmt: ast.Stmt, v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) (Q: (State, Verifier) => VerificationResult) : VerificationResult - def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier) + def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) (Q: (State, Verifier) => VerificationResult) : VerificationResult } @@ -223,7 +223,7 @@ object executor extends ExecutionRules { block match { case cfg.StatementBlock(stmt) => - execs(s, stmt, v)((s1, v1) => + execs(s, stmt, v, doAbduction = true)((s1, v1) => follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint)(Q)) case _: cfg.PreconditionBlock[ast.Stmt, ast.Exp] @@ -267,13 +267,18 @@ object executor extends ExecutionRules { val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => { val xNew = v.decider.fresh(x) - map.updated(x, xNew)})) + map.updated(x, xNew) + })) val sBody = s.copy(g = gBody, h = Heap()) - val invReses = executionFlowController.locally(s, v) ((sAbd, vAbd) => - LoopInvariantSolver.solveLoopInvariants(sAbd, vAbd, sAbd.g.values.keys.toSeq, block, otherEdges, joinPoint, vAbd.decider.pcs.branchConditions) - ) - + val invReses = executionFlowController.locally(s, v)((sInv, vInv) => + // We have to consume the existing invariants once, because we produce it at the start of each iteration + // We do this as an assert so that abduction guarantees it to exist + executor.exec(sInv, ast.Exhale(BigAnd(existingInvs))(), vInv, doAbduction = true) { (sInv1, vInv1) => + LoopInvariantSolver.solveLoopInvariants(sInv1, vInv1, sInv1.g.values.keys.toSeq, block, otherEdges, joinPoint, vInv1.decider.pcs.branchConditions) + } + ) + invReses match { case f: Failure => f @@ -282,12 +287,12 @@ object executor extends ExecutionRules { val (foundInvs, invSuc) = abductionUtils.getInvariantSuccesses(nfr) match { case Seq(invSuc) => (invSuc.invs.distinct, Success(Some(LoopInvariantSuccess(s, v, invSuc.invs.distinct, invSuc.loop, v.decider.pcs.duplicate())))) - case Seq() => (Seq(), Success()) } - val invs = existingInvs ++ foundInvs + val invs = foundInvs ++ existingInvs type PhaseData = (State, RecordedPathConditions, Set[FunctionDecl]) var phase1data: Vector[PhaseData] = Vector.empty + val wfi = executionFlowController.locally(sBody, v)((s0, v0) => { v0.decider.prover.comment("Loop head block: Check well-definedness of invariant") val mark = v0.decider.setPathConditionMark() @@ -314,7 +319,7 @@ object executor extends ExecutionRules { if (v2.decider.checkSmoke()) Success() else { - execs(s3, stmts, v2)((s4, v3) => { + execs(s3, stmts, v2, doAbduction=true)((s4, v3) => { v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions") val wde = edgeConditions.foldLeft(Success(): VerificationResult) { case (result, _) if !result.continueVerification => result @@ -335,8 +340,7 @@ object executor extends ExecutionRules { ) }) // Continue after the loop (with the new invariants) - val atl = - follows(s4, outEdges, WhileFailed, v3, joinPoint)(Q) + val atl = follows(s4, outEdges, WhileFailed, v3, joinPoint)(Q) wde combine lie combine atl }) @@ -368,7 +372,8 @@ object executor extends ExecutionRules { (s1, v1, QS) => consumes(s1, invs, LoopInvariantNotPreserved, v1)(QS) } { - (s2, _, v2) => Q(s2, v2) + (s2, _, v2) => + Q(s2, v2) } { f => // There are cases where it is incorrect to abduce state here, but only some cases and it is hard to distinguish them @@ -378,17 +383,17 @@ object executor extends ExecutionRules { } } - def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier) + def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) (Q: (State, Verifier) => VerificationResult) : VerificationResult = if (stmts.nonEmpty) - exec(s, stmts.head, v)((s1, v1) => - execs(s1, stmts.tail, v1)(Q)) + exec(s, stmts.head, v, doAbduction)((s1, v1) => + execs(s1, stmts.tail, v1, doAbduction)(Q)) else Q(s, v) - def exec(s: State, stmt: ast.Stmt, v: Verifier) + def exec(s: State, stmt: ast.Stmt, v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { val sepIdentifier = v.symbExLog.openScope(new ExecuteRecord(stmt, s, v.decider.pcs)) @@ -399,11 +404,16 @@ object executor extends ExecutionRules { Q(s2, v2) } { f => - BiAbductionSolver.solveAbduction(s, v, f, Some(stmt))((s3, res, v3) => { - v3.symbExLog.closeScope(sepIdentifier) - Success(Some(res)) && exec(s3, stmt, v3)(Q) + if (doAbduction) { + val loc = if (abdLoc.isDefined) abdLoc else Some(stmt) + BiAbductionSolver.solveAbduction(s, v, f, loc)((s3, res, v3) => { + v3.symbExLog.closeScope(sepIdentifier) + Success(Some(res)) && exec(s3, stmt, v3)(Q) + } + ) + } else { + f } - ) } } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 576257b7b..2de7f8abf 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -19,7 +19,6 @@ import viper.silicon.utils.freshSnap import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.{Map, toMap} import viper.silver.ast -import viper.silver.ast.Method import viper.silver.components.StatefulComponent import viper.silver.reporter.AnnotationWarning import viper.silver.verifier.DummyNode diff --git a/src/test/resources/biabduction/dafny/examples-16.0.0.vpr b/src/test/resources/biabduction/dafny/checksum/checksum1.vpr similarity index 63% rename from src/test/resources/biabduction/dafny/examples-16.0.0.vpr rename to src/test/resources/biabduction/dafny/checksum/checksum1.vpr index ff0314d23..c5ba23a1b 100644 --- a/src/test/resources/biabduction/dafny/examples-16.0.0.vpr +++ b/src/test/resources/biabduction/dafny/checksum/checksum1.vpr @@ -8,12 +8,11 @@ predicate ChecksumMachine(this: Ref) method ChecksumMachineConstructor() returns (this: Ref) - ensures ChecksumMachine(this) - //ensures unfolding ChecksumMachine(this) in this.checksumData == 0 + //ensures ChecksumMachine(this) { this := new(checksumData) this.checksumData := 0 - fold ChecksumMachine(this) + //fold ChecksumMachine(this) } diff --git a/src/test/resources/biabduction/dafny/examples-16.0.1.vpr b/src/test/resources/biabduction/dafny/checksum/checksum2.vpr similarity index 52% rename from src/test/resources/biabduction/dafny/examples-16.0.1.vpr rename to src/test/resources/biabduction/dafny/checksum/checksum2.vpr index 6c2c60151..5abf5a209 100644 --- a/src/test/resources/biabduction/dafny/examples-16.0.1.vpr +++ b/src/test/resources/biabduction/dafny/checksum/checksum2.vpr @@ -7,14 +7,13 @@ predicate ChecksumMachine(this: Ref) } method Append(this: Ref, d: Int) - requires ChecksumMachine(this) + //requires ChecksumMachine(this) requires 0 <= d - ensures ChecksumMachine(this) - //ensures getChecksumData(this) == old(getChecksumData(this)) + d + //ensures ChecksumMachine(this) { - unfold ChecksumMachine(this) + //unfold ChecksumMachine(this) this.checksumData := this.checksumData + d - fold ChecksumMachine(this) + //fold ChecksumMachine(this) } diff --git a/src/test/resources/biabduction/dafny/exercises-16.0.vpr b/src/test/resources/biabduction/dafny/checksum/exercises-16.0.vpr similarity index 86% rename from src/test/resources/biabduction/dafny/exercises-16.0.vpr rename to src/test/resources/biabduction/dafny/checksum/exercises-16.0.vpr index 99a04fbaf..d8d7050d8 100644 --- a/src/test/resources/biabduction/dafny/exercises-16.0.vpr +++ b/src/test/resources/biabduction/dafny/checksum/exercises-16.0.vpr @@ -1,18 +1,7 @@ //import "examples-16.0.vpr" + field checksumData: Int -// Exercise 16.3 -/** - * This is a quick implementation of the ChecksumMachine with an additional - * field ocs, which is an optional checksum value. The checksum value will only - * be computed if it is not already present in the ocs field. If a checksum is - * present, it will be returned instead of recomputing it. When the - * checksumData value changes, the ocs field will be reset to None. This avoids - * an additional computation of the checksum value because we would have to - * check if the ocs value is still correct. - * Because the implementation is a variation of already seen and explained code, - * we will not go into detail about the individual code sections. - */ adt Option[T] { Some(value: T) None() diff --git a/src/test/resources/biabduction/dafny/examples-16.2.vpr b/src/test/resources/biabduction/dafny/coffee/examples-16.2.vpr similarity index 100% rename from src/test/resources/biabduction/dafny/examples-16.2.vpr rename to src/test/resources/biabduction/dafny/coffee/examples-16.2.vpr diff --git a/src/test/resources/biabduction/dafny/exercises-16.2.vpr b/src/test/resources/biabduction/dafny/coffee/exercises-16.2.vpr similarity index 55% rename from src/test/resources/biabduction/dafny/exercises-16.2.vpr rename to src/test/resources/biabduction/dafny/coffee/exercises-16.2.vpr index 4fb937174..bb5ffb1e3 100644 --- a/src/test/resources/biabduction/dafny/exercises-16.2.vpr +++ b/src/test/resources/biabduction/dafny/coffee/exercises-16.2.vpr @@ -1,12 +1,5 @@ import "examples-16.2.vpr" -// Exercise 16.8 -/** - * This method is an extension of the CoffeeMaker code from 16.2. It removes - * the grinder from a given CoffeeMaker and returns it. The CoffeeMaker - * receives a new grinder without any beans inside. The state of the removed - * grinder is maintained. The harness tests its functionality. - */ method CoffeemakerRemoveGrinder(this: Ref) returns (grinder: Ref) requires CoffeeMaker(this) ensures CoffeeMaker(this) @@ -26,11 +19,4 @@ method RemoveGrinderHarness() var grinder: Ref := CoffeemakerRemoveGrinder(cm) CoffeeMakerRestock(cm) GrinderAddBeans(grinder) -} - -// Exercise 16.9 -/** - * This exercise wants to add representation sets to the basic implementation - * from 16.0. Because representation sets are not needed with Viper predicates, - * we do not need to solve this exercise. - */ \ No newline at end of file +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/exercises-16.3.vpr b/src/test/resources/biabduction/dafny/exercises-16.3.vpr deleted file mode 100644 index 5d2b4853b..000000000 --- a/src/test/resources/biabduction/dafny/exercises-16.3.vpr +++ /dev/null @@ -1,16 +0,0 @@ -// Exercise 16.10 -/** - * Skipped because it concerns representation sets only. - */ - -// Exercise 16.11 -/** - * The current implementation already supports the desired functionality - * because we do not need representation sets. - */ - -// Exercise 16.12 -/** - * You may also use the VSCode IDE with the Viper extension to get IDE - * functionality and support for your Viper programs. - */ \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/exercises-16.1.vpr b/src/test/resources/biabduction/dafny/tokenizer/exercises-16.1.vpr similarity index 99% rename from src/test/resources/biabduction/dafny/exercises-16.1.vpr rename to src/test/resources/biabduction/dafny/tokenizer/exercises-16.1.vpr index ea358c5c4..707d90cdb 100644 --- a/src/test/resources/biabduction/dafny/exercises-16.1.vpr +++ b/src/test/resources/biabduction/dafny/tokenizer/exercises-16.1.vpr @@ -1,10 +1,5 @@ import "examples-16.1.vpr" -// Exercise 16.5 -/** - * Skipped because it is textual. - */ - // Exercise 16.6 /** * This is a modification of the Tokenizer code from the section 16.1 where we diff --git a/src/test/resources/biabduction/dafny/examples-16.1.0.vpr b/src/test/resources/biabduction/dafny/tokenizer/tokenizer1.vpr similarity index 79% rename from src/test/resources/biabduction/dafny/examples-16.1.0.vpr rename to src/test/resources/biabduction/dafny/tokenizer/tokenizer1.vpr index daf49ebc3..2c47feb12 100644 --- a/src/test/resources/biabduction/dafny/examples-16.1.0.vpr +++ b/src/test/resources/biabduction/dafny/tokenizer/tokenizer1.vpr @@ -11,13 +11,12 @@ predicate Tokenizer(this: Ref) method TokenizerConstructor(s: Seq[Int]) returns (this: Ref) requires forall i: Int :: 0 <= i < |s| ==> 0 <= s[i] <= 127 - ensures Tokenizer(this) - //ensures getSource(this) == s && getN(this) == 0 + //ensures Tokenizer(this) { this := new(source, n) this.source := s this.n := 0 - fold Tokenizer(this) + //fold Tokenizer(this) } diff --git a/src/test/resources/biabduction/dafny/examples-16.1.1.vpr b/src/test/resources/biabduction/dafny/tokenizer/tokenizer2.vpr similarity index 64% rename from src/test/resources/biabduction/dafny/examples-16.1.1.vpr rename to src/test/resources/biabduction/dafny/tokenizer/tokenizer2.vpr index ad1b669db..00c2bb2cd 100644 --- a/src/test/resources/biabduction/dafny/examples-16.1.1.vpr +++ b/src/test/resources/biabduction/dafny/tokenizer/tokenizer2.vpr @@ -49,30 +49,30 @@ function getN(this: Ref): Int } method Read(this: Ref) returns (cat: Category, p: Int, token: Seq[Int]) - requires Tokenizer(this) - ensures 0 <= p - ensures Tokenizer(this) - ensures getSource(this) == old(getSource(this)) - ensures !cat.isWhitespace - ensures old(getN(this)) <= p <= getN(this) <= |getSource(this)| - ensures cat.isEnd <==> p == |getSource(this)| - ensures cat.isEnd || cat.isError <==> p == getN(this) - ensures forall i: Int :: old(getN(this)) <= i < p ==> - Is(getSource(this)[i], Whitespace()) - ensures forall i: Int :: p <= i < getN(this) ==> Is(getSource(this)[i], cat) - ensures p < getN(this) ==> getN(this) == |getSource(this)| || !Is(getSource(this)[getN(this)], cat) - ensures !cat.isError ==> token == getSource(this)[p..getN(this)] + //requires Tokenizer(this) + //ensures Tokenizer(this) + //ensures 0 <= p + //ensures getSource(this) == old(getSource(this)) + //ensures !cat.isWhitespace + //ensures old(getN(this)) <= p <= getN(this) <= |getSource(this)| + //ensures cat.isEnd <==> p == |getSource(this)| + //ensures cat.isEnd || cat.isError <==> p == getN(this) + //ensures forall i: Int :: old(getN(this)) <= i < p ==> + // Is(getSource(this)[i], Whitespace()) + //ensures forall i: Int :: p <= i < getN(this) ==> Is(getSource(this)[i], cat) + //ensures p < getN(this) ==> getN(this) == |getSource(this)| || !Is(getSource(this)[getN(this)], cat) + //ensures !cat.isError ==> token == getSource(this)[p..getN(this)] { // skip whitespace while (getN(this) != |getSource(this)| && Is(getSource(this)[getN(this)], Whitespace())) - invariant Tokenizer(this) - invariant getSource(this) == old(getSource(this)) - invariant old(getN(this)) <= getN(this) <= |getSource(this)| - invariant forall i: Int :: old(getN(this)) <= i < getN(this) ==> Is(getSource(this)[i], Whitespace()) + //invariant Tokenizer(this) + //invariant getSource(this) == old(getSource(this)) + //invariant old(getN(this)) <= getN(this) <= |getSource(this)| + //invariant forall i: Int :: old(getN(this)) <= i < getN(this) ==> Is(getSource(this)[i], Whitespace()) { - unfold Tokenizer(this) + //unfold Tokenizer(this) this.n := this.n + 1 - fold Tokenizer(this) + //fold Tokenizer(this) } p := getN(this) // determine syntactic category @@ -105,18 +105,18 @@ method Read(this: Ref) returns (cat: Category, p: Int, token: Seq[Int]) if (!return) { var start: Int := getN(this) - unfold Tokenizer(this) + //unfold Tokenizer(this) this.n := this.n + 1 - fold Tokenizer(this) + //fold Tokenizer(this) while (getN(this) != |getSource(this)| && Is(getSource(this)[getN(this)], cat)) - invariant Tokenizer(this) - invariant getSource(this) == old(getSource(this)) - invariant p <= getN(this) <= |getSource(this)| - invariant forall i: Int :: p <= i < getN(this) ==> Is(getSource(this)[i], cat) + //invariant Tokenizer(this) + //invariant getSource(this) == old(getSource(this)) + //invariant p <= getN(this) <= |getSource(this)| + //invariant forall i: Int :: p <= i < getN(this) ==> Is(getSource(this)[i], cat) { - unfold Tokenizer(this) + //unfold Tokenizer(this) this.n := this.n + 1 - fold Tokenizer(this) + //fold Tokenizer(this) } token := getSource(this)[start..getN(this)] } diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr index 1ebf7fe32..d63ef4e09 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr @@ -6,7 +6,7 @@ requires list(y) //ensures list(res) { if (x == null) { - x := y + res := y } else { var curr: Ref := x //package list(curr) --* list(x) @@ -20,13 +20,15 @@ requires list(y) curr := curr.next //unfold list(curr) //package list(curr) --* list(x) { - // fold list(prev) - // apply list(prev) --* list(x) + // fold list(prev) + // apply list(prev) --* list(x) //} } curr.next := y - //fold list(curr) - //apply list(curr) --* list(x) res := x } + //if(x != null){ + // fold list(curr) + // apply list(curr) --* list(x) + //} } diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_dispose.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_dispose.vpr index 8c5e98ccf..9a1df0350 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_dispose.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_dispose.vpr @@ -1,19 +1,19 @@ import "./sl.vpr" method dispose(lst: Ref) -requires list(lst) +//requires list(lst) { var curr: Ref := lst while(curr != null) - invariant list(curr) + //invariant list(curr) { var curr_old: Ref := curr - unfold list(curr) + //unfold list(curr) curr := curr.next free(curr_old) } } method free(x: Ref) -requires acc(x.next) \ No newline at end of file +requires acc(x.next) && acc(x.data) diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_double_all.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_double_all.vpr index 35fe342ae..9864dde87 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_double_all.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_double_all.vpr @@ -1,29 +1,25 @@ import "./sl.vpr" method sls_double_all(lst: Ref) returns (res: Ref) -requires list(lst) -requires lst != null -ensures list(lst) +//requires list(lst) +//ensures list(lst) { var x: Ref := lst - //var bound: Int := unfolding list(x) in x.data - - package list(x) --* list(lst) + //package list(x) --* list(lst) while(x != null) - invariant list(x) - //invariant x != null ==> unfolding list(x) in bound <= x.data - invariant list(x) --* list(lst) + //invariant list(x) + //invariant list(x) --* list(lst) { var x_old: Ref := x - //var old_bound: Int := bound - unfold list(x) - //bound := x.data + //unfold list(x) + x.data := x.data * 2 x := x.next - package list(x) --* list(lst) { - fold list(x_old) - apply list(x_old) --* list(lst) - } + + //package list(x) --* list(lst) { + // fold list(x_old) + // apply list(x_old) --* list(lst) + //} } - apply list(x) --* list(lst) + //apply list(x) --* list(lst) } \ No newline at end of file diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr index c2b7a1aa6..ed535ef2b 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr @@ -1,46 +1,51 @@ import "./sl.vpr" method filter(x: Ref) returns (res: Ref) -requires list(x) -ensures list(x) +//requires list(x) +//ensures list(x) { if(x == null) { res := null } else { - unfold list(x) + //unfold list(x) var prev: Ref := x var curr: Ref := x.next - package list(prev) --* list(x) + //package list(prev) --* list(x) while(curr != null) - invariant list(prev) --* list(x) - invariant acc(prev.next) && acc(prev.data) + //invariant list(prev) --* list(x) + invariant acc(prev.next) + //invariant acc(prev.data) invariant prev.next == curr - invariant list(curr) + //invariant list(curr) { var old_curr: Ref := curr var old_prev: Ref := prev - unfold list(curr) + //unfold list(curr) curr := curr.next var nondet: Bool if(nondet) { prev.next := curr; + free(old_curr) } else { prev := old_curr } if(!nondet){ - package list(prev) --* list(x) { - fold list(old_prev) - apply list(old_prev) --* list(x) - } + //package list(prev) --* list(x) { + // fold list(old_prev) + // apply list(old_prev) --* list(x) + //} } } - fold list(curr) - fold list(prev) - apply list(prev) --* list(x) + //fold list(curr) + //fold list(prev) + //apply list(prev) --* list(x) } -} \ No newline at end of file +} + +method free(x: Ref) +requires acc(x.next) && acc(x.data) \ No newline at end of file diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr index a6730f061..4ff3888a5 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr @@ -1,40 +1,41 @@ import "./sl.vpr" method insert(x: Ref, elt: Ref) returns (res: Ref) -requires list(x) && acc(elt.next) && acc(elt.data) -ensures list(res) +//requires list(x) +//requires acc(elt.next) && acc(elt.data) +//ensures list(res) { if(x == null){ elt.next := null - fold list(elt.next) - fold list(elt) + //fold list(elt.next) + //fold list(elt) res := elt } else { var nondet: Bool var curr: Ref := x - package list(curr) --* list(x) - unfold list(curr) + //package list(curr) --* list(x) + //unfold list(curr) while(nondet && curr.next != null) - invariant acc(curr.next) && acc(curr.data) - invariant list(curr.next) - invariant list(curr) --* list(x) + //invariant acc(curr.next) && acc(curr.data) + //invariant list(curr.next) + //invariant list(curr) --* list(x) { var old_curr: Ref := curr nondet := havoc() curr := curr.next - unfold list(curr) - package list(curr) --* list(x) { - fold list(old_curr) - apply list(old_curr) --* list(x) - } + //unfold list(curr) + //package list(curr) --* list(x) { + // fold list(old_curr) + // apply list(old_curr) --* list(x) + //} } elt.next := curr.next curr.next := elt - fold list(elt) - fold list(curr) - apply list(curr) --* list(x) + //fold list(elt) + //fold list(curr) + //apply list(curr) --* list(x) res := x } } diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_pairwise_sum.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_pairwise_sum.vpr index 25ff0a7a4..04af57202 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_pairwise_sum.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_pairwise_sum.vpr @@ -1,12 +1,12 @@ import "./sl.vpr" method pairwise_sum(x: Ref, y: Ref) returns (z: Ref) -requires list(x) && list(y) -ensures list(x) && list(y) && list(z) +//requires list(x) && list(y) +//ensures list(x) && list(y) && list(z) { if(x == null || y == null){ z := null - fold list(z) + //fold list(z) } else { z := new(*) @@ -15,24 +15,24 @@ ensures list(x) && list(y) && list(z) var curr_y: Ref := y var curr_z: Ref := z - package list(x) --* list(x) - package list(y) --* list(y) - package list(z) --* list(z) + //package list(x) --* list(x) + //package list(y) --* list(y) + //package list(z) --* list(z) - unfold list(x) - unfold list(y) + //unfold list(x) + //unfold list(y) //z.next := null //fold list(z.next) z.data := x.data + y.data while(curr_x.next != null && curr_y.next != null) - invariant acc(curr_x.next) && acc(curr_x.data) && list(curr_x.next) - invariant list(curr_x) --* list(x) - invariant acc(curr_y.next) && acc(curr_y.data) && list(curr_y.next) - invariant list(curr_y) --* list(y) - invariant acc(curr_z.next) && acc(curr_z.data) - invariant list(curr_z) --* list(z) + //invariant acc(curr_x.next) && acc(curr_x.data) && list(curr_x.next) + //invariant list(curr_x) --* list(x) + //invariant acc(curr_y.next) && acc(curr_y.data) && list(curr_y.next) + //invariant list(curr_y) --* list(y) + //invariant acc(curr_z.next) && acc(curr_z.data) + //invariant list(curr_z) --* list(z) { var prev_x: Ref := curr_x var prev_y: Ref := curr_y @@ -40,15 +40,15 @@ ensures list(x) && list(y) && list(z) curr_x := curr_x.next curr_y := curr_y.next - unfold list(curr_x) - unfold list(curr_y) + //unfold list(curr_x) + //unfold list(curr_y) curr_z := new(*) curr_z.next := null curr_z.data := curr_x.data + curr_y.data prev_z.next := curr_z - + /* package list(curr_x) --* list(x){ fold list(prev_x) apply list(prev_x) --* list(x) @@ -63,15 +63,16 @@ ensures list(x) && list(y) && list(z) fold list(prev_z) apply list(prev_z) --* list(z) } + */ } - fold list(curr_x) - apply list(curr_x) --* list(x) - fold list(curr_y) - apply list(curr_y) --* list(y) + //fold list(curr_x) + //apply list(curr_x) --* list(x) + //fold list(curr_y) + //apply list(curr_y) --* list(y) curr_z.next := null - fold list(curr_z.next) - fold list(curr_z) - apply list(curr_z) --* list(z) + //fold list(curr_z.next) + //fold list(curr_z) + //apply list(curr_z) --* list(z) } } \ No newline at end of file diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr index 74e4a8b42..809c37327 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr @@ -18,5 +18,4 @@ ensures list(res) res := tmp fold list(tmp) } - } \ No newline at end of file diff --git a/src/test/resources/biabduction/mytests/nlist/chain.vpr b/src/test/resources/biabduction/mytests/nlist/chain.vpr new file mode 100644 index 000000000..b27db5a2f --- /dev/null +++ b/src/test/resources/biabduction/mytests/nlist/chain.vpr @@ -0,0 +1,10 @@ +field next: Ref + +method test(x: Ref) +{ + var y: Ref := x.next + + var z: Ref := y.next + + var a: Ref := z.next +} \ No newline at end of file diff --git a/src/test/resources/biabduction/vipertests/basic/disjunction_fast_20.vpr b/src/test/resources/biabduction/vipertests/basic/disjunction_fast_20.vpr index e13c89870..84e149f5f 100644 --- a/src/test/resources/biabduction/vipertests/basic/disjunction_fast_20.vpr +++ b/src/test/resources/biabduction/vipertests/basic/disjunction_fast_20.vpr @@ -1,11 +1,3 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -/* - * The performance of silicon used to depend on the disjunction order in the following predicate - * Compare disjunction_slow_20.vpr - */ - field val: Int predicate Slow(this: Ref) { @@ -16,198 +8,198 @@ predicate Slow(this: Ref) { method havoc() returns (res:Int) method test(this: Ref) - requires Slow(this) - ensures Slow(this) + //requires Slow(this) + //ensures Slow(this) { - unfold Slow(this) + //unfold Slow(this) var tmp: Int tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) + //fold Slow(this) } diff --git a/src/test/resources/biabduction/vipertests/basic/disjunction_slow_20.vpr b/src/test/resources/biabduction/vipertests/basic/disjunction_slow_20.vpr index 5586bf8fc..d78270e5d 100644 --- a/src/test/resources/biabduction/vipertests/basic/disjunction_slow_20.vpr +++ b/src/test/resources/biabduction/vipertests/basic/disjunction_slow_20.vpr @@ -16,198 +16,198 @@ predicate Slow(this: Ref) { method havoc() returns (res:Int) method test(this: Ref) - requires Slow(this) - ensures Slow(this) + //requires Slow(this) + //ensures Slow(this) { - unfold Slow(this) + //unfold Slow(this) var tmp: Int tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) - unfold Slow(this) + //fold Slow(this) + //unfold Slow(this) tmp := havoc() this.val := tmp - fold Slow(this) + //fold Slow(this) } diff --git a/src/test/resources/biabduction/vipertests/basic/funcpred.vpr b/src/test/resources/biabduction/vipertests/basic/funcpred.vpr index 551b992f7..e82f6d709 100644 --- a/src/test/resources/biabduction/vipertests/basic/funcpred.vpr +++ b/src/test/resources/biabduction/vipertests/basic/funcpred.vpr @@ -19,12 +19,12 @@ predicate valid(this: Ref) { } method a(this: Ref) - requires acc(valid(this), write) && acc(this.f, write) - ensures acc(valid(this), write) + //requires acc(valid(this), write) && acc(this.f, write) + //ensures acc(valid(this), write) { - unfold acc(valid(this), write) + //unfold acc(valid(this), write) this.value := 1 - fold acc(valid(this), write) + //fold acc(valid(this), write) void(this) assert itemat(this, 0) == 1 } diff --git a/src/test/resources/biabduction/vipertests/functions/linkedlists.vpr b/src/test/resources/biabduction/vipertests/functions/linkedlists.vpr index 354b4b49f..b31f147a9 100644 --- a/src/test/resources/biabduction/vipertests/functions/linkedlists.vpr +++ b/src/test/resources/biabduction/vipertests/functions/linkedlists.vpr @@ -1,17 +1,3 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -//:: IgnoreFile(/silicon/issue/104/) - -// NOTES (important points are also commented in the code below) -// (1) The definition of list(xs) precludes the case xs==null. But, without unfolding the predicate, this information is not available. This is important for e.g., -// showing that length increases by 1 when prepending. For now, the explicit non-nullity of the argument has been conjoined everywhere. -// (2) The definition of the function ascending in terms of the function head means that framing head is often necessary. This is true even in cases where the head -// element is "clear", e.g. when a postcondition about elems is also written, since relating the sequence to the head() function is not automatic. -// (3) The relationships between different abstractions is not always automatic. For example, the if-condition tail(xs)==null actually implies that elems(xs) has -// length 1 and also that head(xs) == tail(xs). Both of these facts are needed to prove the postconditions of insert. Resorting to limited functions would allow -// manual assertions to trigger these properties. Without limited-functions-style triggering (i.e. only based on fold/unfold of predicates), these must be assumptions - field next: Ref field val: Int @@ -54,12 +40,13 @@ function get(xs: Ref, index: Int): Int { unfolding acc(list(xs)) in index == 0 ? xs.val : get(xs.next, index - 1) } method prepend(xs: Ref, y: Int) returns (ys: Ref) - requires acc(list(xs)) && xs != null - ensures acc(list(ys)) && ys != null - ensures length(ys) == old(length(xs)) + 1 // (1) - ensures elems(ys) == Seq(y) ++ old(elems(xs)) - ensures head(ys) == y // (2) - ensures old(y <= head(xs) && ascending(xs)) ==> ascending(ys) + //requires acc(list(xs)) && xs != null + //ensures acc(list(ys)) + //ensures ys != null + //ensures length(ys) == old(length(xs)) + 1 // (1) + //ensures elems(ys) == Seq(y) ++ old(elems(xs)) + //ensures head(ys) == y // (2) + //ensures old(y <= head(xs) && ascending(xs)) ==> ascending(ys) { ys := new(val, next) ys.val := y @@ -67,6 +54,7 @@ method prepend(xs: Ref, y: Int) returns (ys: Ref) fold acc(list(ys)) } + method append(xs: Ref, y: Int) requires acc(list(xs)) && xs != null ensures acc(list(xs)) && xs != null @@ -160,4 +148,4 @@ method test02(xs: Ref, x: Int, ys: Ref) fold acc(list(xs)) assert forall i: Int :: i in [1..length(xs)) ==> get(xs, i) == unfolding acc(list(xs), write) in get(ys, i - 1) -} +} \ No newline at end of file diff --git a/src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr b/src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr index 778c8563e..c9a270c9d 100644 --- a/src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr +++ b/src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr @@ -7,45 +7,40 @@ predicate node(this: Ref) { acc(this.next) && (this.next != null ==> acc(node(this.next))) } -function length(this: Ref): Int - requires acc(node(this)) - ensures result > 0 -{ - 1 + unfolding acc(node(this)) in - this.next == null ? 0 : length(this.next) -} - +/* method test01() { var n1: Ref; n1 := new(next) n1.next := null - fold acc(node(n1)) + //fold acc(node(n1)) var n2: Ref; n2 := new(next) n2.next := n1 - fold acc(node(n2)) + //fold acc(node(n2)) var n3: Ref; n3 := new(next) n3.next := n2 - fold acc(node(n3)) + //fold acc(node(n3)) var n4: Ref; n4 := new(next) n4.next := n3 - fold acc(node(n4)) + //fold acc(node(n4)) var n5: Ref; n5 := new(next) n5.next := n4 - fold acc(node(n5)) + //fold acc(node(n5)) - assert length(n5) == 5 + assert acc(node(n5)) } +*/ method test02(n4: Ref) - requires acc(node(n4)) && length(n4) == 4 + //requires acc(node(n4)) + //requires length(n4) == 4 { - unfold acc(node(n4)) - unfold acc(node(n4.next)) - unfold acc(node(n4.next.next)) - unfold acc(node(n4.next.next.next)) + //unfold acc(node(n4)) + //unfold acc(node(n4.next)) + //unfold acc(node(n4.next.next)) + //unfold acc(node(n4.next.next.next)) - assert n4.next.next.next.next == null + n4.next.next.next.next := null }