Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix model checking of inlined ADT invariant #780

Draft
wants to merge 1 commit into
base: scala-2
Choose a base branch
from

Conversation

romac
Copy link
Member

@romac romac commented Jun 10, 2020

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.

@romac romac force-pushed the romac/check-model-inline-invariant-fix branch from 530d850 to 6e08d3b Compare June 11, 2020 19:11
@vkuncak
Copy link
Collaborator

vkuncak commented Jul 31, 2020

Should maybe counterexample validation be done on less transformed trees? How early in the pipeline does this make sense?

@romac romac force-pushed the romac/check-model-inline-invariant-fix branch from 6e08d3b to 589c8d6 Compare March 4, 2021 10:37
@vkuncak
Copy link
Collaborator

vkuncak commented Nov 8, 2023

@mario-bucev this does not appear to be an issue any more. Why did we need inlineInvariant to start with?

@mario-bucev
Copy link
Collaborator

This issue is still here, but --check-models needs to be passed

@romac
Copy link
Member Author

romac commented Nov 8, 2023

Why did we need inlineInvariant to start with?

#741 (comment)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants