Elide vacuous pointer checks on contract-closure capture loads

[tautschnig]

Kani's function-contract instrumentation wraps every requires/ensures clause in a closure capturing the contracted function's arguments by reference. Evaluating a clause loads each captured argument through a reference that closure construction itself created from a live local of the enclosing frame - a load that cannot fail - yet CBMC's --pointer-check instruments each one with all six pointer-validity checks.

On contract-heavy code these vacuous checks dominate the reported property count: verifying ffi::c_str::verify::check_to_bytes from verify-rust-std with dependency contracts asserted (the default since #3802) produces 943 checks, of which 294 are pointer_dereference sextets on contract-closure capture loads. With this change the same harness reports 649 checks. Note that this is a report-noise and formula-size reduction, not a solve-time one: measured end-to-end verification time and peak memory on that harness are unchanged, as the solver discharged these locally-provable checks cheaply.

Suppress these checks by attaching CBMC's disable:pointer-check source-location pragma - the same mechanism backing kanitool::disable_checks, already used by the mem-init instrumentation - to exactly those statements whose every dereference is a direct load of a by-reference closure capture in a contract-clause closure. A local qualifies only if:

• the current instance is a closure taking its environment by value (contract closures are invoked in place; escaping closures, whose captures could outlive the frame, are called via reference-typed environments and remain fully checked);
• the innermost enclosing non-closure item carries a Kani contract (kanitool::checked_with); kanitool::is_contract_generated cannot be used due to #[kanitool::is_contract_generated] attribute is not detected #3921;
• the closure environment is never written to;
• the local is reference-typed, never address-taken, and its single assignment copies an environment field whose corresponding capture is a ByRef capture of an unprojected place.

The ByRef-capture condition matters for soundness: a by-value capture of reference type (e.g. a &mut argument moved into the closure, as in tests/expected/function-contract/mutable-references/return_mut_ref.rs) holds a caller-provided reference whose dereference must remain checked.

User-written dereferences inside clause expressions (e.g. #[requires(*ptr == 42)]) always remain checked: they operate on a different MIR local, assigned from the capture load rather than from an environment field.

Regression tests cover all three behaviours: capture loads generate no pointer checks; a valid user-written clause dereference keeps its (passing) checks; an invalid user-written clause dereference is still caught.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Reduces CBMC property/report noise for function contracts by suppressing vacuous --pointer-check instrumentation on dereferences that are only contract-clause closure capture loads, while keeping user-written dereferences inside contract expressions fully checked.

Changes:

• Detect contract-clause closure capture-load dereferences and tag the corresponding generated locations with disable:pointer-check.
• Extend span codegen to support attaching additional CBMC check pragmas to a Location (with a fast path to avoid per-location allocations).
• Add regression tests asserting (1) capture-load pointer checks are elided, (2) valid user dereferences in clauses remain checked, and (3) invalid user dereferences are still caught.

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/expected/function-contract/capture_load_user_deref_pass.rs	New expected-mode test where a user-written deref inside a clause must still produce passing pointer checks.
tests/expected/function-contract/capture_load_user_deref_pass.expected	Pins presence of a successful pointer_dereference check within a clause closure.
tests/expected/function-contract/capture_load_user_deref_fail.rs	New expected-mode test where a clause deref is dangling and must fail verification.
tests/expected/function-contract/capture_load_user_deref_fail.expected	Pins the expected pointer-dereference failure for the dangling clause deref.
tests/expected/function-contract/capture_load_checks_elided.rs	New expected-mode test asserting capture-load dereferences do not generate pointer-validity checks.
tests/expected/function-contract/capture_load_checks_elided.expected	Pins the reduced overall check count/output for the elision test.
kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs	Computes a conservative set of “capture ref locals” eligible for pointer-check suppression.
kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs	Detects statements whose dereferences are exclusively capture loads and emits locations with disable:pointer-check.
kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs	Adds codegen_span_stable_with_pragmas to attach extra CBMC pragmas and avoids allocations when only extra pragmas are present.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.