Override std::ptr::align_offset

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

@@ -1235,6 +1235,91 @@ fn find_closure_call_expr(instance: &Instance, gcx: &mut GotocCtx, loc: Location
     None
 }
 
+/// This hook intercepts calls to `std::ptr::align_offset<T>`. The real implementation in
+/// `library/core/src/ptr/mod.rs` computes from the pointer's integer address, which is expensive to
+/// symbolically execute: it is the reason the string test in
+/// <https://github.com/model-checking/kani/issues/2363> was slow.
+///
+/// We answer from the pointer's offset within its object instead: aligned when
+/// `__CPROVER_pointer_offset(ptr)` is a multiple of `align`, and `usize::MAX` otherwise, which
+/// `align_offset`'s documentation explicitly permits ("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.").
+///
+/// The offset is the only part of an address CBMC's memory model represents; object base addresses
+/// are not modelled as having a particular alignment. Answering from the offset therefore matches
+/// what the real implementation concludes under that model, which is what makes this a shortcut
+/// rather than a change in behaviour.
+///
+/// The caveat is that this reports "aligned" for a pointer whose object base is less aligned than
+/// `align` -- something CBMC cannot represent either way, so the real implementation does not
+/// discover it under this model either. Returning `usize::MAX` unconditionally would avoid that, but
+/// it makes Kani report failures in correct code: `debug_assert_eq!(p.align_offset(a), 0)` is a
+/// pattern real crates use, aws/s2n-quic among them, and Kani honours debug assertions.
+struct AlignOffset;
+
+impl GotocHook for AlignOffset {
+    fn hook_applies(
+        &self,
+        _tcx: TyCtxt,
+        _instance: Instance,
+        instance_name: &str,
+        _kani_tool_attr: Option<&String>,
+    ) -> bool {
+        // Every alignment helper -- the `align_offset` methods on raw pointers, `is_aligned`,
+        // `is_aligned_to` -- eventually calls this one function. Kani normally renders the path as
+        // `std::ptr`, but a `no_std` crate sees `core::ptr`, so match both.
+        instance_name.starts_with("std::ptr::align_offset::<")
+            || instance_name.starts_with("core::ptr::align_offset::<")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let ptr = fargs.remove(0);
+        let align = fargs.remove(0);
+        // test power-of-two: align > 0 && (align & (align - 1)) == 0
+        let zero = Expr::int_constant(0, align.typ().clone());
+        let one = Expr::int_constant(1, align.typ().clone());
+        let cond = align
+            .clone()
+            .gt(zero.clone())
+            .and(align.clone().bitand(align.clone().sub(one)).eq(zero));
+        let loc = gcx.codegen_span_stable(span);
+        let safety_check = gcx.codegen_assert_assume(
+            cond,
+            PropertyClass::SafetyCheck,
+            "align_offset: align is not a power-of-two",
+            loc,
+        );
+        let place_expr = unwrap_or_return_codegen_unimplemented_stmt!(
+            gcx,
+            gcx.codegen_place_stable(assign_to, loc)
+        )
+        .goto_expr;
+        // Aligned when the offset within the object is a multiple of `align`, which is the most
+        // CBMC's memory model can tell us; `usize::MAX` when it is not, which the documentation
+        // permits. The offset is taken as unsigned so that the remainder is the byte distance into
+        // the object rather than a signed remainder.
+        let align_typ = align.typ().clone();
+        let offset = ptr.pointer_offset().cast_to(align_typ.clone());
+        let is_aligned = offset.rem(align).eq(Expr::int_constant(0, align_typ));
+        let rhs = is_aligned.ternary(
+            Expr::int_constant(0, place_expr.typ().clone()),
+            Expr::int_constant(usize::MAX, place_expr.typ().clone()),
+        );
+        let assign = place_expr.assign(rhs, loc).with_location(loc);
+        Stmt::block(vec![safety_check, assign, Stmt::goto(bb_label(target.unwrap()), loc)], loc)
+    }
+}
+
 /// Find the closure Instance from the quantifier function's generic args.
 fn find_closure_instance(instance: &Instance) -> Option<Instance> {
     for arg in instance.args().0.iter() {
@@ -1362,6 +1447,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(LoopInvariantRegister),
+            Rc::new(AlignOffset),
         ],
     }
 }

tests/kani/StdOverrides/align_offset.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test makes sure Kani uses its hook for align_offset.
+
+#[kani::proof]
+fn align_offset() {
+    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);
+
+    // Offset 1 is not a multiple of 4. The hook answers `usize::MAX`, which `align_offset` is
+    // explicitly permitted to return; the real implementation would answer 3. Asserting
+    // `usize::MAX` here is what shows the hook is being used rather than the real implementation.
+    let unaligned_ptr = unsafe { base_ptr.add(1) };
+    assert_eq!(unaligned_ptr.align_offset(4), usize::MAX);
+}

tests/kani/Strings/2363.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is to check that we have addressed the performance issue called out in
+//! https://github.com/model-checking/kani/issues/2363.
+
+#[kani::proof]
+#[kani::unwind(7)]
+#[kani::solver(cadical)]
+fn main() {
+    let s = "Mary had a little lamb";
+    let v: Vec<&str> = s.split(' ').collect();
+    assert_eq!(v, ["Mary", "had", "a", "little", "lamb"]);
+}