From 29c83416474b9a6b05882e2a30a53800f0804c3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 27 May 2026 16:20:27 +0200 Subject: [PATCH 1/3] drive-by: avoid some useless rebuilds --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index a5e5a7044..f30b43029 100644 --- a/Makefile +++ b/Makefile @@ -32,7 +32,7 @@ build-charon-rust: .PHONY: build-dev-charon-rust build-dev-charon-rust: - cd charon && cargo build --profile test + cd charon && cargo test --no-run mkdir -p bin cp -f charon/target/debug/charon bin cp -f charon/target/debug/charon-driver bin From 683de619e4d23dcd5b07b46fc581c07a4f6b0a63 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 27 May 2026 19:06:38 +0200 Subject: [PATCH 2/3] Remove most unstable features from `charon_lib` --- charon/macros/src/lib.rs | 2 -- charon/src/ast/hash_cons.rs | 3 ++- charon/src/ast/names_utils.rs | 4 ++-- charon/src/ast/types_utils.rs | 2 -- charon/src/common.rs | 3 ++- charon/src/ids/index_map.rs | 15 ++++++++++++--- charon/src/ids/index_vec.rs | 14 +++++++++----- charon/src/lib.rs | 9 --------- charon/src/pretty/fmt_with_ctx.rs | 16 ++++++++-------- .../resugar/inline_local_panic_functions.rs | 4 ++-- .../simplify_output/ops_to_function_calls.rs | 8 ++++---- 11 files changed, 41 insertions(+), 39 deletions(-) diff --git a/charon/macros/src/lib.rs b/charon/macros/src/lib.rs index 4061652d6..d862e6e51 100644 --- a/charon/macros/src/lib.rs +++ b/charon/macros/src/lib.rs @@ -1,8 +1,6 @@ //! This module contains some macros for Charon. Due to technical reasons, Rust //! forces users to define such macros in a separate, dedicated library. Note //! that this doesn't apply to `macro_rules`. -#![feature(non_exhaustive_omitted_patterns_lint)] - extern crate proc_macro; use proc_macro::TokenStream; diff --git a/charon/src/ast/hash_cons.rs b/charon/src/ast/hash_cons.rs index f00a9f4cc..d2fb403db 100644 --- a/charon/src/ast/hash_cons.rs +++ b/charon/src/ast/hash_cons.rs @@ -27,7 +27,8 @@ impl HashConsed { } } -pub trait HashConsable = Hash + PartialEq + Eq + Clone + Mappable; +pub trait HashConsable: Hash + PartialEq + Eq + Clone + Mappable {} +impl HashConsable for T where T: Hash + PartialEq + Eq + Clone + Mappable {} /// Unique id identifying a hashconsed value amongst all hashconsed values. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] diff --git a/charon/src/ast/names_utils.rs b/charon/src/ast/names_utils.rs index d2b65bace..d909cb936 100644 --- a/charon/src/ast/names_utils.rs +++ b/charon/src/ast/names_utils.rs @@ -93,9 +93,9 @@ impl Name { /// Created an instantiated version of this name by putting a `PathElem::Instantiated` last. If /// the item was already instantiated, this merges the two instantiations. pub fn instantiate(mut self, binder: Binder) -> Self { - if let [.., PathElem::Instantiated(box x)] = self.name.as_mut_slice() { + if let [.., PathElem::Instantiated(x)] = self.name.as_mut_slice() { // Put the new args in place; the params are what we want but the args are wrong. - let old_args = std::mem::replace(x, binder); + let old_args = std::mem::replace(x.as_mut(), binder); // Apply the new args to the old binder to get correct args. x.skip_binder = old_args.apply(&x.skip_binder); } else { diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 41bd57723..e6338b905 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -858,8 +858,6 @@ impl std::ops::Deref for Ty { self.kind() } } -/// For deref patterns. -unsafe impl std::ops::DerefPure for Ty {} impl TypeDeclRef { pub fn new(id: TypeId, generics: GenericArgs) -> Self { diff --git a/charon/src/common.rs b/charon/src/common.rs index 8ae3e1c52..59f4ad2b1 100644 --- a/charon/src/common.rs +++ b/charon/src/common.rs @@ -103,7 +103,8 @@ pub mod type_map { marker::PhantomData, }; - pub trait Mappable = Any + Send + Sync; + pub trait Mappable: Any + Send + Sync {} + impl Mappable for T where T: Any + Send + Sync {} pub trait Mapper { type Value: Mappable; diff --git a/charon/src/ids/index_map.rs b/charon/src/ids/index_map.rs index 47f7b9c94..748bdf6ad 100644 --- a/charon/src/ids/index_map.rs +++ b/charon/src/ids/index_map.rs @@ -419,7 +419,11 @@ where I: Idx, { type Item = &'a T; - type IntoIter = impl Iterator; + type IntoIter = std::iter::FlatMap< + <&'a index_vec::IndexVec> as IntoIterator>::IntoIter, + Option<&'a T>, + fn(&'a Option) -> Option<&'a T>, + >; fn into_iter(self) -> Self::IntoIter { self.vector.iter().flat_map(|opt| opt.as_ref()) @@ -431,7 +435,11 @@ where I: Idx, { type Item = &'a mut T; - type IntoIter = impl Iterator; + type IntoIter = std::iter::FlatMap< + <&'a mut index_vec::IndexVec> as IntoIterator>::IntoIter, + Option<&'a mut T>, + fn(&'a mut Option) -> Option<&'a mut T>, + >; fn into_iter(self) -> Self::IntoIter { self.vector.iter_mut().flat_map(|opt| opt.as_mut()) @@ -443,7 +451,8 @@ where I: Idx, { type Item = T; - type IntoIter = impl DoubleEndedIterator; + type IntoIter = + std::iter::Flatten<> as IntoIterator>::IntoIter>; fn into_iter(self) -> Self::IntoIter { self.vector.into_iter().flatten() diff --git a/charon/src/ids/index_vec.rs b/charon/src/ids/index_vec.rs index 53293ae99..64a4c4249 100644 --- a/charon/src/ids/index_vec.rs +++ b/charon/src/ids/index_vec.rs @@ -47,6 +47,9 @@ impl DerefMut for IndexVec { } } +/// Only used to make a function uncallable. +pub trait Unimplemented {} + impl IndexVec where I: Idx, @@ -63,11 +66,12 @@ where } } - /// Shadow the `index_vec::IndexVec` method because it silently shifts ids. + /// Shadow the `index_vec::IndexVec` method because it silently shifts ids. Use + /// `remove_and_shift_ids` instead to be explicit. pub fn remove(&mut self, _: I) -> Option where // Make it not callable. - String: Copy, + I: Unimplemented, { panic!("remove") } @@ -187,7 +191,7 @@ where I: Idx, { type Item = &'a T; - type IntoIter = impl Iterator; + type IntoIter = <&'a index_vec::IndexVec as IntoIterator>::IntoIter; fn into_iter(self) -> Self::IntoIter { self.vector.iter() @@ -199,7 +203,7 @@ where I: Idx, { type Item = &'a mut T; - type IntoIter = impl Iterator; + type IntoIter = <&'a mut index_vec::IndexVec as IntoIterator>::IntoIter; fn into_iter(self) -> Self::IntoIter { self.vector.iter_mut() @@ -211,7 +215,7 @@ where I: Idx, { type Item = T; - type IntoIter = impl DoubleEndedIterator; + type IntoIter = as IntoIterator>::IntoIter; fn into_iter(self) -> Self::IntoIter { self.vector.into_iter() diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 3258f1814..bc3cc8870 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -23,17 +23,8 @@ clippy::should_implement_trait, clippy::useless_format )] -#![expect(incomplete_features)] -#![feature(assert_matches)] -#![feature(box_patterns)] -#![feature(deref_patterns)] -#![feature(deref_pure_trait)] #![feature(if_let_guard)] -#![feature(impl_trait_in_assoc_type)] -#![feature(iterator_try_collect)] #![feature(register_tool)] -#![feature(trait_alias)] -#![feature(trivial_bounds)] // For when we use charon on itself :3 #![register_tool(charon)] diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 37499e08c..1b76f131f 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1646,14 +1646,14 @@ impl FmtWithCtx for ullbc::Statement { place.with_ctx(ctx), variant_id ), - StatementKind::CopyNonOverlapping(box CopyNonOverlapping { src, dst, count }) => { + StatementKind::CopyNonOverlapping(cno) => { write!( f, "{}copy_nonoverlapping({}, {}, {})", tab, - src.with_ctx(ctx), - dst.with_ctx(ctx), - count.with_ctx(ctx), + cno.src.with_ctx(ctx), + cno.dst.with_ctx(ctx), + cno.count.with_ctx(ctx), ) } StatementKind::StorageLive(var_id) => { @@ -1693,13 +1693,13 @@ impl FmtWithCtx for llbc::Statement { StatementKind::SetDiscriminant(place, variant_id) => { write!(f, "@discriminant({}) = {}", place.with_ctx(ctx), variant_id) } - StatementKind::CopyNonOverlapping(box CopyNonOverlapping { src, dst, count }) => { + StatementKind::CopyNonOverlapping(cno) => { write!( f, "copy_nonoverlapping({}, {}, {})", - src.with_ctx(ctx), - dst.with_ctx(ctx), - count.with_ctx(ctx), + cno.src.with_ctx(ctx), + cno.dst.with_ctx(ctx), + cno.count.with_ctx(ctx), ) } StatementKind::StorageLive(var_id) => { diff --git a/charon/src/transform/resugar/inline_local_panic_functions.rs b/charon/src/transform/resugar/inline_local_panic_functions.rs index 9b0b2a16d..1b01071ef 100644 --- a/charon/src/transform/resugar/inline_local_panic_functions.rs +++ b/charon/src/transform/resugar/inline_local_panic_functions.rs @@ -49,14 +49,14 @@ impl UllbcPass for Transform { Call { func: FnOperand::Regular(FnPtr { - kind: box FnPtrKind::Fun(FunId::Regular(fun_id)), - .. + kind: fn_ptr_kind, .. }), .. }, on_unwind: _, // TODO: shouldn't we use this? .. } = &block.terminator.kind + && let FnPtrKind::Fun(FunId::Regular(fun_id)) = fn_ptr_kind.as_ref() && panic_fns.contains(fun_id) { block.terminator.kind = panic_terminator.clone(); diff --git a/charon/src/transform/simplify_output/ops_to_function_calls.rs b/charon/src/transform/simplify_output/ops_to_function_calls.rs index 4ed46b0c9..5f8ae5715 100644 --- a/charon/src/transform/simplify_output/ops_to_function_calls.rs +++ b/charon/src/transform/simplify_output/ops_to_function_calls.rs @@ -17,10 +17,10 @@ fn transform_st(s: &mut Statement) { op, ), ) => { - if let ( - TyKind::Ref(_, deref!(TyKind::Array(arr_ty, len)), kind1), - TyKind::Ref(_, deref!(TyKind::Slice(_)), kind2), - ) = (src_ty.kind(), tgt_ty.kind()) + if let (TyKind::Ref(_, ty1, kind1), TyKind::Ref(_, ty2, kind2)) = + (src_ty.kind(), tgt_ty.kind()) + && let TyKind::Array(arr_ty, len) = ty1.kind() + && let TyKind::Slice(..) = ty2.kind() { // In MIR terminology, we go from &[T; l] to &[T] which means we // effectively "unsize" the type, as `l` no longer appears in the From 4f5514754ba02bf5f42a5ec86c8f5f6cc095a044 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 27 May 2026 19:17:07 +0200 Subject: [PATCH 3/3] Gate `#[charon::*]` attribute usage --- charon/Cargo.toml | 2 ++ charon/src/ast/expressions.rs | 38 ++++++++++---------- charon/src/ast/gast.rs | 18 +++++----- charon/src/ast/krate.rs | 8 ++--- charon/src/ast/llbc_ast.rs | 2 +- charon/src/ast/meta.rs | 12 +++---- charon/src/ast/names.rs | 4 +-- charon/src/ast/types.rs | 56 +++++++++++++++--------------- charon/src/ast/types/vars.rs | 2 +- charon/src/ast/ullbc_ast.rs | 8 ++--- charon/src/ast/values.rs | 8 ++--- charon/src/bin/generate-ml/main.rs | 2 ++ charon/src/export.rs | 2 +- charon/src/ids/index_map.rs | 2 +- charon/src/lib.rs | 4 +-- charon/src/options.rs | 6 ++-- 16 files changed, 89 insertions(+), 85 deletions(-) diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 9a333eaa7..bde3b9aa3 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -116,6 +116,8 @@ which = "7.0" [features] default = [] +# Enable the `charon` tool attribute when translating charon with itself. +charon_on_charon = [] # This feature enables the `popular-crates` test which runs Charon on the most downloaded crates from crates.io. popular-crates-test = [ "dep:crates_io_api", diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index a7f343137..fd2d3f2fd 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -27,7 +27,7 @@ pub struct Place { Drive, DriveMut, )] -#[charon::variants_prefix("Place")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Place"))] pub enum PlaceKind { /// A local variable in a function body. Local(LocalId), @@ -78,7 +78,7 @@ pub enum ProjectionElem { /// MIR imposes that the argument to an index projection be a local variable, meaning /// that even constant indices into arrays are let-bound as separate variables. /// We **eliminate** this variant in a micro-pass for LLBC. - #[charon::rename("ProjIndex")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("ProjIndex"))] Index { offset: Box, #[drive(skip)] @@ -108,7 +108,7 @@ pub enum ProjectionElem { Drive, DriveMut, )] -#[charon::variants_prefix("Proj")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Proj"))] pub enum FieldProjKind { Adt(TypeDeclId, Option), /// If we project from a tuple, the projection kind gives the arity of the tuple. @@ -129,7 +129,7 @@ pub enum FieldProjKind { Drive, DriveMut, )] -#[charon::variants_prefix("B")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("B"))] pub enum BorrowKind { Shared, Mut, @@ -169,7 +169,7 @@ pub enum BorrowKind { Drive, DriveMut, )] -#[charon::rename("Unop")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Unop"))] pub enum UnOp { Not, /// This can overflow, for `-i::MIN`. @@ -193,7 +193,7 @@ pub enum UnOp { Drive, DriveMut, )] -#[charon::rename("Nullop")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Nullop"))] pub enum NullOp { SizeOf, AlignOf, @@ -217,7 +217,7 @@ pub enum NullOp { Drive, DriveMut, )] -#[charon::variants_prefix("Cast")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Cast"))] pub enum CastKind { /// Conversion between types in `{Integer, Bool}` /// Remark: for now we don't support conversions with Char. @@ -259,7 +259,7 @@ pub enum CastKind { DriveMut, Hash, )] -#[charon::variants_prefix("Meta")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Meta"))] pub enum UnsizingMetadata { /// Cast from `[T; N]` to `[T]`. Length(Box), @@ -276,7 +276,7 @@ pub enum UnsizingMetadata { } #[derive(Debug, PartialEq, Eq, Copy, Clone, Serialize, Deserialize)] -#[charon::variants_prefix("O")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("O"))] pub enum OverflowMode { /// If this operation overflows, it panics. Only exists in debug mode, for instance in /// `a + b`, and only if `--reconstruct-fallible-operations` is passed to Charon. Otherwise the @@ -304,7 +304,7 @@ pub enum OverflowMode { Drive, DriveMut, )] -#[charon::rename("Binop")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Binop"))] #[serde_state(stateless)] pub enum BinOp { BitXor, @@ -365,7 +365,7 @@ pub enum Operand { Copy(Place), Move(Place), /// Constant value (including constant and static variables) - #[charon::rename("Constant")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("Constant"))] Const(Box), } @@ -384,7 +384,7 @@ pub enum Operand { Drive, DriveMut, )] -#[charon::variants_prefix("F")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("F"))] #[serde_state(stateless)] pub enum FunId { /// A "regular" function (function local to the crate, external function @@ -393,7 +393,7 @@ pub enum FunId { /// A primitive function, coming from a standard library (for instance: /// `alloc::boxed::Box::new`). /// TODO: rename to "Primitive" - #[charon::rename("FBuiltin")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("FBuiltin"))] Builtin(BuiltinFunId), } @@ -493,12 +493,12 @@ pub struct MaybeBuiltinFunDeclRef { Hash, )] pub enum FnPtrKind { - #[charon::rename("FunId")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("FunId"))] Fun(FunId), /// If a trait: the reference to the trait and the id of the trait method. /// The fun decl id is not really necessary - we put it here for convenience /// purposes. - #[charon::rename("TraitMethod")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("TraitMethod"))] Trait(TraitRef, TraitMethodId, FunDeclId), } @@ -526,7 +526,7 @@ impl From for FnPtr { } #[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, Hash)] -#[charon::variants_prefix("Prov")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Prov"))] pub enum Provenance { Global(GlobalDeclRef), Function(FunDeclRef), @@ -589,7 +589,7 @@ pub enum Byte { Drive, DriveMut, )] -#[charon::variants_prefix("C")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("C"))] pub enum ConstantExprKind { #[serde_state(stateless)] Literal(Literal), @@ -693,7 +693,7 @@ pub enum Rvalue { Use(Operand), /// Takes a reference to the given place. /// The `Operand` refers to the init value of the metadata, it is `()` if no metadata - #[charon::rename("RvRef")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("RvRef"))] Ref { place: Place, #[serde_state(stateless)] @@ -790,7 +790,7 @@ pub enum Rvalue { Drive, DriveMut, )] -#[charon::variants_prefix("Aggregated")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Aggregated"))] pub enum AggregateKind { /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 1851b1cd9..3e0106f84 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -22,7 +22,7 @@ pub struct Local { /// Span of the variable declaration. pub span: Span, /// The variable type - #[charon::rename("local_ty")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("local_ty"))] pub ty: Ty, } #[deprecated(note = "use `Local` intead")] @@ -50,7 +50,7 @@ pub struct Locals { /// TODO: arg_count should be stored in GFunDecl below. But then, /// the print is obfuscated and Aeneas may need some refactoring. #[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)] -#[charon::rename("GexprBody")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("GexprBody"))] pub struct GExprBody { pub span: Span, /// The number of regions existentially bound in this body. We introduce fresh such regions @@ -63,7 +63,7 @@ pub struct GExprBody { pub body: T, /// For each line inside the body, we record any whole-line `//` comments found before it. They /// are added to statements in the late `recover_body_comments` pass. - #[charon::opaque] + #[cfg_attr(feature = "charon_on_charon", charon::opaque)] #[drive(skip)] pub comments: Vec<(usize, Vec)>, } @@ -83,7 +83,7 @@ pub struct GExprBody { EnumToGetters, )] #[serde_state(state_implements = HashConsSerializerState)] -#[charon::variants_suffix("Body")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Body"))] pub enum Body { /// Body represented as a CFG. This is what ullbc is made of, and what we get after translating MIR. Unstructured(ullbc_ast::ExprBody), @@ -146,7 +146,7 @@ pub enum Body { /// } /// ``` #[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, PartialEq, Eq)] -#[charon::variants_suffix("Item")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Item"))] pub enum ItemSource { /// This item stands on its own. TopLevel, @@ -207,7 +207,7 @@ pub enum ItemSource { } #[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, PartialEq, Eq)] -#[charon::variants_prefix("VTable")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("VTable"))] pub enum VTableField { Size, Align, @@ -450,7 +450,7 @@ pub struct TraitAssocTyImpl { pub value: Ty, /// This matches the corresponding vector in `TraitAssocTy`. In the same way, this is empty /// after the `lift_associated_item_clauses` pass. - #[charon::opaque] + #[cfg_attr(feature = "charon_on_charon", charon::opaque)] pub implied_trait_refs: IndexVec, } @@ -458,7 +458,7 @@ pub struct TraitAssocTyImpl { /// It either designates a top-level function, or a place in case /// we are using function pointers stored in local variables. #[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)] -#[charon::variants_prefix("FnOp")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("FnOp"))] pub enum FnOperand { /// Regular case: call to a top-level function, trait method, etc. Regular(FnPtr), @@ -548,7 +548,7 @@ pub enum DropKind { /// because they're implicit in the semantics of our array accesses etc. Finally we introduce new asserts in /// [crate::transform::resugar::reconstruct_asserts]. #[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)] -#[charon::rename("Assertion")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Assertion"))] pub struct Assert { pub cond: Operand, /// The value that the operand should evaluate to for the assert to succeed. diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 2d40c5936..a4834e630 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -41,7 +41,7 @@ generate_index_type!(TraitImplId, "TraitImpl"); Drive, DriveMut, )] -#[charon::variants_prefix("Id")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Id"))] #[serde_state(stateless)] pub enum ItemId { Type(TypeDeclId), @@ -71,7 +71,7 @@ pub enum ItemId { Drive, DriveMut, )] -#[charon::variants_prefix("AssocId")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("AssocId"))] #[serde_state(stateless)] pub enum AssocItemId { Type(AssocTypeId), @@ -163,7 +163,7 @@ pub enum ItemRefMut<'ctx> { #[derive( Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize, )] -#[charon::variants_suffix("Group")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Group"))] pub enum GDeclarationGroup { /// A non-recursive declaration NonRec(Id), @@ -175,7 +175,7 @@ pub enum GDeclarationGroup { #[derive( Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize, )] -#[charon::variants_suffix("Group")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Group"))] pub enum DeclarationGroup { /// A type declaration group Type(GDeclarationGroup), diff --git a/charon/src/ast/llbc_ast.rs b/charon/src/ast/llbc_ast.rs index c5d8fa00b..97d44e483 100644 --- a/charon/src/ast/llbc_ast.rs +++ b/charon/src/ast/llbc_ast.rs @@ -92,7 +92,7 @@ pub struct Statement { pub span: Span, /// Integer uniquely identifying this statement among the statmeents in the current body. To /// simplify things we generate globally-fresh ids when creating a new `Statement`. - #[charon::rename("statement_id")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("statement_id"))] pub id: StatementId, pub kind: StatementKind, /// Comments that precede this statement. diff --git a/charon/src/ast/meta.rs b/charon/src/ast/meta.rs index df3713581..36bea94c8 100644 --- a/charon/src/ast/meta.rs +++ b/charon/src/ast/meta.rs @@ -35,11 +35,11 @@ pub struct Loc { /// Span information #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] pub struct SpanData { - #[charon::rename("file")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("file"))] pub file_id: FileId, - #[charon::rename("beg_loc")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("beg_loc"))] pub beg: Loc, - #[charon::rename("end_loc")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("end_loc"))] pub end: Loc, } @@ -111,7 +111,7 @@ pub enum InlineAttr { Drive, DriveMut, )] -#[charon::variants_prefix("Attr")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Attr"))] pub enum Attribute { /// Do not translate the body of this item. /// Written `#[charon::opaque]` @@ -203,7 +203,7 @@ pub enum ItemOpacity { /// /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was /// declared opaque via a command-line argument. - #[charon::rename("ItemOpaque")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("ItemOpaque"))] Opaque, /// Translate nothing of this item. The corresponding map will not have an entry for the /// `ItemId`. Useful when even the signature of the item causes errors. @@ -260,7 +260,7 @@ pub enum FileName { )] pub struct File { /// The file identifier. - #[charon::opaque] + #[cfg_attr(feature = "charon_on_charon", charon::opaque)] pub id: FileId, /// The path to the file. #[drive(skip)] diff --git a/charon/src/ast/names.rs b/charon/src/ast/names.rs index df956f2c1..9337e61b0 100644 --- a/charon/src/ast/names.rs +++ b/charon/src/ast/names.rs @@ -20,7 +20,7 @@ generate_index_type!(Disambiguator); EnumIsA, EnumAsGetters, )] -#[charon::variants_prefix("Pe")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Pe"))] pub enum PathElem { #[serde_state(stateless)] Ident(#[drive(skip)] String, Disambiguator), @@ -45,7 +45,7 @@ pub enum PathElem { /// ``` /// We distinguish the two. #[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)] -#[charon::variants_prefix("ImplElem")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("ImplElem"))] pub enum ImplElem { Ty(Box>), Trait(TraitImplId), diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 6b301f05a..332fe84d2 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -25,7 +25,7 @@ pub use vars::*; Drive, DriveMut, )] -#[charon::variants_prefix("R")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("R"))] pub enum Region { /// Region variable. See `DeBruijnVar` for details. Var(RegionDbVar), @@ -106,7 +106,7 @@ pub enum TraitRefKind { /// The implicit `Self: Trait` clause. Present inside trait declarations, including trait /// method declarations. Not present in trait implementations as we can use `TraitImpl` intead. - #[charon::rename("Self")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("Self"))] SelfId, /// A trait implementation that is computed by the compiler, such as for built-in trait @@ -132,7 +132,7 @@ pub enum TraitRefKind { Dyn, /// For error reporting. - #[charon::rename("UnknownTrait")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("UnknownTrait"))] #[drive(skip)] Unknown(String), } @@ -140,7 +140,7 @@ pub enum TraitRefKind { /// Describes a built-in impl. Mostly lists the implemented trait, sometimes with more details /// about the contents of the implementation. #[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)] -#[charon::variants_prefix("Builtin")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Builtin"))] pub enum BuiltinImplData { // Marker traits (without methods). Sized, @@ -242,17 +242,17 @@ pub type BoxedArgs = Box; /// issues in the derived ocaml visitors. #[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)] pub struct RegionBinder { - #[charon::rename("binder_regions")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_regions"))] #[serde_state(stateless)] pub regions: IndexVec, /// Named this way to highlight accesses to the inner value that might be handling parameters /// incorrectly. Prefer using helper methods. - #[charon::rename("binder_value")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_value"))] pub skip_binder: T, } #[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)] -#[charon::variants_prefix("BK")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("BK"))] pub enum BinderKind { /// The parameters of a generic associated type. TraitType(TraitDeclId, AssocTypeId), @@ -272,14 +272,14 @@ pub enum BinderKind { /// now), trait methods, GATs (TODO). #[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)] pub struct Binder { - #[charon::rename("binder_params")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_params"))] pub params: GenericParams, /// Named this way to highlight accesses to the inner value that might be handling parameters /// incorrectly. Prefer using helper methods. - #[charon::rename("binder_value")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_value"))] pub skip_binder: T, /// The kind of binder this is. - #[charon::opaque] + #[cfg_attr(feature = "charon_on_charon", charon::opaque)] #[drive(skip)] pub kind: BinderKind, } @@ -347,7 +347,7 @@ pub enum PredicateOrigin { // ``` TraitItem(AssocTypeId), /// Clauses that are part of a `dyn Trait` type. - #[charon::rename("OriginDyn")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("OriginDyn"))] Dyn, } @@ -440,7 +440,7 @@ pub struct Layout { #[serde_state(default_state = ())] pub enum PtrMetadata { /// Types that need no metadata, namely `T: Sized` types. - #[charon::rename("NoMetadata")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("NoMetadata"))] None, /// Metadata for `[T]` and `str`, and user-defined types /// that directly or indirectly contain one of the two. @@ -553,7 +553,7 @@ pub enum TypeDeclKind { Alias(Ty), /// Used if an error happened during the extraction, and we don't panic /// on error. - #[charon::rename("TDeclError")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("TDeclError"))] #[drive(skip)] Error(String), } @@ -565,7 +565,7 @@ pub struct Variant { pub span: Span, #[drive(skip)] pub attr_info: AttrInfo, - #[charon::rename("variant_name")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("variant_name"))] #[drive(skip)] pub name: String, #[serde_state(stateful)] @@ -582,10 +582,10 @@ pub struct Field { pub span: Span, #[drive(skip)] pub attr_info: AttrInfo, - #[charon::rename("field_name")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("field_name"))] #[drive(skip)] pub name: Option, - #[charon::rename("field_ty")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("field_ty"))] #[serde_state(stateful)] pub ty: Ty, } @@ -656,7 +656,7 @@ pub enum UIntTy { Ord, PartialOrd, )] -#[charon::rename("IntegerType")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("IntegerType"))] pub enum IntegerTy { Signed(IntTy), Unsigned(UIntTy), @@ -678,7 +678,7 @@ pub enum IntegerTy { Ord, PartialOrd, )] -#[charon::rename("FloatType")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("FloatType"))] pub enum FloatTy { F16, F32, @@ -704,7 +704,7 @@ pub enum FloatTy { Ord, PartialOrd, )] -#[charon::variants_prefix("R")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("R"))] #[serde_state(stateless)] pub enum RefKind { Mut, @@ -716,7 +716,7 @@ pub enum RefKind { #[derive( Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize, EnumIsA, )] -#[charon::variants_prefix("Lt")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Lt"))] pub enum LifetimeMutability { /// A lifetime that is used for a mutable reference. Mutable, @@ -746,13 +746,13 @@ pub enum LifetimeMutability { Ord, PartialOrd, )] -#[charon::variants_prefix("T")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))] pub enum TypeId { /// A "regular" ADT type. /// /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque, /// and external ADTs). - #[charon::rename("TAdtId")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("TAdtId"))] Adt(TypeDeclId), Tuple, /// Built-in type. Either a primitive type like array or slice, or a @@ -762,7 +762,7 @@ pub enum TypeId { /// The Array and Slice types were initially modelled as primitive in /// the [Ty] type. We decided to move them to built-in types as it allows /// for more uniform treatment throughout the codebase. - #[charon::rename("TBuiltin")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("TBuiltin"))] #[serde_state(stateless)] Builtin(BuiltinTy), } @@ -795,8 +795,8 @@ pub struct TypeDeclRef { Ord, PartialOrd, )] -#[charon::rename("LiteralType")] -#[charon::variants_prefix("T")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("LiteralType"))] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))] #[serde_state(stateless)] pub enum LiteralTy { Int(IntTy), @@ -830,7 +830,7 @@ pub struct Ty(pub HashConsed); Drive, DriveMut, )] -#[charon::variants_prefix("T")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))] pub enum TyKind { /// An ADT. /// Note that here ADTs are very general. They can be: @@ -844,7 +844,7 @@ pub enum TyKind { /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern /// types. Adt(TypeDeclRef), - #[charon::rename("TVar")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("TVar"))] TypeVar(TypeDbVar), Literal(LiteralTy), /// The never type, for computations which don't return. It is sometimes @@ -932,7 +932,7 @@ pub enum TyKind { Ord, PartialOrd, )] -#[charon::variants_prefix("T")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))] pub enum BuiltinTy { /// Boxes are de facto a primitive type. Box, diff --git a/charon/src/ast/types/vars.rs b/charon/src/ast/types/vars.rs index 13afa157c..d171f1618 100644 --- a/charon/src/ast/types/vars.rs +++ b/charon/src/ast/types/vars.rs @@ -150,7 +150,7 @@ pub struct TraitParam { #[drive(skip)] pub origin: PredicateOrigin, /// The trait that is implemented. - #[charon::rename("trait")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("trait"))] pub trait_: PolyTraitDeclRef, } diff --git a/charon/src/ast/ullbc_ast.rs b/charon/src/ast/ullbc_ast.rs index 456fd1e6e..875bd6b83 100644 --- a/charon/src/ast/ullbc_ast.rs +++ b/charon/src/ast/ullbc_ast.rs @@ -12,7 +12,7 @@ generate_index_type!(BlockId, "Block"); // The entry block of a function is always the block with id 0 pub static START_BLOCK_ID: BlockId = BlockId::ZERO; -#[charon::rename("Blocks")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Blocks"))] pub type BodyContents = IndexVec; pub type ExprBody = GExprBody; @@ -88,7 +88,7 @@ pub struct Statement { Drive, DriveMut, )] -#[charon::rename("Switch")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Switch"))] pub enum SwitchTargets { /// Gives the `if` block and the `else` block If(BlockId, BlockId), @@ -140,7 +140,7 @@ pub enum TerminatorKind { }, /// Assert that the given condition holds, and if not, unwind to the given block. This is used for /// bounds checks, overflow checks, etc. - #[charon::rename("TAssert")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("TAssert"))] Assert { assert: Assert, target: BlockId, @@ -163,7 +163,7 @@ pub struct Terminator { } #[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)] -#[charon::rename("Block")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("Block"))] pub struct BlockData { pub statements: Vec, pub terminator: Terminator, diff --git a/charon/src/ast/values.rs b/charon/src/ast/values.rs index eec3e4467..3d1e0447f 100644 --- a/charon/src/ast/values.rs +++ b/charon/src/ast/values.rs @@ -36,7 +36,7 @@ generate_index_type!(LocalId, ""); PartialOrd, Ord, )] -#[charon::variants_prefix("V")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("V"))] #[serde_state(stateless)] pub enum Literal { Scalar(ScalarValue), @@ -71,7 +71,7 @@ pub enum Literal { DriveMut, )] #[drive(skip)] -#[charon::variants_suffix("Scalar")] +#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Scalar"))] pub enum ScalarValue { Unsigned( UIntTy, @@ -91,9 +91,9 @@ pub enum ScalarValue { Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Hash, PartialOrd, Ord, Drive, DriveMut, )] pub struct FloatValue { - #[charon::rename("float_value")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("float_value"))] #[drive(skip)] pub value: String, - #[charon::rename("float_ty")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("float_ty"))] pub ty: FloatTy, } diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 252d94597..4c014ebe7 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -149,6 +149,8 @@ fn main() -> Result<()> { cmd.arg(&charon_llbc); cmd.arg("--"); cmd.arg("--lib"); + cmd.arg("--features"); + cmd.arg("charon_on_charon"); let output = cmd.output()?; if !output.status.success() { diff --git a/charon/src/export.rs b/charon/src/export.rs index bfd468375..d5428958e 100644 --- a/charon/src/export.rs +++ b/charon/src/export.rs @@ -19,7 +19,7 @@ pub struct CrateData { pub charon_version: CharonVersion, pub translated: TranslatedCrate, #[serde_state(stateless)] - #[charon::opaque] // Don't change, this would break version detection for old charon-ml + #[cfg_attr(feature = "charon_on_charon", charon::opaque)] // Don't change, this would break version detection for old charon-ml /// If there were errors, this contains only a partial description of the input crate. pub has_errors: bool, } diff --git a/charon/src/ids/index_map.rs b/charon/src/ids/index_map.rs index 748bdf6ad..2b0096acc 100644 --- a/charon/src/ids/index_map.rs +++ b/charon/src/ids/index_map.rs @@ -18,7 +18,7 @@ use derive_generic_visitor::*; /// To prevent accidental id reuse, the vector supports reserving a slot to be filled later. Use /// `IndexVec` if this is not needed. #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -#[charon::rename("IndexedMap")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("IndexedMap"))] pub struct IndexMap where I: Idx, diff --git a/charon/src/lib.rs b/charon/src/lib.rs index bc3cc8870..d85c8b395 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -24,9 +24,9 @@ clippy::useless_format )] #![feature(if_let_guard)] -#![feature(register_tool)] // For when we use charon on itself :3 -#![register_tool(charon)] +#![cfg_attr(feature = "charon_on_charon", feature(register_tool))] +#![cfg_attr(feature = "charon_on_charon", register_tool(charon))] #[macro_use] pub mod ids; diff --git a/charon/src/options.rs b/charon/src/options.rs index ce3b20d0c..e1c0b3712 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -28,7 +28,7 @@ pub const CHARON_ARGS: &str = "CHARON_ARGS"; // `Deserialize` options). #[derive(Debug, Default, Clone, clap::Args, PartialEq, Eq, Serialize, Deserialize)] #[clap(name = "Charon")] -#[charon::rename("cli_options")] +#[cfg_attr(feature = "charon_on_charon", charon::rename("cli_options"))] pub struct CliOpts { /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow) #[clap(long)] @@ -138,7 +138,7 @@ pub struct CliOpts { items in it transparent (we will translate them if we encounter them.) "))] #[serde(default)] - #[charon::rename("included")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("included"))] pub include: Vec, /// Blacklist of items to keep opaque. Works just like `--include`, see the doc there. #[clap(long)] @@ -344,7 +344,7 @@ pub enum MonomorphizeMut { pub enum SerializationFormatArg { Json, Postcard, - #[charon::rename("AllFormats")] + #[cfg_attr(feature = "charon_on_charon", charon::rename("AllFormats"))] All, }