Skip to content

Commit

Permalink
Upgrade toolchain to 2024-03-11 (#3071)
Browse files Browse the repository at this point in the history
Relevant upstream changes:

rust-lang/rust#120675: An intrinsic `Symbol` is
now wrapped in a `IntrinsicDef` struct, so the relevant part of the code
needed to be updated.
rust-lang/rust#121464: The second argument of
the `create_wrapper_file` function changed from a vector to a string.
rust-lang/rust#121662: `NullOp::DebugAssertions`
was renamed to `NullOp::UbCheck` and it now has data (currently unused
by Kani)
rust-lang/rust#121728: Introduces `F16` and
`F128`, so needed to add stubs for them
rust-lang/rust#121969: `parse_sess` was renamed
to `psess`, so updated the relevant code.
rust-lang/rust#122059: The
`is_val_statically_known` intrinsic is now used in some `core::fmt`
code, so had to handle it in (codegen'ed to false).
rust-lang/rust#122233: This added a new
`retag_box_to_raw` intrinsic. This is an operation that is primarily
relevant for stacked borrows. For Kani, we just return the pointer.

Resolves #3057
  • Loading branch information
zhassan-aws authored Mar 12, 2024
1 parent a8db120 commit e7a4d83
Show file tree
Hide file tree
Showing 11 changed files with 39 additions and 15 deletions.
19 changes: 19 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -474,6 +474,11 @@ impl<'tcx> GotocCtx<'tcx> {
let binop_stmt = codegen_intrinsic_binop!(sub);
self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
}
"is_val_statically_known" => {
// Returning false is sound according do this intrinsic's documentation:
// https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html
self.codegen_expr_to_place_stable(place, Expr::c_false())
}
"likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0)),
"log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)),
"log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)),
Expand Down Expand Up @@ -506,6 +511,7 @@ impl<'tcx> GotocCtx<'tcx> {
"ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
"ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc),
"raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
"retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc),
"rintf32" => codegen_simple_intrinsic!(Rintf),
"rintf64" => codegen_simple_intrinsic!(Rint),
"rotate_left" => codegen_intrinsic_binop!(rol),
Expand Down Expand Up @@ -1259,6 +1265,19 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_expr_to_place_stable(p, e)
}

// This is an operation that is primarily relevant for stacked borrow
// checks. For Kani, we simply return the pointer.
fn codegen_retag_box_to_raw(
&mut self,
mut fargs: Vec<Expr>,
p: &Place,
_loc: Location,
) -> Stmt {
assert_eq!(fargs.len(), 1, "raw_box_to_box expected one argument");
let arg = fargs.remove(0);
self.codegen_expr_to_place_stable(p, arg)
}

fn vtable_info(
&mut self,
info: VTableInfo,
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 @@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
.bytes(),
Type::size_t(),
),
NullOp::DebugAssertions => Expr::c_false(),
NullOp::UbCheck(_) => Expr::c_false(),
}
}
Rvalue::ShallowInitBox(ref operand, content_ty) => {
Expand Down
6 changes: 6 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -542,6 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Float(k) => match k {
FloatTy::F32 => Type::float(),
FloatTy::F64 => Type::double(),
// `F16` and `F128` are not yet handled.
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
FloatTy::F16 | FloatTy::F128 => unimplemented!(),
},
ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
ty::Adt(def, subst) => {
Expand Down Expand Up @@ -1346,6 +1349,9 @@ impl<'tcx> GotocCtx<'tcx> {

Primitive::F32 => self.tcx.types.f32,
Primitive::F64 => self.tcx.types.f64,
// `F16` and `F128` are not yet handled.
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
Primitive::F16 | Primitive::F128 => unimplemented!(),
Primitive::Pointer(_) => Ty::new_ptr(
self.tcx,
ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -397,7 +397,7 @@ impl CodegenBackend for GotocCodegenBackend {
let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps);
let (metadata, _metadata_position) = create_wrapper_file(
sess,
b".rmeta".to_vec(),
".rmeta".to_string(),
codegen_results.metadata.raw_data(),
);
let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME);
Expand Down
7 changes: 3 additions & 4 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -611,9 +611,8 @@ fn parse_modify_values<'a>(
let mut iter = t.trees();
std::iter::from_fn(move || {
let tree = iter.next()?;
let wrong_token_err = || {
tcx.sess.parse_sess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.")
};
let wrong_token_err =
|| tcx.sess.psess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.");
let result = match tree {
TokenTree::Token(token, _) => {
if let TokenKind::Ident(id, _) = &token.kind {
Expand All @@ -640,7 +639,7 @@ fn parse_modify_values<'a>(
match iter.next() {
None | Some(comma_tok!()) => (),
Some(not_comma) => {
tcx.sess.parse_sess.dcx.span_err(
tcx.sess.psess.dcx.span_err(
not_comma.span(),
"Unexpected token, expected end of attribute or comma",
);
Expand Down
8 changes: 4 additions & 4 deletions kani-compiler/src/kani_middle/intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use rustc_index::IndexVec;
use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind};
use rustc_middle::mir::{Local, LocalDecl};
use rustc_middle::ty::{self, Ty, TyCtxt};
use rustc_middle::ty::{Const, GenericArgsRef};
use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef};
use rustc_span::source_map::Spanned;
use rustc_span::symbol::{sym, Symbol};
use tracing::{debug, trace};
Expand All @@ -33,8 +33,8 @@ impl<'tcx> ModelIntrinsics<'tcx> {
let terminator = block.terminator_mut();
if let TerminatorKind::Call { func, args, .. } = &mut terminator.kind {
let func_ty = func.ty(&self.local_decls, self.tcx);
if let Some((intrinsic_name, generics)) = resolve_rust_intrinsic(self.tcx, func_ty)
{
if let Some((intrinsic, generics)) = resolve_rust_intrinsic(self.tcx, func_ty) {
let intrinsic_name = intrinsic.name;
trace!(?func, ?intrinsic_name, "run_pass");
if intrinsic_name == sym::simd_bitmask {
self.replace_simd_bitmask(func, args, generics)
Expand Down Expand Up @@ -99,7 +99,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx>
fn resolve_rust_intrinsic<'tcx>(
tcx: TyCtxt<'tcx>,
func_ty: Ty<'tcx>,
) -> Option<(Symbol, GenericArgsRef<'tcx>)> {
) -> Option<(IntrinsicDef, GenericArgsRef<'tcx>)> {
if let ty::FnDef(def_id, args) = *func_ty.kind() {
if let Some(symbol) = tcx.intrinsic(def_id) {
return Some((symbol, args));
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -515,8 +515,8 @@ fn collect_alloc_items(alloc_id: AllocId) -> Vec<MonoItem> {
}

#[cfg(debug_assertions)]
#[allow(dead_code)]
mod debug {
#![allow(dead_code)]

use std::fmt::{Display, Formatter};
use std::{
Expand Down
2 changes: 1 addition & 1 deletion kani-driver/src/assess/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ fn reconstruct_metadata_structure(
}
if !package_artifacts.is_empty() {
let mut merged = crate::metadata::merge_kani_metadata(package_artifacts);
merged.crate_name = package.name.clone();
merged.crate_name.clone_from(&package.name);
package_metas.push(merged);
}
}
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-2024-03-01"
channel = "nightly-2024-03-11"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/variant/expected
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
coverage/unreachable/variant/main.rs, 15, PARTIAL
coverage/unreachable/variant/main.rs, 15, FULL
coverage/unreachable/variant/main.rs, 16, NONE
coverage/unreachable/variant/main.rs, 17, NONE
coverage/unreachable/variant/main.rs, 18, FULL
Expand Down
2 changes: 1 addition & 1 deletion tools/bookrunner/librustdoc/html/markdown.rs
Original file line number Diff line number Diff line change
Expand Up @@ -225,7 +225,7 @@ impl LangString {
let mut data = LangString::default();
let mut ignores = vec![];

data.original = string.to_owned();
string.clone_into(&mut data.original);

for token in Self::tokens(string) {
match token {
Expand Down

0 comments on commit e7a4d83

Please sign in to comment.