From 530d85057da2930bed958248885c4c605766ba8c Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 5 Jun 2020 13:59:21 +0200 Subject: [PATCH] WIP: Fix model checking of inlined adt invariant --- .../verification/DefaultTactic.scala | 2 +- .../stainless/verification/TypeChecker.scala | 6 ++--- .../verification/VerificationChecker.scala | 27 +++++++++++++------ .../verification/VerificationConditions.scala | 2 +- inline-invariant.scala | 23 ++++++++++++++++ 5 files changed, 47 insertions(+), 13 deletions(-) create mode 100644 inline-invariant.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 8b5a50de2c..df67c854a0 100644 --- a/core/src/main/scala/stainless/verification/TypeChecker.scala +++ b/core/src/main/scala/stainless/verification/TypeChecker.scala @@ -795,7 +795,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)) @@ -834,10 +834,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..64047157d0 100644 --- a/core/src/main/scala/stainless/verification/VerificationChecker.scala +++ b/core/src/main/scala/stainless/verification/VerificationChecker.scala @@ -144,13 +144,9 @@ 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, expr: 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) - } - def success: VCStatus = { reporter.debug("- Model validated.") VCStatus.Invalid(VCStatus.CounterExample(model)) @@ -161,6 +157,21 @@ trait VerificationChecker { self => VCStatus.Unknown } + val pcCond = collectWithPC(expr) { + case (inv @ FunctionInvocation(`invId`, _, Seq(adt: ADT)), path) => (inv, adt, path) + } + + if (pcCond.isEmpty) { + return evaluator.eval(expr, model) match { + case Successful(BooleanLiteral(false)) => success + case Successful(_) => failure("- Invalid model.") + case RuntimeError(msg) => failure(s"- Model leads to runtime error: $msg") + case EvaluatorError(msg) => failure(s"- Model leads to evaluation error: $msg") + } + } + + val Seq((inv, adt, path)) = pcCond + 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 +195,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), expr) evaluator.eval(newCondition, newModel) match { case Successful(BooleanLiteral(false)) => success @@ -252,8 +263,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) = vc.kind + val status = checkAdtInvariantModel(vc, invId, expr.asInstanceOf[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 3ce176f821..f61ac0464d 100644 --- a/core/src/main/scala/stainless/verification/VerificationConditions.scala +++ b/core/src/main/scala/stainless/verification/VerificationConditions.scala @@ -40,7 +40,7 @@ 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: Any) extends VCKind("adt invariant", "adt inv.") def fromErr(optErr: Option[String]) = { optErr.map { err => diff --git a/inline-invariant.scala b/inline-invariant.scala new file mode 100644 index 0000000000..30aa8ad224 --- /dev/null +++ b/inline-invariant.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) + } + +}