Repository navigation
test(kani): cover short frames in ethernet from_bytes harnesses - #6367
Open
feliperodri wants to merge 1 commit into
Open
feliperodri wants to merge 1 commit into
feliperodri wants to merge 1 commit into
Conversation
verify_from_bytes and verify_from_bytes_unchecked built their input as a MAX_FRAME_SIZE array, so the frame length was always 1514 bytes despite the "up to MAX_FRAME_SIZE" comment. The branch for frames shorter than the Ethernet header (from_bytes returning an error, and from_bytes_unchecked producing an invalid frame) was never reached: kani::cover!(slice_length < PAYLOAD_OFFSET) is UNSATISFIABLE on main. Take a nondeterministic prefix of the buffer with kani::slice::any_slice_of_array_mut, so the harnesses check every length from 0 to MAX_FRAME_SIZE, and add covers showing that both the short and the valid frame paths are reached. Signed-off-by: Felipe Monteiro <[email protected]>
marco-marangoni
approved these changes
Nov 2, 2026
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
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.
Changes
verify_from_bytesandverify_from_bytes_uncheckednow take a nondeterministic prefix of theMAX_FRAME_SIZEbuffer (kani::slice::any_slice_of_array_mut), so they check every frame length from 0 to 1514 bytes, and they gainkani::cover!s for the short-frame and valid-frame paths.Reason
Both harnesses built their input as
[u8; MAX_FRAME_SIZE]and passed the whole array, so the length was always 1514 despite the "up to MAX_FRAME_SIZE" comment. The path for frames shorter than the Ethernet header (from_bytesreturning an error,from_bytes_uncheckedproducing an invalid frame) was never reached. Onmain, addingkani::cover!(slice_length < PAYLOAD_OFFSET, "short frame")toverify_from_bytesgives:With this change, with the flags from
tests/integration_tests/test_kani.py(-Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable), on Kani 0.68.0:The other ethernet harnesses also use a fixed-length buffer, but they assume or unwrap a valid frame, so a variable length would need extra assumptions; this PR leaves them unchanged.
License Acceptance
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. For more information on following Developer Certificate of Origin and signing off your commits, please check
CONTRIBUTING.md.PR Checklist
tools/devtool checkbuild --allto verify that the PR passesbuild checks on all supported architectures. (Not run: harness-only change under
#[cfg(kani)]; verified withcargo kanion x86_64.)tools/devtool checkstyle --no-clippyto verify that the PRpasses the automated style checks. (Not run;
rustfmt --checkwith the repository'srustfmt.tomlpasses on the changed file.)how they are solving the problem in a clear and encompassing way.
in the PR.
CHANGELOG.md. (No user-facing changes.)Runbook for Firecracker API changes. (No API changes.)
integration tests. (The changed harnesses run in
test_kani.py.)TODO. (No newTODOs.)rust-vmm.