Remove most unstable features from charon_lib

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

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",

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;

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<Operand>,
         #[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<VariantId>),
     /// 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<ConstantExpr>),
@@ -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<ConstantExpr>),
 }
 
@@ -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<FunDeclRef> 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

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<T> {
     pub span: Span,
     /// The number of regions existentially bound in this body. We introduce fresh such regions
@@ -63,7 +63,7 @@ pub struct GExprBody<T> {
     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<String>)>,
 }
@@ -83,7 +83,7 @@ pub struct GExprBody<T> {
     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,15 +450,15 @@ 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<TraitClauseId, TraitRef>,
 }
 
 /// A function operand is used in function calls.
 /// 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.

charon/src/ast/hash_cons.rs

@@ -27,7 +27,8 @@ impl<T> HashConsed<T> {
     }
 }
 
-pub trait HashConsable = Hash + PartialEq + Eq + Clone + Mappable;
+pub trait HashConsable: Hash + PartialEq + Eq + Clone + Mappable {}
+impl<T> 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)]

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<Id> {
     /// A non-recursive declaration
     NonRec(Id),
@@ -175,7 +175,7 @@ pub enum GDeclarationGroup<Id> {
 #[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<TypeDeclId>),

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.

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)]

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<Binder<Ty>>),
     Trait(TraitImplId),