Skip to content

Commit 2aa6306

Browse files
Merge pull request #63 from triblespace/codex/improve-system-robustness-with-testing
Wire fuzz harness into verify workflow
2 parents a8ea273 + 5d7857b commit 2aa6306

File tree

9 files changed

+231
-4
lines changed

9 files changed

+231
-4
lines changed

.gitignore

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,7 @@
11
.DS_Store
22
Cargo.lock
33
target/
4+
fuzz/artifacts/
5+
fuzz/corpus/
6+
fuzz/coverage/
7+
fuzz/target/

CHANGELOG.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
# Changelog
22

33
## Unreleased
4+
- added proptest coverage for prefix/suffix invariants and introduced a fuzz target for mutating `Bytes` operations
5+
- extended `verify.sh` to install cargo-fuzz and execute deterministic fuzz runs alongside Kani proofs
6+
- added Kani proofs ensuring `is_subslice` accepts only slices from the original allocation
47
- add Kani proof checking `Bytes::downcast_to_owner` for matching and mismatched owners
58
- added Kani verification harnesses for `Bytes::pop_front` and `Bytes::pop_back`
69
- avoid flushing empty memory maps in `Section::freeze` to prevent macOS errors

INVENTORY.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
## Desired Functionality
77
- Add Kani proofs for winnow view helpers.
88
- Add test covering freezing an empty section to guard against flush errors on macOS.
9+
- Explore how to model `ByteArea` for Kani or fuzzing without depending on OS-backed memory maps.
910

1011
## Discovered Issues
1112
- None at the moment.

README.md

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -175,10 +175,17 @@ Run `./scripts/preflight.sh` from the repository root before committing. The
175175
script formats the code and executes all tests using Python 3.12 for the `pyo3`
176176
feature.
177177

178-
Kani proofs are executed separately with `./scripts/verify.sh`, which should be
179-
run on a dedicated system. The script will install the Kani verifier
180-
automatically. Verification can take a long time and isn't needed for quick
181-
development iterations.
178+
Kani proofs and deterministic fuzz smoke tests are executed with
179+
`./scripts/verify.sh`, which should be run on a dedicated system. The script
180+
installs the Kani verifier, `cargo-fuzz`, and the nightly toolchain before
181+
running `cargo kani --workspace --all-features` followed by a bounded
182+
`cargo +nightly fuzz run`. Override the fuzz target or arguments by setting
183+
`FUZZ_TARGET` or `FUZZ_ARGS` in the environment. Verification can take a long
184+
time and isn't needed for quick development iterations.
185+
186+
For exploratory fuzzing use `cargo fuzz run bytes_mut_ops`. The fuzz target
187+
mirrors a simple vector model to ensure helpers like `take_prefix` and
188+
`pop_front` remain consistent when exercised by randomized sequences.
182189

183190
## Glossary
184191

fuzz/Cargo.toml

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
[package]
2+
name = "anybytes-fuzz"
3+
version = "0.0.0"
4+
edition = "2021"
5+
publish = false
6+
7+
[package.metadata]
8+
cargo-fuzz = true
9+
10+
[dependencies]
11+
libfuzzer-sys = "0.4"
12+
anybytes = { path = ".." }
13+
14+
[dev-dependencies]
15+
arbitrary = { version = "1", features = ["derive"] }
16+
17+
[[bin]]
18+
name = "bytes_mut_ops"
19+
path = "fuzz_targets/bytes_mut_ops.rs"
20+
test = false
21+
doc = false

