Use generated exprs to test expression evaluation against smt solver#499
Use generated exprs to test expression evaluation against smt solver#499
Conversation
| val t = timeoutSec match { | ||
| case Some(n) => Seq(s"-T:$n") | ||
| case _ => Seq() | ||
| } | ||
| val softT = softTimeoutMillis match { | ||
| case Some(n) => Seq(s"-t:$n") | ||
| case None => Seq() | ||
| } |
There was a problem hiding this comment.
use .map. Options can be ++-ed onto a sequence and they act like a sequence of zero or one items.
| def genExpr(size: Option[Int] = None, depthLimit: Int = 10): Gen[Expr] = | ||
| if (size.exists(_ <= 1) || depthLimit <= 0) then genValue(size) | ||
| else Gen.oneOf(genBinExp(size, depthLimit - 1), genUnExp(size), genValue(size)) | ||
|
|
||
| def genNonLiteralExpr(size: Option[Int] = None, depthLimit: Int = 3): Gen[Expr] = | ||
| if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size, depthLimit), genUnExp(size)) |
There was a problem hiding this comment.
ik it's not new in this pr, but what is this condition on size.exists(_ <= 1)? so, if size is negative or 0, it'll get passed to genValue? this seems wrong
There was a problem hiding this comment.
Its ugly but its because you can reliably generate width 1 bitvectors but the other options need more careful consideration as they sometimes try and partition it down further, e.g. bvconcat. I just didnt bother dealing with each possible leaf needed for the other cases. note size is option
|
I don't think theres a way to reliably generate expressions that its possible for Z3 to always verify within a timeframe, maybe I just let timeouts silently pass the test (maybe there's a way to ask scalacheck to generate more checks in that case to make sure there's a certain number of positive examples?). I don't think we should merge as is since it will lead to unreliable failures from timeouts. |
|
@katrinafyi I guess we can just mark this as disabled and merge so we can run manually? Its a somewhat useful test to have but probably too flaky. |
|
That makes sense. Should the scalacheck cases be in a different test suite so that the existing genSMT can still run? |
|
Yeah |
3 participants
Reuses the scalacheck-based expr generator to test the interpreter against z3 with more complex expressions:
@b-paul
This test tends to time out when it generates difficult expressions, maybe z3's simplify tactic would be more appropriate than just an assertion.