Reuse prebuilt KMIR definition to avoid redundant llvm-kompile processes#1069
Merged
Reuse prebuilt KMIR definition to avoid redundant llvm-kompile processes#1069
llvm-kompile processes#1069Conversation
`test_verify_rust_std` has multiple harnesses in the one file. Instead of reducing / kompiling for each harness, reduce once for the set of start symbols and kompile once for the file. This means that kompilation is pushed earlier in the pipeline into the test runner. Performance increase for challenge 11 has been observed at approx 3x.
Fixture is left as it provides fast fail if the defintion cannot be built
Stevengre
reviewed
Apr 20, 2026
| kmir: KMIR, | ||
| smir_info: SMIRInfo, | ||
| opts: ProveOpts, | ||
| ) -> APRProof: |
Contributor
There was a problem hiding this comment.
Thank you! I think it's really a good idea. But I see some redundant lines of code here compared to _prove. What do you think to make kmir as a ProveOpts so that we can separate the proof prepare and proof run process?
Collaborator
Author
There was a problem hiding this comment.
There is some duplication, and I did consider merging them. In the end prove is changed in the stacked PR #1071 . I would be open to discussing the design and improvements in the context of that PR.
mariaKt
approved these changes
Apr 20, 2026
Collaborator
mariaKt
left a comment
mariaKt
left a comment
There was a problem hiding this comment.
LGTM, especially since there is further refactoring to address the duplication issues.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
If a Rust file contains multiple targets to prove (e.g. verify-rust-std challenge 11) then multiple
llvm-kompileprocesses will be invoked by _prove. This PR pushes this process earlier to create a KMIR definition with all the required start symbols so thatllvm-kompileis called once per file.In particular:
test_verify_rust_stdnow compiles a prebuilt KMIR definition with reduced start symbols. This definition is reused for all proof harnesses in a file;prove_with_kmiris added as separate control-flow toprove. This may not be elegant, but right now I think it is the clearest separation, and I was hesitant to add flags or refactor too aggressively;Results from verify-std-rust challenge 11:
llvm-kompile/ start-symbol = 138llvm-kompileinvocationsllvm-kompile/ file = 16llvm-kompileinvocationsDetails
PRIOR:
real 31m16.872s
user 170m18.245s
sys 5m51.240s
real 31m36.755s
user 175m15.830s
sys 6m32.859s
AFTER:
real 10m20.730s
user 44m10.271s
sys 2m15.364s
real 10m58s
user 47m0s
sys 2m24s
real 10m40.395s
user 45m54.822s
sys 2m20.399s
real 10m38.370s
user 45m32.886s
sys 2m19.782s