Skip to content

Commit

Permalink
Update toolchain to 2023-02-16
Browse files Browse the repository at this point in the history
Skip over all the nightlies from 2023-02-06 until 2023-02-15 as those
ICE when trying to build kani with:
```
error: internal compiler error: cannot relate constants (Const { ty: fn() -> usize {std::mem::size_of::<[T; N]>}, kind: Value(Branch([])) }, Const { ty: fn() -> usize {std::mem::size_of::<[T; _]>}, kind: Value(Branch([])) }) of different types: fn() -> usize {std::mem::size_of::<[T; N]>} != fn() -> usize {std::mem::size_of::<[T; _]>}
```

This issue was reported upstream as
rust-lang/rust#107898, and fixed in
rust-lang/rust#107940, which isn't part of any
of the above nightlies.

Doing this multi-day update also requires addressing:

Remove some superfluous type parameters from layout.rs rust-lang/rust#107163
Introduce -Zterminal-urls to use OSC8 for error codes rust-lang/rust#107838
s/eval_usize/eval_target_usize/ for clarity rust-lang/rust#108029

Co-authored-by: Qinheping Hu <[email protected]>
  • Loading branch information
tautschnig and qinheping committed Apr 15, 2023
1 parent 22b14f4 commit d4966cd
Show file tree
Hide file tree
Showing 5 changed files with 22 additions and 19 deletions.
18 changes: 10 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1226,14 +1226,16 @@ impl<'tcx> GotocCtx<'tcx> {
// `simd_shuffle4`) is type-checked
match farg_types[2].kind() {
ty::Array(ty, len) if matches!(ty.kind(), ty::Uint(ty::UintTy::U32)) => {
len.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(|| {
self.tcx.sess.span_err(
span.unwrap(),
"could not evaluate shuffle index array length",
);
// Return a dummy value
u64::MIN
})
len.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(
|| {
self.tcx.sess.span_err(
span.unwrap(),
"could not evaluate shuffle index array length",
);
// Return a dummy value
u64::MIN
},
)
}
_ => {
let err_msg = format!(
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ impl<'tcx> GotocCtx<'tcx> {
) -> Expr {
let res_t = self.codegen_ty(res_ty);
let op_expr = self.codegen_operand(op);
let width = sz.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
let width = sz.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
Expr::struct_expr(
res_t,
btree_string_map![("0", op_expr.array_constant(width))],
Expand Down
16 changes: 8 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -777,7 +777,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
ty::Foreign(defid) => self.codegen_foreign(ty, *defid),
ty::Array(et, len) => {
let evaluated_len = len.try_eval_usize(self.tcx, self.param_env()).unwrap();
let evaluated_len = len.try_eval_target_usize(self.tcx, self.param_env()).unwrap();
let array_name = format!("[{}; {evaluated_len}]", self.ty_mangled_name(*et));
let array_pretty_name = format!("[{}; {evaluated_len}]", self.ty_pretty_name(*et));
// wrap arrays into struct so that one can take advantage of struct copy in C
Expand Down Expand Up @@ -902,7 +902,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_alignment_padding(
&self,
size: Size,
layout: &LayoutS<VariantIdx>,
layout: &LayoutS,
idx: usize,
) -> Option<DatatypeComponent> {
let align = Size::from_bits(layout.align.abi.bits());
Expand All @@ -927,7 +927,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_struct_fields(
&mut self,
flds: Vec<(String, Ty<'tcx>)>,
layout: &LayoutS<VariantIdx>,
layout: &LayoutS,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
match &layout.fields {
Expand Down Expand Up @@ -1385,7 +1385,7 @@ impl<'tcx> GotocCtx<'tcx> {
&mut self,
variant: &VariantDef,
subst: &'tcx InternalSubsts<'tcx>,
layout: &LayoutS<VariantIdx>,
layout: &LayoutS,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
let flds: Vec<_> =
Expand Down Expand Up @@ -1554,7 +1554,7 @@ impl<'tcx> GotocCtx<'tcx> {
ty: Ty<'tcx>,
adtdef: &'tcx AdtDef,
subst: &'tcx InternalSubsts<'tcx>,
variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
variants: &IndexVec<VariantIdx, LayoutS>,
) -> Type {
let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
let mangled_name = self.ty_mangled_name(ty);
Expand All @@ -1573,7 +1573,7 @@ impl<'tcx> GotocCtx<'tcx> {

pub(crate) fn variant_min_offset(
&self,
variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
variants: &IndexVec<VariantIdx, LayoutS>,
) -> Option<Size> {
variants
.iter()
Expand Down Expand Up @@ -1657,7 +1657,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_name: InternedString,
def: &'tcx AdtDef,
subst: &'tcx InternalSubsts<'tcx>,
layouts: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
layouts: &IndexVec<VariantIdx, LayoutS>,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
def.variants()
Expand Down Expand Up @@ -1689,7 +1689,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_name: InternedString,
case: &VariantDef,
subst: &'tcx InternalSubsts<'tcx>,
variant: &LayoutS<VariantIdx>,
variant: &LayoutS,
initial_offset: Size,
) -> Type {
let case_name = format!("{name}::{}", case.name);
Expand Down
3 changes: 2 additions & 1 deletion kani-compiler/src/session.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use crate::parser;
use clap::ArgMatches;
use rustc_errors::{
emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
ColorConfig, Diagnostic,
ColorConfig, Diagnostic, TerminalUrl,
};
use std::panic;
use std::str::FromStr;
Expand Down Expand Up @@ -57,6 +57,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
None,
false,
false,
TerminalUrl::No,
);
let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
emitter.emit_diagnostic(&diagnostic);
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-02-05"
channel = "nightly-2023-02-16"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit d4966cd

Please sign in to comment.