Override std::ptr::align_offset #2396
Conversation
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." Fixes: model-checking#2363
|
Perhaps @karkhaz:
|
| 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" |
There was a problem hiding this comment.
I think we should include core::ptr::align_offset as well.
There was a problem hiding this comment.
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:
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.
There was a problem hiding this comment.
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);
}
Description of changes:
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 inlibrary/core/src/ptr/mod.rs. Instead, we choose to always returnusize::MAX, peralign_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."Resolved issues:
Fixes: #2363
Related RFC:
n/a
Call-outs:
n/a
Testing:
How is this change tested? Local runs of the example from Improve symbolic execution performance when running against concrete values #2363.
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.