Skip to content

Commit 63af43d

Browse files
tautschnigcelinvaladpaco-aws
authored
Update the rust toolchain to nightly-2023-12-07 (#2913)
Changes required due to: - rust-lang/rust@99ac405b96 Move MetadataLoader{,Dyn} to rustc_metadata. - rust-lang/rust@c997c6d822 Add more information to stable Instance - rust-lang/rust#116915 This also fixes an issue in the `simd_shuffle` implementation that was exposed by the update. Resolves #2911 --------- Co-authored-by: Celina G. Val <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>
1 parent 01bf411 commit 63af43d

File tree

13 files changed

+94
-82
lines changed

13 files changed

+94
-82
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1729,7 +1729,7 @@ impl<'tcx> GotocCtx<'tcx> {
17291729
// [u32; n]: translated wrapped in a struct
17301730
let indexes = fargs.remove(0);
17311731

1732-
let (_, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx);
1732+
let (in_type_len, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx);
17331733
let (ret_type_len, ret_type_subtype) = rust_ret_type.simd_size_and_type(self.tcx);
17341734
if ret_type_len != n {
17351735
let err_msg = format!(
@@ -1749,7 +1749,7 @@ impl<'tcx> GotocCtx<'tcx> {
17491749
// An unsigned type here causes an invariant violation in CBMC.
17501750
// Issue: https://github.com/diffblue/cbmc/issues/6298
17511751
let st_rep = Type::ssize_t();
1752-
let n_rep = Expr::int_constant(n, st_rep.clone());
1752+
let n_rep = Expr::int_constant(in_type_len, st_rep.clone());
17531753

17541754
// P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N])
17551755
let elems = (0..n)

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,14 +33,14 @@ use rustc_data_structures::temp_dir::MaybeTempDir;
3333
use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
3434
use rustc_hir::def_id::LOCAL_CRATE;
3535
use rustc_hir::definitions::DefPathHash;
36+
use rustc_metadata::creader::MetadataLoaderDyn;
3637
use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
3738
use rustc_metadata::EncodedMetadata;
3839
use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
3940
use rustc_middle::mir::mono::MonoItem;
4041
use rustc_middle::ty::TyCtxt;
4142
use rustc_middle::util::Providers;
4243
use rustc_session::config::{CrateType, OutputFilenames, OutputType};
43-
use rustc_session::cstore::MetadataLoaderDyn;
4444
use rustc_session::output::out_filename;
4545
use rustc_session::Session;
4646
use rustc_smir::rustc_internal;

kani-compiler/src/kani_middle/analysis.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,6 @@ impl From<&Terminator> for Key {
151151
TerminatorKind::Assert { .. } => Key("Assert"),
152152
TerminatorKind::Call { .. } => Key("Call"),
153153
TerminatorKind::Drop { .. } => Key("Drop"),
154-
TerminatorKind::CoroutineDrop => Key("CoroutineDrop"),
155154
TerminatorKind::Goto { .. } => Key("Goto"),
156155
TerminatorKind::InlineAsm { .. } => Key("InlineAsm"),
157156
TerminatorKind::Resume { .. } => Key("Resume"),

kani-compiler/src/kani_middle/reachability.rs

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,11 @@ impl<'tcx> MonoItemsCollector<'tcx> {
153153
/// instruction looking for the items that should be included in the compilation.
154154
fn reachable_items(&mut self) {
155155
while let Some(to_visit) = self.queue.pop() {
156-
if !self.collected.contains(&to_visit) {
156+
// TODO: This should only check is_foreign_item() or even `has_body()`.
157+
// We need https://github.com/rust-lang/rust/pull/118681 to land first.
158+
if !self.collected.contains(&to_visit)
159+
&& !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id())
160+
{
157161
self.collected.insert(to_visit.clone());
158162
let next_items = match &to_visit {
159163
MonoItem::Fn(instance) => self.visit_fn(*instance),
@@ -266,7 +270,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
266270
/// Collect an instance depending on how it is used (invoked directly or via fn_ptr).
267271
fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) {
268272
let should_collect = match instance.kind {
269-
InstanceKind::Virtual | InstanceKind::Intrinsic => {
273+
InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => {
270274
// Instance definition has no body.
271275
assert!(is_direct_call, "Expected direct call {instance:?}");
272276
false
@@ -453,8 +457,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
453457
TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => {
454458
// We generate code for this without invoking any lang item.
455459
}
456-
TerminatorKind::CoroutineDrop { .. }
457-
| TerminatorKind::Goto { .. }
460+
TerminatorKind::Goto { .. }
458461
| TerminatorKind::SwitchInt { .. }
459462
| TerminatorKind::Resume
460463
| TerminatorKind::Return

kani-compiler/src/kani_middle/stubbing/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ pub fn harness_stub_map(
4646
pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
4747
let internal_instance = rustc_internal::internal(instance);
4848
if get_stub(tcx, internal_instance.def_id()).is_some() {
49+
debug!(?instance, "validate_instance");
4950
let item = CrateItem::try_from(instance).unwrap();
5051
let mut checker = StubConstChecker::new(tcx, internal_instance, item);
5152
checker.visit_body(&item.body());

kani-driver/src/concrete_playback/test_generator.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,7 @@ impl KaniSession {
163163
let mut curr_line_num = 0;
164164

165165
// Use a buffered reader/writer to generate the unit test line by line
166-
for line in source_reader.lines().flatten() {
166+
for line in source_reader.lines().map_while(Result::ok) {
167167
curr_line_num += 1;
168168
writeln!(temp_file, "{line}")?;
169169
if curr_line_num == proof_harness_end_line {

library/kani/src/models/mod.rs

Lines changed: 24 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -137,8 +137,8 @@ mod test {
137137
/// masks with lanes represented using i16.
138138
#[test]
139139
fn test_bitmask_i16() {
140-
check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false));
141-
check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true));
140+
check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false));
141+
check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true));
142142
}
143143

144144
/// Tests that the model correctly fails if an invalid value is given.
@@ -165,11 +165,11 @@ mod test {
165165
/// These values shouldn't be symmetric and ensure that we also handle endianness correctly.
166166
#[test]
167167
fn test_bitmask_i32() {
168-
check_portable_bitmask::<_, i32, 8>(mask32x8::from([
168+
check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([
169169
true, true, false, true, false, false, false, true,
170170
]));
171171

172-
check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true]));
172+
check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true]));
173173
}
174174

175175
#[repr(simd)]
@@ -185,15 +185,16 @@ mod test {
185185
}
186186

187187
/// Compare the value returned by our model and the portable simd representation.
188-
fn check_portable_bitmask<T, E, const LANES: usize>(mask: T)
188+
fn check_portable_bitmask<T, E, const LANES: usize, M>(mask: Mask<T, LANES>)
189189
where
190-
T: ToBitMask + Clone,
191-
T::BitMask: Debug + PartialEq,
190+
T: std::simd::MaskElement,
191+
LaneCount<LANES>: SupportedLaneCount,
192192
E: kani_intrinsic::MaskElement,
193193
[u8; kani_intrinsic::mask_len(LANES)]: Sized,
194+
u64: From<M>,
194195
{
195196
assert_eq!(
196-
unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) },
197+
unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) },
197198
mask.to_bitmask()
198199
);
199200
}
@@ -211,4 +212,19 @@ mod test {
211212
unsafe { simd_bitmask::<T, U>(mask) }
212213
);
213214
}
215+
216+
/// Similar to portable simd_harness.
217+
#[test]
218+
fn check_mask_harness() {
219+
// From array doesn't work either. Manually build [false, true, false, true]
220+
let mut mask = mask32x4::splat(false);
221+
mask.set(1, true);
222+
mask.set(3, true);
223+
let bitmask = mask.to_bitmask();
224+
assert_eq!(bitmask, 0b1010);
225+
226+
let kani_mask =
227+
unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) };
228+
assert_eq!(kani_mask, bitmask);
229+
}
214230
}

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
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-2023-12-01"
5+
channel = "nightly-2023-12-07"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
Checking harness check_access_length_17...
22

3-
Failed Checks: dereference failure: pointer outside object bounds\
4-
in check_access_length_17
3+
Failed Checks: assumption failed\
4+
in <usize as std::slice::SliceIndex<[Dummy]>>::get_unchecked
55

66
Checking harness check_access_length_zero...
77

8-
Failed Checks: dereference failure: pointer outside object bounds\
9-
in check_access_length_zero
8+
Failed Checks: assumption failed\
9+
in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
1010

1111
Verification failed for - check_access_length_17
1212
Verification failed for - check_access_length_zero
Lines changed: 4 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -1,61 +1,6 @@
1-
check_always_out_bounds::check_0.pointer_dereference\
2-
Status: FAILURE\
3-
Description: "dereference failure: pointer NULL"\
4-
function check_always_out_bounds::check_0
5-
6-
check_always_out_bounds::check_0.pointer_dereference\
7-
Status: FAILURE\
8-
Description: "dereference failure: pointer outside object bounds"\
9-
function check_always_out_bounds::check_0
10-
11-
check_always_out_bounds::check_0.pointer_dereference\
12-
Status: FAILURE\
13-
Description: "dereference failure: invalid integer address"\
14-
function check_always_out_bounds::check_0
15-
16-
check_always_out_bounds::check_1.pointer_dereference\
17-
Status: FAILURE\
18-
Description: "dereference failure: pointer outside object bounds"\
19-
function check_always_out_bounds::check_1
20-
21-
check_always_out_bounds::check_2.pointer_dereference\
22-
Status: FAILURE\
23-
Description: "dereference failure: pointer outside object bounds"\
24-
function check_always_out_bounds::check_2
25-
26-
check_always_out_bounds::check_3.pointer_dereference\
27-
Status: FAILURE\
28-
Description: "dereference failure: pointer outside object bounds"\
29-
function check_always_out_bounds::check_3
30-
31-
check_always_out_bounds::check_4.pointer_dereference\
32-
Status: FAILURE\
33-
Description: "dereference failure: pointer outside object bounds"\
34-
function check_always_out_bounds::check_4
35-
36-
check_always_out_bounds::check_5.pointer_dereference\
37-
Status: FAILURE\
38-
Description: "dereference failure: pointer outside object bounds"\
39-
function check_always_out_bounds::check_5
40-
41-
check_always_out_bounds::check_6.pointer_dereference\
42-
Status: FAILURE\
43-
Description: "dereference failure: pointer outside object bounds"\
44-
function check_always_out_bounds::check_6
45-
46-
check_always_out_bounds::check_7.pointer_dereference\
47-
Status: FAILURE\
48-
Description: "dereference failure: pointer outside object bounds"\
49-
function check_always_out_bounds::check_7
50-
51-
check_always_out_bounds::check_8.pointer_dereference\
52-
Status: FAILURE\
53-
Description: "dereference failure: pointer outside object bounds"\
54-
function check_always_out_bounds::check_8
55-
56-
check_always_out_bounds::check_9.cover\
57-
Status: UNREACHABLE\
58-
Description: "cover condition: *val == 0"\
59-
function check_always_out_bounds::check_9
1+
Checking harness check_always_out_bounds...
602

3+
Failed Checks: assumption failed
4+
in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
615

6+
Verification failed for - check_always_out_bounds

tests/kani/Intrinsics/SIMD/Shuffle/main.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,3 +45,13 @@ fn main() {
4545
assert!(c == i64x4(2, 4, 6, 8));
4646
}
4747
}
48+
49+
#[kani::proof]
50+
fn check_shuffle() {
51+
{
52+
let y = i64x2(0, 1);
53+
let z = i64x2(1, 2);
54+
const I: [u32; 4] = [1, 2, 0, 3];
55+
let _x: i64x4 = unsafe { simd_shuffle(y, z, I) };
56+
}
57+
}

tests/kani/SIMD/portable_simd.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
//! Ensure we have basic support of portable SIMD.
55
#![feature(portable_simd)]
66

7-
use std::simd::{mask32x4, u64x16, ToBitMask};
7+
use std::simd::{mask32x4, u32x4, u64x16};
88

99
#[kani::proof]
1010
fn check_sum_any() {
@@ -23,3 +23,10 @@ fn check_mask() {
2323
let bitmask = mask.to_bitmask();
2424
assert_eq!(bitmask, 0b1010);
2525
}
26+
27+
#[kani::proof]
28+
fn check_resize() {
29+
let x = u32x4::from_array([0, 1, 2, 3]);
30+
assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]);
31+
assert_eq!(x.resize::<2>(9).to_array(), [0, 1]);
32+
}

