Skip to content

Commit bb50371

Browse files
Upgrade rust toolchain to 2022-11-20 (rust-lang#1927)
Co-authored-by: Ted Kaminski <[email protected]>
1 parent 4746575 commit bb50371

File tree

5 files changed

+30
-8
lines changed

5 files changed

+30
-8
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -556,7 +556,7 @@ impl<'tcx> GotocCtx<'tcx> {
556556
mut_name: F,
557557
imm_name: Option<String>,
558558
) -> Expr {
559-
debug!("codegen_allocation imm_name {:?} alloc {:?}", imm_name, alloc);
559+
debug!("codegen_allocation imm_name {:?}", imm_name);
560560
let mem_var = match alloc.mutability {
561561
Mutability::Mut => {
562562
let name = mut_name(self);
@@ -670,12 +670,12 @@ impl<'tcx> GotocCtx<'tcx> {
670670
/// representation of what those fields should be initialized with.
671671
/// (A field is either bytes, or initialized with an expression.)
672672
fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec<AllocData<'tcx>> {
673-
let mut alloc_vals = Vec::with_capacity(alloc.provenance().len() + 1);
673+
let mut alloc_vals = Vec::with_capacity(alloc.provenance().ptrs().len() + 1);
674674
let pointer_size =
675675
Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());
676676

677677
let mut next_offset = Size::ZERO;
678-
for &(offset, alloc_id) in alloc.provenance().iter() {
678+
for &(offset, alloc_id) in alloc.provenance().ptrs().iter() {
679679
if offset > next_offset {
680680
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
681681
next_offset.bytes_usize()..offset.bytes_usize(),

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,13 @@ impl<'tcx> ProjectedPlace<'tcx> {
176176
goto_expr, expr_ty, ty_from_mir
177177
);
178178
warn!("{}", msg);
179-
debug_assert!(false, "{}", msg);
179+
// TODO: there's an expr type mismatch with the rust 2022-11-20 toolchain
180+
// for simd:
181+
// https://github.com/model-checking/kani/issues/1926
182+
// Disabling it for this specific case.
183+
if !(expr_ty.is_integer() && ty_from_mir.is_struct_tag()) {
184+
debug_assert!(false, "{}", msg);
185+
}
180186
return Err(UnimplementedData::new(
181187
"Projection mismatch",
182188
"https://github.com/model-checking/kani/issues/277",

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,18 @@ impl<'tcx> GotocCtx<'tcx> {
5353
self.current_fn().mir().var_debug_info.iter().find(|info| match info.value {
5454
VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0,
5555
VarDebugInfoContents::Const(_) => false,
56+
// This variant was added in
57+
// https://github.com/rust-lang/rust/pull/102570 and is concerned
58+
// with a scalar replacement of aggregates (SROA) MIR optimization
59+
// that is only enabled with `--mir-opt-level=3` or higher.
60+
// TODO: create a test and figure out if we should return debug info
61+
// for this case:
62+
// https://github.com/model-checking/kani/issues/1933
63+
VarDebugInfoContents::Composite { .. } => {
64+
// Fail in debug mode to determine if we ever hit this case
65+
debug_assert!(false, "Unhandled VarDebugInfoContents::Composite");
66+
false
67+
}
5668
})
5769
}
5870
}

kani-compiler/src/kani_middle/reachability.rs

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
154154

155155
// Collect initialization.
156156
let alloc = self.tcx.eval_static_initializer(def_id).unwrap();
157-
for &id in alloc.inner().provenance().values() {
157+
for id in alloc.inner().provenance().provenances() {
158158
self.queue.extend(collect_alloc_items(self.tcx, id).iter());
159159
}
160160
}
@@ -260,7 +260,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
260260
}
261261
ConstValue::Slice { data: alloc, start: _, end: _ }
262262
| ConstValue::ByRef { alloc, .. } => {
263-
for &id in alloc.inner().provenance().values() {
263+
for id in alloc.inner().provenance().provenances() {
264264
self.collected.extend(collect_alloc_items(self.tcx, id).iter())
265265
}
266266
}
@@ -491,7 +491,11 @@ fn collect_alloc_items<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec<MonoIt
491491
}
492492
GlobalAlloc::Memory(alloc) => {
493493
items.extend(
494-
alloc.inner().provenance().values().flat_map(|id| collect_alloc_items(tcx, *id)),
494+
alloc
495+
.inner()
496+
.provenance()
497+
.provenances()
498+
.flat_map(|id| collect_alloc_items(tcx, id)),
495499
);
496500
}
497501
GlobalAlloc::VTable(ty, trait_ref) => {

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-2022-11-06"
5+
channel = "nightly-2022-11-20"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)