diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index d8aadc52a499218e1f71e9e1eac3d204c3feb1ab..3b83def31b084747d88d27b1ce139b19adc77e0c 100644 --- a/src/main/scala/leon/purescala/ExprOps.scala +++ b/src/main/scala/leon/purescala/ExprOps.scala @@ -1270,6 +1270,10 @@ object ExprOps { } } + def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = { + CollectorWithPaths(f).traverse(expr) + } + def patternSize(p: Pattern): Int = p match { case wp: WildcardPattern => 1 @@ -2047,4 +2051,46 @@ object ExprOps { None } + + /** Collects correctness conditions from within an expression + * (taking into account the path condition). + * + * Collection of preconditions of function invocations + * can be disabled (mainly for [[leon.verification.Tactic]]). + * + * @param e The expression to traverse + * @param collectFIs Whether we also want to collect preconditions for function invocations + * @return A sequence of pairs (expression, condition) + */ + def collectCorrectnessConditions(e: Expr, collectFIs: Boolean = true): Seq[(Expr, Expr)] = { + val conds = collectWithPC { + + case m @ MatchExpr(scrut, cases) => + (m, orJoin(cases map (matchCaseCondition(scrut, _)))) + + case e @ Error(_, _) => + (e, BooleanLiteral(false)) + + case a @ Assert(cond, _, _) => + (a, cond) + + case e @ Ensuring(body, post) => + (e, application(post, Seq(body))) + + case r @ Require(pred, e) => + (r, pred) + + case fi @ FunctionInvocation(tfd, args) if tfd.hasPrecondition && collectFIs => + (fi, tfd.withParamSubst(args, tfd.precondition.get)) + }(e) + + conds map { + case ((e, cond), path) => + (e, implies(path, cond)) + } + } + + + + } diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala index f6dfaa543c4ce31d508461e195a5bbea8958490d..cce26dec5a45ea6cfad1a4fbfada8be48208c623 100644 --- a/src/main/scala/leon/purescala/TransformerWithPC.scala +++ b/src/main/scala/leon/purescala/TransformerWithPC.scala @@ -16,11 +16,11 @@ abstract class TransformerWithPC extends Transformer { protected def register(cond: Expr, path: C): C protected def rec(e: Expr, path: C): Expr = e match { - case Let(i, e, b) => - val se = rec(e, path) + case Let(i, v, b) => + val se = rec(v, path) val sb = rec(b, register(Equals(Variable(i), se), path)) Let(i, se, sb).copiedFrom(e) - + case p:Passes => applyAsMatches(p,rec(_,path)) @@ -71,8 +71,6 @@ abstract class TransformerWithPC extends Transformer { case o @ Operator(es, builder) => builder(es.map(rec(_, path))).copiedFrom(o) - case t : Terminal => t - case _ => sys.error("Expression "+e+" ["+e.getClass+"] is not extractable") } diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala index 616f3420d686569e6cbfe4485b399d0d7823129d..a00066ef1d4aca5f42ef3820d3fe133db074a7c3 100644 --- a/src/main/scala/leon/verification/DefaultTactic.scala +++ b/src/main/scala/leon/verification/DefaultTactic.scala @@ -9,82 +9,76 @@ import purescala.Definitions._ import purescala.Constructors._ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) { - val description = "Default verification condition generation approach" + val description = "Default verification condition generation approach" - def generatePostconditions(fd: FunDef): Seq[VC] = { - (fd.postcondition, fd.body) match { - case (Some(post), Some(body)) => - val vc = implies(precOrTrue(fd), application(post, Seq(body))) - - Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post)) - case _ => - Nil - } + def generatePostconditions(fd: FunDef): Seq[VC] = { + (fd.postcondition, fd.body) match { + case (Some(post), Some(body)) => + val vc = implies(precOrTrue(fd), application(post, Seq(body))) + Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post)) + case _ => + Nil } - - def generatePreconditions(fd: FunDef): Seq[VC] = { - fd.body match { - case Some(body) => - val calls = collectWithPC { - case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (c, tfd.precondition.get) - }(body) + } - calls.map { - case ((fi @ FunctionInvocation(tfd, args), pre), path) => - val pre2 = tfd.withParamSubst(args, pre) - val vc = implies(and(precOrTrue(fd), path), pre2) - val fiS = sizeLimit(fi.asString, 40) - VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi) - } + def generatePreconditions(fd: FunDef): Seq[VC] = { + fd.body match { + case Some(body) => + val calls = collectWithPC { + case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (c, tfd.precondition.get) + }(body) - case None => - Nil - } - } + calls.map { + case ((fi @ FunctionInvocation(tfd, args), pre), path) => + val pre2 = tfd.withParamSubst(args, pre) + val vc = implies(and(precOrTrue(fd), path), pre2) + val fiS = sizeLimit(fi.asString, 40) + VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi) + } - def generateCorrectnessConditions(fd: FunDef): Seq[VC] = { - fd.body match { - case Some(body) => - val calls = collectWithPC { + case None => + Nil + } + } - case m @ MatchExpr(scrut, cases) => - (m, VCKinds.ExhaustiveMatch, orJoin(cases map (matchCaseCondition(scrut, _)))) + def generateCorrectnessConditions(fd: FunDef): Seq[VC] = { - case e @ Error(_, _) => - (e, VCKinds.Assert, BooleanLiteral(false)) + def eToVCKind(e: Expr) = e match { + case _ : MatchExpr => + VCKinds.ExhaustiveMatch - case a @ Assert(cond, Some(err), _) => - val kind = if (err.startsWith("Map ")) { - VCKinds.MapUsage - } else if (err.startsWith("Array ")) { - VCKinds.ArrayUsage - } else if (err.startsWith("Division ")) { - VCKinds.DivisionByZero - } else if (err.startsWith("Modulo ")) { - VCKinds.ModuloByZero - } else if (err.startsWith("Remainder ")) { - VCKinds.RemainderByZero - } else if (err.startsWith("Cast ")) { - VCKinds.CastError - } else { - VCKinds.Assert - } + case Assert(_, Some(err), _) => + if (err.startsWith("Map ")) { + VCKinds.MapUsage + } else if (err.startsWith("Array ")) { + VCKinds.ArrayUsage + } else if (err.startsWith("Division ")) { + VCKinds.DivisionByZero + } else if (err.startsWith("Modulo ")) { + VCKinds.ModuloByZero + } else if (err.startsWith("Remainder ")) { + VCKinds.RemainderByZero + } else if (err.startsWith("Cast ")) { + VCKinds.CastError + } else { + VCKinds.Assert + } - (a, kind, cond) - case a @ Assert(cond, None, _) => (a, VCKinds.Assert, cond) - // Only triggered for inner ensurings, general postconditions are handled by generatePostconditions - case a @ Ensuring(body, post) => (a, VCKinds.Assert, application(post, Seq(body))) - }(body) + case _ => + VCKinds.Assert + } - calls.map { - case ((e, kind, correctnessCond), path) => - val vc = implies(and(precOrTrue(fd), path), correctnessCond) + fd.body.toSeq.flatMap { body => + // We don't collect preconditions here, because these are handled by generatePreconditions + val calls = collectCorrectnessConditions(body, collectFIs = false) - VC(vc, fd, kind).setPos(e) - } + calls.map { + case (e, correctnessCond) => + val vc = implies(precOrTrue(fd), correctnessCond) - case None => - Nil + VC(vc, fd, eToVCKind(e)).setPos(e) } } + } + } diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala index 2295cb191bd1005b9233ebfb368da407411f480c..77691739f6d57488d7dd13a43261976e3ca4df6d 100644 --- a/src/main/scala/leon/verification/Tactic.scala +++ b/src/main/scala/leon/verification/Tactic.scala @@ -10,7 +10,7 @@ import purescala.ExprOps._ abstract class Tactic(vctx: VerificationContext) { val description : String - implicit val ctx = vctx.context + implicit protected val ctx = vctx.context def generateVCs(fd: FunDef): Seq[VC] = { generatePostconditions(fd) ++ @@ -28,10 +28,6 @@ abstract class Tactic(vctx: VerificationContext) { case None => BooleanLiteral(true) } - protected def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = { - CollectorWithPaths(f).traverse(expr) - } - protected def sizeLimit(s: String, limit: Int) = { require(limit > 3) // Crop the call to display it properly