diff --git a/Cargo.lock b/Cargo.lock index 5ca35559aa8d..9a705c531ec3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -244,7 +244,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.58" +version = "0.1.62" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon b/charon index adc0a855aa14..df3b7fd4c127 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit adc0a855aa1428d68e4270edef0d52131cef06ab +Subproject commit df3b7fd4c1277827c92b4a2cb84347f1f54d92a6 diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 6fc462cbd42d..e87bed0ea388 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -12,10 +12,12 @@ use crate::kani_middle::provide; use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; use crate::kani_queries::QueryDb; -use charon_lib::ast::{AnyTransId, TranslatedCrate}; +use charon_lib::ast::{AnyTransId, TranslatedCrate, meta::ItemOpacity::*, meta::Span}; use charon_lib::errors::ErrorCtx; +use charon_lib::errors::error_or_panic; +use charon_lib::name_matcher::NamePattern; use charon_lib::transform::TransformCtx; -use charon_lib::transform::ctx::TransformOptions; +use charon_lib::transform::ctx::{TransformOptions, TransformPass}; use kani_metadata::ArtifactType; use kani_metadata::{AssignsContract, CompilerArtifactStub}; use rustc_codegen_ssa::back::archive::{ @@ -133,8 +135,8 @@ impl LlbcCodegenBackend { // - compute the order in which to extract the definitions // - find the recursive definitions // - group the mutually recursive definitions - let reordered_decls = charon_lib::reorder_decls::compute_reordered_decls(&ccx); - ccx.translated.ordered_decls = Some(reordered_decls); + let reordered_decls = charon_lib::transform::reorder_decls::Transform {}; + reordered_decls.transform_ctx(&mut ccx); // // ================= @@ -151,10 +153,6 @@ impl LlbcCodegenBackend { // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing // the control flow. - charon_lib::ullbc_to_llbc::translate_functions(&mut ccx); - - trace!("# LLBC resulting from control-flow reconstruction:\n\n{}\n", ccx); - // Run the micro-passes that clean up bodies. for pass in charon_lib::transform::LLBC_PASSES.iter() { pass.run(&mut ccx) @@ -385,17 +383,61 @@ where ret } -fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { - let options = TransformOptions { +fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> TransformOptions { + let mut parse_pattern = |s: &str| match NamePattern::parse(s) { + Ok(p) => Ok(p), + Err(e) => { + let msg = format!("failed to parse pattern `{s}` ({e})"); + error_or_panic!(error_ctx, &TranslatedCrate::default(), Span::dummy(), msg) + } + }; + let options = tcx.options.clone(); + let item_opacities = { + let mut opacities = vec![]; + + // This is how to treat items that don't match any other pattern. + if options.extract_opaque_bodies { + opacities.push(("_".to_string(), Transparent)); + } else { + opacities.push(("_".to_string(), Foreign)); + } + + // We always include the items from the crate. + opacities.push(("crate".to_owned(), Transparent)); + + for pat in options.include.iter() { + opacities.push((pat.to_string(), Transparent)); + } + for pat in options.opaque.iter() { + opacities.push((pat.to_string(), Opaque)); + } + for pat in options.exclude.iter() { + opacities.push((pat.to_string(), Invisible)); + } + + // We always hide this trait. + opacities.push(("core::alloc::Allocator".to_string(), Invisible)); + opacities + .push(("alloc::alloc::{{impl core::alloc::Allocator for _}}".to_string(), Invisible)); + + opacities + .into_iter() + .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity))) + .collect() + }; + TransformOptions { no_code_duplication: false, hide_marker_traits: true, no_merge_goto_chains: false, - item_opacities: Vec::new(), - }; + item_opacities, + print_built_llbc: true, + } +} + +fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); - let mut translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; - //This option setting is for Aeneas compatibility - translated.options.hide_marker_traits = true; - let errors = ErrorCtx::new(true, false); + let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; + let mut errors = ErrorCtx::new(true, false); + let options = get_transform_options(&translated, &mut errors); TransformCtx { options, translated, errors } } 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 58f7561b4fc9..4780b4023a02 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 @@ -14,23 +14,23 @@ use charon_lib::ast::types::{Ty as CharonTy, TyKind as CharonTyKind}; use charon_lib::ast::{ AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind, AnyTransId as CharonAnyTransId, Assert as CharonAssert, BinOp as CharonBinOp, - Body as CharonBody, BodyId as CharonBodyId, BorrowKind as CharonBorrowKind, - BuiltinTy as CharonBuiltinTy, Call as CharonCall, CastKind as CharonCastKind, - ConstGeneric as CharonConstGeneric, ConstGenericVar as CharonConstGenericVar, - ConstGenericVarId as CharonConstGenericVarId, ConstantExpr as CharonConstantExpr, - DeBruijnId as CharonDeBruijnId, DeBruijnVar as CharonDeBruijnVar, - Disambiguator as CharonDisambiguator, ExistentialPredicate as CharonExistentialPredicate, - Field as CharonField, FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, - File as CharonFile, FileId as CharonFileId, FileName as CharonFileName, - FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, FunDecl as CharonFunDecl, - FunDeclId as CharonFunDeclId, FunId as CharonFunId, - FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, FunSig as CharonFunSig, - GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, - GlobalDeclId as CharonGlobalDeclId, GlobalDeclRef as CharonGlobalDeclRef, - IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, - ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, - Locals as CharonLocals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, - PathElem as CharonPathElem, Place as CharonPlace, PolyTraitDeclRef as CharonPolyTraitDeclRef, + Body as CharonBody, BorrowKind as CharonBorrowKind, BuiltinTy as CharonBuiltinTy, + Call as CharonCall, CastKind as CharonCastKind, ConstGeneric as CharonConstGeneric, + ConstGenericVar as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId, + ConstantExpr as CharonConstantExpr, DeBruijnId as CharonDeBruijnId, + DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator, + ExistentialPredicate as CharonExistentialPredicate, Field as CharonField, + FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, File as CharonFile, + FileId as CharonFileId, FileName as CharonFileName, FnOperand as CharonFnOperand, + FnPtr as CharonFnPtr, FunDecl as CharonFunDecl, FunDeclId as CharonFunDeclId, + FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, + FunSig as CharonFunSig, GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, + GenericsSource as CharonGenericsSource, GlobalDeclId as CharonGlobalDeclId, + GlobalDeclRef as CharonGlobalDeclRef, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, + ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, + LiteralTy as CharonLiteralTy, Locals as CharonLocals, Name as CharonName, + Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem, + Place as CharonPlace, PolyTraitDeclRef as CharonPolyTraitDeclRef, PredicateOrigin as CharonPredicateOrigin, ProjectionElem as CharonProjectionElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, RegionBinder as CharonRegionBinder, RegionId as CharonRegionId, RegionVar as CharonRegionVar, @@ -180,7 +180,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { continue; }; let c_traitdecl_id = self.translate_traitdecl(trait_def); - let c_genarg = self.translate_generic_args_without_trait(trait_ref.args().clone()); + let c_genarg = self + .translate_generic_args_without_trait(trait_ref.args().clone(), trait_def.def_id()); let c_polytrait = CharonPolyTraitDeclRef { regions: CharonVector::new(), skip_binder: CharonTraitDeclRef { @@ -221,7 +222,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { continue; }; let c_traitdecl_id = self.translate_traitdecl(trait_def); - let c_genarg = self.translate_generic_args_without_trait(trait_ref.args().clone()); + let c_genarg = self + .translate_generic_args_without_trait(trait_ref.args().clone(), trait_def.def_id()); let c_polytrait = CharonPolyTraitDeclRef { regions: CharonVector::new(), skip_binder: CharonTraitDeclRef { trait_id: c_traitdecl_id, generics: c_genarg }, @@ -1167,19 +1169,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } - fn translate_function_body( - &mut self, - instance: Instance, - ) -> Result { + fn translate_function_body(&mut self, instance: Instance) -> Result { let fndef = match instance.ty().kind() { TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef, _ => panic!("Expected a function type"), }; let mir_body = fndef.body().unwrap(); - let body_id = self.translated.bodies.reserve_slot(); let body = self.translate_body(mir_body); - self.translated.bodies.set_slot(body_id, body); - Ok(body_id) + Ok(body) } fn translate_body(&mut self, mir_body: Body) -> CharonBody { @@ -1195,6 +1192,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_generic_args(&mut self, ga: GenericArgs, defid: DefId) -> CharonGenericArgs { + let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap()); let genvec = ga.0; let mut c_regions: CharonVector = CharonVector::new(); let mut c_types: CharonVector = CharonVector::new(); @@ -1244,6 +1242,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: t_types, const_generics: t_const_generics, trait_refs: trait_ref.trait_decl_ref.skip_binder.generics.trait_refs.clone(), + target: target.clone(), }; let traitdecl_id = trait_ref.trait_decl_ref.skip_binder.trait_id; let subs_traitdeclref = CharonPolyTraitDeclRef { @@ -1264,10 +1263,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs, + target, } } - fn translate_generic_args_without_trait(&mut self, ga: GenericArgs) -> CharonGenericArgs { + fn translate_generic_args_without_trait( + &mut self, + ga: GenericArgs, + defid: DefId, + ) -> CharonGenericArgs { + let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap()); let genvec = ga.0; let mut c_regions: CharonVector = CharonVector::new(); let mut c_types: CharonVector = CharonVector::new(); @@ -1295,6 +1300,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs: CharonVector::new(), + target, } } @@ -1345,12 +1351,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { CharonTypeId::Builtin(CharonBuiltinTy::Str), // TODO: find out whether any of the information below should be // populated for strings - CharonGenericArgs { - regions: CharonVector::new(), - types: CharonVector::new(), - const_generics: CharonVector::new(), - trait_refs: CharonVector::new(), - }, + CharonGenericArgs::empty(CharonGenericsSource::Builtin), )), RigidTy::Array(ty, tyconst) => { let c_ty = self.translate_ty(ty); @@ -1366,6 +1367,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs: CharonVector::new(), + target: CharonGenericsSource::Builtin, }, )) } @@ -1380,12 +1382,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { RigidTy::Tuple(ty) => { let types = ty.iter().map(|ty| self.translate_ty(*ty)).collect(); // TODO: find out if any of the information below is needed - let generic_args = CharonGenericArgs { - regions: CharonVector::new(), - types, - const_generics: CharonVector::new(), - trait_refs: CharonVector::new(), - }; + let generic_args = CharonGenericArgs::new_for_builtin(types); CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args)) } RigidTy::FnDef(def_id, _args) => { @@ -1414,7 +1411,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { c_types.push(c_ty); CharonTy::new(CharonTyKind::Adt( CharonTypeId::Builtin(CharonBuiltinTy::Slice), - CharonGenericArgs::new_from_types(c_types), + CharonGenericArgs::new_for_builtin(c_types), )) } RigidTy::RawPtr(ty, mutability) => { @@ -1672,7 +1669,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { CharonTypeId::Tuple, None, None, - CharonGenericArgs::empty(), + CharonGenericArgs::empty(CharonGenericsSource::Builtin), ), c_operands, ),