From 6e08d3b3989053a251abea8eba9333fe6b61eb94 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 | 6 ++--- .../verification/VerificationChecker.scala | 18 +++++++++------ .../verification/VerificationConditions.scala | 3 ++- .../invalid/ADTInvariantInlineCheck.scala | 23 +++++++++++++++++++ 5 files changed, 40 insertions(+), 12 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 1603c1f4fd..de2432451b 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 883bdf52f3..9331907e3c 100644 --- a/core/src/main/scala/stainless/verification/TypeChecker.scala +++ b/core/src/main/scala/stainless/verification/TypeChecker.scala @@ -797,7 +797,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) = tc.freshBindWithValues(inv.params, Seq(e)) @@ -836,10 +836,10 @@ 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) = tc.freshBindWithValues(inv.params, Seq(e)) + val (tc3, freshener) = tc2.freshBindWithValues(inv.params, Seq(e)) buildVC(tc3, freshener.transform(inv.fullBody)) } else { buildVC(tc2, inv.applied(Seq(e))) diff --git a/core/src/main/scala/stainless/verification/VerificationChecker.scala b/core/src/main/scala/stainless/verification/VerificationChecker.scala index ca1fc6d879..3196e05984 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 95d93b9d35..858b67afc8 100644 --- a/core/src/main/scala/stainless/verification/VerificationConditions.scala +++ b/core/src/main/scala/stainless/verification/VerificationConditions.scala @@ -41,7 +41,8 @@ object VCKind { case object InvariantSat extends VCKind("invariant satisfiability", "inv. sat") case class AssertErr(err: String) extends VCKind("body assertion: " + err, "assert.") 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) + } + +}