From ce7f803d7dedaf14411c43198320965abfa324cd Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 30 Dec 2024 09:49:08 -0800 Subject: [PATCH 1/4] Update charon submodule --- Cargo.lock | 194 ++++++++---------- charon | 2 +- .../codegen_aeneas_llbc/compiler_interface.rs | 13 +- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 56 ++--- 4 files changed, 110 insertions(+), 155 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2d7e93794faf..b98f1aa2b2ae 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,6 +39,16 @@ dependencies = [ "memchr", ] +[[package]] +name = "annotate-snippets" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "710e8eae58854cdc1790fcb56cca04d712a17be849eeb81da2a724bf4bae2bc4" +dependencies = [ + "anstyle", + "unicode-width 0.2.0", +] + [[package]] name = "anstream" version = "0.6.18" @@ -94,12 +104,6 @@ version = "1.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34ac096ce696dc2fcabef30516bb13c0a68a11d30131d3df6f04711467681b04" -[[package]] -name = "arrayvec" -version = "0.5.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" - [[package]] name = "arrayvec" version = "0.7.6" @@ -155,7 +159,7 @@ version = "3.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22" dependencies = [ - "arrayvec 0.7.6", + "arrayvec", ] [[package]] @@ -176,7 +180,7 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", - "which 7.0.1", + "which", ] [[package]] @@ -240,28 +244,27 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.45" +version = "0.1.58" dependencies = [ + "annotate-snippets", + "anstream", "anyhow", "assert_cmd", "clap", "colored", - "convert_case 0.6.0", - "derive-visitor", + "convert_case", + "derive_generic_visitor", "env_logger", "hashlink", "index_vec", "indoc", - "itertools 0.13.0", + "itertools", "lazy_static", "log", "macros", "nom", "nom-supreme", "petgraph", - "pretty", - "regex", - "rustc_apfloat", "rustc_version", "serde", "serde-map-to-array", @@ -273,7 +276,7 @@ dependencies = [ "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)", - "which 6.0.3", + "which", ] [[package]] @@ -307,7 +310,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -383,12 +386,6 @@ dependencies = [ "windows-sys 0.59.0", ] -[[package]] -name = "convert_case" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" - [[package]] name = "convert_case" version = "0.6.0" @@ -481,6 +478,41 @@ dependencies = [ "memchr", ] +[[package]] +name = "darling" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f63b86c8a8826a49b8c21f08a2d07338eec8d900540f8630dc76284be802989" +dependencies = [ + "darling_core", + "darling_macro", +] + +[[package]] +name = "darling_core" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "95133861a8032aaea082871032f5815eb9e98cef03fa916ab4500513994df9e5" +dependencies = [ + "fnv", + "ident_case", + "proc-macro2", + "quote", + "strsim", + "syn", +] + +[[package]] +name = "darling_macro" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d336a2a514f6ccccaa3e09b02d41d35330c07ddf03a62165fcec10bb561c7806" +dependencies = [ + "darling_core", + "quote", + "syn", +] + [[package]] name = "deranged" version = "0.3.11" @@ -491,25 +523,26 @@ dependencies = [ ] [[package]] -name = "derive-visitor" -version = "0.4.0" +name = "derive_generic_visitor" +version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d47165df83b9707cbada3216607a5d66125b6a66906de0bc1216c0669767ca9e" +checksum = "e0729a8f5d509da0c280502837a56a9d05c16866ae5b608ef34bd687e9f21af8" dependencies = [ - "derive-visitor-macros", + "derive_generic_visitor_macros", ] [[package]] -name = "derive-visitor-macros" -version = "0.4.0" +name = "derive_generic_visitor_macros" +version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" +checksum = "3c2b7f15bf93ca0d978ecb96792c71a43c629a1e18b2a5de7a35a5d218e6c85e" dependencies = [ - "convert_case 0.4.0", - "itertools 0.10.5", + "convert_case", + "darling", + "itertools", "proc-macro2", "quote", - "syn 1.0.109", + "syn", ] [[package]] @@ -593,6 +626,12 @@ version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + [[package]] name = "foldhash" version = "0.1.4" @@ -691,6 +730,12 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" +[[package]] +name = "ident_case" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" + [[package]] name = "indent_write" version = "2.2.0" @@ -728,15 +773,6 @@ version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" -[[package]] -name = "itertools" -version = "0.10.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" -dependencies = [ - "either", -] - [[package]] name = "itertools" version = "0.13.0" @@ -774,7 +810,7 @@ dependencies = [ "clap", "cprover_bindings", "home", - "itertools 0.13.0", + "itertools", "kani_metadata", "lazy_static", "num", @@ -785,7 +821,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.93", + "syn", "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)", @@ -834,7 +870,7 @@ dependencies = [ "toml", "tracing", "tracing-subscriber", - "which 7.0.1", + "which", ] [[package]] @@ -860,7 +896,7 @@ dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -924,7 +960,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -1222,17 +1258,6 @@ dependencies = [ "termtree", ] -[[package]] -name = "pretty" -version = "0.12.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579" -dependencies = [ - "arrayvec 0.5.2", - "typed-arena", - "unicode-width 0.1.14", -] - [[package]] name = "proc-macro-error-attr2" version = "2.0.0" @@ -1252,7 +1277,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -1391,16 +1416,6 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" -[[package]] -name = "rustc_apfloat" -version = "0.2.2+llvm-462a31f5a5ab" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "121e2195ff969977a4e2b5c9965ea867fce7e4cb5aee5b09dee698a7932d574f" -dependencies = [ - "bitflags", - "smallvec", -] - [[package]] name = "rustc_version" version = "0.4.1" @@ -1497,7 +1512,7 @@ checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -1648,18 +1663,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.93", -] - -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", + "syn", ] [[package]] @@ -1724,7 +1728,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -1735,7 +1739,7 @@ checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -1858,7 +1862,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] [[package]] @@ -1967,12 +1971,6 @@ dependencies = [ "tree-sitter-language", ] -[[package]] -name = "typed-arena" -version = "2.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" - [[package]] name = "unicode-ident" version = "1.0.14" @@ -2046,18 +2044,6 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" -[[package]] -name = "which" -version = "6.0.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4ee928febd44d98f2f459a4a79bd4d928591333a494a10a868418ac1b39cf1f" -dependencies = [ - "either", - "home", - "rustix", - "winsafe", -] - [[package]] name = "which" version = "7.0.1" @@ -2216,5 +2202,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn", ] diff --git a/charon b/charon index 454078ebdb4a..adc0a855aa14 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 454078ebdb4a607e2b21dc115e1ca99b516e436f +Subproject commit adc0a855aa1428d68e4270edef0d52131cef06ab diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 5a5f02969b01..ddc6f6264d1e 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -38,7 +38,6 @@ use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; -use std::collections::{HashMap, HashSet}; use std::fs::File; use std::path::Path; use std::sync::{Arc, Mutex}; @@ -394,16 +393,6 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { }; let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; - let errors = ErrorCtx { - continue_on_failure: true, - error_on_warnings: false, - dcx: &(), - external_decls_with_errors: HashSet::new(), - ignored_failed_decls: HashSet::new(), - external_dep_sources: HashMap::new(), - def_id: None, - def_id_is_local: true, - error_count: 0, - }; + let errors = ErrorCtx::new(true, false); 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 24cb007be0b8..fd1722857237 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 @@ -10,30 +10,11 @@ use charon_lib::ast::meta::{ AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan, }; use charon_lib::ast::types::{ - Ty as CharonTy, TyKind as CharonTyKind, TypeDeclId as CharonTypeDeclId, + Ty as CharonTy, TyKind as CharonTyKind, }; +use charon_lib::ast::krate::TypeDeclId as CharonTypeDeclId; 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, - Disambiguator as CharonDisambiguator, Field as CharonField, FieldId as CharonFieldId, - FieldProjKind as CharonFieldProjKind, 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, - IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, - ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, - Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, - PathElem as CharonPathElem, Place as CharonPlace, ProjectionElem as CharonProjectionElem, - RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, - RegionId as CharonRegionId, RegionVar as CharonRegionVar, Rvalue as CharonRvalue, - ScalarValue as CharonScalarValue, Span as CharonSpan, TranslatedCrate as CharonTranslatedCrate, - TypeDecl as CharonTypeDecl, TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, - TypeVar as CharonTypeVar, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, - VarId as CharonVarId, Variant as CharonVariant, VariantId as CharonVariantId, + 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, Disambiguator as CharonDisambiguator, Field as CharonField, FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, 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, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, Locals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem, Place as CharonPlace, ProjectionElem as CharonProjectionElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, RegionId as CharonRegionId, RegionVar as CharonRegionVar, Rvalue as CharonRvalue, ScalarValue as CharonScalarValue, Span as CharonSpan, TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, Variant as CharonVariant, VariantId as CharonVariantId }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx}; use charon_lib::ids::Vector as CharonVector; @@ -70,7 +51,7 @@ pub struct Context<'a, 'tcx> { instance: Instance, translated: &'a mut CharonTranslatedCrate, id_map: &'a mut FxHashMap, - errors: &'a mut CharonErrorCtx<'tcx>, + errors: &'a mut CharonErrorCtx, local_names: FxHashMap, } @@ -82,7 +63,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { instance: Instance, translated: &'a mut CharonTranslatedCrate, id_map: &'a mut FxHashMap, - errors: &'a mut CharonErrorCtx<'tcx>, + errors: &'a mut CharonErrorCtx, ) -> Self { let mut local_names = FxHashMap::default(); // populate names of locals @@ -102,7 +83,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn span_err(&mut self, span: CharonSpan, msg: &str) { - self.errors.span_err(span, msg); + self.errors.span_err(self.translated, span, msg); } fn continue_on_failure(&self) -> bool { @@ -136,6 +117,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { item_meta, signature, kind: CharonItemKind::Regular, + is_global_initializer: None, body: Ok(body), }; @@ -699,7 +681,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { is_closure: false, closure_info: None, generics: CharonGenericParams::default(), - parent_params_info: None, inputs: args, output: ret_type, } @@ -717,11 +698,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_body(&mut self, mir_body: Body) -> CharonBody { let span = self.translate_span(mir_body.span); let arg_count = self.instance.fn_abi().unwrap().args.len(); - let locals = self.translate_body_locals(&mir_body); + let vars = self.translate_body_locals(&mir_body); + let locals = Locals { vars, arg_count }; let body: CharonBodyContents = mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect(); - let body_expr = CharonExprBody { span, arg_count, locals, body, comments: Vec::new() }; + let body_expr = CharonExprBody { span, locals, body, comments: Vec::new() }; CharonBody::Unstructured(body_expr) } @@ -851,7 +833,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); let output = self.translate_ty(sig.output()); // TODO: populate regions? - CharonTy::new(CharonTyKind::Arrow(CharonVector::new(), inputs, output)) + CharonTy::new(CharonTyKind::Arrow(inputs)) } RigidTy::Adt(adt_def, genarg) => { let def_id = adt_def.def_id(); @@ -1004,10 +986,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_place(&mut self, place: &Place) -> CharonPlace { - let projection = self.translate_projection(place, &place.projection); + let (_projection, ty) = self.translate_projection(place, &place.projection); let local = place.local; let var_id = CharonVarId::from_usize(local); - CharonPlace { var_id, projection } + CharonPlace::new(var_id, ty) } fn place_ty(&self, place: &Place) -> Ty { @@ -1251,7 +1233,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { &mut self, place: &Place, projection: &[ProjectionElem], - ) -> Vec { + ) -> (Vec, CharonTy) { let c_place_ty = self.translate_ty(self.place_ty(place)); let mut c_provec = Vec::new(); let mut current_ty = c_place_ty.clone(); @@ -1292,26 +1274,24 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } ProjectionElem::Index(local) => { let c_operand = - CharonOperand::Copy(CharonPlace::new(CharonVarId::from_usize(*local))); + CharonOperand::Copy(CharonPlace::new(CharonVarId::from_usize(*local), current_ty.clone())); c_provec.push(CharonProjectionElem::Index { - offset: c_operand, + offset: Box::new(c_operand), from_end: false, - ty: current_ty.clone(), }); } _ => continue, } } - c_provec + (c_provec, current_ty) } fn translate_region(&self, region: Region) -> CharonRegion { match region.kind { RegionKind::ReStatic => CharonRegion::Static, RegionKind::ReErased => CharonRegion::Erased, - RegionKind::ReEarlyParam(_) => CharonRegion::Unknown, - RegionKind::ReBound(_, _) | RegionKind::RePlaceholder(_) => { + RegionKind::ReEarlyParam(_) | RegionKind::ReBound(_, _) | RegionKind::RePlaceholder(_) => { todo!("Not yet implemented RegionKind: {:?}", region.kind) } } From 9042391da08ab4614936371f077eb0fb9da80207 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 2 Jan 2025 10:44:04 -0800 Subject: [PATCH 2/4] update charon submodule --- .../codegen_aeneas_llbc/compiler_interface.rs | 20 ++--- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 81 ++++++++++++++----- 2 files changed, 71 insertions(+), 30 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index ddc6f6264d1e..90d00e3773f0 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -35,7 +35,7 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; -use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; use std::fs::File; @@ -111,14 +111,16 @@ impl LlbcCodegenBackend { for item in &items { match item { MonoItem::Fn(instance) => { - let mut fcx = Context::new( - tcx, - *instance, - &mut ccx.translated, - &mut id_map, - &mut ccx.errors, - ); - let _ = fcx.translate(); + if let InstanceKind::Item = instance.kind { + let mut fcx = Context::new( + tcx, + *instance, + &mut ccx.translated, + &mut id_map, + &mut ccx.errors, + ); + let _ = fcx.translate(); + } } MonoItem::Static(_def) => todo!(), MonoItem::GlobalAsm(_) => {} // We have already warned above 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 fd1722857237..fdcefbdadc68 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 @@ -6,15 +6,35 @@ //! This module contains a context for translating stable MIR into Charon's //! unstructured low-level borrow calculus (ULLBC) +use charon_lib::ast::krate::TypeDeclId as CharonTypeDeclId; use charon_lib::ast::meta::{ AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan, }; -use charon_lib::ast::types::{ - Ty as CharonTy, TyKind as CharonTyKind, -}; -use charon_lib::ast::krate::TypeDeclId as CharonTypeDeclId; +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, Disambiguator as CharonDisambiguator, Field as CharonField, FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, 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, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, Locals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem, Place as CharonPlace, ProjectionElem as CharonProjectionElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, RegionId as CharonRegionId, RegionVar as CharonRegionVar, Rvalue as CharonRvalue, ScalarValue as CharonScalarValue, Span as CharonSpan, TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, Variant as CharonVariant, VariantId as CharonVariantId + 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, + DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator, 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, + IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, + ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, + Locals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, + PathElem as CharonPathElem, Place as CharonPlace, ProjectionElem as CharonProjectionElem, + RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, + RegionBinder as CharonRegionBinder, RegionId as CharonRegionId, RegionVar as CharonRegionVar, + Rvalue as CharonRvalue, ScalarValue as CharonScalarValue, Span as CharonSpan, + TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, + TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, + TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, + Variant as CharonVariant, VariantId as CharonVariantId, }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx}; use charon_lib::ids::Vector as CharonVector; @@ -624,14 +644,23 @@ impl<'a, 'tcx> Context<'a, 'tcx> { self.translate_span(instance.def.span()) } + fn file_to_id(&mut self, filename: &CharonFileName) -> Option { + for (id, file) in self.translated.files.iter().enumerate() { + if file.name == *filename { + return Some(CharonFileId::from_usize(id)); + } + } + None + } + /// Compute the span information for MIR span fn translate_span(&mut self, span: Span) -> CharonSpan { let filename = CharonFileName::Local(PathBuf::from(span.get_filename())); - let file_id = match self.translated.file_to_id.get(&filename) { - Some(file_id) => *file_id, + let file_id = match self.file_to_id(&filename) { + Some(file_id) => file_id, None => { - let file_id = self.translated.id_to_file.push(filename.clone()); - self.translated.file_to_id.insert(filename, file_id); + let file = CharonFile { name: filename.clone(), contents: None }; + let file_id = self.translated.files.push(file); file_id } }; @@ -746,9 +775,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_ty(&mut self, ty: Ty) -> CharonTy { match ty.kind() { TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), - TyKind::Param(paramty) => CharonTy::new(CharonTyKind::TypeVar( - CharonTypeVarId::from_usize(paramty.index as usize), - )), + TyKind::Param(paramty) => { + let debr = + CharonDeBruijnVar::free(CharonTypeVarId::from_usize(paramty.index as usize)); + CharonTy::new(CharonTyKind::TypeVar(debr)) + } x => todo!("Not yet implemented translation for TyKind: {:?}", x), } } @@ -760,7 +791,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap() } TyConstKind::Param(paramc) => { - CharonConstGeneric::Var(CharonConstGenericVarId::from_usize(paramc.index as usize)) + let debr = CharonDeBruijnVar::free(CharonConstGenericVarId::from_usize( + paramc.index as usize, + )); + CharonConstGeneric::Var(debr) } _ => todo!(), } @@ -825,15 +859,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }; CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args)) } - RigidTy::FnDef(def_id, args) => { - if !args.0.is_empty() { - unimplemented!("generic args are not yet handled"); - } + RigidTy::FnDef(def_id, _args) => { let sig = def_id.fn_sig().value; let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); let output = self.translate_ty(sig.output()); // TODO: populate regions? - CharonTy::new(CharonTyKind::Arrow(inputs)) + let rb = CharonRegionBinder { + regions: CharonVector::new(), + skip_binder: (inputs, output), + }; + CharonTy::new(CharonTyKind::Arrow(rb)) } RigidTy::Adt(adt_def, genarg) => { let def_id = adt_def.def_id(); @@ -1273,8 +1308,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { current_var = varid.to_index(); } ProjectionElem::Index(local) => { - let c_operand = - CharonOperand::Copy(CharonPlace::new(CharonVarId::from_usize(*local), current_ty.clone())); + let c_operand = CharonOperand::Copy(CharonPlace::new( + CharonVarId::from_usize(*local), + current_ty.clone(), + )); c_provec.push(CharonProjectionElem::Index { offset: Box::new(c_operand), from_end: false, @@ -1291,7 +1328,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { match region.kind { RegionKind::ReStatic => CharonRegion::Static, RegionKind::ReErased => CharonRegion::Erased, - RegionKind::ReEarlyParam(_) | RegionKind::ReBound(_, _) | RegionKind::RePlaceholder(_) => { + RegionKind::ReEarlyParam(_) + | RegionKind::ReBound(_, _) + | RegionKind::RePlaceholder(_) => { todo!("Not yet implemented RegionKind: {:?}", region.kind) } } From 92bf1d5d1150f7692ea37d8eb3f29d47135d1b54 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 2 Jan 2025 14:45:37 -0800 Subject: [PATCH 3/4] add file_id Hashmap --- .../codegen_aeneas_llbc/compiler_interface.rs | 20 +++++++++---------- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 20 +++++++------------ 2 files changed, 16 insertions(+), 24 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 90d00e3773f0..ddc6f6264d1e 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -35,7 +35,7 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; -use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem}; +use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; use std::fs::File; @@ -111,16 +111,14 @@ impl LlbcCodegenBackend { for item in &items { match item { MonoItem::Fn(instance) => { - if let InstanceKind::Item = instance.kind { - let mut fcx = Context::new( - tcx, - *instance, - &mut ccx.translated, - &mut id_map, - &mut ccx.errors, - ); - let _ = fcx.translate(); - } + let mut fcx = Context::new( + tcx, + *instance, + &mut ccx.translated, + &mut id_map, + &mut ccx.errors, + ); + let _ = fcx.translate(); } MonoItem::Static(_def) => todo!(), MonoItem::GlobalAsm(_) => {} // We have already warned above 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 fdcefbdadc68..1664867b087d 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 @@ -61,6 +61,7 @@ use stable_mir::ty::{ MirConst, Region, RegionKind, RigidTy, Span, Ty, TyConst, TyConstKind, TyKind, UintTy, }; use stable_mir::{CrateDef, DefId}; +use std::collections::HashMap; use std::path::PathBuf; use tracing::{debug, trace}; @@ -73,6 +74,7 @@ pub struct Context<'a, 'tcx> { id_map: &'a mut FxHashMap, errors: &'a mut CharonErrorCtx, local_names: FxHashMap, + file_to_id: HashMap, } impl<'a, 'tcx> Context<'a, 'tcx> { @@ -94,8 +96,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } } - - Self { tcx, instance, translated, id_map, errors, local_names } + let file_to_id: HashMap = HashMap::new(); + Self { tcx, instance, translated, id_map, errors, local_names, file_to_id } } fn tcx(&self) -> TyCtxt<'tcx> { @@ -644,23 +646,15 @@ impl<'a, 'tcx> Context<'a, 'tcx> { self.translate_span(instance.def.span()) } - fn file_to_id(&mut self, filename: &CharonFileName) -> Option { - for (id, file) in self.translated.files.iter().enumerate() { - if file.name == *filename { - return Some(CharonFileId::from_usize(id)); - } - } - None - } - /// Compute the span information for MIR span fn translate_span(&mut self, span: Span) -> CharonSpan { let filename = CharonFileName::Local(PathBuf::from(span.get_filename())); - let file_id = match self.file_to_id(&filename) { - Some(file_id) => file_id, + let file_id = match self.file_to_id.get(&filename) { + Some(file_id) => *file_id, None => { let file = CharonFile { name: filename.clone(), contents: None }; let file_id = self.translated.files.push(file); + self.file_to_id.insert(filename, file_id); file_id } }; From 06ccb0bbb28d8fc9caf7d5171b6881cc9bbbcc30 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 2 Jan 2025 16:57:24 -0800 Subject: [PATCH 4/4] Update Cargo.lock --- Cargo.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index b98f1aa2b2ae..6a1e30011044 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -524,18 +524,18 @@ dependencies = [ [[package]] name = "derive_generic_visitor" -version = "0.1.0" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e0729a8f5d509da0c280502837a56a9d05c16866ae5b608ef34bd687e9f21af8" +checksum = "b3e1c241e4f464b614bd7650f1a7c4c0e20e5ef21564d6b916b4c51fd76f7688" dependencies = [ "derive_generic_visitor_macros", ] [[package]] name = "derive_generic_visitor_macros" -version = "0.1.0" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c2b7f15bf93ca0d978ecb96792c71a43c629a1e18b2a5de7a35a5d218e6c85e" +checksum = "885f5274163b5b1720591c0c24b34350a0b05e4774351f9fb3d13c192d8c995b" dependencies = [ "convert_case", "darling",