diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala index 8b3dd1463d8807775c31861277f875cee6a86077..86405da600c7ec006c41da3c4c33433354775b66 100644 --- a/src/main/scala/leon/codegen/CodeGeneration.scala +++ b/src/main/scala/leon/codegen/CodeGeneration.scala @@ -197,18 +197,10 @@ trait CodeGeneration { val idParams = (if (requireMonitor) Seq(monitorID) else Seq.empty) ++ funDef.paramIds val newMapping = idParams.zipWithIndex.toMap.mapValues(_ + (if (!isStatic) 1 else 0)) - val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name)) - - val bodyWithPre = if(funDef.hasPrecondition && params.checkContracts) { - IfExpr(funDef.precondition.get, body, Error(body.getType, "Precondition failed")) + val body = if (params.checkContracts) { + funDef.fullBody } else { - body - } - - val bodyWithPost = funDef.postcondition match { - case Some(post) if params.checkContracts => - ensur(bodyWithPre, post).toAssert - case _ => bodyWithPre + funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name)) } val locals = NoLocals.withVars(newMapping) @@ -218,7 +210,7 @@ trait CodeGeneration { ch << InvokeVirtual(MonitorClass, "onInvoke", "()V") } - mkExpr(bodyWithPost, ch)(locals) + mkExpr(body, ch)(locals) funDef.returnType match { case ValueType() => @@ -802,6 +794,9 @@ trait CodeGeneration { case en @ Ensuring(_, _) => mkExpr(en.toAssert, ch) + case Require(pre, body) => + mkExpr(IfExpr(pre, body, Error(body.getType, "Precondition failed")), ch) + case Let(i,d,b) => mkExpr(d, ch) val slot = ch.getFreshVar diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index 38915fe511475eb9d302fcafa9b01667af38479a..27525657e8605ea828607951b2c29a56b1f0fc84 100644 --- a/src/main/scala/leon/purescala/ExprOps.scala +++ b/src/main/scala/leon/purescala/ExprOps.scala @@ -2182,7 +2182,7 @@ object ExprOps { * @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)] = { + def collectCorrectnessConditions(e: Expr, collectFIs: Boolean = false): Seq[(Expr, Expr)] = { val conds = collectWithPC { case m @ MatchExpr(scrut, cases) => @@ -2194,11 +2194,11 @@ object ExprOps { case a @ Assert(cond, _, _) => (a, cond) - case e @ Ensuring(body, post) => + /*case e @ Ensuring(body, post) => (e, application(post, Seq(body))) case r @ Require(pred, e) => - (r, pred) + (r, pred)*/ case fi @ FunctionInvocation(tfd, args) if tfd.hasPrecondition && collectFIs => (fi, tfd.withParamSubst(args, tfd.precondition.get)) diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala index f47bc4cf6c8673291b393d943aa2f42f20d217e6..3fc618d67c925ec9367c7274d0b9e0671788682e 100644 --- a/src/main/scala/leon/purescala/TransformerWithPC.scala +++ b/src/main/scala/leon/purescala/TransformerWithPC.scala @@ -29,12 +29,32 @@ abstract class TransformerWithPC extends Transformer { val sb = rec(b, register(Equals(Variable(i), se), path)) Let(i, se, sb).copiedFrom(e) - case Require(pred, body) => - val sp = rec(pred, path) + case Ensuring(req@Require(pre, body), lam@Lambda(Seq(arg), post)) => + val spre = rec(pre, path) + val sbody = rec(body, register(spre, path)) + val spost = rec(post, register( + and(spre, Equals(arg.toVariable, sbody)), + path + )) + Ensuring( + Require(spre, sbody).copiedFrom(req), + Lambda(Seq(arg), spost).copiedFrom(lam) + ).copiedFrom(e) + + case Ensuring(body, lam@Lambda(Seq(arg), post)) => + val sbody = rec(body, path) + val spost = rec(post, register(Equals(arg.toVariable, sbody), path)) + Ensuring( + sbody, + Lambda(Seq(arg), spost).copiedFrom(lam) + ).copiedFrom(e) + + case Require(pre, body) => + val sp = rec(pre, path) val sb = rec(body, register(sp, path)) Require(sp, sb).copiedFrom(e) - //@mk: Discuss if we should include asserted predicates in the pc + //@mk: TODO Discuss if we should include asserted predicates in the pc //case Assert(pred, err, body) => // val sp = rec(pred, path) // val sb = rec(body, register(sp, path)) diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala index 4ea8a029dd285cef58bca2ab9c6e35d4ed1202ce..08b415c6b787a4f64dd7611ff8c755d2cdc419ba 100644 --- a/src/main/scala/leon/utils/TypingPhase.scala +++ b/src/main/scala/leon/utils/TypingPhase.scala @@ -44,7 +44,7 @@ object TypingPhase extends SimpleLeonPhase[Program, Program] { argTypesPreconditions match { case Nil => fd.precondition case xs => fd.precondition match { - case Some(p) => Some(andJoin(p +: xs)) + case Some(p) => Some(andJoin(xs :+ p)) case None => Some(andJoin(xs)) } } diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala index 6e90f0da4cf9de18af003d8bb04ffd0c2dd11500..244b38b30a885d588ef4b38336d9765c60e55417 100644 --- a/src/main/scala/leon/verification/DefaultTactic.scala +++ b/src/main/scala/leon/verification/DefaultTactic.scala @@ -22,23 +22,20 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) { } 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(fd.precOrTrue, path), pre2) - val fiS = sizeLimit(fi.asString, 40) - VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi) - } - case None => - Nil + val calls = collectWithPC { + case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => + c + }(fd.fullBody) + + calls.map { + case (fi @ FunctionInvocation(tfd, args), path) => + val pre = tfd.withParamSubst(args, tfd.precondition.get) + val vc = implies(path, pre) + val fiS = sizeLimit(fi.asString, 40) + VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi) } + } def generateCorrectnessConditions(fd: FunDef): Seq[VC] = { @@ -68,17 +65,14 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) { VCKinds.Assert } - fd.body.toSeq.flatMap { body => - // We don't collect preconditions here, because these are handled by generatePreconditions - val calls = collectCorrectnessConditions(body, collectFIs = false) - - calls.map { - case (e, correctnessCond) => - val vc = implies(fd.precOrTrue, correctnessCond) + // We don't collect preconditions here, because these are handled by generatePreconditions + val calls = collectCorrectnessConditions(fd.fullBody) - VC(vc, fd, eToVCKind(e)).setPos(e) - } + calls.map { + case (e, correctnessCond) => + VC(correctnessCond, fd, eToVCKind(e)).setPos(e) } } + } diff --git a/src/test/resources/regression/verification/purescala/invalid/PreInSpecs.scala b/src/test/resources/regression/verification/purescala/invalid/PreInSpecs.scala new file mode 100644 index 0000000000000000000000000000000000000000..4f184bac1d597ccaac1eee8e9e2a5cdb6f5cae26 --- /dev/null +++ b/src/test/resources/regression/verification/purescala/invalid/PreInSpecs.scala @@ -0,0 +1,25 @@ +import leon.lang._ + +object PreInSpecs { + + def f(i : BigInt): Boolean = { + require(i >= 0) + i > 0 + } + + def g(i : BigInt): Boolean = { + require(i >= 0) + i >= -1 + } holds + + def invoke(i : BigInt): BigInt = { + require(i == 0 || i > 0 && f(i - 1)) + i + 1 + } ensuring(res => g(i - 1)) + + def invoke2(i: BigInt): BigInt = { + require(g(i)) + 0 + } + +} diff --git a/src/test/resources/regression/verification/purescala/valid/PreInSpecs.scala b/src/test/resources/regression/verification/purescala/valid/PreInSpecs.scala new file mode 100644 index 0000000000000000000000000000000000000000..988f7331aac7f839ff01d7550cfa9f72b90ecc71 --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/PreInSpecs.scala @@ -0,0 +1,25 @@ +import leon.lang._ + +object PreInSpecs { + + def f(i : BigInt): Boolean = { + require(i >= 0) + i > 0 + } + + def g(i : BigInt): Boolean = { + require(i > 0) + i >= -1 + } holds + + def invoke(i : BigInt): BigInt = { + require(i == 0 || i > 0 && f(i - 1)) + i + 1 + } ensuring(res => g(i + 1)) + + def invoke2(i: BigInt): BigInt = { + require(i > 0 && g(i)) + 0 + } + +}