Skip to content

Commit

Permalink
Add comments and --check-cfg
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval committed Jun 11, 2024
1 parent bced939 commit 2509480
Show file tree
Hide file tree
Showing 4 changed files with 36 additions and 10 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/rustc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -62,8 +62,8 @@ jobs:
- name: Run tests
working-directory: upstream
env:
# Avoid error due to unexpected `cfg`
RUSTFLAGS: "-A unexpected_cfgs"
# Avoid error due to unexpected `cfg`.
RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
run: |
./configure --set=llvm.download-ci-llvm=true
./x test --stage 0 library/std
4 changes: 0 additions & 4 deletions library/contracts/safety/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,3 @@ proc-macro2 = "1.0"
proc-macro-error = "1.0.4"
quote = "1.0.20"
syn = { version = "2.0.18", features = ["full"] }


[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani_host)'] }
4 changes: 4 additions & 0 deletions library/contracts/safety/build.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
fn main() {
// We add the configurations here to be checked.
println!("cargo:rustc-check-cfg=cfg(kani_host)");
}
34 changes: 30 additions & 4 deletions library/core/src/ub_checks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -168,12 +168,38 @@ pub use predicates::*;
/// At runtime, they are no-op, and always return true.
#[cfg(not(kani))]
mod predicates {
pub fn can_dereference<T>(ptr: *const T) -> bool { true }
pub fn can_write<T>(ptr: *mut T) -> bool { true }
/// Check if a pointer can be dereferenced. I.e.:
/// * `src` must be valid for reads. See [crate::ptr] documentation.
/// * `src` must be properly aligned. Use read_unaligned if this is not the case.
/// * `src` must point to a properly initialized value of type T.
///
pub fn can_dereference<T>(src: *const T) -> bool {
let _ = src;
true
}

pub fn can_read_unaligned<T>(ptr: *const T) -> bool { true }
/// Check if a pointer can be written to:
/// * `dst` must be valid for writes.
/// * `dst` must be properly aligned. Use [`write_unaligned`] if this is not the
/// case.
pub fn can_write<T>(dst: *mut T) -> bool {
let _ = dst;
true
}

pub fn can_write_unaligned<T>(ptr: *mut T) -> bool {true}
/// Check if a pointer can be the target of unaligned reads.
/// * `src` must be valid for reads.
/// * `src` must point to a properly initialized value of type `T`.
pub fn can_read_unaligned<T>(src: *const T) -> bool {
let _ = src;
true
}

/// * `dst` must be valid for writes.
pub fn can_write_unaligned<T>(dst: *mut T) -> bool {
let _ = dst;
true
}
}

#[cfg(kani)]
Expand Down

0 comments on commit 2509480

Please sign in to comment.