From d62c26d910d6299e8047c479f7e6de27b0b48c70 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 5 Nov 2024 13:56:09 -0800 Subject: [PATCH] Update Charon submodule to 2024-11-04 --- Cargo.lock | 95 +++++------- charon | 2 +- deny.toml | 2 + .../codegen_aeneas_llbc/compiler_interface.rs | 34 +++-- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 140 ++++++++++-------- 5 files changed, 139 insertions(+), 134 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 316d0ff154df..f810d2c7be22 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -145,18 +145,15 @@ dependencies = [ [[package]] name = "bitflags" -version = "2.6.0" +version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] -name = "bitmaps" -version = "2.1.0" +name = "bitflags" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2" -dependencies = [ - "typenum", -] +checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "brownstone" @@ -249,7 +246,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.36" +version = "0.1.45" dependencies = [ "anyhow", "assert_cmd", @@ -260,7 +257,6 @@ dependencies = [ "derive-visitor", "env_logger", "hashlink", - "im", "index_vec", "indoc", "itertools 0.13.0", @@ -272,6 +268,7 @@ dependencies = [ "petgraph", "pretty", "regex", + "rustc_apfloat", "rustc_version", "serde", "serde-map-to-array", @@ -282,7 +279,7 @@ dependencies = [ "toml", "tracing", "tracing-subscriber", - "tracing-tree 0.3.1", + "tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)", "which", ] @@ -454,7 +451,7 @@ version = "0.27.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df" dependencies = [ - "bitflags", + "bitflags 2.6.0", "crossterm_winapi", "libc", "parking_lot", @@ -703,20 +700,6 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" -[[package]] -name = "im" -version = "15.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9" -dependencies = [ - "bitmaps", - "rand_core", - "rand_xoshiro", - "sized-chunks", - "typenum", - "version_check", -] - [[package]] name = "indent_write" version = "2.2.0" @@ -814,7 +797,7 @@ dependencies = [ "syn 2.0.87", "tracing", "tracing-subscriber", - "tracing-tree 0.4.0", + "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)", ] [[package]] @@ -1121,6 +1104,15 @@ dependencies = [ "autocfg", ] +[[package]] +name = "num_threads" +version = "0.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9" +dependencies = [ + "libc", +] + [[package]] name = "object" version = "0.36.5" @@ -1329,15 +1321,6 @@ dependencies = [ "getrandom", ] -[[package]] -name = "rand_xoshiro" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" -dependencies = [ - "rand_core", -] - [[package]] name = "rayon" version = "1.10.0" @@ -1364,7 +1347,7 @@ version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" dependencies = [ - "bitflags", + "bitflags 2.6.0", ] [[package]] @@ -1417,6 +1400,16 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" +[[package]] +name = "rustc_apfloat" +version = "0.2.1+llvm-462a31f5a5ab" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "886d94c63c812a8037c4faca2607453a0fa4cf82f734665266876b022244543f" +dependencies = [ + "bitflags 1.3.2", + "smallvec", +] + [[package]] name = "rustc_version" version = "0.4.1" @@ -1432,7 +1425,7 @@ version = "0.38.38" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "aa260229e6538e52293eeb577aabd09945a09d6d9cc0fc550ed7529056c2e32a" dependencies = [ - "bitflags", + "bitflags 2.6.0", "errno", "libc", "linux-raw-sys", @@ -1600,16 +1593,6 @@ dependencies = [ "libc", ] -[[package]] -name = "sized-chunks" -version = "0.6.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" -dependencies = [ - "bitmaps", - "typenum", -] - [[package]] name = "smallvec" version = "1.13.2" @@ -1757,7 +1740,9 @@ checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885" dependencies = [ "deranged", "itoa", + "libc", "num-conv", + "num_threads", "powerfmt", "serde", "time-core", @@ -1906,9 +1891,9 @@ dependencies = [ [[package]] name = "tracing-tree" -version = "0.3.1" +version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b56c62d2c80033cb36fae448730a2f2ef99410fe3ecbffc916681a32f6807dbe" +checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c" dependencies = [ "nu-ansi-term 0.50.1", "tracing-core", @@ -1919,10 +1904,10 @@ dependencies = [ [[package]] name = "tracing-tree" version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c" +source = "git+https://github.com/Nadrieril/tracing-tree#841286bfffd3c2200810244506cd127013dbeff9" dependencies = [ "nu-ansi-term 0.50.1", + "time", "tracing-core", "tracing-log", "tracing-subscriber", @@ -1962,12 +1947,6 @@ version = "2.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" -[[package]] -name = "typenum" -version = "1.17.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" - [[package]] name = "unicode-ident" version = "1.0.13" diff --git a/charon b/charon index cdc1dcde447a..2193aa00fd89 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd +Subproject commit 2193aa00fd89e991226ada10d8a8f66e0594f212 diff --git a/deny.toml b/deny.toml index 9866397b4655..e90324704993 100644 --- a/deny.toml +++ b/deny.toml @@ -23,6 +23,7 @@ confidence-threshold = 0.8 # All these exceptions should probably appear in: tools/build-kani/license-notes.txt exceptions = [ { name = "unicode-ident", allow=["Unicode-DFS-2016"] }, + { name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] }, ] [licenses.private] @@ -42,3 +43,4 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] +allow-git = ["https://github.com/Nadrieril/tracing-tree"] diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index f9922f237bd5..9f4365b194b2 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -12,7 +12,7 @@ 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::TranslatedCrate; +use charon_lib::ast::{AnyTransId, TranslatedCrate}; use charon_lib::errors::ErrorCtx; use charon_lib::transform::TransformCtx; use charon_lib::transform::ctx::TransformOptions; @@ -24,7 +24,7 @@ use rustc_codegen_ssa::back::archive::{ use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; -use rustc_data_structures::fx::FxIndexMap; +use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed}; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::EncodedMetadata; @@ -106,13 +106,19 @@ impl LlbcCodegenBackend { // Create a Charon transformation context that will be populated with translation results let mut ccx = create_charon_transformation_context(tcx); + let mut id_map: FxHashMap = FxHashMap::default(); // Translate all the items for item in &items { match item { MonoItem::Fn(instance) => { - let mut fcx = - Context::new(tcx, *instance, &mut ccx.translated, &mut ccx.errors); + let mut fcx = Context::new( + tcx, + *instance, + &mut ccx.translated, + &mut id_map, + &mut ccx.errors, + ); let _ = fcx.translate(); } MonoItem::Static(_def) => todo!(), @@ -140,7 +146,7 @@ impl LlbcCodegenBackend { // Run the micro-passes that clean up bodies. for pass in charon_lib::transform::ULLBC_PASSES.iter() { - pass.transform_ctx(&mut ccx) + pass.run(&mut ccx) } // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing @@ -151,7 +157,7 @@ impl LlbcCodegenBackend { // Run the micro-passes that clean up bodies. for pass in charon_lib::transform::LLBC_PASSES.iter() { - pass.transform_ctx(&mut ccx) + pass.run(&mut ccx) } // Print the LLBC if requested. This is useful for expected tests. @@ -161,8 +167,10 @@ impl LlbcCodegenBackend { debug!("# Final LLBC before serialization:\n\n{}\n", ccx); } - // Display an error report about the external dependencies, if necessary - ccx.errors.report_external_deps_errors(); + // TODO: display an error report about the external dependencies, if necessary + if ccx.errors.error_count > 0 { + todo!() + } let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(&ccx); @@ -393,18 +401,20 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { let options = TransformOptions { no_code_duplication: false, hide_marker_traits: false, + no_merge_goto_chains: false, item_opacities: Vec::new(), }; 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, - errors_as_warnings: false, - dcx: tcx.dcx(), - decls_with_errors: HashSet::new(), + error_on_warnings: false, + dcx: &(), + external_decls_with_errors: HashSet::new(), ignored_failed_decls: HashSet::new(), - dep_sources: HashMap::new(), + external_dep_sources: HashMap::new(), def_id: None, + def_id_is_local: true, error_count: 0, }; 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 23bff8b638b9..35e4d137229d 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 @@ -16,6 +16,7 @@ use charon_lib::ast::Rvalue as CharonRvalue; use charon_lib::ast::Span as CharonSpan; use charon_lib::ast::meta::{AttrInfo, Loc, RawSpan}; use charon_lib::ast::types::Ty as CharonTy; +use charon_lib::ast::types::TyKind as CharonTyKind; use charon_lib::ast::{AbortKind, Body as CharonBody, Var, VarId}; use charon_lib::ast::{ AnyTransId, Assert, BodyId, BuiltinTy, Disambiguator, FileName, FunDecl, FunSig, GenericArgs, @@ -30,7 +31,7 @@ use charon_lib::ast::{ use charon_lib::ast::{ BorrowKind as CharonBorrowKind, ConstantExpr, Operand as CharonOperand, UnOp, }; -use charon_lib::common::Error; +use charon_lib::errors::Error; use charon_lib::errors::ErrorCtx; use charon_lib::ids::Vector; use charon_lib::ullbc_ast::{ @@ -40,13 +41,12 @@ use charon_lib::ullbc_ast::{ }; use charon_lib::{error_assert, error_or_panic}; use rustc_data_structures::fx::FxHashMap; -use rustc_errors::MultiSpan; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; -use rustc_span::def_id::DefId as InternalDefId; use stable_mir::abi::PassMode; use stable_mir::mir::VarDebugInfoContents; use stable_mir::mir::mono::Instance; +use stable_mir::mir::mono::InstanceDef; use stable_mir::mir::{ BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, @@ -65,6 +65,7 @@ pub struct Context<'a, 'tcx> { tcx: TyCtxt<'tcx>, instance: Instance, translated: &'a mut TranslatedCrate, + id_map: &'a mut FxHashMap, errors: &'a mut ErrorCtx<'tcx>, local_names: FxHashMap, } @@ -76,6 +77,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { tcx: TyCtxt<'tcx>, instance: Instance, translated: &'a mut TranslatedCrate, + id_map: &'a mut FxHashMap, errors: &'a mut ErrorCtx<'tcx>, ) -> Self { let mut local_names = FxHashMap::default(); @@ -88,14 +90,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } - Self { tcx, instance, translated, errors, local_names } + Self { tcx, instance, translated, id_map, errors, local_names } } fn tcx(&self) -> TyCtxt<'tcx> { self.tcx } - fn span_err>(&mut self, span: S, msg: &str) { + fn span_err(&mut self, span: CharonSpan, msg: &str) { self.errors.span_err(span, msg); } @@ -105,13 +107,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { /// Perform the translation pub fn translate(&mut self) -> Result<(), ()> { - // Charon's `id_map` is in terms of internal `DefId` - let def_id = rustc_internal::internal(self.tcx(), self.instance.def.def_id()); - // TODO: might want to populate `errors.dep_sources` to help with // debugging - let fid = self.register_fun_decl_id(def_id); + let fid = self.register_fun_decl_id(self.instance.def.def_id()); let item_meta = match self.translate_item_meta_from_rid(self.instance) { Ok(item_meta) => item_meta, @@ -128,14 +127,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } }; - let fun_decl = FunDecl { - def_id: fid, - rust_id: def_id, - item_meta, - signature, - kind: ItemKind::Regular, - body: Ok(body), - }; + let fun_decl = + FunDecl { def_id: fid, item_meta, signature, kind: ItemKind::Regular, body: Ok(body) }; self.translated.fun_decls.set_slot(fid, fun_decl); @@ -143,24 +136,26 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } /// Get or create a `FunDeclId` for the given function - fn register_fun_decl_id(&mut self, def_id: InternalDefId) -> FunDeclId { - let tid = match self.translated.id_map.get(&def_id) { + fn register_fun_decl_id(&mut self, def_id: DefId) -> FunDeclId { + debug!("register_fun_decl_id: {:?}", def_id); + let tid = match self.id_map.get(&def_id) { Some(tid) => *tid, None => { + debug!("***Not found!"); let tid = AnyTransId::Fun(self.translated.fun_decls.reserve_slot()); - self.translated.id_map.insert(def_id, tid); - self.translated.reverse_id_map.insert(tid, def_id); + self.id_map.insert(def_id, tid); self.translated.all_ids.insert(tid); tid } }; - *tid.as_fun() + debug!("register_fun_decl_id: {:?}", self.id_map); + tid.try_into().unwrap() } /// Compute the meta information for a Rust item identified by its id. fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result { let span = self.translate_instance_span(instance); - let name = self.def_id_to_name(instance.def.def_id())?; + let name = self.def_to_name(instance.def)?; // TODO: populate the source text let source_text = None; // TODO: populate the attribute info @@ -181,11 +176,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { /// Retrieve an item name from a [DefId]. /// This function is adapted from Charon: /// https://github.com/AeneasVerif/charon/blob/53530427db2941ce784201e64086766504bc5642/charon/src/bin/charon-driver/translate/translate_ctx.rs#L344 - fn def_id_to_name(&mut self, def_id: DefId) -> Result { + fn def_to_name(&mut self, def: InstanceDef) -> Result { + let def_id = def.def_id(); trace!("{:?}", def_id); - let def_id = rustc_internal::internal(self.tcx(), def_id); let tcx = self.tcx(); - let span = tcx.def_span(def_id); + let span: CharonSpan = self.translate_span(def.span()); + let def_id = rustc_internal::internal(self.tcx(), def_id); // We have to be a bit careful when retrieving names from def ids. For instance, // due to reexports, [`TyCtxt::def_path_str`](TyCtxt::def_path_str) might give @@ -341,7 +337,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { file_id, beg: Loc { line: lineinfo.start_line, col: lineinfo.start_col }, end: Loc { line: lineinfo.end_line, col: lineinfo.end_col }, - rust_span_data: rustc_internal::internal(self.tcx(), span).data(), }; // TODO: populate `generated_from_span` info @@ -405,7 +400,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let body: BodyContents = mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect(); - let body_expr = ExprBody { span, arg_count, locals, body }; + let body_expr = ExprBody { span, arg_count, locals, body, comments: Vec::new() }; CharonBody::Unstructured(body_expr) } @@ -424,12 +419,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_rigid_ty(&self, rigid_ty: RigidTy) -> CharonTy { debug!("translate_rigid_ty: {rigid_ty:?}"); match rigid_ty { - RigidTy::Bool => CharonTy::Literal(LiteralTy::Bool), - RigidTy::Char => CharonTy::Literal(LiteralTy::Char), - RigidTy::Int(it) => CharonTy::Literal(LiteralTy::Integer(translate_int_ty(it))), - RigidTy::Uint(uit) => CharonTy::Literal(LiteralTy::Integer(translate_uint_ty(uit))), - RigidTy::Never => CharonTy::Never, - RigidTy::Str => CharonTy::Adt( + RigidTy::Bool => CharonTy::new(CharonTyKind::Literal(LiteralTy::Bool)), + RigidTy::Char => CharonTy::new(CharonTyKind::Literal(LiteralTy::Char)), + RigidTy::Int(it) => { + CharonTy::new(CharonTyKind::Literal(LiteralTy::Integer(translate_int_ty(it)))) + } + RigidTy::Uint(uit) => { + CharonTy::new(CharonTyKind::Literal(LiteralTy::Integer(translate_uint_ty(uit)))) + } + RigidTy::Never => CharonTy::new(CharonTyKind::Never), + RigidTy::Str => CharonTy::new(CharonTyKind::Adt( TypeId::Builtin(BuiltinTy::Str), // TODO: find out whether any of the information below should be // populated for strings @@ -439,15 +438,15 @@ impl<'a, 'tcx> Context<'a, 'tcx> { const_generics: Vector::new(), trait_refs: Vector::new(), }, - ), - RigidTy::Ref(region, ty, mutability) => CharonTy::Ref( + )), + RigidTy::Ref(region, ty, mutability) => CharonTy::new(CharonTyKind::Ref( self.translate_region(region), - Box::new(self.translate_ty(ty)), + self.translate_ty(ty), match mutability { Mutability::Mut => RefKind::Mut, Mutability::Not => RefKind::Shared, }, - ), + )), 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 @@ -457,7 +456,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { const_generics: Vector::new(), trait_refs: Vector::new(), }; - CharonTy::Adt(TypeId::Tuple, generic_args) + CharonTy::new(CharonTyKind::Adt(TypeId::Tuple, generic_args)) } RigidTy::FnDef(def_id, args) => { if !args.0.is_empty() { @@ -467,7 +466,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::Arrow(Vector::new(), inputs, Box::new(output)) + CharonTy::new(CharonTyKind::Arrow(Vector::new(), inputs, output)) } _ => todo!(), } @@ -488,9 +487,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_block(&mut self, bb: &BasicBlock) -> BlockData { - let statements = + let mut statements: Vec = bb.statements.iter().filter_map(|stmt| self.translate_statement(stmt)).collect(); - let terminator = self.translate_terminator(&bb.terminator); + let (statement, terminator) = self.translate_terminator(&bb.terminator); + if let Some(statement) = statement { + statements.push(statement); + } BlockData { statements, terminator } } @@ -520,21 +522,27 @@ impl<'a, 'tcx> Context<'a, 'tcx> { None } - fn translate_terminator(&mut self, terminator: &Terminator) -> CharonTerminator { + fn translate_terminator( + &mut self, + terminator: &Terminator, + ) -> (Option, CharonTerminator) { let span = self.translate_span(terminator.span); - let content = match &terminator.kind { - TerminatorKind::Return => RawTerminator::Return, + let (statement, terminator) = match &terminator.kind { + TerminatorKind::Return => (None, RawTerminator::Return), TerminatorKind::Goto { target } => { - RawTerminator::Goto { target: BlockId::from_usize(*target) } + (None, RawTerminator::Goto { target: BlockId::from_usize(*target) }) + } + TerminatorKind::Unreachable => { + (None, RawTerminator::Abort(AbortKind::UndefinedBehavior)) + } + TerminatorKind::Drop { place, target, .. } => { + (Some(RawStatement::Drop(self.translate_place(&place))), RawTerminator::Goto { + target: BlockId::from_usize(*target), + }) } - TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior), - TerminatorKind::Drop { place, target, .. } => RawTerminator::Drop { - place: self.translate_place(&place), - target: BlockId::from_usize(*target), - }, TerminatorKind::SwitchInt { discr, targets } => { let (discr, targets) = self.translate_switch_targets(discr, targets); - RawTerminator::Switch { discr, targets } + (None, RawTerminator::Switch { discr, targets }) } TerminatorKind::Call { func, args, destination, target, .. } => { debug!("translate_call: {func:?} {args:?} {destination:?} {target:?}"); @@ -542,7 +550,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let fn_ptr = match fn_ty.kind() { TyKind::RigidTy(RigidTy::FnDef(def, args)) => { let instance = Instance::resolve(def, &args).unwrap(); - let def_id = rustc_internal::internal(self.tcx(), instance.def.def_id()); + let def_id = instance.def.def_id(); let fid = self.register_fun_decl_id(def_id); FnPtr { func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fid)), @@ -567,17 +575,23 @@ impl<'a, 'tcx> Context<'a, 'tcx> { args: args.iter().map(|arg| self.translate_operand(arg)).collect(), dest: self.translate_place(destination), }; - RawTerminator::Call { call, target: target.map(BlockId::from_usize) } - } - TerminatorKind::Assert { cond, expected, msg: _, target, .. } => { - RawTerminator::Assert { - assert: Assert { cond: self.translate_operand(cond), expected: *expected }, - target: BlockId::from_usize(*target), - } + (Some(RawStatement::Call(call)), RawTerminator::Goto { + target: BlockId::from_usize(target.unwrap()), + }) } + TerminatorKind::Assert { cond, expected, msg: _, target, .. } => ( + Some(RawStatement::Assert(Assert { + cond: self.translate_operand(cond), + expected: *expected, + })), + RawTerminator::Goto { target: BlockId::from_usize(*target) }, + ), _ => todo!(), }; - CharonTerminator { span, content } + ( + statement.map(|statement| CharonStatement { span, content: statement }), + CharonTerminator { span, content: terminator }, + ) } fn translate_place(&self, place: &Place) -> CharonPlace { @@ -707,7 +721,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { if value == 0 { (targets.otherwise(), bb) } else { (bb, targets.otherwise()) }; CharonSwitchTargets::If(BlockId::from_usize(then_bb), BlockId::from_usize(else_bb)) } else { - let CharonTy::Literal(LiteralTy::Integer(int_ty)) = charon_ty else { + let CharonTyKind::Literal(LiteralTy::Integer(int_ty)) = charon_ty.kind() else { panic!("Expected integer type for switch discriminant"); }; let branches = targets @@ -731,7 +745,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }) .collect(); let otherwise = BlockId::from_usize(targets.otherwise()); - CharonSwitchTargets::SwitchInt(int_ty, branches, otherwise) + CharonSwitchTargets::SwitchInt(*int_ty, branches, otherwise) }; (discr, switch_targets) }