From 91fd8a9f6bde7c9f38ae8854a21312f39c922c37 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 20 Apr 2023 11:49:56 +0000 Subject: [PATCH 1/5] Override std::ptr::align_offset MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This hook intercepts calls to `std::ptr::align_offset` 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 `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." Fixes: #2363 --- .../codegen_cprover_gotoc/overrides/hooks.rs | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index e68a9ed50af2..b7c136325138 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -908,6 +908,41 @@ fn find_closure_call_expr(instance: &Instance, gcx: &mut GotocCtx, loc: Location None } +/// This hook intercepts calls to `std::ptr::align_offset` 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 `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." +pub struct AlignOffset; + +impl<'tcx> GotocHook<'tcx> for AlignOffset { + fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { + let name = with_no_trimmed_paths!(tcx.def_path_str(instance.def_id())); + name == "std::ptr::align_offset" + } + + fn handle( + &self, + tcx: &mut GotocCtx<'tcx>, + _instance: Instance<'tcx>, + mut _fargs: Vec, + assign_to: Place<'tcx>, + target: Option, + span: Option, + ) -> Stmt { + let loc = tcx.codegen_span_option(span); + let target = target.unwrap(); + let place_expr = + unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) + .goto_expr; + let rhs = Expr::int_constant(usize::MAX, place_expr.typ().clone()); + let code = place_expr.assign(rhs, loc).with_location(loc); + Stmt::block(vec![code, Stmt::goto(tcx.current_fn().find_label(&target), loc)], loc) + } +} + pub fn fn_hooks() -> GotocHooks { let kani_lib_hooks = [ (KaniHook::Assert, Rc::new(Assert) as Rc), @@ -935,6 +970,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(RustAlloc), Rc::new(MemCmp), Rc::new(LoopInvariantRegister), + Rc::new(AlignOffset), ], } } From cb2a6a4782a5744a8b22a45ef11b4141508a9e93 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Jun 2025 12:04:04 +0000 Subject: [PATCH 2/5] Update to current code base and apply suggestions --- .../codegen_cprover_gotoc/overrides/hooks.rs | 53 ++++++++++++------- 1 file changed, 35 insertions(+), 18 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index b7c136325138..32921dfbfef7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -915,31 +915,48 @@ fn find_closure_call_expr(instance: &Instance, gcx: &mut GotocCtx, loc: Location /// `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." -pub struct AlignOffset; +struct AlignOffset; -impl<'tcx> GotocHook<'tcx> for AlignOffset { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let name = with_no_trimmed_paths!(tcx.def_path_str(instance.def_id())); - name == "std::ptr::align_offset" +impl GotocHook for AlignOffset { + fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool { + let full_name = instance.name(); + full_name.starts_with("std::ptr::align_offset::<") } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, - mut _fargs: Vec, - assign_to: Place<'tcx>, - target: Option, - span: Option, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, ) -> Stmt { - let loc = tcx.codegen_span_option(span); - let target = target.unwrap(); - let place_expr = - unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) - .goto_expr; + 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; let rhs = Expr::int_constant(usize::MAX, place_expr.typ().clone()); - let code = place_expr.assign(rhs, loc).with_location(loc); - Stmt::block(vec![code, Stmt::goto(tcx.current_fn().find_label(&target), loc)], loc) + let assign = place_expr.assign(rhs, loc).with_location(loc); + Stmt::block(vec![safety_check, assign, Stmt::goto(bb_label(target.unwrap()), loc)], loc) } } From 190590832c8863cf8faedbf7324958a437a7d80d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Jun 2025 12:30:11 +0000 Subject: [PATCH 3/5] Add tests --- tests/kani/StdOverrides/align_offset.rs | 12 ++++++++++++ tests/kani/Strings/2363.rs | 14 ++++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 tests/kani/StdOverrides/align_offset.rs create mode 100644 tests/kani/Strings/2363.rs diff --git a/tests/kani/StdOverrides/align_offset.rs b/tests/kani/StdOverrides/align_offset.rs new file mode 100644 index 000000000000..ec058c6e6a1a --- /dev/null +++ b/tests/kani/StdOverrides/align_offset.rs @@ -0,0 +1,12 @@ +// 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 = 10; + let ptr = &x as *const i32; + let alignment = ptr.align_offset(1); + assert_eq!(alignment, usize::MAX); +} diff --git a/tests/kani/Strings/2363.rs b/tests/kani/Strings/2363.rs new file mode 100644 index 000000000000..e7d1fb539d4f --- /dev/null +++ b/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"]); +} From a7da5438c7fa3eb45a17fab5e6f190461e3f9a34 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 27 Jun 2025 12:49:48 +0000 Subject: [PATCH 4/5] Clippy --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 32921dfbfef7..3eedffc7b79f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -951,7 +951,7 @@ impl GotocHook for AlignOffset { ); let place_expr = unwrap_or_return_codegen_unimplemented_stmt!( gcx, - gcx.codegen_place_stable(&assign_to, loc) + gcx.codegen_place_stable(assign_to, loc) ) .goto_expr; let rhs = Expr::int_constant(usize::MAX, place_expr.typ().clone()); From 12482c95eb9529ed31f061fb8009ce7d6e5b0a55 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jul 2025 18:16:05 +0000 Subject: [PATCH 5/5] Use zero offset when the pointer is guaranteed to be aligned --- .../src/codegen_cprover_gotoc/overrides/hooks.rs | 10 ++++++++-- tests/kani/StdOverrides/align_offset.rs | 11 +++++++---- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 3eedffc7b79f..06388291588d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -933,7 +933,7 @@ impl GotocHook for AlignOffset { span: Span, ) -> Stmt { assert_eq!(fargs.len(), 2); - let _ptr = fargs.remove(0); + 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()); @@ -954,7 +954,13 @@ impl GotocHook for AlignOffset { gcx.codegen_place_stable(assign_to, loc) ) .goto_expr; - let rhs = Expr::int_constant(usize::MAX, place_expr.typ().clone()); + let pointer_offset = Expr::pointer_offset(ptr); + let trivially_aligned = + pointer_offset.clone().eq(Expr::int_constant(0, pointer_offset.typ().clone())); + let rhs = trivially_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) } diff --git a/tests/kani/StdOverrides/align_offset.rs b/tests/kani/StdOverrides/align_offset.rs index ec058c6e6a1a..13a54f87057b 100644 --- a/tests/kani/StdOverrides/align_offset.rs +++ b/tests/kani/StdOverrides/align_offset.rs @@ -5,8 +5,11 @@ #[kani::proof] fn align_offset() { - let x = 10; - let ptr = &x as *const i32; - let alignment = ptr.align_offset(1); - assert_eq!(alignment, usize::MAX); + let x = [10, 42]; + let base_ptr = &x[0] as *const i32; + let base_alignment = base_ptr.align_offset(1); + assert_eq!(base_alignment, 0); + let offset_ptr = &x[1] as *const i32; + let offset_alignment = offset_ptr.align_offset(1); + assert_eq!(offset_alignment, usize::MAX); }