-
Notifications
You must be signed in to change notification settings - Fork 3.7k
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
[move-prover][cli] Add benchmark functionality #15636
Merged
Merged
+360
−1,780
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
wrwg
requested review from
gregnazario,
banool,
davidiw and
movekevin
as code owners
December 19, 2024 03:12
⏱️ 8h 23m total CI duration on this PR
🚨 1 job on the last run was significantly faster/slower than expected
|
rahxephon89
approved these changes
Dec 19, 2024
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, thanks!
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
vineethk
approved these changes
Dec 19, 2024
wrwg
force-pushed
the
wrwg/benchmark
branch
2 times, most recently
from
December 19, 2024 16:19
50c4149
to
79021d9
Compare
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
… can be in the form `mod::func` or just `func`. This connects the CLI to the existing VerificationScope option of the Move Prover.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
❌ Forge suite
|
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
✅ Forge suite
|
✅ Forge suite
|
georgemitenkov
pushed a commit
that referenced
this pull request
Jan 6, 2025
This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time. The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`. The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605: - Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug` - Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>` - Adds an option `--skip-instance-check` to completely turn off verification of type instantiations. - Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long and confusing when trying to understand what functions are verified
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
This adds a new option
aptos move prove --benchmark
which lets verification run in the benchmark framework of themove-prover/lab
tool. This tool verifies function by function and detects timeouts as well as measure verification time.The result of the benchmark will be stored in
<move-package>/prover_benchmark.fun_data
. A graphic representation will be stored as well inprover_benchmark.svg
.The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:
move prove -v debug
f<#1, #2>
andf<#2, #1>
--skip-instance-check
to completely turn off verification of type instantiations.How Has This Been Tested?
Existing tests for not breaking something, and manually for the new feature