Skip to content

Commit

Permalink
Update Rust toolchain to 2023-10-09 (model-checking#2814)
Browse files Browse the repository at this point in the history
Source changes required by the following upstream commits:

* rust-lang/rust@e8a2673159 Add VariantIdx back
* rust-lang/rust@f14b7c9443 Move FieldIdx and Layout to rustc_target
* rust-lang/rust@b47ad3b744 Bring back generic FieldIdx

Resolves: model-checking#2813
  • Loading branch information
tautschnig authored Oct 9, 2023
1 parent 7a3e746 commit ab41be5
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 14 deletions.
3 changes: 1 addition & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,13 @@ use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
use crate::codegen_cprover_gotoc::GotocCtx;
use crate::unwrap_or_return_codegen_unimplemented;
use cbmc::goto_program::{Expr, Location, Type};
use rustc_abi::FieldIdx;
use rustc_hir::Mutability;
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::{
mir::{Local, Place, ProjectionElem},
ty::{self, Ty, TypeAndMut, VariantDef},
};
use rustc_target::abi::{TagEncoding, VariantIdx, Variants};
use rustc_target::abi::{FieldIdx, TagEncoding, VariantIdx, Variants};
use tracing::{debug, trace, warn};

/// A projection in Kani can either be to a type (the normal case),
Expand Down
3 changes: 1 addition & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,12 @@ use cbmc::goto_program::{
use cbmc::MachineModel;
use cbmc::{btree_string_map, InternString, InternedString};
use num::bigint::BigInt;
use rustc_abi::FieldIdx;
use rustc_index::IndexVec;
use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
use rustc_middle::ty::adjustment::PointerCoercion;
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants};
use rustc_target::abi::{FieldIdx, FieldsShape, Size, TagEncoding, VariantIdx, Variants};
use std::collections::BTreeMap;
use tracing::{debug, trace, warn};

Expand Down
18 changes: 9 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@ use rustc_middle::ty::{
use rustc_middle::ty::{List, TypeFoldable};
use rustc_span::def_id::DefId;
use rustc_target::abi::{
Abi::Vector, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding, TyAndLayout,
VariantIdx, Variants,
Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
TyAndLayout, VariantIdx, Variants,
};
use rustc_target::spec::abi::Abi;
use std::iter;
Expand Down Expand Up @@ -870,7 +870,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_alignment_padding(
&self,
size: Size,
layout: &LayoutS,
layout: &LayoutS<FieldIdx, VariantIdx>,
idx: usize,
) -> Option<DatatypeComponent> {
let align = Size::from_bits(layout.align.abi.bits());
Expand All @@ -895,7 +895,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_struct_fields(
&mut self,
flds: Vec<(String, Ty<'tcx>)>,
layout: &LayoutS,
layout: &LayoutS<FieldIdx, VariantIdx>,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
match &layout.fields {
Expand Down Expand Up @@ -1352,7 +1352,7 @@ impl<'tcx> GotocCtx<'tcx> {
&mut self,
variant: &VariantDef,
subst: &'tcx GenericArgsRef<'tcx>,
layout: &LayoutS,
layout: &LayoutS<FieldIdx, VariantIdx>,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
let flds: Vec<_> =
Expand Down Expand Up @@ -1521,7 +1521,7 @@ impl<'tcx> GotocCtx<'tcx> {
ty: Ty<'tcx>,
adtdef: &'tcx AdtDef,
subst: &'tcx GenericArgsRef<'tcx>,
variants: &IndexVec<VariantIdx, LayoutS>,
variants: &IndexVec<VariantIdx, LayoutS<FieldIdx, VariantIdx>>,
) -> Type {
let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
let mangled_name = self.ty_mangled_name(ty);
Expand All @@ -1540,7 +1540,7 @@ impl<'tcx> GotocCtx<'tcx> {

pub(crate) fn variant_min_offset(
&self,
variants: &IndexVec<VariantIdx, LayoutS>,
variants: &IndexVec<VariantIdx, LayoutS<FieldIdx, VariantIdx>>,
) -> Option<Size> {
variants
.iter()
Expand Down Expand Up @@ -1625,7 +1625,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_name: InternedString,
def: &'tcx AdtDef,
subst: &'tcx GenericArgsRef<'tcx>,
layouts: &IndexVec<VariantIdx, LayoutS>,
layouts: &IndexVec<VariantIdx, LayoutS<FieldIdx, VariantIdx>>,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
def.variants()
Expand Down Expand Up @@ -1657,7 +1657,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_name: InternedString,
case: &VariantDef,
subst: &'tcx GenericArgsRef<'tcx>,
variant: &LayoutS,
variant: &LayoutS<FieldIdx, VariantIdx>,
initial_offset: Size,
) -> Type {
let case_name = format!("{name}::{}", case.name);
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2023-10-06"
channel = "nightly-2023-10-09"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit ab41be5

Please sign in to comment.