Override std::ptr::align_offset

[tautschnig]

This hook intercepts calls to std::ptr::align_offset<T> as CBMC's memory model has no concept of alignment of allocations, so we would have to non-deterministically choose an alignment of the base pointer, add the pointer's offset to it, and then do the math that is done in library/core/src/ptr/mod.rs. Instead, we choose to always return either 0 when the pointer points to the beginning of an object (and, therefore, is necessarily aligned), or usize::MAX, per align_offset's documentation, which states: "It is permissible for the implementation to always return usize::MAX. Only your algorithm’s performance can depend on getting a usable offset here, not its correctness."

Towards: #2363

[tautschnig]

Perhaps @karkhaz:

1. The alleged performance regression (https://github.com/model-checking/kani/actions/runs/4753944159/jobs/8446153448?pr=2396) is the same as previously reported upon a merge into main: https://github.com/model-checking/kani/actions/runs/4747428362/jobs/8432323295.
2. Would benchcomp also tell us about any performance improvements?

[zhassan-aws]

Is there any potential unsoundness with this change?

[celinval]

I don't think this implementation is sound. The code should panic if the input is not a power of two.
For example, the following code panic in Rust:

use std::mem::align_of;

fn main() {
  let x = 10;
  let ptr = &x as *const i32;
  let _ = ptr.align_offset(5);
}

Requested changes have been implemented.

[Copilot]

Pull request overview

This PR introduces a new gotoc hook to override std::ptr::align_offset during codegen, motivated by CBMC’s lack of allocation-alignment modeling and the performance impact this has on symbolic execution (Issue #2363). It also adds regression tests to exercise the override and to ensure the motivating performance scenario is covered.

Changes:

• Add a new GotocHook (AlignOffset) that intercepts std::ptr::align_offset::<T> calls in gotoc codegen.
• Add a regression test for Issue #2363 based on string splitting/collection.
• Add a std-override test intended to confirm the align_offset hook is being used.

Reviewed changes

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

File	Description
kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs	Adds the AlignOffset hook and registers it in fn_hooks().
tests/kani/Strings/2363.rs	Adds a regression/performance-oriented harness reproducing the reported slowdown scenario.
tests/kani/StdOverrides/align_offset.rs	Adds a test to validate that Kani’s align_offset override is active.

---

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

[feliperodri]

I've pushed two commits here to get this unstuck (2daf127, 8fa15a3). @tautschnig, the second one changes the semantics of your hook, the reasoning is below and in the commit message.

The mechanical failures (2daf127)

Three of the four red jobs had nothing to do with the feature:

• hooks.rs had lost its trailing newline. That fails the format check, which is the first step of kani-regression.sh — so all five regression jobs and llbc-regression died before running a single test. One missing byte was taking out six jobs.
• ptr became unused when the hook stopped inspecting the pointer, failing clippy-check under -D warnings.
• The test contradicted the implementation. tests/kani/StdOverrides/align_offset.rs still asserted 0 for a pointer at an object's base while the hook had been changed to return usize::MAX unconditionally.

I also merged current main (the branch was behind), and made hook_applies match core::ptr::align_offset::< as well as std::ptr::align_offset::<. Kani renders the path as std::ptr for an ordinary crate, but a no_std crate sees core::ptr and the hook would silently not apply, that's the durable half of @zhassan-aws's original request.

The real blocker (8fa15a3)

The last commit before mine switched the hook to return usize::MAX unconditionally. That's sound, but it makes Kani report failures in correct code, and it's what broke perf:

Failed Checks: "contents must be aligned to cmsghdr"
 File: "quic/s2n-quic-platform/src/message/cmsg/decode.rs", line 136

s2n-quic does this:

debug_assert_eq!(
    cursor.align_offset(align_of::<cmsghdr>()),
    0,
    "contents must be aligned to cmsghdr"
);

The documentation does say callers must not depend on a usable offset for correctness, but real crates depend on it in debug assertions, and Kani honours those. Reduced to a standalone case, a buffer that is provably aligned:

#[repr(align(8))]
struct Aligned([u8; 32]);

#[kani::proof]
fn asserts_alignment_of_an_aligned_buffer() {
    let buf = Aligned([0u8; 32]);
    let cursor = buf.0.as_ptr();
    assert_eq!(cursor.align_offset(align_of::<u64>()), 0);
}

This fails with the hook and passes without it. I confirmed causation by toggling only the hook registration on one build. CI's own history agrees: perf passed on 32e0731 (the merge commit, with the original offset-based behaviour) and failed on 50f4a37 (the switch to unconditional usize::MAX).

So the hook now reports aligned when __CPROVER_pointer_offset(ptr) is a multiple of align, and usize::MAX otherwise, which align_offset explicitly permits. The offset is the only part of an address CBMC's memory model represents, so this is what the real implementation concludes under that model. That makes it a shortcut rather than a change in behaviour, which is the point of the hook.

The caveat is documented on the hook rather than papered over: it reports "aligned" for a pointer whose object base is less aligned than align. CBMC cannot represent that either way, so the real implementation does not discover it under this model either. @tautschnig, you know that model well, so if you think that's the wrong trade, the alternatives are to model alignment properly with a non-deterministic base (which defeats the performance purpose, and would make any
alignment assertion fail anyway) or to accept the false positives and adjust the s2n-quic expectations.

Test

The previous test could not actually detect the hook: with alignment 1 every pointer is aligned, so the hook and the real implementation agree. It now checks offset 0 against alignment 4 (aligned, so 0) and offset 1 against alignment 4, where the hook answers usize::MAX and the real implementation would answer 3.

[Copilot]

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated no new comments.

Suppressed comments (2)

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs:1317

• usize::MAX is taken from the host compiler and may not match the target machine model’s usize width (e.g., 32-bit targets). Prefer deriving the max value from place_expr’s type using the MachineModel so the hook remains target-width correct.

        let rhs = is_aligned.ternary(
            Expr::int_constant(0, place_expr.typ().clone()),
            Expr::int_constant(usize::MAX, place_expr.typ().clone()),
        );

tests/kani/StdOverrides/align_offset.rs:11

• This test assumes x.as_ptr() is 4-byte aligned, but [u8; 8] only guarantees 1-byte alignment in Rust. On targets where the stack/placement isn’t 4-aligned, base_ptr.align_offset(4) may legitimately be non-zero and the test would fail. Consider explicitly aligning the allocation to 4 so the assertion is portable and the comment is accurate.

    let x = [10u8; 8];
    let base_ptr = x.as_ptr();
    // Offset 0 within the object is a multiple of any alignment, so this is already aligned.
    assert_eq!(base_ptr.align_offset(4), 0);