-
Notifications
You must be signed in to change notification settings - Fork 121
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
Add autogenerated Bolero harnesses #2306
Conversation
|(mut callee, count, _value): (EncoderLenEstimator, usize, u8)| { | ||
Some(callee.write_repeated(count, _value)) | ||
}, |
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.
I guess you're pulling the variable names from the function declaration but I wonder if we could automatically remove the _
prefix? Not a huge deal, just a minor nit.
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.
Also I'm assuming this panics when callee.len + count
exceeds usize::MAX
. With our current implementation, the Encoder impls are expected to panic on extreme values, since they don't return Result
anywhere. Not sure what's the best way to capture that - do we filter out inputs in the harness that we expect to panic?
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.
Not exactly sure how to filter out the inputs. The code below still errors out with the input:
Input:
(
EncoderLenEstimator {
capacity: 0,
len: 9151314442816847872,
},
9295429630892703744,
0,
)1
which I figured would be filtered by the harness.
#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_29_write_repeated() {
bolero::check!().with_type().cloned().for_each(
|(mut callee, count, value): (EncoderLenEstimator, usize, u8)| {
if callee.len + count > usize::MAX {
None
} else {
Some(callee.write_repeated(count, value))
}
},
);
}
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.
Returning None
from for_each
will result in the harness failing. You need to use filter instead.
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.
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.
you'd need to use the tuple, rather than separate arguments (similar to for_each
)
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.
Tried to add a filter like this:
fn encoder_len_estimator_write_repeated() {
bolero::check!()
.with_type()
.cloned()
.filter(|(callee, count, _): &(EncoderLenEstimator, usize, u8)| {
(callee.len + count) < usize::MAX
})
.for_each(
|(mut callee, count, value): (EncoderLenEstimator, usize, u8)| {
Some(callee.write_repeated(count, value))
},
);
}
I still get an error in this test but now bolero isn't giving an input that causes the error. Instead I get this:
---- encoder::estimator::tests::encoder_len_estimator_write_repeated stdout ----
thread 'encoder::estimator::tests::encoder_len_estimator_write_repeated' panicked at 'attempt to add with overflow', /rustc/eb26296b556cef10fb713a38f3d16b9886080f26/library/core/src/ops/arith.rs:109:1
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
failures:
encoder::estimator::tests::encoder_len_estimator_write_repeated
test result: FAILED. 79 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 7.01s
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.
Oh that filter fails because it overflows in the filter check... This filter should get around that:
filter(|(callee, count, _): &(EncoderLenEstimator, usize, u8)| {
count <= &(usize::MAX - callee.len)
})
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.
Looks great! Thanks for making those changes
Description of changes:
Adds 58 Bolero harnesses and all necessary
TypeGenerator
derivations. These harnesses were automatically generated by a tool currently under development by the Kani team.Summary of running
cargo test
listed below.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.