Towards stubbing stabilization#4566
Open
feliperodri wants to merge 9 commits intomodel-checking:mainfrom
Open
Conversation
Print stubs applied to each harness in verification output (model-checking#2119): When a harness uses #[kani::stub] or #[kani::stub_verified], the stub mappings are now printed before verification begins, e.g.: Checking harness my_harness... - Stub: original_fn -> replacement_fn This makes the assumptions introduced by stubbing visible to users. Split stubbing tests into individual harnesses (model-checking#1861): Four test files had multiple stub scenarios bundled into a single harness (a workaround from when stubbing only supported one harness). Split each into separate harnesses with descriptive names: - public_function.rs: check_local_fn_stub, check_pub_fn_in_module_stub - struct_method.rs: check_pub_method_stub, check_priv_method_via_delegation - enum_method.rs: check_enum_pub_method_stub, check_enum_priv_method_via_delegation - method_generic_type.rs: check_generic_type_pub_method_stub, check_generic_type_priv_method_via_delegation Also removed the --harness main flag since multiple harnesses now run. Documentation audit (stubbing.md): - Add 'Stub visibility in verification output' section with example - Add 'Trait method stubbing' limitation section explaining that <Type as Trait>::method syntax is not supported - Improve limitations section organization Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
…#2664) ExternFnStubPass::transform previously allocated a MutableBody copy for every function body, even when no stubs applied. This caused unnecessary memory duplication across the entire codebase. Apply the COW (Copy-On-Write) pattern: scan the body for references to stubbed functions first, and only allocate a mutable copy if at least one stub target is found. Functions with no stub references return the original body unchanged with zero allocation overhead. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Error message quality pass:
- Trait bounds error in stubs.rs: remove raw 'Callee:' debug info,
fix inconsistent whitespace, add actionable guidance ('All trait
bounds of the stub must be satisfied by the original's call sites').
- No-body error in attributes.rs: explain the likely cause ('This
typically means a trait method without a default implementation').
Feature interaction documentation (stubbing.md):
- Add 'Feature interactions' section documenting how stubbing works
with function contracts, loop contracts, and concrete playback.
- Remove outdated note claiming concrete playback is incompatible
with stubbing — verified that it works correctly (Kani generates
concrete test cases for failing stubbed harnesses).
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
github-actions
bot
added
Z-EndToEndBenchCI
COW pre-scan completeness (stubs.rs): Replace ad-hoc locals+terminators scan with a proper StubScanner that implements MirVisitor and checks all constant operands. This correctly handles function pointers in non-call positions (e.g., storing a function pointer in a variable) that the previous scan could miss. Thread-index prefix for stub output (harness_runner.rs): Prefix stub print lines with 'Thread N:' when running in multi-threaded mode (-j N) to prevent ambiguous interleaved output. Split remaining cargo-kani tests (model-checking#1861): Three cargo-kani test files still had the model-checking#1861 TODO with bundled harnesses. Split each into individual harnesses: - stubbing-public-foreign-function: 2 harnesses - stubbing-private-foreign-function: 2 harnesses - stubbing-foreign-method: 3 harnesses Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
On Linux (x86_64), stubbing libc functions and assigning them to
function pointers causes a GOTO codegen panic: CInteger(Int) vs
Signedbv{32} type mismatch. These are the same underlying type but
have different CBMC representations when the original is a C extern
function and the stub is a Rust function.
This is a pre-existing bug that passes on macOS but fails on Linux CI.
Rename to fixme_foreign_functions.rs so it is skipped in CI while
documenting the issue for future investigation.
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Two UI tests checked for the old error message strings: - resolution_errors.expected: update 'does not have a body, but is not an extern function' to the new message explaining it typically means a trait method without a default implementation. - stubbing-trait-validation/expected: update trait bounds error from 'doesn't implement X. The function Y cannot be stubbed by Z due to generic bounds not being met' to the new format 'type X doesn't implement trait Y, so Z cannot be stubbed by W. All trait bounds of the stub must be satisfied by the original's call sites.' Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
The harness split in this PR replaced the single 'main' proof harness with multiple individually-named harnesses. However, the expected output files were still named 'main.expected', causing compiletest to pass '--harness main' which fails with E0601 since no 'main' function exists. Renaming to 'expected' (no extension) skips the --harness flag entirely, allowing all harnesses in the crate to run.
feliperodri
force-pushed
the
fix-stubbing-issues
branch
from
9838cab to
053e177
Compare
…ssage The error message for trait bound mismatches was improved in this PR but the cargo-ui/function-stubbing-trait-mismatch expected file was not updated to match the new format.
The type mismatch bug (CInteger(Int) vs Signedbv{32}) that caused this
test to fail on Linux has been resolved by the FFI stubbing fixes in
this PR. The test now passes on both macOS and Linux, so it no longer
needs to be marked as fixme.
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
1 participant
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.
Improves trust, maintainability, performance, documentation, and error messages.
Resolves #2119
Resolves #1861
Resolves #2664
Changes
Print exercised stubs in verification output (#2119)
When a harness uses
#[kani::stub]or#[kani::stub_verified], the stub mappings are now printed before verification begins:This makes the assumptions introduced by stubbing visible to users, improving trust in verification results.
Split tests into individual harnesses (#1861)
Four test files bundled multiple stub scenarios into a single harness (a workaround from when stubbing only supported one harness at a time). Split each into separate harnesses with descriptive names:
check_local_fn_stub,check_pub_fn_in_module_stubcheck_pub_method_stub,check_priv_method_via_delegationcheck_enum_pub_method_stub,check_enum_priv_method_via_delegationcheck_generic_type_pub_method_stub,check_generic_type_priv_method_via_delegationRemoved the
--harnessmain flag since multiple harnesses now run.Avoid unnecessary body allocation in
ExternFnStubPass(#2664)ExternFnStubPass::transformpreviously allocated aMutableBodycopy for every function body, even when no stubs applied. Apply the COW (Copy-On-Write) pattern: scan the body for references to stubbed functions first, and only allocate a mutable copy if at least one stub target is found.Error message quality pass
Documentation audit (stubbing.md)
stub_verified), loop contracts, and concrete playbackBy submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.