Skip to content

Commit 52a5b77

Browse files
zhassan-awszhassan-aws
authored
Upgrade toolchain to 2024-05-14 (rust-lang#3183)
Relevant upstream PRs: rust-lang#124797 rust-lang#124957 rust-lang#124003
1 parent 997a54c commit 52a5b77

35 files changed

+241
-130
lines changed

‎cprover_bindings/src/goto_program/expr.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -1331,11 +1331,11 @@ impl Expr {
13311331
fn unop_return_type(op: UnaryOperator, arg: &Expr) -> Type {
13321332
match op {
13331333
Bitnot | BitReverse | Bswap | UnaryMinus => arg.typ.clone(),
1334-
CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(),
1334+
CountLeadingZeros { .. } | CountTrailingZeros { .. } => Type::unsigned_int(32),
13351335
ObjectSize | PointerObject => Type::size_t(),
13361336
PointerOffset => Type::ssize_t(),
13371337
IsDynamicObject | IsFinite | Not => Type::bool(),
1338-
Popcount => arg.typ.clone(),
1338+
Popcount => Type::unsigned_int(32),
13391339
}
13401340
}
13411341
/// Private helper function to make unary operators

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

+11-6
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ use rustc_middle::ty::{List, TypeFoldable};
1818
use rustc_smir::rustc_internal;
1919
use rustc_span::def_id::DefId;
2020
use rustc_target::abi::{
21-
Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
21+
Abi::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutS, Primitive, Size, TagEncoding,
2222
TyAndLayout, VariantIdx, Variants,
2323
};
2424
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
@@ -1354,13 +1354,18 @@ impl<'tcx> GotocCtx<'tcx> {
13541354
}
13551355
}
13561356
},
1357+
Primitive::Float(f) => self.codegen_float_type(f),
1358+
Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
1359+
}
1360+
}
13571361

1358-
Primitive::F32 => self.tcx.types.f32,
1359-
Primitive::F64 => self.tcx.types.f64,
1362+
pub fn codegen_float_type(&self, f: Float) -> Ty<'tcx> {
1363+
match f {
1364+
Float::F32 => self.tcx.types.f32,
1365+
Float::F64 => self.tcx.types.f64,
13601366
// `F16` and `F128` are not yet handled.
13611367
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
1362-
Primitive::F16 | Primitive::F128 => unimplemented!(),
1363-
Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
1368+
Float::F16 | Float::F128 => unimplemented!(),
13641369
}
13651370
}
13661371

@@ -1672,7 +1677,7 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
16721677
/// Extracts the pointee type if the given mir type is either a known smart pointer (Box, Rc, ..)
16731678
/// or a regular pointer.
16741679
pub fn std_pointee_type(mir_type: Ty) -> Option<Ty> {
1675-
mir_type.builtin_deref(true).map(|tm| tm.ty)
1680+
mir_type.builtin_deref(true)
16761681
}
16771682

16781683
/// This is a place holder function that should normalize the given type.

‎kani-compiler/src/kani_middle/coercion.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@
1616
use rustc_hir::lang_items::LangItem;
1717
use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
1818
use rustc_middle::ty::adjustment::CustomCoerceUnsized;
19+
use rustc_middle::ty::TraitRef;
1920
use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
20-
use rustc_middle::ty::{TraitRef, TypeAndMut};
2121
use rustc_smir::rustc_internal;
2222
use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
2323
use stable_mir::Symbol;
@@ -263,5 +263,5 @@ fn custom_coerce_unsize_info<'tcx>(
263263

264264
/// Extract pointee type from builtin pointer types.
265265
fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option<Ty<'_>> {
266-
rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
266+
rustc_internal::internal(tcx, typ).builtin_deref(true)
267267
}

‎library/kani_macros/build.rs

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
fn main() {
5+
// Make sure `kani_sysroot` is a recognized config
6+
println!("cargo::rustc-check-cfg=cfg(kani_sysroot)");
7+
}

