kani/
lib.rs

1// Copyright Kani Contributors
2// SPDX-License-Identifier: Apache-2.0 OR MIT
3
4// Required so we can use kani_macros attributes.
5#![feature(register_tool)]
6#![register_tool(kanitool)]
7// Used for rustc_diagnostic_item.
8// Note: We could use a kanitool attribute instead.
9#![feature(rustc_attrs)]
10// Used to model simd.
11#![feature(repr_simd)]
12#![feature(generic_const_exprs)]
13#![allow(incomplete_features)]
14// Features used for tests only.
15#![cfg_attr(test, feature(core_intrinsics, portable_simd))]
16// Required for `rustc_diagnostic_item` and `core_intrinsics`
17#![allow(internal_features)]
18// Required for implementing memory predicates.
19// `core::mem::{size_of,align_of}_val_raw` are only reached by the `concrete_playback` paths of
20// the `kani_core` memory models this crate expands.
21#![cfg_attr(feature = "concrete_playback", feature(layout_for_ptr))]
22#![feature(bstr)]
23#![feature(wtf8_internals)]
24#![feature(ptr_metadata)]
25#![feature(formatting_options)]
26#![feature(f16)]
27#![feature(f128)]
28#![feature(convert_float_to_int)]
29#![feature(sized_hierarchy)]
30
31// Allow us to use `kani::` to access crate features.
32extern crate self as kani;
33
34pub mod arbitrary;
35pub mod bounded_arbitrary;
36#[cfg(feature = "concrete_playback")]
37mod concrete_playback;
38pub mod futures;
39pub mod iter;
40pub mod shadow;
41pub mod vec;
42
43mod models;
44
45#[cfg(feature = "concrete_playback")]
46pub use concrete_playback::concrete_playback_run;
47
48#[cfg(not(feature = "concrete_playback"))]
49/// NOP `concrete_playback` for type checking during verification mode.
50pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
51    unreachable!("Concrete playback does not work during verification")
52}
53
54pub use futures::{RoundRobin, block_on, block_on_with_spawn, spawn, yield_now};
55
56// Kani proc macros must be in a separate crate
57pub use kani_macros::*;
58
59// Declare common Kani API such as assume, assert
60kani_core::kani_lib!(kani);
61
62/// Compatibility module: the `Invariant` trait is now defined at the crate root (its
63/// definition moved into `kani_core`), but it was previously importable as
64/// `kani::invariant::Invariant`; keep that path working.
65pub mod invariant {
66    pub use super::Invariant;
67}
68
69// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
70// crate uses `extern crate std as core`. See
71// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
72#[doc(hidden)]
73#[cfg(not(feature = "concrete_playback"))]
74pub use core::assert as __kani__workaround_core_assert;
75
76#[macro_export]
77macro_rules! cover {
78    () => {{
79        kani::cover(true, "cover location");
80    }};
81    ($cond:expr $(,)?) => {{
82        kani::cover($cond, concat!("cover condition: ", stringify!($cond)));
83    }};
84    ($cond:expr, $msg:literal) => {{
85        kani::cover($cond, $msg);
86    }};
87}
88
89/// `implies!(premise => conclusion)` means that if the `premise` is true, so
90/// must be the `conclusion`.
91///
92/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
93/// as the concept of an implication is more natural to think about than its expansion.
94#[macro_export]
95macro_rules! implies {
96    ($premise:expr => $conclusion:expr) => {
97        !($premise) || ($conclusion)
98    };
99}
100
101/// Define a reusable set of function stubs that can be applied to multiple proof harnesses.
102///
103/// # Example
104///
105/// ```ignore
106/// kani::stub_set!(my_stubs,
107///     stub(std::fs::read, my_read),
108///     stub(std::fs::write, my_write),
109/// );
110///
111/// #[kani::proof]
112/// #[kani::use_stub_set(my_stubs)]
113/// fn my_harness() { /* ... */ }
114/// ```
115///
116/// Stub sets can also include other stub sets:
117///
118/// ```ignore
119/// kani::stub_set!(all_stubs,
120///     use_stub_set(my_stubs),
121///     stub(other::func, my_func),
122/// );
123/// ```
124#[macro_export]
125macro_rules! stub_set {
126    (pub $name:ident, $($entry:tt)*) => {
127        /// A Kani stub set definition.
128        #[allow(non_upper_case_globals)]
129        #[kanitool::stub_set($($entry)*)]
130        pub const $name: () = ();
131    };
132    ($vis:vis $name:ident, $($entry:tt)*) => {
133        #[doc(hidden)]
134        #[allow(non_upper_case_globals)]
135        #[kanitool::stub_set($($entry)*)]
136        $vis const $name: () = ();
137    };
138}
139
140pub(crate) use kani_macros::unstable_feature as unstable;
141
142pub mod contracts;
kani/lib.rs

kani/
lib.rs
