From 589c8d6a0c8547da8793a705a9c4c5962656983d Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Thu, 11 Jun 2020 21:11:05 +0200 Subject: [PATCH] Fix model checking of inlined adt invariant --- .../verification/DefaultTactic.scala | 2 +- .../stainless/verification/TypeChecker.scala | 4 ++-- .../verification/VerificationChecker.scala | 18 +++++++++------ .../verification/VerificationConditions.scala | 3 ++- .../invalid/ADTInvariantInlineCheck.scala | 23 +++++++++++++++++++ 5 files changed, 39 insertions(+), 11 deletions(-) create mode 100644 frontends/benchmarks/verification/invalid/ADTInvariantInlineCheck.scala diff --git a/core/src/main/scala/stainless/verification/DefaultTactic.scala b/core/src/main/scala/stainless/verification/DefaultTactic.scala index d13f441f05..5bd6d83830 100644 --- a/core/src/main/scala/stainless/verification/DefaultTactic.scala +++ b/core/src/main/scala/stainless/verification/DefaultTactic.scala @@ -126,7 +126,7 @@ trait DefaultTactic extends Tactic { case (a @ ADT(aid, tps, args), path) if a.getConstructor.sort.hasInvariant => val invId = a.getConstructor.sort.invariant.get.id val condition = path implies FunctionInvocation(invId, tps, Seq(a)) - VC(condition, id, VCKind.AdtInvariant(invId), false).setPos(a) + VC(condition, id, VCKind.AdtInvariant(invId, condition), false).setPos(a) }(getFunction(id).fullBody) } } diff --git a/core/src/main/scala/stainless/verification/TypeChecker.scala b/core/src/main/scala/stainless/verification/TypeChecker.scala index 1443930408..d0b59eb45f 100644 --- a/core/src/main/scala/stainless/verification/TypeChecker.scala +++ b/core/src/main/scala/stainless/verification/TypeChecker.scala @@ -825,7 +825,7 @@ trait TypeChecker { val trInv = if (sort.hasInvariant) { val inv = sort.typed(tps).invariant.get - val invKind = VCKind.AdtInvariant(id) + val invKind = VCKind.AdtInvariant(id, inv.applied(Seq(e))) val tc2 = tc.withVCKind(invKind).setPos(e) if (inv.flags.contains(InlineInvariant)) { val (tc3, freshener) = tc2.freshBindWithValues(inv.params, Seq(e)) @@ -864,7 +864,7 @@ trait TypeChecker { val trInv = if (sort.hasInvariant) { val inv = sort.typed(tps).invariant.get - val invKind = VCKind.AdtInvariant(inv.id) + val invKind = VCKind.AdtInvariant(inv.id, inv.applied(Seq(e))) val tc2 = tc.withVCKind(invKind).setPos(e) if (inv.flags.contains(InlineInvariant)) { val (tc3, freshener) = tc2.freshBindWithValues(inv.params, Seq(e)) diff --git a/core/src/main/scala/stainless/verification/VerificationChecker.scala b/core/src/main/scala/stainless/verification/VerificationChecker.scala index f0a5a6ad87..31f68b31e5 100644 --- a/core/src/main/scala/stainless/verification/VerificationChecker.scala +++ b/core/src/main/scala/stainless/verification/VerificationChecker.scala @@ -144,12 +144,12 @@ trait VerificationChecker { self => * - rewrite the invariant's invocation to be applied to this new variable instead. * - evaluate the resulting condition under the new model. */ - protected def checkAdtInvariantModel(vc: VC, invId: Identifier, model: Model): VCStatus = { + protected def checkAdtInvariantModel(vc: VC, invId: Identifier, originalCondition: Expr, model: Model): VCStatus = { import inox.evaluators.EvaluationResults._ - val Seq((inv, adt, path)) = collectWithPC(vc.condition) { - case (inv @ FunctionInvocation(`invId`, _, Seq(adt: ADT)), path) => (inv, adt, path) - } + val condition = simplifyExpr( + simplifyLets(simplifyAssertions(originalCondition)) + )(PurityOptions.assumeChecked) def success: VCStatus = { reporter.debug("- Model validated.") @@ -161,6 +161,10 @@ trait VerificationChecker { self => VCStatus.Unknown } + val Seq((inv, adt, path)) = collectWithPC(condition) { + case (inv @ FunctionInvocation(`invId`, _, Seq(adt: ADT)), path) => (inv, adt, path) + } + evaluator.eval(path.toClause, model) match { case Successful(BooleanLiteral(true)) => // path condition was true, we must evaluate invariant case Successful(BooleanLiteral(false)) => return success @@ -184,7 +188,7 @@ trait VerificationChecker { self => val adtVar = Variable(FreshIdentifier("adt"), adt.getType(symbols), Seq()) val newInv = FunctionInvocation(invId, inv.tps, Seq(adtVar)) val newModel = inox.Model(program)(model.vars + (adtVar.toVal -> newAdt), model.chooses) - val newCondition = exprOps.replace(Map(inv -> newInv), vc.condition) + val newCondition = exprOps.replace(Map(inv -> newInv), condition) evaluator.eval(newCondition, newModel) match { case Successful(BooleanLiteral(false)) => success @@ -252,8 +256,8 @@ trait VerificationChecker { self => VCResult(VCStatus.Valid, s.getResultSolver, Some(time)) case SatWithModel(model) if checkModels && vc.kind.isInstanceOf[VCKind.AdtInvariant] => - val VCKind.AdtInvariant(invId) = vc.kind - val status = checkAdtInvariantModel(vc, invId, model) + val VCKind.AdtInvariant(invId, expr: Expr) = vc.kind + val status = checkAdtInvariantModel(vc, invId, expr, model) VCResult(status, s.getResultSolver, Some(time)) case SatWithModel(model) if !vc.satisfiability => diff --git a/core/src/main/scala/stainless/verification/VerificationConditions.scala b/core/src/main/scala/stainless/verification/VerificationConditions.scala index 49ea802a49..d57a864c1c 100644 --- a/core/src/main/scala/stainless/verification/VerificationConditions.scala +++ b/core/src/main/scala/stainless/verification/VerificationConditions.scala @@ -45,7 +45,8 @@ object VCKind { case class AssertErr(err: String) extends VCKind("body assertion: " + err, "assert.") case object CoqMethod extends VCKind("coq function", "coq fun.") case class Error(err: String) extends VCKind(err, "error") - case class AdtInvariant(inv: Identifier) extends VCKind("adt invariant", "adt inv.") + + case class AdtInvariant(inv: Identifier, expr: ast.Trees#Expr) extends VCKind("adt invariant", "adt inv.") def fromErr(optErr: Option[String]) = { optErr.map { err => diff --git a/frontends/benchmarks/verification/invalid/ADTInvariantInlineCheck.scala b/frontends/benchmarks/verification/invalid/ADTInvariantInlineCheck.scala new file mode 100644 index 0000000000..30aa8ad224 --- /dev/null +++ b/frontends/benchmarks/verification/invalid/ADTInvariantInlineCheck.scala @@ -0,0 +1,23 @@ + +import stainless.lang._ +import stainless.annotation._ +import stainless.collection._ + +object inlineInv { + + @inlineInvariant + sealed abstract class Toto + + case class Foo(x: BigInt) extends Toto { + require(x > 10) + } + + def bad: Toto = { + Foo(5) + } + + def ok: Toto = { + Foo(15) + } + +}