‎rust-toolchain.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-04-22"
5+
channel = "nightly-2024-05-14"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

‎tests/expected/coroutines/as_parameter/main.rs

+7-4
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,11 @@ where
2121

2222
#[kani::proof]
2323
fn main() {
24-
foo(|| {
25-
yield 1;
26-
return 2;
27-
});
24+
foo(
25+
#[coroutine]
26+
|| {
27+
yield 1;
28+
return 2;
29+
},
30+
);
2831
}

‎tests/expected/coroutines/main.rs

+3-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
#![feature(coroutines, coroutine_trait)]
5+
#![feature(stmt_expr_attributes)]
56

67
use std::ops::{Coroutine, CoroutineState};
78
use std::pin::Pin;
@@ -10,7 +11,8 @@ use std::pin::Pin;
1011
#[kani::unwind(2)]
1112
fn main() {
1213
let val: bool = kani::any();
13-
let mut coroutine = move || {
14+
let mut coroutine = #[coroutine]
15+
move || {
1416
let x = val;
1517
yield x;
1618
return !x;

‎tests/expected/coroutines/pin/main.rs

+3-1
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,15 @@
55
// from https://github.com/model-checking/kani/issues/416
66

77
#![feature(coroutines, coroutine_trait)]
8+
#![feature(stmt_expr_attributes)]
89

910
use std::ops::{Coroutine, CoroutineState};
1011
use std::pin::Pin;
1112

1213
#[kani::proof]
1314
fn main() {
14-
let mut coroutine = || {
15+
let mut coroutine = #[coroutine]
16+
|| {
1517
yield 1;
1618
return true;
1719
};

‎tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs

-14
This file was deleted.

‎tests/expected/intrinsics/ctpop-ice/expected

-6
This file was deleted.

‎tests/kani/Coroutines/main.rs

+3-1
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,16 @@
44
// This tests that coroutines work, even with a non-() resume type.
55

66
#![feature(coroutines, coroutine_trait)]
7+
#![feature(stmt_expr_attributes)]
78

89
use std::ops::{Coroutine, CoroutineState};
910
use std::pin::Pin;
1011

1112
#[kani::proof]
1213
#[kani::unwind(3)]
1314
fn main() {
14-
let mut add_one = |mut resume: u8| {
15+
let mut add_one = #[coroutine]
16+
|mut resume: u8| {
1517
loop {
1618
resume = yield resume.saturating_add(1);
1719
}

‎tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs

+5-2
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
//[nomiropt]compile-flags: -Z mir-opt-level=0
1313

1414
#![feature(coroutines, coroutine_trait)]
15+
#![feature(stmt_expr_attributes)]
1516

1617
use std::ops::Coroutine;
1718
use std::pin::Pin;
@@ -41,7 +42,8 @@ fn main() {
4142
}
4243

4344
fn t1() {
44-
let mut a = || {
45+
let mut a = #[coroutine]
46+
|| {
4547
let b = B;
4648
if test() {
4749
drop(b);
@@ -57,7 +59,8 @@ fn t1() {
5759
}
5860

5961
fn t2() {
60-
let mut a = || {
62+
let mut a = #[coroutine]
63+
|| {
6164
let b = B;
6265
if test2() {
6366
drop(b);

‎tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs

+48-28
Original file line numberDiff line numberDiff line change
@@ -35,32 +35,52 @@ where
3535
#[kani::proof]
3636
#[kani::unwind(16)]
3737
fn main() {
38-
finish(1, || yield);
39-
finish(8, || {
40-
for _ in 0..8 {
41-
yield;
42-
}
43-
});
44-
finish(1, || {
45-
if true {
46-
yield;
47-
} else {
48-
}
49-
});
50-
finish(1, || {
51-
if false {
52-
} else {
53-
yield;
54-
}
55-
});
56-
finish(2, || {
57-
if {
58-
yield;
59-
false
60-
} {
61-
yield;
62-
panic!()
63-
}
64-
yield
65-
});
38+
finish(
39+
1,
40+
#[coroutine]
41+
|| yield,
42+
);
43+
finish(
44+
8,
45+
#[coroutine]
46+
|| {
47+
for _ in 0..8 {
48+
yield;
49+
}
50+
},
51+
);
52+
finish(
53+
1,
54+
#[coroutine]
55+
|| {
56+
if true {
57+
yield;
58+
} else {
59+
}
60+
},
61+
);
62+
finish(
63+
1,
64+
#[coroutine]
65+
|| {
66+
if false {
67+
} else {
68+
yield;
69+
}
70+
},
71+
);
72+
finish(
73+
2,
74+
#[coroutine]
75+
|| {
76+
if {
77+
yield;
78+
false
79+
} {
80+
yield;
81+
panic!()
82+
}
83+
yield
84+
},
85+
);
6686
}

‎tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs

+7-3
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
//[nomiropt]compile-flags: -Z mir-opt-level=0
1313

1414
#![feature(coroutines, coroutine_trait)]
15+
#![feature(stmt_expr_attributes)]
1516

1617
use std::ops::Coroutine;
1718
use std::pin::Pin;
@@ -36,7 +37,8 @@ fn main() {
3637

3738
fn t1() {
3839
let b = B;
39-
let mut foo = || {
40+
let mut foo = #[coroutine]
41+
|| {
4042
yield;
4143
drop(b);
4244
};
@@ -50,7 +52,8 @@ fn t1() {
5052

5153
fn t2() {
5254
let b = B;
53-
let mut foo = || {
55+
let mut foo = #[coroutine]
56+
|| {
5457
yield b;
5558
};
5659

@@ -63,7 +66,8 @@ fn t2() {
6366

6467
fn t3() {
6568
let b = B;
66-
let foo = || {
69+
let foo = #[coroutine]
70+
|| {
6771
yield;
6872
drop(b);
6973
};

‎tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs

+2
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ impl<T: Coroutine<(), Return = ()> + Unpin> Iterator for W<T> {
3030
}
3131

3232
fn test() -> impl Coroutine<(), Return = (), Yield = u8> + Unpin {
33+
#[coroutine]
3334
|| {
3435
for i in 1..6 {
3536
yield i
@@ -43,6 +44,7 @@ fn main() {
4344
let end = 11;
4445

4546
let closure_test = |start| {
47+
#[coroutine]
4648
move || {
4749
for i in start..end {
4850
yield i

‎tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs

+3-1
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,16 @@
99
// run-pass
1010

1111
#![feature(coroutines, coroutine_trait)]
12+
#![feature(stmt_expr_attributes)]
1213

1314
use std::ops::Coroutine;
1415
use std::pin::Pin;
1516

1617
#[kani::proof]
1718
fn main() {
1819
let b = |_| 3;
19-
let mut a = || {
20+
let mut a = #[coroutine]
21+
|| {
2022
b(yield);
2123
};
2224
Pin::new(&mut a).resume(());

‎tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs

+4
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ impl Drop for Foo {
4141
}
4242

4343
fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
44+
#[coroutine]
4445
static || {
4546
let first = Foo([0; FOO_SIZE]);
4647
let _second = first;
@@ -52,6 +53,7 @@ fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
5253
fn noop() {}
5354

5455
fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
56+
#[coroutine]
5557
static || {
5658
let first = Foo([0; FOO_SIZE]);
5759
noop();
@@ -64,6 +66,7 @@ fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
6466
// Today we don't have NRVO (we allocate space for both `first` and `second`,)
6567
// but we can overlap `first` with `_third`.
6668
fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
69+
#[coroutine]
6770
static || {
6871
let first = Foo([0; FOO_SIZE]);
6972
yield;
@@ -75,6 +78,7 @@ fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
7578
}
7679

7780
fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
81+
#[coroutine]
7882
static || {
7983
let x = Foo([0; FOO_SIZE]);
8084
yield;

0 commit comments

Comments
 (0)