Skip to content

Commit

Permalink
Use fully-qualified name for size_of (model-checking#3838)
Browse files Browse the repository at this point in the history
Add `core::mem::` prefix to all uses of `size_of`.

Background: in some cases, I get errors of the form:
```
   Compiling kani_core v0.58.0 (https://github.com/model-checking/kani#35015dce)
error[E0425]: cannot find function `size_of` in this scope
  --> /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/35015dc/library/kani/src/lib.rs:54:1
   |
54 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^ not found in this scope
   |
   = help: consider importing one of these items:
           core::mem::size_of
           crate::core_path::intrinsics::size_of
           crate::core_path::mem::size_of
           std::mem::size_of
   = note: this error originates in the macro `kani_core::ptr_generator` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
```
when adding the Kani library as a dependency. Adding `core::mem::` fixes
those issues.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws authored Jan 17, 2025
1 parent 35015dc commit 6f70c7d
Show file tree
Hide file tree
Showing 7 changed files with 57 additions and 5 deletions.
1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ exclude = [
"tests/script-based-pre/build-cache-bin/target/new_dep",
"tests/script-based-pre/build-cache-dirty/target/new_dep",
"tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std",
"tests/script-based-pre/kani_lib_dep",
]

[workspace.lints.clippy]
Expand Down
10 changes: 5 additions & 5 deletions library/kani_core/src/arbitrary/pointer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -265,7 +265,7 @@ macro_rules! ptr_generator {
let ptr = match status {
AllocationStatus::Dangling => {
// Generate potentially unaligned pointer.
let offset = kani::any_where(|b: &usize| *b < size_of::<T>());
let offset = kani::any_where(|b: &usize| *b < core::mem::size_of::<T>());
crate::ptr::NonNull::<T>::dangling().as_ptr().wrapping_add(offset)
}
AllocationStatus::DeadObject => {
Expand All @@ -279,7 +279,7 @@ macro_rules! ptr_generator {
AllocationStatus::OutOfBounds => {
// Generate potentially unaligned pointer.
let buf_ptr = addr_of_mut!(self.buf) as *mut u8;
let offset = kani::any_where(|b: &usize| *b < size_of::<T>());
let offset = kani::any_where(|b: &usize| *b < core::mem::size_of::<T>());
unsafe { buf_ptr.add(Self::BUF_LEN - offset) as *mut T }
}
};
Expand Down Expand Up @@ -331,7 +331,7 @@ macro_rules! ptr_generator {
"Cannot generate in-bounds object of the requested type. Buffer is not big enough."
);
let buf_ptr = addr_of_mut!(self.buf) as *mut u8;
let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - size_of::<T>());
let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - core::mem::size_of::<T>());
let ptr = unsafe { buf_ptr.add(offset) as *mut T };
let is_initialized = kani::any();
if is_initialized {
Expand All @@ -356,8 +356,8 @@ macro_rules! ptr_generator_fn {
() => {
/// Create a pointer generator that fits at least `N` elements of type `T`.
pub fn pointer_generator<T, const NUM_ELTS: usize>()
-> PointerGenerator<{ size_of::<T>() * NUM_ELTS }> {
PointerGenerator::<{ size_of::<T>() * NUM_ELTS }>::new()
-> PointerGenerator<{ core::mem::size_of::<T>() * NUM_ELTS }> {
PointerGenerator::<{ core::mem::size_of::<T>() * NUM_ELTS }>::new()
}
};
}
Expand Down
10 changes: 10 additions & 0 deletions tests/script-based-pre/kani_lib_dep/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
[package]
name = "kani_lib_dep"
version = "0.1.0"
edition = "2021"

[dependencies]
kani_core = { path = "../../../library/kani_core" }
kani = { path = "../../../library/kani" }
13 changes: 13 additions & 0 deletions tests/script-based-pre/kani_lib_dep/build.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
#!/usr/bin/env bash
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
# Test building a crate that has the Kani library as a dependency

set -e

rm -rf target

set -e
cargo build

rm -rf target
5 changes: 5 additions & 0 deletions tests/script-based-pre/kani_lib_dep/config.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
script: build.sh
expected: expected
exit_code: 0
Empty file.
23 changes: 23 additions & 0 deletions tests/script-based-pre/kani_lib_dep/src/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

use kani::Arbitrary;

struct Foo {
x: i32,
y: i32,
z: i32,
}

impl Arbitrary for Foo {
fn any() -> Self {
Foo { x: 3, y: 4, z: 5 }
}
}

fn main() {
let f: Foo = kani::any();
assert_eq!(f.x, 3);
assert_eq!(f.y, 4);
assert_eq!(f.z, 5);
}

0 comments on commit 6f70c7d

Please sign in to comment.