fuzz/fuzz_targets/bytes_mut_ops.rs

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
#![no_main]
2+
3+
use anybytes::Bytes;
4+
use arbitrary::{Arbitrary, Result as ArbResult, Unstructured};
5+
use libfuzzer_sys::fuzz_target;
6+
7+
#[derive(Debug)]
8+
enum Operation {
9+
TakePrefix(u16),
10+
TakeSuffix(u16),
11+
PopFront,
12+
PopBack,
13+
}
14+
15+
impl<'a> Arbitrary<'a> for Operation {
16+
fn arbitrary(u: &mut Unstructured<'a>) -> ArbResult<Self> {
17+
let tag = u.int_in_range::<u8>(0..=3)?;
18+
let op = match tag {
19+
0 => Operation::TakePrefix(u.arbitrary()?),
20+
1 => Operation::TakeSuffix(u.arbitrary()?),
21+
2 => Operation::PopFront,
22+
_ => Operation::PopBack,
23+
};
24+
Ok(op)
25+
}
26+
}
27+
28+
#[derive(Debug)]
29+
struct FuzzCase {
30+
data: Vec<u8>,
31+
ops: Vec<Operation>,
32+
}
33+
34+
impl<'a> Arbitrary<'a> for FuzzCase {
35+
fn arbitrary(u: &mut Unstructured<'a>) -> ArbResult<Self> {
36+
let len = u.int_in_range::<usize>(0..=64)?;
37+
let mut data = Vec::with_capacity(len);
38+
for _ in 0..len {
39+
data.push(u.arbitrary()?);
40+
}
41+
42+
let ops_len = u.int_in_range::<usize>(0..=64)?;
43+
let mut ops = Vec::with_capacity(ops_len);
44+
for _ in 0..ops_len {
45+
ops.push(u.arbitrary()?);
46+
}
47+
48+
Ok(Self { data, ops })
49+
}
50+
}
51+
52+
fuzz_target!(|case: FuzzCase| {
53+
let mut bytes = Bytes::from(case.data.clone());
54+
let mut model = case.data;
55+
56+
for op in case.ops {
57+
match op {
58+
Operation::TakePrefix(n) => {
59+
let len = n as usize;
60+
let result = bytes.take_prefix(len);
61+
if len <= model.len() {
62+
let expected: Vec<u8> = model.drain(..len).collect();
63+
let prefix = result.expect("prefix should exist");
64+
assert_eq!(prefix.as_ref(), expected.as_slice());
65+
assert_eq!(bytes.as_ref(), model.as_slice());
66+
} else {
67+
assert!(result.is_none());
68+
assert_eq!(bytes.as_ref(), model.as_slice());
69+
}
70+
}
71+
Operation::TakeSuffix(n) => {
72+
let len = n as usize;
73+
let result = bytes.take_suffix(len);
74+
if len <= model.len() {
75+
let split = model.len() - len;
76+
let expected = model.split_off(split);
77+
let suffix = result.expect("suffix should exist");
78+
assert_eq!(suffix.as_ref(), expected.as_slice());
79+
assert_eq!(bytes.as_ref(), model.as_slice());
80+
} else {
81+
assert!(result.is_none());
82+
assert_eq!(bytes.as_ref(), model.as_slice());
83+
}
84+
}
85+
Operation::PopFront => {
86+
let expected = if model.is_empty() {
87+
None
88+
} else {
89+
Some(model.remove(0))
90+
};
91+
let got = bytes.pop_front();
92+
assert_eq!(got, expected);
93+
assert_eq!(bytes.as_ref(), model.as_slice());
94+
}
95+
Operation::PopBack => {
96+
let expected = model.pop();
97+
let got = bytes.pop_back();
98+
assert_eq!(got, expected);
99+
assert_eq!(bytes.as_ref(), model.as_slice());
100+
}
101+
}
102+
}
103+
});

scripts/verify.sh

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,26 @@ cargo install rustfmt || true
1111
# Install the Kani verifier as needed; this is also idempotent.
1212
cargo install --locked kani-verifier || true
1313

14+
# Install cargo-fuzz to run libFuzzer targets. This subcommand is optional
15+
# during development so we ignore installation failures here as well.
16+
cargo install cargo-fuzz || true
17+
18+
# Ensure the nightly toolchain is present for cargo-fuzz and required LLVM tools
19+
rustup toolchain install nightly || true
20+
rustup component add llvm-tools-preview --toolchain nightly || true
21+
1422
# Run all Kani proofs in the workspace
1523
cargo kani --workspace --all-features
1624

