Skip to content

Fix SMT interaction in Booster #3987

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 8 commits into from
Jul 18, 2024
Merged

Fix SMT interaction in Booster #3987

merged 8 commits into from
Jul 18, 2024

Conversation

geo2a
Copy link
Contributor

@geo2a geo2a commented Jul 17, 2024 •
edited
Loading

  • do not proceed if the ground truth is not SAT:
    • trigger retry on Unknown and log the predicates with context `[smt][detail]
    • fail hard on Unsat
  • post-process the validity check result to eliminate Unknowns where possible
  • remove duplicate log message

@geo2a
Copy link
Contributor Author

geo2a commented Jul 18, 2024

No substantial difference in KEVM performance:

Test georgy-booster-smt-changes time master-5fdd57a75 time (georgy-booster-smt-changes/master-5fdd57a75) time
mcd/flopper-dent-guy-same-pass-rough-spec.k 826.04 861.3 0.9590618831998142
mcd/functional-spec.k 589.87 568.68 1.0372617289160864
mcd/vow-fess-fail-rough-spec.k 124.51 114.3 1.089326334208224
TOTAL 1540.4199999999998 1544.28 0.9975004532856735

@geo2a geo2a marked this pull request as ready for review July 18, 2024 07:11
@geo2a geo2a force-pushed the georgy/booster-smt-changes branch from 517dd73 to 8ab9ad4 Compare July 18, 2024 12:10
jberthold
jberthold approved these changes Jul 18, 2024
View reviewed changes
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Two small suggestions about the logging

booster/library/Booster/SMT/Interface.hs
Unknown -> do
Log.getPrettyModifiers >>= \case
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
Log.withContext Log.CtxDetail
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe log in the context that these conditions actually cause an "Abort"?

Suggested change
Log.withContext Log.CtxDetail
Log.withContext Log.CtxAbort
$ Log.withContext Log.CtxDetail

github-actions and others added 2 commits July 18, 2024 14:12
@geo2a geo2a merged commit 1103673 into master Jul 18, 2024
6 checks passed
@geo2a geo2a deleted the georgy/booster-smt-changes branch July 18, 2024 15:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jberthold jberthold jberthold approved these changes

@goodlyrottenapple goodlyrottenapple Awaiting requested review from goodlyrottenapple

Assignees
No one assigned
Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@geo2a @jberthold