stainless
stainless copied to clipboard
Published
20 hours ago •
epfl-lara
epfl-lara
Fix model checking of inlined ADT invariant
Running Stainless on this benchmark:
import stainless.lang._
import stainless.annotation._
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)
}
yields:
$ sbt stainless-scalac/run --debug=verification --check-models=true --type-checker=true ../../inv.scala
[info] [ Debug ] Generating VCs for those functions: inv$7, inv$8, bad$0, ok$0
[info] [ Debug ] Checking Verification Conditions...
[info] [ Info ] - Now solving 'body assertion' VC for bad @13:3...
[info] [ Debug ] inv(Foo(5))
[info] [ Debug ] Solving with: U:smt-z3
[info] [Warning ] - Model leads to runtime error: ADT invariant violation for Foo(5)
[info] [ Error ] Something went wrong. The model should have been valid, yet we got this:
[info] [ Error ] (Empty model)
[info] [ Error ] for formula ¬inv(Foo(5))
[info] [ Info ] - Result for 'body assertion' VC for bad @13:3:
[info] [Warning ] => UNKNOWN
[info] [ Info ] - Now solving 'body assertion' VC for ok @17:3...
[info] [ Debug ] inv(Foo(15))
[info] [ Debug ] Solving with: U:smt-z3
[info] [ Info ] - Result for 'body assertion' VC for ok @17:3:
[info] [ Info ] => VALID
[info] [ Info ] - Now solving 'precond. (call inv(@unchecked { assert(thiss is Fo...)' VC for inv @10:13...
[info] [ Debug ] true
[info] [ Debug ] Solving with: U:smt-z3
[info] [ Info ] - Result for 'precond. (call inv(@unchecked { assert(thiss is Fo...)' VC for inv @10:13:
[info] [ Info ] => VALID
[info] [ Info ] ┌───────────────────┐
[info] [ Info ] ╔═╡ stainless summary ╞══════════════════════════════════════════════════════════════════════════════════════════╗
[info] [ Info ] ║ └───────────────────┘ ║
[info] [ Info ] ║ bad body assertion unknown U:smt-z3 ../../inv.scala:13:3 0.235 ║
[info] [ Info ] ║ inv precond. (call inv(@unchecked { assert(thiss is Fo...) valid U:smt-z3 ../../inv.scala:10:13 0.017 ║
[info] [ Info ] ║ ok body assertion valid U:smt-z3 ../../inv.scala:17:3 0.023 ║
[info] [ Info ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[info] [ Info ] ║ total: 3 valid: 2 (0 from cache) invalid: 0 unknown: 1 time: 0.275 ║
[info] [ Info ] ╚════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
Notice that what should be adt invariant VCs are just body assertions.
With this fix, Stainless then generates the right VC kinds, but then fails again during model checking with:
[info] [ Info ] - Now solving 'adt invariant' VC for bad @14:5...
[info] [ Debug ] inv(Foo(5))
[info] [ Debug ] Solving with: U:smt-z3
[info] [ Error ] Stainless terminated with an error.
[info] [ Error ] Debug output is available in the file `stainless-debug.txt`, you may report your issue on https://github.com/epfl-lara/stainless/issues
[info] [ Error ] scala.MatchError: List() (of class scala.collection.immutable.Nil$)
[info] [ Error ] at stainless.verification.VerificationChecker.checkAdtInvariantModel(VerificationChecker.scala:150)
[info] [ Error ] at stainless.verification.VerificationChecker.checkAdtInvariantModel$(VerificationChecker.scala:147)
[info] [ Error ] at stainless.verification.VerificationChecker$Checker$1.checkAdtInvariantModel(VerificationChecker.scala:336)
[info] [ Error ] at stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:256)
[info] [ Error ] at stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:214)
[info] [ Error ] at stainless.verification.VerificationChecker$Checker$1.checkVC(VerificationChecker.scala:336)
[info] [ Error ] at stainless.verification.VerificationChecker.$anonfun$checkVCs$2(VerificationChecker.scala:107)
[info] [ Error ] at scala.concurrent.Future$.$anonfun$traverse$1(Future.scala:850)
[info] [ Error ] at scala.collection.TraversableOnce.$anonfun$foldLeft$1(TraversableOnce.scala:160)
[info] [ Error ] at scala.collection.TraversableOnce.$anonfun$foldLeft$1$adapted(TraversableOnce.scala:160)
[info] [ Error ] at scala.collection.Iterator.foreach(Iterator.scala:941)
[info] [ Error ] at scala.collection.Iterator.foreach$(Iterator.scala:941)
[info] [ Error ] at scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[info] [ Error ] at scala.collection.IterableLike.foreach(IterableLike.scala:74)
[info] [ Error ] at scala.collection.IterableLike.foreach$(IterableLike.scala:73)
[info] [ Error ] at scala.collection.AbstractIterable.foreach(Iterable.scala:56)
[info] [ Error ] at scala.collection.TraversableOnce.foldLeft(TraversableOnce.scala:160)
[info] [ Error ] at scala.collection.TraversableOnce.foldLeft$(TraversableOnce.scala:158)
[info] [ Error ] at scala.collection.AbstractTraversable.foldLeft(Traversable.scala:108)
[info] [ Error ] at scala.concurrent.Future$.traverse(Future.scala:850)
[info] [ Error ] at stainless.verification.VerificationChecker.checkVCs(VerificationChecker.scala:97)
[info] [ Error ] at stainless.verification.VerificationChecker.checkVCs$(VerificationChecker.scala:90)
[info] [ Error ] at stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:336)
[info] [ Error ] at stainless.verification.VerificationChecker.verify(VerificationChecker.scala:81)
[info] [ Error ] at stainless.verification.VerificationChecker.verify$(VerificationChecker.scala:77)
[info] [ Error ] at stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:336)
[info] [ Error ] at stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:350)
[info] [ Error ] at stainless.verification.VerificationRun.execute(VerificationComponent.scala:111)
[info] [ Error ] at stainless.verification.VerificationRun.execute(VerificationComponent.scala:44)
[info] [ Error ] at stainless.ComponentRun.apply(Component.scala:103)
[info] [ Error ] at stainless.ComponentRun.apply$(Component.scala:97)
[info] [ Error ] at stainless.verification.VerificationRun.apply(VerificationComponent.scala:44)
[info] [ Error ] at stainless.frontend.BatchedCallBack.$anonfun$endExtractions$15(BatchedCallBack.scala:97)
[info] [ Error ] at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[info] [ Error ] at scala.collection.immutable.List.foreach(List.scala:392)
[info] [ Error ] at scala.collection.TraversableLike.map(TraversableLike.scala:238)
[info] [ Error ] at scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[info] [ Error ] at scala.collection.immutable.List.map(List.scala:298)
[info] [ Error ] at stainless.frontend.BatchedCallBack.endExtractions(BatchedCallBack.scala:95)
[info] [ Error ] at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:38)
[info] [ Error ] at java.lang.Thread.run(Thread.java:748)
[info] [ Error ]
[error] Nonzero exit code returned from runner: 2
Because the original invariant (inv$8) has been inlined, resulting in inv$7(Foo$0(5)), we cannot find a call for it in order to pull Foo$0(5) out from the VC and into the model to avoid the evaluator choking when evaluating the original invariant on Foo$0(5). Symbols below:
[info] [ Debug ] -------------Functions-------------
[info] [ Debug ] @derived(inv$7)
[info] [ Debug ] @inlineInvariant
[info] [ Debug ] def inv$8(thiss$2: Toto$0): Boolean = inv$7(@unchecked {
[info] [ Debug ] assert(thiss$2 is Foo$0, "Cast error")
[info] [ Debug ] thiss$2
[info] [ Debug ] })
[info] [ Debug ]
[info] [ Debug ] def bad$0: Toto$0 = Foo$0(5)
[info] [ Debug ]
[info] [ Debug ] def inv$7(thiss$1: Toto$0): Boolean = {
[info] [ Debug ] require(thiss$1 is Foo$0)
[info] [ Debug ] thiss$1.x$107 > 10
[info] [ Debug ] }
[info] [ Debug ]
[info] [ Debug ] def ok$0: Toto$0 = Foo$0(15)
[info] [ Debug ]
[info] [ Debug ] -------------Sorts-------------
[info] [ Debug ] @inlineInvariant
[info] [ Debug ] @invariant(inv$8)
[info] [ Debug ] abstract class Toto$0
[info] [ Debug ] case class Foo$0(x$107: BigInt) extends Toto$0
To fix that, this PR stores the original, non inlined, ADT invariant within the VCKind itself, so that we can work with the original invariant instead of the inlined one. This should be fine for model checking since there should be no semantic differences between evaluating either invariants (original or inlined).
This is all very hacky, and I would be happy hear other suggestions as to how to solve this issue.
Should maybe counterexample validation be done on less transformed trees? How early in the pipeline does this make sense?
@mario-bucev this does not appear to be an issue any more. Why did we need inlineInvariant to start with?
Why did we need inlineInvariant to start with?
https://github.com/epfl-lara/stainless/pull/741#issuecomment-588914059