diff --git a/charon/Cargo.lock b/charon/Cargo.lock index bdf1d80f..29dd7f47 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -167,6 +167,7 @@ dependencies = [ "rustc_version", "serde", "serde_json", + "serde_stacker", "snapbox", "stacker", "take_mut", @@ -994,6 +995,16 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_stacker" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "babfccff5773ff80657f0ecf553c7c516bdc2eb16389c0918b36b73e7015276e" +dependencies = [ + "serde", + "stacker", +] + [[package]] name = "sharded-slab" version = "0.1.7" diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 8b32a203..c12239fc 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -39,7 +39,8 @@ petgraph = "0.6.2" pretty = "0.12" regex = "1.7.1" rustc_version = "0.4" -serde_json = "1.0.91" +serde_json = { version = "1.0.91", features = ["unbounded_depth"] } +serde_stacker = "0.1.11" serde = { version = "1.0.152", features = ["derive"] } stacker = "0.1" take_mut = "0.2.2" diff --git a/charon/Charon.toml b/charon/Charon.toml index c45200ed..6f2e303f 100644 --- a/charon/Charon.toml +++ b/charon/Charon.toml @@ -6,5 +6,4 @@ opaque_modules = [ "ids", "logger", "pretty", - "translate", ] diff --git a/charon/src/ast/assumed.rs b/charon/src/ast/assumed.rs index 33ac7c0e..90015361 100644 --- a/charon/src/ast/assumed.rs +++ b/charon/src/ast/assumed.rs @@ -54,7 +54,7 @@ pub static PTR_NON_NULL_NAME: [&str; 3] = ["core", "ptr", "NonNull"]; /// - some of the ids here are actually traits, that we disambiguate later /// TODO: merge with the other enum? #[derive(Copy, Clone, EnumIsA)] -pub(crate) enum BuiltinFun { +pub enum BuiltinFun { Panic, BoxNew, BoxFree, @@ -69,7 +69,7 @@ pub struct FunInfo { impl BuiltinFun { /// Converts to the ullbc equivalent. Panics if `self` is `Panic` as this should be handled /// separately. - pub(crate) fn to_ullbc_builtin_fun(self) -> ullbc_ast::AssumedFunId { + pub fn to_ullbc_builtin_fun(self) -> ullbc_ast::AssumedFunId { match self { BuiltinFun::BoxNew => ullbc_ast::AssumedFunId::BoxNew, BuiltinFun::BoxFree => ullbc_ast::AssumedFunId::BoxFree, @@ -78,7 +78,7 @@ impl BuiltinFun { } /// Parse a name to recognize built-in functions. - pub(crate) fn parse_name(name: &Name) -> Option { + pub fn parse_name(name: &Name) -> Option { if PANIC_NAMES.iter().any(|panic| name.equals_ref_name(panic)) { Some(BuiltinFun::Panic) } else if name.equals_ref_name(&["alloc", "alloc", "box_free"]) { @@ -125,7 +125,7 @@ impl BuiltinFun { } /// See the comments for [type_to_used_params] - pub(crate) fn to_fun_info(self) -> Option { + pub fn to_fun_info(self) -> Option { match self { BuiltinFun::Panic => None, BuiltinFun::BoxNew => None, diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index c36462d3..8649ed92 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -2,7 +2,6 @@ use crate::gast::{FunDeclId, TraitItemName}; use crate::types::*; -pub use crate::values::VarId; use crate::values::*; use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index feb24bff..6690ec1e 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -1,5 +1,6 @@ //! This file groups everything which is linked to implementations about [crate::expressions] use crate::expressions::*; +use crate::values::*; use std::vec::Vec; impl Place { diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index f35b06b9..0662149e 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -1,29 +1,25 @@ //! Definitions common to [crate::ullbc_ast] and [crate::llbc_ast] -pub use crate::expressions::*; -pub use crate::gast_utils::*; +pub use super::gast_utils::*; +use crate::expressions::*; use crate::generate_index_type; use crate::ids::Vector; use crate::llbc_ast; use crate::meta::{ItemMeta, Span}; use crate::names::Name; -pub use crate::types::GlobalDeclId; -pub use crate::types::TraitClauseId; use crate::types::*; -pub use crate::types::{ - GenericArgs, GenericParams, TraitDeclId, TraitImplId, TraitInstanceId, TraitRef, -}; use crate::ullbc_ast; +use crate::values::*; use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use macros::EnumIsA; use macros::EnumToGetters; +use rustc_span::def_id::{CrateNum, DefId, DefIndex}; use serde::{Deserialize, Serialize}; generate_index_type!(FunDeclId, "Fun"); generate_index_type!(BodyId, "Body"); /// For use when deserializing. -fn dummy_def_id() -> rustc_hir::def_id::DefId { - use rustc_hir::def_id::*; +fn dummy_def_id() -> DefId { DefId { krate: CrateNum::MAX, index: DefIndex::MAX, @@ -149,7 +145,7 @@ pub struct FunDecl { #[serde(skip)] #[drive(skip)] #[serde(default = "dummy_def_id")] - pub rust_id: rustc_hir::def_id::DefId, + pub rust_id: DefId, /// The meta data associated with the declaration. pub item_meta: ItemMeta, /// The signature contains the inputs/output types *with* non-erased regions. @@ -171,7 +167,7 @@ pub struct GlobalDecl { #[serde(skip)] #[drive(skip)] #[serde(default = "dummy_def_id")] - pub rust_id: rustc_hir::def_id::DefId, + pub rust_id: DefId, /// The meta data associated with the declaration. pub item_meta: ItemMeta, pub generics: GenericParams, diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs index 7bbbe2a4..8d6bdaad 100644 --- a/charon/src/ast/gast_utils.rs +++ b/charon/src/ast/gast_utils.rs @@ -1,9 +1,8 @@ //! Implementations for [crate::gast] -use crate::gast::*; +use crate::ast::*; use crate::ids::Vector; use crate::llbc_ast; -use crate::types::*; use crate::ullbc_ast; /// Makes a lambda that generates a new variable id, pushes a new variable in @@ -19,7 +18,7 @@ pub fn make_locals_generator(locals: &mut Vector) -> impl FnMut(Ty) } impl FunIdOrTraitMethodRef { - pub(crate) fn mk_assumed(aid: AssumedFunId) -> Self { + pub fn mk_assumed(aid: AssumedFunId) -> Self { Self::Fun(FunId::Assumed(aid)) } } diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs new file mode 100644 index 00000000..dae46473 --- /dev/null +++ b/charon/src/ast/krate.rs @@ -0,0 +1,172 @@ +use crate::formatter::{FmtCtx, Formatter, IntoFormatter}; +use crate::gast::*; +use crate::ids::{Generator, Vector}; +use crate::meta::{FileId, FileName, LocalFileId, VirtualFileId}; +use crate::reorder_decls::DeclarationsGroups; +use crate::types::*; +use derive_visitor::{Drive, DriveMut}; +use linked_hash_set::LinkedHashSet; +use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; +use rustc_span::def_id::DefId; +use serde::{Deserialize, Serialize}; +use std::cmp::{Ord, PartialOrd}; +use std::collections::HashMap; +use std::fmt; + +/// The id of a translated item. +#[derive( + Copy, + Clone, + Debug, + PartialOrd, + Ord, + PartialEq, + Eq, + Hash, + EnumIsA, + EnumAsGetters, + VariantName, + VariantIndexArity, + Serialize, + Deserialize, + Drive, + DriveMut, +)] +#[charon::rename("AnyDeclId")] +#[charon::variants_prefix("Id")] +pub enum AnyTransId { + Type(TypeDeclId), + Fun(FunDeclId), + Global(GlobalDeclId), + TraitDecl(TraitDeclId), + TraitImpl(TraitImplId), +} + +/// Implement `TryFrom` and `From` to convert between an enum and its variants. +macro_rules! wrap_unwrap_enum { + ($enum:ident::$variant:ident($variant_ty:ident)) => { + impl TryFrom<$enum> for $variant_ty { + type Error = (); + fn try_from(x: $enum) -> Result { + match x { + $enum::$variant(x) => Ok(x), + _ => Err(()), + } + } + } + + impl From<$variant_ty> for $enum { + fn from(x: $variant_ty) -> Self { + $enum::$variant(x) + } + } + }; +} + +wrap_unwrap_enum!(AnyTransId::Fun(FunDeclId)); +wrap_unwrap_enum!(AnyTransId::Global(GlobalDeclId)); +wrap_unwrap_enum!(AnyTransId::Type(TypeDeclId)); +wrap_unwrap_enum!(AnyTransId::TraitDecl(TraitDeclId)); +wrap_unwrap_enum!(AnyTransId::TraitImpl(TraitImplId)); + +/// A translated item. +#[derive(Debug, Clone, Copy, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)] +pub enum AnyTransItem<'ctx> { + Type(&'ctx TypeDecl), + Fun(&'ctx FunDecl), + Global(&'ctx GlobalDecl), + TraitDecl(&'ctx TraitDecl), + TraitImpl(&'ctx TraitImpl), +} + +/// The data of a translated crate. +#[derive(Default)] +pub struct TranslatedCrate { + /// The name of the crate. + pub crate_name: String, + + /// File names to ids and vice-versa + pub file_to_id: HashMap, + pub id_to_file: HashMap, + pub real_file_counter: Generator, + pub virtual_file_counter: Generator, + + /// All the ids, in the order in which we encountered them + pub all_ids: LinkedHashSet, + /// The map from rustc id to translated id. + pub id_map: HashMap, + /// The reverse map of ids. + pub reverse_id_map: HashMap, + + /// The translated type definitions + pub type_decls: Vector, + /// The translated function definitions + pub fun_decls: Vector, + /// The translated global definitions + pub global_decls: Vector, + /// The bodies of functions and constants + pub bodies: Vector, + /// The translated trait declarations + pub trait_decls: Vector, + /// The translated trait declarations + pub trait_impls: Vector, + /// The re-ordered groups of declarations, initialized as empty. + pub ordered_decls: Option, +} + +impl TranslatedCrate { + pub fn get_item(&self, trans_id: AnyTransId) -> Option> { + match trans_id { + AnyTransId::Type(id) => self.type_decls.get(id).map(AnyTransItem::Type), + AnyTransId::Fun(id) => self.fun_decls.get(id).map(AnyTransItem::Fun), + AnyTransId::Global(id) => self.global_decls.get(id).map(AnyTransItem::Global), + AnyTransId::TraitDecl(id) => self.trait_decls.get(id).map(AnyTransItem::TraitDecl), + AnyTransId::TraitImpl(id) => self.trait_impls.get(id).map(AnyTransItem::TraitImpl), + } + } +} + +impl fmt::Display for TranslatedCrate { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + let fmt: FmtCtx = self.into_fmt(); + match &self.ordered_decls { + None => { + // We do simple: types, globals, traits, functions + for d in &self.type_decls { + writeln!(f, "{}\n", fmt.format_object(d))? + } + for d in &self.global_decls { + writeln!(f, "{}\n", fmt.format_object(d))? + } + for d in &self.trait_decls { + writeln!(f, "{}\n", fmt.format_object(d))? + } + for d in &self.trait_impls { + writeln!(f, "{}\n", fmt.format_object(d))? + } + for d in &self.fun_decls { + writeln!(f, "{}\n", fmt.format_object(d))? + } + } + Some(ordered_decls) => { + for gr in ordered_decls { + for id in gr.get_ids() { + writeln!(f, "{}\n", fmt.format_decl_id(id))? + } + } + } + } + fmt::Result::Ok(()) + } +} + +impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate { + type C = FmtCtx<'a>; + + fn into_fmt(self) -> Self::C { + FmtCtx { + translated: Some(self), + ..Default::default() + } + } +} diff --git a/charon/src/ast/llbc_ast.rs b/charon/src/ast/llbc_ast.rs index b89c6103..10a08884 100644 --- a/charon/src/ast/llbc_ast.rs +++ b/charon/src/ast/llbc_ast.rs @@ -6,12 +6,8 @@ //! Also note that we completely break the definitions Statement and Terminator //! from MIR to use Statement only. -pub use crate::gast::*; -pub use crate::llbc_ast_utils::*; -use crate::meta::Span; -use crate::types::*; -pub use crate::ullbc_ast::{Call, FunDeclId, GlobalDeclId, Var}; -use crate::values::*; +pub use super::llbc_ast_utils::*; +pub use crate::ast::*; use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; diff --git a/charon/src/ast/meta.rs b/charon/src/ast/meta.rs index 94e5e7f8..4e931397 100644 --- a/charon/src/ast/meta.rs +++ b/charon/src/ast/meta.rs @@ -1,11 +1,11 @@ //! Meta-information about programs (spans, etc.). -pub use crate::meta_utils::*; +pub use super::meta_utils::*; use crate::names::Name; use derive_visitor::{Drive, DriveMut}; -use hax_frontend_exporter::PathBuf; use macros::{EnumAsGetters, EnumIsA, EnumToGetters}; use serde::{Deserialize, Serialize}; +use std::path::PathBuf; generate_index_type!(LocalFileId); generate_index_type!(VirtualFileId); diff --git a/charon/src/ast/meta_utils.rs b/charon/src/ast/meta_utils.rs index eaba721e..a5eed59b 100644 --- a/charon/src/ast/meta_utils.rs +++ b/charon/src/ast/meta_utils.rs @@ -1,22 +1,9 @@ //! This file groups everything which is linked to implementations about [crate::meta] use crate::meta::*; use crate::names::{Disambiguator, Name, PathElem}; -use hax_frontend_exporter as hax; -use rustc_ast::{AttrArgs, NormalAttr}; -use rustc_hir::def_id::DefId; -use rustc_middle::ty::TyCtxt; use rustc_span::source_map::SourceMap; use std::cmp::Ordering; use std::iter::Iterator; -use std::path::Component; - -/// Retrieve the Rust span from a def id. -/// -/// Rem.: we use [TyCtxt::def_span], not [TyCtxt::def_ident_span] to retrieve -/// the span. -pub fn get_rspan_from_def_id(ctx: TyCtxt, def_id: DefId) -> rustc_span::Span { - ctx.def_span(def_id) -} impl Loc { fn min(l0: &Loc, l1: &Loc) -> Loc { @@ -84,56 +71,6 @@ pub fn combine_span_iter<'a, T: Iterator>(mut ms: T) -> Span { mc } -pub fn convert_filename(name: &hax::FileName) -> FileName { - match name { - hax::FileName::Real(name) => { - use hax::RealFileName; - match name { - RealFileName::LocalPath(path) => FileName::Local(path.clone()), - RealFileName::Remapped { virtual_name, .. } => { - // We use the virtual name because it is always available. - // That name normally starts with `/rustc//`. For our purposes we hide - // the hash. - let mut components_iter = virtual_name.components(); - if let Some( - [Component::RootDir, Component::Normal(rustc), Component::Normal(hash)], - ) = components_iter.by_ref().array_chunks().next() - && rustc.to_str() == Some("rustc") - && hash.len() == 40 - { - let path_without_hash = [Component::RootDir, Component::Normal(rustc)] - .into_iter() - .chain(components_iter) - .collect(); - FileName::Virtual(path_without_hash) - } else { - FileName::Virtual(virtual_name.clone()) - } - } - } - } - hax::FileName::QuoteExpansion(_) - | hax::FileName::Anon(_) - | hax::FileName::MacroExpansion(_) - | hax::FileName::ProcMacroSourceCode(_) - | hax::FileName::CliCrateAttr(_) - | hax::FileName::Custom(_) - | hax::FileName::DocTest(..) - | hax::FileName::InlineAsm(_) => { - // We use the debug formatter to generate a filename. - // This is not ideal, but filenames are for debugging anyway. - FileName::NotReal(format!("{name:?}")) - } - } -} - -pub fn convert_loc(loc: hax::Loc) -> Loc { - Loc { - line: loc.line, - col: loc.col, - } -} - // TODO: remove? pub fn span_to_string(source_map: &SourceMap, span: rustc_span::Span) -> String { // Convert the span to lines @@ -183,36 +120,14 @@ pub fn span_to_string(source_map: &SourceMap, span: rustc_span::Span) -> String } impl Attribute { - pub(crate) fn parse(normal_attr: &NormalAttr, span: rustc_span::Span) -> Result { - // We use `pprust` to render the attribute somewhat like it is written in the source. - // WARNING: this can change whitespace, and sometimes even adds newlines. Maybe we - // should use spans and SourceMap info instead. - use rustc_ast_pretty::pprust::PrintState; - - // If the attribute path has two components, the first of which is `charon` or `aeneas`, we - // try to parse it. Otherwise we return `Unknown`. - let attr_name = if let [path_start, attr_name] = normal_attr.item.path.segments.as_slice() - && let path_start = path_start.ident.as_str() - && (path_start == "charon" || path_start == "aeneas") - { - attr_name.ident.as_str() - } else { - let full_attr = rustc_ast_pretty::pprust::State::to_string(|s| { - s.print_attr_item(&normal_attr.item, span) - }); - return Ok(Self::Unknown(full_attr)); - }; - - let args = match &normal_attr.item.args { - AttrArgs::Empty => None, - AttrArgs::Delimited(args) => Some(rustc_ast_pretty::pprust::State::to_string(|s| { - s.print_tts(&args.tokens, false) - })), - AttrArgs::Eq(..) => unimplemented!("`#[charon::foo = val]` syntax is unsupported"), - }; - match attr_name { + /// Parse a `charon::*` or `aeneas::*` attribute. + pub fn parse_special_attr( + attr_name: &str, + args: Option, + ) -> Result, String> { + let parsed = match attr_name { // `#[charon::opaque]` - "opaque" if args.is_none() => Ok(Self::Opaque), + "opaque" if args.is_none() => Self::Opaque, // `#[charon::rename("new_name")]` "rename" if let Some(attr) = args => { let Some(attr) = attr @@ -237,7 +152,7 @@ impl Attribute { )); } - Ok(Self::Rename(attr.to_string())) + Self::Rename(attr.to_string()) } // `#[charon::variants_prefix("T")]` "variants_prefix" if let Some(attr) = args => { @@ -250,7 +165,7 @@ impl Attribute { )); }; - Ok(Self::VariantsPrefix(attr.to_string())) + Self::VariantsPrefix(attr.to_string()) } // `#[charon::variants_suffix("T")]` "variants_suffix" if let Some(attr) = args => { @@ -263,20 +178,16 @@ impl Attribute { )); }; - Ok(Self::VariantsSuffix(attr.to_string())) - } - _ => { - let full_attr = rustc_ast_pretty::pprust::State::to_string(|s| { - s.print_attr_item(&normal_attr.item, span) - }); - Err(format!("Unrecognized attribute: `{full_attr}`")) + Self::VariantsSuffix(attr.to_string()) } - } + _ => return Ok(None), + }; + Ok(Some(parsed)) } } impl ItemOpacity { - pub(crate) fn with_content_visibility(self, contents_are_public: bool) -> Self { + pub fn with_content_visibility(self, contents_are_public: bool) -> Self { use ItemOpacity::*; match self { Transparent => Transparent, @@ -286,7 +197,7 @@ impl ItemOpacity { } } - pub(crate) fn with_private_contents(self) -> Self { + pub fn with_private_contents(self) -> Self { self.with_content_visibility(false) } } diff --git a/charon/src/ast/mod.rs b/charon/src/ast/mod.rs index 36fd6a6d..bb6c6d9c 100644 --- a/charon/src/ast/mod.rs +++ b/charon/src/ast/mod.rs @@ -6,6 +6,7 @@ pub mod expressions_utils; pub mod gast; #[charon::opaque] pub mod gast_utils; +pub mod krate; pub mod llbc_ast; #[charon::opaque] pub mod llbc_ast_utils; @@ -24,3 +25,13 @@ pub mod ullbc_ast_utils; pub mod values; #[charon::opaque] pub mod values_utils; + +// Re-export everything except llbc/ullbc, for convenience. +pub use assumed::*; +pub use expressions::*; +pub use gast::*; +pub use krate::*; +pub use meta::*; +pub use names::*; +pub use types::*; +pub use values::*; diff --git a/charon/src/ast/names_utils.rs b/charon/src/ast/names_utils.rs index 3d9697e9..43f50de6 100644 --- a/charon/src/ast/names_utils.rs +++ b/charon/src/ast/names_utils.rs @@ -2,14 +2,7 @@ //! //! For now, we have one function per object kind (type, trait, function, //! module): many of them could be factorized (will do). -use crate::common::*; use crate::names::*; -use crate::translate_ctx::*; -use crate::types::PredicateOrigin; -use hax_frontend_exporter as hax; -use hax_frontend_exporter::SInto; -use rustc_hir::{Item, ItemKind}; -use rustc_span::def_id::DefId; use std::collections::HashSet; impl PathElem { @@ -89,243 +82,3 @@ impl Name { } } } - -impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { - /// Retrieve an item name from a [DefId]. - pub fn def_id_to_name(&mut self, def_id: DefId) -> Result { - trace!("{:?}", def_id); - let tcx = self.tcx; - let span = tcx.def_span(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 - // different names depending on the def id on which it is called, even though - // those def ids might actually identify the same definition. - // For instance: `std::boxed::Box` and `alloc::boxed::Box` are actually - // the same (the first one is a reexport). - // This is why we implement a custom function to retrieve the original name - // (though this makes us loose aliases - we may want to investigate this - // issue in the future). - - // We lookup the path associated to an id, and convert it to a name. - // Paths very precisely identify where an item is. There are important - // subcases, like the items in an `Impl` block: - // ``` - // impl List { - // fn new() ... - // } - // ``` - // - // One issue here is that "List" *doesn't appear* in the path, which would - // look like the following: - // - // `TypeNS("Crate") :: Impl :: ValueNs("new")` - // ^^^ - // This is where "List" should be - // - // For this reason, whenever we find an `Impl` path element, we actually - // lookup the type of the sub-path, from which we can derive a name. - // - // Besides, as there may be several "impl" blocks for one type, each impl - // block is identified by a unique number (rustc calls this a - // "disambiguator"), which we grab. - // - // Example: - // ======== - // For instance, if we write the following code in crate `test` and module - // `bla`: - // ``` - // impl Foo { - // fn foo() { ... } - // } - // - // impl Foo { - // fn bar() { ... } - // } - // ``` - // - // The names we will generate for `foo` and `bar` are: - // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(0), Ident("foo")]` - // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(1), Ident("bar")]` - let mut found_crate_name = false; - let mut name: Vec = Vec::new(); - - let def_path = tcx.def_path(def_id); - let crate_name = tcx.crate_name(def_path.krate).to_string(); - - let parents: Vec = { - let mut parents = vec![def_id]; - let mut cur_id = def_id; - while let Some(parent) = tcx.opt_parent(cur_id) { - parents.push(parent); - cur_id = parent; - } - parents.into_iter().rev().collect() - }; - - // Rk.: below we try to be as tight as possible with regards to sanity - // checks, to make sure we understand what happens with def paths, and - // fail whenever we get something which is even slightly outside what - // we expect. - for cur_id in parents { - let data = tcx.def_key(cur_id).disambiguated_data; - // Match over the key data - let disambiguator = Disambiguator::new(data.disambiguator as usize); - use rustc_hir::definitions::DefPathData; - match &data.data { - DefPathData::TypeNs(symbol) => { - assert!(data.disambiguator == 0); // Sanity check - name.push(PathElem::Ident(symbol.to_string(), disambiguator)); - } - DefPathData::ValueNs(symbol) => { - // I think `disambiguator != 0` only with names introduced by macros (though - // not sure). - name.push(PathElem::Ident(symbol.to_string(), disambiguator)); - } - DefPathData::CrateRoot => { - // Sanity check - assert!(data.disambiguator == 0); - - // This should be the beginning of the path - assert!(name.is_empty()); - found_crate_name = true; - name.push(PathElem::Ident(crate_name.clone(), disambiguator)); - } - DefPathData::Impl => { - // We need to convert the type, which may contain quantified - // substs and bounds. In order to properly do so, we introduce - // a body translation context. - let id = cur_id; - - // Translate from hax to LLBC - let mut bt_ctx = BodyTransCtx::new(id, self); - - // Translate to hax types - // TODO: use the bounds - let _bounds: Vec = bt_ctx - .t_ctx - .tcx - .predicates_of(id) - .predicates - .iter() - .map(|(x, _)| x.sinto(&bt_ctx.hax_state)) - .collect(); - let ty = tcx - .type_of(id) - .instantiate_identity() - .sinto(&bt_ctx.hax_state); - - bt_ctx.translate_generic_params(id)?; - bt_ctx.translate_predicates_of(None, id, PredicateOrigin::WhereClauseOnImpl)?; - let erase_regions = false; - // Two cases, depending on whether the impl block is - // a "regular" impl block (`impl Foo { ... }`) or a trait - // implementation (`impl Bar for Foo { ... }`). - let kind = match bt_ctx.t_ctx.tcx.impl_trait_ref(id) { - None => { - // Inherent impl ("regular" impl) - let ty = bt_ctx.translate_ty(span, erase_regions, &ty)?; - ImplElemKind::Ty(ty) - } - Some(trait_ref) => { - // Trait implementation - let trait_ref = trait_ref.sinto(&bt_ctx.hax_state); - let erase_regions = false; - let trait_ref = - bt_ctx.translate_trait_decl_ref(span, erase_regions, &trait_ref)?; - match trait_ref { - None => error_or_panic!(self, span, "The trait reference was ignored while we need it to compute the name"), - Some(trait_ref) => { - ImplElemKind::Trait(trait_ref) - } - } - } - }; - - name.push(PathElem::Impl(ImplElem { - disambiguator, - generics: bt_ctx.get_generics(), - kind, - })); - } - DefPathData::OpaqueTy => { - // TODO: do nothing for now - } - DefPathData::MacroNs(symbol) => { - assert!(data.disambiguator == 0); // Sanity check - - // There may be namespace collisions between, say, function - // names and macros (not sure). However, this isn't much - // of an issue here, because for now we don't expose macros - // in the AST, and only use macro names in [register], for - // instance to filter opaque modules. - name.push(PathElem::Ident(symbol.to_string(), disambiguator)); - } - DefPathData::Closure => { - // TODO: this is not very satisfactory, but on the other hand - // we should be able to extract closures in local let-bindings - // (i.e., we shouldn't have to introduce top-level let-bindings). - name.push(PathElem::Ident("closure".to_string(), disambiguator)) - } - DefPathData::ForeignMod => { - // Do nothing, functions in `extern` blocks are in the same namespace as the - // block. - } - _ => { - error!("Unexpected DefPathData: {:?}", data); - unreachable!("Unexpected DefPathData: {:?}", data); - } - } - } - - // We always add the crate name - if !found_crate_name { - name.push(PathElem::Ident(crate_name, Disambiguator::new(0))); - } - - trace!("{:?}", name); - Ok(Name { name }) - } - - /// Returns an optional name for an HIR item. - /// - /// If the option is `None`, it means the item is to be ignored (example: it - /// is a `use` item). - /// - /// Rk.: this function is only used by [crate::register], and implemented with this - /// context in mind. - pub fn hir_item_to_name(&mut self, item: &Item) -> Result, Error> { - let def_id = item.owner_id.to_def_id(); - - let name = match &item.kind { - ItemKind::OpaqueTy(..) => unimplemented!(), - ItemKind::Union(..) => unimplemented!(), - ItemKind::ExternCrate(..) => { - // We ignore this - - // TODO: investigate when extern crates appear, and why - None - } - ItemKind::Use(..) => None, - ItemKind::TyAlias(..) - | ItemKind::Enum(..) - | ItemKind::Struct(..) - | ItemKind::Fn(..) - | ItemKind::Impl(..) - | ItemKind::Mod(..) - | ItemKind::ForeignMod { .. } - | ItemKind::Const(..) - | ItemKind::Static(..) - | ItemKind::Macro(..) - | ItemKind::Trait(..) => Some(self.def_id_to_name(def_id)?), - _ => { - unimplemented!("{:?}", item.kind); - } - }; - Ok(name) - } - - pub fn hax_def_id_to_name(&mut self, def_id: &hax::DefId) -> Result { - // We have to create a hax state, which is annoying... - self.def_id_to_name(DefId::from(def_id)) - } -} diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 4f3171d6..6e9592fc 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -1,8 +1,6 @@ -pub use crate::gast::{FunDeclId, TraitItemName}; +pub use super::types_utils::*; +use crate::ast::{AttrInfo, ItemMeta, Literal, ScalarValue, Span, TraitItemName}; use crate::ids::Vector; -use crate::meta::{AttrInfo, ItemMeta, Span}; -pub use crate::types_utils::*; -use crate::values::{Literal, ScalarValue}; use derivative::Derivative; use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut}; use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName}; diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index a11ff0de..c1448a25 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -1,7 +1,6 @@ //! This file groups everything which is linked to implementations about [crate::types] use crate::ids::Vector; use crate::types::*; -use hax_frontend_exporter as hax; use std::collections::HashMap; use std::iter::Iterator; @@ -149,30 +148,6 @@ impl TypeDecl { } impl IntegerTy { - pub fn rust_int_ty_to_integer_ty(ty: hax::IntTy) -> IntegerTy { - use hax::IntTy::*; - match ty { - Isize => IntegerTy::Isize, - I8 => IntegerTy::I8, - I16 => IntegerTy::I16, - I32 => IntegerTy::I32, - I64 => IntegerTy::I64, - I128 => IntegerTy::I128, - } - } - - pub fn rust_uint_ty_to_integer_ty(ty: hax::UintTy) -> IntegerTy { - use hax::UintTy::*; - match ty { - Usize => IntegerTy::Usize, - U8 => IntegerTy::U8, - U16 => IntegerTy::U16, - U32 => IntegerTy::U32, - U64 => IntegerTy::U64, - U128 => IntegerTy::U128, - } - } - pub fn is_signed(&self) -> bool { matches!( self, @@ -406,11 +381,7 @@ impl TySubst { Ok(()) } - fn unify_args( - &mut self, - src: &crate::gast::GenericArgs, - tgt: &crate::gast::GenericArgs, - ) -> Result<(), ()> { + fn unify_args(&mut self, src: &GenericArgs, tgt: &GenericArgs) -> Result<(), ()> { if !self.ignore_regions { self.unify_regions_lists(&src.regions, &tgt.regions)?; } @@ -425,8 +396,8 @@ impl TySubst { pub fn unify_args_with_fixed( fixed_type_vars: impl std::iter::Iterator, fixed_const_generic_vars: impl std::iter::Iterator, - src: &crate::gast::GenericArgs, - tgt: &crate::gast::GenericArgs, + src: &GenericArgs, + tgt: &GenericArgs, ) -> Result { let mut s = TySubst::new(); for v in fixed_type_vars { diff --git a/charon/src/ast/ullbc_ast.rs b/charon/src/ast/ullbc_ast.rs index 1fc63312..13644d09 100644 --- a/charon/src/ast/ullbc_ast.rs +++ b/charon/src/ast/ullbc_ast.rs @@ -1,12 +1,8 @@ //! "Unstructured LLBC" ast (ULLBC). This is LLBC before the control-flow //! reconstruction. In effect, this is a cleaned up version of MIR. -pub use crate::gast::*; +pub use super::ullbc_ast_utils::*; +pub use crate::ast::*; use crate::ids::Vector; -use crate::meta::Span; -pub use crate::types::GlobalDeclId; -use crate::types::*; -pub use crate::ullbc_ast_utils::*; -use crate::values::*; use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; diff --git a/charon/src/ast/values.rs b/charon/src/ast/values.rs index 0cf28671..9ed02d4d 100644 --- a/charon/src/ast/values.rs +++ b/charon/src/ast/values.rs @@ -1,6 +1,5 @@ //! Contains definitions for variables and constant values. -pub use crate::values_utils::*; use core::hash::Hash; use derive_visitor::{Drive, DriveMut}; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index 2c25569d..a105966b 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -1,9 +1,9 @@ -use crate::cli_options; +use crate::translate::translate_crate_to_ullbc; use charon_lib::export; -use charon_lib::get_mir::MirLevel; +use charon_lib::options; +use charon_lib::options::MirLevel; use charon_lib::reorder_decls::compute_reordered_decls; use charon_lib::transform::{LLBC_PASSES, ULLBC_PASSES}; -use charon_lib::translate_crate_to_ullbc; use charon_lib::ullbc_to_llbc; use regex::Regex; use rustc_driver::{Callbacks, Compilation}; @@ -15,7 +15,7 @@ use std::panic::{self, AssertUnwindSafe}; /// The callbacks for Charon pub struct CharonCallbacks { - pub options: cli_options::CliOpts, + pub options: options::CliOpts, /// This is to be filled during the extraction pub crate_data: Option, pub error_count: usize, @@ -41,7 +41,7 @@ impl fmt::Display for CharonFailure { } impl CharonCallbacks { - pub fn new(options: cli_options::CliOpts) -> Self { + pub fn new(options: options::CliOpts) -> Self { Self { options, crate_data: None, diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index 813a6402..f9e4a1e3 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -1,24 +1,39 @@ //! The Charon driver, which calls Rustc with callbacks to compile some Rust //! crate to LLBC. #![feature(rustc_private)] - +#![expect(incomplete_features)] +#![feature(box_patterns)] +#![feature(deref_patterns)] +#![feature(iter_array_chunks)] +#![feature(iterator_try_collect)] +#![feature(let_chains)] +#![feature(lint_reasons)] + +extern crate rustc_ast; +extern crate rustc_ast_pretty; +extern crate rustc_attr; extern crate rustc_driver; +extern crate rustc_error_messages; +extern crate rustc_errors; extern crate rustc_hir; +extern crate rustc_index; extern crate rustc_interface; extern crate rustc_middle; extern crate rustc_span; +extern crate rustc_target; #[macro_use] extern crate charon_lib; mod driver; +mod translate; use crate::driver::{ arg_values, get_args_crate_index, get_args_source_index, CharonCallbacks, CharonFailure, RunCompilerNormallyCallbacks, }; -use charon_lib::cli_options; use charon_lib::logger; +use charon_lib::options; use charon_lib::trace; fn main() { @@ -61,7 +76,7 @@ fn main() { // Retrieve the Charon options by deserializing them from the environment variable // (cargo-charon serialized the arguments and stored them in a specific environment // variable before calling cargo with RUSTC_WORKSPACE_WRAPPER=charon-driver). - let options: cli_options::CliOpts = match std::env::var(cli_options::CHARON_ARGS) { + let options: options::CliOpts = match std::env::var(options::CHARON_ARGS) { Ok(opts) => serde_json::from_str(opts.as_str()).unwrap(), Err(_) => { // Parse any arguments after `--` as charon arguments. @@ -69,7 +84,7 @@ fn main() { use clap::Parser; let mut charon_args = compiler_args.split_off(i); charon_args[0] = origin_args[0].clone(); // Replace `--` with the name of the binary - cli_options::CliOpts::parse_from(charon_args) + options::CliOpts::parse_from(charon_args) } else { Default::default() } @@ -192,24 +207,27 @@ fn main() { if !options.no_serialize { // # Final step: generate the files. - res = res.and_then(|()| { + if res.is_ok() || options.errors_as_warnings { // `crate_data` is set by our callbacks when there is no fatal error. - let crate_data = crate_data.unwrap(); - let dest_file = match options.dest_file.clone() { - Some(f) => f, - None => { - let mut target_filename = options.dest_dir.clone().unwrap_or_default(); - let crate_name = &crate_data.name; - let extension = if options.ullbc { "ullbc" } else { "llbc" }; - target_filename.push(format!("{crate_name}.{extension}")); - target_filename - } - }; - trace!("Target file: {:?}", dest_file); - crate_data - .serialize_to_file(&dest_file) - .map_err(|()| CharonFailure::Serialize) - }); + if let Some(crate_data) = crate_data { + let dest_file = match options.dest_file.clone() { + Some(f) => f, + None => { + let mut target_filename = options.dest_dir.clone().unwrap_or_default(); + let crate_name = &crate_data.name; + let extension = if options.ullbc { "ullbc" } else { "llbc" }; + target_filename.push(format!("{crate_name}.{extension}")); + target_filename + } + }; + trace!("Target file: {:?}", dest_file); + res = res.and( + crate_data + .serialize_to_file(&dest_file) + .map_err(|()| CharonFailure::Serialize), + ); + } + } } match res { @@ -220,6 +238,9 @@ fn main() { log::warn!("{}", msg); } } + Err(err) if errors_as_warnings => { + log::error!("{err}"); + } Err(CharonFailure::Panic) => { // Standard rust panic error code. std::process::exit(101); diff --git a/charon/src/translate/get_mir.rs b/charon/src/bin/charon-driver/translate/get_mir.rs similarity index 83% rename from charon/src/translate/get_mir.rs rename to charon/src/bin/charon-driver/translate/get_mir.rs index 68e67aab..b4bf1ab6 100644 --- a/charon/src/translate/get_mir.rs +++ b/charon/src/bin/charon-driver/translate/get_mir.rs @@ -1,23 +1,11 @@ //! Various utilities to load MIR. //! Allow to easily load the MIR code generated by a specific pass. +use crate::options::MirLevel; use rustc_hir::def_id::DefId; use rustc_middle::mir::Body; use rustc_middle::ty::TyCtxt; -/// TODO: maybe we should always target MIR Built, this would make things -/// simpler. In particular, the MIR optimized is very low level and -/// reveals too many types and data-structures that we don't want to manipulate. -#[derive(Clone, Copy, PartialEq, Eq)] -pub enum MirLevel { - /// Original MIR, directly translated from HIR. - Built, - /// Not sure what this is. Not well tested. - Promoted, - /// MIR after optimization passes. The last one before codegen. - Optimized, -} - /// Indicates if the constants should be extracted in their own identifier, /// or if they must be evaluated to a constant value, depending on the /// MIR level which we extract. diff --git a/charon/src/translate/mod.rs b/charon/src/bin/charon-driver/translate/mod.rs similarity index 100% rename from charon/src/translate/mod.rs rename to charon/src/bin/charon-driver/translate/mod.rs diff --git a/charon/src/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs similarity index 98% rename from charon/src/translate/translate_constants.rs rename to charon/src/bin/charon-driver/translate/translate_constants.rs index 08cc28be..98de29d5 100644 --- a/charon/src/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -1,9 +1,7 @@ //! Functions to translate constants to LLBC. -use crate::common::*; -use crate::gast::*; -use crate::translate_ctx::*; -use crate::types::*; -use crate::values::*; +use super::translate_ctx::*; +use charon_lib::ast::*; +use charon_lib::common::*; use hax_frontend_exporter as hax; use rustc_hir::def_id::DefId; @@ -146,7 +144,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { generics_impls: trait_refs, method_impl: trait_info, } => { - use crate::translate_functions_to_ullbc::SubstFunIdOrPanic; + use super::translate_functions_to_ullbc::SubstFunIdOrPanic; let erase_regions = true; // TODO: not sure let fn_id = self.translate_fun_decl_id_with_args( span, diff --git a/charon/src/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs similarity index 95% rename from charon/src/translate/translate_crate_to_ullbc.rs rename to charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index 6c5c1a12..1d62ca2a 100644 --- a/charon/src/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -1,8 +1,9 @@ -use crate::cli_options::CliOpts; -use crate::common::*; -use crate::get_mir::{extract_constants_at_top_level, MirLevel}; -use crate::transform::TransformCtx; -use crate::translate_ctx::*; +use super::get_mir::extract_constants_at_top_level; +use super::translate_ctx::*; +use charon_lib::ast::krate::*; +use charon_lib::common::*; +use charon_lib::options::{CliOpts, MirLevel, TransOptions}; +use charon_lib::transform::TransformCtx; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; @@ -345,6 +346,7 @@ pub fn translate<'tcx, 'ctx>( tcx, hax::options::Options { inline_macro_calls: Vec::new(), + // downgrade_errors: options.errors_as_warnings, }, ); let mut ctx = TranslateCtx { @@ -392,11 +394,17 @@ pub fn translate<'tcx, 'ctx>( let hir = tcx.hir(); for item_id in hir.root_module().item_ids { let item_id = item_id.hir_id(); - let rustc_hir::Node::Item(item) = tcx.hir_node(item_id) else { - unreachable!() - }; - // If registration fails we simply skip the item. - let _ = ctx.register_local_hir_item(true, item); + { + let mut ctx = std::panic::AssertUnwindSafe(&mut ctx); + // Stopgap measure because there are still many panics in charon and hax. + // If registration fails we simply skip the item. + let _ = std::panic::catch_unwind(move || { + let rustc_hir::Node::Item(item) = ctx.tcx.hir_node(item_id) else { + unreachable!() + }; + ctx.register_local_hir_item(true, item) + }); + } } trace!( diff --git a/charon/src/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs similarity index 66% rename from charon/src/translate/translate_ctx.rs rename to charon/src/bin/charon-driver/translate/translate_ctx.rs index 0add2b34..2f920b0e 100644 --- a/charon/src/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -1,172 +1,31 @@ //! The translation contexts. -use crate::common::*; -use crate::formatter::{FmtCtx, Formatter, IntoFormatter}; -use crate::gast::*; -use crate::get_mir::MirLevel; -use crate::ids::{Generator, MapGenerator, Vector}; -use crate::meta::{self, AttrInfo, Attribute, ItemMeta, ItemOpacity, RawSpan}; -use crate::meta::{FileId, FileName, InlineAttr, LocalFileId, Span, VirtualFileId}; -use crate::names::Name; -use crate::reorder_decls::DeclarationsGroups; -use crate::translate_predicates::NonLocalTraitClause; -use crate::translate_traits::ClauseTransCtx; -use crate::types::*; -use crate::ullbc_ast as ast; -use crate::values::*; -use derive_visitor::{Drive, DriveMut}; +use super::translate_predicates::NonLocalTraitClause; +use super::translate_traits::ClauseTransCtx; +use charon_lib::ast::*; +use charon_lib::common::*; +use charon_lib::formatter::{FmtCtx, IntoFormatter}; +use charon_lib::ids::{MapGenerator, Vector}; +use charon_lib::options::TransOptions; +use charon_lib::ullbc_ast as ast; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; -use linked_hash_set::LinkedHashSet; -use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; +use macros::VariantIndexArity; +use rustc_ast::AttrArgs; +use rustc_ast_pretty::pprust; use rustc_error_messages::MultiSpan; -use rustc_errors::DiagCtxtHandle; use rustc_hir::def_id::DefId; use rustc_hir::Node as HirNode; +use rustc_hir::{Item, ItemKind}; use rustc_middle::ty::TyCtxt; -use serde::{Deserialize, Serialize}; use std::cmp::{Ord, PartialOrd}; -use std::collections::{BTreeMap, HashMap, HashSet, VecDeque}; +use std::collections::{BTreeMap, VecDeque}; use std::fmt; +use std::path::Component; -macro_rules! register_error_or_panic { - ($ctx:expr, $span: expr, $msg: expr) => {{ - $ctx.span_err($span, &$msg); - if !$ctx.continue_on_failure() { - panic!("{}", $msg); - } - }}; -} -pub(crate) use register_error_or_panic; - -/// Macro to either panic or return on error, depending on the CLI options -macro_rules! error_or_panic { - ($ctx:expr, $span:expr, $msg:expr) => {{ - $crate::translate_ctx::register_error_or_panic!($ctx, $span, $msg); - let e = crate::common::Error { - span: $span, - msg: $msg.to_string(), - }; - return Err(e); - }}; -} -pub(crate) use error_or_panic; - -/// Custom assert to either panic or return an error -macro_rules! error_assert { - ($ctx:expr, $span: expr, $b: expr) => { - if !$b { - let msg = format!("assertion failure: {:?}", stringify!($b)); - $crate::translate_ctx::error_or_panic!($ctx, $span, msg); - } - }; - ($ctx:expr, $span: expr, $b: expr, $msg: expr) => { - if !$b { - $crate::translate_ctx::error_or_panic!($ctx, $span, $msg); - } - }; -} -pub(crate) use error_assert; - -/// We use this to save the origin of an id. This is useful for the external -/// dependencies, especially if some external dependencies don't extract: -/// we use this information to tell the user what is the code which -/// (transitively) lead to the extraction of those problematic dependencies. -#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] -pub struct DepSource { - pub src_id: DefId, - pub span: rustc_span::Span, -} - -impl DepSource { - /// Value with which we order `DepSource`s. - fn sort_key(&self) -> impl Ord { - (self.src_id.index, self.src_id.krate) - } -} - -/// Manual impls because `DefId` is not orderable. -impl PartialOrd for DepSource { - fn partial_cmp(&self, other: &Self) -> Option { - Some(self.cmp(other)) - } -} -impl Ord for DepSource { - fn cmp(&self, other: &Self) -> std::cmp::Ordering { - self.sort_key().cmp(&other.sort_key()) - } -} - -impl DepSource { - pub(crate) fn make(src_id: DefId, span: rustc_span::Span) -> Option { - Some(DepSource { src_id, span }) - } -} - -/// The id of a translated item. -#[derive( - Copy, - Clone, - Debug, - PartialOrd, - Ord, - PartialEq, - Eq, - Hash, - EnumIsA, - EnumAsGetters, - VariantName, - VariantIndexArity, - Serialize, - Deserialize, - Drive, - DriveMut, -)] -#[charon::rename("AnyDeclId")] -#[charon::variants_prefix("Id")] -pub enum AnyTransId { - Type(TypeDeclId), - Fun(FunDeclId), - Global(GlobalDeclId), - TraitDecl(TraitDeclId), - TraitImpl(TraitImplId), -} - -/// Implement `TryFrom` and `From` to convert between an enum and its variants. -macro_rules! wrap_unwrap_enum { - ($enum:ident::$variant:ident($variant_ty:ident)) => { - impl TryFrom<$enum> for $variant_ty { - type Error = (); - fn try_from(x: $enum) -> Result { - match x { - $enum::$variant(x) => Ok(x), - _ => Err(()), - } - } - } - - impl From<$variant_ty> for $enum { - fn from(x: $variant_ty) -> Self { - $enum::$variant(x) - } - } - }; -} - -wrap_unwrap_enum!(AnyTransId::Fun(FunDeclId)); -wrap_unwrap_enum!(AnyTransId::Global(GlobalDeclId)); -wrap_unwrap_enum!(AnyTransId::Type(TypeDeclId)); -wrap_unwrap_enum!(AnyTransId::TraitDecl(TraitDeclId)); -wrap_unwrap_enum!(AnyTransId::TraitImpl(TraitImplId)); - -/// A translated item. -#[derive(Debug, Clone, Copy, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)] -pub enum AnyTransItem<'ctx> { - Type(&'ctx TypeDecl), - Fun(&'ctx FunDecl), - Global(&'ctx GlobalDecl), - TraitDecl(&'ctx TraitDecl), - TraitImpl(&'ctx TraitImpl), -} +// Re-export to avoid having to fix imports. +pub(crate) use charon_lib::errors::{ + error_assert, error_or_panic, register_error_or_panic, DepSource, ErrorCtx, +}; /// We use a special type to store the Rust identifiers in the stack, to /// make sure we translate them in a specific order (top-level constants @@ -216,76 +75,6 @@ impl Ord for OrdRustId { } } -/// The options that control translation. -pub struct TransOptions { - /// The level at which to extract the MIR - pub mir_level: MirLevel, - /// Error out if some code ends up being duplicated by the control-flow - /// reconstruction (note that because several patterns in a match may lead - /// to the same branch, it is node always possible not to duplicate code). - pub no_code_duplication: bool, - /// Whether to extract the bodies of foreign methods and structs with private fields. - pub extract_opaque_bodies: bool, - /// Modules to consider opaque. - pub opaque_mods: HashSet, -} - -/// The data of a translated crate. -#[derive(Default)] -pub struct TranslatedCrate { - /// The name of the crate. - pub crate_name: String, - - /// File names to ids and vice-versa - pub file_to_id: HashMap, - pub id_to_file: HashMap, - pub real_file_counter: Generator, - pub virtual_file_counter: Generator, - - /// All the ids, in the order in which we encountered them - pub all_ids: LinkedHashSet, - /// The map from rustc id to translated id. - pub id_map: HashMap, - /// The reverse map of ids. - pub reverse_id_map: HashMap, - - /// The translated type definitions - pub type_decls: Vector, - /// The translated function definitions - pub fun_decls: Vector, - /// The translated global definitions - pub global_decls: Vector, - /// The bodies of functions and constants - pub bodies: Vector, - /// The translated trait declarations - pub trait_decls: Vector, - /// The translated trait declarations - pub trait_impls: Vector, - /// The re-ordered groups of declarations, initialized as empty. - pub ordered_decls: Option, -} - -/// The context for tracking and reporting errors. -pub struct ErrorCtx<'ctx> { - /// If true, do not abort on the first error and attempt to extract as much as possible. - pub continue_on_failure: bool, - /// If true, print the errors as warnings, and do not abort. - pub errors_as_warnings: bool, - - /// The compiler session, used for displaying errors. - pub dcx: DiagCtxtHandle<'ctx>, - /// The ids of the declarations for which extraction we encountered errors. - pub decls_with_errors: HashSet, - /// The ids of the declarations we completely failed to extract and had to ignore. - pub ignored_failed_decls: HashSet, - /// Dependency graph with sources. See [DepSource]. - pub dep_sources: HashMap>, - /// The id of the definition we are exploring, used to track the source of errors. - pub def_id: Option, - /// The number of errors encountered so far. - pub error_count: usize, -} - /// Translation context used while translating the crate data into our representation. pub struct TranslateCtx<'tcx, 'ctx> { /// The Rust compiler type context @@ -396,66 +185,6 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> { pub blocks_stack: VecDeque, } -impl ErrorCtx<'_> { - pub(crate) fn continue_on_failure(&self) -> bool { - self.continue_on_failure - } - pub(crate) fn has_errors(&self) -> bool { - self.error_count > 0 - } - - /// Report an error without registering anything. - pub(crate) fn span_err_no_register>(&self, span: S, msg: &str) { - let msg = msg.to_string(); - if self.errors_as_warnings { - self.dcx.span_warn(span, msg); - } else { - self.dcx.span_err(span, msg); - } - } - - /// Report and register an error. - pub fn span_err>(&mut self, span: S, msg: &str) { - self.span_err_no_register(span, msg); - self.error_count += 1; - if let Some(id) = self.def_id { - let _ = self.decls_with_errors.insert(id); - } - } - - /// Register the fact that `id` is a dependency of `src` (if `src` is not `None`). - pub(crate) fn register_dep_source(&mut self, src: &Option, id: DefId) { - if let Some(src) = src { - if src.src_id != id { - match self.dep_sources.get_mut(&id) { - None => { - let _ = self.dep_sources.insert(id, HashSet::from([*src])); - } - Some(srcs) => { - let _ = srcs.insert(*src); - } - } - } - } - } - - pub(crate) fn ignore_failed_decl(&mut self, id: DefId) { - self.ignored_failed_decls.insert(id); - } -} - -impl TranslatedCrate { - pub fn get_item(&self, trans_id: AnyTransId) -> Option> { - match trans_id { - AnyTransId::Type(id) => self.type_decls.get(id).map(AnyTransItem::Type), - AnyTransId::Fun(id) => self.fun_decls.get(id).map(AnyTransItem::Fun), - AnyTransId::Global(id) => self.global_decls.get(id).map(AnyTransItem::Global), - AnyTransId::TraitDecl(id) => self.trait_decls.get(id).map(AnyTransItem::TraitDecl), - AnyTransId::TraitImpl(id) => self.trait_impls.get(id).map(AnyTransItem::TraitImpl), - } - } -} - impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub fn continue_on_failure(&self) -> bool { self.errors.continue_on_failure() @@ -489,10 +218,248 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } } + /// Retrieve an item name from a [DefId]. + pub fn def_id_to_name(&mut self, def_id: DefId) -> Result { + trace!("{:?}", def_id); + let tcx = self.tcx; + let span = tcx.def_span(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 + // different names depending on the def id on which it is called, even though + // those def ids might actually identify the same definition. + // For instance: `std::boxed::Box` and `alloc::boxed::Box` are actually + // the same (the first one is a reexport). + // This is why we implement a custom function to retrieve the original name + // (though this makes us loose aliases - we may want to investigate this + // issue in the future). + + // We lookup the path associated to an id, and convert it to a name. + // Paths very precisely identify where an item is. There are important + // subcases, like the items in an `Impl` block: + // ``` + // impl List { + // fn new() ... + // } + // ``` + // + // One issue here is that "List" *doesn't appear* in the path, which would + // look like the following: + // + // `TypeNS("Crate") :: Impl :: ValueNs("new")` + // ^^^ + // This is where "List" should be + // + // For this reason, whenever we find an `Impl` path element, we actually + // lookup the type of the sub-path, from which we can derive a name. + // + // Besides, as there may be several "impl" blocks for one type, each impl + // block is identified by a unique number (rustc calls this a + // "disambiguator"), which we grab. + // + // Example: + // ======== + // For instance, if we write the following code in crate `test` and module + // `bla`: + // ``` + // impl Foo { + // fn foo() { ... } + // } + // + // impl Foo { + // fn bar() { ... } + // } + // ``` + // + // The names we will generate for `foo` and `bar` are: + // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(0), Ident("foo")]` + // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(1), Ident("bar")]` + let mut found_crate_name = false; + let mut name: Vec = Vec::new(); + + let def_path = tcx.def_path(def_id); + let crate_name = tcx.crate_name(def_path.krate).to_string(); + + let parents: Vec = { + let mut parents = vec![def_id]; + let mut cur_id = def_id; + while let Some(parent) = tcx.opt_parent(cur_id) { + parents.push(parent); + cur_id = parent; + } + parents.into_iter().rev().collect() + }; + + // Rk.: below we try to be as tight as possible with regards to sanity + // checks, to make sure we understand what happens with def paths, and + // fail whenever we get something which is even slightly outside what + // we expect. + for cur_id in parents { + let data = tcx.def_key(cur_id).disambiguated_data; + // Match over the key data + let disambiguator = Disambiguator::new(data.disambiguator as usize); + use rustc_hir::definitions::DefPathData; + match &data.data { + DefPathData::TypeNs(symbol) => { + error_assert!(self, span, data.disambiguator == 0); // Sanity check + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::ValueNs(symbol) => { + // I think `disambiguator != 0` only with names introduced by macros (though + // not sure). + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::CrateRoot => { + // Sanity check + error_assert!(self, span, data.disambiguator == 0); + + // This should be the beginning of the path + error_assert!(self, span, name.is_empty()); + found_crate_name = true; + name.push(PathElem::Ident(crate_name.clone(), disambiguator)); + } + DefPathData::Impl => { + // We need to convert the type, which may contain quantified + // substs and bounds. In order to properly do so, we introduce + // a body translation context. + let id = cur_id; + + // Translate from hax to LLBC + let mut bt_ctx = BodyTransCtx::new(id, self); + + // Translate to hax types + // TODO: use the bounds + let _bounds: Vec = bt_ctx + .t_ctx + .tcx + .predicates_of(id) + .predicates + .iter() + .map(|(x, _)| x.sinto(&bt_ctx.hax_state)) + .collect(); + let ty = tcx + .type_of(id) + .instantiate_identity() + .sinto(&bt_ctx.hax_state); + + bt_ctx.translate_generic_params(id)?; + bt_ctx.translate_predicates_of(None, id, PredicateOrigin::WhereClauseOnImpl)?; + let erase_regions = false; + // Two cases, depending on whether the impl block is + // a "regular" impl block (`impl Foo { ... }`) or a trait + // implementation (`impl Bar for Foo { ... }`). + let kind = match bt_ctx.t_ctx.tcx.impl_trait_ref(id) { + None => { + // Inherent impl ("regular" impl) + let ty = bt_ctx.translate_ty(span, erase_regions, &ty)?; + ImplElemKind::Ty(ty) + } + Some(trait_ref) => { + // Trait implementation + let trait_ref = trait_ref.sinto(&bt_ctx.hax_state); + let erase_regions = false; + let trait_ref = + bt_ctx.translate_trait_decl_ref(span, erase_regions, &trait_ref)?; + match trait_ref { + None => error_or_panic!(self, span, "The trait reference was ignored while we need it to compute the name"), + Some(trait_ref) => { + ImplElemKind::Trait(trait_ref) + } + } + } + }; + + name.push(PathElem::Impl(ImplElem { + disambiguator, + generics: bt_ctx.get_generics(), + kind, + })); + } + DefPathData::OpaqueTy => { + // TODO: do nothing for now + } + DefPathData::MacroNs(symbol) => { + error_assert!(self, span, data.disambiguator == 0); // Sanity check + + // There may be namespace collisions between, say, function + // names and macros (not sure). However, this isn't much + // of an issue here, because for now we don't expose macros + // in the AST, and only use macro names in [register], for + // instance to filter opaque modules. + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::Closure => { + // TODO: this is not very satisfactory, but on the other hand + // we should be able to extract closures in local let-bindings + // (i.e., we shouldn't have to introduce top-level let-bindings). + name.push(PathElem::Ident("closure".to_string(), disambiguator)) + } + DefPathData::ForeignMod => { + // Do nothing, functions in `extern` blocks are in the same namespace as the + // block. + } + _ => { + error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data)); + } + } + } + + // We always add the crate name + if !found_crate_name { + name.push(PathElem::Ident(crate_name, Disambiguator::new(0))); + } + + trace!("{:?}", name); + Ok(Name { name }) + } + + /// Returns an optional name for an HIR item. + /// + /// If the option is `None`, it means the item is to be ignored (example: it + /// is a `use` item). + /// + /// Rk.: this function is only used by [crate::register], and implemented with this + /// context in mind. + pub fn hir_item_to_name(&mut self, item: &Item) -> Result, Error> { + let def_id = item.owner_id.to_def_id(); + + let name = match &item.kind { + ItemKind::OpaqueTy(..) => unimplemented!(), + ItemKind::Union(..) => unimplemented!(), + ItemKind::ExternCrate(..) => { + // We ignore this - + // TODO: investigate when extern crates appear, and why + None + } + ItemKind::Use(..) => None, + ItemKind::TyAlias(..) + | ItemKind::Enum(..) + | ItemKind::Struct(..) + | ItemKind::Fn(..) + | ItemKind::Impl(..) + | ItemKind::Mod(..) + | ItemKind::ForeignMod { .. } + | ItemKind::Const(..) + | ItemKind::Static(..) + | ItemKind::Macro(..) + | ItemKind::Trait(..) => Some(self.def_id_to_name(def_id)?), + _ => { + unimplemented!("{:?}", item.kind); + } + }; + Ok(name) + } + + pub fn hax_def_id_to_name(&mut self, def_id: &hax::DefId) -> Result { + // We have to create a hax state, which is annoying... + self.def_id_to_name(DefId::from(def_id)) + } + /// Compute the span information for a Rust definition identified by its id. pub(crate) fn translate_span_from_rid(&mut self, def_id: DefId) -> Span { - // Retrieve the span from the def id - let rspan = meta::get_rspan_from_def_id(self.tcx, def_id); + // Retrieve the span from the def id. + // Rem.: we use [TyCtxt::def_span], not [TyCtxt::def_ident_span] to retrieve the span. + let rspan = self.tcx.def_span(def_id); let rspan = rspan.sinto(&self.hax_state); self.translate_span_from_rspan(rspan) } @@ -561,8 +528,51 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { }) } + pub fn translate_filename(&mut self, name: &hax::FileName) -> meta::FileName { + match name { + hax::FileName::Real(name) => { + use hax::RealFileName; + match name { + RealFileName::LocalPath(path) => FileName::Local(path.clone()), + RealFileName::Remapped { virtual_name, .. } => { + // We use the virtual name because it is always available. + // That name normally starts with `/rustc//`. For our purposes we hide + // the hash. + let mut components_iter = virtual_name.components(); + if let Some( + [Component::RootDir, Component::Normal(rustc), Component::Normal(hash)], + ) = components_iter.by_ref().array_chunks().next() + && rustc.to_str() == Some("rustc") + && hash.len() == 40 + { + let path_without_hash = [Component::RootDir, Component::Normal(rustc)] + .into_iter() + .chain(components_iter) + .collect(); + FileName::Virtual(path_without_hash) + } else { + FileName::Virtual(virtual_name.clone()) + } + } + } + } + hax::FileName::QuoteExpansion(_) + | hax::FileName::Anon(_) + | hax::FileName::MacroExpansion(_) + | hax::FileName::ProcMacroSourceCode(_) + | hax::FileName::CliCrateAttr(_) + | hax::FileName::Custom(_) + | hax::FileName::DocTest(..) + | hax::FileName::InlineAsm(_) => { + // We use the debug formatter to generate a filename. + // This is not ideal, but filenames are for debugging anyway. + FileName::NotReal(format!("{name:?}")) + } + } + } + pub fn translate_span(&mut self, rspan: hax::Span) -> meta::RawSpan { - let filename = meta::convert_filename(&rspan.filename); + let filename = self.translate_filename(&rspan.filename); let file_id = match &filename { FileName::NotReal(_) => { // For now we forbid not real filenames @@ -571,8 +581,14 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename), }; - let beg = meta::convert_loc(rspan.lo); - let end = meta::convert_loc(rspan.hi); + fn convert_loc(loc: hax::Loc) -> Loc { + Loc { + line: loc.line, + col: loc.col, + } + } + let beg = convert_loc(rspan.lo); + let end = convert_loc(rspan.hi); // Put together meta::RawSpan { @@ -636,12 +652,54 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { .unwrap_or_default() } + /// Parse an attribute to recognize our special `charon::*` and `aeneas::*` attributes. + pub(crate) fn parse_attribute( + &mut self, + normal_attr: &rustc_ast::NormalAttr, + span: rustc_span::Span, + ) -> Result { + // We use `pprust` to render the attribute somewhat like it is written in the source. + // WARNING: this can change whitespace, and sometimes even adds newlines. Maybe we + // should use spans and SourceMap info instead. + use pprust::PrintState; + + // If the attribute path has two components, the first of which is `charon` or `aeneas`, we + // try to parse it. Otherwise we return `Unknown`. + let attr_name = if let [path_start, attr_name] = normal_attr.item.path.segments.as_slice() + && let path_start = path_start.ident.as_str() + && (path_start == "charon" || path_start == "aeneas") + { + attr_name.ident.as_str() + } else { + let full_attr = + pprust::State::to_string(|s| s.print_attr_item(&normal_attr.item, span)); + return Ok(Attribute::Unknown(full_attr)); + }; + + let args = match &normal_attr.item.args { + AttrArgs::Empty => None, + AttrArgs::Delimited(args) => Some(rustc_ast_pretty::pprust::State::to_string(|s| { + s.print_tts(&args.tokens, false) + })), + AttrArgs::Eq(..) => unimplemented!("`#[charon::foo = val]` syntax is unsupported"), + }; + match Attribute::parse_special_attr(attr_name, args)? { + Some(parsed) => Ok(parsed), + None => { + let full_attr = rustc_ast_pretty::pprust::State::to_string(|s| { + s.print_attr_item(&normal_attr.item, span) + }); + Err(format!("Unrecognized attribute: `{full_attr}`")) + } + } + } + /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc /// encodes them as attributes). For now we use `String`s for `Attributes`. pub(crate) fn translate_attribute(&mut self, attr: &rustc_ast::Attribute) -> Option { use rustc_ast::ast::AttrKind; match &attr.kind { - AttrKind::Normal(normal_attr) => match Attribute::parse(&normal_attr, attr.span) { + AttrKind::Normal(normal_attr) => match self.parse_attribute(&normal_attr, attr.span) { Ok(a) => Some(a), Err(msg) => { self.span_err(attr.span, &format!("Error parsing attribute: {msg}")); @@ -803,8 +861,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { src: &Option, id: DefId, ) -> Result, Error> { - use crate::assumed; - if assumed::IGNORE_BUILTIN_MARKER_TRAITS { + if IGNORE_BUILTIN_MARKER_TRAITS { let name = self.def_id_to_name(id)?; if assumed::is_marker_trait(&name) { return Ok(None); @@ -1116,17 +1173,6 @@ impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslateCtx<'tcx, 'ctx> { } } -impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate { - type C = FmtCtx<'a>; - - fn into_fmt(self) -> Self::C { - FmtCtx { - translated: Some(self), - ..Default::default() - } - } -} - impl<'tcx, 'ctx, 'ctx1, 'a> IntoFormatter for &'a BodyTransCtx<'tcx, 'ctx, 'ctx1> { type C = FmtCtx<'a>; @@ -1146,37 +1192,3 @@ impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx, 'ctx> { self.translated.fmt(f) } } - -impl fmt::Display for TranslatedCrate { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - let fmt: FmtCtx = self.into_fmt(); - match &self.ordered_decls { - None => { - // We do simple: types, globals, traits, functions - for d in &self.type_decls { - writeln!(f, "{}\n", fmt.format_object(d))? - } - for d in &self.global_decls { - writeln!(f, "{}\n", fmt.format_object(d))? - } - for d in &self.trait_decls { - writeln!(f, "{}\n", fmt.format_object(d))? - } - for d in &self.trait_impls { - writeln!(f, "{}\n", fmt.format_object(d))? - } - for d in &self.fun_decls { - writeln!(f, "{}\n", fmt.format_object(d))? - } - } - Some(ordered_decls) => { - for gr in ordered_decls { - for id in gr.get_ids() { - writeln!(f, "{}\n", fmt.format_decl_id(id))? - } - } - } - } - fmt::Result::Ok(()) - } -} diff --git a/charon/src/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs similarity index 98% rename from charon/src/translate/translate_functions_to_ullbc.rs rename to charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index 4c4a25cd..a04cf67a 100644 --- a/charon/src/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -5,23 +5,19 @@ use std::mem; use std::panic; - -use crate::assumed::BuiltinFun; -use crate::common::*; -use crate::expressions::*; -use crate::formatter::{Formatter, IntoFormatter}; -use crate::get_mir::{boxes_are_desugared, get_mir_for_def_id_and_level}; -use crate::ids::Vector; -use crate::meta::ItemMeta; -use crate::names::Name; -use crate::pretty::FmtWithCtx; -use crate::translate_ctx::*; -use crate::translate_types; -use crate::types::*; -use crate::ullbc_ast::*; -use crate::values::*; +use std::rc::Rc; + +use super::get_mir::{boxes_are_desugared, get_mir_for_def_id_and_level}; +use super::translate_ctx::*; +use super::translate_types; +use charon_lib::ast::*; +use charon_lib::common::*; +use charon_lib::formatter::{Formatter, IntoFormatter}; +use charon_lib::ids::Vector; +use charon_lib::pretty::FmtWithCtx; +use charon_lib::ullbc_ast::*; use hax_frontend_exporter as hax; -use hax_frontend_exporter::SInto; +use hax_frontend_exporter::{HasMirSetter, HasOwnerIdSetter, SInto}; use rustc_hir::def_id::DefId; use rustc_middle::mir::START_BLOCK; use rustc_middle::ty; @@ -1448,16 +1444,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { }; // Here, we have to create a MIR state, which contains the body - let state = hax::state::State::new_from_mir( - tcx, - hax::options::Options { - inline_macro_calls: Vec::new(), - }, - // Yes, we have to clone, this is annoying: we end up cloning the body twice - body.clone(), - // Owner id - rust_id, - ); + // Yes, we have to clone, this is annoying: we end up cloning the body twice + let state = self + .hax_state + .clone() + .with_owner_id(rust_id) + .with_mir(Rc::new(body.clone())); // Translate let body: hax::MirBody<()> = body.sinto(&state); diff --git a/charon/src/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs similarity index 98% rename from charon/src/translate/translate_predicates.rs rename to charon/src/bin/charon-driver/translate/translate_predicates.rs index df8406e3..e39a6178 100644 --- a/charon/src/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -1,11 +1,10 @@ -use crate::common::*; -use crate::formatter::Formatter; -use crate::formatter::IntoFormatter; -use crate::gast::*; -use crate::meta::Span; -use crate::pretty::FmtWithCtx; -use crate::translate_ctx::*; -use crate::types::*; +use super::translate_ctx::*; +use charon_lib::common::*; +use charon_lib::formatter::{AstFormatter, IntoFormatter}; +use charon_lib::gast::*; +use charon_lib::meta::Span; +use charon_lib::pretty::FmtWithCtx; +use charon_lib::types::*; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; use macros::{EnumAsGetters, EnumIsA, EnumToGetters}; @@ -56,6 +55,15 @@ impl NonLocalTraitClause { } } +impl FmtWithCtx for NonLocalTraitClause { + fn fmt_with_ctx(&self, ctx: &C) -> String { + let clause_id = self.clause_id.fmt_with_ctx(ctx); + let trait_id = ctx.format_object(self.trait_id); + let generics = self.generics.fmt_with_ctx(ctx); + format!("[{clause_id}]: {trait_id}{generics}") + } +} + #[derive(Debug, Clone, EnumIsA, EnumAsGetters, EnumToGetters)] pub(crate) enum Predicate { Trait(#[expect(dead_code)] TraitClauseId), diff --git a/charon/src/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs similarity index 98% rename from charon/src/translate/translate_traits.rs rename to charon/src/bin/charon-driver/translate/translate_traits.rs index 7494c859..5d294dcb 100644 --- a/charon/src/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -1,12 +1,13 @@ -use crate::common::*; -use crate::formatter::IntoFormatter; -use crate::gast::*; -use crate::ids::Vector; -use crate::meta::ItemMeta; -use crate::pretty::FmtWithCtx; -use crate::translate_ctx::*; -use crate::types::*; -use crate::ullbc_ast as ast; +use super::translate_ctx::*; +use charon_lib::ast::krate::*; +use charon_lib::common::*; +use charon_lib::formatter::IntoFormatter; +use charon_lib::gast::*; +use charon_lib::ids::Vector; +use charon_lib::meta::ItemMeta; +use charon_lib::pretty::FmtWithCtx; +use charon_lib::types::*; +use charon_lib::ullbc_ast as ast; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; use rustc_hir::def_id::DefId; diff --git a/charon/src/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs similarity index 96% rename from charon/src/translate/translate_types.rs rename to charon/src/bin/charon-driver/translate/translate_types.rs index 8d5f831d..dab59b88 100644 --- a/charon/src/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -1,13 +1,10 @@ -use crate::assumed; -use crate::common::*; -use crate::formatter::IntoFormatter; -use crate::gast::*; -use crate::ids::Vector; -use crate::meta::ItemMeta; -use crate::pretty::FmtWithCtx; -use crate::translate_ctx::*; -use crate::types::*; -use crate::values::ScalarValue; +use super::translate_ctx::*; +use charon_lib::assumed; +use charon_lib::ast::*; +use charon_lib::common::*; +use charon_lib::formatter::IntoFormatter; +use charon_lib::ids::Vector; +use charon_lib::pretty::FmtWithCtx; use core::convert::*; use hax::Visibility; use hax_frontend_exporter as hax; @@ -180,12 +177,28 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { match ty { hax::Ty::Bool => Ok(Ty::Literal(LiteralTy::Bool)), hax::Ty::Char => Ok(Ty::Literal(LiteralTy::Char)), - hax::Ty::Int(int_ty) => Ok(Ty::Literal(LiteralTy::Integer( - IntegerTy::rust_int_ty_to_integer_ty(*int_ty), - ))), - hax::Ty::Uint(int_ty) => Ok(Ty::Literal(LiteralTy::Integer( - IntegerTy::rust_uint_ty_to_integer_ty(*int_ty), - ))), + hax::Ty::Int(int_ty) => { + use hax::IntTy; + Ok(Ty::Literal(LiteralTy::Integer(match int_ty { + IntTy::Isize => IntegerTy::Isize, + IntTy::I8 => IntegerTy::I8, + IntTy::I16 => IntegerTy::I16, + IntTy::I32 => IntegerTy::I32, + IntTy::I64 => IntegerTy::I64, + IntTy::I128 => IntegerTy::I128, + }))) + } + hax::Ty::Uint(int_ty) => { + use hax::UintTy; + Ok(Ty::Literal(LiteralTy::Integer(match int_ty { + UintTy::Usize => IntegerTy::Usize, + UintTy::U8 => IntegerTy::U8, + UintTy::U16 => IntegerTy::U16, + UintTy::U32 => IntegerTy::U32, + UintTy::U64 => IntegerTy::U64, + UintTy::U128 => IntegerTy::U128, + }))) + } hax::Ty::Float(_) => { trace!("Float"); error_or_panic!(self, span, "Floats are not supported yet") diff --git a/charon/src/bin/charon/main.rs b/charon/src/bin/charon/main.rs index 4b7ffa03..dde5953c 100644 --- a/charon/src/bin/charon/main.rs +++ b/charon/src/bin/charon/main.rs @@ -32,15 +32,15 @@ // Don't link with the `charon_lib` crate so that the `charon` binary doesn't have to dynamically // link to `librustc_driver.so` etc. -#[path = "../../cli_options.rs"] -mod cli_options; #[path = "../../logger.rs"] mod logger; +#[path = "../../options.rs"] +mod options; mod toml_config; use anyhow::bail; use clap::Parser; -use cli_options::{CliOpts, CHARON_ARGS}; +use options::{CliOpts, CHARON_ARGS}; use serde::Deserialize; use std::env; use std::ffi::OsStr; diff --git a/charon/src/bin/charon/toml_config.rs b/charon/src/bin/charon/toml_config.rs index 8c0ef03e..64b02556 100644 --- a/charon/src/bin/charon/toml_config.rs +++ b/charon/src/bin/charon/toml_config.rs @@ -2,7 +2,7 @@ use serde::Deserialize; use std::path::PathBuf; -use crate::{cli_options::CliOpts, trace}; +use crate::{options::CliOpts, trace}; /// The struct used to define the options available in `Charon.toml` files. #[derive(Debug, Deserialize)] diff --git a/charon/src/deps_errors.rs b/charon/src/deps_errors.rs deleted file mode 100644 index 04cb7e43..00000000 --- a/charon/src/deps_errors.rs +++ /dev/null @@ -1,136 +0,0 @@ -//! Utilities to generate error reports about the external dependencies. -use crate::translate_ctx::*; -use macros::VariantIndexArity; -use petgraph::algo::dijkstra::dijkstra; -use petgraph::graphmap::DiGraphMap; -use rustc_error_messages::MultiSpan; -use rustc_hir::def_id::DefId; -use rustc_span::Span; - -/// For error reporting -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, VariantIndexArity)] -enum Node { - External(DefId), - /// We use the span information only for local references - Local(DefId, Span), -} - -impl Node { - /// Value with which we order `Node`s. - fn sort_key(&self) -> impl Ord { - let (variant_index, _) = self.variant_index_arity(); - let (Self::External(def_id) | Self::Local(def_id, _)) = self; - (variant_index, def_id.index, def_id.krate) - } -} - -/// Manual impls because `DefId` is not orderable. -impl PartialOrd for Node { - fn partial_cmp(&self, other: &Self) -> Option { - Some(self.cmp(other)) - } -} -impl Ord for Node { - fn cmp(&self, other: &Self) -> std::cmp::Ordering { - self.sort_key().cmp(&other.sort_key()) - } -} - -struct Graph { - dgraph: DiGraphMap, -} - -impl std::fmt::Display for Graph { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - for (from, to, _) in self.dgraph.all_edges() { - writeln!(f, "{from:?} -> {to:?}")? - } - Ok(()) - } -} - -impl Graph { - fn new() -> Self { - Graph { - dgraph: DiGraphMap::new(), - } - } - - fn insert_node(&mut self, n: Node) { - // We have to be careful about duplicate nodes - if !self.dgraph.contains_node(n) { - self.dgraph.add_node(n); - } - } - - fn insert_edge(&mut self, from: Node, to: Node) { - self.insert_node(from); - self.insert_node(to); - if !self.dgraph.contains_edge(from, to) { - self.dgraph.add_edge(from, to, ()); - } - } -} - -impl ErrorCtx<'_> { - /// In case errors happened when extracting the definitions coming from - /// the external dependencies, print a detailed report to explain - /// to the user which dependencies were problematic, and where they - /// are used in the code. - pub fn report_external_deps_errors(&self) { - if !self.has_errors() { - return; - } - - // Create a dependency graph, with spans. - // We want to know what are the usages in the source code which - // lead to the extraction of the problematic definitions. For this - // reason, we only include edges: - // - from external def to external def - // - from local def to external def - let mut graph = Graph::new(); - - trace!("dep_sources:\n{:?}", self.dep_sources); - for (id, srcs) in &self.dep_sources { - // Only insert dependencies from external defs - if !id.is_local() { - let node = Node::External(*id); - graph.insert_node(node); - - for src in srcs { - if src.src_id.is_local() { - graph.insert_edge(node, Node::Local(src.src_id, src.span)); - } else { - graph.insert_edge(node, Node::External(src.src_id)); - } - } - } - } - trace!("Graph:\n{}", graph); - - // We need to compute the reachability graph. An easy way is simply - // to use Dijkstra on every external definition which triggered an - // error. - for id in &self.decls_with_errors { - if !id.is_local() { - let reachable = dijkstra(&graph.dgraph, Node::External(*id), None, &mut |_| 1); - trace!("id: {:?}\nreachable:\n{:?}", id, reachable); - - let reachable: Vec = reachable - .iter() - .filter_map(|(n, _)| match n { - Node::External(_) => None, - Node::Local(_, span) => Some(*span), - }) - .collect(); - - // Display the error message - let span = MultiSpan::from_spans(reachable); - let msg = format!("The external definition `{:?}` triggered errors. It is (transitively) used at the following location(s):", - *id, - ); - self.span_err_no_register(span, &msg); - } - } - } -} diff --git a/charon/src/errors.rs b/charon/src/errors.rs new file mode 100644 index 00000000..d2c2d71b --- /dev/null +++ b/charon/src/errors.rs @@ -0,0 +1,283 @@ +//! Utilities to generate error reports about the external dependencies. +use macros::VariantIndexArity; +use petgraph::algo::dijkstra::dijkstra; +use petgraph::graphmap::DiGraphMap; +use rustc_error_messages::MultiSpan; +use rustc_errors::DiagCtxtHandle; +use rustc_span::def_id::DefId; +use std::cmp::{Ord, PartialOrd}; +use std::collections::{HashMap, HashSet}; + +#[macro_export] +macro_rules! register_error_or_panic { + ($ctx:expr, $span: expr, $msg: expr) => {{ + $ctx.span_err($span, &$msg); + if !$ctx.continue_on_failure() { + panic!("{}", $msg); + } + }}; +} +pub use register_error_or_panic; + +/// Macro to either panic or return on error, depending on the CLI options +#[macro_export] +macro_rules! error_or_panic { + ($ctx:expr, $span:expr, $msg:expr) => {{ + $crate::errors::register_error_or_panic!($ctx, $span, $msg); + let e = $crate::common::Error { + span: $span, + msg: $msg.to_string(), + }; + return Err(e); + }}; +} +pub use error_or_panic; + +/// Custom assert to either panic or return an error +#[macro_export] +macro_rules! error_assert { + ($ctx:expr, $span: expr, $b: expr) => { + if !$b { + let msg = format!("assertion failure: {:?}", stringify!($b)); + $crate::errors::error_or_panic!($ctx, $span, msg); + } + }; + ($ctx:expr, $span: expr, $b: expr, $msg: expr) => { + if !$b { + $crate::errors::error_or_panic!($ctx, $span, $msg); + } + }; +} +pub use error_assert; + +/// We use this to save the origin of an id. This is useful for the external +/// dependencies, especially if some external dependencies don't extract: +/// we use this information to tell the user what is the code which +/// (transitively) lead to the extraction of those problematic dependencies. +#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] +pub struct DepSource { + pub src_id: DefId, + pub span: rustc_span::Span, +} + +impl DepSource { + /// Value with which we order `DepSource`s. + fn sort_key(&self) -> impl Ord { + (self.src_id.index, self.src_id.krate) + } +} + +/// Manual impls because `DefId` is not orderable. +impl PartialOrd for DepSource { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} +impl Ord for DepSource { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.sort_key().cmp(&other.sort_key()) + } +} + +impl DepSource { + pub fn make(src_id: DefId, span: rustc_span::Span) -> Option { + Some(DepSource { src_id, span }) + } +} + +/// The context for tracking and reporting errors. +pub struct ErrorCtx<'ctx> { + /// If true, do not abort on the first error and attempt to extract as much as possible. + pub continue_on_failure: bool, + /// If true, print the errors as warnings, and do not abort. + pub errors_as_warnings: bool, + + /// The compiler session, used for displaying errors. + pub dcx: DiagCtxtHandle<'ctx>, + /// The ids of the declarations for which extraction we encountered errors. + pub decls_with_errors: HashSet, + /// The ids of the declarations we completely failed to extract and had to ignore. + pub ignored_failed_decls: HashSet, + /// Dependency graph with sources. See [DepSource]. + pub dep_sources: HashMap>, + /// The id of the definition we are exploring, used to track the source of errors. + pub def_id: Option, + /// The number of errors encountered so far. + pub error_count: usize, +} + +impl ErrorCtx<'_> { + pub fn continue_on_failure(&self) -> bool { + self.continue_on_failure + } + pub(crate) fn has_errors(&self) -> bool { + self.error_count > 0 + } + + /// Report an error without registering anything. + pub(crate) fn span_err_no_register>(&self, span: S, msg: &str) { + let msg = msg.to_string(); + if self.errors_as_warnings { + self.dcx.span_warn(span, msg); + } else { + self.dcx.span_err(span, msg); + } + } + + /// Report and register an error. + pub fn span_err>(&mut self, span: S, msg: &str) { + self.span_err_no_register(span, msg); + self.error_count += 1; + if let Some(id) = self.def_id { + let _ = self.decls_with_errors.insert(id); + } + } + + /// Register the fact that `id` is a dependency of `src` (if `src` is not `None`). + pub fn register_dep_source(&mut self, src: &Option, id: DefId) { + if let Some(src) = src { + if src.src_id != id { + match self.dep_sources.get_mut(&id) { + None => { + let _ = self.dep_sources.insert(id, HashSet::from([*src])); + } + Some(srcs) => { + let _ = srcs.insert(*src); + } + } + } + } + } + + pub fn ignore_failed_decl(&mut self, id: DefId) { + self.ignored_failed_decls.insert(id); + } +} + +/// For tracing error dependencies. +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, VariantIndexArity)] +enum Node { + External(DefId), + /// We use the span information only for local references + Local(DefId, rustc_span::Span), +} + +impl Node { + /// Value with which we order `Node`s. + fn sort_key(&self) -> impl Ord { + let (variant_index, _) = self.variant_index_arity(); + let (Self::External(def_id) | Self::Local(def_id, _)) = self; + (variant_index, def_id.index, def_id.krate) + } +} + +/// Manual impls because `DefId` is not orderable. +impl PartialOrd for Node { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} +impl Ord for Node { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.sort_key().cmp(&other.sort_key()) + } +} + +struct Graph { + dgraph: DiGraphMap, +} + +impl std::fmt::Display for Graph { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { + for (from, to, _) in self.dgraph.all_edges() { + writeln!(f, "{from:?} -> {to:?}")? + } + Ok(()) + } +} + +impl Graph { + fn new() -> Self { + Graph { + dgraph: DiGraphMap::new(), + } + } + + fn insert_node(&mut self, n: Node) { + // We have to be careful about duplicate nodes + if !self.dgraph.contains_node(n) { + self.dgraph.add_node(n); + } + } + + fn insert_edge(&mut self, from: Node, to: Node) { + self.insert_node(from); + self.insert_node(to); + if !self.dgraph.contains_edge(from, to) { + self.dgraph.add_edge(from, to, ()); + } + } +} + +impl ErrorCtx<'_> { + /// In case errors happened when extracting the definitions coming from + /// the external dependencies, print a detailed report to explain + /// to the user which dependencies were problematic, and where they + /// are used in the code. + pub fn report_external_deps_errors(&self) { + if !self.has_errors() { + return; + } + + // Create a dependency graph, with spans. + // We want to know what are the usages in the source code which + // lead to the extraction of the problematic definitions. For this + // reason, we only include edges: + // - from external def to external def + // - from local def to external def + let mut graph = Graph::new(); + + trace!("dep_sources:\n{:?}", self.dep_sources); + for (id, srcs) in &self.dep_sources { + // Only insert dependencies from external defs + if !id.is_local() { + let node = Node::External(*id); + graph.insert_node(node); + + for src in srcs { + if src.src_id.is_local() { + graph.insert_edge(node, Node::Local(src.src_id, src.span)); + } else { + graph.insert_edge(node, Node::External(src.src_id)); + } + } + } + } + trace!("Graph:\n{}", graph); + + // We need to compute the reachability graph. An easy way is simply + // to use Dijkstra on every external definition which triggered an + // error. + for id in &self.decls_with_errors { + if !id.is_local() { + let reachable = dijkstra(&graph.dgraph, Node::External(*id), None, &mut |_| 1); + trace!("id: {:?}\nreachable:\n{:?}", id, reachable); + + let reachable: Vec = reachable + .iter() + .filter_map(|(n, _)| match n { + Node::External(_) => None, + Node::Local(_, span) => Some(*span), + }) + .collect(); + + // Display the error message + let span = MultiSpan::from_spans(reachable); + let msg = format!("The external definition `{:?}` triggered errors. It is (transitively) used at the following location(s):", + *id, + ); + self.span_err_no_register(span, &msg); + } + } + } +} diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 78a0d0b4..1e7c9917 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -11,15 +11,12 @@ //! we reconstructed the control-flow to have `if ... then ... else ...`, //! loops, etc. instead of `GOTO`s). -#![expect(incomplete_features)] #![feature(rustc_private)] // For rustdoc: prevents overflows #![recursion_limit = "256"] #![feature(box_patterns)] -#![feature(deref_patterns)] #![feature(if_let_guard)] #![feature(impl_trait_in_assoc_type)] -#![feature(iter_array_chunks)] #![feature(iterator_try_collect)] #![feature(let_chains)] #![feature(lint_reasons)] @@ -28,42 +25,27 @@ // For when we use charon on itself :3 #![register_tool(charon)] -extern crate rustc_ast; -extern crate rustc_ast_pretty; -extern crate rustc_attr; +extern crate rustc_driver; extern crate rustc_error_messages; extern crate rustc_errors; -extern crate rustc_hir; -extern crate rustc_index; -extern crate rustc_middle; extern crate rustc_span; -extern crate rustc_target; #[macro_use] pub mod ids; #[macro_use] pub mod logger; pub mod ast; -pub mod cli_options; pub mod common; -pub mod deps_errors; +pub mod errors; pub mod export; +pub mod options; pub mod pretty; pub mod transform; -pub mod translate; // Re-export all the ast modules so we can keep the old import structure. -pub use ast::{ - assumed, expressions, expressions_utils, gast, gast_utils, llbc_ast, llbc_ast_utils, meta, - meta_utils, names, names_utils, types, types_utils, ullbc_ast, ullbc_ast_utils, values, - values_utils, -}; +pub use ast::{assumed, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values}; pub use pretty::formatter; pub use transform::{graphs, reorder_decls, ullbc_to_llbc}; -pub use translate::{ - get_mir, translate_constants, translate_crate_to_ullbc, translate_ctx, - translate_functions_to_ullbc, translate_predicates, translate_traits, translate_types, -}; /// The version of the crate, as defined in `Cargo.toml`. const VERSION: &str = env!("CARGO_PKG_VERSION"); diff --git a/charon/src/cli_options.rs b/charon/src/options.rs similarity index 85% rename from charon/src/cli_options.rs rename to charon/src/options.rs index e6f1413b..5de86c69 100644 --- a/charon/src/cli_options.rs +++ b/charon/src/options.rs @@ -1,7 +1,8 @@ +#![allow(dead_code)] use clap::Parser; /// The options received as input by cargo-charon use serde::{Deserialize, Serialize}; -use std::path::PathBuf; +use std::{collections::HashSet, path::PathBuf}; /// The name of the environment variable we use to save the serialized Cli options /// when calling charon-driver from cargo-charon. @@ -198,3 +199,30 @@ impl CliOpts { ); } } + +/// TODO: maybe we should always target MIR Built, this would make things +/// simpler. In particular, the MIR optimized is very low level and +/// reveals too many types and data-structures that we don't want to manipulate. +#[derive(Clone, Copy, PartialEq, Eq)] +pub enum MirLevel { + /// Original MIR, directly translated from HIR. + Built, + /// Not sure what this is. Not well tested. + Promoted, + /// MIR after optimization passes. The last one before codegen. + Optimized, +} + +/// The options that control translation. +pub struct TransOptions { + /// The level at which to extract the MIR + pub mir_level: MirLevel, + /// Error out if some code ends up being duplicated by the control-flow + /// reconstruction (note that because several patterns in a match may lead + /// to the same branch, it is node always possible not to duplicate code). + pub no_code_duplication: bool, + /// Whether to extract the bodies of foreign methods and structs with private fields. + pub extract_opaque_bodies: bool, + /// Modules to consider opaque. + pub opaque_mods: HashSet, +} diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index eb5656d2..c82e0d28 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1,20 +1,13 @@ //! Utilities for pretty-printing (u)llbc. use crate::{ - assumed::get_name_from_type_id, common::TAB_INCR, formatter::*, gast, ids::Vector, llbc_ast::{self as llbc, *}, - meta::*, - names::*, reorder_decls::*, - translate_predicates::NonLocalTraitClause, - types::*, ullbc_ast::{self as ullbc, *}, - values::*, }; -use hax_frontend_exporter as hax; use itertools::Itertools; /// Format the AST type as a string. @@ -650,15 +643,6 @@ impl FmtWithCtx for Name { } } -impl FmtWithCtx for NonLocalTraitClause { - fn fmt_with_ctx(&self, ctx: &C) -> String { - let clause_id = self.clause_id.fmt_with_ctx(ctx); - let trait_id = ctx.format_object(self.trait_id); - let generics = self.generics.fmt_with_ctx(ctx); - format!("[{clause_id}]: {trait_id}{generics}") - } -} - impl FmtWithCtx for Operand { fn fmt_with_ctx(&self, ctx: &C) -> String { match self { @@ -1682,29 +1666,3 @@ pub fn fmt_where_clauses(tab: &str, num_parent_clauses: usize, clauses: Vec String { - use hax::IntTy::*; - match ty { - Isize => "isize".to_string(), - I8 => "i8".to_string(), - I16 => "i16".to_string(), - I32 => "i32".to_string(), - I64 => "i64".to_string(), - I128 => "i128".to_string(), - } -} - -// UintTy is not defined in the current crate -pub fn uintty_to_string(ty: hax::UintTy) -> String { - use hax::UintTy::*; - match ty { - Usize => "usize".to_string(), - U8 => "u8".to_string(), - U16 => "u16".to_string(), - U32 => "u32".to_string(), - U64 => "u64".to_string(), - U128 => "u128".to_string(), - } -} diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index e8adbc32..9bdfb978 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -1,16 +1,13 @@ use std::collections::VecDeque; +use crate::ast::*; use crate::common::TAB_INCR; use crate::gast; use crate::ids::Vector; use crate::llbc_ast; -use crate::llbc_ast::*; use crate::pretty::{fmt_with_ctx, FmtWithCtx}; -use crate::translate_ctx::{AnyTransId, TranslatedCrate}; -use crate::types::*; use crate::ullbc_ast; use crate::ullbc_ast as ast; -use crate::values::*; /// [`Formatter`](Formatter) is a trait for converting objects to string. /// diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 67235a69..2b08221f 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -1,13 +1,13 @@ +use crate::ast::*; +use crate::errors::ErrorCtx; use crate::formatter::{FmtCtx, IntoFormatter}; -use crate::gast::{Body, BodyId, FunDecl, FunDeclId, GlobalDecl, GlobalDeclId, Opaque}; use crate::ids::Vector; use crate::llbc_ast; -use crate::names::Name; +use crate::options::TransOptions; use crate::pretty::FmtWithCtx; -use crate::translate_ctx::{ErrorCtx, TransOptions, TranslatedCrate}; use crate::ullbc_ast; use rustc_error_messages::MultiSpan; -use rustc_hir::def_id::DefId; +use rustc_span::def_id::DefId; use std::fmt; /// Simpler context used for rustc-independent code transformation. This only depends on rustc for diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs index 5364b9c3..74ecd231 100644 --- a/charon/src/transform/index_to_function_calls.rs +++ b/charon/src/transform/index_to_function_calls.rs @@ -2,14 +2,10 @@ use derive_visitor::{DriveMut, VisitorMut}; -use crate::expressions::{BorrowKind, Operand, Place, ProjectionElem, Rvalue}; -use crate::gast::{Call, GenericArgs, Var}; +use crate::ast::*; use crate::ids::Vector; use crate::llbc_ast::*; -use crate::meta::Span; use crate::transform::TransformCtx; -use crate::types::*; -use crate::values::VarId; use super::ctx::LlbcPass; diff --git a/charon/src/transform/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs index e95fbc29..96d00ef5 100644 --- a/charon/src/transform/insert_assign_return_unit.rs +++ b/charon/src/transform/insert_assign_return_unit.rs @@ -4,10 +4,8 @@ //! For this reason, when the function has return type unit, we insert //! an extra assignment just before returning. -use crate::expressions::*; -use crate::llbc_ast::{ExprBody, FunDecl, GlobalDecl, Opaque, RawStatement, Statement}; +use crate::llbc_ast::*; use crate::transform::TransformCtx; -use crate::types::*; use super::ctx::LlbcPass; diff --git a/charon/src/transform/ops_to_function_calls.rs b/charon/src/transform/ops_to_function_calls.rs index 4384c520..6eedb944 100644 --- a/charon/src/transform/ops_to_function_calls.rs +++ b/charon/src/transform/ops_to_function_calls.rs @@ -2,10 +2,8 @@ //! For instance, we desugar ArrayToSlice from an unop to a function call. //! This allows a more uniform treatment later on. //! TODO: actually transform all the unops and binops to function calls? -use crate::expressions::{Rvalue, UnOp}; use crate::llbc_ast::*; use crate::transform::TransformCtx; -use crate::types::*; use super::ctx::LlbcPass; diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs index 1c8b691a..df3559ad 100644 --- a/charon/src/transform/remove_dynamic_checks.rs +++ b/charon/src/transform/remove_dynamic_checks.rs @@ -4,11 +4,11 @@ //! compiling for release). In our case, we take this into account in the semantics of our //! array/slice manipulation and arithmetic functions, on the verification side. +use crate::errors::register_error_or_panic; use crate::formatter::IntoFormatter; use crate::llbc_ast::{BinOp, FieldProjKind, Operand, ProjectionElem, Rvalue}; use crate::pretty::FmtWithCtx; use crate::transform::TransformCtx; -use crate::translate_ctx::register_error_or_panic; use crate::ullbc_ast::{BlockData, ExprBody, RawStatement, RawTerminator, Statement}; use super::ctx::UllbcPass; diff --git a/charon/src/transform/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs index e85b9eec..c17a44ea 100644 --- a/charon/src/transform/remove_read_discriminant.rs +++ b/charon/src/transform/remove_read_discriminant.rs @@ -3,11 +3,10 @@ //! `drop(v)` where `v` has type `Never` (it can happen - this module does the //! filtering). Then, we filter the unused variables ([crate::remove_unused_locals]). +use crate::ast::*; +use crate::errors::register_error_or_panic; use crate::llbc_ast::*; use crate::transform::TransformCtx; -use crate::translate_ctx::*; -use crate::types::*; -use crate::values::{Literal, ScalarValue}; use derive_visitor::visitor_enter_fn_mut; use derive_visitor::DriveMut; use itertools::Itertools; diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs index 531c6461..a3bd15d8 100644 --- a/charon/src/transform/reorder_decls.rs +++ b/charon/src/transform/reorder_decls.rs @@ -2,9 +2,6 @@ use crate::common::*; use crate::formatter::{AstFormatter, IntoFormatter}; use crate::graphs::*; use crate::transform::TransformCtx; -pub use crate::translate_ctx::AnyTransId; -use crate::translate_ctx::AnyTransItem; -use crate::types::*; use crate::ullbc_ast::*; use derive_visitor::{Drive, Visitor}; use hashlink::linked_hash_map::LinkedHashMap; diff --git a/charon/src/transform/simplify_constants.rs b/charon/src/transform/simplify_constants.rs index 3fdd4bc9..0d34a64b 100644 --- a/charon/src/transform/simplify_constants.rs +++ b/charon/src/transform/simplify_constants.rs @@ -14,8 +14,9 @@ use crate::expressions::*; use crate::meta::Span; use crate::transform::TransformCtx; use crate::types::*; -use crate::ullbc_ast::{make_locals_generator, ExprBody, RawStatement, Statement}; -use crate::ullbc_ast_utils::body_transform_operands; +use crate::ullbc_ast::{ + body_transform_operands, make_locals_generator, ExprBody, RawStatement, Statement, +}; use crate::values::VarId; use super::ctx::UllbcPass; diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index 3c729473..613c4a36 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -7,7 +7,6 @@ use crate::common::*; use crate::ids::Vector; use crate::llbc_ast::*; use crate::transform::TransformCtx; -use crate::types::*; use super::ctx::LlbcPass; diff --git a/charon/tests/generate-ml.rs b/charon/tests/generate-ml.rs index be4690be..3c36033a 100644 --- a/charon/tests/generate-ml.rs +++ b/charon/tests/generate-ml.rs @@ -350,9 +350,15 @@ fn generate_ml() -> Result<()> { } let crate_data: CrateData = { + use serde::Deserialize; let file = File::open(charon_llbc)?; let reader = BufReader::new(file); - serde_json::from_reader(reader)? + let mut deserializer = serde_json::Deserializer::from_reader(reader); + // Deserialize without recursion limit. + deserializer.disable_recursion_limit(); + // Grow stack space as needed. + let deserializer = serde_stacker::Deserializer::new(&mut deserializer); + CrateData::deserialize(deserializer)? }; let mut ctx = GenerateCtx { diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out index d8c4e780..367cc6c6 100644 --- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out +++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out @@ -6,5 +6,5 @@ error: Unsupported statement kind: intrinsic error: aborting due to 1 previous error -[ERROR charon_driver:228] Compilation encountered 1 errors +[ERROR charon_driver:249] Compilation encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/rename_attribute_failure.out b/charon/tests/ui/rename_attribute_failure.out index 56559c2f..ae9c7e1d 100644 --- a/charon/tests/ui/rename_attribute_failure.out +++ b/charon/tests/ui/rename_attribute_failure.out @@ -36,5 +36,5 @@ error: Error parsing attribute: Unrecognized attribute: `charon::something_else( error: aborting due to 6 previous errors -[ERROR charon_driver:228] Compilation encountered 6 errors +[ERROR charon_driver:249] Compilation encountered 6 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/gat.out b/charon/tests/ui/unsupported/gat.out index 1bebe58e..f62dea4b 100644 --- a/charon/tests/ui/unsupported/gat.out +++ b/charon/tests/ui/unsupported/gat.out @@ -18,5 +18,5 @@ error: Ignoring the following item due to an error: test_crate::ArraySize error: aborting due to 3 previous errors -[ERROR charon_driver:228] Compilation encountered 2 errors +[ERROR charon_driver:249] Compilation encountered 2 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/issue-165-vec-macro.out b/charon/tests/ui/unsupported/issue-165-vec-macro.out index 95a17ffa..798b1b90 100644 --- a/charon/tests/ui/unsupported/issue-165-vec-macro.out +++ b/charon/tests/ui/unsupported/issue-165-vec-macro.out @@ -8,5 +8,5 @@ error: Nullary operations are not supported error: aborting due to 1 previous error -[ERROR charon_driver:228] Compilation encountered 1 errors +[ERROR charon_driver:249] Compilation encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/projection-index-from-end.out b/charon/tests/ui/unsupported/projection-index-from-end.out index b81cfb4b..60a65d6a 100644 --- a/charon/tests/ui/unsupported/projection-index-from-end.out +++ b/charon/tests/ui/unsupported/projection-index-from-end.out @@ -6,5 +6,5 @@ error: Unexpected ProjectionElem::ConstantIndex error: aborting due to 1 previous error -[ERROR charon_driver:228] Compilation encountered 1 errors +[ERROR charon_driver:249] Compilation encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/unbound-lifetime.out b/charon/tests/ui/unsupported/unbound-lifetime.out index 543ebb38..200afb42 100644 --- a/charon/tests/ui/unsupported/unbound-lifetime.out +++ b/charon/tests/ui/unsupported/unbound-lifetime.out @@ -27,5 +27,5 @@ error: Ignoring the following item due to an error: test_crate::get error: aborting due to 3 previous errors For more information about this error, try `rustc --explain E0261`. -[ERROR charon_driver:228] Compilation encountered 2 errors +[ERROR charon_driver:249] Compilation encountered 2 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/well-formedness-bound.out b/charon/tests/ui/unsupported/well-formedness-bound.out index 6fe09249..1da14f81 100644 --- a/charon/tests/ui/unsupported/well-formedness-bound.out +++ b/charon/tests/ui/unsupported/well-formedness-bound.out @@ -14,5 +14,5 @@ error: Ignoring the following item due to an error: test_crate::get error: aborting due to 2 previous errors -[ERROR charon_driver:228] Compilation encountered 2 errors +[ERROR charon_driver:249] Compilation encountered 2 errors Error: Charon driver exited with code 1