Skip to content

Commit 8767fe6

Browse files
zhassan-awscelinval
zhassan-aws
and
celinval
authored
Delete kani::expect_fail and associated hook (rust-lang#2027)
Co-authored-by: Celina G. Val <celinval@amazon.com>
1 parent 245db28 commit 8767fe6

33 files changed

+387
-589
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

-5
Original file line numberDiff line numberDiff line change
@@ -55,11 +55,6 @@ pub enum PropertyClass {
5555
///
5656
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?
5757
ExactDiv,
58-
/// The `kani::expect_fail` assertion.
59-
///
60-
/// SPECIAL BEHAVIOR: Inverted interpretation of success/failure.
61-
/// (Note: Possibly this should be the same as Cover, or perhaps an ExplicitCover?)
62-
ExpectFail,
6358
/// Another instrinsic check.
6459
///
6560
/// SPECIAL BEHAVIOR: None TODO: Why should this exist?

‎kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

-35
Original file line numberDiff line numberDiff line change
@@ -87,40 +87,6 @@ impl<'tcx> GotocHook<'tcx> for Cover {
8787
}
8888
}
8989

90-
struct ExpectFail;
91-
impl<'tcx> GotocHook<'tcx> for ExpectFail {
92-
fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
93-
matches_function(tcx, instance, "KaniExpectFail")
94-
}
95-
96-
fn handle(
97-
&self,
98-
tcx: &mut GotocCtx<'tcx>,
99-
_instance: Instance<'tcx>,
100-
mut fargs: Vec<Expr>,
101-
_assign_to: Place<'tcx>,
102-
target: Option<BasicBlock>,
103-
span: Option<Span>,
104-
) -> Stmt {
105-
assert_eq!(fargs.len(), 2);
106-
let target = target.unwrap();
107-
let cond = fargs.remove(0).cast_to(Type::bool());
108-
109-
// Add "EXPECTED FAIL" to the message because compiletest relies on it
110-
let msg =
111-
format!("EXPECTED FAIL: {}", tcx.extract_const_message(&fargs.remove(0)).unwrap());
112-
113-
let loc = tcx.codegen_span_option(span);
114-
Stmt::block(
115-
vec![
116-
tcx.codegen_assert(cond, PropertyClass::ExpectFail, &msg, loc),
117-
Stmt::goto(tcx.current_fn().find_label(&target), loc),
118-
],
119-
loc,
120-
)
121-
}
122-
}
123-
12490
struct Assume;
12591
impl<'tcx> GotocHook<'tcx> for Assume {
12692
fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
@@ -411,7 +377,6 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
411377
Rc::new(Assume),
412378
Rc::new(Assert),
413379
Rc::new(Cover),
414-
Rc::new(ExpectFail),
415380
Rc::new(Nondet),
416381
Rc::new(RustAlloc),
417382
Rc::new(SliceFromRawPart),

‎library/kani/src/lib.rs

-9
Original file line numberDiff line numberDiff line change
@@ -138,15 +138,6 @@ fn any_raw_inner<T>() -> T {
138138
unimplemented!("Kani any_raw_inner");
139139
}
140140

141-
/// Function used in tests for cases where the condition is not always true.
142-
#[inline(never)]
143-
#[rustc_diagnostic_item = "KaniExpectFail"]
144-
pub fn expect_fail(_cond: bool, _message: &'static str) {
145-
if cfg!(feature = "concrete_playback") {
146-
assert!(!_cond, "kani::expect_fail does not hold: {_message}");
147-
}
148-
}
149-
150141
/// Function used to generate panic with a static message as this is the only one currently
151142
/// supported by Kani display.
152143
///

‎tests/expected/arbitrary/enums/expected

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
Checking harness check_random...
2+
3+
Status: SATISFIED\
4+
Description: "This should be reachable"\
5+
in function check_random
6+
7+
Status: SATISFIED\
8+
Description: "This should be reachable"\
9+
in function check_random
10+
11+
Status: SATISFIED\
12+
Description: "This should be reachable"\
13+
in function check_random
14+
15+
Checking harness check_basic...
16+
17+
Status: SATISFIED\
18+
Description: "This should be reachable"\
19+
in function check_basic
20+
21+
Status: SATISFIED\
22+
Description: "This should be reachable"\
23+
in function check_basic
24+
25+
Status: SATISFIED\
26+
Description: "This should be reachable"\
27+
in function check_basic
28+
29+
Checking harness check_continuous...
30+
31+
Status: SATISFIED\
32+
Description: "This should be reachable"\
33+
in function check_continuous
34+
35+
Status: SATISFIED\
36+
Description: "This should be reachable"\
37+
in function check_continuous
38+
39+
Status: SATISFIED\
40+
Description: "This should be reachable"\
41+
in function check_continuous
42+
43+
** 3 of 3 cover properties satisfied
44+
45+
46+
VERIFICATION:- SUCCESSFUL
47+
48+
Complete - 3 successfully verified harnesses, 0 failures, 3 total.

‎tests/kani/Arbitrary/enum.rs renamed to ‎tests/expected/arbitrary/enums/main.rs

+3-5
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,6 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
//
44
//! Check that user can correctly generate arbitrary types for enums.
5-
//! TODO: We should replace these expect_fail / assert with cover statements.
6-
//! <https://github.com/model-checking/kani/issues/696>
75
#[derive(Copy, Clone)]
86
enum Basic {
97
Variant1,
@@ -43,19 +41,19 @@ macro_rules! check_enum {
4341
match e {
4442
$enum_type::Variant1 => {
4543
let val = e as $repr;
46-
kani::expect_fail(false, "This should be reachable");
44+
kani::cover!(true, "This should be reachable");
4745
assert!(val == $v1);
4846
return;
4947
}
5048
$enum_type::Variant2 => {
5149
let val = e as $repr;
52-
kani::expect_fail(false, "This should be reachable");
50+
kani::cover!(true, "This should be reachable");
5351
assert!(val == $v2);
5452
return;
5553
}
5654
$enum_type::Variant3 => {
5755
let val = e as $repr;
58-
kani::expect_fail(false, "This should be reachable");
56+
kani::cover!(true, "This should be reachable");
5957
assert!(val == $v3);
6058
return;
6159
}

‎tests/expected/arbitrary/floats/expected

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
Checking harness check_f64...
2+
3+
Status: SATISFIED\
4+
Description: "This may be true"\
5+
in function check_f64
6+
7+
Status: SATISFIED\
8+
Description: "This may also be true"\
9+
in function check_f64
10+
11+
Status: SATISFIED\
12+
Description: "NaN should be valid float"\
13+
in function check_f64
14+
15+
Status: SATISFIED\
16+
Description: "Subnormal should be valid float"\
17+
in function check_f64
18+
19+
Status: SATISFIED\
20+
Description: "Normal should be valid float"\
21+
in function check_f64
22+
23+
Status: SATISFIED\
24+
Description: "Non-finite numbers are valid float"\
25+
in function check_f64
26+
27+
28+
Checking harness check_f32...
29+
30+
Status: SATISFIED\
31+
Description: "This may be true"\
32+
in function check_f32
33+
34+
Status: SATISFIED\
35+
Description: "This may also be true"\
36+
in function check_f32
37+
38+
Status: SATISFIED\
39+
Description: "NaN should be valid float"\
40+
in function check_f32
41+
42+
Status: SATISFIED\
43+
Description: "Subnormal should be valid float"\
44+
in function check_f32
45+
46+
Status: SATISFIED\
47+
Description: "Normal should be valid float"\
48+
in function check_f32
49+
50+
Status: SATISFIED\
51+
Description: "Non-finite numbers are valid float"\
52+
in function check_f32
53+
54+
55+
** 6 of 6 cover properties satisfied
56+
57+
58+
VERIFICATION:- SUCCESSFUL
59+
60+
Complete - 2 successfully verified harnesses, 0 failures, 2 total.

‎tests/expected/arbitrary/floats/main.rs

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//
4+
// Ensure that kani::any and kani::any_raw can be used with floats.
5+
6+
macro_rules! test {
7+
( $type: ty ) => {{
8+
let v1 = kani::any::<$type>();
9+
let v2 = kani::any::<$type>();
10+
kani::cover!(v1 == v2, "This may be true");
11+
kani::cover!(v1 != v2, "This may also be true");
12+
kani::cover!(v1.is_nan(), "NaN should be valid float");
13+
kani::cover!(v1.is_subnormal(), "Subnormal should be valid float");
14+
kani::cover!(v1.is_normal(), "Normal should be valid float");
15+
kani::cover!(!v1.is_finite(), "Non-finite numbers are valid float");
16+
}};
17+
}
18+
19+
#[kani::proof]
20+
fn check_f32() {
21+
test!(f32);
22+
}
23+
24+
#[kani::proof]
25+
fn check_f64() {
26+
test!(f64);
27+
}

0 commit comments

Comments
 (0)