25+
# Execute fuzz targets with deterministic settings so verification stays
26+
# reproducible. The default run count can be overridden by setting FUZZ_ARGS.
27+
FUZZ_TARGET="${FUZZ_TARGET:-bytes_mut_ops}"
28+
FUZZ_ARG_STRING="${FUZZ_ARGS:-}"
29+
if [[ -n "$FUZZ_ARG_STRING" ]]; then
30+
IFS=' ' read -r -a FUZZ_ARG_ARRAY <<< "$FUZZ_ARG_STRING"
31+
else
32+
FUZZ_ARG_ARRAY=(-seed=1 -runs=50000)
33+
fi
34+
35+
cargo +nightly fuzz run "$FUZZ_TARGET" -- "${FUZZ_ARG_ARRAY[@]}"
36+

src/bytes.rs

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -718,4 +718,43 @@ mod verification {
718718
};
719719
assert_eq!(returned.as_ref(), data.as_slice());
720720
}
721+
722+
#[kani::proof]
723+
#[kani::unwind(16)]
724+
pub fn check_is_subslice_accepts_ranges() {
725+
let data: Vec<u8> = Vec::bounded_any::<16>();
726+
let bytes = Bytes::from_source(data.clone());
727+
728+
let start: usize = kani::any();
729+
let end: usize = kani::any();
730+
kani::assume(start <= end);
731+
kani::assume(end <= data.len());
732+
733+
let slice = &bytes.as_ref()[start..end];
734+
assert!(is_subslice(bytes.as_ref(), slice));
735+
}
736+
737+
#[kani::proof]
738+
#[kani::unwind(16)]
739+
pub fn check_is_subslice_rejects_disjoint_ranges() {
740+
let data: Vec<u8> = Vec::bounded_any::<16>();
741+
let other: Vec<u8> = Vec::bounded_any::<8>();
742+
743+
let base_len = data.len();
744+
kani::assume(base_len > 0);
745+
let base_ptr = data.as_ptr();
746+
747+
let other_len = other.len();
748+
kani::assume(other_len > 0);
749+
let other_ptr = other.as_ptr();
750+
751+
let base_start = base_ptr as usize;
752+
let base_end = base_start + base_len;
753+
let other_start = other_ptr as usize;
754+
let other_end = other_start + other_len;
755+
kani::assume(other_end <= base_start || other_start >= base_end);
756+
757+
let bytes = Bytes::from_source(data);
758+
assert!(!is_subslice(bytes.as_ref(), other.as_slice()));
759+
}
721760
}

src/tests.rs

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,35 @@ proptest! {
2626
prop_assert_eq!(&b[..], &a[..b.len()]);
2727
prop_assert!(b.is_empty() || a.as_ptr() == b.as_ptr());
2828
}
29+
30+
#[test]
31+
fn test_take_prefix_matches_split(data in proptest::collection::vec(any::<u8>(), 0..64)) {
32+
for len in 0..=data.len() {
33+
let mut bytes = Bytes::from(data.clone());
34+
let prefix = bytes.take_prefix(len).expect("prefix within bounds");
35+
prop_assert_eq!(prefix.as_ref(), &data[..len]);
36+
prop_assert_eq!(bytes.as_ref(), &data[len..]);
37+
}
38+
39+
let mut bytes = Bytes::from(data.clone());
40+
prop_assert!(bytes.take_prefix(data.len() + 1).is_none());
41+
prop_assert_eq!(bytes.as_ref(), data.as_slice());
42+
}
43+
44+
#[test]
45+
fn test_take_suffix_matches_split(data in proptest::collection::vec(any::<u8>(), 0..64)) {
46+
for len in 0..=data.len() {
47+
let mut bytes = Bytes::from(data.clone());
48+
let suffix = bytes.take_suffix(len).expect("suffix within bounds");
49+
let split = data.len() - len;
50+
prop_assert_eq!(suffix.as_ref(), &data[split..]);
51+
prop_assert_eq!(bytes.as_ref(), &data[..split]);
52+
}
53+
54+
let mut bytes = Bytes::from(data.clone());
55+
prop_assert!(bytes.take_suffix(data.len() + 1).is_none());
56+
prop_assert_eq!(bytes.as_ref(), data.as_slice());
57+
}
2958
}
3059

3160
#[test]

0 commit comments

Comments
 (0)