diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 2a29985cb229..5805dc4f7280 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -285,10 +285,13 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type { // give the struct the name "overflow_result_", e.g. // "overflow_result_Unsignedbv" let name: InternedString = format!("overflow_result_{operand_type:?}").into(); - Type::struct_type(name, vec![ - DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type), - DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()), - ]) + Type::struct_type( + name, + vec![ + DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type), + DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()), + ], + ) } /////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index b3e29d8b5c65..5a0ad76b81c6 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -1594,10 +1594,10 @@ mod type_tests { fn check_typedef_struct_properties() { // Create a struct with a random field. let struct_name: InternedString = "MyStruct".into(); - let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field { - name: "field".into(), - typ: Double, - }]); + let struct_type = Type::struct_type( + struct_name, + vec![DatatypeComponent::Field { name: "field".into(), typ: Double }], + ); // Insert a field to the sym table to represent the struct field. let mut sym_table = SymbolTable::new(machine_model_test_stub()); sym_table.ensure(struct_type.type_name().unwrap(), |_, name| { diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs index 6985d4a60dee..51a2b06fd874 100644 --- a/cprover_bindings/src/irep/serialize.rs +++ b/cprover_bindings/src/irep/serialize.rs @@ -149,12 +149,10 @@ mod test { #[test] fn serialize_irep() { let irep = Irep::empty(); - assert_ser_tokens(&irep, &[ - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - ]); + assert_ser_tokens( + &irep, + &[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd], + ); } #[test] @@ -189,77 +187,80 @@ mod test { is_weak: false, }; sym_table.insert(symbol); - assert_ser_tokens(&sym_table, &[ - Token::Map { len: None }, - Token::String("symbolTable"), - Token::Map { len: Some(1) }, - Token::String("my_name"), - // symbol start - Token::Map { len: None }, - // type irep - Token::String("type"), - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - // value irep - Token::String("value"), - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - // value locaton - Token::String("location"), - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - Token::String("name"), - Token::String("my_name"), - Token::String("module"), - Token::String(""), - Token::String("baseName"), - Token::String(""), - Token::String("prettyName"), - Token::String(""), - Token::String("mode"), - Token::String(""), - Token::String("isType"), - Token::Bool(false), - Token::String("isMacro"), - Token::Bool(false), - Token::String("isExported"), - Token::Bool(false), - Token::String("isInput"), - Token::Bool(false), - Token::String("isOutput"), - Token::Bool(false), - Token::String("isStateVar"), - Token::Bool(false), - Token::String("isProperty"), - Token::Bool(false), - Token::String("isStaticLifetime"), - Token::Bool(false), - Token::String("isThreadLocal"), - Token::Bool(false), - Token::String("isLvalue"), - Token::Bool(false), - Token::String("isFileLocal"), - Token::Bool(false), - Token::String("isExtern"), - Token::Bool(false), - Token::String("isVolatile"), - Token::Bool(false), - Token::String("isParameter"), - Token::Bool(false), - Token::String("isAuxiliary"), - Token::Bool(false), - Token::String("isWeak"), - Token::Bool(false), - Token::MapEnd, - Token::MapEnd, - Token::MapEnd, - ]); + assert_ser_tokens( + &sym_table, + &[ + Token::Map { len: None }, + Token::String("symbolTable"), + Token::Map { len: Some(1) }, + Token::String("my_name"), + // symbol start + Token::Map { len: None }, + // type irep + Token::String("type"), + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + // value irep + Token::String("value"), + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + // value locaton + Token::String("location"), + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + Token::String("name"), + Token::String("my_name"), + Token::String("module"), + Token::String(""), + Token::String("baseName"), + Token::String(""), + Token::String("prettyName"), + Token::String(""), + Token::String("mode"), + Token::String(""), + Token::String("isType"), + Token::Bool(false), + Token::String("isMacro"), + Token::Bool(false), + Token::String("isExported"), + Token::Bool(false), + Token::String("isInput"), + Token::Bool(false), + Token::String("isOutput"), + Token::Bool(false), + Token::String("isStateVar"), + Token::Bool(false), + Token::String("isProperty"), + Token::Bool(false), + Token::String("isStaticLifetime"), + Token::Bool(false), + Token::String("isThreadLocal"), + Token::Bool(false), + Token::String("isLvalue"), + Token::Bool(false), + Token::String("isFileLocal"), + Token::Bool(false), + Token::String("isExtern"), + Token::Bool(false), + Token::String("isVolatile"), + Token::Bool(false), + Token::String("isParameter"), + Token::Bool(false), + Token::String("isAuxiliary"), + Token::Bool(false), + Token::String("isWeak"), + Token::Bool(false), + Token::MapEnd, + Token::MapEnd, + Token::MapEnd, + ], + ); } #[test] @@ -268,38 +269,41 @@ mod test { let one_irep = Irep::one(); let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]); let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]); - assert_ser_tokens(&top_irep, &[ - // top_irep - Token::Map { len: None }, - Token::String("id"), - Token::String(""), - Token::String("sub"), - Token::Seq { len: Some(2) }, - // sub_irep - Token::Map { len: None }, - Token::String("id"), - Token::String(""), - Token::String("sub"), - Token::Seq { len: Some(2) }, - // empty_irep - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - // one_irep - Token::Map { len: None }, - Token::String("id"), - Token::String("1"), - Token::MapEnd, - Token::SeqEnd, - Token::MapEnd, - // empty_irep - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - Token::SeqEnd, - Token::MapEnd, - ]); + assert_ser_tokens( + &top_irep, + &[ + // top_irep + Token::Map { len: None }, + Token::String("id"), + Token::String(""), + Token::String("sub"), + Token::Seq { len: Some(2) }, + // sub_irep + Token::Map { len: None }, + Token::String("id"), + Token::String(""), + Token::String("sub"), + Token::Seq { len: Some(2) }, + // empty_irep + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + // one_irep + Token::Map { len: None }, + Token::String("id"), + Token::String("1"), + Token::MapEnd, + Token::SeqEnd, + Token::MapEnd, + // empty_irep + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + Token::SeqEnd, + Token::MapEnd, + ], + ); } } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index e007652a04a9..7fd364e5d725 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -273,12 +273,10 @@ impl ToIrep for ExprValue { )], } } - ExprValue::FunctionCall { function, arguments } => { - side_effect_irep(IrepId::FunctionCall, vec![ - function.to_irep(mm), - arguments_irep(arguments.iter(), mm), - ]) - } + ExprValue::FunctionCall { function, arguments } => side_effect_irep( + IrepId::FunctionCall, + vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)], + ), ExprValue::If { c, t, e } => Irep { id: IrepId::If, sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)], @@ -320,11 +318,10 @@ impl ToIrep for ExprValue { named_sub: linear_map![], }, ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]), - ExprValue::StatementExpression { statements: ops, location: loc } => { - side_effect_irep(IrepId::StatementExpression, vec![ - Stmt::block(ops.to_vec(), *loc).to_irep(mm), - ]) - } + ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep( + IrepId::StatementExpression, + vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)], + ), ExprValue::StringConstant { s } => Irep { id: IrepId::StringConstant, sub: vec![], @@ -491,10 +488,10 @@ impl ToIrep for StmtBody { StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]), StmtBody::Decl { lhs, value } => { if value.is_some() { - code_irep(IrepId::Decl, vec![ - lhs.to_irep(mm), - value.as_ref().unwrap().to_irep(mm), - ]) + code_irep( + IrepId::Decl, + vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)], + ) } else { code_irep(IrepId::Decl, vec![lhs.to_irep(mm)]) } @@ -507,19 +504,18 @@ impl ToIrep for StmtBody { .with_comment("deinit") } StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]), - StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![ - init.to_irep(mm), - cond.to_irep(mm), - update.to_irep(mm), - body.to_irep(mm), - ]), - StmtBody::FunctionCall { lhs, function, arguments } => { - code_irep(IrepId::FunctionCall, vec![ + StmtBody::For { init, cond, update, body } => code_irep( + IrepId::For, + vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)], + ), + StmtBody::FunctionCall { lhs, function, arguments } => code_irep( + IrepId::FunctionCall, + vec![ lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), function.to_irep(mm), arguments_irep(arguments.iter(), mm), - ]) - } + ], + ), StmtBody::Goto { dest, loop_invariants } => { let stmt_goto = code_irep(IrepId::Goto, vec![]) .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())); @@ -532,11 +528,14 @@ impl ToIrep for StmtBody { stmt_goto } } - StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![ - i.to_irep(mm), - t.to_irep(mm), - e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), - ]), + StmtBody::Ifthenelse { i, t, e } => code_irep( + IrepId::Ifthenelse, + vec![ + i.to_irep(mm), + t.to_irep(mm), + e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), + ], + ), StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)]) .with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())), StmtBody::Return(e) => { @@ -548,10 +547,10 @@ impl ToIrep for StmtBody { if default.is_some() { switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm)); } - code_irep(IrepId::Switch, vec![ - control.to_irep(mm), - code_irep(IrepId::Block, switch_arms), - ]) + code_irep( + IrepId::Switch, + vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)], + ) } StmtBody::While { cond, body } => { code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)]) 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 4780b4023a02..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 @@ -1416,10 +1416,13 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } RigidTy::RawPtr(ty, mutability) => { let c_ty = self.translate_ty(ty); - CharonTy::new(CharonTyKind::RawPtr(c_ty, match mutability { - Mutability::Mut => CharonRefKind::Mut, - Mutability::Not => CharonRefKind::Shared, - })) + CharonTy::new(CharonTyKind::RawPtr( + c_ty, + match mutability { + Mutability::Mut => CharonRefKind::Mut, + Mutability::Not => CharonRefKind::Shared, + }, + )) } RigidTy::FnPtr(polyfunsig) => { let value = polyfunsig.value; @@ -1539,9 +1542,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { args: args.iter().map(|arg| self.translate_operand(arg)).collect(), dest: self.translate_place(destination), }; - (Some(CharonRawStatement::Call(call)), CharonRawTerminator::Goto { - target: CharonBlockId::from_usize(target.unwrap()), - }) + ( + Some(CharonRawStatement::Call(call)), + CharonRawTerminator::Goto { + target: CharonBlockId::from_usize(target.unwrap()), + }, + ) } TerminatorKind::Assert { cond, expected, msg: _, target, .. } => ( Some(CharonRawStatement::Assert(CharonAssert { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 8cabd10c87ad..01796a832b78 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}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 7f5568ccf152..860619668c9d 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::{ @@ -851,7 +851,7 @@ impl GotocCtx<'_> { .bytes(), Type::size_t(), ), - NullOp::UbChecks => Expr::c_false(), + NullOp::ContractChecks | NullOp::UbChecks => Expr::c_false(), } } Rvalue::ShallowInitBox(ref operand, content_ty) => { @@ -964,10 +964,10 @@ impl GotocCtx<'_> { pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty) -> Expr { let layout = self.layout_of_stable(ty); assert!( - matches!(&layout.variants, Variants::Multiple { - tag_encoding: TagEncoding::Direct, - .. - }), + matches!( + &layout.variants, + Variants::Multiple { tag_encoding: TagEncoding::Direct, .. } + ), "discriminant field (`case`) only exists for multiple variants and direct encoding" ); let expr = if ty.kind().is_coroutine() { @@ -1505,8 +1505,10 @@ 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_binder = principal.with_self_ty(src_mir_type); - ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder)) + 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) } 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 90635a71f2e8..2d876899f235 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -7,10 +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::{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::{ @@ -552,7 +552,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.map_or(true, |abi| abi.mode != PassMode::Ignore) { + } else if arg_abi.is_none_or(|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 18c121694223..a22528d55407 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -4,6 +4,10 @@ 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::Vector, 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; @@ -17,10 +21,6 @@ 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,6 +371,7 @@ 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a0ae5ae99eff..6077f85e5668 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -23,6 +23,7 @@ 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, }; @@ -40,7 +41,6 @@ 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}; 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 0e5e72af70b6..79410bd3373e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -26,6 +26,7 @@ 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::{ @@ -35,8 +36,7 @@ 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::abi::call::FnAbi; -use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use rustc_target::callconv::FnAbi; use stable_mir::mir::Body; use stable_mir::mir::mono::Instance; use stable_mir::ty::Allocation; diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index b232db8feecb..f0828dace441 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/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 67d32b0079c4..e3ebb20b71d9 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -58,11 +58,8 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { let attributes = KaniAttributes::for_def_id(tcx, item.def_id()); if attributes.has_contract() { - fn_to_data.insert(item.def_id(), ContractedFunction { - function, - file, - harnesses: vec![], - }); + fn_to_data + .insert(item.def_id(), ContractedFunction { function, file, harnesses: vec![] }); } else if let Some((target_name, internal_def_id, _)) = attributes.interpret_for_contract_attribute() { @@ -72,11 +69,14 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { if let Some(cf) = fn_to_data.get_mut(&target_def_id) { cf.harnesses.push(function); } else { - fn_to_data.insert(target_def_id, ContractedFunction { - function: target_name.to_string(), - file, - harnesses: vec![function], - }); + fn_to_data.insert( + target_def_id, + ContractedFunction { + function: target_name.to_string(), + file, + harnesses: vec![function], + }, + ); } } } 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 3d80397530b3..a89baf963e7f 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 @@ -463,19 +463,22 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { // Sanity check. The first argument is the closure itself and the second argument is the tupled arguments from the caller. assert!(args.len() == 2); // First, connect all upvars. - let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { - local: 1usize.into(), - projection: List::empty(), - })]); + let lvalue_set = HashSet::from([MemLoc::new_stack_allocation( + instance, + Place { local: 1usize.into(), projection: List::empty() }, + )]); let rvalue_set = self.successors_for_operand(state, args[0].node.clone()); initial_graph.extend(&lvalue_set, &rvalue_set); // Then, connect the argument tuple to each of the spread arguments. let spread_arg_operand = args[1].node.clone(); for i in 0..new_body.arg_count { - let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { - local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. - projection: List::empty(), - })]); + let lvalue_set = HashSet::from([MemLoc::new_stack_allocation( + instance, + Place { + local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. + projection: List::empty(), + }, + )]); // This conservatively assumes all arguments alias to all parameters. let rvalue_set = self.successors_for_operand(state, spread_arg_operand.clone()); initial_graph.extend(&lvalue_set, &rvalue_set); @@ -483,10 +486,13 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { } else { // Otherwise, simply connect all arguments to parameters. for (i, arg) in args.iter().enumerate() { - let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { - local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. - projection: List::empty(), - })]); + let lvalue_set = HashSet::from([MemLoc::new_stack_allocation( + instance, + Place { + local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. + projection: List::empty(), + }, + )]); let rvalue_set = self.successors_for_operand(state, arg.node.clone()); initial_graph.extend(&lvalue_set, &rvalue_set); } @@ -500,10 +506,10 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { // Connect the return value to the return destination. let lvalue_set = state.resolve_place(*destination, self.instance); - let rvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { - local: 0usize.into(), - projection: List::empty(), - })]); + let rvalue_set = HashSet::from([MemLoc::new_stack_allocation( + instance, + Place { local: 0usize.into(), projection: List::empty() }, + )]); state.extend(&lvalue_set, &state.successors(&rvalue_set)); } @@ -519,7 +525,8 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { Rvalue::Use(operand) | Rvalue::ShallowInitBox(operand, _) | Rvalue::Cast(_, operand, _) - | Rvalue::Repeat(operand, ..) => self.successors_for_operand(state, operand), + | Rvalue::Repeat(operand, ..) + | Rvalue::WrapUnsafeBinder(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. 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 0b52a84eaa59..6e473a84eecc 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,7 +163,8 @@ impl<'tcx> PointsToGraph<'tcx> { | ProjectionElem::Subslice { .. } | ProjectionElem::Downcast(..) | ProjectionElem::OpaqueCast(..) - | ProjectionElem::Subtype(..) => { + | ProjectionElem::Subtype(..) + | ProjectionElem::UnwrapUnsafeBinder(..) => { /* 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 2267af56a684..fdc81e177d1f 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -256,11 +256,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 poly_trait_ref = principal.with_self_ty(concrete_ty); + 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); // Walk all methods of the trait, including those of its supertraits - let entries = - self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref)); + let entries = self.tcx.vtable_entries(trait_ref); let methods = entries.iter().filter_map(|entry| match entry { VtblEntry::MetadataAlign | VtblEntry::MetadataDropInPlace @@ -458,7 +458,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/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 9ad23071df4a..7469508e2c70 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, Rvalue, Statement, StatementKind}, + mir::{FieldIdx, Mutability, Operand, Place, RawPtrKind, 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(Mutability::Not, place.clone()); + let rvalue = Rvalue::AddressOf(RawPtrKind::Const, 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(Mutability::Not, lvalue.clone()); + let address_of = Rvalue::AddressOf(RawPtrKind::Const, 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(Mutability::Not, place.clone()); + 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 }; diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index eba23503dacb..e2c8a153c9a1 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, ConstOperand, FieldIdx, Local, LocalDecl, - MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, - Statement, StatementKind, Terminator, TerminatorKind, + MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, + Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; use stable_mir::target::{MachineInfo, MachineSize}; use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Span, Ty, TyKind, UintTy}; @@ -86,7 +86,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(Mutability::Not, Place::from(value)); + let rvalue_ptr = Rvalue::AddressOf(RawPtrKind::Const, Place::from(value)); for range in ranges { let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source); let msg = diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index fea8a8a1bc3c..41a41d2e73f7 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -434,10 +434,10 @@ impl FunctionWithContractPass { &mut mode_call, InsertPosition::Before, ); - new_body.replace_terminator(&mode_call, Terminator { - kind: TerminatorKind::Goto { target }, - span, - }); + new_body.replace_terminator( + &mode_call, + Terminator { kind: TerminatorKind::Goto { target }, span }, + ); new_body.into() } diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index fd499db7c3c6..090c74311fa4 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_target::abi::FieldIdx::from_usize), + maybe_field_idx.map(rustc_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_target::abi::FieldIdx::from_usize(*field_idx), + rustc_abi::FieldIdx::from_usize(*field_idx), ) }) .collect::>() @@ -215,6 +215,7 @@ impl RustcInternalMir for NullOp { ), ), NullOp::UbChecks => rustc_middle::mir::NullOp::UbChecks, + NullOp::ContractChecks => rustc_middle::mir::NullOp::ContractChecks, } } } @@ -224,8 +225,8 @@ impl RustcInternalMir for Rvalue { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - Rvalue::AddressOf(mutability, place) => { - rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place)) + Rvalue::AddressOf(raw_ptr_kind, place) => { + rustc_middle::mir::Rvalue::RawPtr(internal(tcx, raw_ptr_kind), internal(tcx, place)) } Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate( Box::new(aggregate_kind.internal_mir(tcx)), @@ -545,6 +546,9 @@ 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/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 8001b1f1d359..32caea57750e 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -83,11 +83,14 @@ impl BodyTransformation { // would also make sense to check that the values are initialized before checking their // validity. In the future, it would be nice to have a mechanism to skip automatically // generated code for future instrumentation passes. - transformer.add_pass(queries, UninitPass { - // Since this uses demonic non-determinism under the hood, should not assume the assertion. - check_type: CheckType::new_assert(queries), - mem_init_fn_cache: queries.kani_functions().clone(), - }); + transformer.add_pass( + queries, + UninitPass { + // Since this uses demonic non-determinism under the hood, should not assume the assertion. + check_type: CheckType::new_assert(queries), + mem_init_fn_cache: queries.kani_functions().clone(), + }, + ); transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries)); transformer.add_pass(queries, LoopContractPass::new(tcx, queries, &unit)); transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries)); diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 5b4990790a10..8efabb2c9517 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -4,7 +4,6 @@ //! 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, @@ -16,6 +15,7 @@ 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(Lrc::new(SourceMap::new(FilePathMapping::empty()))), + Some(Arc::new(SourceMap::new(FilePathMapping::empty()))), fallback_bundle, false, HumanReadableErrorType::Default, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index b6050d915666..b26b84ca2632 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -309,9 +309,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, diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index cc48449e01b2..95a2175a2eac 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -22,96 +22,126 @@ static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { map.insert("error_label", vec![]); map.insert("division-by-zero", vec![("division by zero", None)]); map.insert("enum-range-check", vec![("enum range check", None)]); - map.insert("undefined-shift", vec![ - ("shift distance is negative", None), - ("shift distance too large", None), - ("shift operand is negative", None), - ("shift of non-integer type", None), - ]); - map.insert("overflow", vec![ - ("result of signed mod is not representable", None), - ("arithmetic overflow on signed type conversion", None), - ("arithmetic overflow on signed division", None), - ("arithmetic overflow on signed unary minus", None), - ("arithmetic overflow on signed shl", None), - ("arithmetic overflow on unsigned unary minus", None), - ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")), - ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")), - ("arithmetic overflow on signed *", Some("arithmetic overflow on signed multiplication")), - ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")), - ("arithmetic overflow on unsigned -", Some("arithmetic overflow on unsigned subtraction")), - ( - "arithmetic overflow on unsigned *", - Some("arithmetic overflow on unsigned multiplication"), - ), - ("arithmetic overflow on floating-point typecast", None), - ("arithmetic overflow on floating-point division", None), - ("arithmetic overflow on floating-point addition", None), - ("arithmetic overflow on floating-point subtraction", None), - ("arithmetic overflow on floating-point multiplication", None), - ("arithmetic overflow on unsigned to signed type conversion", None), - ("arithmetic overflow on float to signed integer type conversion", None), - ("arithmetic overflow on signed to unsigned type conversion", None), - ("arithmetic overflow on unsigned to unsigned type conversion", None), - ("arithmetic overflow on float to unsigned integer type conversion", None), - ]); - map.insert("NaN", vec![ - ("NaN on +", Some("NaN on addition")), - ("NaN on -", Some("NaN on subtraction")), - ("NaN on /", Some("NaN on division")), - ("NaN on *", Some("NaN on multiplication")), - ]); - map.insert("pointer_arithmetic", vec![ - ("pointer relation: deallocated dynamic object", None), - ("pointer relation: dead object", None), - ("pointer relation: pointer NULL", None), - ("pointer relation: pointer invalid", None), - ("pointer relation: pointer outside dynamic object bounds", None), - ("pointer relation: pointer outside object bounds", None), - ("pointer relation: invalid integer address", None), - ("pointer arithmetic: deallocated dynamic object", None), - ("pointer arithmetic: dead object", None), - ("pointer arithmetic: pointer NULL", None), - ("pointer arithmetic: pointer invalid", None), - ("pointer arithmetic: pointer outside dynamic object bounds", None), - ("pointer arithmetic: pointer outside object bounds", None), - ("pointer arithmetic: invalid integer address", None), - ]); - map.insert("pointer_dereference", vec![ - ( - "dereferenced function pointer must be", - Some("dereference failure: invalid function pointer"), - ), - ("dereference failure: pointer NULL", None), - ("dereference failure: pointer invalid", None), - ("dereference failure: deallocated dynamic object", None), - ("dereference failure: dead object", None), - ("dereference failure: pointer outside dynamic object bounds", None), - ("dereference failure: pointer outside object bounds", None), - ("dereference failure: invalid integer address", None), - ]); + map.insert( + "undefined-shift", + vec![ + ("shift distance is negative", None), + ("shift distance too large", None), + ("shift operand is negative", None), + ("shift of non-integer type", None), + ], + ); + map.insert( + "overflow", + vec![ + ("result of signed mod is not representable", None), + ("arithmetic overflow on signed type conversion", None), + ("arithmetic overflow on signed division", None), + ("arithmetic overflow on signed unary minus", None), + ("arithmetic overflow on signed shl", None), + ("arithmetic overflow on unsigned unary minus", None), + ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")), + ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")), + ( + "arithmetic overflow on signed *", + Some("arithmetic overflow on signed multiplication"), + ), + ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")), + ( + "arithmetic overflow on unsigned -", + Some("arithmetic overflow on unsigned subtraction"), + ), + ( + "arithmetic overflow on unsigned *", + Some("arithmetic overflow on unsigned multiplication"), + ), + ("arithmetic overflow on floating-point typecast", None), + ("arithmetic overflow on floating-point division", None), + ("arithmetic overflow on floating-point addition", None), + ("arithmetic overflow on floating-point subtraction", None), + ("arithmetic overflow on floating-point multiplication", None), + ("arithmetic overflow on unsigned to signed type conversion", None), + ("arithmetic overflow on float to signed integer type conversion", None), + ("arithmetic overflow on signed to unsigned type conversion", None), + ("arithmetic overflow on unsigned to unsigned type conversion", None), + ("arithmetic overflow on float to unsigned integer type conversion", None), + ], + ); + map.insert( + "NaN", + vec![ + ("NaN on +", Some("NaN on addition")), + ("NaN on -", Some("NaN on subtraction")), + ("NaN on /", Some("NaN on division")), + ("NaN on *", Some("NaN on multiplication")), + ], + ); + map.insert( + "pointer_arithmetic", + vec![ + ("pointer relation: deallocated dynamic object", None), + ("pointer relation: dead object", None), + ("pointer relation: pointer NULL", None), + ("pointer relation: pointer invalid", None), + ("pointer relation: pointer outside dynamic object bounds", None), + ("pointer relation: pointer outside object bounds", None), + ("pointer relation: invalid integer address", None), + ("pointer arithmetic: deallocated dynamic object", None), + ("pointer arithmetic: dead object", None), + ("pointer arithmetic: pointer NULL", None), + ("pointer arithmetic: pointer invalid", None), + ("pointer arithmetic: pointer outside dynamic object bounds", None), + ("pointer arithmetic: pointer outside object bounds", None), + ("pointer arithmetic: invalid integer address", None), + ], + ); + map.insert( + "pointer_dereference", + vec![ + ( + "dereferenced function pointer must be", + Some("dereference failure: invalid function pointer"), + ), + ("dereference failure: pointer NULL", None), + ("dereference failure: pointer invalid", None), + ("dereference failure: deallocated dynamic object", None), + ("dereference failure: dead object", None), + ("dereference failure: pointer outside dynamic object bounds", None), + ("dereference failure: pointer outside object bounds", None), + ("dereference failure: invalid integer address", None), + ], + ); // These are very hard to understand without more context. - map.insert("pointer_primitives", vec![ - ("pointer invalid", None), - ("deallocated dynamic object", Some("pointer to deallocated dynamic object")), - ("dead object", Some("pointer to dead object")), - ("pointer outside dynamic object bounds", None), - ("pointer outside object bounds", None), - ("invalid integer address", None), - ]); - map.insert("array_bounds", vec![ - ("lower bound", Some("index out of bounds")), - // This one is redundant: - // ("dynamic object upper bound", Some("access out of bounds")), - ( - "upper bound", - Some("index out of bounds: the length is less than or equal to the given index"), - ), - ]); - map.insert("bit_count", vec![ - ("count trailing zeros is undefined for value zero", None), - ("count leading zeros is undefined for value zero", None), - ]); + map.insert( + "pointer_primitives", + vec![ + ("pointer invalid", None), + ("deallocated dynamic object", Some("pointer to deallocated dynamic object")), + ("dead object", Some("pointer to dead object")), + ("pointer outside dynamic object bounds", None), + ("pointer outside object bounds", None), + ("invalid integer address", None), + ], + ); + map.insert( + "array_bounds", + vec![ + ("lower bound", Some("index out of bounds")), + // This one is redundant: + // ("dynamic object upper bound", Some("access out of bounds")), + ( + "upper bound", + Some("index out of bounds: the length is less than or equal to the given index"), + ), + ], + ); + map.insert( + "bit_count", + vec![ + ("count trailing zeros is undefined for value zero", None), + ("count leading zeros is undefined for value zero", None), + ], + ); map.insert("memory-leak", vec![("dynamically allocated memory never freed", None)]); // These pre-conditions should not print temporary variables since they are embedded in the libc implementation. // They are added via `__CPROVER_precondition`. diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 5c4076f13591..282ae42a7c37 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -500,11 +500,10 @@ mod tests { /// Check that the generated unit tests have the right formatting and indentation #[test] fn format_two_concrete_vals() { - let concrete_vals = - [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, ConcreteVal { - byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], - interp_val: "0l".to_string(), - }]; + let concrete_vals = [ + ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, + ConcreteVal { byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], interp_val: "0l".to_string() }, + ]; let actual: Vec<_> = format_concrete_vals(&concrete_vals).collect(); let expected = vec![ format!("{:<8}// 0", " "), @@ -598,11 +597,10 @@ mod tests { #[test] fn check_rustfmt_args_some_line_ranges() { - let file_line_ranges = - [FileLineRange { file: "file1".to_string(), line_range: None }, FileLineRange { - file: "path/to/file2".to_string(), - line_range: Some((1, 3)), - }]; + let file_line_ranges = [ + FileLineRange { file: "file1".to_string(), line_range: None }, + FileLineRange { file: "path/to/file2".to_string(), line_range: Some((1, 3)) }, + ]; let args = rustfmt_args(&file_line_ranges); let expected: Vec = [ "--unstable-features", diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index af5ac336e09e..3329b1d4b895 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 + 7) / 8 + len.div_ceil(8) } #[cfg(target_endian = "little")] diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 3741e551a5b8..307d7e8a6120 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-01-28" +channel = "nightly-2025-02-10" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/delayed-ub.expected similarity index 88% rename from tests/expected/uninit/delayed-ub/expected rename to tests/expected/uninit/delayed-ub/delayed-ub.expected index b7c139c2d101..f062a30cf6b0 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/tests/expected/uninit/delayed-ub/delayed-ub.expected @@ -2,10 +2,6 @@ delayed_ub_trigger_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_slices.assertion.\ - - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" - delayed_ub_structs.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" @@ -44,7 +40,6 @@ delayed_ub.assertion.\ 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 @@ -54,4 +49,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, 11 failures, 11 total. +Complete - 0 successfully verified harnesses, 10 failures, 10 total. diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index d7f258c27ba5..17b654533406 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -170,19 +170,6 @@ 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/slices_fixme.expected b/tests/expected/uninit/delayed-ub/slices_fixme.expected new file mode 100644 index 000000000000..902980a2bf1c --- /dev/null +++ b/tests/expected/uninit/delayed-ub/slices_fixme.expected @@ -0,0 +1,5 @@ +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 new file mode 100644 index 000000000000..c112a4638363 --- /dev/null +++ b/tests/expected/uninit/delayed-ub/slices_fixme.rs @@ -0,0 +1,21 @@ +// 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/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected index 153024dc692b..0f503b624ca4 100644 --- a/tests/expected/uninit/multiple-instrumentations.expected +++ b/tests/expected/uninit/multiple-instrumentations.expected @@ -1,16 +1,16 @@ -multiple_instrumentations_different_vars.assertion.3\ +multiple_instrumentations_different_vars.assertion\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -multiple_instrumentations_different_vars.assertion.4\ +multiple_instrumentations_different_vars.assertion\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`" -multiple_instrumentations.assertion.2\ +multiple_instrumentations.assertion\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -multiple_instrumentations.assertion.3\ +multiple_instrumentations.assertion\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/expected/zst/expected b/tests/expected/zst/expected index bec891bea92c..3efe59d3445f 100644 --- a/tests/expected/zst/expected +++ b/tests/expected/zst/expected @@ -1,4 +1,4 @@ -Status: FAILURE\ -Description: "dereference failure: pointer NULL" +- Status: FAILURE\ +- Description: "null pointer dereference occurred" VERIFICATION:- FAILED diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 95eba4d252ee..398f45fd47cb 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -261,7 +261,8 @@ 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. - offset += b.bytes().len(); + // 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(); } escaped_str } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index e56008daade1..f07f4a83afdb 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(Some((0, MarkerInfo::FullLine))) - .take(end_line - start_line + 1) - .collect(); + line_status = + std::iter::repeat_n(Some((0, MarkerInfo::FullLine)), end_line - start_line + 1) + .collect(); } line_status }