diff --git a/src/main/scala/biabduction/Abduction.scala b/src/main/scala/biabduction/Abduction.scala index 77467728b..733e6b8fa 100644 --- a/src/main/scala/biabduction/Abduction.scala +++ b/src/main/scala/biabduction/Abduction.scala @@ -2,7 +2,6 @@ package viper.silicon.biabduction import viper.silicon import viper.silicon.interfaces._ -import viper.silicon.resources.{FieldID, PredicateID} import viper.silicon.rules._ import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.rules.evaluator.{eval, evals} @@ -11,8 +10,8 @@ import viper.silicon.state._ import viper.silicon.state.terms.{SortWrapper, Term} import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier -import viper.silver.ast import viper.silver.ast._ +import viper.silver.verifier.errors.Internal import viper.silver.verifier.{BiAbductionQuestion, DummyReason} object AbductionApplier extends RuleApplier[AbductionQuestion] { @@ -21,8 +20,8 @@ object AbductionApplier extends RuleApplier[AbductionQuestion] { } case class AbductionQuestion(s: State, v: Verifier, goal: Seq[Exp], - lostAccesses: Map[Exp, Term] = Map(), foundState: Seq[Exp] = Seq(), - foundStmts: Seq[Stmt] = Seq(), trigger: Option[Positioned]) extends BiAbductionQuestion + lostAccesses: Map[Exp, Term] = Map(), foundState: Seq[(Exp, Option[BasicChunk])] = Seq(), + foundStmts: Seq[Stmt] = Seq(), trigger: Option[Positioned], stateAllowed: Boolean) extends BiAbductionQuestion /** * A rule for abduction. A rule is a pair of a check method and an apply method. The check method checks whether the @@ -222,7 +221,7 @@ object AbductionFold extends AbductionRule { //val pveTransformed = pve.withReasonNodeTransformed(reasonTransformer) val fold = Fold(a)() - executor.exec(q.s, fold, q.v, doAbduction = true, q.trigger) { (s1, v1) => + 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)) @@ -324,7 +323,7 @@ object AbductionUnfold extends AbductionRule { 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, FullPerm()())())(), foundState = q.foundState ++ conds))) + Q(Some(q.copy(s = s2, v = v2, foundStmts = q.foundStmts :+ Unfold(PredicateAccessPredicate(pred, FullPerm()())())(), foundState = q.foundState ++ conds.map(c => c -> None)))) } }) } @@ -374,7 +373,7 @@ object AbductionApply extends AbductionRule { 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))) + Q(Some(AbductionQuestion(s2, v2, g1, lost, state, stmts, q.trigger, q.stateAllowed))) /*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)()))) @@ -402,23 +401,42 @@ object AbductionPackage extends AbductionRule { q.goal.collectFirst { case a: MagicWand => a } match { case None => Q(None) case Some(wand) => - 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 => - - 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 - //val lost = q.lostAccesses ++ packRes.lostAccesses - Q(Some(q.copy(s = packRes.s, v = packRes.v, goal = g1, foundStmts = stmts, foundState = pres))) + 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 = Seq(wand.right)) + AbductionApplier.applyRules(packQ) { packRes => + if (packRes.goal.nonEmpty) { + Failure(pve dueTo(DummyReason)) + //T(BiAbductionFailure(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate())) + } else { + val newState = packRes.foundState + val newStmts = packRes.foundStmts + Success(Some(AbductionSuccess(packRes.s, packRes.v, packRes.v.decider.pcs.duplicate(), newState, newStmts, Map(), None))) + } } } - }) + } 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 script = Seqn(stmts, Seq())() + magicWandSupporter.packageWand(s1, 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))) + } + } + } } } } @@ -430,13 +448,20 @@ object AbductionPackage extends AbductionRule { object AbductionMissing extends AbductionRule { override def apply(q: AbductionQuestion)(Q: Option[AbductionQuestion] => VerificationResult): VerificationResult = { - val accs = q.goal.collect { case e: AccessPredicate => e } - if (accs.isEmpty) { + val accs = q.goal.collect { + 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) => - Q(Some(q.copy(s = s1, v = v1, goal = g1, foundState = q.foundState ++ accs))) + val locs: Map[LocationAccess, Exp] = accs.map {p => p.loc -> p}.toMap + abductionUtils.findChunks(locs.keys.toSeq, s1, v1, Internal()) { newChunks => + val newState = newChunks.map {case (c, loc) => (locs(loc), Some(c))} + Q(Some(q.copy(s = s1, 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 d9b7013eb..a0427b7b4 100644 --- a/src/main/scala/biabduction/Abstraction.scala +++ b/src/main/scala/biabduction/Abstraction.scala @@ -14,67 +14,70 @@ object AbstractionApplier extends RuleApplier[AbstractionQuestion] { override val rules: Seq[AbstractionRule] = Seq(AbstractionFold, AbstractionPackage, AbstractionJoin, AbstractionApply) } -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 +case class AbstractionQuestion(s: State, v: Verifier) { def varTran: VarTransformer = VarTransformer(s, v, s.g.values, s.h) - def isTriggerField(bc: BasicChunk): Boolean = { - bc.resourceID match { - case FieldID => fields.contains(abductionUtils.getField(bc.id, s.program)) && !fixedChunks.contains(bc) - case _ => false - } - } } trait AbstractionRule extends BiAbductionRule[AbstractionQuestion] object AbstractionFold extends AbstractionRule { - private def checkChunks(chunks: Seq[BasicChunk], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { + + // TODO we assume each field only appears in at most one predicate + private def getFieldPredicate(bc: BasicChunk, q: AbstractionQuestion): Option[Predicate] = { + + if (bc.resourceID != FieldID) None else { + val field = abductionUtils.getField(bc.id, q.s.program) + + q.s.program.predicates.collectFirst { case pred if pred.collect{case fa: FieldAccess => fa.field}.toSeq.contains(field) => pred } + } + } + + private def checkChunks(chunks: Seq[(BasicChunk, Predicate)], q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { chunks match { - case Seq() => Q(None) - case chunk +: rest => - val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program)) + case _ if chunks.isEmpty => Q(None) + case (chunk, pred) +: rest => + //val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program)) val wildcards = q.s.constrainableARPs -- q.s.constrainableARPs executionFlowController.tryOrElse0(q.s, q.v) { (s1, v1, T) => - val fargs = pred.formalArgs.map(_.localVar) + //val fargs = pred.formalArgs.map(_.localVar) val eArgs = q.varTran.transformTerm(chunk.args.head) - val formalsToActuals: Map[LocalVar, Exp] = fargs.zip(eArgs).to(Map) - val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals) - val pveTransformed = pve.withReasonNodeTransformed(reasonTransformer) + //val formalsToActuals: Map[LocalVar, 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(PredicateAccessPredicate(PredicateAccess(Seq(eArgs.get), pred.name)(), FullPerm()())())() + executor.exec(s1, fold, v1, None, abdStateAllowed = false)(T) // TODO nklose this can branch - predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pveTransformed, v1)(T) + //predicateSupporter.fold(s1, pred, List(chunk.args.head), None, terms.FullPerm, Some(FullPerm()()), wildcards, pveTransformed, v1)(T) } { (s2, v2) => Q(Some(q.copy(s = s2, v = v2))) } { - f => + + f => checkChunks(rest, q)(Q) + + /* executionFlowController.tryOrElse0(q.s, q.v) { (s3, v3, T) => - BiAbductionSolver.solveAbduction(s3, v3, f, None) { (s4, res, v4) => - res.state match { - case Seq() => T(s4, v4) - case _ => f - } - } + BiAbductionSolver.solveAbductionForError(s3, v3, f, stateAllowed = false, None) { T } } { (s5, v5) => Q(Some(q.copy(s = s5, v = v5))) } { f => checkChunks(rest, q)(Q) - } + }*/ } } } override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - val candChunks = q.s.h.values.collect { case bc: BasicChunk if q.isTriggerField(bc) => bc }.toSeq + val candChunks = q.s.h.values.collect { case bc: BasicChunk => (bc, getFieldPredicate(bc, q)) }.collect { case (c, Some(pred)) => (c, pred) }.toSeq checkChunks(candChunks, q)(Q) } } @@ -82,30 +85,51 @@ object AbstractionFold extends AbstractionRule { object AbstractionPackage extends AbstractionRule { - // TODO nklose we should only trigger on fields for which there is a recursive predicate call + // TODO if the fold fails for a different reason than the recursive predicate missing, then this will do nonsense + // We should actually check what is missing and be smarter about what we package. + private def checkField(bc: BasicChunk, q: AbstractionQuestion): Option[MagicWand] = { + if (bc.resourceID != FieldID) None else { + + // TODO this fails if the sorts don't line up + 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 => None + case Some(lhsArgExp) => + val field = abductionUtils.getField(bc.id, q.s.program) + // TODO we assume each field only appears in at most one predicate + val predOpt = q.s.program.predicates.collectFirst { case pred if pred.collect{case fa: FieldAccess => fa.field}.toSeq.contains(field) => pred } + predOpt.flatMap { pred => + val recPredOpt = pred.collectFirst { + case recPred@PredicateAccess(Seq(FieldAccess(_, field2)), _) if field == field2 => recPred + } + recPredOpt.flatMap { recPred => + val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArgExp), recPred.predicateName)(NoPosition, NoInfo, NoTrafos), FullPerm()())() + val rhsArg = q.varTran.transformTerm(bc.args.head).get + val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())() + Some(MagicWand(lhs, rhs)()) + } + } + } + } + } + @tailrec - private def findWandFieldChunk(chunks: Seq[Chunk], q: AbstractionQuestion): Option[(Exp, BasicChunk)] = { + private def findWand(chunks: Seq[Chunk], q: AbstractionQuestion): Option[MagicWand] = { chunks match { case Seq() => None - case (chunk: BasicChunk) +: rest if q.isTriggerField(chunk) => - q.varTran.transformTerm(chunk.snap) match { - case None => findWandFieldChunk(rest, q) - case Some(snap) => Some((snap, chunk)) + case (chunk: BasicChunk) +: rest => + checkField(chunk, q) match { + case None => findWand(rest, q) + case wand => wand } - case _ +: rest => findWandFieldChunk(rest, q) + case (_: Chunk) +: rest => findWand(rest, q) } } override def apply(q: AbstractionQuestion)(Q: Option[AbstractionQuestion] => VerificationResult): VerificationResult = { - findWandFieldChunk(q.s.h.values.toSeq, q) match { + findWand(q.s.h.values.toSeq, q) match { case None => Q(None) - case Some((lhsArg, chunk)) => - val pred = q.fields(abductionUtils.getField(chunk.id, q.s.program)) - val lhs = PredicateAccessPredicate(PredicateAccess(Seq(lhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())() - val rhsArg = q.varTran.transformTerm(chunk.args.head).get - val rhs = PredicateAccessPredicate(PredicateAccess(Seq(rhsArg), pred)(NoPosition, NoInfo, NoTrafos), FullPerm()())() - val wand = MagicWand(lhs, rhs)() + case Some(wand) => executor.exec(q.s, Assert(wand)(), q.v) { (s1, v1) => Q(Some(q.copy(s = s1, v = v1))) @@ -137,7 +161,7 @@ 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 if !q.fixedChunks.contains(c) => q.varTran.transformChunk(c) }.collect { case Some(exp) => exp }.toSeq + 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 { case None => Q(None) diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index 71c96abc7..3559d27e2 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -2,14 +2,12 @@ package viper.silicon.biabduction import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces._ -import viper.silicon.interfaces.state.Chunk import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.rules.consumer.consumes -import viper.silicon.rules.{evaluator, executionFlowController, executor, producer} +import viper.silicon.rules.{evaluator, executionFlowController} import viper.silicon.state._ import viper.silicon.state.terms.{Term, True} import viper.silicon.utils.ast.BigAnd -import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ import viper.silver.verifier.errors.Internal @@ -27,19 +25,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(), newFieldChunks: Map[BasicChunk, LocationAccess], 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], trigger: Option[Positioned] = None) extends BiAbductionSuccess { + + val preTrans = VarTransformer override def toString: String = { "Abduced pres " + state.length + ", Abduced statements " + stmts.length } - def addToMethod(m: Method, bcsTerms: Seq[Term], newFieldChunks: Map[BasicChunk, LocationAccess]): Option[Method] = { + def addToMethod(m: Method, bcExps: Seq[Exp], 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, newFieldChunks) val finalStmts = getStatements(bcExps) v.decider.setPcs(prevPcs) @@ -51,7 +50,8 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat 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) + addToInnerBody(body, finalStmt) + //Seqn(, 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) @@ -73,20 +73,44 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat } } + private def addToInnerBody(outer: Seqn, bcStmts: Seq[Stmt]): Seqn = { + outer match { + case o@Seqn(Seq(in: Seqn), _) => + val newInner = addToInnerBody(in, bcStmts) + o.copy(ss = Seq(newInner))(o.pos, o.info, o.errT) + case in => in.copy(ss = in.ss ++ bcStmts)(pos = in.pos, info = in.info, errT = in.errT) + } + } + def getBcExps(bcsTerms: Seq[Term]): Seq[Option[Exp]] = { + val prevPcs = v.decider.pcs + + v.decider.setPcs(pcs) + val varTrans = VarTransformer(s, v, s.g.values, s.h) val bcExps = bcsTerms.map { t => varTrans.transformTerm(t) } - bcExps + + // 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 preTrans = VarTransformer(s, v, preVars, s.h) + val preExps = bcExps.map { + case Some(t) => preTrans.transformExp(t, strict = false) + case None => None + } + + v.decider.setPcs(prevPcs) + preExps } - def getStatements(bcExps: Seq[Option[Exp]]): Option[Seq[Stmt]] = { + def getStatements(bcExps: Seq[Exp]): Option[Seq[Stmt]] = { 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 { - val con = BigAnd(bcExps.collect { case Some(e) => e }) + val con = BigAnd(bcExps) con match { case _: TrueLit => Some(stmts) case _ => Some(Seq(If(con, Seqn(stmts, Seq())(), Seqn(Seq(), Seq())())())) @@ -94,7 +118,7 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat } } - def getPreconditions(preVars: Map[AbstractLocalVar, (Term, Option[Exp])], preHeap: Heap, bcExps: Seq[Option[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()) @@ -102,10 +126,10 @@ case class AbductionSuccess(s: State, v: Verifier, pcs: PathConditionStack, stat val varTrans = VarTransformer(s, v, preVars, preHeap, newFieldChunks) val presTransformed = state.map { pre => - varTrans.transformExp(pre) + varTrans.transformExp(pre._1) } val bcPreExps = bcExps.collect { - case Some(exp) => varTrans.transformExp(exp) + case exp => varTrans.transformExp(exp) } // If we cannot express the precondition, we have to fail @@ -266,76 +290,75 @@ trait BiAbductionRule[S] { object BiAbductionSolver { - def solveAbduction(s: State, v: Verifier, f: Failure, trigger: Option[Positioned] = None)(Q: (State, AbductionSuccess, Verifier) => VerificationResult): VerificationResult = { + def solveAbductionForError(s: State, v: Verifier, f: Failure, stateAllowed: Boolean, trigger: Option[Positioned] = None)(Q: (State, Verifier) => VerificationResult): VerificationResult = { - val initPcs = v.decider.pcs.duplicate() - //val initTra = VarTransformer(s, v, s.g.values, s.h) + if (!s.doAbduction) { + f + } else { - val reason = f.message.reason match { - case reason: InsufficientPermission => - val acc = reason.offendingNode match { - case n: FieldAccess => FieldAccessPredicate(n, FullPerm()())() - case n: PredicateAccess => PredicateAccessPredicate(n, FullPerm()())() - } - Some(acc) - case reason: MagicWandChunkNotFound => Some(reason.offendingNode) - case _ => None - } - reason match { - case None => f - case Some(abdGoal) => + val initPcs = v.decider.pcs.duplicate() + //val initTra = VarTransformer(s, v, s.g.values, s.h) - val tra = f.message.failureContexts.collectFirst { - case SiliconAbductionFailureContext(trafo) if trafo.isDefined => trafo.get - } + val reason = f.message.reason match { + case reason: InsufficientPermission => + val acc = reason.offendingNode match { + case n: FieldAccess => FieldAccessPredicate(n, FullPerm()())() + case n: PredicateAccess => PredicateAccessPredicate(n, FullPerm()())() + } + Some(acc) + case reason: MagicWandChunkNotFound => Some(reason.offendingNode) + case _ => None + } + reason match { + case None => f + case Some(abdGoal) => - //val reses = executionFlowController.locally(s, v) { (s1, v1) => - val qPre = AbductionQuestion(s, v, Seq(abdGoal), trigger = trigger) - val q = tra match { - case Some(trafo) => trafo.f(qPre).asInstanceOf[AbductionQuestion] - case _ => qPre - } - AbductionApplier.applyRules(q) { - q1 => - if (q1.goal.isEmpty) { - 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) => + val tra = f.message.failureContexts.collectFirst { + case SiliconAbductionFailureContext(trafo) if trafo.isDefined => trafo.get + } + + val qPre = AbductionQuestion(s, v, Seq(abdGoal), stateAllowed = stateAllowed, trigger = trigger) + val q = tra match { + case Some(trafo) => trafo.f(qPre).asInstanceOf[AbductionQuestion] + case _ => qPre + } + AbductionApplier.applyRules(q) { + q1 => + if (q1.goal.isEmpty) { + val newState = q1.foundState.reverse + val newStmts = q1.foundStmts + + // TODO nklose created chunks can go away again before we finish abduction, due to a package or a fold + // We have to do this in place when the chunks are created and not here + //abductionUtils.findChunks(newLocs, q1.s, q1.v, Internal()) { newChunks => 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 newChunks = newState.collect { case (e, 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 fieldChunks = newChunks.collect { case (c, fa: FieldAccess) => (c, fa) } + val fieldChunks = newState.collect { case (fa: FieldAccessPredicate, c) => (c.get, fa.loc) }.toMap val abd = AbductionSuccess(s1, q1.v, q1.v.decider.pcs.duplicate(), newState, newStmts, fieldChunks, trigger) - Q(s1, abd, q1.v) + Success(Some(abd)) && Q(s1, q1.v) } //} + } else { + f } - //} - } else { - f - } - } + } + } } } - def solveAbstraction(s: State, v: Verifier, fixedChunks: Seq[Chunk] = Seq())(Q: (State, Seq[Exp], Verifier) => VerificationResult): VerificationResult = { - val q = AbstractionQuestion(s, v, fixedChunks) + def solveAbstraction(s: State, v: Verifier)(Q: (State, Seq[Exp], Verifier) => VerificationResult): VerificationResult = { + val q = AbstractionQuestion(s, v) AbstractionApplier.applyRules(q) { q1 => val res = VarTransformer(q1.s, q1.v, q1.s.g.values, q1.s.h).transformState(q1.s) Q(q1.s, res, q1.v) } } - def solveFraming(s: State, v: Verifier, pvef: Exp => PartialVerificationError, tra: VarTransformer, loc: Positioned, knownPosts: Seq[Exp])(Q: FramingSuccess => VerificationResult): VerificationResult = { + 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[Term](s, v) { (s, v, QS) => @@ -352,7 +375,7 @@ object BiAbductionSolver { 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 => + solveFraming(s1, v1, pvef, tra, loc, newPosts1, stateAllowed) { frame => val newFrame = frame.copy(posts = frame.posts ++ newPosts1) Q(newFrame) } @@ -360,18 +383,19 @@ object BiAbductionSolver { } { // We failed to fulfill the posts. Perform abduction, add the results and try again. f => - BiAbductionSolver.solveAbduction(s, v, f, Some(loc))((s3, res, v3) => { - solveFraming(s3, v3, pvef, tra, loc, knownPosts) { + 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) { + val newAbdRes = if (res.state.nonEmpty) { Success(Some(res.copy(stmts = Seq()))) } else { Success() - }*/ - val newAbdRes = Success(Some(res)) + } //val newFrame = frame.copy(stmts = frame.stmts ++ res.stmts) - newAbdRes && Q(frame) - } + Q(frame) + }*/ } ) } @@ -381,20 +405,31 @@ object BiAbductionSolver { val abdReses = abductionUtils.getAbductionSuccesses(nf) val newMatches = abdReses.flatMap(_.newFieldChunks).toMap val abdCases = abdReses.groupBy(res => (res.trigger, res.stmts, res.state)) + + // Try to join by bc terms val joinedCases = abdCases.flatMap { case (_, reses) => - val unjoined = reses.map(res => (Seq(res), res.pcs.branchConditions.distinct.filter(_ != True))) - val joined = abductionUtils.joinBcs(unjoined) - joined.map { - case (reses, pcs) => - reses.head -> pcs + val unjoined = reses.map(res => + + (Seq(res), res.pcs.branchConditions.distinct.filter(_ != True))) + val termJoined = abductionUtils.joinBcs(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 { + case (reses, bcTerms) => + reses -> reses.head.getBcExps(bcTerms).distinct.collect { case Some(bc) => bc } } + expUnjoined.groupBy(_._2).map { case (bcs, list) => list.head._1.head -> bcs } } + // 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 - }} + 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) }) } @@ -410,7 +445,7 @@ object BiAbductionSolver { 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))) + val cases = frames.map(f => (f.posts.diff(everyPosts), f.getBcExps(f.pcs.branchConditions.distinct.filter(_ != True), vars))).distinct // We can remove bcs that hold in every branch val everyTerms = cases.head._2.filter { t => cases.forall(_._2.contains(t)) } @@ -545,7 +580,7 @@ object abductionUtils { p.predicates.filter { pred => val absAcc = f.copy(rcv = pred.formalArgs.head.localVar)(f.pos, f.info, f.errT) - pred.body.get.contains(absAcc) + pred.body.isDefined && pred.body.get.contains(absAcc) } } @@ -616,4 +651,10 @@ object abductionUtils { } } + // We need to sort exps before producing them because we have to create fields before creating stuff on the fields + // The idea is that the length of something on the field will always be greater than the field itself. + def sortExps(exps: Seq[Exp]): Seq[Exp] = { + exps.sortBy(e => e.size) + } + } diff --git a/src/main/scala/biabduction/Invariant.scala b/src/main/scala/biabduction/Invariant.scala index f84a04890..8d72d02b4 100644 --- a/src/main/scala/biabduction/Invariant.scala +++ b/src/main/scala/biabduction/Invariant.scala @@ -1,11 +1,10 @@ package viper.silicon.biabduction import viper.silicon.interfaces._ -import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.rules.producer.produces import viper.silicon.rules.{evaluator, executionFlowController, executor, producer} import viper.silicon.state.terms.Term -import viper.silicon.state.{BasicChunk, ChunkIdentifier, Heap, State} +import viper.silicon.state.{Heap, State} import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.ast._ @@ -29,41 +28,31 @@ object LoopInvariantSolver { // In particular, we need to ensure that permissions are not doubled between the two. Whenever the two invariants describe the same // point in time, we should make sure that there is no duplication going on, possible using abduction. // Also we need to guarantee well-definedness of the invariants - private def getPreInvariant(pres: Seq[Exp], posts: Seq[Exp], con: Exp, s: State, v: Verifier)(Q: Seq[Exp] => VerificationResult): VerificationResult = { + private def getInvariants(pres: Seq[Exp], posts: Seq[Exp], loopCon: Exp, existingInvs: Seq[Exp], s: State, v: Verifier)(Q: Seq[Exp] => VerificationResult): VerificationResult = { //TODO nklose probably we want to keep things that apply to non-reassigned variables just as part of the invariant. - val inverted = pres.collect { case m: MagicWand => m.left } + val invs = pres.collect { case m: MagicWand => m.left } ++ posts // If the loop condition requires permissions which are folded away in the invariant, we need to partially unfold it. executionFlowController.locallyWithResult[Seq[Exp]](s.copy(h = Heap()), v) { (s1, v1, Q1) => - producer.produces(s1, freshSnap, inverted, pveLam, v1) { (s2, v2) => + producer.produces(s1, freshSnap, invs ++ existingInvs, pveLam, v1) { (s2, v2) => executionFlowController.tryOrElse0(s2, v2) { (s3, v3, T) => - evaluator.eval(s3, con, pve, v3)((s4, _, _, v4) => T(s4, v4)) + evaluator.eval(s3, loopCon, pve, v3)((s4, _, _, v4) => T(s4, v4)) } { - (_, _) => Q1(inverted) + (_, _) => Q1(invs) } { f => - val abdRes = BiAbductionSolver.solveAbduction(s2, v2, f, Some(con)) { (_, res, _) => - Success(Some(res)) - } - abdRes match { + BiAbductionSolver.solveAbductionForError(s2, v2, f, stateAllowed = false, Some(loopCon)) { (_, _) => + Success() + } match { case f: Failure => f case abdRes: NonFatalResult => // TODO nklose we do not guarantee length 1 here anymore abductionUtils.getAbductionSuccesses(abdRes) match { 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 - val unfolded = inverted.map { - case inv: PredicateAccessPredicate => unfolds.getOrElse(inv.toString, inv) - case inv => inv + Q1(unfolded) } - Q1(unfolded) - */ } } } @@ -79,10 +68,18 @@ object LoopInvariantSolver { joinPoint: Option[SilverBlock], initialBcs: Seq[Term], q: InvariantAbductionQuestion = InvariantAbductionQuestion(Heap(), Seq(), Seq()), - loopConBcs: Seq[Term] = Seq(), + //loopConBcs: Seq[Term] = Seq(), iteration: Int = 1): VerificationResult = { + + // TODO if the loop condition (and maybe also the loop invs) contain permissions which require statements from the starting state, then this will fail. + // I need thought out way to eval / assume / check all of these things each iteration. + println("\nIteration: " + iteration) + + // We assume there is only one loop internal edge + val loopConExp = loopEdges.head.asInstanceOf[ConditionalEdge[Stmt, Exp]].condition + // 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) => @@ -90,34 +87,34 @@ 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) { (_, _) => Success()} + executor.follows(sFP, loopEdges, pveLam, vFP, joinPoint) { + (_, _) => Success() + //(s1, v1) => + // We evaluate the loop condition at the end of loop so that we can start the next iteration from a valid state + //evaluator.evalWithAbduction(s1, loopConExp, pve, v1){(_, _, _, _) => 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).reverse - // TODO nklose do we want to join branches here like we do for preconditions? + // TODO nklose do we want to join branches properly 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(), newMatches).get } + val newStateOpt = abdReses.flatMap { case abd => abd.getPreconditions(preStateVars, sPreInv.h, Seq(), newMatches).get }.distinct // We still need to remove the current loop condition - val newState = newStateOpt.map(_.transform { + val newState = abductionUtils.sortExps(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) => + producer.produces(sPreInv, freshSnap, newState, pveLam, vPreInv) { (sPreAbd, vPreAbd) => abductionUtils.findChunks(newState.collect { case loc: FieldAccessPredicate => loc.loc @@ -141,29 +138,30 @@ object LoopInvariantSolver { val postStateVars = sPostAbs.g.values.filter { case (v, _) => origVars.contains(v) } val postTran = VarTransformer(sPostAbs, vPostAbs, postStateVars, sPostAbs.h) - val postAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get) + val newpostAbstraction = postAbstraction0.map(e => postTran.transformExp(e, strict = false).get) + + println("New post abstraction:\n " + newpostAbstraction.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.toSet == q.preAbstraction.toSet && postAbstraction.toSet == q.postAbstraction.toSet) { - getPreInvariant(newPreAbstraction, postAbstraction, loopConExp, sPostAbs, vPostAbs) { preInv => + if (newPreAbstraction.toSet == q.preAbstraction.toSet && newpostAbstraction.toSet == q.postAbstraction.toSet) { - val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method]) - Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = preInv ++ postAbstraction, loop, vPostAbs.decider.pcs.duplicate()))) + val loop = abductionUtils.getWhile(loopConExp, s.currentMember.get.asInstanceOf[Method]) + val existingInvs = loop.invs + getInvariants(newPreAbstraction, newpostAbstraction, loopConExp, existingInvs, sPostAbs, vPostAbs) { res => + println("Invariants:\n " + res.mkString("\n ")) + Success(Some(LoopInvariantSuccess(sPostAbs, vPostAbs, invs = res, loop, vPostAbs.decider.pcs.duplicate()))) } } else { - val newLoopCons = loopConBcs :+ loopCondTerm + //val newLoopCons = loopConBcs :+ loopCondTerm // Else continue with next iteration, using the state from the end of the loop solveLoopInvariants(sPostAbs, vPostAbs, origVars, loopHead, loopEdges, joinPoint, initialBcs, q.copy(preHeap = newPreState.h, preAbstraction = newPreAbstraction, - postAbstraction = postAbstraction), newLoopCons, iteration = iteration + 1) + postAbstraction = newpostAbstraction), iteration = iteration + 1) } } - } - ) + }) } } - } + //} } } } diff --git a/src/main/scala/biabduction/VarTransformer.scala b/src/main/scala/biabduction/VarTransformer.scala index 47faf70d5..48ad7a329 100644 --- a/src/main/scala/biabduction/VarTransformer.scala +++ b/src/main/scala/biabduction/VarTransformer.scala @@ -5,22 +5,22 @@ import viper.silicon.resources.{FieldID, PredicateID} import viper.silicon.rules.chunkSupporter.findChunk import viper.silicon.state.terms.{BuiltinEquals, Term, Var} import viper.silicon.state._ +import viper.silicon.utils.ast.BigAnd import viper.silicon.verifier.Verifier import viper.silver.ast -import viper.silver.ast._ import scala.annotation.tailrec -case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap, newFieldChunks: Map[BasicChunk, LocationAccess] = Map()) { +case class VarTransformer(s: State, v: Verifier, targetVars: Map[ast.AbstractLocalVar, (Term, Option[ast.Exp])], targetHeap: Heap, newFieldChunks: Map[BasicChunk, ast.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 matches: Map[Term, ast.Exp] = resolveMatches() - val newChunkBySnap = newFieldChunks.map { case (c, fa: FieldAccess) => c.snap -> (c, fa) } + val newChunkBySnap = newFieldChunks.map { case (c, fa: ast.FieldAccess) => c.snap -> (c, fa) } - private def resolveMatches(): Map[Term, Exp] = { + private def resolveMatches(): Map[Term, ast.Exp] = { 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) }.flatten @@ -43,63 +43,92 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa } @tailrec - private def resolveChunks(currentMatches: Map[Term, Exp], remainingChunks: Seq[BasicChunk], remainingTerms: Seq[Term]): Map[Term, Exp] = { + private def resolveChunks(currentMatches: Map[Term, ast.Exp], remainingChunks: Seq[BasicChunk], remainingTerms: Seq[Term]): Map[Term, ast.Exp] = { remainingChunks.collectFirst { case c if currentMatches.contains(c.args.head) => c } match { case None => currentMatches case Some(c) => - val newExp = FieldAccess(currentMatches(c.args.head), abductionUtils.getField(c.id, s.program))() + val newExp = ast.FieldAccess(currentMatches(c.args.head), abductionUtils.getField(c.id, s.program))() val newMatches = currentMatches ++ remainingTerms.collect { case t if t.sort == c.snap.sort && v.decider.check(BuiltinEquals(t, c.snap), Verifier.config.checkTimeout()) => t -> newExp } resolveChunks(newMatches, remainingChunks.filter(_ != c), remainingTerms.filter(!newMatches.contains(_))) } } - def transformTerm(t: Term): Option[Exp] = { + def transformTerm(t: Term): Option[ast.Exp] = { t match { case t if matches.contains(t) => matches.get(t) case BuiltinEquals(t1, t2) => (transformTerm(t1), transformTerm(t2)) match { case (Some(e1), Some(e2)) => - Some(EqCmp(e1, e2)()) + Some(ast.EqCmp(e1, e2)()) case _ => None } - case terms.FractionPermLiteral(r) => Some(FractionalPerm(IntLit(r.numerator)(), IntLit(r.denominator)())()) - case terms.FullPerm => Some(FullPerm()()) - case terms.Null => Some(NullLit()()) + case terms.FractionPermLiteral(r) => Some(ast.FractionalPerm(ast.IntLit(r.numerator)(), ast.IntLit(r.denominator)())()) + case terms.FullPerm => Some(ast.FullPerm()()) + 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 { - case (Some(e1), Some(e2)) => - Some(NeCmp(e1, e2)()) + case (Some(e1), Some(e2)) => Some(ast.NeCmp(e1, e2)()) case _ => None } - case terms.True => Some(TrueLit()()) + case terms.True => Some(ast.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)()) + Some(ast.FieldAccess(rcv.get, c._2.field)()) + case and: terms.And => + val subs = and.ts.map(transformTerm) + if (subs.contains(None)) None else Some(BigAnd(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 } } - def transformState(s: State): Seq[Exp] = { + def transformState(s: State): Seq[ast.Exp] = { val transformed = s.h.values.collect { case c: NonQuantifiedChunk => transformChunk(c) }.collect { case Some(e) => e }.toSeq transformed.filter { - case _: FieldAccessPredicate => true + case _: ast.FieldAccessPredicate => true case _ => false } ++ transformed.filter { - case _: FieldAccessPredicate => false + case _: ast.FieldAccessPredicate => false case _ => true } } - def transformChunk(b: NonQuantifiedChunk): Option[Exp] = { + def transformChunk(b: NonQuantifiedChunk): Option[ast.Exp] = { b match { case bc: BasicChunk => val rcv = transformTerm(bc.args.head) (bc, rcv) match { case (_, None) => None - case (BasicChunk(FieldID, _, _, _, _, _, _), rcv) => Some(FieldAccessPredicate(FieldAccess(rcv.get, abductionUtils.getField(bc.id, s.program))(), transformTerm(b.perm).get)()) - case (BasicChunk(PredicateID, id, _, _, _, _, _), rcv) => Some(PredicateAccessPredicate(PredicateAccess(Seq(rcv.get), id.name)(), transformTerm(b.perm).get)()) + case (BasicChunk(FieldID, _, _, _, _, _, _), rcv) => Some(ast.FieldAccessPredicate(ast.FieldAccess(rcv.get, abductionUtils.getField(bc.id, s.program))(), transformTerm(b.perm).get)()) + case (BasicChunk(PredicateID, id, _, _, _, _, _), rcv) => Some(ast.PredicateAccessPredicate(ast.PredicateAccess(Seq(rcv.get), id.name)(), transformTerm(b.perm).get)()) } case mwc: MagicWandChunk => @@ -114,10 +143,10 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa } } - private def safeEval(e: Exp): Option[Term] = { + private def safeEval(e: ast.Exp): Option[Term] = { e match { - case lv: LocalVar => Some(s.g(lv)) - case fa@FieldAccess(target, _) => + case lv: ast.LocalVar => Some(s.g(lv)) + case fa@ast.FieldAccess(target, _) => safeEval(target) match { case None => None case Some(arg) => @@ -132,14 +161,15 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa } } - def transformExp(e: Exp, strict: Boolean = true): Option[Exp] = { + def transformExp(e: ast.Exp, strict: Boolean = true): Option[ast.Exp] = { try { val res = e.transform { - case FieldAccessPredicate(fa, perm) => + 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 - FieldAccessPredicate(FieldAccess(newRcv, fa.field)(), perm)() - case fa@FieldAccess(target, field) => + 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 @@ -148,11 +178,11 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa case Some(term) => val existingChunkTerm = transformTerm(term) existingChunkTerm match { - case Some(nfa: FieldAccess) => nfa + case Some(nfa: ast.FieldAccess) => nfa - case Some(NullLit()) | Some(LocalVar(_, _)) | None => + case Some(ast.NullLit()) | Some(ast.LocalVar(_, _)) | None => val rvcExp = transformExp(target) - FieldAccess(rvcExp.get, field)() + ast.FieldAccess(rvcExp.get, field)() // TODO nklose this wrong sometimes? // Specifically I think if we are transforming "in-place" then this is fine, @@ -163,9 +193,9 @@ case class VarTransformer(s: State, v: Verifier, targetVars: Map[AbstractLocalVa // Else we want to recurse and try to match the target case None => val rvcExp = transformExp(target) - FieldAccess(rvcExp.get, field)() + ast.FieldAccess(rvcExp.get, field)() } - case lv: LocalVar => { + case lv: ast.LocalVar => { val term: Term = s.g.values.getOrElse(lv, targetVars(lv))._1 transformTerm(term).get } diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index cc74198a9..a44b2d196 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -7,7 +7,7 @@ package viper.silicon.rules import viper.silicon.Config.JoinMode -import viper.silicon.biabduction.AbductionQuestion +import viper.silicon.biabduction.{AbductionQuestion, BiAbductionSolver} import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.debugger.DebugExp import viper.silicon.interfaces._ @@ -86,6 +86,22 @@ object evaluator extends EvaluationRules { evals2(s1, es.tail, t :: ts, pvef, v1)((s2, ts2, es2, v2) => Q(s2, ts2, eNew.map(eN => eN :: es2.get), v2))) } + /* + def evalWithAbduction(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier) + (Q: (State, Term, Option[ast.Exp], Verifier) => VerificationResult) + : VerificationResult = { + executionFlowController.tryOrElse2[Term, Option[ast.Exp]](s, v) { (s1, v1, T) => + evaluator.eval(s1, e, pve, v1)(T) + } { + Q + } { + f => + BiAbductionSolver.solveAbductionForError(s, v, f, stateAllowed = true, Some(e)) { (s2, v2) => + evalWithAbduction(s2, e, pve, v2)(Q) + } + } + }*/ + /** Wrapper Method for eval, for logging. See Executor.scala for explanation of analogue. * */ @inline def eval(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 95d6340e1..634777d42 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, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) + def exec(s: State, stmt: ast.Stmt, v: Verifier, abdLoc: Option[Positioned] = None, abdStateAllowed: Boolean = true) (Q: (State, Verifier) => VerificationResult) : VerificationResult - def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) + def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier, abdLoc: Option[Positioned] = None) (Q: (State, Verifier) => VerificationResult) : VerificationResult } @@ -85,8 +85,8 @@ object executor extends ExecutionRules { Success() })} { f => - BiAbductionSolver.solveAbduction(s1, v, f, Some(ce.condition))((s5, res, v5) => { - Success(Some(res)) && follow(s5, edge, v5, joinPoint)(Q) + BiAbductionSolver.solveAbductionForError(s1, v, f, stateAllowed = true, Some(ce.condition))((s5, v5) => { + follow(s5, edge, v5, joinPoint)(Q) } ) } @@ -223,7 +223,7 @@ object executor extends ExecutionRules { block match { case cfg.StatementBlock(stmt) => - execs(s, stmt, v, doAbduction = true)((s1, v1) => + execs(s, stmt, v)((s1, v1) => follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint)(Q)) case _: cfg.PreconditionBlock[ast.Stmt, ast.Exp] @@ -271,13 +271,13 @@ object executor extends ExecutionRules { })) val sBody = s.copy(g = gBody, h = Heap()) - 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 + val invReses = if(s.doAbduction) {executionFlowController.locally(s, v)((sInv, vInv) => + // We have to consume the existing invariants once, because we produce them 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) => + executor.exec(sInv, ast.Exhale(BigAnd(existingInvs))(), vInv) { (sInv1, vInv1) => LoopInvariantSolver.solveLoopInvariants(sInv1, vInv1, sInv1.g.values.keys.toSeq, block, otherEdges, joinPoint, vInv1.decider.pcs.branchConditions) } - ) + )} else Success() invReses match { @@ -286,7 +286,8 @@ object executor extends ExecutionRules { case nfr: NonFatalResult => { 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(invSuc) if s.doAbduction => (invSuc.invs.distinct, Success(Some(LoopInvariantSuccess(s, v, invSuc.invs.distinct, invSuc.loop, v.decider.pcs.duplicate())))) + case Seq() if !s.doAbduction => (Seq(), Success()) } val invs = foundInvs ++ existingInvs @@ -306,7 +307,7 @@ object executor extends ExecutionRules { val con = executionFlowController.locally(s, v) ((s0, v0) => { v0.decider.prover.comment("Loop head block: Establish invariant") - checkInvariants(s0, v0, invs, condition)((sLeftover, v1) => { + checkInvariants(s0, v0, invs, condition, stateAllowed = true)((sLeftover, v1) => { v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)") phase1data.foldLeft(Success(): VerificationResult) { case (result, _) if !result.continueVerification => result @@ -319,7 +320,7 @@ object executor extends ExecutionRules { if (v2.decider.checkSmoke()) Success() else { - execs(s3, stmts, v2, doAbduction=true)((s4, v3) => { + execs(s3, stmts, v2)((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,7 +336,7 @@ object executor extends ExecutionRules { follows(s5, otherEdges, WhileFailed, v5, joinPoint)((s6, v6) => { // We have to check the inferred invariants after loop manually here instead of // relying on the reentry of the loop head, as this will not have the found invariants - checkInvariants(s6, v6, foundInvs, endStmt)((_, _) => Success()) + checkInvariants(s6, v6, foundInvs, endStmt, stateAllowed = false)((_, _) => Success()) } ) }) @@ -359,12 +360,13 @@ object executor extends ExecutionRules { * attempting to re-establish the invariant. */ v.decider.prover.comment("Loop head block: Re-establish invariant") - checkInvariants(s, v, existingInvs, endStmt)(Q) + // TODO If we reach this from the invariant generation, then state is OK. If from the final loop checking, it is not! + checkInvariants(s, v, existingInvs, endStmt, stateAllowed = true)(Q) } } } - private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], location: Positioned)(Q: (State, Verifier) => VerificationResult): VerificationResult = { + private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], location: Positioned, stateAllowed: Boolean)(Q: (State, Verifier) => VerificationResult): VerificationResult = { if (invs.isEmpty) { Q(s, v) } else { @@ -376,24 +378,23 @@ object executor extends ExecutionRules { 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 - BiAbductionSolver.solveAbduction(s, v, f, Some(location))((s3, res, v3) => - Success(Some(res)) && checkInvariants(s3, v3, invs, location)(Q)) + BiAbductionSolver.solveAbductionForError(s, v, f, stateAllowed, Some(location))((s3, v3) => + checkInvariants(s3, v3, invs, location, stateAllowed)(Q)) } } } - def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) + def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier, abdLoc: Option[Positioned] = None) (Q: (State, Verifier) => VerificationResult) : VerificationResult = if (stmts.nonEmpty) - exec(s, stmts.head, v, doAbduction)((s1, v1) => - execs(s1, stmts.tail, v1, doAbduction)(Q)) + exec(s, stmts.head, v)((s1, v1) => + execs(s1, stmts.tail, v1)(Q)) else Q(s, v) - def exec(s: State, stmt: ast.Stmt, v: Verifier, doAbduction: Boolean = true, abdLoc: Option[Positioned] = None) + def exec(s: State, stmt: ast.Stmt, v: Verifier, abdLoc: Option[Positioned] = None, abdStateAllowed: Boolean = true) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { val sepIdentifier = v.symbExLog.openScope(new ExecuteRecord(stmt, s, v.decider.pcs)) @@ -404,16 +405,12 @@ object executor extends ExecutionRules { Q(s2, v2) } { f => - 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 + val loc = if (abdLoc.isDefined) abdLoc else Some(stmt) + BiAbductionSolver.solveAbductionForError(s, v, f, stateAllowed = abdStateAllowed, loc)((s3, v3) => { + v3.symbExLog.closeScope(sepIdentifier) + exec(s3, stmt, v3)(Q) } + ) } } diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index d0379d08d..86840d6b0 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -34,6 +34,7 @@ final case class State(g: Store = Store(), oldHeaps: OldHeaps = Map.empty, parallelizeBranches: Boolean = false, + doAbduction: Boolean = false, recordVisited: Boolean = false, visited: List[ast.Predicate] = Nil, /* TODO: Use a multiset instead of a list */ @@ -159,6 +160,7 @@ object State { functionData, oldHeaps1, parallelizeBranches1, + doAbduction1, recordVisited1, visited1, methodCfg1, invariantContexts1, constrainableARPs1, @@ -184,6 +186,7 @@ object State { `predicateData`, `functionData`, `oldHeaps1`, `parallelizeBranches1`, + `doAbduction1`, `recordVisited1`, `visited1`, `methodCfg1`, `invariantContexts1`, constrainableARPs2, @@ -309,6 +312,7 @@ object State { predicateData, functionData, oldHeaps1, parallelizeBranches1, + doAbduction1, recordVisited1, visited1, methodCfg1, invariantContexts1, constrainableARPs1, @@ -333,6 +337,7 @@ object State { `predicateData`, `functionData`, oldHeaps2, `parallelizeBranches1`, + `doAbduction1`, `recordVisited1`, `visited1`, `methodCfg1`, invariantContexts2, constrainableARPs2, diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 2de7f8abf..9cd07661f 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -12,6 +12,7 @@ import viper.silicon.biabduction.{VarTransformer, abductionUtils} import viper.silicon.decider.Decider import viper.silicon.interfaces._ import viper.silicon.logger.records.data.WellformednessCheckRecord +import viper.silicon.rules.consumer.consumes import viper.silicon.rules.{executionFlowController, executor, producer} import viper.silicon.state.State.OldHeaps import viper.silicon.state.{Heap, State, Store} @@ -49,6 +50,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { def units = _units def verify(sInit: State, method: ast.Method): Seq[VerificationResult] = { + logger.debug("\n\n" + "-" * 10 + " METHOD " + method.name + "-" * 10 + "\n") decider.prover.comment("%s %s %s".format("-" * 10, method.name, "-" * 10)) @@ -108,23 +110,30 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) val s2a = s2.copy(oldHeaps = s2.oldHeaps + (Verifier.PRE_STATE_LABEL -> s2.h)) - val wfc = executionFlowController.locally(s2a, v2)((s3, v3) => { - val s4 = s3.copy(h = Heap()) - val impLog = new WellformednessCheckRecord(posts, s, v.decider.pcs) - val sepIdentifier = symbExLog.openScope(impLog) - produces(s4, freshSnap, posts, ContractNotWellformed, v3)((_, _) => { - symbExLog.closeScope(sepIdentifier) - Success() + val wfc = if (sInit.doAbduction) Success() else { + executionFlowController.locally(s2a, v2)((s3, v3) => { + val s4 = s3.copy(h = Heap()) + val impLog = new WellformednessCheckRecord(posts, s, v.decider.pcs) + val sepIdentifier = symbExLog.openScope(impLog) + produces(s4, freshSnap, posts, ContractNotWellformed, v3)((_, _) => { + symbExLog.closeScope(sepIdentifier) + Success() + }) }) - }) + } val ex = executionFlowController.locally(s2a, v2)((s3, v3) => { exec(s3, body, v3) { (s4, v4) => { - 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) } - val tra = VarTransformer(s4, v4, vars, s4.h) - solveFraming(s4, v4, postViolated, tra, abductionUtils.dummyEndStmt, posts) { - frame => Success(Some(frame.copy(s = s4, v = 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) } + val tra = VarTransformer(s4, v4, vars, s4.h) + solveFraming(s4, v4, postViolated, tra, abductionUtils.dummyEndStmt, posts, stateAllowed = true) { + frame => Success(Some(frame.copy(s = s4, v = v4)) + ) + } + } else { + consumes(s4, posts, postViolated, v4)((_, _, _) => + Success()) } } } @@ -133,27 +142,33 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { }) }) - val abdResult: VerificationResult = 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 => Failure(Internal(reason = InternalReason(DummyNode, "Resolving Biabduction results failed"))) - case Some(m) => - println("Original method: \n" + method.toString + "\nAbduced method: \n" + m.toString) - result - } - case _ => result + val finalRes = if(sInit.doAbduction) { + 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) => + println("Original method: \n" + method.toString + "\nAbduced method: \n" + m.toString) + val sNoAbd = sInit.copy(doAbduction = false) + verify(sNoAbd, m) + } + case _ => Seq(result) + } + } else { + Seq(result) } v.decider.resetProverOptions() symbExLog.closeMemberScope() - Seq(abdResult) + finalRes } /* Lifetime */ diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 2764f5b2e..3d6d8eef2 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -396,6 +396,7 @@ class DefaultMainVerifier(config: Config, State(program = program, functionData = functionData, predicateData = predicateData, + doAbduction = true, qpFields = quantifiedFields, qpPredicates = quantifiedPredicates, qpMagicWands = quantifiedMagicWands, diff --git a/src/test/resources/biabduction/dafny/checksum/checksum1.vpr b/src/test/resources/biabduction/dafny/16-0/checksum1.vpr similarity index 100% rename from src/test/resources/biabduction/dafny/checksum/checksum1.vpr rename to src/test/resources/biabduction/dafny/16-0/checksum1.vpr diff --git a/src/test/resources/biabduction/dafny/checksum/checksum2.vpr b/src/test/resources/biabduction/dafny/16-0/checksum2.vpr similarity index 89% rename from src/test/resources/biabduction/dafny/checksum/checksum2.vpr rename to src/test/resources/biabduction/dafny/16-0/checksum2.vpr index 5abf5a209..cc30d7a8d 100644 --- a/src/test/resources/biabduction/dafny/checksum/checksum2.vpr +++ b/src/test/resources/biabduction/dafny/16-0/checksum2.vpr @@ -7,7 +7,7 @@ predicate ChecksumMachine(this: Ref) } method Append(this: Ref, d: Int) - //requires ChecksumMachine(this) + requires ChecksumMachine(this) requires 0 <= d //ensures ChecksumMachine(this) { diff --git a/src/test/resources/biabduction/dafny/16-0/checksum3.vpr b/src/test/resources/biabduction/dafny/16-0/checksum3.vpr new file mode 100644 index 000000000..3714a2b92 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-0/checksum3.vpr @@ -0,0 +1,27 @@ +//import "examples-16.0.vpr" + +field checksumData: Int + +adt Option[T] { + Some(value: T) + None() +} + +field ocs: Option[Int] + +predicate ChecksumMachineOCS(this: Ref) +{ + acc(this.checksumData) && 0 <= this.checksumData && + acc(this.ocs) +} + +method ChecksumMachineOCSConstructor() returns (this: Ref) + //ensures ChecksumMachineOCS(this) + //ensures unfolding ChecksumMachineOCS(this) in this.checksumData == 0 + //ensures unfolding ChecksumMachineOCS(this) in this.ocs.isNone +{ + this := new(checksumData, ocs) + this.checksumData := 0 + this.ocs := None() + //fold ChecksumMachineOCS(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-0/checksum4.vpr b/src/test/resources/biabduction/dafny/16-0/checksum4.vpr new file mode 100644 index 000000000..a08048840 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-0/checksum4.vpr @@ -0,0 +1,31 @@ +//import "examples-16.0.vpr" + +field checksumData: Int + +adt Option[T] { + Some(value: T) + None() +} + +field ocs: Option[Int] + +predicate ChecksumMachineOCS(this: Ref) +{ + acc(this.checksumData) && 0 <= this.checksumData && + acc(this.ocs) +} + + + +method AppendOCS(this: Ref, d: Int) + requires ChecksumMachineOCS(this) + requires 0 <= d + //ensures ChecksumMachineOCS(this) + //ensures unfolding ChecksumMachineOCS(this) in this.checksumData == old(unfolding ChecksumMachineOCS(this) in this.checksumData) + d + //ensures unfolding ChecksumMachineOCS(this) in this.ocs.isNone +{ + //unfold ChecksumMachineOCS(this) + this.checksumData := this.checksumData + d + this.ocs := None() + //fold ChecksumMachineOCS(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-0/checksum5.vpr b/src/test/resources/biabduction/dafny/16-0/checksum5.vpr new file mode 100644 index 000000000..0eec63e23 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-0/checksum5.vpr @@ -0,0 +1,33 @@ +//import "examples-16.0.vpr" + +field checksumData: Int + +adt Option[T] { + Some(value: T) + None() +} + +field ocs: Option[Int] + +predicate ChecksumMachineOCS(this: Ref) +{ + acc(this.checksumData) && 0 <= this.checksumData && + acc(this.ocs) +} + +method ChecksumOCS(this: Ref) returns (checksum: Int) + requires ChecksumMachineOCS(this) + //requires unfolding ChecksumMachineOCS(this) in this.ocs.isNone || this.ocs.value == Hash(this.checksumData) + //ensures ChecksumMachineOCS(this) + //ensures unfolding ChecksumMachineOCS(this) in this.checksumData == old(unfolding ChecksumMachineOCS(this) in this.checksumData) + //ensures unfolding ChecksumMachineOCS(this) in checksum == Hash(this.checksumData) + //ensures unfolding ChecksumMachineOCS(this) in this.ocs == Some(checksum) +{ + //unfold ChecksumMachineOCS(this) + if (this.ocs.isNone) + { + this.ocs := Some(this.checksumData % 137) + } + checksum := this.ocs.value + //fold ChecksumMachineOCS(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-0/ledger1.vpr b/src/test/resources/biabduction/dafny/16-0/ledger1.vpr new file mode 100644 index 000000000..68d942668 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-0/ledger1.vpr @@ -0,0 +1,25 @@ +function Sum(s: Seq[Int]): Int +{ + (|s| == 0) ? 0 : s[0] + Sum(s[1..]) +} + +field LedgerTransactions: Seq[Int] +field LedgerBalance: Int + +predicate Ledger(this: Ref) +{ + acc(this.LedgerTransactions) && + acc(this.LedgerBalance) && 0 <= this.LedgerBalance && + this.LedgerBalance == Sum(this.LedgerTransactions) +} + +method LedgerConstructor() returns (this: Ref) + //ensures Ledger(this) + //ensures unfolding Ledger(this) in this.LedgerTransactions == Seq() + //ensures unfolding Ledger(this) in this.LedgerBalance == 0 +{ + this := new(LedgerTransactions, LedgerBalance) + this.LedgerTransactions := Seq() + this.LedgerBalance := 0 + //fold Ledger(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-0/ledger2.vpr b/src/test/resources/biabduction/dafny/16-0/ledger2.vpr new file mode 100644 index 000000000..bfd8fe338 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-0/ledger2.vpr @@ -0,0 +1,27 @@ +function Sum(s: Seq[Int]): Int +{ + (|s| == 0) ? 0 : s[0] + Sum(s[1..]) +} + +field LedgerTransactions: Seq[Int] +field LedgerBalance: Int + +predicate Ledger(this: Ref) +{ + acc(this.LedgerTransactions) && + acc(this.LedgerBalance) && 0 <= this.LedgerBalance && + this.LedgerBalance == Sum(this.LedgerTransactions) +} + +method LedgerDeposit(this: Ref, n: Int) + requires Ledger(this) + requires 0 <= n + //ensures Ledger(this) + //ensures unfolding Ledger(this) in this.LedgerTransactions == Seq(n) ++ old(unfolding Ledger(this) in this.LedgerTransactions) + //ensures unfolding Ledger(this) in this.LedgerBalance == n + old(unfolding Ledger(this) in this.LedgerBalance) +{ + //unfold Ledger(this) + this.LedgerTransactions := Seq(n) ++ this.LedgerTransactions + this.LedgerBalance := this.LedgerBalance + n + //fold Ledger(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-0/ledger3.vpr b/src/test/resources/biabduction/dafny/16-0/ledger3.vpr new file mode 100644 index 000000000..a337d0da9 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-0/ledger3.vpr @@ -0,0 +1,28 @@ +function Sum(s: Seq[Int]): Int +{ + (|s| == 0) ? 0 : s[0] + Sum(s[1..]) +} + +field LedgerTransactions: Seq[Int] +field LedgerBalance: Int + +predicate Ledger(this: Ref) +{ + acc(this.LedgerTransactions) && + acc(this.LedgerBalance) && 0 <= this.LedgerBalance && + this.LedgerBalance == Sum(this.LedgerTransactions) +} + +method LedgerWithdraw(this: Ref, n: Int) + requires Ledger(this) + requires 0 <= n + requires unfolding Ledger(this) in n <= this.LedgerBalance + //ensures Ledger(this) + //ensures unfolding Ledger(this) in this.LedgerTransactions == Seq(-n) ++ old(unfolding Ledger(this) in this.LedgerTransactions) + //ensures unfolding Ledger(this) in this.LedgerBalance == old(unfolding Ledger(this) in this.LedgerBalance) - n +{ + //unfold Ledger(this) + this.LedgerTransactions := Seq(-n) ++ this.LedgerTransactions + this.LedgerBalance := this.LedgerBalance - n + //fold Ledger(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-1/tokenizer.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer.vpr new file mode 100644 index 000000000..ad0217ce7 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-1/tokenizer.vpr @@ -0,0 +1,49 @@ +adt Category { + Identifier() + Number() + Operator() + Whitespace() + Error() + End() +} + +function Is(ch: Int, cat: Category): Bool + requires !cat.isEnd + requires 0 <= ch <= 127 +{ + (cat.isWhitespace) ? ch == 32 || ch == 9 || ch == 13 || ch == 10 : // " \t\r\n" + (cat.isIdentifier) ? 65 <= ch <= 90 || 97 <= ch <= 122 : // 'A' <= ch <= 'Z' || 'a' <= ch <= 'z' + (cat.isNumber) ? 48 <= ch <= 57 : // '0' <= ch <= '9' + (cat.isOperator) ? ch == 43 || ch == 45 || ch == 42 || ch == 47 || ch == 37 || ch == 33 || + ch == 61 || ch == 62 || ch == 60 || ch == 126 || ch == 94 || ch == 38 || + ch == 124 : // "+-*/%!=><=~^&|" + !Is(ch, Identifier()) && !Is(ch, Number()) && !Is(ch, Operator()) && + !Is(ch, Whitespace()) // error case +} + +field source: Seq[Int] +field n: Int + +predicate Tokenizer(this: Ref) +{ + acc(this.source) && + acc(this.n) && 0 <= this.n <= |this.source| && + forall i: Int :: 0 <= i < |this.source| ==> 0 <= this.source[i] <= 127 +} + + +function getSource(this: Ref): Seq[Int] + requires Tokenizer(this) + ensures forall i: Int :: 0 <= i < |result| ==> 0 <= result[i] <= 127 +{ + unfolding Tokenizer(this) in + this.source +} + +function getN(this: Ref): Int + requires Tokenizer(this) + ensures 0 <= result <= |getSource(this)| +{ + unfolding Tokenizer(this) in + this.n +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/tokenizer/tokenizer1.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer1.vpr similarity index 100% rename from src/test/resources/biabduction/dafny/tokenizer/tokenizer1.vpr rename to src/test/resources/biabduction/dafny/16-1/tokenizer1.vpr diff --git a/src/test/resources/biabduction/dafny/tokenizer/tokenizer2.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer2.vpr similarity index 60% rename from src/test/resources/biabduction/dafny/tokenizer/tokenizer2.vpr rename to src/test/resources/biabduction/dafny/16-1/tokenizer2.vpr index 00c2bb2cd..26da8656e 100644 --- a/src/test/resources/biabduction/dafny/tokenizer/tokenizer2.vpr +++ b/src/test/resources/biabduction/dafny/16-1/tokenizer2.vpr @@ -1,52 +1,4 @@ -adt Category { - Identifier() - Number() - Operator() - Whitespace() - Error() - End() -} - -function Is(ch: Int, cat: Category): Bool - requires !cat.isEnd - requires 0 <= ch <= 127 -{ - (cat.isWhitespace) ? ch == 32 || ch == 9 || ch == 13 || ch == 10 : // " \t\r\n" - (cat.isIdentifier) ? 65 <= ch <= 90 || 97 <= ch <= 122 : // 'A' <= ch <= 'Z' || 'a' <= ch <= 'z' - (cat.isNumber) ? 48 <= ch <= 57 : // '0' <= ch <= '9' - (cat.isOperator) ? ch == 43 || ch == 45 || ch == 42 || ch == 47 || ch == 37 || ch == 33 || - ch == 61 || ch == 62 || ch == 60 || ch == 126 || ch == 94 || ch == 38 || - ch == 124 : // "+-*/%!=><=~^&|" - !Is(ch, Identifier()) && !Is(ch, Number()) && !Is(ch, Operator()) && - !Is(ch, Whitespace()) // error case -} - -field source: Seq[Int] -field n: Int - -predicate Tokenizer(this: Ref) -{ - acc(this.source) && - acc(this.n) && 0 <= this.n <= |this.source| && - forall i: Int :: 0 <= i < |this.source| ==> 0 <= this.source[i] <= 127 -} - - -function getSource(this: Ref): Seq[Int] - requires Tokenizer(this) - ensures forall i: Int :: 0 <= i < |result| ==> 0 <= result[i] <= 127 -{ - unfolding Tokenizer(this) in - this.source -} - -function getN(this: Ref): Int - requires Tokenizer(this) - ensures 0 <= result <= |getSource(this)| -{ - unfolding Tokenizer(this) in - this.n -} +import "tokenizer.vpr" method Read(this: Ref) returns (cat: Category, p: Int, token: Seq[Int]) //requires Tokenizer(this) @@ -57,8 +9,7 @@ method Read(this: Ref) returns (cat: Category, p: Int, token: Seq[Int]) //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 :: 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)] diff --git a/src/test/resources/biabduction/dafny/16-1/tokenizer3.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer3.vpr new file mode 100644 index 000000000..4ea9aaf96 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-1/tokenizer3.vpr @@ -0,0 +1,116 @@ +import "tokenizer.vpr" + +function IsStart(ch: Int, cat: Category): Bool + requires !cat.isEnd + requires 0 <= ch <= 127 +{ + Is(ch, Identifier()) +} + +function IsFollow(ch: Int, cat: Category): Bool + requires !cat.isEnd + requires 0 <= ch <= 127 +{ + Is(ch, Identifier()) || Is(ch, Number()) +} + +method ReadModifedIdentifier(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 token == getSource(this)[p..getN(this)] + // New + //ensures cat.isIdentifier ==> IsStart(token[0], cat) && forall i: Int :: 1 <= i < |token| ==> IsFollow(token[i], cat) +{ + // 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()) + { + //unfold Tokenizer(this) + this.n := this.n + 1 + //fold Tokenizer(this) + } + p := getN(this) + // determine syntactic category + var return: Bool := false + if (getN(this) == |getSource(this)|) + { + cat := End() + token := Seq() + return := true + } + elseif (Is(getSource(this)[getN(this)], Identifier())) + { + cat := Identifier() + } + elseif (Is(getSource(this)[getN(this)], Number())) + { + cat := Number() + } + elseif (Is(getSource(this)[getN(this)], Operator())) + { + cat := Operator() + } + else + { + cat := Error() + token := Seq() + return := true + } + // read token + if (!return) + { + var start: Int := getN(this) + if (cat.isIdentifier && !IsStart(getSource(this)[getN(this)], cat)) + { + return := true + } + else + { + //unfold Tokenizer(this) + this.n := this.n + 1 + //fold Tokenizer(this) + while (getN(this) != |getSource(this)| && Is(getSource(this)[getN(this)], cat) && !return) + //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) + { + if (cat.isIdentifier && !IsFollow(getSource(this)[getN(this)], cat)) + { + return := true + } + else + { + //unfold Tokenizer(this) + this.n := this.n + 1 + //fold Tokenizer(this) + } + } + } + if (return) + { + cat := Error() + token := Seq() + //unfold Tokenizer(this) + this.n := p + //fold Tokenizer(this) + } + else + { + token := getSource(this)[start..getN(this)] + } + } +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-1/tokenizer4.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer4.vpr new file mode 100644 index 000000000..d2d9b94db --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-1/tokenizer4.vpr @@ -0,0 +1,29 @@ +field suffix: Seq[Int] +field m: Int +field j: Int +field source: Seq[Int] +field n: Int + +predicate TokenizerWithPruning(this: Ref) +{ + acc(this.source) && acc(this.suffix) && acc(this.m) && acc(this.j) && + acc(this.n) && 0 <= this.n <= |this.source| && + this.suffix == this.source[this.m..] && this.m + this.j == this.n && + 0 <= this.m <= this.n && 0 <= this.j <= |this.suffix| && + forall i: Int :: 0 <= i < |this.source| ==> 0 <= this.source[i] <= 127 +} + +method TokenizerWithPruningConstructor(s: Seq[Int]) returns (this: Ref) + requires forall i: Int :: 0 <= i < |s| ==> 0 <= s[i] <= 127 + //ensures TokenizerWithPruning(this) + //ensures unfolding TokenizerWithPruning(this) in this.source == s && + // this.suffix == s && this.m == 0 && this.j == 0 && this.n == 0 +{ + this := new(source, suffix, m, j, n) + this.source := s + this.suffix := s + this.m := 0 + this.j := 0 + this.n := 0 + //fold TokenizerWithPruning(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-1/tokenizer5.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer5.vpr new file mode 100644 index 000000000..851f25083 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-1/tokenizer5.vpr @@ -0,0 +1,27 @@ +field suffix: Seq[Int] +field m: Int +field j: Int +field source: Seq[Int] +field n: Int + +predicate TokenizerWithPruning(this: Ref) +{ + acc(this.source) && acc(this.suffix) && acc(this.m) && acc(this.j) && + acc(this.n) && 0 <= this.n <= |this.source| && + this.suffix == this.source[this.m..] && this.m + this.j == this.n && + 0 <= this.m <= this.n && 0 <= this.j <= |this.suffix| && + forall i: Int :: 0 <= i < |this.source| ==> 0 <= this.source[i] <= 127 +} +method TokenizerWithPruningPrune(this: Ref) + //requires TokenizerWithPruning(this) + //ensures TokenizerWithPruning(this) + //ensures unfolding TokenizerWithPruning(this) in this.m == this.n && this.j == 0 + //ensures unfolding TokenizerWithPruning(this) in this.suffix == this.source[this.m..] +{ + //unfold TokenizerWithPruning(this) + this.m := this.n + this.j := 0 + this.suffix := this.source[this.m..] + //fold TokenizerWithPruning(this) + +} diff --git a/src/test/resources/biabduction/dafny/16-1/tokenizer6.vpr b/src/test/resources/biabduction/dafny/16-1/tokenizer6.vpr new file mode 100644 index 000000000..7d10a40a9 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-1/tokenizer6.vpr @@ -0,0 +1,102 @@ +field suffix: Seq[Int] +field m: Int +field j: Int +field source: Seq[Int] +field n: Int + +predicate TokenizerWithPruning(this: Ref) +{ + acc(this.source) && acc(this.suffix) && acc(this.m) && acc(this.j) && + acc(this.n) && 0 <= this.n <= |this.source| && + this.suffix == this.source[this.m..] && this.m + this.j == this.n && + 0 <= this.m <= this.n && 0 <= this.j <= |this.suffix| && + forall i: Int :: 0 <= i < |this.source| ==> 0 <= this.source[i] <= 127 +} + +method ReadWithPruning(this: Ref) returns (cat: Category, p: Int, token: Seq[Int]) + requires TokenizerWithPruning(this) + ensures 0 <= p + ensures TokenizerWithPruning(this) + ensures unfolding TokenizerWithPruning(this) in this.source == old(unfolding TokenizerWithPruning(this) in this.source) + ensures unfolding TokenizerWithPruning(this) in this.m == old(unfolding TokenizerWithPruning(this) in this.m) + ensures !cat.isWhitespace + ensures unfolding TokenizerWithPruning(this) in old(unfolding TokenizerWithPruning(this) in this.n) <= p <= this.n <= |this.source| + ensures unfolding TokenizerWithPruning(this) in cat.isEnd <==> p == |this.source| + ensures unfolding TokenizerWithPruning(this) in cat.isEnd || cat.isError <==> p == this.n + ensures unfolding TokenizerWithPruning(this) in forall i: Int :: old(unfolding TokenizerWithPruning(this) in this.n) <= i < p ==> + Is(this.source[i], Whitespace()) + ensures unfolding TokenizerWithPruning(this) in forall i: Int :: p <= i < this.n ==> Is(this.source[i], cat) + ensures unfolding TokenizerWithPruning(this) in p < this.n ==> this.n == |this.source| || !Is(this.source[this.n], cat) + ensures unfolding TokenizerWithPruning(this) in token == this.suffix[p-this.m..this.j] +{ + unfold TokenizerWithPruning(this) + assert 0 <= this.j <= |this.suffix| + fold TokenizerWithPruning(this) + // skip whitespace + while (unfolding TokenizerWithPruning(this) in this.j != |this.suffix| && Is(this.suffix[this.j], Whitespace())) + invariant TokenizerWithPruning(this) + invariant unfolding TokenizerWithPruning(this) in this.m == old(unfolding TokenizerWithPruning(this) in this.m) + invariant unfolding TokenizerWithPruning(this) in this.source == old(unfolding TokenizerWithPruning(this) in this.source) + invariant unfolding TokenizerWithPruning(this) in old(unfolding TokenizerWithPruning(this) in this.n) <= this.n <= |this.source| + invariant unfolding TokenizerWithPruning(this) in forall i: Int :: old(unfolding TokenizerWithPruning(this) in this.n) <= i < this.n ==> Is(this.source[i], Whitespace()) + { + unfold TokenizerWithPruning(this) + this.n := this.n + 1 + this.j := this.j + 1 + fold TokenizerWithPruning(this) + } + unfold TokenizerWithPruning(this) + p := this.n + fold TokenizerWithPruning(this) + // determine syntactic category + var return: Bool := false + if (unfolding TokenizerWithPruning(this) in this.n == |this.source|) + { + cat := End() + token := Seq() + return := true + } + elseif (unfolding TokenizerWithPruning(this) in Is(this.source[this.n], Identifier())) + { + cat := Identifier() + } + elseif (unfolding TokenizerWithPruning(this) in Is(this.source[this.n], Number())) + { + cat := Number() + } + elseif (unfolding TokenizerWithPruning(this) in Is(this.source[this.n], Operator())) + { + cat := Operator() + } + else + { + cat := Error() + token := Seq() + return := true + assert unfolding TokenizerWithPruning(this) in p - this.m == this.j + } + // read token + if (!return) + { + unfold TokenizerWithPruning(this) + var start: Int := this.j + this.n := this.n + 1 + this.j := this.j + 1 + fold TokenizerWithPruning(this) + while (unfolding TokenizerWithPruning(this) in this.n != |this.source| && Is(this.source[this.n], cat)) + invariant TokenizerWithPruning(this) + invariant unfolding TokenizerWithPruning(this) in this.m == old(unfolding TokenizerWithPruning(this) in this.m) + invariant unfolding TokenizerWithPruning(this) in this.source == old(unfolding TokenizerWithPruning(this) in this.source) + invariant unfolding TokenizerWithPruning(this) in p <= this.n <= |this.source| + invariant unfolding TokenizerWithPruning(this) in forall i: Int :: p <= i < this.n ==> Is(this.source[i], cat) + { + unfold TokenizerWithPruning(this) + this.n := this.n + 1 + this.j := this.j + 1 + fold TokenizerWithPruning(this) + } + unfold TokenizerWithPruning(this) + token := this.suffix[start..this.j] + fold TokenizerWithPruning(this) + } +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-2/coffee.vpr b/src/test/resources/biabduction/dafny/16-2/coffee.vpr new file mode 100644 index 000000000..73a0cc342 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-2/coffee.vpr @@ -0,0 +1,89 @@ +field hasBeans: Bool + +predicate Grinder(this: Ref) +{ + acc(this.hasBeans) +} + +function getHasBeans(this: Ref): Bool + requires Grinder(this) +{ + unfolding Grinder(this) in + this.hasBeans +} + +field Level: Int + +predicate WaterTank(this: Ref) +{ + acc(this.Level) && 0 <= this.Level +} + +function getLevel(this: Ref): Int + requires WaterTank(this) + ensures 0 <= result +{ + unfolding WaterTank(this) in + this.Level +} + +method GrinderAddBeans(this: Ref) + requires Grinder(this) + ensures Grinder(this) + ensures getHasBeans(this) + +method GrinderGrind(this: Ref) + requires Grinder(this) + requires getHasBeans(this) + ensures Grinder(this) + ensures !getHasBeans(this) + + method WaterTankFill(this: Ref) + requires WaterTank(this) + ensures WaterTank(this) + ensures getLevel(this) == 10 + +method WaterTankUse(this: Ref) + requires WaterTank(this) + requires getLevel(this) != 0 + ensures WaterTank(this) + ensures getLevel(this) == old(getLevel(this)) - 1 + + +predicate Cup(this: Ref) + + +method CupConstructor() returns (this: Ref) + ensures Cup(this) + + +field CMGrinder: Ref +field CMWaterTank: Ref + +predicate CoffeeMaker(this: Ref) +{ + acc(this.CMGrinder) && Grinder(this.CMGrinder) && + acc(this.CMWaterTank) && WaterTank(this.CMWaterTank) +} + +function getCoffeeMakerGrinder(this: Ref): Ref + requires CoffeeMaker(this) +{ + unfolding CoffeeMaker(this) in + this.CMGrinder +} + +function getCoffeeMakerWaterTank(this: Ref): Ref + requires CoffeeMaker(this) +{ + unfolding CoffeeMaker(this) in + this.CMWaterTank +} + +function CoffeeMakerReady(this: Ref): Bool + requires CoffeeMaker(this) +{ + true + //unfolding CoffeeMaker(this) in + //getHasBeans(this.CMGrinder) && 2 <= getLevel(this.CMWaterTank) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/16-2/coffee1.vpr b/src/test/resources/biabduction/dafny/16-2/coffee1.vpr new file mode 100644 index 000000000..e185417e3 --- /dev/null +++ b/src/test/resources/biabduction/dafny/16-2/coffee1.vpr @@ -0,0 +1,94 @@ +import "coffee.vpr" + + +method GrinderConstructor() returns (this: Ref) + //ensures Grinder(this) + //ensures !getHasBeans(this) +{ + this := new(hasBeans) + this.hasBeans := false + //fold Grinder(this) +} + + +method WaterTankConstructor() returns (this: Ref) + //ensures WaterTank(this) + //ensures getLevel(this) == 0 +{ + this := new(Level) + this.Level := 0 + //fold WaterTank(this) +} + + +method CoffeeMakerConstructor() returns (this: Ref) + //ensures CoffeeMaker(this) + //ensures unfolding CoffeeMaker(this) in !getHasBeans(this.CMGrinder) + //ensures unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank) == 0 +{ + this := new(CMGrinder, CMWaterTank) + this.CMGrinder := GrinderConstructor() + this.CMWaterTank := WaterTankConstructor() + //fold CoffeeMaker(this) +} + + +method CoffeeMakerRestock(this: Ref) + //requires CoffeeMaker(this) + //ensures CoffeeMaker(this) + //ensures CoffeeMakerReady(this) + //ensures unfolding CoffeeMaker(this) in getHasBeans(this.CMGrinder) + //ensures unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank) == 10 +{ + //unfold CoffeeMaker(this) + GrinderAddBeans(this.CMGrinder) + WaterTankFill(this.CMWaterTank) + //fold CoffeeMaker(this) +} + +method CoffeeMakerDispense(this: Ref, double: Bool) returns (c: Ref) + //requires CoffeeMaker(this) + //requires CoffeeMakerReady(this) + //ensures CoffeeMaker(this) + //ensures unfolding CoffeeMaker(this) in !getHasBeans(this.CMGrinder) + //ensures unfolding CoffeeMaker(this) in + // double ==> getLevel(this.CMWaterTank) == old(unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank)) - 2 + //ensures unfolding CoffeeMaker(this) in + // !double ==> getLevel(this.CMWaterTank) == old(unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank)) - 1 + //ensures Cup(c) +{ + //unfold CoffeeMaker(this) + GrinderGrind(this.CMGrinder) + if (double) + { + WaterTankUse(this.CMWaterTank) + WaterTankUse(this.CMWaterTank) + } + else + { + WaterTankUse(this.CMWaterTank) + } + c := CupConstructor() + //fold CoffeeMaker(this) +} + +method CoffeeMakerChangeGrinder(this: Ref) + //requires CoffeeMaker(this) + //ensures CoffeeMaker(this) + //ensures unfolding CoffeeMaker(this) in !getHasBeans(this.CMGrinder) +{ + //unfold CoffeeMaker(this) + this.CMGrinder := GrinderConstructor() + //fold CoffeeMaker(this) +} + +method CoffeeMakerInstallCustomGrinder(this: Ref, grinder: Ref) + //requires CoffeeMaker(this) + //requires Grinder(grinder) + //ensures CoffeeMaker(this) + //ensures unfolding CoffeeMaker(this) in old(getHasBeans(grinder)) == getHasBeans(this.CMGrinder) +{ + //unfold CoffeeMaker(this) + this.CMGrinder := grinder + //fold CoffeeMaker(this) +} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/coffee/exercises-16.2.vpr b/src/test/resources/biabduction/dafny/16-2/coffeen.vpr similarity index 96% rename from src/test/resources/biabduction/dafny/coffee/exercises-16.2.vpr rename to src/test/resources/biabduction/dafny/16-2/coffeen.vpr index bb5ffb1e3..a702a5571 100644 --- a/src/test/resources/biabduction/dafny/coffee/exercises-16.2.vpr +++ b/src/test/resources/biabduction/dafny/16-2/coffeen.vpr @@ -1,4 +1,4 @@ -import "examples-16.2.vpr" +import "coffee1.vpr" method CoffeemakerRemoveGrinder(this: Ref) returns (grinder: Ref) requires CoffeeMaker(this) diff --git a/src/test/resources/biabduction/dafny/checksum/exercises-16.0.vpr b/src/test/resources/biabduction/dafny/checksum/exercises-16.0.vpr deleted file mode 100644 index d8d7050d8..000000000 --- a/src/test/resources/biabduction/dafny/checksum/exercises-16.0.vpr +++ /dev/null @@ -1,128 +0,0 @@ -//import "examples-16.0.vpr" - -field checksumData: Int - -adt Option[T] { - Some(value: T) - None() -} - -field ocs: Option[Int] - -predicate ChecksumMachineOCS(this: Ref) -{ - acc(this.checksumData) && 0 <= this.checksumData && - acc(this.ocs) -} - -method ChecksumMachineOCSConstructor() returns (this: Ref) - ensures ChecksumMachineOCS(this) - ensures unfolding ChecksumMachineOCS(this) in this.checksumData == 0 - ensures unfolding ChecksumMachineOCS(this) in this.ocs.isNone -{ - this := new(checksumData, ocs) - this.checksumData := 0 - this.ocs := None() - fold ChecksumMachineOCS(this) -} - -method AppendOCS(this: Ref, d: Int) - requires ChecksumMachineOCS(this) - requires 0 <= d - ensures ChecksumMachineOCS(this) - ensures unfolding ChecksumMachineOCS(this) in this.checksumData == old(unfolding ChecksumMachineOCS(this) in this.checksumData) + d - ensures unfolding ChecksumMachineOCS(this) in this.ocs.isNone -{ - unfold ChecksumMachineOCS(this) - this.checksumData := this.checksumData + d - this.ocs := None() - fold ChecksumMachineOCS(this) -} - -method ChecksumOCS(this: Ref) returns (checksum: Int) - requires ChecksumMachineOCS(this) - //requires unfolding ChecksumMachineOCS(this) in this.ocs.isNone || this.ocs.value == Hash(this.checksumData) - ensures ChecksumMachineOCS(this) - ensures unfolding ChecksumMachineOCS(this) in this.checksumData == old(unfolding ChecksumMachineOCS(this) in this.checksumData) - //ensures unfolding ChecksumMachineOCS(this) in checksum == Hash(this.checksumData) - ensures unfolding ChecksumMachineOCS(this) in this.ocs == Some(checksum) -{ - unfold ChecksumMachineOCS(this) - if (this.ocs.isNone) - { - this.ocs := Some(this.checksumData % 137) - } - checksum := this.ocs.value - fold ChecksumMachineOCS(this) -} - -// Exercise 16.4 -/** - * This is a simple implementation of a ledger system, where we can deposit and - * withdraw a value. All transactions are stored in a sequence and the balance - * is the sum of all transactions. The balance cannot be negative. - * At the time of writing the Silicon symbolic execution backend is unable to - * verify the presented code, while the Carbon condition generation backend is - * able to verify the presented code. - */ -/* function Sum(s: Seq[Int]): Int -{ - (|s| == 0) ? 0 : s[0] + Sum(s[1..]) -} - -field LedgerTransactions: Seq[Int] -field LedgerBalance: Int - -predicate Ledger(this: Ref) -{ - acc(this.LedgerTransactions) && - acc(this.LedgerBalance) && 0 <= this.LedgerBalance && - this.LedgerBalance == Sum(this.LedgerTransactions) -} - -method LedgerConstructor() returns (this: Ref) - ensures Ledger(this) - ensures unfolding Ledger(this) in this.LedgerTransactions == Seq() - ensures unfolding Ledger(this) in this.LedgerBalance == 0 -{ - this := new(LedgerTransactions, LedgerBalance) - this.LedgerTransactions := Seq() - this.LedgerBalance := 0 - fold Ledger(this) -} - -method LedgerDeposit(this: Ref, n: Int) - requires Ledger(this) - requires 0 <= n - ensures Ledger(this) - ensures unfolding Ledger(this) in this.LedgerTransactions == Seq(n) ++ old(unfolding Ledger(this) in this.LedgerTransactions) - ensures unfolding Ledger(this) in this.LedgerBalance == n + old(unfolding Ledger(this) in this.LedgerBalance) -{ - unfold Ledger(this) - this.LedgerTransactions := Seq(n) ++ this.LedgerTransactions - this.LedgerBalance := this.LedgerBalance + n - fold Ledger(this) -} - -method LedgerWithdraw(this: Ref, n: Int) - requires Ledger(this) - requires 0 <= n - requires unfolding Ledger(this) in n <= this.LedgerBalance - ensures Ledger(this) - ensures unfolding Ledger(this) in this.LedgerTransactions == Seq(-n) ++ old(unfolding Ledger(this) in this.LedgerTransactions) - ensures unfolding Ledger(this) in this.LedgerBalance == old(unfolding Ledger(this) in this.LedgerBalance) - n -{ - unfold Ledger(this) - this.LedgerTransactions := Seq(-n) ++ this.LedgerTransactions - this.LedgerBalance := this.LedgerBalance - n - fold Ledger(this) -} - -method LedgerTestHarness() -{ - var l: Ref := LedgerConstructor() - LedgerDeposit(l, 100) - LedgerDeposit(l, 200) - LedgerWithdraw(l, 50) - assert unfolding Ledger(l) in l.LedgerBalance == 250 -} */ \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/coffee/examples-16.2.vpr b/src/test/resources/biabduction/dafny/coffee/examples-16.2.vpr deleted file mode 100644 index a62b38128..000000000 --- a/src/test/resources/biabduction/dafny/coffee/examples-16.2.vpr +++ /dev/null @@ -1,184 +0,0 @@ - -field hasBeans: Bool - -predicate Grinder(this: Ref) -{ - acc(this.hasBeans) -} - -function getHasBeans(this: Ref): Bool - requires Grinder(this) -{ - unfolding Grinder(this) in - this.hasBeans -} - -method GrinderConstructor() returns (this: Ref) - ensures Grinder(this) - ensures !getHasBeans(this) -{ - this := new(hasBeans) - this.hasBeans := false - fold Grinder(this) -} - - -method GrinderAddBeans(this: Ref) - requires Grinder(this) - ensures Grinder(this) - ensures getHasBeans(this) - -method GrinderGrind(this: Ref) - requires Grinder(this) - requires getHasBeans(this) - ensures Grinder(this) - ensures !getHasBeans(this) - -field Level: Int - -predicate WaterTank(this: Ref) -{ - acc(this.Level) && 0 <= this.Level -} - - -function getLevel(this: Ref): Int - requires WaterTank(this) - ensures 0 <= result -{ - unfolding WaterTank(this) in - this.Level -} - -method WaterTankConstructor() returns (this: Ref) - ensures WaterTank(this) - ensures getLevel(this) == 0 -{ - this := new(Level) - this.Level := 0 - fold WaterTank(this) -} - - -method WaterTankFill(this: Ref) - requires WaterTank(this) - ensures WaterTank(this) - ensures getLevel(this) == 10 - -method WaterTankUse(this: Ref) - requires WaterTank(this) - requires getLevel(this) != 0 - ensures WaterTank(this) - ensures getLevel(this) == old(getLevel(this)) - 1 - - -predicate Cup(this: Ref) - - -method CupConstructor() returns (this: Ref) - ensures Cup(this) - - -field CMGrinder: Ref -field CMWaterTank: Ref - -predicate CoffeeMaker(this: Ref) -{ - acc(this.CMGrinder) && Grinder(this.CMGrinder) && - acc(this.CMWaterTank) && WaterTank(this.CMWaterTank) -} - -function getCoffeeMakerGrinder(this: Ref): Ref - requires CoffeeMaker(this) -{ - unfolding CoffeeMaker(this) in - this.CMGrinder -} - -function getCoffeeMakerWaterTank(this: Ref): Ref - requires CoffeeMaker(this) -{ - unfolding CoffeeMaker(this) in - this.CMWaterTank -} - - -method CoffeeMakerConstructor() returns (this: Ref) - ensures CoffeeMaker(this) - ensures unfolding CoffeeMaker(this) in !getHasBeans(this.CMGrinder) - ensures unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank) == 0 -{ - this := new(CMGrinder, CMWaterTank) - this.CMGrinder := GrinderConstructor() - this.CMWaterTank := WaterTankConstructor() - fold CoffeeMaker(this) -} - - -function CoffeeMakerReady(this: Ref): Bool - requires CoffeeMaker(this) -{ - unfolding CoffeeMaker(this) in - getHasBeans(this.CMGrinder) && 2 <= getLevel(this.CMWaterTank) -} - - -method CoffeeMakerRestock(this: Ref) - requires CoffeeMaker(this) - ensures CoffeeMaker(this) - ensures CoffeeMakerReady(this) - ensures unfolding CoffeeMaker(this) in getHasBeans(this.CMGrinder) - ensures unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank) == 10 -{ - unfold CoffeeMaker(this) - GrinderAddBeans(this.CMGrinder) - WaterTankFill(this.CMWaterTank) - fold CoffeeMaker(this) -} - -method CoffeeMakerDispense(this: Ref, double: Bool) returns (c: Ref) - requires CoffeeMaker(this) - requires CoffeeMakerReady(this) - ensures CoffeeMaker(this) - ensures unfolding CoffeeMaker(this) in !getHasBeans(this.CMGrinder) - ensures unfolding CoffeeMaker(this) in - double ==> getLevel(this.CMWaterTank) == old(unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank)) - 2 - ensures unfolding CoffeeMaker(this) in - !double ==> getLevel(this.CMWaterTank) == old(unfolding CoffeeMaker(this) in getLevel(this.CMWaterTank)) - 1 - ensures Cup(c) -{ - unfold CoffeeMaker(this) - GrinderGrind(this.CMGrinder) - if (double) - { - WaterTankUse(this.CMWaterTank) - WaterTankUse(this.CMWaterTank) - } - else - { - WaterTankUse(this.CMWaterTank) - } - c := CupConstructor() - fold CoffeeMaker(this) -} - -method CoffeeMakerChangeGrinder(this: Ref) - requires CoffeeMaker(this) - ensures CoffeeMaker(this) - ensures unfolding CoffeeMaker(this) in !getHasBeans(this.CMGrinder) -{ - unfold CoffeeMaker(this) - this.CMGrinder := GrinderConstructor() - fold CoffeeMaker(this) -} - -method CoffeeMakerInstallCustomGrinder(this: Ref, grinder: Ref) - requires CoffeeMaker(this) - requires Grinder(grinder) - ensures CoffeeMaker(this) - ensures unfolding CoffeeMaker(this) in old(getHasBeans(grinder)) == getHasBeans(this.CMGrinder) -{ - unfold CoffeeMaker(this) - this.CMGrinder := grinder - fold CoffeeMaker(this) -} \ No newline at end of file diff --git a/src/test/resources/biabduction/dafny/tokenizer/exercises-16.1.vpr b/src/test/resources/biabduction/dafny/tokenizer/exercises-16.1.vpr deleted file mode 100644 index 707d90cdb..000000000 --- a/src/test/resources/biabduction/dafny/tokenizer/exercises-16.1.vpr +++ /dev/null @@ -1,270 +0,0 @@ -import "examples-16.1.vpr" - -// Exercise 16.6 -/** - * This is a modification of the Tokenizer code from the section 16.1 where we - * have two additional functions IsStart and IsFollow. Is start determines if - * the given character is a letter and IsFollow determines if the given character - * is a letter or a digit. With that we can modify the Read method to only - * allow Identifier tokens to start with a letter and follow with a letter or a - * digit. The change is only in the "read token" part of the method and if a - * faulty Identifier token is found, the method will return the Error category. - */ -function IsStart(ch: Int, cat: Category): Bool - requires !cat.isEnd - requires 0 <= ch <= 127 -{ - Is(ch, Identifier()) -} - -function IsFollow(ch: Int, cat: Category): Bool - requires !cat.isEnd - requires 0 <= ch <= 127 -{ - Is(ch, Identifier()) || Is(ch, Number()) -} - -method ReadModifedIdentifier(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 token == getSource(this)[p..getN(this)] - // New - ensures cat.isIdentifier ==> IsStart(token[0], cat) && forall i: Int :: 1 <= i < |token| ==> IsFollow(token[i], cat) -{ - // 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()) - { - unfold Tokenizer(this) - this.n := this.n + 1 - fold Tokenizer(this) - } - p := getN(this) - // determine syntactic category - var return: Bool := false - if (getN(this) == |getSource(this)|) - { - cat := End() - token := Seq() - return := true - } - elseif (Is(getSource(this)[getN(this)], Identifier())) - { - cat := Identifier() - } - elseif (Is(getSource(this)[getN(this)], Number())) - { - cat := Number() - } - elseif (Is(getSource(this)[getN(this)], Operator())) - { - cat := Operator() - } - else - { - cat := Error() - token := Seq() - return := true - } - // read token - if (!return) - { - var start: Int := getN(this) - if (cat.isIdentifier && !IsStart(getSource(this)[getN(this)], cat)) - { - return := true - } - else - { - unfold Tokenizer(this) - this.n := this.n + 1 - fold Tokenizer(this) - while (getN(this) != |getSource(this)| && Is(getSource(this)[getN(this)], cat) && !return) - 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) - { - if (cat.isIdentifier && !IsFollow(getSource(this)[getN(this)], cat)) - { - return := true - } - else - { - unfold Tokenizer(this) - this.n := this.n + 1 - fold Tokenizer(this) - } - } - } - if (return) - { - cat := Error() - token := Seq() - unfold Tokenizer(this) - this.n := p - fold Tokenizer(this) - } - else - { - token := getSource(this)[start..getN(this)] - } - } -} - -// Exercise 16.7 -/** - * This is a modification of the Tokenizer code from the section 16.1 where we - * have the ability to prune the input string, or sequence of ASCII code - * integers. For that, we track three - * additional fields suffix, m and j. The suffix field is the remaining part of - * the input string that has not been pruned. The m field tracks how many - * characters have been pruned from the input string and the j field tracks how - * many characters have been read from the suffix without pruning. We still - * maintain the source field for specification purposes, but we only use the - * suffix field for program logic. We also add a new method - * TokenizerWithPruningPrune that prunes the input string to the current read - * position m + j == n. - */ -field suffix: Seq[Int] -field m: Int -field j: Int - -predicate TokenizerWithPruning(this: Ref) -{ - acc(this.source) && acc(this.suffix) && acc(this.m) && acc(this.j) && - acc(this.n) && 0 <= this.n <= |this.source| && - this.suffix == this.source[this.m..] && this.m + this.j == this.n && - 0 <= this.m <= this.n && 0 <= this.j <= |this.suffix| && - forall i: Int :: 0 <= i < |this.source| ==> 0 <= this.source[i] <= 127 -} - -method TokenizerWithPruningConstructor(s: Seq[Int]) returns (this: Ref) - requires forall i: Int :: 0 <= i < |s| ==> 0 <= s[i] <= 127 - ensures TokenizerWithPruning(this) - ensures unfolding TokenizerWithPruning(this) in this.source == s && - this.suffix == s && this.m == 0 && this.j == 0 && this.n == 0 -{ - this := new(source, suffix, m, j, n) - this.source := s - this.suffix := s - this.m := 0 - this.j := 0 - this.n := 0 - fold TokenizerWithPruning(this) -} - -method TokenizerWithPruningPrune(this: Ref) - requires TokenizerWithPruning(this) - ensures TokenizerWithPruning(this) - ensures unfolding TokenizerWithPruning(this) in this.m == this.n && this.j == 0 - ensures unfolding TokenizerWithPruning(this) in this.suffix == this.source[this.m..] -{ - unfold TokenizerWithPruning(this) - this.m := this.n - this.j := 0 - this.suffix := this.source[this.m..] - fold TokenizerWithPruning(this) - -} - -method ReadWithPruning(this: Ref) returns (cat: Category, p: Int, token: Seq[Int]) - requires TokenizerWithPruning(this) - ensures 0 <= p - ensures TokenizerWithPruning(this) - ensures unfolding TokenizerWithPruning(this) in this.source == old(unfolding TokenizerWithPruning(this) in this.source) - ensures unfolding TokenizerWithPruning(this) in this.m == old(unfolding TokenizerWithPruning(this) in this.m) - ensures !cat.isWhitespace - ensures unfolding TokenizerWithPruning(this) in old(unfolding TokenizerWithPruning(this) in this.n) <= p <= this.n <= |this.source| - ensures unfolding TokenizerWithPruning(this) in cat.isEnd <==> p == |this.source| - ensures unfolding TokenizerWithPruning(this) in cat.isEnd || cat.isError <==> p == this.n - ensures unfolding TokenizerWithPruning(this) in forall i: Int :: old(unfolding TokenizerWithPruning(this) in this.n) <= i < p ==> - Is(this.source[i], Whitespace()) - ensures unfolding TokenizerWithPruning(this) in forall i: Int :: p <= i < this.n ==> Is(this.source[i], cat) - ensures unfolding TokenizerWithPruning(this) in p < this.n ==> this.n == |this.source| || !Is(this.source[this.n], cat) - ensures unfolding TokenizerWithPruning(this) in token == this.suffix[p-this.m..this.j] -{ - unfold TokenizerWithPruning(this) - assert 0 <= this.j <= |this.suffix| - fold TokenizerWithPruning(this) - // skip whitespace - while (unfolding TokenizerWithPruning(this) in this.j != |this.suffix| && Is(this.suffix[this.j], Whitespace())) - invariant TokenizerWithPruning(this) - invariant unfolding TokenizerWithPruning(this) in this.m == old(unfolding TokenizerWithPruning(this) in this.m) - invariant unfolding TokenizerWithPruning(this) in this.source == old(unfolding TokenizerWithPruning(this) in this.source) - invariant unfolding TokenizerWithPruning(this) in old(unfolding TokenizerWithPruning(this) in this.n) <= this.n <= |this.source| - invariant unfolding TokenizerWithPruning(this) in forall i: Int :: old(unfolding TokenizerWithPruning(this) in this.n) <= i < this.n ==> Is(this.source[i], Whitespace()) - { - unfold TokenizerWithPruning(this) - this.n := this.n + 1 - this.j := this.j + 1 - fold TokenizerWithPruning(this) - } - unfold TokenizerWithPruning(this) - p := this.n - fold TokenizerWithPruning(this) - // determine syntactic category - var return: Bool := false - if (unfolding TokenizerWithPruning(this) in this.n == |this.source|) - { - cat := End() - token := Seq() - return := true - } - elseif (unfolding TokenizerWithPruning(this) in Is(this.source[this.n], Identifier())) - { - cat := Identifier() - } - elseif (unfolding TokenizerWithPruning(this) in Is(this.source[this.n], Number())) - { - cat := Number() - } - elseif (unfolding TokenizerWithPruning(this) in Is(this.source[this.n], Operator())) - { - cat := Operator() - } - else - { - cat := Error() - token := Seq() - return := true - assert unfolding TokenizerWithPruning(this) in p - this.m == this.j - } - // read token - if (!return) - { - unfold TokenizerWithPruning(this) - var start: Int := this.j - this.n := this.n + 1 - this.j := this.j + 1 - fold TokenizerWithPruning(this) - while (unfolding TokenizerWithPruning(this) in this.n != |this.source| && Is(this.source[this.n], cat)) - invariant TokenizerWithPruning(this) - invariant unfolding TokenizerWithPruning(this) in this.m == old(unfolding TokenizerWithPruning(this) in this.m) - invariant unfolding TokenizerWithPruning(this) in this.source == old(unfolding TokenizerWithPruning(this) in this.source) - invariant unfolding TokenizerWithPruning(this) in p <= this.n <= |this.source| - invariant unfolding TokenizerWithPruning(this) in forall i: Int :: p <= i < this.n ==> Is(this.source[i], cat) - { - unfold TokenizerWithPruning(this) - this.n := this.n + 1 - this.j := this.j + 1 - fold TokenizerWithPruning(this) - } - unfold TokenizerWithPruning(this) - token := this.suffix[start..this.j] - fold TokenizerWithPruning(this) - } -} \ No newline at end of file diff --git a/src/test/resources/biabduction/grasshopper/nested_sl/destroy.vpr b/src/test/resources/biabduction/grasshopper/nested_sl/destroy.vpr index 47c70cc5c..7d65d5e9a 100644 --- a/src/test/resources/biabduction/grasshopper/nested_sl/destroy.vpr +++ b/src/test/resources/biabduction/grasshopper/nested_sl/destroy.vpr @@ -1,22 +1,22 @@ import "./nested_def.vpr" method destroy(x: Ref) -requires OuterNode(x) +//requires OuterNode(x) { var currO: Ref := x while(currO != null) - invariant OuterNode(currO) + //invariant OuterNode(currO) { var currO_old: Ref := currO - unfold OuterNode(currO) + //unfold OuterNode(currO) var ic: Ref := currO.down var currI: Ref := ic while(currI != null) - invariant InnerNode(currI) + //invariant InnerNode(currI) { var currI_old: Ref := currI - unfold InnerNode(currI) + //unfold InnerNode(currI) currI := currI.inext freeI(currI_old) } diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr index d63ef4e09..f0e568c5f 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_concat.vpr @@ -5,10 +5,11 @@ method concat(x: Ref, y: Ref) returns (res: Ref) requires list(y) //ensures list(res) { + var curr: Ref if (x == null) { res := y } else { - var curr: Ref := x + curr := x //package list(curr) --* list(x) //unfold list(curr) while (curr.next != null) diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr index ed535ef2b..912c903fb 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_filter.vpr @@ -15,7 +15,7 @@ method filter(x: Ref) returns (res: Ref) while(curr != null) //invariant list(prev) --* list(x) - invariant acc(prev.next) + //invariant acc(prev.next) //invariant acc(prev.data) invariant prev.next == curr //invariant list(curr) diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr index 4ff3888a5..c9f65aaab 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_insert.vpr @@ -38,6 +38,7 @@ method insert(x: Ref, elt: Ref) returns (res: Ref) //apply list(curr) --* list(x) res := x } + assert acc(elt.next, write) } diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_remove.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_remove.vpr index 3811aeb2b..b39cb6cac 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_remove.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_remove.vpr @@ -1,39 +1,42 @@ import "./sl.vpr" method remove(x: Ref) returns (res: Ref) -requires list(x) -ensures list(res) +//requires list(x) +//ensures list(res) { + var curr: Ref + var tmp: Ref + var nondet: Bool + if(x == null){ res := null } else { - var nondet: Bool - var curr: Ref := x + curr := 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) + //} } - var tmp: Ref := curr.next + tmp := curr.next if(tmp != null) { - unfold list(tmp) + //unfold list(tmp) curr.next := tmp.next } - fold list(curr) - apply list(curr) --* list(x) + //fold list(curr) + //apply list(curr) --* list(x) res := x } } diff --git a/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr b/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr index 809c37327..246023de6 100644 --- a/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr +++ b/src/test/resources/biabduction/grasshopper/sl/sl_reverse.vpr @@ -1,21 +1,23 @@ import "./sl.vpr" method reverse(x: Ref) returns (res: Ref) -requires list(x) -ensures list(res) +//requires list(x) +//ensures list(res) { + //var tmp: Ref := null res := null - fold list(res) + //fold list(res) var curr: Ref := x while(curr != null) - invariant list(curr) - invariant list(res) + //invariant list(curr) + //invariant list(res) { var tmp: Ref := curr - unfold list(curr) + //unfold list(curr) curr := curr.next tmp.next := res res := tmp - fold list(tmp) + assert res.data == tmp.data + //fold list(tmp) } } \ No newline at end of file diff --git a/src/test/resources/biabduction/mytests/nlist/abstract.vpr b/src/test/resources/biabduction/mytests/nlist/abstract.vpr new file mode 100644 index 000000000..0351338a4 --- /dev/null +++ b/src/test/resources/biabduction/mytests/nlist/abstract.vpr @@ -0,0 +1,12 @@ +field next: Ref + +predicate list(x: Ref){ + x != null ==> acc(x.next) && list(x.next) +} + +method foo() returns (x: Ref, y: Ref) +//requires acc(this.next, write) +{ + x := new(next) + x.next := y +} diff --git a/src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr b/src/test/resources/biabduction/vipertests/basic/recursive_unrolling.vpr similarity index 99% rename from src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr rename to src/test/resources/biabduction/vipertests/basic/recursive_unrolling.vpr index c9a270c9d..d1446a858 100644 --- a/src/test/resources/biabduction/vipertests/functions/recursive_unrolling.vpr +++ b/src/test/resources/biabduction/vipertests/basic/recursive_unrolling.vpr @@ -7,7 +7,7 @@ predicate node(this: Ref) { acc(this.next) && (this.next != null ==> acc(node(this.next))) } -/* + method test01() { var n1: Ref; n1 := new(next) n1.next := null @@ -31,7 +31,7 @@ method test01() { assert acc(node(n5)) } -*/ + method test02(n4: Ref) //requires acc(node(n4)) diff --git a/src/test/resources/biabduction/vipertests/predicates/arguments.vpr b/src/test/resources/biabduction/vipertests/predicates/arguments.vpr index 784c9dcec..f0b0c76a6 100644 --- a/src/test/resources/biabduction/vipertests/predicates/arguments.vpr +++ b/src/test/resources/biabduction/vipertests/predicates/arguments.vpr @@ -37,54 +37,4 @@ method t2(this: Ref) { fold acc(valid(this, true), write) unrelated(this) -} - -method t2b(this: Ref) - requires acc(this.f, write) - ensures acc(valid(this, true), write) -{ - //:: ExpectedOutput(fold.failed:insufficient.permission) - fold acc(valid(this, false), write) -} - -method t3(this: Ref, b: Bool) - requires acc(this.unrelatedField, write) - requires acc(valid(this, b), write) - requires acc(valid(this, !b), write) - //:: UnexpectedOutput(not.wellformed:insufficient.permission, /silicon/issue/36/) - requires (unfolding acc(valid(this, false), write) in ((this.g) == 2)) - ensures acc(valid(this, b), write) - ensures acc(valid(this, !b), write) - ensures (unfolding acc(valid(this, false), write) in ((this.g) == 2)) -{ - unfold acc(valid(this, true), write) - this.f := 1 - fold acc(valid(this, true), write) -} - -method t3a(this: Ref, b: Bool) - requires acc(this.unrelatedField, write) - requires acc(valid(this, b), write) - requires acc(valid(this, !b), write) - //:: UnexpectedOutput(not.wellformed:insufficient.permission, /silicon/issue/36/) - requires (unfolding acc(valid(this, false), write) in ((this.g) == 2)) - ensures acc(valid(this, b), write) - ensures acc(valid(this, !b), write) - ensures (unfolding acc(valid(this, false), write) in ((this.g) == 2)) -{ - unfold acc(valid(this, true), write) - this.f := 1 - fold acc(valid(this, true), write) - unrelated(this) -} - -method t3b(this: Ref, b: Bool) - requires acc(valid(this, b), write) - requires acc(valid(this, !b), write) -{ - //:: UnexpectedOutput(unfold.failed:insufficient.permission, /silicon/issue/36/) - unfold acc(valid(this, true), write) - //:: ExpectedOutput(assignment.failed:insufficient.permission) - //:: MissingOutput(assignment.failed:insufficient.permission, /silicon/issue/36/) - this.g := 1 -} +} \ No newline at end of file diff --git a/src/test/resources/biabduction/vipertests/functions/linkedlists.vpr b/src/test/resources/biabduction/vipertests/predicates/linkedlists.vpr similarity index 100% rename from src/test/resources/biabduction/vipertests/functions/linkedlists.vpr rename to src/test/resources/biabduction/vipertests/predicates/linkedlists.vpr diff --git a/src/test/resources/biabduction/vipertests/tree-delete-min/tree_delete_min.vpr b/src/test/resources/biabduction/vipertests/predicates/tree_delete_min.vpr similarity index 100% rename from src/test/resources/biabduction/vipertests/tree-delete-min/tree_delete_min.vpr rename to src/test/resources/biabduction/vipertests/predicates/tree_delete_min.vpr diff --git a/src/test/resources/biabduction/vipertests/wands/Assume.vpr b/src/test/resources/biabduction/vipertests/wands/Assume.vpr index fa52d53d0..c7989fd8d 100644 --- a/src/test/resources/biabduction/vipertests/wands/Assume.vpr +++ b/src/test/resources/biabduction/vipertests/wands/Assume.vpr @@ -12,6 +12,7 @@ predicate LinkedList(x: Ref) { method test0(x: Ref) requires LinkedList(x) ensures LinkedList(x) +ensures LinkedList(x) --* acc(x.next) && LinkedList(x.next) { package LinkedList(x) --* acc(x.next) && LinkedList(x.next) { unfold LinkedList(x)