Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Override std::ptr::align_offset #2396

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -358,6 +358,41 @@ impl<'tcx> GotocHook<'tcx> for MemCmp {
}
}

/// 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 `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"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should include core::ptr::align_offset as well.

Copy link
Contributor

@celinval celinval Apr 25, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, they are two different methods. the std one is safe, while the core one is unsafe. Instead of using the name here, I would recommend using the align_offset lang_item instead, since it is way more reliable. This is how MIRI does it:

https://github.com/rust-lang/rust/blob/94524020ea12f7947275063b65f8b7d705be073e/src/tools/miri/src/shims/mod.rs#L43

In this case, you would be overriding the core version, which is unsafe and it is UB to execute it with an input that is not power of 2. So please add a check for that.

}

fn handle(
&self,
tcx: &mut GotocCtx<'tcx>,
_instance: Instance<'tcx>,
mut _fargs: Vec<Expr>,
assign_to: Place<'tcx>,
target: Option<BasicBlock>,
span: Option<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;
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<'tcx>() -> GotocHooks<'tcx> {
GotocHooks {
hooks: vec![
Expand All @@ -369,6 +404,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
Rc::new(RustAlloc),
Rc::new(SliceFromRawPart),
Rc::new(MemCmp),
Rc::new(AlignOffset),
],
}
}
Expand Down