WIP: Fix model checking of inlined adt invariant

Author: romac

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)
   }
 }

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)))

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 =>

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 =>

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)
+  }
+
+}