Fix model checking of inlined adt invariant

epfl-lara · Mar 4, 2021 · 589c8d6 · 589c8d6
1 parent cf69de0
commit 589c8d6
Show file tree

Hide file tree

Showing 5 changed files with 39 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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)
+  }
+
+}