Add kani test and remove TODO #2393
Merged
Conversation
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
Add a kani test to check `div_rem`.
Pull Request Test Coverage Report for Build 7623004415
💛 - Coveralls |
|
I"m a bit rusty on |
Kixunil
approved these changes
Jan 23, 2024
| let _ = x.mul_u64(y); | ||
| } | ||
|
|
||
| #[kani::unwind(5)] // I can't remember exactly why we need this. |
There was a problem hiding this comment.
I believe the code uses a loop of length 5 somewhere (or more likely 4).
apoelstra
approved these changes
Jan 23, 2024
|
This fails right now because we have a Do we want to modify the test or what? |
|
I just clobbered it, onwards and upwards. |
|
That does mean we have lost the |
apoelstra
added a commit
that referenced
this pull request
Feb 6, 2024
343510d kani: fix Amount overflow test (Andrew Poelstra) Pull request description: Our Kani CI job is currently failing. See https://github.com/rust-bitcoin/rust-bitcoin/actions/runs/7770495422/job/21190756253 This fixes one of the issues; the other is that we're hitting a multiplication assertion in the test we added in #2393 which I'm unsure how to deal with. For reference, testing this was a bit of a PITA. I needed to ``` # Ok, these steps are easy/obvious cargo install kani-verifier cargo kani ``` This will give you an error located in core/panic.rs or something with the description `This is a placeholder message; Kani doesn't support message formatted at runtime` which is not super helpful. To get the actual failure, you need to write ``` cargo kani --enable-unstable --concrete-playback=inplace ``` which will add a weird unit test which calls into Kani to exercise the original test with a specific input value. Because it calls into Kani you can't just run it with `cargo test`. You need to run ``` RUST_BACKTRACE=1 CARGO_INCREMENTAL=0 cargo kani playback -Z concrete-playback -- kani_concrete_playback_check_div_rem_8626518785677487871 ``` where `CARGO_INCREMENTAL=0` disables incremental compilation (this was causing rustc to flame out with a "filename too long" error because it was trying to create some intermediate file with multiple hashes and crate names in it), and the `kani_concrete_playback_123456789` thing is the name of the test that gets added (which you can easily find by reading `git diff`). ACKs for top commit: tcharding: ACK 343510d Kixunil: ACK 343510d Tree-SHA512: 398ce3c61ffa3246bd27ae5719b4ac4fda587e87b8645ec8418fdfd039e4ed78d58233faab27bc63df7e2a30bb5467660e77a6e3d3a08fe86e7ff3dd31869ec7
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.
Add a kani test to check
div_rem.