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 a442766d8ad9..392a43f4c2a8 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 @@ -163,7 +163,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { defid: DefId, ) -> (CharonVector, Vec) { let inter_defid = rustc_internal::internal(self.tcx, defid); - let predicates = self.tcx().predicates_of(inter_defid).predicates.to_vec(); + let predicates = self.tcx().clauses_of(inter_defid).clauses.to_vec(); let mut c_trait_refs: CharonVector = CharonVector::new(); let mut c_spans = Vec::new(); @@ -207,7 +207,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { defid: DefId, ) -> CharonVector { let inter_defid = rustc_internal::internal(self.tcx, defid); - let predicates = self.tcx().predicates_of(inter_defid).predicates.to_vec(); + let predicates = self.tcx().clauses_of(inter_defid).clauses.to_vec(); let mut c_trait_clauses: CharonVector = CharonVector::new(); for (i, (clause, span)) in predicates.iter().enumerate() { @@ -1531,7 +1531,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { _ => todo!(), }; if let Some(content) = content { - let span = self.translate_span(stmt.span); + let span = self.translate_span(stmt.source_info.span); return Some(CharonStatement { span, content, comments_before: Vec::new() }); }; None @@ -1541,7 +1541,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { &mut self, terminator: &Terminator, ) -> (Option, CharonTerminator) { - let span = self.translate_span(terminator.span); + let span = self.translate_span(terminator.source_info.span); let (statement, terminator) = match &terminator.kind { TerminatorKind::Return => (None, CharonRawTerminator::Return), TerminatorKind::Goto { target } => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 07d92fe83134..df20cf590cb7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -127,9 +127,9 @@ impl GotocCtx<'_, '_> { // closure capture of a contract-clause closure, which is valid by // construction (see `CurrentFnCtx::is_capture_ref_local`), so tell // CBMC not to generate pointer-validity checks for it. - self.codegen_span_stable_with_pragmas(stmt.span, &["disable:pointer-check"]) + self.codegen_span_stable_with_pragmas(stmt.source_info.span, &["disable:pointer-check"]) } else { - self.codegen_span_stable(stmt.span) + self.codegen_span_stable(stmt.source_info.span) }; match &stmt.kind { StatementKind::Assign(lhs, rhs) => { @@ -151,7 +151,8 @@ impl GotocCtx<'_, '_> { let msg = "found `#[kani::loop_decreases]` without \ `-Z loop-contracts`. The decreases clause \ will be ignored."; - let internal_span = rustc_internal::internal(self.tcx, stmt.span); + let internal_span = + rustc_internal::internal(self.tcx, stmt.source_info.span); self.tcx.dcx().span_warn(internal_span, msg); return Stmt::skip(location); } @@ -293,8 +294,12 @@ impl GotocCtx<'_, '_> { let maybe_source_region = region_from_coverage_opaque(self.tcx, coverage_opaque, instance); if let Some((source_region, file_name)) = maybe_source_region { - let coverage_stmt = - self.codegen_coverage(&counter_data, stmt.span, source_region, &file_name); + let coverage_stmt = self.codegen_coverage( + &counter_data, + stmt.source_info.span, + source_region, + &file_name, + ); // TODO: Avoid single-statement blocks when conversion of // standalone statements to the irep format is fixed. // More details in @@ -318,7 +323,7 @@ impl GotocCtx<'_, '_> { /// /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s. pub fn codegen_terminator(&mut self, term: &Terminator) -> Stmt { - let loc = self.codegen_span_stable(term.span); + let loc = self.codegen_span_stable(term.source_info.span); let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered(); debug!("handling terminator {:?}", term); //TODO: Instead of doing location::none(), and updating, just putit in when we make the stmt. @@ -369,7 +374,7 @@ impl GotocCtx<'_, '_> { self.codegen_drop(place, target, loc) } TerminatorKind::Call { func, args, destination, target, .. } => { - self.codegen_funcall(func, args, destination, target, term.span) + self.codegen_funcall(func, args, destination, target, term.source_info.span) } TerminatorKind::Assert { cond, expected, msg, target, .. } => { let cond = { @@ -395,7 +400,8 @@ impl GotocCtx<'_, '_> { PropertyClass::SafetyCheck, ), // For all other assert kind we can get the static message. - AssertMessage::NullPointerDereference => { + AssertMessage::NullPointerDereference + | AssertMessage::NullReferenceConstructed => { (msg.description().unwrap(), PropertyClass::SafetyCheck) } AssertMessage::Overflow { .. } @@ -410,7 +416,7 @@ impl GotocCtx<'_, '_> { }; let (msg_str, reach_stmt) = - self.codegen_reachability_check(msg.to_owned(), term.span); + self.codegen_reachability_check(msg.to_owned(), term.source_info.span); Stmt::block( vec![ @@ -799,7 +805,10 @@ impl GotocCtx<'_, '_> { self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc) } // Normal, non-virtual function calls - InstanceKind::Item | InstanceKind::Intrinsic | InstanceKind::Shim => { + InstanceKind::Item + | InstanceKind::Intrinsic + | InstanceKind::LlvmIntrinsic + | InstanceKind::Shim => { // We need to handle FnDef items in a special way because `codegen_operand` compiles them to dummy structs. // (cf. the function documentation) let func_exp = self.codegen_func_expr(instance, loc); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 3384db9d0276..3d51c0330870 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -640,7 +640,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { self.tcx, ty::TypingEnv::fully_monomorphized(), *def_id, - args, + args.skip_binder(), ) .unwrap() .unwrap(); diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 3242c1f8147e..8e2861d83cc6 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -497,9 +497,9 @@ fn impl_derived_candidates(tcx: TyCtxt, def: FnDef) -> FxHashMap> // here would leave such a parameter with primitive candidates only. let mut next = Some(rustc_internal::internal(tcx, def.def_id())); while let Some(def_id) = next { - let generic_predicates = tcx.predicates_of(def_id); - next = generic_predicates.parent; - for (predicate, _span) in generic_predicates.predicates { + let generic_clauses = tcx.clauses_of(def_id); + next = generic_clauses.parent; + for (predicate, _span) in generic_clauses.clauses { let Some(trait_pred) = predicate.as_trait_clause() else { continue }; let trait_pred = trait_pred.skip_binder(); let ty::Param(param_ty) = trait_pred.self_ty().kind() else { continue }; @@ -538,7 +538,7 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool let def_id = rustc_internal::internal(tcx, def.def_id()); let args_internal = rustc_internal::internal(tcx, args); - let predicates = tcx.predicates_of(def_id).instantiate(tcx, args_internal); + let predicates = tcx.clauses_of(def_id).instantiate(tcx, args_internal); for (predicate, _span) in predicates { ocx.register_obligation(Obligation::new( tcx, @@ -623,7 +623,7 @@ fn fn_bound_candidates<'tcx>( let fn_tr = tcx.lang_items().fn_trait(); // Collect Fn-ish trait predicates keyed by the self param index, with tupled inputs. let mut sig_inputs: FxHashMap = FxHashMap::default(); - for (predicate, _span) in tcx.predicates_of(def_id).predicates { + for (predicate, _span) in tcx.clauses_of(def_id).clauses { let Some(tp) = predicate.as_trait_clause() else { continue }; // HRTB bounds (e.g. for<'a> FnOnce(&'a Self)) carry late-bound regions; erase them // rather than skipping the binder, which would leak escaping bound vars into the @@ -645,7 +645,7 @@ fn fn_bound_candidates<'tcx>( } // The return type comes from the FnOnce::Output projection bound. let mut sig_output: FxHashMap = FxHashMap::default(); - for (predicate, _span) in tcx.predicates_of(def_id).predicates { + for (predicate, _span) in tcx.clauses_of(def_id).clauses { let Some(proj) = predicate.as_projection_clause() else { continue }; let proj = tcx.instantiate_bound_regions_with_erased(proj); let rustc_middle::ty::TyKind::Param(param_ty) = proj.projection_term.self_ty().kind() @@ -663,7 +663,7 @@ fn fn_bound_candidates<'tcx>( if inputs.has_param() || output.has_param() { // Signature references other generic parameters: defer construction until a // candidate choice for those parameters is made. - // SAFETY of the transmute-free 'static: predicates_of types live for the whole + // SAFETY of the transmute-free 'static: clauses_of types live for the whole // compilation session ('tcx); we only use them within this query's lifetime. deferred.insert(idx, DeferredFnSpec { inputs, output }); continue; diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index 117906acc67b..9456bb5e892c 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -113,7 +113,7 @@ fn resolve_rust_intrinsic<'tcx>( if let ty::FnDef(def_id, args) = *func_ty.kind() && let Some(symbol) = tcx.intrinsic(def_id) { - return Some((symbol, args)); + return Some((symbol, args.skip_binder())); } None } 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 4b0828b4c679..33ea3f1a4558 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 @@ -359,7 +359,7 @@ fn try_resolve_instance<'tcx>( tcx, TypingEnv::fully_monomorphized(), *def, - args, + args.skip_binder(), DUMMY_SP, )) } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 8cf387862a41..452b6c6cf1ae 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -271,6 +271,11 @@ impl MonoItemsFnCollector<'_, '_> { assert!(is_direct_call, "Expected direct call {instance:?}"); false } + InstanceKind::LlvmIntrinsic => { + // LLVM intrinsics have no Rust body to collect. + assert!(is_direct_call, "Expected direct call {instance:?}"); + false + } InstanceKind::Intrinsic => { // Intrinsics may have a fallback body. assert!(is_direct_call, "Expected direct call {instance:?}"); diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 4a0e9ef1ffd2..96c7737f1613 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -10,7 +10,7 @@ use crate::kani_middle::stable_fn_def; use quote::ToTokens; use rustc_hir::def::{DefKind, Res}; -use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModDefId}; +use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModId}; use rustc_hir::{ItemKind, UseKind}; use rustc_middle::ty::TyCtxt; use rustc_middle::ty::fast_reject::{self, TreatParams}; @@ -522,7 +522,7 @@ enum RelativeResolution { } /// Resolves a path relative to a local module. -fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> RelativeResolution { +fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> RelativeResolution { debug!(?name, ?current_module, "resolve_relative"); let mut glob_imports = vec![]; @@ -590,7 +590,7 @@ fn resolve_in_module<'tcx>( ResolveError::MissingItem { tcx, base: current_module, unresolved: name.to_string() } }), Some(local_id) => { - let result = resolve_relative(tcx, LocalModDefId::new_unchecked(local_id), name); + let result = resolve_relative(tcx, LocalModId::new_unchecked(local_id), name); match result { RelativeResolution::Found(def_id) => Ok(def_id), RelativeResolution::Globs(globs) => { @@ -644,7 +644,7 @@ fn resolve_in_glob_uses<'tcx>( fn resolve_in_glob_use(tcx: TyCtxt, res: &Res, name: &str) -> RelativeResolution { if let Res::Def(DefKind::Mod, def_id) = res { if let Some(local_id) = def_id.as_local() { - resolve_relative(tcx, LocalModDefId::new_unchecked(local_id), name) + resolve_relative(tcx, LocalModId::new_unchecked(local_id), name) } else { resolve_in_foreign_module(tcx, *def_id, name) .map_or(RelativeResolution::Globs(vec![]), RelativeResolution::Found) diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 187c5067aa18..1683f3bad1be 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -12,6 +12,7 @@ use tracing::{debug, trace}; use kani_metadata::HarnessMetadata; use rustc_hir::def_id::DefId; use rustc_middle::mir::Const; +use rustc_middle::ty::RegionExt; use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv}; use rustc_public::mir::ConstOperand; use rustc_public::mir::mono::Instance; diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 83b27d7bf66b..3b730ba83d24 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -11,7 +11,9 @@ use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::mined_invariants::{MinedConjunct, MinedExpr, mine_self_assert_conjuncts}; -use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::body::{ + InsertPosition, MutableBody, SourceInstruction, synthetic_source_info, +}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_middle::{ CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, can_derive_arbitrary, @@ -480,7 +482,7 @@ fn inline_with_assumed_panics( }; bb.statements.push(Statement { kind: StatementKind::Assign(Place::from(cond_lcl), rv), - span: self.span, + source_info: synthetic_source_info(self.span), }); bb.terminator.kind = self .assume_call_terminator(Operand::Move(Place::from(cond_lcl)), target); @@ -511,7 +513,7 @@ fn inline_with_assumed_panics( statements: vec![], terminator: Terminator { kind: TerminatorKind::Unreachable, - span: self.span, + source_info: synthetic_source_info(self.span), }, }, ); @@ -542,7 +544,7 @@ fn inline_with_assumed_panics( Place::from(a), Rvalue::Use(arg_op.clone(), WithRetag::No), ), - span: self.span, + source_info: synthetic_source_info(self.span), }); inner_map.push(a); } @@ -566,11 +568,11 @@ fn inline_with_assumed_panics( WithRetag::No, ), ), - span: self.span, + source_info: synthetic_source_info(self.span), }], terminator: Terminator { kind: TerminatorKind::Goto { target }, - span: self.span, + source_info: synthetic_source_info(self.span), }, }, ); @@ -593,7 +595,7 @@ fn inline_with_assumed_panics( statements: vec![], terminator: Terminator { kind: TerminatorKind::Unreachable, - span: self.span, + source_info: synthetic_source_info(self.span), }, }, ); @@ -629,7 +631,10 @@ fn inline_with_assumed_panics( let planned = ctx.planned; // Commit: split the caller and append all planned blocks at their precomputed indices. - let placeholder = Terminator { kind: TerminatorKind::Goto { target: outer_base }, span }; + let placeholder = Terminator { + kind: TerminatorKind::Goto { target: outer_base }, + source_info: synthetic_source_info(span), + }; let (_goto_bb, actual_continuation) = body.split_with_terminator(source, placeholder); assert_eq!(actual_continuation, continuation); for bb in planned { @@ -1506,7 +1511,10 @@ impl AutomaticArbitraryPass { body.insert_terminator( source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Return, span: source.span(body.blocks()) }, + Terminator { + kind: TerminatorKind::Return, + source_info: synthetic_source_info(source.span(body.blocks())), + }, ); let mut assign_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; let rvalue = Rvalue::Aggregate( @@ -1579,7 +1587,7 @@ impl AutomaticArbitraryPass { new_body.insert_terminator( &mut source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Return, span }, + Terminator { kind: TerminatorKind::Return, source_info: synthetic_source_info(span) }, ); Some(new_body.into()) } @@ -1644,7 +1652,10 @@ impl AutomaticArbitraryPass { new_body.insert_terminator( &mut source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Return, span: ret_span }, + Terminator { + kind: TerminatorKind::Return, + source_info: synthetic_source_info(ret_span), + }, ); return new_body.into(); } @@ -1690,7 +1701,10 @@ impl AutomaticArbitraryPass { new_body.insert_terminator( &mut source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Unreachable, span }, + Terminator { + kind: TerminatorKind::Unreachable, + source_info: synthetic_source_info(span), + }, ); let switch_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; @@ -1712,7 +1726,10 @@ impl AutomaticArbitraryPass { new_body.insert_terminator( &mut source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Unreachable, span }, + Terminator { + kind: TerminatorKind::Unreachable, + source_info: synthetic_source_info(span), + }, ); // insert_call + terminator added two blocks; the failure branch starts at the first. let bad_bb = source.bb() - 2; @@ -1728,7 +1745,7 @@ impl AutomaticArbitraryPass { new_body.insert_terminator( &mut source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Return, span }, + Terminator { kind: TerminatorKind::Return, source_info: synthetic_source_info(span) }, ); let ok_bb = source.bb() - 1; let mut assign_instr = SourceInstruction::Terminator { bb: ok_bb }; @@ -1744,7 +1761,7 @@ impl AutomaticArbitraryPass { discr: Operand::Copy(Place::from(discr_lcl)), targets: SwitchTargets::new(vec![(ok_idx as u128, ok_bb)], bad_bb), }, - span, + source_info: synthetic_source_info(span), }; new_body.replace_terminator(&switch_instr, switch); @@ -1789,7 +1806,10 @@ impl AutomaticArbitraryPass { new_body.insert_terminator( &mut source, InsertPosition::Before, - Terminator { kind: TerminatorKind::Unreachable, span }, + Terminator { + kind: TerminatorKind::Unreachable, + source_info: synthetic_source_info(span), + }, ); let switch_int_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; @@ -1819,7 +1839,7 @@ impl AutomaticArbitraryPass { discr: Operand::Copy(Place::from(discr_lcl)), targets: SwitchTargets::new(branches, otherwise), }, - span: source.span(new_body.blocks()), + source_info: synthetic_source_info(source.span(new_body.blocks())), }; new_body.replace_terminator(&switch_int_instr, match_term); diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index d8ed035b1ba0..ae984c26e220 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -13,6 +13,15 @@ use rustc_public::ty::{GenericArgs, MirConst, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; +/// The `SourceInfo` for a statement or terminator that Kani synthesizes at `span`. +/// +/// As of nightly-2026-08-01 `Statement` and `Terminator` carry a `SourceInfo` (span plus source +/// scope) instead of a bare `Span`. Kani-synthesized MIR does not belong to any inlined scope, so +/// it uses the outermost one -- scope 0, which `Body::new` always allocates. +pub fn synthetic_source_info(span: Span) -> SourceInfo { + SourceInfo { span, scope: 0 } +} + #[derive(Debug)] /// This structure mimics a Body that can actually be modified. pub struct MutableBody { @@ -153,7 +162,10 @@ impl MutableBody { let span = source.span(&self.blocks); let ret_ty = rvalue.ty(&self.locals).unwrap(); let result = self.new_local(ret_ty, span, Mutability::Not); - let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span }; + let stmt = Statement { + kind: StatementKind::Assign(Place::from(result), rvalue), + source_info: synthetic_source_info(span), + }; self.insert_stmt(stmt, source, position); result } @@ -167,7 +179,10 @@ impl MutableBody { position: InsertPosition, ) { let span = source.span(&self.blocks); - let stmt = Statement { kind: StatementKind::Assign(place, rvalue), span }; + let stmt = Statement { + kind: StatementKind::Assign(place, rvalue), + source_info: synthetic_source_info(span), + }; self.insert_stmt(stmt, source, position); } @@ -214,7 +229,7 @@ impl MutableBody { target: Some(new_bb), unwind: UnwindAction::Terminate, }; - let terminator = Terminator { kind, span }; + let terminator = Terminator { kind, source_info: synthetic_source_info(span) }; self.insert_terminator(source, position, terminator); } @@ -243,7 +258,7 @@ impl MutableBody { target: Some(new_bb), unwind: UnwindAction::Terminate, }; - let terminator = Terminator { kind, span }; + let terminator = Terminator { kind, source_info: synthetic_source_info(span) }; self.insert_terminator(source, position, terminator); } @@ -344,7 +359,7 @@ impl MutableBody { *target = split_bb_idx; let new_term = Terminator { kind: TerminatorKind::Goto { target: inserted_bb_idx }, - span: source.span(&self.blocks), + source_info: synthetic_source_info(source.span(&self.blocks)), }; self.split_bb(source, position, new_term); self.blocks.push(bb); @@ -422,7 +437,7 @@ impl MutableBody { statements: vec![new_stmt], terminator: Terminator { kind: TerminatorKind::Goto { target: *target_bb }, - span, + source_info: synthetic_source_info(span), }, }; *target_bb = new_bb_idx; @@ -443,7 +458,7 @@ impl MutableBody { /// Keep all the locals untouched, so they can be reused by the passes if needed. pub fn clear_body(&mut self, kind: TerminatorKind) { self.blocks.clear(); - let terminator = Terminator { kind, span: self.span }; + let terminator = Terminator { kind, source_info: synthetic_source_info(self.span) }; self.blocks.push(BasicBlock { statements: Vec::default(), terminator }) } @@ -513,8 +528,8 @@ pub enum SourceInstruction { impl SourceInstruction { pub fn span(&self, blocks: &[BasicBlock]) -> Span { match *self { - SourceInstruction::Statement { idx, bb } => blocks[bb].statements[idx].span, - SourceInstruction::Terminator { bb } => blocks[bb].terminator.span, + SourceInstruction::Statement { idx, bb } => blocks[bb].statements[idx].source_info.span, + SourceInstruction::Terminator { bb } => blocks[bb].terminator.source_info.span, } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index f788a3b761b3..dbb8c6ed087e 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -6,7 +6,7 @@ use crate::kani_middle::nonnull_pointee; use crate::kani_middle::transform::body::{ - CheckType, InsertPosition, MutableBody, SourceInstruction, + CheckType, InsertPosition, MutableBody, SourceInstruction, synthetic_source_info, }; use relevant_instruction::{InitRelevantInstruction, MemoryInitOp}; use rustc_public::{ @@ -271,7 +271,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), } } PointeeLayout::Slice { element_layout } => { @@ -304,7 +304,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), } } PointeeLayout::TraitObject => { @@ -415,7 +415,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // this will be overriden in add_bb unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), } } PointeeLayout::Slice { element_layout } => { @@ -456,7 +456,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), } } PointeeLayout::TraitObject => { @@ -510,7 +510,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // this will be overriden in add_bb unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), } } }; @@ -596,7 +596,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // this will be overriden in add_bb unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), }; // Construct the basic block and insert it into the body. @@ -635,7 +635,7 @@ impl<'a> UninitInstrumenter<'a> { target: Some(0), // this will be overriden in add_bb unwind: UnwindAction::Terminate, }, - span: source.span(body.blocks()), + source_info: synthetic_source_info(source.span(body.blocks())), }; // Construct the basic block and insert it into the body. @@ -707,7 +707,10 @@ pub fn mk_layout_operand( ); 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 }; + let stmt = Statement { + kind: StatementKind::Assign(Place::from(result), rvalue), + source_info: synthetic_source_info(span), + }; statements.push(stmt); Operand::Move(Place { local: result, projection: vec![] }) 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 d7468526e2af..66547cf9cc60 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 @@ -4,7 +4,9 @@ //! Module containing data structures used in identifying places that need instrumentation and the //! character of instrumentation needed. -use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::body::{ + InsertPosition, MutableBody, SourceInstruction, synthetic_source_info, +}; use rustc_public::{ mir::{FieldIdx, Mutability, Operand, Place, RawPtrKind, Rvalue, Statement, StatementKind}, ty::{RigidTy, Ty}, @@ -274,7 +276,10 @@ fn mk_ref( let rvalue = Rvalue::AddressOf(RawPtrKind::Const, 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 }; + let stmt = Statement { + kind: StatementKind::Assign(Place::from(result), rvalue), + source_info: synthetic_source_info(span), + }; statements.push(stmt); result }; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index d2dc5217b400..f413e8f3a1a0 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -363,10 +363,11 @@ fn data_bytes_for_ty( // Thin pointer, ABI is a single scalar. vec![DataBytes { offset: current_offset, size: value.size(machine_info) }] } - ValueAbi::ScalarPair( - Scalar::Initialized { value: value_first, .. }, - Scalar::Initialized { value: value_second, .. }, - ) => { + ValueAbi::ScalarPair { + a: Scalar::Initialized { value: value_first, .. }, + b: Scalar::Initialized { value: value_second, .. }, + .. + } => { // Fat pointer, ABI is a scalar pair. let FieldsShape::Arbitrary { offsets } = layout.fields else { unreachable!() diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 56baa5e5d55c..52aad2cf06a0 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -208,7 +208,7 @@ impl ValidValueReq { let shape = ty.layout().unwrap().shape(); match shape.abi { ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) - | ValueAbi::ScalarPair(Scalar::Initialized { value, valid_range }, _) => { + | ValueAbi::ScalarPair { a: Scalar::Initialized { value, valid_range }, .. } => { Some(ValidValueReq { offset: 0, size: value.size(machine_info), @@ -216,7 +216,7 @@ impl ValidValueReq { }) } ValueAbi::Scalar(_) - | ValueAbi::ScalarPair(_, _) + | ValueAbi::ScalarPair { .. } | ValueAbi::Vector { .. } | ValueAbi::ScalableVector { .. } | ValueAbi::Aggregate { .. } => None, diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 585d05716ccc..0840f88bb7e6 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -5,7 +5,9 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; -use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::body::{ + InsertPosition, MutableBody, SourceInstruction, synthetic_source_info, +}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; @@ -119,7 +121,7 @@ impl AnyModifiesPass { { let instance = Instance::resolve(self.kani_any.unwrap(), &instance_args).unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); - let span = bb.terminator.span; + let span = bb.terminator.source_info.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); changed = true; @@ -141,7 +143,7 @@ impl AnyModifiesPass { Instance::resolve(self.kani_write_any_slice.unwrap(), &instance_args) .unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); - let span = bb.terminator.span; + let span = bb.terminator.source_info.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } else if let TyKind::RigidTy(RigidTy::Str) = internal_type.kind() { @@ -150,7 +152,7 @@ impl AnyModifiesPass { Instance::resolve(self.kani_write_any_str.unwrap(), &instance_args) .unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); - let span = bb.terminator.span; + let span = bb.terminator.source_info.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } else { @@ -159,7 +161,7 @@ impl AnyModifiesPass { Instance::resolve(self.kani_write_any_slim.unwrap(), &instance_args) .unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); - let span = bb.terminator.span; + let span = bb.terminator.source_info.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } @@ -196,7 +198,10 @@ impl AnyModifiesPass { format!("`{receiver_ty}` doesn't implement `kani::Arbitrary`.") }; tcx.dcx() - .struct_span_err(rustc_internal::internal(tcx, bb.terminator.span), msg) + .struct_span_err( + rustc_internal::internal(tcx, bb.terminator.source_info.span), + msg, + ) .with_help( "All objects in the modifies clause must implement the Arbitrary. \ The return type must also implement the Arbitrary trait if you \ @@ -526,7 +531,10 @@ impl FunctionWithContractPass { } new_body.replace_terminator( &mode_call, - Terminator { kind: TerminatorKind::Goto { target }, span }, + Terminator { + kind: TerminatorKind::Goto { target }, + source_info: synthetic_source_info(span), + }, ); new_body.into() @@ -686,7 +694,7 @@ fn check_mutual_recursion(tcx: TyCtxt, fn_def: FnDef, body: &Body) { if transitive_def.def_id() == fn_def.def_id() { let callee_name = tcx.def_path_str(rustc_internal::internal(tcx, callee_def.def_id())); - let span = rustc_internal::internal(tcx, bb.terminator.span); + let span = rustc_internal::internal(tcx, bb.terminator.source_info.span); tcx.dcx().span_err( span, format!( diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index f7cf38bcb247..f75d6cf4a795 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -400,7 +400,8 @@ impl RustcInternalMir for Statement { type T<'tcx> = rustc_middle::mir::Statement<'tcx>; fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { - let source_info = rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span)); + let source_info = + rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.source_info.span)); let kind = self.kind.internal_mir(tcx); rustc_middle::mir::Statement::new(source_info, kind) } @@ -504,6 +505,9 @@ impl RustcInternalMir for AssertMessage { AssertMessage::NullPointerDereference => { rustc_middle::mir::AssertMessage::NullPointerDereference } + AssertMessage::NullReferenceConstructed => { + rustc_middle::mir::AssertMessage::NullReferenceConstructed + } AssertMessage::Overflow(bin_op, left_operand, right_operand) => { rustc_middle::mir::AssertMessage::Overflow( internal(tcx, bin_op), @@ -597,7 +601,10 @@ impl RustcInternalMir for Terminator { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { rustc_middle::mir::Terminator { - source_info: rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span)), + source_info: rustc_middle::mir::SourceInfo::outermost(internal( + tcx, + self.source_info.span, + )), kind: self.kind.internal_mir(tcx), // Terminators gained MIR-level attributes; the stable representation has no // equivalent, and Kani-synthesized terminators carry none. diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 49fdeee7bf96..7def650ad5fc 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -12,7 +12,7 @@ use crate::kani_middle::abi::LayoutOf; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{ - CheckType, InsertPosition, MutableBody, SourceInstruction, + CheckType, InsertPosition, MutableBody, SourceInstruction, synthetic_source_info, }; use crate::kani_middle::transform::check_uninit::PointeeInfo; use crate::kani_middle::transform::check_uninit::{ @@ -151,7 +151,7 @@ impl IntrinsicGeneratorPass { WithRetag::No, ), ); - let stmt = Statement { kind: assign, span }; + let stmt = Statement { kind: assign, source_info: synthetic_source_info(span) }; new_body.insert_stmt(stmt, &mut terminator, InsertPosition::Before); let machine_info = MachineInfo::target(); @@ -175,7 +175,7 @@ impl IntrinsicGeneratorPass { Operand::Move(Place::from(result)), ); let assign = StatementKind::Assign(Place::from(ret_var), rvalue); - let stmt = Statement { kind: assign, span }; + let stmt = Statement { kind: assign, source_info: synthetic_source_info(span) }; new_body.insert_stmt(stmt, &mut terminator, InsertPosition::Before); } } @@ -226,7 +226,7 @@ impl IntrinsicGeneratorPass { ), ); new_body.insert_stmt( - Statement { kind: assign, span }, + Statement { kind: assign, source_info: synthetic_source_info(span) }, &mut source, InsertPosition::Before, ); @@ -264,7 +264,10 @@ impl IntrinsicGeneratorPass { ), ); new_body.insert_stmt( - Statement { kind: assign, span }, + Statement { + kind: assign, + source_info: synthetic_source_info(span), + }, &mut source, InsertPosition::Before, ); @@ -290,7 +293,7 @@ impl IntrinsicGeneratorPass { target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. unwind: UnwindAction::Terminate, }, - span: source.span(new_body.blocks()), + source_info: synthetic_source_info(source.span(new_body.blocks())), }; // Construct the basic block and insert it into the body. new_body.insert_bb( @@ -333,7 +336,7 @@ impl IntrinsicGeneratorPass { target: Some(0), // The current value does not matter, since it will be overwritten in add_bb. unwind: UnwindAction::Terminate, }, - span: source.span(new_body.blocks()), + source_info: synthetic_source_info(source.span(new_body.blocks())), }; // Construct the basic block and insert it into the body. new_body.insert_bb( diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 9460e556fa42..338399721734 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -9,7 +9,9 @@ use crate::kani_middle::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::KaniModel; use crate::kani_middle::transform::TransformationType; -use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::body::{ + InsertPosition, MutableBody, SourceInstruction, synthetic_source_info, +}; use crate::kani_queries::QueryDb; use crate::rustc_public::CrateDef; use itertools::Itertools; @@ -274,9 +276,12 @@ impl LoopContractPass { &SourceInstruction::Terminator { bb: first_blockid }, new_terminator, ); - let span = body.blocks()[first_blockid].statements.first().unwrap().span; + let span = body.blocks()[first_blockid].statements.first().unwrap().source_info.span; // Add the StorageLive(nthpat) statement at the begining of the same block - let storagelive_stmt = Statement { kind: StatementKind::StorageLive(nthvar), span }; + let storagelive_stmt = Statement { + kind: StatementKind::StorageLive(nthvar), + source_info: synthetic_source_info(span), + }; body.insert_stmt( storagelive_stmt, &mut SourceInstruction::Statement { idx: 0, bb: first_blockid }, @@ -452,7 +457,7 @@ impl LoopContractPass { let new_rval = Rvalue::Aggregate(aggrkind.clone(), new_operands); new_loophead_stmts.push(Statement { kind: StatementKind::Assign(lhs.clone(), new_rval), - span: stmt.span, + source_info: synthetic_source_info(stmt.source_info.span), }); } else if let StatementKind::Assign( lhs, @@ -468,7 +473,7 @@ impl LoopContractPass { ); new_loophead_stmts.push(Statement { kind: StatementKind::Assign(lhs.clone(), new_rval), - span: stmt.span, + source_info: synthetic_source_info(stmt.source_info.span), }); } else { new_loophead_stmts.push(stmt.clone()); @@ -847,10 +852,13 @@ impl LoopContractPass { // For the performance benefits remove the re-assign statements of kaniiter variables // after adding the same one at loop head for block_idx in kaniiter_blocks { - let span = body.blocks()[block_idx].terminator.span; + let span = body.blocks()[block_idx].terminator.source_info.span; body.replace_terminator( &SourceInstruction::Terminator { bb: block_idx }, - Terminator { kind: TerminatorKind::Goto { target: block_idx + 1 }, span }, + Terminator { + kind: TerminatorKind::Goto { target: block_idx + 1 }, + source_info: synthetic_source_info(span), + }, ); } } @@ -1017,7 +1025,7 @@ impl LoopContractPass { &SourceInstruction::Terminator { bb: bb_idx }, Terminator { kind: TerminatorKind::Goto { target: self.new_loop_latches[terminator_target] }, - span: terminator.span, + source_info: synthetic_source_info(terminator.source_info.span), }, ); } @@ -1045,7 +1053,7 @@ impl LoopContractPass { &SourceInstruction::Terminator { bb: bb_idx }, Terminator { kind: TerminatorKind::SwitchInt { discr: discr.clone(), targets: new_targets }, - span: terminator.span, + source_info: synthetic_source_info(terminator.source_info.span), }, ); } @@ -1180,7 +1188,7 @@ impl LoopContractPass { terminator_destination.clone(), Rvalue::Use( Operand::Constant(ConstOperand { - span: terminator.span, + span: terminator.source_info.span, user_ty: None, const_: MirConst::from_bool(true), }), @@ -1206,7 +1214,7 @@ impl LoopContractPass { let new_args = vec![ terminator_args[0].clone(), Operand::Constant(ConstOperand { - span: terminator.span, + span: terminator.source_info.span, user_ty: None, const_: MirConst::try_from_uint(1, UintTy::Usize).unwrap(), }), @@ -1221,14 +1229,14 @@ impl LoopContractPass { target: *terminator_target, unwind: *terminator_unwind, }, - span: terminator.span, + source_info: synthetic_source_info(terminator.source_info.span), }, ); new_body.replace_terminator( &SourceInstruction::Terminator { bb: bb_idx }, Terminator { kind: TerminatorKind::Goto { target: terminator_target.unwrap() }, - span: terminator.span, + source_info: synthetic_source_info(terminator.source_info.span), }, ); // Cache the new loop latch. diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 87cf17281045..1e4f0c99c833 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -117,8 +117,8 @@ impl RustcIntrinsicsPass { // Double check input parameters of `offset` operation. let offset_ty = op2.ty(body.locals()).unwrap(); let pointer_ty = op1.ty(body.locals()).unwrap(); - validate_offset(tcx, offset_ty, statement.span); - validate_raw_ptr(tcx, pointer_ty, statement.span); + validate_offset(tcx, offset_ty, statement.source_info.span); + validate_raw_ptr(tcx, pointer_ty, statement.source_info.span); tcx.dcx().abort_if_errors(); let pointee_ty = pointer_ty.kind().builtin_deref(true).unwrap().ty; @@ -204,7 +204,7 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_, '_> { // Construct the wrapper types needed to insert our resolved model [Instance] // back into the MIR as an operand. let literal = MirConst::try_new_zero_sized(new_instance.ty()).unwrap(); - let span = term.span; + let span = term.source_info.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); self.changed = true; diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index f8e4a656199d..d2770fe7f45e 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -197,7 +197,7 @@ impl MutMirVisitor for ExternFnStubVisitor<'_> { { let instance = Instance::resolve(*new_def, &args).unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); - let span = term.span; + let span = term.source_info.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); self.changed = true; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a2690c311ae3..38b9a5467956 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2026-07-01" +channel = "nightly-2026-08-01" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected index bed39a66b7af..b7057cf1700f 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: null reference produced VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) diff --git a/tests/kani/DynTrait/nested_boxes.rs b/tests/kani/DynTrait/nested_boxes.rs index 6fbf42e08b68..b689a7b01c22 100644 --- a/tests/kani/DynTrait/nested_boxes.rs +++ b/tests/kani/DynTrait/nested_boxes.rs @@ -10,7 +10,7 @@ #![feature(ptr_metadata)] use std::any::Any; -use std::intrinsics::size_of; +use std::mem::size_of; use std::ptr::DynMetadata; include!("../Helpers/vtable_utils_ignore.rs"); diff --git a/tests/kani/DynTrait/vtable_size_align_drop.rs b/tests/kani/DynTrait/vtable_size_align_drop.rs index dd6bf3de0919..5f4b0e131bfb 100644 --- a/tests/kani/DynTrait/vtable_size_align_drop.rs +++ b/tests/kani/DynTrait/vtable_size_align_drop.rs @@ -9,7 +9,7 @@ #![feature(core_intrinsics)] #![feature(ptr_metadata)] -use std::intrinsics::size_of; +use std::mem::size_of; include!("../Helpers/vtable_utils_ignore.rs"); // Different sized data fields on each struct diff --git a/tests/kani/Intrinsics/ConstEval/align_of.rs b/tests/kani/Intrinsics/ConstEval/align_of.rs index 06d8cd9b79a5..2cda8cd23675 100644 --- a/tests/kani/Intrinsics/ConstEval/align_of.rs +++ b/tests/kani/Intrinsics/ConstEval/align_of.rs @@ -3,6 +3,10 @@ // Check that we get the expected results for the `align_of` intrinsic // with common data types +// +// As of nightly-2026-08-01 `std::intrinsics::align_of` is a comptime fn and can only be called at +// compile time, so each call is bound to a `const` and the assertions compare those. That is +// exactly what this directory is about -- const evaluation of the intrinsic. #![feature(core_intrinsics)] use std::intrinsics::align_of; @@ -17,27 +21,47 @@ fn main() { #[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))] { // Scalar types - assert!(align_of::() == 1); - assert!(align_of::() == 2); - assert!(align_of::() == 4); - assert!(align_of::() == 8); - assert!(align_of::() == 16); - assert!(align_of::() == 8); - assert!(align_of::() == 1); - assert!(align_of::() == 2); - assert!(align_of::() == 4); - assert!(align_of::() == 8); - assert!(align_of::() == 16); - assert!(align_of::() == 8); - assert!(align_of::() == 4); - assert!(align_of::() == 8); - assert!(align_of::() == 1); - assert!(align_of::() == 4); + const S1: usize = align_of::(); + assert!(S1 == 1); + const S2: usize = align_of::(); + assert!(S2 == 2); + const S3: usize = align_of::(); + assert!(S3 == 4); + const S4: usize = align_of::(); + assert!(S4 == 8); + const S5: usize = align_of::(); + assert!(S5 == 16); + const S6: usize = align_of::(); + assert!(S6 == 8); + const S7: usize = align_of::(); + assert!(S7 == 1); + const S8: usize = align_of::(); + assert!(S8 == 2); + const S9: usize = align_of::(); + assert!(S9 == 4); + const S10: usize = align_of::(); + assert!(S10 == 8); + const S11: usize = align_of::(); + assert!(S11 == 16); + const S12: usize = align_of::(); + assert!(S12 == 8); + const S13: usize = align_of::(); + assert!(S13 == 4); + const S14: usize = align_of::(); + assert!(S14 == 8); + const S15: usize = align_of::(); + assert!(S15 == 1); + const S16: usize = align_of::(); + assert!(S16 == 4); // Compound types (tuple and array) - assert!(align_of::<(i32, i32)>() == 4); - assert!(align_of::<[i32; 5]>() == 4); + const S17: usize = align_of::<(i32, i32)>(); + assert!(S17 == 4); + const S18: usize = align_of::<[i32; 5]>(); + assert!(S18 == 4); // Custom data types (struct and enum) - assert!(align_of::() == 1); - assert!(align_of::() == 1); + const S19: usize = align_of::(); + assert!(S19 == 1); + const S20: usize = align_of::(); + assert!(S20 == 1); } } diff --git a/tests/kani/Intrinsics/ConstEval/size_of.rs b/tests/kani/Intrinsics/ConstEval/size_of.rs index ef960a34a304..20df637f14f4 100644 --- a/tests/kani/Intrinsics/ConstEval/size_of.rs +++ b/tests/kani/Intrinsics/ConstEval/size_of.rs @@ -3,6 +3,10 @@ // Check that we get the expected results for the `size_of` intrinsic // with common data types +// +// As of nightly-2026-08-01 `std::intrinsics::size_of` is a comptime fn and can only be called at +// compile time, so each call is bound to a `const` and the assertions compare those. That is +// exactly what this directory is about -- const evaluation of the intrinsic. #![feature(core_intrinsics)] use std::intrinsics::size_of; @@ -13,26 +17,46 @@ enum MyEnum {} #[kani::proof] fn main() { // Scalar types - assert!(size_of::() == 1); - assert!(size_of::() == 2); - assert!(size_of::() == 4); - assert!(size_of::() == 8); - assert!(size_of::() == 16); - assert!(size_of::() == 8); - assert!(size_of::() == 1); - assert!(size_of::() == 2); - assert!(size_of::() == 4); - assert!(size_of::() == 8); - assert!(size_of::() == 16); - assert!(size_of::() == 8); - assert!(size_of::() == 4); - assert!(size_of::() == 8); - assert!(size_of::() == 1); - assert!(size_of::() == 4); + const S1: usize = size_of::(); + assert!(S1 == 1); + const S2: usize = size_of::(); + assert!(S2 == 2); + const S3: usize = size_of::(); + assert!(S3 == 4); + const S4: usize = size_of::(); + assert!(S4 == 8); + const S5: usize = size_of::(); + assert!(S5 == 16); + const S6: usize = size_of::(); + assert!(S6 == 8); + const S7: usize = size_of::(); + assert!(S7 == 1); + const S8: usize = size_of::(); + assert!(S8 == 2); + const S9: usize = size_of::(); + assert!(S9 == 4); + const S10: usize = size_of::(); + assert!(S10 == 8); + const S11: usize = size_of::(); + assert!(S11 == 16); + const S12: usize = size_of::(); + assert!(S12 == 8); + const S13: usize = size_of::(); + assert!(S13 == 4); + const S14: usize = size_of::(); + assert!(S14 == 8); + const S15: usize = size_of::(); + assert!(S15 == 1); + const S16: usize = size_of::(); + assert!(S16 == 4); // Compound types (tuple and array) - assert!(size_of::<(i32, i32)>() == 8); - assert!(size_of::<[i32; 5]>() == 20); + const S17: usize = size_of::<(i32, i32)>(); + assert!(S17 == 8); + const S18: usize = size_of::<[i32; 5]>(); + assert!(S18 == 20); // Custom data types (struct and enum) - assert!(size_of::() == 0); - assert!(size_of::() == 0); + const S19: usize = size_of::(); + assert!(S19 == 0); + const S20: usize = size_of::(); + assert!(S20 == 0); }