diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 136c4efbdbaa..aa65b0fbeb19 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -118,7 +118,7 @@ impl LlbcCodegenBackend { *instance, &mut ccx.translated, &mut id_map, - &mut *errors_borrow, + &mut errors_borrow, ); let _ = fcx.translate(); } 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 a944d227362e..12ded90f6064 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 @@ -12,20 +12,21 @@ use charon_lib::ast::meta::{ use charon_lib::ast::types::{Ty as CharonTy, TyKind as CharonTyKind}; use charon_lib::ast::{ Abi as CharonAbi, AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind, - Assert as CharonAssert, BinOp as CharonBinOp, Body as CharonBody, - BorrowKind as CharonBorrowKind, BuiltinAdt as CharonBuiltinAdt, - BuiltinAssertKind as CharonBuiltinAssertKind, BuiltinImplData as CharonBuiltinImplData, - BuiltinPathElem as CharonBuiltinPathElem, Call as CharonCall, CastKind as CharonCastKind, - ConstGenericParam as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId, - ConstantExpr as CharonConstantExpr, ConstantExprKind as CharonRawConstantExpr, - DeBruijnId as CharonDeBruijnId, DeBruijnVar as CharonDeBruijnVar, - Disambiguator as CharonDisambiguator, DropKind as CharonDropKind, Field as CharonField, - FieldId as CharonFieldId, File as CharonFile, FileId as CharonFileId, - FileName as CharonFileName, FloatTy as CharonFloatTy, FnOperand as CharonFnOperand, - FnPtr as CharonFnPtr, FnPtrKind as CharonFunIdOrTraitMethodRef, FunDecl as CharonFunDecl, - FunDeclId as CharonFunDeclId, FunSig as CharonFunSig, FunSource as CharonFunSource, - GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, - GlobalDeclId as CharonGlobalDeclId, GlobalDeclRef as CharonGlobalDeclRef, IntTy as CharonIntTy, + Assert as CharonAssert, BinOp as CharonBinOp, Binder as CharonBinder, + BinderKind as CharonBinderKind, Body as CharonBody, BorrowKind as CharonBorrowKind, + BuiltinAdt as CharonBuiltinAdt, BuiltinAssertKind as CharonBuiltinAssertKind, + BuiltinImplData as CharonBuiltinImplData, BuiltinPathElem as CharonBuiltinPathElem, + Call as CharonCall, CastKind as CharonCastKind, ConstGenericParam as CharonConstGenericVar, + ConstGenericVarId as CharonConstGenericVarId, ConstantExpr as CharonConstantExpr, + ConstantExprKind as CharonRawConstantExpr, DeBruijnId as CharonDeBruijnId, + DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator, + DropKind as CharonDropKind, Field as CharonField, FieldId as CharonFieldId, File as CharonFile, + FileId as CharonFileId, FileName as CharonFileName, FloatTy as CharonFloatTy, + FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, FnPtrKind as CharonFunIdOrTraitMethodRef, + FunDecl as CharonFunDecl, FunDeclId as CharonFunDeclId, FunSig as CharonFunSig, + FunSource as CharonFunSource, GenericArgs as CharonGenericArgs, + GenericParams as CharonGenericParams, GlobalDeclId as CharonGlobalDeclId, + GlobalDeclRef as CharonGlobalDeclRef, ImplElem as CharonImplElem, IntTy as CharonIntTy, IntegerTy as CharonIntegerTy, IntegerValue as CharonScalarValue, ItemId as CharonAnyTransId, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, LifetimeMutability as CharonLifetimeMutability, Local as CharonVar, LocalId as CharonVarId, @@ -39,14 +40,15 @@ use charon_lib::ast::{ SwitchScrutinee as CharonSwitchScrutinee, TargetInfo as CharonTargetInfo, TraitClauseId as CharonTraitClauseId, TraitDecl as CharonTraitDecl, TraitDeclId as CharonTraitDeclId, TraitDeclRef as CharonTraitDeclRef, - TraitDeclSource as CharonTraitDeclSource, TraitImplId as CharonTraitImplId, + TraitDeclSource as CharonTraitDeclSource, TraitImpl as CharonTraitImpl, + TraitImplId as CharonTraitImplId, TraitImplSource as CharonTraitImplSource, TraitParam as CharonTraitClause, TraitRef as CharonTraitRef, TraitRefKind as CharonTraitRefKind, TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, TypeDeclId as CharonTypeDeclId, TypeDeclKind as CharonTypeDeclKind, TypeDeclRef as CharonTypeDeclRef, TypeParam as CharonTypeVar, TypeSource as CharonTypeSource, TypeVarId as CharonTypeVarId, UIntTy as CharonUIntTy, UnOp as CharonUnOp, - Variance as CharonVariance, Variant as CharonVariant, VariantId as CharonVariantId, - WithRetag as CharonWithRetag, + VTableDecl as CharonVTableDecl, Variance as CharonVariance, Variant as CharonVariant, + VariantId as CharonVariantId, WithRetag as CharonWithRetag, }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx, Level as CharonLevel}; use charon_lib::ids::IndexVec as CharonVector; @@ -128,10 +130,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let mut local_names = FxHashMap::default(); // populate names of locals for info in instance.body().unwrap().var_debug_info { - if let VarDebugInfoContents::Place(p) = info.value { - if p.projection.is_empty() { - local_names.insert(p.local, info.name); - } + if let VarDebugInfoContents::Place(p) = info.value + && p.projection.is_empty() + { + local_names.insert(p.local, info.name); } } let file_to_id: HashMap = HashMap::new(); @@ -966,7 +968,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { found_crate_name = true; name.push(CharonPathElem::Ident(crate_name.clone(), disambiguator)); } - DefPathData::Impl => {} //will check + DefPathData::Impl => { + let impl_elem = self.impl_path_elem(cur_id); + name.push(CharonPathElem::Impl(impl_elem)); + } DefPathData::OpaqueTy => { // TODO: do nothing for now } @@ -1005,32 +1010,123 @@ impl<'a, 'tcx> Context<'a, 'tcx> { Ok(CharonName { name }) } - /// The name of a function instance: its path, with the method name suffixed by the - /// implementing type when it is defined in an `impl` block. + /// The name of a function instance: its path, in which a method's `impl` block appears as + /// Charon's `PathElem::Impl`. fn def_to_name(&mut self, def: InstanceDef) -> Result { - let mut name = self.defid_to_name(def.def_id())?; - let def_id = rustc_internal::internal(self.tcx(), def.def_id()); - if let Some(impl_defid_internal) = self.tcx.impl_of_assoc(def_id) { - // `{impl}` path elements are skipped, so methods of different impls share a path - // (`core::num::wrapping_add` for every integer type); tell them apart by the - // implementing type. That is the impl's self type for inherent and trait impls - // alike -- only trait impls have a trait ref, and asking an inherent impl for one - // aborted the compiler on any inherent method call. - let self_ty = self.tcx.type_of(impl_defid_internal).skip_binder().to_string(); - if self.tcx.impl_is_of_trait(impl_defid_internal) { - let impl_defid = DefId::to_val(impl_defid_internal.index.as_usize()); - let _impl_id = self.register_trait_impl_id(impl_defid); - } - let funcname = match name.name.pop().unwrap() { - CharonPathElem::Ident(name, _) => name + self_ty.as_str(), - _ => panic!("Expected ident"), - }; - name.name.push(CharonPathElem::Ident(funcname, CharonDisambiguator::new(0))); - }; + let name = self.defid_to_name(def.def_id())?; trace!("{:?}", name); Ok(name) } + /// The path element of an `impl` block, built as in Charon's translation: an inherent impl is + /// identified by its self type (bound by the impl's generics), a trait impl by its declaration, + /// which is created the first time the impl is named. + fn impl_path_elem(&mut self, impl_id: rustc_span::def_id::DefId) -> CharonImplElem { + let impl_def: DefId = rustc_internal::stable(impl_id); + if self.tcx.impl_is_of_trait(impl_id) { + return CharonImplElem::Trait(self.translate_trait_impl(impl_def)); + } + let (params, self_ty) = self.with_item_generics(impl_def, false, |this| { + let params = this.generic_params_from_impl(impl_def); + let self_ty = this.tcx.type_of(impl_id).instantiate_identity().skip_normalization(); + (params, this.translate_ty(rustc_internal::stable(self_ty))) + }); + CharonImplElem::Ty(Box::new(CharonBinder { + params, + skip_binder: self_ty, + kind: CharonBinderKind::InherentImplBlock, + })) + } + + /// Declare the trait impl `impl_def` (if not done yet) and return its id. As with trait + /// declarations, Kani only declares the implemented trait and the generics: no associated + /// items, methods or vtable. + fn translate_trait_impl(&mut self, impl_def: DefId) -> CharonTraitImplId { + // The impl's own name refers to the impl (see `impl_path_elem`), so the id must be + // registered before the name is computed, and the declaration built only once. + let first_time = !self.id_map.contains_key(&impl_def); + let trait_impl_id = self.register_trait_impl_id(impl_def); + if first_time { + let impl_id = rustc_internal::internal(self.tcx, impl_def); + let (generics, impl_trait) = self.with_item_generics(impl_def, false, |this| { + let generics = this.generic_params_from_impl(impl_def); + let trait_ref = this.tcx.impl_trait_ref(impl_id).instantiate_identity(); + let trait_ref: rustc_public::ty::TraitRef = + rustc_internal::stable(trait_ref.skip_normalization()); + let trait_decl_id = this.translate_traitdecl(trait_ref.def_id); + let args = this.translate_generic_args_without_trait(trait_ref.args().clone()); + (generics, CharonTraitDeclRef { id: trait_decl_id, generics: Box::new(args) }) + }); + let item_meta = self.translate_item_meta_from_defid(impl_def); + let trait_impl = CharonTraitImpl { + def_id: trait_impl_id, + item_meta, + src: CharonTraitImplSource::Normal, + impl_trait, + generics, + implied_trait_refs: CharonVector::new(), + consts: Default::default(), + types: Default::default(), + methods: Default::default(), + vtable: CharonVTableDecl::Unknown("Kani does not translate vtables".to_owned()), + }; + self.translated.trait_impls.set_slot(trait_impl_id, trait_impl); + } + trait_impl_id + } + + /// The generic parameters of the `impl` block `impl_def`, in Charon's numbering. Must run in + /// the scope of the impl's generics (`with_item_generics`). + fn generic_params_from_impl(&mut self, impl_def: DefId) -> CharonGenericParams { + let impl_id = rustc_internal::internal(self.tcx, impl_def); + // An impl block has no parent generics. + let params = self.tcx.generics_of(impl_id).own_params.clone(); + let mut regions: CharonVector = CharonVector::new(); + let mut types: CharonVector = CharonVector::new(); + let mut const_generics: CharonVector = + CharonVector::new(); + for param in params { + let position = self.param_position(param.index); + let name = param.name.to_string(); + match param.kind { + rustc_middle::ty::GenericParamDefKind::Lifetime => { + regions.push(CharonRegionVar { + index: CharonRegionId::from_usize(position), + // Charon leaves elided (`'_`) regions unnamed. + name: (name != "'_").then_some(name), + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, + }); + } + rustc_middle::ty::GenericParamDefKind::Type { .. } => { + types.push(CharonTypeVar { + index: CharonTypeVarId::from_usize(position), + name, + variance: CharonVariance::Unknown, + }); + } + rustc_middle::ty::GenericParamDefKind::Const { .. } => { + let ty = self.tcx.type_of(param.def_id).instantiate_identity(); + let ty = self.translate_ty(rustc_internal::stable(ty.skip_normalization())); + const_generics.push(CharonConstGenericVar { + index: CharonConstGenericVarId::from_usize(position), + name, + ty, + }); + } + } + } + CharonGenericParams { + regions, + types, + const_generics, + trait_clauses: self.get_traitclauses_from_defid(impl_def), + regions_outlive: Vec::new(), + types_outlive: Vec::new(), + trait_type_constraints: CharonVector::new(), + } + } + fn adtdef_to_name(&mut self, def: AdtDef) -> Result { self.defid_to_name(def.def_id()) } @@ -1621,8 +1717,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { //Get the Ty of the Place fn place_ty(&self, place: &Place) -> Ty { let body = self.instance.body().unwrap(); - let ty = body.local_decl(place.local).unwrap().ty; - ty + body.local_decl(place.local).unwrap().ty } fn translate_rvalue(&mut self, rvalue: &Rvalue) -> CharonRvalue { diff --git a/scripts/kani-llbc-regression.sh b/scripts/kani-llbc-regression.sh index 9d07814e4ab3..b82dd1b9a34b 100755 --- a/scripts/kani-llbc-regression.sh +++ b/scripts/kani-llbc-regression.sh @@ -17,6 +17,15 @@ ${SCRIPT_DIR}/kani-fmt.sh --check # Build kani cargo build-dev -- --features cprover --features llbc +# The LLBC backend is only built by this script, so its warnings and lints are checked here: CI's +# `-D warnings` build and clippy run cover the default (`cprover`) features only. +# The `-D warnings` build also covers Charon itself: it is a path dependency, and cargo only caps +# lints for registry and git dependencies, so a Charon pin that introduces a warning fails here. +# The clippy run lints `kani-compiler` only. +echo "--- Build and lint the LLBC backend with warnings denied" +RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_llbc_build_warnings --features llbc +cargo clippy -p kani-compiler --features llbc -- -D warnings + # Build compiletest and print configuration. We pick suite / mode combo so there's no test. echo "--- Compiletest configuration" cargo run -p compiletest --quiet -- --suite kani --mode cargo-kani --dry-run --verbose diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 99d8541d7679..ddebd65f5e55 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -119,11 +119,8 @@ cargo clean --manifest-path "$FEATURES_MANIFEST_PATH" # Setting RUSTFLAGS like this always resets cargo's build cache resulting in # all tests to be re-run. I.e., cannot keep re-runing the regression from where # we stopped. -# Only run with the `cprover` feature to avoid compiling the `charon` library -# which is not our code and may have warnings. The downside is that we wouldn't -# detect any warnings in the charon code path. TODO: Remove -# `--no-default-features --features cprover` when the warnings in charon are -# fixed and we advance the charon pin to that version +# Only the `cprover` feature is built here; the LLBC backend (`llbc`, which pulls in Charon) is +# built with warnings denied, and linted, by `kani-llbc-regression.sh`. RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings --no-default-features --features cprover echo diff --git a/tests/llbc/impl_paths/expected b/tests/llbc/impl_paths/expected new file mode 100644 index 000000000000..fadc8b9f88b2 --- /dev/null +++ b/tests/llbc/impl_paths/expected @@ -0,0 +1,18 @@ +// Full name: test::{impl Tr for Wrapper}\ +impl "impl_Tr_for_Wrapper" Tr for Wrapper {\ + vtable: unknown // Kani does not translate vtables\ +} + +// Full name: test::{impl Tr for Wrapper}::m\ +pub fn impl_Tr_for_Wrapper::m<'_0, T, U>(self: &'_0 Wrapper, u: U) -> U + +// Full name: test::{Wrapper}::get\ +pub fn get<'_0, T>(self: &'_0 Wrapper) -> T + +// Full name: test::{impl Tr for &'a u32}::m\ +pub fn {impl Tr for &'a u32}::m<'a, '_1>(self: &'_1 &'a u32, u: u8) -> u8 + +// Full name: test::{impl Tr for &'a u32}\ +impl<'a> Tr for &'a u32 {\ + vtable: unknown // Kani does not translate vtables\ +} diff --git a/tests/llbc/impl_paths/test.rs b/tests/llbc/impl_paths/test.rs new file mode 100644 index 000000000000..07434d3d5de8 --- /dev/null +++ b/tests/llbc/impl_paths/test.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend names methods the way Charon does, with the `impl` +//! block as a path element: `{Wrapper}` for an inherent impl (bound by the impl's generics) +//! and `{impl Tr for Wrapper}` for a trait impl, which is declared. The method's own name +//! used to carry the implementing type as a suffix (`getWrapper`). + +struct Wrapper { + v: T, +} + +impl Wrapper { + fn get(&self) -> T { + self.v + } +} + +trait Tr { + fn m(&self, u: U) -> U; +} + +impl Tr for Wrapper { + fn m(&self, u: U) -> U { + u + } +} + +impl<'a> Tr for &'a u32 { + fn m(&self, u: u8) -> u8 { + u + } +} + +#[kani::proof] +fn main() { + let w = Wrapper { v: 1u8 }; + let _ = w.get(); + let _ = w.m(2u16); + let x = 3u32; + let r = &x; + let _ = r.m(4u8); +} diff --git a/tests/llbc/inherent_core/expected b/tests/llbc/inherent_core/expected index 84fed9697c5f..e38df0399434 100644 --- a/tests/llbc/inherent_core/expected +++ b/tests/llbc/inherent_core/expected @@ -1,5 +1,5 @@ -// Full name: core::num::wrapping_addu8\ -pub fn wrapping_addu8(_1: u8, _2: u8) -> u8\ +// Full name: core::num::{u8}::wrapping_add\ +pub fn wrapping_add(_1: u8, _2: u8) -> u8\ = // Full name: test::wrap\ @@ -10,7 +10,7 @@ pub fn wrap(a: u8, b: u8) -> u8\ let b: u8; // arg #2\ \ storage_live(_0)\ - _0 = wrapping_addu8(copy a, copy b)\ + _0 = wrapping_add(copy a, copy b)\ ↳⚡ undefined_behavior\ storage_dead(b)\ storage_dead(a)\ diff --git a/tests/llbc/inherent_local/expected b/tests/llbc/inherent_local/expected index 57c97bf10cf5..2e07b7d33e71 100644 --- a/tests/llbc/inherent_local/expected +++ b/tests/llbc/inherent_local/expected @@ -3,8 +3,8 @@ pub struct Counter {\ n: u32,\ } -// Full name: test::getCounter\ -pub fn getCounter<'_0>(self: &'_0 Counter) -> u32\ +// Full name: test::{Counter}::get\ +pub fn get<'_0>(self: &'_0 Counter) -> u32\ {\ let _0: u32; // return\ let self: &'_ Counter; // arg #1\ @@ -30,7 +30,7 @@ pub fn main()\ _0 = ()\ c = Counter { n: const 1u32 }\ _3 = &c\ - _2 = getCounter<'_>(move _3)\ + _2 = get<'_>(move _3)\ ↳⚡ undefined_behavior\ storage_dead(_3)\ storage_dead(_2)\ diff --git a/tests/llbc/regions/expected b/tests/llbc/regions/expected index 320fade27327..7f0dd8fb7d9a 100644 --- a/tests/llbc/regions/expected +++ b/tests/llbc/regions/expected @@ -4,11 +4,9 @@ pub fn deref2<'_0, '_1>(x: &'_0 &'_1 u32) -> u32 // Full name: test::early\ pub fn early<'a, T>(x: &'a T) -> &'a T -// Full name: test::getHolder<'a>\ -pub fn getHolder<'a><'a, '_1>(self: &'_1 Holder<'a>) -> u32 +pub fn test::{Holder<'a>}::get<'a, '_1>(self: &'_1 Holder<'a>) -> u32 -// Full name: test::get\ -pub fn get<'_0>(x: Option<&'_0 u32>) -> u32 +pub fn test::get<'_0>(x: Option<&'_0 u32>) -> u32 // Full name: test::pick\ pub fn pick<'a>(x: &'a u32, y: &'a u32, c: bool) -> &'a u32 diff --git a/tests/llbc/traitimpl/expected b/tests/llbc/traitimpl/expected index 4ebedc78c096..4642657ba5d3 100644 --- a/tests/llbc/traitimpl/expected +++ b/tests/llbc/traitimpl/expected @@ -1,10 +1,20 @@ +// Full name: test::{impl T for A}\ +impl "impl_T_for_A" T for A {\ + vtable: unknown // Kani does not translate vtables\ +} + +// Full name: test::{impl T for B}\ +impl "impl_T_for_B" T for B {\ + vtable: unknown // Kani does not translate vtables\ +} + // Full name: test::B\ pub struct B {\ index: i32,\ } -// Full name: test::get_valB\ -pub fn get_valB<'_0>(self: &'_0 B) -> i32\ +// Full name: test::{impl T for B}::get_val\ +pub fn impl_T_for_B::get_val<'_0>(self: &'_0 B) -> i32\ {\ let _0: i32; // return\ let self: &'_ B; // arg #1\ @@ -20,8 +30,8 @@ pub struct A {\ val: i32,\ } -// Full name: test::get_valA\ -pub fn get_valA<'_0>(self: &'_0 A) -> i32\ +// Full name: test::{impl T for A}::get_val\ +pub fn impl_T_for_A::get_val<'_0>(self: &'_0 A) -> i32\ {\ let _0: i32; // return\ let self: &'_ A; // arg #1\ @@ -54,11 +64,11 @@ pub fn main()\ e = A { val: const 3i32 }\ k = B { index: const 3i32 }\ _4 = &e\ - i = get_valA<'_>(move _4)\ + i = impl_T_for_A::get_val<'_>(move _4)\ ↳⚡ undefined_behavior\ storage_dead(_4)\ _6 = &k\ - j = get_valB<'_>(move _6)\ + j = impl_T_for_B::get_val<'_>(move _6)\ ↳⚡ undefined_behavior\ storage_dead(_6)\ storage_dead(j)\