tests/kani/SIMD/swizzle.rs

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! Ensure we can safely swizzle between SIMD types of different sizes.
5+
#![feature(portable_simd)]
6+
7+
use std::simd::{simd_swizzle, u32x4, u32x8};
8+
9+
#[kani::proof]
10+
fn harness_from_u32x4_to_u32x4() {
11+
let a = u32x4::from_array([0, 1, 2, 3]);
12+
let b = u32x4::from_array([4, 5, 6, 7]);
13+
let r: u32x4 = simd_swizzle!(a, b, [0, 1, 6, 7]);
14+
assert_eq!(r.to_array(), [0, 1, 6, 7]);
15+
}
16+
17+
#[kani::proof]
18+
fn harness_from_u32x4_to_u32x8() {
19+
let a = u32x4::from_array([0, 1, 2, 3]);
20+
let b = u32x4::from_array([4, 5, 6, 7]);
21+
let r: u32x8 = simd_swizzle!(a, b, [0, 1, 2, 3, 4, 5, 6, 7]);
22+
assert_eq!(r.to_array(), [0, 1, 2, 3, 4, 5, 6, 7]);
23+
}
24+
25+
#[kani::proof]
26+
fn harness_from_u32x8_to_u32x4() {
27+
let a = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]);
28+
let b = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]);
29+
let r: u32x4 = simd_swizzle!(a, b, [0, 1, 2, 3]);
30+
assert_eq!(r.to_array(), [0, 1, 2, 3]);
31+
}

0 commit comments

Comments
 (0)