diff --git a/.cargo/config.toml b/.cargo/config.toml index 9bb4e0808345..321a3ec14cb7 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -20,6 +20,7 @@ KANI_SYSROOT ={value = "target/kani", relative = true} KANI_BUILD_LIBS ={value = "target/build-libs", relative = true} # Build Kani library without `build-std`. KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true} +RUSTC_BOOTSTRAP ={value="1"} [target.'cfg(all())'] rustflags = [ # Global lints/warnings. Need to use underscore instead of -. diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index f925bfcfe58e..a0c1f211b5e2 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -6,7 +6,7 @@ use super::{Expr, Location, Symbol, Type}; use std::fmt::Display; -#[derive(Debug, Clone, Copy, PartialEq)] +#[derive(Debug, Clone, Copy)] pub enum BuiltinFn { Abort, Assert, diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index 56578cc87aa4..15cc0afa8902 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -84,7 +84,7 @@ use std::collections::HashMap; use std::fs::File; use std::hash::Hash; use std::io::{self, BufReader}; -use std::io::{BufWriter, Bytes, Error, Read, Write}; +use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write}; use std::path::Path; /// Writes a symbol table to a file in goto binary format in version 6. @@ -557,7 +557,7 @@ where R: Read, { /// Stream of bytes from which GOTO objects are read. - bytes: Bytes>, + bytes: Bytes, /// Numbering for ireps numbering: IrepNumbering, @@ -584,9 +584,8 @@ where /// Constructor. The reader is moved into this object and cannot be used /// afterwards. fn new(reader: R) -> Self { - let buffered_reader = BufReader::new(reader); GotoBinaryDeserializer { - bytes: buffered_reader.bytes(), + bytes: reader.bytes(), numbering: IrepNumbering::new(), string_count: Vec::new(), string_map: Vec::new(), @@ -598,9 +597,12 @@ where /// Returns Err if the found value is not the expected value. fn expect(found: T, expected: T) -> io::Result { if found != expected { - return Err(Error::other(format!( - "Invalid goto binary input: expected {expected} in byte stream, found {found} instead)" - ))); + return Err(Error::new( + ErrorKind::Other, + format!( + "Invalid goto binary input: expected {expected} in byte stream, found {found} instead)" + ), + )); } Ok(found) } @@ -658,7 +660,10 @@ where match self.bytes.next() { Some(Ok(u)) => Ok(u), Some(Err(error)) => Err(error), - None => Err(Error::other("Invalid goto binary input: unexpected end of input")), + None => Err(Error::new( + ErrorKind::Other, + "Invalid goto binary input: unexpected end of input", + )), } } @@ -672,7 +677,8 @@ where match self.bytes.next() { Some(Ok(u)) => { if shift >= max_shift { - return Err(Error::other( + return Err(Error::new( + ErrorKind::Other, "Invalid goto binary input: serialized value is too large to fit in usize", )); }; @@ -686,7 +692,10 @@ where return Err(error); } None => { - return Err(Error::other("Invalid goto binary input: unexpected end of input")); + return Err(Error::new( + ErrorKind::Other, + "Invalid goto binary input: unexpected end of input", + )); } } } @@ -712,7 +721,10 @@ where return Ok(numbered); } Err(error) => { - return Err(Error::other(error.to_string())); + return Err(Error::new( + ErrorKind::Other, + error.to_string(), + )); } } } @@ -726,7 +738,8 @@ where return Err(error); } None => { - return Err(Error::other( + return Err(Error::new( + ErrorKind::Other, "Invalid goto binary input: unexpected end of input", )); } @@ -744,7 +757,8 @@ where } None => { // No more bytes left - return Err(Error::other( + return Err(Error::new( + ErrorKind::Other, "Invalid goto binary input: unexpected end of input", )); } @@ -775,7 +789,8 @@ where match c { b'S' => { if sub_done { - return Err(Error::other( + return Err(Error::new( + ErrorKind::Other, "Invalid goto binary input: incorrect binary structure", )); } @@ -801,10 +816,13 @@ where return Ok(numbered); } other => { - return Err(Error::other(format!( - "Invalid goto binary input: unexpected character in input stream {}", - other as char - ))); + return Err(Error::new( + ErrorKind::Other, + format!( + "Invalid goto binary input: unexpected character in input stream {}", + other as char + ), + )); } } } @@ -859,7 +877,8 @@ where let shifted_flags = flags >> 16; if shifted_flags != 0 { - return Err(Error::other( + return Err(Error::new( + ErrorKind::Other, "incorrect binary format: true bits remain in decoded symbol flags", )); } @@ -897,10 +916,13 @@ where // Read goto binary version let goto_binary_version = self.read_usize_varenc()?; if goto_binary_version != 6 { - return Err(Error::other(format!( - "Unsupported GOTO binary version: {}. Supported version: {}", - goto_binary_version, 6 - ))); + return Err(Error::new( + ErrorKind::Other, + format!( + "Unsupported GOTO binary version: {}. Supported version: {}", + goto_binary_version, 6 + ), + )); } Ok(()) } diff --git a/cprover_bindings/src/machine_model.rs b/cprover_bindings/src/machine_model.rs index 463fe8f047e6..31427a83a629 100644 --- a/cprover_bindings/src/machine_model.rs +++ b/cprover_bindings/src/machine_model.rs @@ -45,7 +45,6 @@ pub enum RoundingMode { Downward = 1, Upward = 2, TowardsZero = 3, - ToAway = 4, } impl From for BigInt { diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 2fa8b54094fc..9f3495da0adc 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -180,6 +180,8 @@ minnumf32 | Yes | | minnumf64 | Yes | | move_val_init | No | | mul_with_overflow | Yes | | +nearbyintf32 | Yes | | +nearbyintf64 | Yes | | needs_drop | Yes | | nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | @@ -196,10 +198,8 @@ ptr_guaranteed_eq | Yes | | ptr_guaranteed_ne | Yes | | ptr_offset_from | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-4) | raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) | -round_ties_even_f16 | No | | -round_ties_even_f32 | Yes | | -round_ties_even_f64 | Yes | | -round_ties_even_f128 | No | | +rintf32 | Yes | | +rintf64 | Yes | | rotate_left | Yes | | rotate_right | Yes | | roundf32 | Yes | | diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 219bc48c4d91..546a3aa4f127 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -813,7 +813,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let disambiguator = CharonDisambiguator::new(data.disambiguator as usize); use rustc_hir::definitions::DefPathData; match &data.data { - DefPathData::TypeNs(Some(symbol)) => { + DefPathData::TypeNs(symbol) => { error_assert!(self, span, data.disambiguator == 0); // Sanity check name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator)); } @@ -956,7 +956,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let disambiguator = CharonDisambiguator::new(data.disambiguator as usize); use rustc_hir::definitions::DefPathData; match &data.data { - DefPathData::TypeNs(Some(symbol)) => { + DefPathData::TypeNs(symbol) => { error_assert!(self, span, data.disambiguator == 0); // Sanity check name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator)); } @@ -1063,7 +1063,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let disambiguator = CharonDisambiguator::new(data.disambiguator as usize); use rustc_hir::definitions::DefPathData; match &data.data { - DefPathData::TypeNs(Some(symbol)) => { + DefPathData::TypeNs(symbol) => { error_assert!(self, span, data.disambiguator == 0); // Sanity check name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator)); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index d3d4481bf258..254fc854e8b5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -63,7 +63,9 @@ impl GotocCtx<'_> { // Return item tagged with `#[kanitool::recursion_tracker]` let mut recursion_trackers = items.iter().filter_map(|item| { let MonoItem::Static(static_item) = item else { return None }; - if !static_item.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty() + if !static_item + .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()]) + .is_empty() { let span = static_item.span(); let loc = self.codegen_span_stable(span); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 7def214fc5a8..07e19c4f132c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -227,7 +227,7 @@ impl GotocCtx<'_> { pub mod rustc_smir { use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region}; use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::BasicCoverageBlock; + use rustc_middle::mir::coverage::CovTerm; use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; @@ -243,16 +243,16 @@ pub mod rustc_smir { coverage_opaque: &CoverageOpaque, instance: Instance, ) -> Option<(SourceRegion, Filename)> { - let bcb = parse_coverage_opaque(coverage_opaque); - region_from_coverage(tcx, bcb, instance) + let cov_term = parse_coverage_opaque(coverage_opaque); + region_from_coverage(tcx, cov_term, instance) } - /// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object. + /// Retrieves the `SourceRegion` associated with a `CovTerm` object. /// /// Note: This function could be in the internal `rustc` impl for `Coverage`. pub fn region_from_coverage( tcx: TyCtxt<'_>, - coverage: BasicCoverageBlock, + coverage: CovTerm, instance: Instance, ) -> Option<(SourceRegion, Filename)> { // We need to pull the coverage info from the internal MIR instance. @@ -264,10 +264,10 @@ pub mod rustc_smir { if let Some(cov_info) = &body.function_coverage_info { // Iterate over the coverage mappings and match with the coverage term. for mapping in &cov_info.mappings { - let Code { bcb } = mapping.kind else { unreachable!() }; + let Code(term) = mapping.kind else { unreachable!() }; let source_map = tcx.sess.source_map(); let file = source_map.lookup_source_file(cov_info.body_span.lo()); - if bcb == coverage { + if term == coverage { return Some(( make_source_region(source_map, cov_info, &file, mapping.span).unwrap(), rustc_internal::stable(cov_info.body_span).get_filename(), @@ -278,17 +278,25 @@ pub mod rustc_smir { None } - /// Parse a `CoverageOpaque` item and return the corresponding `BasicCoverageBlock`: - fn parse_coverage_opaque(coverage_opaque: &Opaque) -> BasicCoverageBlock { + /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`: + /// + /// + /// At present, a `CovTerm` can be one of the following: + /// - `CounterIncrement()`: A physical counter. + /// - `ExpressionUsed()`: An expression-based counter. + /// - `Zero`: A counter with a constant zero value. + fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm { let coverage_str = coverage_opaque.to_string(); - if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") { + if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { + let (num_str, _rest) = rest.split_once(')').unwrap(); + let num = num_str.parse::().unwrap(); + CovTerm::Counter(num.into()) + } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); - BasicCoverageBlock::from_u32(num) + CovTerm::Expression(num.into()) } else { - // When the coverage statement is injected into mir_body, it always has the form CoverageKind::VirtualCounter { bcb } - // https://github.com/rust-lang/rust/pull/136053/files#diff-c99ec9a281dce4a381fa7e11cf2d04f55dba5573d1d14389d47929fe0a154d24R209-R212 - unreachable!(); + CovTerm::Zero } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 88f4763be49e..bbdc0be7910a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -414,6 +414,8 @@ impl GotocCtx<'_> { Intrinsic::MulWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc) } + Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf), + Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint), Intrinsic::NeedsDrop => codegen_intrinsic_const!(), Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf), Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow), @@ -423,13 +425,12 @@ impl GotocCtx<'_> { Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), + Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), + Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint), Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol), Intrinsic::RotateRight => codegen_intrinsic_binop!(ror), Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf), Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round), - Intrinsic::RoundTiesEvenF32 | Intrinsic::RoundTiesEvenF64 => { - self.codegen_round_to_integral(cbmc::RoundingMode::ToNearest, fargs, place, loc) - } Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add), Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub), Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf), @@ -637,23 +638,6 @@ impl GotocCtx<'_> { dividend_is_int_min.and(divisor_is_minus_one).not() } - // Builds a floatbv_round_to_integral expression with specified cbmc::RoundingMode. - fn codegen_round_to_integral( - &mut self, - rounding_mode: cbmc::RoundingMode, - mut fargs: Vec, - place: &Place, - loc: Location, - ) -> Stmt { - let place_ty = self.place_ty_stable(place); - let result_type = self.codegen_ty_stable(place_ty); - let f = fargs.remove(0); - assert!(fargs.is_empty()); - let rm = Expr::int_constant(rounding_mode, Type::c_int()); - let expr = Expr::floatbv_round_to_integral(f, rm, result_type); - self.codegen_expr_to_place_stable(place, expr, loc) - } - /// Intrinsics of the form *_with_overflow fn codegen_op_with_overflow( &mut self, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 721082c20bd6..8cabd10c87ad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -12,9 +12,9 @@ use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type}; -use rustc_abi::{TagEncoding, Variants}; use rustc_middle::ty::layout::LayoutOf; use rustc_smir::rustc_internal; +use rustc_target::abi::{TagEncoding, Variants}; use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem}; use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx}; use tracing::{debug, trace, warn}; @@ -150,7 +150,7 @@ impl ProjectedPlace { goto_expr: Expr, ty: Ty, ctx: &mut GotocCtx, - ) -> Result> { + ) -> Result { Self::try_new(goto_expr, TypeOrVariant::Type(ty), None, None, ctx) } @@ -160,7 +160,7 @@ impl ProjectedPlace { fat_ptr_goto_expr: Option, fat_ptr_mir_typ: Option, ctx: &mut GotocCtx, - ) -> Result> { + ) -> Result { if let Some(fat_ptr) = &fat_ptr_goto_expr { assert!( fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table), @@ -183,12 +183,12 @@ impl ProjectedPlace { if !(expr_ty.is_integer() && ty_from_mir.is_struct_tag()) { debug_assert!(false, "{}", msg); } - return Err(Box::new(UnimplementedData::new( + return Err(UnimplementedData::new( "Projection mismatch", "https://github.com/model-checking/kani/issues/277", ty_from_mir, *goto_expr.location(), - ))); + )); } assert!( @@ -236,7 +236,7 @@ impl GotocCtx<'_> { parent_ty_or_var: TypeOrVariant, field_idx: FieldIdx, field_ty_or_var: TypeOrVariant, - ) -> Result> { + ) -> Result { match parent_ty_or_var { TypeOrVariant::Type(parent_ty) => { match parent_ty.kind() { @@ -286,12 +286,12 @@ impl GotocCtx<'_> { TyKind::RigidTy(RigidTy::CoroutineClosure(def, args)) => { let typ = Ty::new_coroutine_closure(def, args); let goto_typ = self.codegen_ty_stable(typ); - Err(Box::new(UnimplementedData::new( + Err(UnimplementedData::new( "Coroutine closures", "https://github.com/model-checking/kani/issues/3783", goto_typ, *parent_expr.location(), - ))) + )) } TyKind::RigidTy(RigidTy::Str) | TyKind::RigidTy(RigidTy::Array(_, _)) @@ -414,10 +414,10 @@ impl GotocCtx<'_> { /// the return value is the expression after. fn codegen_projection( &mut self, - before: Result>, + before: Result, proj: &ProjectionElem, loc: Location, - ) -> Result> { + ) -> Result { let before = before?; trace!(?before, ?proj, "codegen_projection"); match proj { @@ -550,12 +550,12 @@ impl GotocCtx<'_> { let typ = Ty::try_new_array(ty, subarray_len).unwrap(); let goto_typ = self.codegen_ty_stable(typ); // unimplemented - Err(Box::new(UnimplementedData::new( + Err(UnimplementedData::new( "Sub-array binding", "https://github.com/model-checking/kani/issues/707", goto_typ, *before.goto_expr.location(), - ))) + )) } TyKind::RigidTy(RigidTy::Slice(_)) => { let len = if *from_end { @@ -722,7 +722,7 @@ impl GotocCtx<'_> { &mut self, place: &Place, loc: Location, - ) -> Result> { + ) -> Result { debug!(?place, "codegen_place"); let initial_expr = self.codegen_local(place.local, loc); let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local)); @@ -734,12 +734,12 @@ impl GotocCtx<'_> { .iter() .fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj, loc)); match result { - Err(data) => Err(Box::new(UnimplementedData::new( + Err(data) => Err(UnimplementedData::new( &data.operation, &data.bug_url, self.codegen_ty_stable(self.place_ty_stable(place)), data.loc, - ))), + )), _ => result, } } @@ -770,7 +770,7 @@ impl GotocCtx<'_> { offset: u64, min_length: u64, from_end: bool, - ) -> Result> { + ) -> Result { match before.mir_typ().kind() { //TODO, ask on zulip if we can ever have from_end here? TyKind::RigidTy(RigidTy::Array(elemt, length)) => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f2327b51b6ad..ed7382e16fc6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -18,9 +18,9 @@ use cbmc::goto_program::{ }; use cbmc::{InternString, InternedString, btree_string_map}; use num::bigint::BigInt; -use rustc_abi::{FieldsShape, TagEncoding, Variants}; use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry}; use rustc_smir::rustc_internal; +use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; use stable_mir::abi::{Primitive, Scalar, ValueAbi}; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ @@ -667,7 +667,7 @@ impl GotocCtx<'_> { assert!(operands.len() == 2); let typ = self.codegen_ty_stable(res_ty); let layout = self.layout_of_stable(res_ty); - assert!(layout.ty.is_raw_ptr()); + assert!(layout.ty.is_unsafe_ptr()); let data = self.codegen_operand_stable(&operands[0]); match pointee_ty.kind() { TyKind::RigidTy(RigidTy::Slice(inner_ty)) => { @@ -851,7 +851,7 @@ impl GotocCtx<'_> { .bytes(), Type::size_t(), ), - NullOp::ContractChecks | NullOp::UbChecks => Expr::c_false(), + NullOp::UbChecks => Expr::c_false(), } } Rvalue::ShallowInitBox(ref operand, content_ty) => { @@ -1002,10 +1002,8 @@ impl GotocCtx<'_> { // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247 // See also the cranelift backend: // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116 - let offset: rustc_abi::Size = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => { - offsets[rustc_abi::FieldIdx::from_usize(0)] - } + let offset = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], _ => unreachable!("niche encoding must have arbitrary fields"), }; @@ -1507,10 +1505,8 @@ impl GotocCtx<'_> { |ctx, var| { // Build the vtable, using Rust's vtable_entries to determine field order let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() { - let trait_ref = - rustc_internal::internal(ctx.tcx, principal.with_self_ty(src_mir_type)); - let trait_ref = ctx.tcx.instantiate_bound_regions_with_erased(trait_ref); - ctx.tcx.vtable_entries(trait_ref) + let trait_ref_binder = principal.with_self_ty(src_mir_type); + ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder)) } else { TyCtxt::COMMON_VTABLE_ENTRIES }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 0ffa893056be..913e860b55cc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -7,11 +7,10 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_cov use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; -use rustc_abi::Size; -use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{List, TypingEnv}; use rustc_smir::rustc_internal; +use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::{ @@ -272,9 +271,6 @@ impl GotocCtx<'_> { ) } // For all other assert kind we can get the static message. - AssertMessage::NullPointerDereference => { - (msg.description().unwrap(), PropertyClass::SafetyCheck) - } AssertMessage::Overflow { .. } | AssertMessage::OverflowNeg { .. } | AssertMessage::DivisionByZero { .. } @@ -351,10 +347,8 @@ impl GotocCtx<'_> { } TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { if *untagged_variant != variant_index_internal { - let offset: Size = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => { - offsets[rustc_abi::FieldIdx::from_usize(0)] - } + let offset = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], _ => unreachable!("niche encoding must have arbitrary fields"), }; let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal); @@ -573,7 +567,7 @@ impl GotocCtx<'_> { let ty = self.operand_ty_stable(op); if ty.kind().is_bool() { Some(self.codegen_operand_stable(op).cast_to(Type::c_bool())) - } else if arg_abi.is_none_or(|abi| abi.mode != PassMode::Ignore) { + } else if arg_abi.map_or(true, |abi| abi.mode != PassMode::Ignore) { Some(self.codegen_operand_stable(op)) } else { None diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 84d2c52afba4..9598e9feecd2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -4,10 +4,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, SymbolTable, Type}; use cbmc::utils::aggr_tag; use cbmc::{InternString, InternedString}; -use rustc_abi::{ - BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size, - TagEncoding, TyAndLayout, VariantIdx, Variants, -}; use rustc_ast::ast::Mutability; use rustc_index::IndexVec; use rustc_middle::ty::GenericArgsRef; @@ -21,6 +17,10 @@ use rustc_middle::ty::{ use rustc_middle::ty::{List, TypeFoldable}; use rustc_smir::rustc_internal; use rustc_span::def_id::DefId; +use rustc_target::abi::{ + BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size, + TagEncoding, TyAndLayout, VariantIdx, Variants, +}; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::Body; use stable_mir::mir::mono::Instance as InstanceStable; @@ -371,7 +371,6 @@ impl<'tcx> GotocCtx<'tcx> { // The virtual methods on the trait ref. Some auto traits have no methods. if let Some(principal) = binder.principal() { let poly = principal.with_self_ty(self.tcx, t); - let poly = self.tcx.instantiate_bound_regions_with_erased(poly); let poly = self.tcx.erase_regions(poly); let mut flds = self .tcx @@ -718,7 +717,7 @@ impl<'tcx> GotocCtx<'tcx> { let mut final_fields = Vec::with_capacity(flds.len()); let mut offset = initial_offset; for idx in layout.fields.index_by_increasing_offset() { - let fld_offset = offsets[rustc_abi::FieldIdx::from(idx)]; + let fld_offset = offsets[idx.into()]; let (fld_name, fld_ty) = &flds[idx]; if let Some(padding) = self.codegen_struct_padding(offset, fld_offset, final_fields.len()) @@ -1472,7 +1471,7 @@ impl<'tcx> GotocCtx<'tcx> { debug! {"handling simd with layout {:?}", layout}; let (element, size) = match layout { - SimdVector { element, count } => (element, count), + Vector { element, count } => (element, count), _ => unreachable!(), }; @@ -1556,9 +1555,9 @@ impl<'tcx> GotocCtx<'tcx> { let components = fields_shape .index_by_increasing_offset() .map(|idx| { - let fidx = FieldIdx::from(idx); - let name = fields[fidx].name.to_string().intern(); - let field_ty = fields[fidx].ty(ctx.tcx, adt_args); + let idx = idx.into(); + let name = fields[idx].name.to_string().intern(); + let field_ty = fields[idx].ty(ctx.tcx, adt_args); let typ = if !ctx.is_zst(field_ty) { last_type.clone() } else { diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 8ed90b2c975e..6b32c53ccfb0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -23,7 +23,6 @@ use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; -use rustc_abi::Endian; use rustc_codegen_ssa::back::archive::{ ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, }; @@ -41,6 +40,7 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; +use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; @@ -420,7 +420,7 @@ impl CodegenBackend for GotocCodegenBackend { let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); let local_crate_name = codegen_results.crate_info.local_crate_name; // Create the rlib if one was requested. - if requested_crate_types.contains(&CrateType::Rlib) { + if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) { link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 79410bd3373e..0e5e72af70b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -26,7 +26,6 @@ use cbmc::goto_program::{ }; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; -use rustc_abi::{HasDataLayout, TargetDataLayout}; use rustc_data_structures::fx::FxHashMap; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ @@ -36,7 +35,8 @@ use rustc_middle::ty::layout::{ use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_span::Span; use rustc_span::source_map::respan; -use rustc_target::callconv::FnAbi; +use rustc_target::abi::call::FnAbi; +use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::Body; use stable_mir::mir::mono::Instance; use stable_mir::ty::Allocation; diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 5d9ab8221453..f58a40bf8cb6 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -86,6 +86,8 @@ pub enum Intrinsic { MinNumF32, MinNumF64, MulWithOverflow, + NearbyIntF32, + NearbyIntF64, NeedsDrop, PowF32, PowF64, @@ -97,12 +99,12 @@ pub enum Intrinsic { PtrOffsetFromUnsigned, RawEq, RetagBoxToRaw, + RintF32, + RintF64, RotateLeft, RotateRight, RoundF32, RoundF64, - RoundTiesEvenF32, - RoundTiesEvenF64, SaturatingAdd, SaturatingSub, SinF32, @@ -674,6 +676,10 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::MinNumF32) } + "nearbyintf32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::NearbyIntF32) + } "powf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::PowF32) @@ -682,13 +688,13 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::PowIF32) } - "roundf32" => { + "rintf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::RoundF32) + Some(Intrinsic::RintF32) } - "round_ties_even_f32" => { + "roundf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::RoundTiesEvenF32) + Some(Intrinsic::RoundF32) } "sinf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); @@ -764,6 +770,10 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::MinNumF64) } + "nearbyintf64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::NearbyIntF64) + } "powf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::PowF64) @@ -772,13 +782,13 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::PowIF64) } - "roundf64" => { + "rintf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::RoundF64) + Some(Intrinsic::RintF64) } - "round_ties_even_f64" => { + "roundf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::RoundTiesEvenF64) + Some(Intrinsic::RoundF64) } "sinf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index e4bfba3113b0..253a9b88a52c 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -3,7 +3,7 @@ //! This module defines all compiler extensions that form the Kani compiler. //! -//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler`]), +//! The [KaniCompiler] can be used across multiple rustc driver runs ([RunCompiler::run()]), //! which is used to implement stubs. //! //! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will @@ -25,7 +25,7 @@ use crate::kani_queries::QueryDb; use crate::session::init_session; use clap::Parser; use rustc_codegen_ssa::traits::CodegenBackend; -use rustc_driver::{Callbacks, Compilation, run_compiler}; +use rustc_driver::{Callbacks, Compilation, RunCompiler}; use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::ErrorOutputType; @@ -34,7 +34,7 @@ use std::sync::{Arc, Mutex}; use tracing::debug; /// Run the Kani flavour of the compiler. -/// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]). +/// This may require multiple runs of the rustc driver ([RunCompiler::run]). pub fn run(args: Vec) { let mut kani_compiler = KaniCompiler::new(); kani_compiler.run(args); @@ -96,7 +96,10 @@ impl KaniCompiler { /// actually invoke the rust compiler multiple times. pub fn run(&mut self, args: Vec) { debug!(?args, "run_compilation_session"); - run_compiler(&args, self); + let queries = self.queries.clone(); + let mut compiler = RunCompiler::new(&args, self); + compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); + compiler.run(); } } @@ -105,10 +108,6 @@ impl Callbacks for KaniCompiler { /// Configure the [KaniCompiler] `self` object during the [CompilationStage::Init]. fn config(&mut self, config: &mut Config) { let mut args = vec!["kani-compiler".to_string()]; - config.make_codegen_backend = Some(Box::new({ - let queries = self.queries.clone(); - move |_cfg| backend(queries) - })); args.extend(config.opts.cg.llvm_args.iter().cloned()); let args = Arguments::parse_from(args); init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index f0828dace441..b232db8feecb 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -149,7 +149,7 @@ impl From<&Terminator> for Key { TerminatorKind::Drop { .. } => Key("Drop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::InlineAsm { .. } => Key("InlineAsm"), - TerminatorKind::Resume => Key("Resume"), + TerminatorKind::Resume { .. } => Key("Resume"), TerminatorKind::Return => Key("Return"), TerminatorKind::SwitchInt { .. } => Key("SwitchInt"), TerminatorKind::Unreachable => Key("Unreachable"), diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 20d5f3ad6a4b..e6a61e84a0b0 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -8,7 +8,7 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr}; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId}; +use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; @@ -214,7 +214,7 @@ impl<'tcx> KaniAttributes<'tcx> { .resolve_from_mod(name.as_str()) .map_err(|e| { let mut err = self.tcx.dcx().struct_span_err( - attr.span(), + attr.span, format!( "Failed to resolve replacement function {}: {e}", name.as_str() @@ -229,7 +229,7 @@ impl<'tcx> KaniAttributes<'tcx> { err.emit(); }) .ok()?; - Some((name, def, attr.span())) + Some((name, def, attr.span)) }) .collect() } @@ -247,10 +247,10 @@ impl<'tcx> KaniAttributes<'tcx> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { let name = expect_key_string_value(self.tcx.sess, target).ok()?; self.resolve_from_mod(name.as_str()) - .map(|ok| (name, ok, target.span())) + .map(|ok| (name, ok, target.span)) .map_err(|resolve_err| { let mut err = self.tcx.dcx().struct_span_err( - target.span(), + target.span, format!( "Failed to resolve checking function {} because {resolve_err}", name.as_str() @@ -347,7 +347,7 @@ impl<'tcx> KaniAttributes<'tcx> { // Check that all attributes are correctly used and well formed. let is_harness = self.is_proof_harness(); for (&kind, attrs) in self.map.iter() { - let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span(), msg); + let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg); if !is_harness && kind.is_harness_only() { local_error(format!( @@ -462,7 +462,7 @@ impl<'tcx> KaniAttributes<'tcx> { kind.as_ref() ); if let Some(attr) = self.map.get(&kind).unwrap().first() { - self.tcx.dcx().span_err(attr.span(), msg); + self.tcx.dcx().span_err(attr.span, msg); } else { self.tcx.dcx().err(msg); } @@ -657,7 +657,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Check that if this item is tagged with a proof_attribute, it is a valid harness. fn check_proof_attribute(&self, kind: KaniAttributeKind, proof_attribute: &Attribute) { - let span = proof_attribute.span(); + let span = proof_attribute.span; let tcx = self.tcx; if let KaniAttributeKind::Proof = kind { expect_no_args(tcx, kind, proof_attribute); @@ -730,7 +730,7 @@ fn expect_key_string_value( sess: &Session, attr: &Attribute, ) -> Result { - let span = attr.span(); + let span = attr.span; let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else { return Err(sess .dcx() @@ -754,7 +754,7 @@ fn expect_single<'a>( .expect(&format!("expected at least one attribute {} in {attributes:?}", kind.as_ref())); if attributes.len() > 1 { tcx.dcx().span_err( - attr.span(), + attr.span, format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()), ); } @@ -785,7 +785,7 @@ impl UnstableAttrParseError<'_> { fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed { tcx.dcx() .struct_span_err( - self.attr.span(), + self.attr.span, format!("failed to parse `#[kani::unstable_feature]`: {}", self.reason), ) .with_note(format!( @@ -828,7 +828,7 @@ impl<'a> TryFrom<&'a Attribute> for UnstableAttribute { fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) { if !attr.is_word() { tcx.dcx() - .struct_span_err(attr.span(), format!("unexpected argument for `{}`", kind.as_ref())) + .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref())) .with_help("remove the extra argument") .emit(); } @@ -841,7 +841,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { None => { // There are no integers or too many arguments given to the attribute tcx.dcx().span_err( - attr.span(), + attr.span, "invalid argument for `unwind` attribute, expected an integer", ); None @@ -850,7 +850,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { if let Ok(val) = unwind_integer_value.try_into() { Some(val) } else { - tcx.dcx().span_err(attr.span(), "value above maximum permitted value - u32::MAX"); + tcx.dcx().span_err(attr.span, "value above maximum permitted value - u32::MAX"); None } } @@ -865,13 +865,13 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { /* no-op */ } Ok(FnResolution::FnImpl { .. }) => { tcx.dcx().span_err( - attr.span(), + attr.span, "Kani currently does not support stubbing trait implementations.", ); } Err(err) => { tcx.dcx().span_err( - attr.span(), + attr.span, format!("failed to resolve `{}`: {err}", pretty_type_path(path)), ); } @@ -882,7 +882,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec Vec { tcx.dcx().span_err( - attr.span(), + attr.span, format!( "attribute `kani::stub` takes two path arguments; found {}", paths.len() @@ -923,7 +923,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { const ATTRIBUTE: &str = "#[kani::solver]"; let invalid_arg_err = |attr: &Attribute| { tcx.dcx().span_err( - attr.span(), + attr.span, format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)"), ) }; @@ -931,7 +931,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { let attr_args = attr.meta_item_list().unwrap(); if attr_args.len() != 1 { tcx.dcx().span_err( - attr.span(), + attr.span, format!( "the `{ATTRIBUTE}` attribute expects a single argument. Got {} arguments.", attr_args.len() @@ -954,7 +954,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { match solver { Ok(solver) => Some(solver), Err(_) => { - tcx.dcx().span_err(attr.span(), format!("unknown solver `{ident_str}`")); + tcx.dcx().span_err(attr.span, format!("unknown solver `{ident_str}`")); None } } @@ -1027,25 +1027,26 @@ fn parse_str_value(attr: &Attribute) -> Option { /// If the attribute is named `kanitool::name`, this extracts `name` fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { - if let Attribute::Unparsed(normal) = attr { - let segments = &normal.path.segments; - if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { - let ident_str = segments[1..] - .iter() - .map(|segment| segment.as_str()) - .intersperse("::") - .collect::(); - KaniAttributeKind::try_from(ident_str.as_str()) - .inspect_err(|&err| { - debug!(?err, "attr_kind_failed"); - tcx.dcx().span_err(attr.span(), format!("unknown attribute `{ident_str}`")); - }) - .ok() - } else { - None + match &attr.kind { + AttrKind::Normal(normal) => { + let segments = &normal.path.segments; + if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { + let ident_str = segments[1..] + .iter() + .map(|segment| segment.as_str()) + .intersperse("::") + .collect::(); + KaniAttributeKind::try_from(ident_str.as_str()) + .inspect_err(|&err| { + debug!(?err, "attr_kind_failed"); + tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`")); + }) + .ok() + } else { + None + } } - } else { - None + _ => None, } } @@ -1109,7 +1110,7 @@ fn pretty_type_path(path: &TypePath) -> String { /// Retrieve the value of the `fn_marker` attribute for the given definition if it has one. pub(crate) fn fn_marker(def: T) -> Option { let fn_marker: [SymbolStable; 2] = ["kanitool".into(), "fn_marker".into()]; - let marker = def.tool_attrs(&fn_marker).pop()?; + let marker = def.attrs_by_path(&fn_marker).pop()?; let attribute = syn_attr_stable(&marker); let meta_name = attribute.meta.require_name_value().unwrap_or_else(|_| { panic!("Expected name value attribute for `kanitool::fn_marker`, but found: `{:?}`", marker) diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index a53abef90e88..a3451c99e029 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -93,7 +93,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx> ty::Adt(def, args) => { assert!(def.repr().simd(), "`simd_size_and_type` called on non-SIMD type"); let variant = def.non_enum_variant(); - let f0_ty = variant.fields[rustc_abi::FieldIdx::from_usize(0)].ty(tcx, args); + let f0_ty = variant.fields[0u32.into()].ty(tcx, args); match f0_ty.kind() { ty::Array(elem_ty, len) => (*len, *elem_ty), diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 85936041cc38..01d237bf0773 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -87,8 +87,8 @@ pub enum KaniModel { Offset, #[strum(serialize = "PtrOffsetFromModel")] PtrOffsetFrom, - #[strum(serialize = "PtrOffsetFromUnsignedModel")] - PtrOffsetFromUnsigned, + #[strum(serialize = "PtrSubPtrModel")] + PtrSubPtr, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index e6839487c046..fba6f5f0e6aa 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -37,7 +37,7 @@ pub mod transform; /// error was found. pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { let krate = tcx.crate_name(LOCAL_CRATE); - for item in tcx.hir_free_items() { + for item in tcx.hir().items() { let def_id = item.owner_id.def_id.to_def_id(); KaniAttributes::for_item(tcx, def_id).check_attributes(); if tcx.def_kind(def_id) == DefKind::GlobalAsm { diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 2008ef1eb0b8..c326172ba843 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -525,8 +525,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { Rvalue::Use(operand) | Rvalue::ShallowInitBox(operand, _) | Rvalue::Cast(_, operand, _) - | Rvalue::Repeat(operand, ..) - | Rvalue::WrapUnsafeBinder(operand, _) => self.successors_for_operand(state, operand), + | Rvalue::Repeat(operand, ..) => self.successors_for_operand(state, operand), Rvalue::Ref(_, _, ref_place) | Rvalue::RawPtr(_, ref_place) => { // Here, a reference to a place is created, which leaves the place // unchanged. @@ -664,6 +663,8 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::MinNumF32 | Intrinsic::MinNumF64 | Intrinsic::MulWithOverflow + | Intrinsic::NearbyIntF32 + | Intrinsic::NearbyIntF64 | Intrinsic::NeedsDrop | Intrinsic::PowF32 | Intrinsic::PowF64 @@ -675,12 +676,12 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PtrOffsetFromUnsigned | Intrinsic::RawEq | Intrinsic::RetagBoxToRaw + | Intrinsic::RintF32 + | Intrinsic::RintF64 | Intrinsic::RotateLeft | Intrinsic::RotateRight | Intrinsic::RoundF32 | Intrinsic::RoundF64 - | Intrinsic::RoundTiesEvenF32 - | Intrinsic::RoundTiesEvenF64 | Intrinsic::SaturatingAdd | Intrinsic::SaturatingSub | Intrinsic::SinF32 diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs index 6e473a84eecc..0b52a84eaa59 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs @@ -163,8 +163,7 @@ impl<'tcx> PointsToGraph<'tcx> { | ProjectionElem::Subslice { .. } | ProjectionElem::Downcast(..) | ProjectionElem::OpaqueCast(..) - | ProjectionElem::Subtype(..) - | ProjectionElem::UnwrapUnsafeBinder(..) => { + | ProjectionElem::Subtype(..) => { /* There operations are no-ops w.r.t aliasing since we are tracking it on per-object basis. */ } } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 237fbf5f8b41..3172e6a010a1 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -84,14 +84,6 @@ where crate_items .iter() .filter_map(|item| { - // avoid stable MIR panic - // https://github.com/model-checking/kani/issues/3919 - if let Ok(instance) = Instance::try_from(*item) { - let int_def_id = rustc_internal::internal(tcx, instance.def.def_id()); - if matches!(tcx.def_kind(int_def_id), rustc_hir::def::DefKind::GlobalAsm) { - return None; - } - }; // Only collect monomorphic items. matches!(item.kind(), ItemKind::Fn) .then(|| { @@ -270,11 +262,11 @@ impl MonoItemsFnCollector<'_, '_> { // A trait object type can have multiple trait bounds but up to one non-auto-trait // bound. This non-auto-trait, named principal, is the only one that can have methods. // https://doc.rust-lang.org/reference/special-types-and-traits.html#auto-traits - let trait_ref = rustc_internal::internal(self.tcx, principal.with_self_ty(concrete_ty)); - let trait_ref = self.tcx.instantiate_bound_regions_with_erased(trait_ref); + let poly_trait_ref = principal.with_self_ty(concrete_ty); // Walk all methods of the trait, including those of its supertraits - let entries = self.tcx.vtable_entries(trait_ref); + let entries = + self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref)); let methods = entries.iter().filter_map(|entry| match entry { VtblEntry::MetadataAlign | VtblEntry::MetadataDropInPlace @@ -472,7 +464,7 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> { // We don't support inline assembly. This shall be replaced by an unsupported // construct during codegen. } - TerminatorKind::Abort | TerminatorKind::Assert { .. } => { + TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. } TerminatorKind::Goto { .. } diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index accb4807f00e..cd1b72c6dc66 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -307,7 +307,7 @@ fn resolve_prefix<'tcx>( (None, Some(segment)) if segment.ident == CRATE => { // Find the module at the root of the crate. let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); - let crate_root = match tcx.hir_parent_iter(current_module_hir_id).last() { + let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() { None => current_module, Some((hir_id, _)) => hir_id.owner.def_id, }; @@ -366,7 +366,7 @@ where I: Iterator, { let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); - let mut parents = tcx.hir_parent_iter(current_module_hir_id); + let mut parents = tcx.hir().parent_iter(current_module_hir_id); let mut base_module = current_module; while segments.next_if(|segment| segment.ident == SUPER).is_some() { if let Some((parent, _)) = parents.next() { @@ -430,8 +430,8 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R debug!(?name, ?current_module, "resolve_relative"); let mut glob_imports = vec![]; - let result = tcx.hir_module_free_items(current_module).find_map(|item_id| { - let item = tcx.hir_item(item_id); + let result = tcx.hir().module_items(current_module).find_map(|item_id| { + let item = tcx.hir().item(item_id); if item.ident.as_str() == name { match item.kind { ItemKind::Use(use_path, UseKind::Single) => use_path.res[0].opt_def_id(), diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 9235287852e1..d70e884400bb 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -130,7 +130,7 @@ pub fn validate_stub_const(tcx: TyCtxt, instance: Instance) -> bool { let item = CrateItem::try_from(instance).unwrap(); let internal_instance = rustc_internal::internal(tcx, instance); let mut checker = StubConstChecker::new(tcx, internal_instance, item); - checker.visit_body(&item.expect_body()); + checker.visit_body(&item.body()); checker.is_valid() } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 9ae4ffd79ad6..20f4538453b5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -468,7 +468,7 @@ impl MirVisitor for CheckUninitVisitor { && !ptx.is_mutating() { let contains_deref_projection = - { place.projection.contains(&ProjectionElem::Deref) }; + { place.projection.iter().any(|elem| *elem == ProjectionElem::Deref) }; if contains_deref_projection { // We do not currently support having a deref projection in the same // place as union field access. @@ -625,6 +625,8 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::MinNumF32 | Intrinsic::MinNumF64 | Intrinsic::MulWithOverflow + | Intrinsic::NearbyIntF32 + | Intrinsic::NearbyIntF64 | Intrinsic::NeedsDrop | Intrinsic::PowF32 | Intrinsic::PowF64 @@ -632,6 +634,8 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PowIF64 | Intrinsic::PrefAlignOf | Intrinsic::RawEq + | Intrinsic::RintF32 + | Intrinsic::RintF64 | Intrinsic::RotateLeft | Intrinsic::RotateRight | Intrinsic::RoundF32 diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 7469508e2c70..9ad23071df4a 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs @@ -6,7 +6,7 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ - mir::{FieldIdx, Mutability, Operand, Place, RawPtrKind, Rvalue, Statement, StatementKind}, + mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind}, ty::{RigidTy, Ty}, }; use strum_macros::AsRefStr; @@ -123,7 +123,7 @@ impl MemoryInitOp { Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), }; - let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone()); + let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); rvalue.ty(body.locals()).unwrap() } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { @@ -147,7 +147,7 @@ impl MemoryInitOp { MemoryInitOp::AssignUnion { lvalue, .. } => { // It does not matter which operand to return for layout generation, since both of // them have the same pointee type. - let address_of = Rvalue::AddressOf(RawPtrKind::Const, lvalue.clone()); + let address_of = Rvalue::AddressOf(Mutability::Not, lvalue.clone()); address_of.ty(body.locals()).unwrap() } } @@ -271,7 +271,7 @@ fn mk_ref( Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), }; - let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone()); + let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); let ret_ty = rvalue.ty(body.locals()).unwrap(); let result = body.new_local(ret_ty, span, Mutability::Not); let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span }; diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index b536de1e2695..a8408e04931a 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -28,8 +28,8 @@ use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; use stable_mir::mir::{ AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, FieldIdx, Local, LocalDecl, MirVisitor, - Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, Rvalue, - Statement, StatementKind, Terminator, TerminatorKind, + Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, Statement, + StatementKind, Terminator, TerminatorKind, }; use stable_mir::target::{MachineInfo, MachineSize}; use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Span, Ty, TyKind, UintTy}; @@ -87,7 +87,7 @@ impl ValidValuePass { match operation { SourceOp::BytesValidity { ranges, target_ty, rvalue } => { let value = body.insert_assignment(rvalue, &mut source, InsertPosition::Before); - let rvalue_ptr = Rvalue::AddressOf(RawPtrKind::Const, Place::from(value)); + let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value)); for range in ranges { let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source); let msg = @@ -213,6 +213,7 @@ impl ValidValueReq { } ValueAbi::Scalar(_) | ValueAbi::ScalarPair(_, _) + | ValueAbi::Uninhabited | ValueAbi::Vector { .. } | ValueAbi::Aggregate { .. } => None, } diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 090c74311fa4..fd499db7c3c6 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -42,7 +42,7 @@ impl RustcInternalMir for AggregateKind { internal(tcx, generic_args), maybe_user_type_annotation_index .map(rustc_middle::ty::UserTypeAnnotationIndex::from_usize), - maybe_field_idx.map(rustc_abi::FieldIdx::from_usize), + maybe_field_idx.map(rustc_target::abi::FieldIdx::from_usize), ), AggregateKind::Closure(closure_def, generic_args) => { rustc_middle::mir::AggregateKind::Closure( @@ -207,7 +207,7 @@ impl RustcInternalMir for NullOp { .map(|(variant_idx, field_idx)| { ( internal(tcx, variant_idx), - rustc_abi::FieldIdx::from_usize(*field_idx), + rustc_target::abi::FieldIdx::from_usize(*field_idx), ) }) .collect::>() @@ -215,7 +215,6 @@ impl RustcInternalMir for NullOp { ), ), NullOp::UbChecks => rustc_middle::mir::NullOp::UbChecks, - NullOp::ContractChecks => rustc_middle::mir::NullOp::ContractChecks, } } } @@ -225,8 +224,8 @@ impl RustcInternalMir for Rvalue { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - Rvalue::AddressOf(raw_ptr_kind, place) => { - rustc_middle::mir::Rvalue::RawPtr(internal(tcx, raw_ptr_kind), internal(tcx, place)) + Rvalue::AddressOf(mutability, place) => { + rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place)) } Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate( Box::new(aggregate_kind.internal_mir(tcx)), @@ -546,9 +545,6 @@ impl RustcInternalMir for AssertMessage { found: found.internal_mir(tcx), } } - AssertMessage::NullPointerDereference => { - rustc_middle::mir::AssertMessage::NullPointerDereference - } } } } diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 43f8e5b7013f..79238e423e62 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -168,9 +168,7 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom], - Intrinsic::PtrOffsetFromUnsigned => { - self.models[&KaniModel::PtrOffsetFromUnsigned] - } + Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr], // The rest is handled in codegen. _ => { return self.super_terminator(term); diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index c8a56d3ef062..02709797cf3a 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -16,6 +16,7 @@ #![feature(f128)] #![feature(f16)] #![feature(non_exhaustive_omitted_patterns_lint)] +#![feature(float_next_up_down)] #![feature(try_blocks)] extern crate rustc_abi; extern crate rustc_ast; @@ -50,7 +51,7 @@ mod kani_middle; mod kani_queries; mod session; -use rustc_driver::{TimePassesCallbacks, run_compiler}; +use rustc_driver::{RunCompiler, TimePassesCallbacks}; use std::env; /// Main function. Configure arguments and run the compiler. @@ -63,7 +64,8 @@ fn main() { kani_compiler::run(rustc_args); } else { let mut callbacks = TimePassesCallbacks::default(); - run_compiler(&rustc_args, &mut callbacks); + let compiler = RunCompiler::new(&rustc_args, &mut callbacks); + compiler.run(); } } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 8efabb2c9517..f448afb801cc 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -4,6 +4,7 @@ //! Module used to configure a compiler session. use crate::args::Arguments; +use rustc_data_structures::sync::Lrc; use rustc_errors::{ ColorConfig, DiagInner, emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, registry::Registry as ErrorRegistry, @@ -15,7 +16,6 @@ use rustc_span::source_map::SourceMap; use std::io; use std::io::IsTerminal; use std::panic; -use std::sync::Arc; use std::sync::LazyLock; use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; use tracing_tree::HierarchicalLayer; @@ -57,7 +57,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + let mut emitter = JsonEmitter::new( Box::new(io::BufWriter::new(io::stderr())), #[allow(clippy::arc_with_non_send_sync)] - Some(Arc::new(SourceMap::new(FilePathMapping::empty()))), + Lrc::new(SourceMap::new(FilePathMapping::empty())), fallback_bundle, false, HumanReadableErrorType::Default, diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 4c39b03183b6..eb0dce1ce599 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -206,6 +206,7 @@ crate-type = ["lib"] // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See // https://doc.rust-lang.org/cargo/reference/environment-variables.html .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f"))) + .env("RUSTC_BOOTSTRAP", "1") .env("CARGO_TERM_PROGRESS_WHEN", "never"); match self.run_build_target(cmd, verification_target.target()) { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 96351a4095ee..b014c671d2ac 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -310,9 +310,9 @@ impl VerificationResult { /// /// NOTE: We actually ignore the CBMC exit status, in favor of two checks: /// 1. Examining the actual results of CBMC properties. - /// (CBMC will regularly report "failure" but that's just our cover checks.) + /// (CBMC will regularly report "failure" but that's just our cover checks.) /// 2. Positively checking for the presence of results. - /// (Do not mistake lack of results for success: report it as failure.) + /// (Do not mistake lack of results for success: report it as failure.) fn from( output: VerificationOutput, should_panic: bool, @@ -502,7 +502,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); COUNTER_RE.get_or_init(|| { Regex::new( - r#"^(?VirtualCounter\(bcb)(?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, + r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, ) .unwrap() }) @@ -512,14 +512,20 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option CoverageTerm::Counter(counter_id), + "ExpressionUsed" => CoverageTerm::Expression(counter_id), + _ => unreachable!("counter kind could not be recognized: {:?}", kind), + }; let region = CoverageRegion::from_str(span); let cov_check = CoverageCheck::new(function, term, region, status); diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 9a09ce6163f8..37c86478f759 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -84,6 +84,7 @@ impl KaniSession { let mut cmd = Command::new(&self.kani_compiler); let kani_compiler_args = to_rustc_arg(kani_args); cmd.arg(kani_compiler_args).args(rustc_args); + cmd.env("RUSTC_BOOTSTRAP", "1"); if self.args.common_args.quiet { self.run_suppress(cmd)?; diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 694cb480bc4f..845ae7de21bb 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -64,6 +64,7 @@ impl CoverageCheck { #[derive(Debug, Clone, Serialize, Deserialize)] pub enum CoverageTerm { Counter(u32), + Expression(u32), } #[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)] diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 3329b1d4b895..af5ac336e09e 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -65,7 +65,7 @@ mod intrinsics { /// Logic similar to `bitmask_len` from `portable_simd`. /// pub(super) const fn mask_len(len: usize) -> usize { - len.div_ceil(8) + (len + 7) / 8 } #[cfg(target_endian = "little")] diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 39fd786f0249..8913c399c959 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -89,8 +89,8 @@ macro_rules! generate_models { } } - #[kanitool::fn_marker = "PtrOffsetFromUnsignedModel"] - pub unsafe fn ptr_offset_from_unsigned(ptr1: *const T, ptr2: *const T) -> usize { + #[kanitool::fn_marker = "PtrSubPtrModel"] + pub unsafe fn ptr_sub_ptr(ptr1: *const T, ptr2: *const T) -> usize { let offset = ptr_offset_from(ptr1, ptr2); kani::safety_check(offset >= 0, "Expected non-negative distance between pointers"); offset as usize diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 8bd21a773249..0292c21dac75 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-03-17" +channel = "1.85.0" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/rustfmt.toml b/rustfmt.toml index 44cbfe4a3dc9..f8ff0d0fd105 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -6,13 +6,3 @@ edition = "2021" style_edition = "2024" use_small_heuristics = "Max" merge_derives = false - -ignore = [ - "**/build/", - "**/target/", - - # Do not format submodules - # For some reason, this is not working without the directory wildcard. - "**/firecracker", - "**/tests/perf/s2n-quic/", -] diff --git a/scripts/kani-fmt.sh b/scripts/kani-fmt.sh index 5eca1582cc40..f5b90f75a145 100755 --- a/scripts/kani-fmt.sh +++ b/scripts/kani-fmt.sh @@ -27,11 +27,11 @@ for suite in "${TESTS[@]}"; do # Find uses breakline to split between files. This ensures that we can # handle files with space in their path. set -f; IFS=$'\n' - files=($(find "${suite}" -name "*.rs")) + files=($(find "${suite}" -name "*.rs" -not -path "*/perf/s2n-quic/*")) set +f; unset IFS # Note: We set the configuration file here because some submodules have # their own configuration file. - rustfmt --unstable-features "$@" --config-path rustfmt.toml "${files[@]}" || error=1 + rustfmt "$@" --config-path rustfmt.toml "${files[@]}" || error=1 done exit $error diff --git a/tests/cargo-ui/verbose-cmds/expected b/tests/cargo-ui/verbose-cmds/expected index f883ef972cb3..b47b60d51ff4 100644 --- a/tests/cargo-ui/verbose-cmds/expected +++ b/tests/cargo-ui/verbose-cmds/expected @@ -1,5 +1,5 @@ CARGO_ENCODED_RUSTFLAGS= -cargo +nightly +cargo + Running: `goto-cc Running: `goto-instrument Checking harness dummy_harness... diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected index 06496f4313d7..a0592c586a03 100644 --- a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected +++ b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected @@ -1,6 +1,6 @@ error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\ -evaluation panicked: PointerGenerator requires at least one byte.\ +the evaluated program panicked at 'PointerGenerator requires at least one byte.' note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\ pointer_generator_error.rs\ diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.expected b/tests/expected/function-contract/as-assertions/assert-postconditions.expected deleted file mode 100644 index e16069ec2fad..000000000000 --- a/tests/expected/function-contract/as-assertions/assert-postconditions.expected +++ /dev/null @@ -1,9 +0,0 @@ -assertion\ - - Status: FAILURE\ - - Description: "|_| old(*add_two_ptr + 1) == *add_two_ptr" - -assertion\ - - Status: SUCCESS\ - - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr" - -VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.rs b/tests/expected/function-contract/as-assertions/assert-postconditions.rs deleted file mode 100644 index c1b92a23c1d1..000000000000 --- a/tests/expected/function-contract/as-assertions/assert-postconditions.rs +++ /dev/null @@ -1,29 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts - -// Test -Zfunction-contracts for asserting postconditions. - -#[kani::requires(*add_three_ptr < 100)] -#[kani::modifies(add_three_ptr)] -fn add_three(add_three_ptr: &mut u32) { - *add_three_ptr += 1; - add_two(add_three_ptr); -} - -#[kani::ensures(|_| old(*add_two_ptr + 1) == *add_two_ptr)] // incorrect -- should be old(*add_two_ptr + 2) -fn add_two(add_two_ptr: &mut u32) { - *add_two_ptr += 1; - add_one(add_two_ptr) -} - -#[kani::ensures(|_| old(*add_one_ptr + 1) == *add_one_ptr)] // correct -- assertion should always succeed -fn add_one(add_one_ptr: &mut u32) { - *add_one_ptr += 1; -} - -#[kani::proof_for_contract(add_three)] -fn prove_add_three() { - let mut i = kani::any(); - add_three(&mut i); -} diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 38f31a63d5ca..0c43cd901cc9 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -4,9 +4,7 @@ Failed Checks: |result| kani::mem::can_dereference(result.0) VERIFICATION:- FAILED Checking harness pre_condition::harness_invalid_ptr... -Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20 Failed Checks: Kani does not support reasoning about pointer to unallocated memory -Failed Checks: dereference failure: pointer outside object bounds VERIFICATION:- FAILED Checking harness pre_condition::harness_stack_ptr... diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected index bed39a66b7af..4c820df5409f 100644 --- a/tests/expected/issue-3571/issue_3571.expected +++ b/tests/expected/issue-3571/issue_3571.expected @@ -1,6 +1,6 @@ Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment -Failed Checks: null pointer dereference occurred +Failed Checks: dereference failure: pointer invalid VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) diff --git a/tests/expected/offset-bounds-check/offset_from_unsigned.expected b/tests/expected/offset-bounds-check/sub_ptr.expected similarity index 52% rename from tests/expected/offset-bounds-check/offset_from_unsigned.expected rename to tests/expected/offset-bounds-check/sub_ptr.expected index fff02a3d96af..611fe2e565c7 100644 --- a/tests/expected/offset-bounds-check/offset_from_unsigned.expected +++ b/tests/expected/offset-bounds-check/sub_ptr.expected @@ -1,29 +1,29 @@ -Checking harness check_offset_from_unsigned_same_dangling... +Checking harness check_sub_ptr_same_dangling... VERIFICATION:- SUCCESSFUL -Checking harness check_offset_from_unsigned_unit_panic... +Checking harness check_sub_ptr_unit_panic... Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) -Checking harness check_offset_from_unsigned_negative_result... +Checking harness check_sub_ptr_negative_result... Failed Checks: Expected non-negative distance between pointers VERIFICATION:- FAILED -Checking harness check_offset_from_unsigned_diff_alloc... +Checking harness check_sub_ptr_diff_alloc... Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED -Checking harness check_offset_from_unsigned_oob_ptr... +Checking harness check_sub_ptr_oob_ptr... Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED -Checking harness check_offset_from_unsigned_self_oob... +Checking harness check_sub_ptr_self_oob... Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED Summary: -Verification failed for - check_offset_from_unsigned_negative_result -Verification failed for - check_offset_from_unsigned_diff_alloc -Verification failed for - check_offset_from_unsigned_oob_ptr -Verification failed for - check_offset_from_unsigned_self_oob +Verification failed for - check_sub_ptr_negative_result +Verification failed for - check_sub_ptr_diff_alloc +Verification failed for - check_sub_ptr_oob_ptr +Verification failed for - check_sub_ptr_self_oob Complete - 2 successfully verified harnesses, 4 failures, 6 total. diff --git a/tests/expected/offset-bounds-check/offset_from_unsigned.rs b/tests/expected/offset-bounds-check/sub_ptr.rs similarity index 62% rename from tests/expected/offset-bounds-check/offset_from_unsigned.rs rename to tests/expected/offset-bounds-check/sub_ptr.rs index f5b11a741403..7ddfa96d94f8 100644 --- a/tests/expected/offset-bounds-check/offset_from_unsigned.rs +++ b/tests/expected/offset-bounds-check/sub_ptr.rs @@ -1,47 +1,47 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that Kani can detect UB due to `offset_from_unsigned` with out-of-bounds pointer or wrong order. +//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order. #![feature(ptr_sub_ptr)] #[kani::proof] -fn check_offset_from_unsigned_self_oob() { +fn check_sub_ptr_self_oob() { let val = 10u128; let ptr: *const u128 = &val; let ptr_oob: *const u128 = ptr.wrapping_add(10); // SAFETY: This is not safe! - let _offset = unsafe { ptr_oob.offset_from_unsigned(ptr) }; + let _offset = unsafe { ptr_oob.sub_ptr(ptr) }; } #[kani::proof] -fn check_offset_from_unsigned_oob_ptr() { +fn check_sub_ptr_oob_ptr() { let val = 10u128; let ptr: *const u128 = &val; let ptr_oob: *const u128 = ptr.wrapping_sub(10); // SAFETY: This is not safe! - let _offset = unsafe { ptr.offset_from_unsigned(ptr_oob) }; + let _offset = unsafe { ptr.sub_ptr(ptr_oob) }; } #[kani::proof] -fn check_offset_from_unsigned_diff_alloc() { +fn check_sub_ptr_diff_alloc() { let val1 = kani::any(); let val2 = kani::any(); let ptr1: *const u128 = &val1; let ptr2: *const u128 = &val2; // SAFETY: This is not safe! - let _offset = unsafe { ptr1.offset_from_unsigned(ptr2) }; + let _offset = unsafe { ptr1.sub_ptr(ptr2) }; } #[kani::proof] -fn check_offset_from_unsigned_negative_result() { +fn check_sub_ptr_negative_result() { let val: [u8; 10] = kani::any(); let ptr_first: *const _ = &val[0]; let ptr_last: *const _ = &val[9]; // SAFETY: This is safe! - let offset_ok = unsafe { ptr_last.offset_from_unsigned(ptr_first) }; + let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) }; // SAFETY: This is not safe! - let offset_not_ok = unsafe { ptr_first.offset_from_unsigned(ptr_last) }; + let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) }; // Just use the result. assert!(offset_ok != offset_not_ok); @@ -49,22 +49,22 @@ fn check_offset_from_unsigned_negative_result() { #[kani::proof] #[kani::should_panic] -fn check_offset_from_unsigned_unit_panic() { +fn check_sub_ptr_unit_panic() { let val1 = kani::any(); let val2 = kani::any(); let ptr1: *const () = &val1 as *const _ as *const (); let ptr2: *const () = &val2 as *const _ as *const (); // SAFETY: This is safe but will panic... - let _offset = unsafe { ptr1.offset_from_unsigned(ptr2) }; + let _offset = unsafe { ptr1.sub_ptr(ptr2) }; } #[kani::proof] -fn check_offset_from_unsigned_same_dangling() { +fn check_sub_ptr_same_dangling() { let val = 10u128; let ptr: *const u128 = &val; let ptr_oob_1: *const u128 = ptr.wrapping_add(10); let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); // SAFETY: This is safe since the pointer is the same! - let offset = unsafe { ptr_oob_1.offset_from_unsigned(ptr_oob_2) }; + let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) }; assert_eq!(offset, 0); } diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index 17b654533406..d7f258c27ba5 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -170,6 +170,19 @@ fn delayed_ub_structs() { } } +/// Delayed UB via mutable pointer write into a slice element. +#[kani::proof] +fn delayed_ub_slices() { + unsafe { + // Create an array. + let mut arr = [0u128; 4]; + // Get a pointer to a part of the array. + let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32); + *ptr = (4, 4); + let arr_copy = arr; // UB: This reads a padding value inside the array! + } +} + /// Delayed UB via mutable pointer copy, which should be the only delayed UB trigger in this case. #[kani::proof] fn delayed_ub_trigger_copy() { diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.expected b/tests/expected/uninit/delayed-ub/expected similarity index 88% rename from tests/expected/uninit/delayed-ub/delayed-ub.expected rename to tests/expected/uninit/delayed-ub/expected index d998801c2ca7..a8d7ebbd837d 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.expected +++ b/tests/expected/uninit/delayed-ub/expected @@ -2,6 +2,10 @@ delayed_ub_trigger_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ +delayed_ub_slices.safety_check.\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" + delayed_ub_structs.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" @@ -40,6 +44,7 @@ delayed_ub.safety_check.\ Summary: Verification failed for - delayed_ub_trigger_copy +Verification failed for - delayed_ub_slices Verification failed for - delayed_ub_structs Verification failed for - delayed_ub_double_copy Verification failed for - delayed_ub_copy @@ -49,4 +54,4 @@ Verification failed for - delayed_ub_laundered Verification failed for - delayed_ub_static Verification failed for - delayed_ub_transmute Verification failed for - delayed_ub -Complete - 0 successfully verified harnesses, 10 failures, 10 total. +Complete - 0 successfully verified harnesses, 11 failures, 11 total. diff --git a/tests/expected/uninit/delayed-ub/slices_fixme.expected b/tests/expected/uninit/delayed-ub/slices_fixme.expected deleted file mode 100644 index 902980a2bf1c..000000000000 --- a/tests/expected/uninit/delayed-ub/slices_fixme.expected +++ /dev/null @@ -1,5 +0,0 @@ -delayed_ub_slices.assertion.\ - - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" - -Verification failed for - delayed_ub_slices diff --git a/tests/expected/uninit/delayed-ub/slices_fixme.rs b/tests/expected/uninit/delayed-ub/slices_fixme.rs deleted file mode 100644 index c112a4638363..000000000000 --- a/tests/expected/uninit/delayed-ub/slices_fixme.rs +++ /dev/null @@ -1,21 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks - -//! Checks that Kani catches instances of delayed UB for slices. -//! This test used to live inside delayed-ub, but the 2/5/2025 toolchain upgrade introduced a regression for this test. -//! Once this test is fixed, move it back into delayed-ub.rs -//! See https://github.com/model-checking/kani/issues/3881 for details. - -/// Delayed UB via mutable pointer write into a slice element. -#[kani::proof] -fn delayed_ub_slices() { - unsafe { - // Create an array. - let mut arr = [0u128; 4]; - // Get a pointer to a part of the array. - let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32); - *ptr = (4, 4); - let arr_copy = arr; // UB: This reads a padding value inside the array! - } -} diff --git a/tests/expected/zst/expected b/tests/expected/zst/expected index 3efe59d3445f..bec891bea92c 100644 --- a/tests/expected/zst/expected +++ b/tests/expected/zst/expected @@ -1,4 +1,4 @@ -- Status: FAILURE\ -- Description: "null pointer dereference occurred" +Status: FAILURE\ +Description: "dereference failure: pointer NULL" VERIFICATION:- FAILED diff --git a/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs similarity index 79% rename from tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs rename to tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs index 057483b3b0cc..25e02f45a943 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs @@ -1,51 +1,51 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `round_ties_even_f32` returns the nearest integer to the argument. The +// Checks that `nearbyintf32` returns the nearest integer to the argument. The // default rounding mode is rounding half to even, which is described here: // https://en.wikipedia.org/wiki/Rounding#Round_half_to_even #![feature(core_intrinsics)] -use std::intrinsics::round_ties_even_f32; +use std::intrinsics::nearbyintf32; #[kani::proof] fn test_one() { let one = 1.0; - let result = round_ties_even_f32(one); + let result = unsafe { nearbyintf32(one) }; assert!(result == 1.0); } #[kani::proof] fn test_one_frac() { let one_frac = 1.9; - let result = round_ties_even_f32(one_frac); + let result = unsafe { nearbyintf32(one_frac) }; assert!(result == 2.0); } #[kani::proof] fn test_half_down() { let one_frac = 2.5; - let result = round_ties_even_f32(one_frac); + let result = unsafe { nearbyintf32(one_frac) }; assert!(result == 2.0); } #[kani::proof] fn test_half_up() { let one_frac = 3.5; - let result = round_ties_even_f32(one_frac); + let result = unsafe { nearbyintf32(one_frac) }; assert!(result == 4.0); } #[kani::proof] fn test_conc() { let conc = -42.6; - let result = round_ties_even_f32(conc); + let result = unsafe { nearbyintf32(conc) }; assert!(result == -43.0); } #[kani::proof] fn test_conc_sci() { let conc = 5.4e-2; - let result = round_ties_even_f32(conc); + let result = unsafe { nearbyintf32(conc) }; assert!(result == 0.0); } @@ -54,7 +54,7 @@ fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = round_ties_even_f32(x); + let result = unsafe { nearbyintf32(x) }; let frac = x.fract().abs(); if x.is_sign_positive() { if frac > 0.5 { @@ -92,7 +92,7 @@ fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = round_ties_even_f32(x); + let result = unsafe { nearbyintf32(x) }; let diff = (x - result).abs(); assert!(diff <= 0.5); assert!(diff >= 0.0); diff --git a/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs similarity index 79% rename from tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs rename to tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs index c7c1a9611bae..589a44a4d1ac 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs @@ -1,51 +1,51 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `round_ties_even_f64` returns the nearest integer to the argument. The +// Checks that `nearbyintf64` returns the nearest integer to the argument. The // default rounding mode is rounding half to even, which is described here: // https://en.wikipedia.org/wiki/Rounding#Round_half_to_even #![feature(core_intrinsics)] -use std::intrinsics::round_ties_even_f64; +use std::intrinsics::nearbyintf64; #[kani::proof] fn test_one() { let one = 1.0; - let result = round_ties_even_f64(one); + let result = unsafe { nearbyintf64(one) }; assert!(result == 1.0); } #[kani::proof] fn test_one_frac() { let one_frac = 1.9; - let result = round_ties_even_f64(one_frac); + let result = unsafe { nearbyintf64(one_frac) }; assert!(result == 2.0); } #[kani::proof] fn test_half_down() { let one_frac = 2.5; - let result = round_ties_even_f64(one_frac); + let result = unsafe { nearbyintf64(one_frac) }; assert!(result == 2.0); } #[kani::proof] fn test_half_up() { let one_frac = 3.5; - let result = round_ties_even_f64(one_frac); + let result = unsafe { nearbyintf64(one_frac) }; assert!(result == 4.0); } #[kani::proof] fn test_conc() { let conc = -42.6; - let result = round_ties_even_f64(conc); + let result = unsafe { nearbyintf64(conc) }; assert!(result == -43.0); } #[kani::proof] fn test_conc_sci() { let conc = 5.4e-2; - let result = round_ties_even_f64(conc); + let result = unsafe { nearbyintf64(conc) }; assert!(result == 0.0); } @@ -54,7 +54,7 @@ fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = round_ties_even_f64(x); + let result = unsafe { nearbyintf64(x) }; let frac = x.fract().abs(); if x.is_sign_positive() { if frac > 0.5 { @@ -92,7 +92,7 @@ fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = round_ties_even_f64(x); + let result = unsafe { nearbyintf64(x) }; let diff = (x - result).abs(); assert!(diff <= 0.5); assert!(diff >= 0.0); diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs new file mode 100644 index 000000000000..79a0a4f9be2c --- /dev/null +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs @@ -0,0 +1,104 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `rintf32` returns the nearest integer to the argument. The +// default rounding mode is rounding half to even, which is described here: +// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even +// +// `rintf32` works like `nearbyintf32`, but it may raise an inexact +// floating-point exception which isn't supported in Rust: +// https://github.com/rust-lang/rust/issues/10186 +// So in practice, `rintf32` and `nearbyintf32` work the same way. +#![feature(core_intrinsics)] +use std::intrinsics::rintf32; + +#[kani::proof] +fn test_one() { + let one = 1.0; + let result = unsafe { rintf32(one) }; + assert!(result == 1.0); +} + +#[kani::proof] +fn test_one_frac() { + let one_frac = 1.9; + let result = unsafe { rintf32(one_frac) }; + assert!(result == 2.0); +} + +#[kani::proof] +fn test_half_down() { + let one_frac = 2.5; + let result = unsafe { rintf32(one_frac) }; + assert!(result == 2.0); +} + +#[kani::proof] +fn test_half_up() { + let one_frac = 3.5; + let result = unsafe { rintf32(one_frac) }; + assert!(result == 4.0); +} + +#[kani::proof] +fn test_conc() { + let conc = -42.6; + let result = unsafe { rintf32(conc) }; + assert!(result == -43.0); +} + +#[kani::proof] +fn test_conc_sci() { + let conc = 5.4e-2; + let result = unsafe { rintf32(conc) }; + assert!(result == 0.0); +} + +#[kani::proof] +fn test_towards_nearest() { + let x: f32 = kani::any(); + kani::assume(!x.is_nan()); + kani::assume(!x.is_infinite()); + let result = unsafe { rintf32(x) }; + let frac = x.fract().abs(); + if x.is_sign_positive() { + if frac > 0.5 { + assert!(result > x); + } else if frac < 0.5 { + assert!(result <= x); + } else { + // This would fail if conversion checks were on + let integer = x as i64; + if integer % 2 == 0 { + assert!(result < x); + } else { + assert!(result > x); + } + } + } else { + if frac > 0.5 { + assert!(result < x); + } else if frac < 0.5 { + assert!(result >= x); + } else { + // This would fail if conversion checks were on + let integer = x as i64; + if integer % 2 == 0 { + assert!(result > x); + } else { + assert!(result < x); + } + } + } +} + +#[kani::proof] +fn test_diff_half_one() { + let x: f32 = kani::any(); + kani::assume(!x.is_nan()); + kani::assume(!x.is_infinite()); + let result = unsafe { rintf32(x) }; + let diff = (x - result).abs(); + assert!(diff <= 0.5); + assert!(diff >= 0.0); +} diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs new file mode 100644 index 000000000000..8c8ea583a2d5 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs @@ -0,0 +1,104 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `rintf64` returns the nearest integer to the argument. The +// default rounding mode is rounding half to even, which is described here: +// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even +// +// `rintf64` works like `nearbyintf64`, but it may raise an inexact +// floating-point exception which isn't supported in Rust: +// https://github.com/rust-lang/rust/issues/10186 +// So in practice, `rintf64` and `nearbyintf64` work the same way. +#![feature(core_intrinsics)] +use std::intrinsics::rintf64; + +#[kani::proof] +fn test_one() { + let one = 1.0; + let result = unsafe { rintf64(one) }; + assert!(result == 1.0); +} + +#[kani::proof] +fn test_one_frac() { + let one_frac = 1.9; + let result = unsafe { rintf64(one_frac) }; + assert!(result == 2.0); +} + +#[kani::proof] +fn test_half_down() { + let one_frac = 2.5; + let result = unsafe { rintf64(one_frac) }; + assert!(result == 2.0); +} + +#[kani::proof] +fn test_half_up() { + let one_frac = 3.5; + let result = unsafe { rintf64(one_frac) }; + assert!(result == 4.0); +} + +#[kani::proof] +fn test_conc() { + let conc = -42.6; + let result = unsafe { rintf64(conc) }; + assert!(result == -43.0); +} + +#[kani::proof] +fn test_conc_sci() { + let conc = 5.4e-2; + let result = unsafe { rintf64(conc) }; + assert!(result == 0.0); +} + +#[kani::proof] +fn test_towards_nearest() { + let x: f64 = kani::any(); + kani::assume(!x.is_nan()); + kani::assume(!x.is_infinite()); + let result = unsafe { rintf64(x) }; + let frac = x.fract().abs(); + if x.is_sign_positive() { + if frac > 0.5 { + assert!(result > x); + } else if frac < 0.5 { + assert!(result <= x); + } else { + // This would fail if conversion checks were on + let integer = x as i64; + if integer % 2 == 0 { + assert!(result < x); + } else { + assert!(result > x); + } + } + } else { + if frac > 0.5 { + assert!(result < x); + } else if frac < 0.5 { + assert!(result >= x); + } else { + // This would fail if conversion checks were on + let integer = x as i64; + if integer % 2 == 0 { + assert!(result > x); + } else { + assert!(result < x); + } + } + } +} + +#[kani::proof] +fn test_diff_half_one() { + let x: f64 = kani::any(); + kani::assume(!x.is_nan()); + kani::assume(!x.is_infinite()); + let result = unsafe { rintf64(x) }; + let diff = (x - result).abs(); + assert!(diff <= 0.5); + assert!(diff >= 0.0); +} diff --git a/tests/kani/PointerOffset/offset_from_vec.rs b/tests/kani/PointerOffset/offset_from_vec.rs index 29865e2c8f81..482b4905df3c 100644 --- a/tests/kani/PointerOffset/offset_from_vec.rs +++ b/tests/kani/PointerOffset/offset_from_vec.rs @@ -18,6 +18,6 @@ fn offset_non_power_two() { let offset = kani::any_where(|o: &usize| *o <= v.len()); let begin = v.as_mut_ptr(); let end = begin.add(offset); - assert_eq!(end.offset_from_unsigned(begin), offset); + assert_eq!(end.sub_ptr(begin), offset); } } diff --git a/tests/kani/SizeAndAlignOfDst/unsized_tuple.rs b/tests/kani/SizeAndAlignOfDst/unsized_tuple.rs new file mode 100644 index 000000000000..0edae52aa0ac --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/unsized_tuple.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Ensure we compute the size correctly including padding for unsized tuple. +#![feature(unsized_tuple_coercion)] + +use std::fmt::Debug; + +#[kani::proof] +fn check_adjusted_tup_size() { + let tup: (u32, [u8; 9]) = kani::any(); + let size = std::mem::size_of_val(&tup); + + let unsized_tup: *const (u32, dyn Debug) = &tup as *const _ as *const _; + let adjusted_size = std::mem::size_of_val(unsafe { &*unsized_tup }); + + assert_eq!(size, adjusted_size); +} diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 398f45fd47cb..95eba4d252ee 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -261,8 +261,7 @@ fn insert_escapes(str: &str, markers: Vec<(ColumnNumber, bool)>, format: &Report escaped_str.insert_str(i + offset, b); // `offset` keeps track of the bytes we've already inserted so the original // index is shifted by the appropriate amount in subsequent insertions. - // Note that b.len() returns the length of the string in bytes, c.f. https://doc.rust-lang.org/std/string/struct.String.html#method.len - offset += b.len(); + offset += b.bytes().len(); } escaped_str } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index f07f4a83afdb..e56008daade1 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -165,9 +165,9 @@ pub fn line_coverage_results( } } } else { - line_status = - std::iter::repeat_n(Some((0, MarkerInfo::FullLine)), end_line - start_line + 1) - .collect(); + line_status = std::iter::repeat(Some((0, MarkerInfo::FullLine))) + .take(end_line - start_line + 1) + .collect(); } line_status } diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs index 1c3907ae1918..89459de72520 100644 --- a/tools/scanner/src/analysis.rs +++ b/tools/scanner/src/analysis.rs @@ -138,7 +138,7 @@ impl OverallStats { if !kind.is_fn() { return None; }; - let unsafe_ops = FnUnsafeOperations::new(item.name()).collect(&item.expect_body()); + let unsafe_ops = FnUnsafeOperations::new(item.name()).collect(&item.body()); let fn_sig = kind.fn_sig().unwrap(); let is_unsafe = fn_sig.skip_binder().safety == Safety::Unsafe; self.fn_stats.get_mut(&item).unwrap().has_unsafe_ops = @@ -167,7 +167,7 @@ impl OverallStats { if !kind.is_fn() { return None; }; - Some(FnLoops::new(item.name()).collect(&item.expect_body())) + Some(FnLoops::new(item.name()).collect(&item.body())) }) .partition::, _>(|props| props.has_loops()); @@ -179,7 +179,7 @@ impl OverallStats { if !kind.is_fn() { return None; }; - Some(FnLoops::new(item.name()).collect(&item.expect_body())) + Some(FnLoops::new(item.name()).collect(&item.body())) }) .partition::, _>(|props| props.has_iterators()); @@ -190,7 +190,7 @@ impl OverallStats { if !kind.is_fn() { return None; }; - let fn_props = FnLoops::new(item.name()).collect(&item.expect_body()); + let fn_props = FnLoops::new(item.name()).collect(&item.body()); self.fn_stats.get_mut(&item).unwrap().has_loop_or_iterator = Some(fn_props.has_iterators() || fn_props.has_loops()); Some(fn_props) @@ -601,7 +601,7 @@ impl Recursion { .into_iter() .filter_map(|item| { if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = item.ty().kind() { - let body = item.expect_body(); + let body = item.body(); let mut visitor = FnCallVisitor { body: &body, fns: vec![] }; visitor.visit_body(&body); Some((def, visitor.fns))