charon_lib/

options.rs

//! The options that control charon behavior.
use annotate_snippets::Level;
use clap::ValueEnum;
use enum_as_inner::EnumAsInner;
use indoc::indoc;
use itertools::Itertools;
use serde::{Deserialize, Serialize};
use std::path::PathBuf;

use crate::{
    ast::*,
    errors::{ErrorCtx, display_unspanned_error},
    name_matcher::NamePattern,
    raise_error, register_error,
};

/// The name of the environment variable we use to save the serialized Cli options
/// when calling charon-driver from cargo-charon.
pub const CHARON_ARGS: &str = "CHARON_ARGS";

/// The name of an environment variable we use to control `cargo`'s caching, so that cargo reruns
/// `charon-driver` on exactly the selected crates and keeps every other crate cached.
pub fn selected_crate_var(crate_name: &str) -> String {
    format!("CHARON_SELECTED_CRATE_{crate_name}")
}

// This structure is used to store the command-line instructions.
// We automatically derive a command-line parser based on this structure.
// Note that the doc comments are used to generate the help message when using
// `--help`.
//
// Note that because we need to transmit the options to the charon driver,
// we store them in a file before calling this driver (hence the `Serialize`,
// `Deserialize` options).
#[derive(Debug, Default, Clone, PartialEq, Eq)]
#[derive(clap::Args)]
#[derive(Serialize, Deserialize)]
#[clap(name = "Charon")]
#[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)]
    #[serde(default)]
    pub ullbc: bool,
    /// Reconstruct the control-flow without duplicating blocks: a block reachable from several
    /// branches is emitted once, and the branches `break` forward to it out of an enclosing
    /// `loop`. This can shrink bodies a lot, at the cost of control-flow that is harder to read.
    /// Note that consumers which expect `if`/`loop`-shaped bodies (e.g. aeneas) may not support
    /// the result.
    #[clap(long)]
    #[serde(default)]
    pub no_code_duplication: bool,
    /// Whether to precisely translate drops and drop-related code. For this, we add explicit
    /// `Destruct` bounds to all generic parameters and set the MIR level to at least `elaborated`.
    ///
    /// Without this option, drops may be "conditional" and we may lack information about what code
    /// is run on drop in a given polymorphic function body.
    #[clap(long)]
    #[serde(default)]
    pub precise_drops: bool,
    /// The MIR stage to extract. This is only relevant for the current crate; for dependencies only
    /// MIR optimized is available.
    #[arg(long)]
    pub mir: Option<MirLevel>,
    /// Extra flags to pass to rustc.
    #[clap(long = "rustc-arg")]
    #[serde(default)]
    pub rustc_args: Vec<String>,
    /// A list of target architectures to translate for. Charon will run the compiler once for each
    /// target and aggregate the results, which is useful if the code includes `#[cfg(..)]`
    /// filters.
    /// Warning: this is an initial implementation which is extremely slow.
    #[clap(long, value_delimiter = ',')]
    #[serde(default)]
    pub targets: Vec<String>,
    /// Sysroot to use for rustc invocations. By default Charon builds a sysroot that has full MIR
    /// for the standard library. You can pass a custom sysroot to use instead, or pass "default"
    /// to use the normal distributed sysroot, which lacks MIR bodies for many standard library
    /// functions.
    #[clap(long)]
    #[serde(default)]
    pub sysroot: Option<String>,

    /// Monomorphize the items encountered when possible. Generic items found in the crate are
    /// skipped. To only translate a particular call graph, use `--start-from`. Note: this doesn't
    /// currently support `dyn Trait`.
    #[clap(long, visible_alias = "mono")]
    #[serde(default)]
    pub monomorphize: bool,
    /// Partially monomorphize items to make it so that no item is ever monomorphized with a
    /// mutable reference (or type containing one); said differently, so that the presence of
    /// mutable references in a type is independent of its generics. This is used by Aeneas.
    #[clap(
        long,
        value_name("INCLUDE_TYPES"),
        num_args(0..=1),
        require_equals(true),
        default_missing_value("all"),
    )]
    #[serde(default)]
    pub monomorphize_mut: Option<MonomorphizeMut>,

    /// A list of item paths to use as starting points for the translation. We will translate these
    /// items and any items they refer to, according to the opacity rules. When absent, we start
    /// from the path `crate` (which translates the whole crate).
    #[clap(long, value_delimiter = ',')]
    #[serde(default)]
    pub start_from: Vec<String>,
    /// Same as --start-from, but won't raise an error if a pattern doesn't match any item. This is useful
    /// when the patterns are generated by a build script and may be out of sync with the code.
    #[clap(long, value_delimiter = ',')]
    #[serde(default)]
    pub start_from_if_exists: Vec<String>,
    /// Use all the items annotated with the given attribute(s) as starting points for translation
    /// (except modules).
    /// If an attribute name is not specified, `verify::start_from` is used.
    #[clap(
        long,
        value_name("ATTRIBUTE"),
        num_args(0..),
        require_equals(true),
        value_delimiter = ',',
        default_missing_value("verify::start_from"),
    )]
    #[serde(default)]
    pub start_from_attribute: Vec<String>,
    /// Use all the `pub` items as starting points for translation (except modules).
    #[clap(long)]
    #[serde(default)]
    pub start_from_pub: bool,
    /// Use global constructors as starting points for translation, i.e. the `#[used]` statics
    /// placed in the linker section that the target runs at startup (e.g. `.init_array` on ELF).
    #[clap(long)]
    #[serde(default)]
    pub start_from_global_ctors: bool,

    /// Whitelist of items to translate. These use the name-matcher syntax.
    #[clap(
        long,
        help = indoc!("
            Whitelist of items to translate. These use the name-matcher syntax (note: this differs
            a bit from the ocaml NameMatcher).

            Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
            built-in type. It is also not possible to filter a trait impl (this will only filter
            its methods). Please report bugs or missing features.

            Examples:
              - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
                  submodules or trait methods);
              - `crate::module1::module2::item::_`: refers only to the subitems of this item;
              - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
                  very useful impl;

            When multiple patterns in the `--include` and `--opaque` options match the same item,
            the most precise pattern wins. E.g.: `charon --opaque crate::module --include
            crate::module::_` makes the `module` opaque (we won't explore its contents), but the
            items in it transparent (we will translate them if we encounter them.)
    "))]
    #[serde(default)]
    #[cfg_attr(feature = "charon_on_charon", charon::rename("included"))]
    pub include: Vec<String>,
    /// Blacklist of items to keep opaque. Works just like `--include`, see the doc there.
    #[clap(long)]
    #[serde(default)]
    pub opaque: Vec<String>,
    /// Blacklist of items to not translate at all. Works just like `--include`, see the doc there.
    #[clap(long)]
    #[serde(default)]
    pub exclude: Vec<String>,
    /// Usually we skip the bodies of foreign methods and structs with private fields. When this
    /// flag is on, we don't.
    #[clap(long)]
    #[serde(default)]
    pub extract_opaque_bodies: bool,
    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
    /// them all.
    #[clap(long)]
    #[serde(default)]
    pub translate_all_methods: bool,
    /// Usually we only translate the vtables that are used in an unsizing coercion, and leave the
    /// `vtable` field of the other trait impls as `Lazy`. When this flag is on, we translate the
    /// vtable of every trait impl of a dyn-compatible trait.
    #[clap(long)]
    #[serde(default)]
    pub eager_vtables: bool,
    /// Whenever an impl doesn't implement a method (because it has a default body), this creates a
    /// duplicate method as if it had been implemented. This can simplify the call-graphs as
    /// otherwise calls within the default body would be indirected through trait proofs.
    #[clap(long)]
    #[serde(default)]
    pub duplicate_defaulted_methods: bool,

    /// Transform the associate types of traits to be type parameters instead. This takes a list
    /// of name patterns of the traits to transform, using the same syntax as `--include`.
    #[clap(long, alias = "remove-associated-types")]
    #[serde(default)]
    pub lift_associated_types: Vec<String>,
    /// Whether to hide various marker traits such as `Sized`, `Sync`, and `Send`
    /// anywhere they show up. This can considerably speed up translation.
    #[clap(long)]
    #[serde(default)]
    pub hide_marker_traits: bool,
    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
    #[clap(long)]
    #[serde(default)]
    pub hide_allocator: bool,
    /// Don't translate doc comments.
    #[clap(long)]
    #[serde(default)]
    pub no_doc_comments: bool,

    /// Remove trait clauses that aren't ultimately used anywhere. This is potentially incorrect as
    /// sometimes the mere presence of a trait clause is used to justify an operation, e.g. copying
    /// `Copy` data using `unsafe`.
    #[clap(long)]
    #[serde(default)]
    pub remove_unused_clauses: bool,
    /// Trait method default bodies take a `Self: Trait` clause as parameter, so that they can be
    /// reused by multiple trait impls. This however causes trait definitions to be mutually
    /// recursive with their default methods. This flag removes `Self` clauses that aren't used to
    /// break this mutual recursion when possible.
    #[clap(long)]
    #[serde(default)]
    pub remove_unused_self_clauses: bool,
    /// Remove trait clauses from type declarations. Best combined with `--lift-associated-types`
    /// for type declarations that use trait associated types in their fields.
    #[clap(long)]
    #[serde(default)]
    pub remove_adt_clauses: bool,

    /// Transform precise drops to the equivalent `drop_glue(&mut p)` call.
    #[clap(long)]
    #[serde(default)]
    pub desugar_drops: bool,
    /// Reconstruct conditional drops from the drop-flags and precise drops introduced by rustc's
    /// drop elaboration, when possible. This may leave drop flags if we couldn't identify a known
    /// pattern.
    #[clap(long)]
    #[serde(default)]
    pub resugar_drops: bool,
    /// Detect the drop flags inserted by rustc, which are booleans that track initialedness of a place.
    #[clap(long)]
    #[serde(default)]
    pub detect_drop_flags: bool,
    /// Transform array-to-slice unsizing and repeat expressions into standard library function
    /// calls in LLBC.
    #[clap(long)]
    #[serde(default)]
    pub ops_to_function_calls: bool,
    /// Transform array/slice indexing into standard library function calls in LLBC. Note that this may
    /// introduce UB since it creates references that were not normally created, including when
    /// indexing behind a raw pointer.
    #[clap(long)]
    #[serde(default)]
    pub index_to_function_calls: bool,
    /// Treat `Box<T>` as if it was a built-in type.
    #[clap(long)]
    #[serde(default)]
    pub treat_box_as_builtin: bool,
    /// Don't generate a type declaration per tuple arity. Instead, every tuple type refers to the
    /// single opaque declaration with id `TypeDeclId::UNIT`, and stores its field types in its
    /// generic arguments. This is meant for consumers that build tuples of arbitrary arity on the
    /// fly and don't care about their declaration. Note that this makes tuple types ill-typed with
    /// respect to their declaration; it is also incompatible with `--monomorphize`.
    #[clap(long)]
    #[serde(default)]
    pub no_gen_tuple_structs: bool,
    /// Do not inline or evaluate constants.
    #[clap(long)]
    #[serde(default)]
    pub raw_consts: bool,
    /// Inline anonymous constants, including promoted constants and inline const blocks. This is
    /// unsound for promoted constants if they're used with a `'static` lifetime, as this will move
    /// the constant to a local variable.
    #[clap(long)]
    #[serde(default)]
    pub inline_anon_consts: bool,
    /// How to represent constants and statics: as a call to their initializer function, as an
    /// evaluated value, or as raw bytes. This is always best-effort: in some cases we only get the
    /// evaluated constant, and in others we cannot evaluate the constant and keep the initializer.
    #[clap(long)]
    #[serde(default)]
    pub consts: Option<ConstHandling>,
    /// Replace "bound checks followed by UB-on-overflow operation" with the corresponding
    /// panic-on-overflow operation. This loses unwinding information.
    #[clap(long)]
    #[serde(default)]
    pub reconstruct_fallible_operations: bool,
    /// Replace calls to built-in panic functions with a `Panic` terminator.
    #[clap(long)]
    #[serde(default)]
    pub reconstruct_panic_calls: bool,
    /// Replace `if x { panic() }` with `assert(x)`.
    #[clap(long)]
    #[serde(default)]
    pub reconstruct_asserts: bool,
    /// Recombine a `read_discriminant(place)` followed by a `switch` into a single operation that
    /// uses enum variants instead of their discriminants.
    #[clap(long)]
    #[serde(default)]
    pub reconstruct_matches: bool,
    /// Ensure all local deallocations are made explicit with `StorageDead` statements. If this flag is not passed,
    /// every non-return local is implicitly deallocated on function return.
    /// Note this can add a lot of statements (quadratically-many, because of unwind paths).
    #[clap(long)]
    #[serde(default)]
    pub deallocate_all_locals: bool,
    /// Use `DeBruijnVar::Free` for the variables bound in item signatures, instead of
    /// `DeBruijnVar::Bound` everywhere. This simplifies the management of generics for projects
    /// that don't intend to manipulate them too much.
    #[clap(long)]
    #[serde(default)]
    pub unbind_item_vars: bool,

    /// Pretty-print the ULLBC immediately after extraction from MIR.
    #[clap(long)]
    #[serde(default)]
    pub print_original_ullbc: bool,
    /// Pretty-print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction).
    #[clap(long)]
    #[serde(default)]
    pub print_ullbc: bool,
    /// Pretty-print the LLBC just after we built it (i.e., immediately after loop reconstruction).
    #[clap(long)]
    #[serde(default)]
    pub print_built_llbc: bool,
    /// Pretty-print the final LLBC (after all the cleaning micro-passes).
    #[clap(long)]
    #[serde(default)]
    pub print_llbc: bool,
    /// When pretty-printing, also print the layout of every type declaration.
    #[clap(long)]
    #[serde(default)]
    pub print_layouts: bool,
    /// When pretty-printing, add comments that indicate which items and statements are unsafe.
    #[clap(long)]
    #[serde(default)]
    pub print_safety: bool,
    /// The destination directory. Files will be generated as
    /// `<dest_dir>/<crate_name>.{u}llbc` for json and `<dest_dir>/<crate_name>.{u}llbc.postcard`
    /// for postcard, unless `dest_file` is set. `dest_dir` defaults to the current directory.
    #[clap(long = "dest", value_parser)]
    #[serde(default)]
    pub dest_dir: Option<PathBuf>,
    /// The destination file. By default this depends on `format` and `ullbc`. If this is set we
    /// ignore `dest_dir`. If used with `format=all`, will add an extension corresponding to the file format
    /// at the end of the provided file name.
    #[clap(long, value_parser)]
    #[serde(default)]
    pub dest_file: Option<PathBuf>,
    /// Don't deduplicate values (types, trait refs) in the .(u)llbc file. This makes the file easier to inspect.
    #[clap(long)]
    #[serde(default)]
    pub no_dedup_serialized_ast: bool,
    /// Serialization format for emitted files. Defaults to json.
    #[clap(long, value_enum)]
    #[serde(default)]
    pub format: Option<SerializationFormatArg>,
    /// Run the translated program with MiniRust.
    #[clap(long)]
    #[serde(default)]
    pub run_with_minirust: bool,
    /// Don't serialize the final (U)LLBC to a file.
    #[clap(long)]
    #[serde(default)]
    pub no_serialize: bool,
    /// If activated, this skips borrow-checking of the crate.
    #[clap(
        long = "skip-borrow-check",
        alias = "skip-borrowck",
        visible_alias = "no-borrow-check",
        alias = "no-borrowck"
    )]
    #[serde(default)]
    pub skip_borrowck: bool,
    /// Don't generate distinct `Region::Body` lifetimes inside function bodies; use `Region::Erased` instead.
    #[clap(long)]
    #[serde(default)]
    pub erase_body_lifetimes: bool,
    /// Skip the typecheck passes.
    #[clap(long)]
    #[serde(default)]
    pub no_typecheck: bool,
    /// Don't normalize associated types.
    #[clap(long)]
    #[serde(default)]
    pub no_normalize: bool,
    /// Don't compute a stable order for declarations.
    #[clap(long)]
    #[serde(default)]
    pub no_reorder_decls: bool,
    /// Don't compute type layout guarantees.
    #[clap(long)]
    #[serde(default)]
    pub no_compute_layout_guarantees: bool,
    /// Panic on the first error. This is useful for debugging.
    #[clap(long)]
    #[serde(default)]
    pub abort_on_error: bool,
    /// Consider any warnings to be errors.
    #[clap(long)]
    #[serde(default)]
    pub error_on_warnings: bool,

    /// Named builtin sets of options.
    #[clap(long)]
    #[arg(value_enum)]
    pub preset: Option<Preset>,
}

/// The MIR stage to use. This is only relevant for the current crate: for dependencies, only mir
/// optimized is available (or mir elaborated for consts).
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
#[derive(ValueEnum)]
#[derive(Serialize, Deserialize)]
pub enum MirLevel {
    /// The MIR just after MIR lowering.
    Built,
    /// The MIR after const promotion. This is the MIR used by the borrow-checker.
    Promoted,
    /// The MIR after drop elaboration. This is the first MIR to include all the runtime
    /// information.
    Elaborated,
    /// The MIR after optimizations. Charon disables all the optimizations it can, so this is
    /// sensibly the same MIR as the elaborated MIR.
    Optimized,
}

/// Presets to make it easier to tweak options without breaking dependent projects. Eventually we
/// should define semantically-meaningful presets instead of project-specific ones.
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
#[derive(ValueEnum)]
#[derive(Serialize, Deserialize)]
#[non_exhaustive]
pub enum Preset {
    /// The default translation used before May 2025. After that, many passes were made optional
    /// and disabled by default.
    OldDefaults,
    /// Emit the MIR as unmodified as possible. This is very imperfect for now, we should make more
    /// passes optional.
    RawMir,
    /// Skip as many optional transformations as possible.
    Fast,
    Aeneas,
    Eurydice,
    Soteria,
    Tests,
}

/// How to handle constants and statics.
#[derive(Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
#[derive(ValueEnum)]
#[derive(Serialize, Deserialize)]
pub enum ConstHandling {
    /// Keep consts as calls to their initializer with `ConstantExprKind::Call`, without attempting
    /// to do any const-evaluation. This is the default.
    #[default]
    Initializers,
    /// Try evaluating consts and statics to their final value. If evaluation fails, we fall back to the
    /// initializer call.
    Values,
    /// Try evaluating consts and statics to raw bytes, using `ConstantExprKind::RawMemory`. If
    /// evaluation fails, we fall back to the initializer call.
    Bytes,
}

#[derive(Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
#[derive(ValueEnum)]
#[derive(Serialize, Deserialize)]
pub enum MonomorphizeMut {
    /// Monomorphize any item instantiated with `&mut`.
    #[default]
    All,
    /// Monomorphize all non-typedecl items instantiated with `&mut`.
    ExceptTypes,
}

#[derive(Debug, Copy, Clone, PartialEq, Eq)]
#[derive(ValueEnum)]
#[derive(Serialize, Deserialize)]
pub enum SerializationFormatArg {
    Json,
    Postcard,
    #[value(name = "minirust")]
    MiniRust,
    #[cfg_attr(feature = "charon_on_charon", charon::rename("AllFormats"))]
    All,
}

#[derive(Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
#[derive(ValueEnum)]
#[derive(Serialize, Deserialize)]
pub enum SerializationFormat {
    #[default]
    Json,
    Postcard,
    #[value(name = "minirust")]
    MiniRust,
}

impl SerializationFormatArg {
    pub fn as_format(self) -> Option<SerializationFormat> {
        match self {
            SerializationFormatArg::Json => Some(SerializationFormat::Json),
            SerializationFormatArg::Postcard => Some(SerializationFormat::Postcard),
            SerializationFormatArg::MiniRust => Some(SerializationFormat::MiniRust),
            SerializationFormatArg::All => None,
        }
    }
}

impl From<SerializationFormat> for SerializationFormatArg {
    fn from(format: SerializationFormat) -> SerializationFormatArg {
        match format {
            SerializationFormat::Json => SerializationFormatArg::Json,
            SerializationFormat::Postcard => SerializationFormatArg::Postcard,
            SerializationFormat::MiniRust => SerializationFormatArg::MiniRust,
        }
    }
}

impl SerializationFormat {
    pub fn output_extension(self, ullbc: bool) -> &'static str {
        match (ullbc, self) {
            (true, SerializationFormat::Json) => "ullbc",
            (false, SerializationFormat::Json) => "llbc",
            (true, SerializationFormat::Postcard) => "ullbc.postcard",
            (false, SerializationFormat::Postcard) => "llbc.postcard",
            (_, SerializationFormat::MiniRust) => "minirust.json",
        }
    }
}

impl CliOpts {
    pub fn apply_preset(&mut self) {
        if let Some(preset) = self.preset {
            match preset {
                Preset::OldDefaults => {
                    self.inline_anon_consts = true;
                    self.treat_box_as_builtin = true;
                    self.hide_allocator = true;
                    self.ops_to_function_calls = true;
                    self.index_to_function_calls = true;
                    self.reconstruct_fallible_operations = true;
                    self.reconstruct_asserts = true;
                    self.reconstruct_panic_calls = true;
                    self.reconstruct_matches = true;
                    self.unbind_item_vars = true;
                    self.duplicate_defaulted_methods = true;
                }
                Preset::RawMir => {
                    self.extract_opaque_bodies = true;
                    self.raw_consts = true;
                    self.ullbc = true;
                }
                Preset::Fast => {
                    self.ullbc = true;
                    self.no_typecheck = true;
                    self.no_normalize = true;
                    self.no_reorder_decls = true;
                    self.no_compute_layout_guarantees = true;
                    self.hide_marker_traits = true;
                    self.raw_consts = true;
                }
                Preset::Aeneas => {
                    self.lift_associated_types.push("*".to_owned());
                    self.treat_box_as_builtin = true;
                    self.ops_to_function_calls = true;
                    self.index_to_function_calls = true;
                    self.reconstruct_fallible_operations = true;
                    self.reconstruct_panic_calls = true;
                    self.reconstruct_asserts = true;
                    self.reconstruct_matches = true;
                    self.hide_marker_traits = true;
                    self.hide_allocator = true;
                    self.remove_unused_self_clauses = true;
                    self.remove_adt_clauses = true;
                    self.unbind_item_vars = true;
                    self.deallocate_all_locals = true;
                    self.no_gen_tuple_structs = true;
                }
                Preset::Eurydice => {
                    self.inline_anon_consts = true;
                    self.hide_allocator = true;
                    self.treat_box_as_builtin = true;
                    self.reconstruct_fallible_operations = true;
                    self.reconstruct_panic_calls = true;
                    self.reconstruct_asserts = true;
                    self.reconstruct_matches = true;
                    self.lift_associated_types.push("*".to_owned());
                    self.unbind_item_vars = true;
                    self.duplicate_defaulted_methods = true;
                    // Eurydice doesn't support opaque vtables it seems?
                    self.include.push("core::marker::MetaSized".to_owned());
                }
                Preset::Soteria => {
                    self.desugar_drops = true;
                    self.extract_opaque_bodies = true;
                    self.mir = Some(MirLevel::Elaborated);
                    self.reconstruct_fallible_operations = true;
                    self.reconstruct_asserts = true;
                    self.monomorphize = true;
                    self.no_normalize = true;
                    self.no_typecheck = true;
                    self.no_reorder_decls = true;
                    self.no_compute_layout_guarantees = true;
                    self.erase_body_lifetimes = true;
                    self.no_doc_comments = true;
                    self.precise_drops = true;
                    self.consts = Some(ConstHandling::Values);
                    self.ullbc = true;
                }
                Preset::Tests => {
                    self.inline_anon_consts = true;
                    self.no_dedup_serialized_ast = true; // Helps debug
                    self.treat_box_as_builtin = true;
                    self.hide_allocator = true;
                    self.reconstruct_fallible_operations = true;
                    self.reconstruct_panic_calls = true;
                    self.reconstruct_asserts = true;
                    self.reconstruct_matches = true;
                    if !self.desugar_drops {
                        self.resugar_drops = true;
                    }
                    if !self.monomorphize {
                        self.ops_to_function_calls = true;
                        self.index_to_function_calls = true;
                    }
                    self.duplicate_defaulted_methods = true;
                    self.deallocate_all_locals = true;
                    self.rustc_args.push("--edition=2021".to_owned());
                    self.rustc_args
                        .push("-Zcrate-attr=feature(register_tool)".to_owned());
                    self.rustc_args
                        .push("-Zcrate-attr=register_tool(charon)".to_owned());
                    self.exclude.push("core::fmt".to_owned());
                    if self.extract_opaque_bodies {
                        self.exclude
                            .extend(["core::array".to_owned(), "core::slice::index".to_owned()]);
                    }
                }
            }
        }

        if self.run_with_minirust || matches!(self.format, Some(SerializationFormatArg::MiniRust)) {
            self.monomorphize = true;
            self.ullbc = true;
            self.precise_drops = true;
            self.desugar_drops = true;
            self.deallocate_all_locals = true;
            self.treat_box_as_builtin = true;
            self.extract_opaque_bodies = true;
            self.consts = Some(ConstHandling::Bytes);
            self.mir = Some(
                self.mir
                    .unwrap_or(MirLevel::Elaborated)
                    .max(MirLevel::Elaborated),
            );
        }
    }

    /// Check that the options are meaningful
    pub fn validate(&self) -> anyhow::Result<()> {
        if self.dest_dir.is_some() {
            display_unspanned_error(
                Level::WARNING,
                "`--dest` is deprecated, use `--dest-file` instead",
            )
        }

        if self.remove_adt_clauses && self.lift_associated_types.is_empty() {
            anyhow::bail!(
                "`--remove-adt-clauses` should be used with `--lift-associated-types='*'` \
                to avoid missing clause errors",
            )
        }
        if matches!(self.monomorphize_mut, Some(MonomorphizeMut::ExceptTypes))
            && !self.remove_adt_clauses
        {
            anyhow::bail!(
                "`--monomorphize-mut=except-types` should be used with `--remove-adt-clauses` \
                to avoid generics mismatches"
            )
        }
        if self.no_gen_tuple_structs && self.monomorphize {
            anyhow::bail!(
                "`--no-gen-tuple-structs` is not compatible with `--monomorphize`, as \
                monomorphization requires each tuple to have its own type declaration"
            )
        }
        if self.monomorphize && (self.ops_to_function_calls || self.index_to_function_calls) {
            anyhow::bail!(
                "`--monomorphize` is not compatible with `--ops-to-function-calls` or \
                  `--index-to-function-calls`"
            )
        }
        if self.no_serialize && self.format.is_some() {
            anyhow::bail!(
                "`--no-serialize` is not compatible with `--format`, the format is only relevant if we serialize"
            );
        }
        if self.run_with_minirust || matches!(self.format, Some(SerializationFormatArg::MiniRust)) {
            if !cfg!(feature = "minirust") {
                anyhow::bail!(
                    "MiniRust output is unavailable because Charon was built without the `minirust` feature"
                );
            }
            if !self.targets.is_empty() {
                anyhow::bail!("MiniRust output does not support multi-target translation");
            }
        }
        if self.resugar_drops && self.desugar_drops {
            anyhow::bail!("`--desugar-drops` and `--resugar-drops` are mutually incompatible")
        }
        Ok(())
    }

    fn target_filename(
        &self,
        path_base: PathBuf,
        format: SerializationFormat,
    ) -> (PathBuf, SerializationFormat) {
        let extension = format.output_extension(self.ullbc);
        let target_filename = path_base.with_added_extension(extension);
        (target_filename, format)
    }

    pub fn targets(&self, crate_name: &str) -> Vec<(PathBuf, SerializationFormat)> {
        if self.no_serialize {
            return vec![];
        }

        let format = self.format.unwrap_or(SerializationFormatArg::Json);
        let mut path_base = self.dest_dir.clone().unwrap_or_default();
        path_base.push(crate_name);

        match format.as_format() {
            Some(format) => match self.dest_file.clone() {
                Some(dest) => vec![(dest, format)],
                None => vec![self.target_filename(path_base, format)],
            },
            None => {
                let path_base = self.dest_file.clone().unwrap_or(path_base);
                vec![
                    self.target_filename(path_base.clone(), SerializationFormat::Json),
                    self.target_filename(path_base, SerializationFormat::Postcard),
                ]
            }
        }
    }
}

/// Predicates that determine wihch items to use as starting point for translation.
#[derive(Debug, Clone, EnumAsInner)]
pub enum StartFrom {
    /// Item identified by a pattern/path. If strict is true, then failing to
    /// find an item matching the pattern is an error; otherwise, we just ignore this pattern.
    Pattern { pattern: NamePattern, strict: bool },
    /// Item annotated with the given attribute.
    Attribute(String),
    /// Item marked `pub`. Note that this does not take accessibility into account; a
    /// non-reexported `pub` item will be included here.
    Pub,
    /// The global constructors of the target.
    GlobalCtors,
}

/// The options that control translation and transformation.
pub struct TranslateOptions {
    /// Items from which to start translation.
    pub start_from: Vec<StartFrom>,
    /// The level at which to extract the MIR
    pub mir_level: MirLevel,
    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
    /// them all.
    pub translate_all_methods: bool,
    /// Translate the vtable of every trait impl, not just those used in an unsizing coercion.
    pub eager_vtables: bool,
    /// Duplicate trait default methods into impls that use them.
    pub duplicate_defaulted_methods: bool,
    /// If `Some(_)`, run the partial mutability monomorphization pass. The contained enum
    /// indicates whether to partially monomorphize types.
    pub monomorphize_mut: Option<MonomorphizeMut>,
    /// Whether to hide various marker traits such as `*Sized` and `Destruct` anywhere they show
    /// up.
    pub hide_marker_traits: bool,
    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
    pub hide_allocator: bool,
    /// Don't translate doc comments.
    pub no_doc_comments: bool,
    /// List of traits to remove any mentions of. Influenced by `hide_marker_traits`,
    /// `hide_allocator`, and `precise_drops`.
    pub hide_traits: Vec<NamePattern>,
    /// Remove trait clauses that aren't ultimately used anywhere. This is potentially incorrect as
    /// sometimes the mere presence of a trait clause is used to justify an operation, e.g. copying
    /// `Copy` data using `unsafe`.
    pub remove_unused_clauses: bool,
    /// Remove unused `Self: Trait` clauses on method declarations.
    pub remove_unused_self_clauses: bool,
    /// Remove trait clauses attached to type declarations.
    pub remove_adt_clauses: bool,
    /// Monomorphize code using hax's instantiation mechanism.
    pub monomorphize_with_hax: bool,
    /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow)
    pub ullbc: bool,
    /// Reconstruct the control-flow by breaking forward out of enclosing loops instead of
    /// duplicating the blocks reachable from several branches.
    pub no_code_duplication: bool,
    /// Transform array-to-slice unsizing and repeat expressions into standard library function
    /// calls in LLBC.
    pub ops_to_function_calls: bool,
    /// Transform array/slice indexing into standard library function calls in LLBC.
    pub index_to_function_calls: bool,
    /// Print the llbc just after control-flow reconstruction.
    pub print_built_llbc: bool,
    /// Treat `Box<T>` as if it was a built-in type.
    pub treat_box_as_builtin: bool,
    /// Make all tuples refer to the single opaque `TypeDeclId::UNIT` declaration, and store their
    /// field types in their generic arguments.
    pub no_gen_tuple_structs: bool,
    /// Don't inline or evaluate constants.
    pub raw_consts: bool,
    /// Inline anonymous constants.
    pub inline_anon_consts: bool,
    /// How much to evaluate constants and statics.
    pub consts: ConstHandling,
    /// Replace "bound checks followed by UB-on-overflow operation" with the corresponding
    /// panic-on-overflow operation. This loses unwinding information.
    pub reconstruct_fallible_operations: bool,
    /// Replace calls to built-in panic functions with a `Panic` terminator.
    pub reconstruct_panic_calls: bool,
    /// Replace `if x { panic() }` with `assert(x)`.
    pub reconstruct_asserts: bool,
    /// Reconstruct matches on enum variants.
    pub reconstruct_matches: bool,
    /// Insert the `StorageDead`s that MIR omits for some locals.
    pub deallocate_all_locals: bool,
    // Use `DeBruijnVar::Free` for the variables bound in item signatures.
    pub unbind_item_vars: bool,
    /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
    /// field.
    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
    /// List of traits for which we transform associated types to type parameters.
    pub lift_associated_types: Vec<NamePattern>,
    /// Use `Region::Erased` instead of fresh `Region::Body` lifetimes inside function bodies.
    pub erase_body_lifetimes: bool,
    /// Skip the typecheck passes.
    pub no_typecheck: bool,
    /// Don't normalize associated types.
    pub no_normalize: bool,
    /// Don't reorder declarations and compute recursive declaration groups.
    pub no_reorder_decls: bool,
    /// Don't compute type layout guarantees.
    pub no_compute_layout_guarantees: bool,
    /// Transform Drop to Call drop_glue
    pub desugar_drops: bool,
    /// Reconstruct conditional drops from rustc drop flags.
    pub resugar_drops: bool,
    /// Detect rustc drop flags.
    pub detect_drop_flags: bool,
    /// Add `Destruct` bounds to all generic params.
    pub add_destruct_bounds: bool,
}

impl TranslateOptions {
    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
        let mut parse_pattern = |s: &str| -> Result<_, Error> {
            match NamePattern::parse(s) {
                Ok(p) => Ok(p),
                Err(e) => raise_error!(error_ctx, no_crate, "failed to parse pattern `{s}` ({e})"),
            }
        };

        let mut mir_level = options.mir.unwrap_or(MirLevel::Promoted);
        if options.precise_drops {
            mir_level = std::cmp::max(mir_level, MirLevel::Elaborated);
        }

        let mut start_from = options
            .start_from
            .iter()
            .filter_map(|path| parse_pattern(path).ok())
            .map(|p| StartFrom::Pattern {
                pattern: p,
                strict: true,
            })
            .collect_vec();
        start_from.extend(
            options
                .start_from_if_exists
                .iter()
                .filter_map(|path| parse_pattern(path).ok())
                .map(|p| StartFrom::Pattern {
                    pattern: p,
                    strict: false,
                }),
        );
        for attr in options.start_from_attribute.iter().cloned() {
            start_from.push(StartFrom::Attribute(attr));
        }
        if options.start_from_pub {
            start_from.push(StartFrom::Pub);
        }
        if options.start_from_global_ctors {
            start_from.push(StartFrom::GlobalCtors);
        }
        if start_from.is_empty() {
            start_from.push(StartFrom::Pattern {
                pattern: parse_pattern("crate").unwrap(),
                strict: true,
            });
        }

        let hide_traits = options
            .hide_marker_traits
            .then_some([
                "core::marker::Sized",
                "core::marker::MetaSized",
                "core::marker::PointeeSized",
                "core::marker::Tuple",
                "core::clone::TrivialClone",
            ])
            .into_iter()
            .flatten()
            .chain(options.hide_allocator.then_some("core::alloc::Allocator"))
            .filter_map(|s| parse_pattern(s).ok())
            .collect_vec();

        let item_opacities = {
            use ItemOpacity::*;
            let mut opacities = vec![];

            // This is how to treat items that don't match any other pattern.
            if options.extract_opaque_bodies {
                opacities.push(("_".to_string(), Transparent));
            } else {
                opacities.push(("_".to_string(), Foreign));
            }

            if options.treat_box_as_builtin {
                // Include this item's body, we inline it in a pass.
                opacities.push((
                    "alloc::boxed::box_assume_init_into_vec_unsafe".to_string(),
                    Transparent,
                ));
            }

            // We always include the items from the crate.
            opacities.push(("crate".to_owned(), Transparent));

            for pat in options.include.iter() {
                opacities.push((pat.to_string(), Transparent));
            }
            for pat in options.opaque.iter() {
                opacities.push((pat.to_string(), Opaque));
            }
            if options.run_with_minirust
                || matches!(options.format, Some(SerializationFormatArg::MiniRust))
            {
                // This is the `intrinsics` crate used by MiniRust's `minimize` test suite. We make
                // it opaque because we replace the function bodies so we don't need to translate
                // them.
                opacities.push(("intrinsics".to_owned(), Opaque));
                // The MiniRust translation models this as a plain unwind.
                opacities.push(("core::panicking::panic_fmt".to_owned(), Opaque));
            }
            for pat in options.exclude.iter() {
                opacities.push((pat.to_string(), Invisible));
            }

            for trait_name in &hide_traits {
                opacities.push((trait_name.to_string(), Invisible));
            }

            // Hide trait impls and defs for the excluded traits.
            let hide_traits = hide_traits
                .iter()
                .cloned()
                .flat_map(|pat| [pat.clone(), NamePattern::impl_for(pat)])
                .map(|pat| (pat, Invisible));
            opacities
                .into_iter()
                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
                .chain(hide_traits)
                .collect()
        };

        let lift_associated_types = options
            .lift_associated_types
            .iter()
            .filter_map(|s| parse_pattern(s).ok())
            .collect();

        TranslateOptions {
            start_from,
            mir_level,
            monomorphize_mut: options.monomorphize_mut,
            hide_marker_traits: options.hide_marker_traits,
            hide_allocator: options.hide_allocator,
            no_doc_comments: options.no_doc_comments,
            hide_traits,
            remove_unused_clauses: options.remove_unused_clauses,
            remove_unused_self_clauses: options.remove_unused_self_clauses,
            remove_adt_clauses: options.remove_adt_clauses,
            monomorphize_with_hax: options.monomorphize,
            ullbc: options.ullbc,
            no_code_duplication: options.no_code_duplication,
            ops_to_function_calls: options.ops_to_function_calls,
            index_to_function_calls: options.index_to_function_calls,
            print_built_llbc: options.print_built_llbc,
            item_opacities,
            treat_box_as_builtin: options.treat_box_as_builtin,
            no_gen_tuple_structs: options.no_gen_tuple_structs,
            raw_consts: options.raw_consts,
            inline_anon_consts: options.inline_anon_consts,
            consts: options.consts.unwrap_or_default(),
            reconstruct_fallible_operations: options.reconstruct_fallible_operations,
            reconstruct_panic_calls: options.reconstruct_panic_calls,
            reconstruct_asserts: options.reconstruct_asserts,
            reconstruct_matches: options.reconstruct_matches,
            deallocate_all_locals: options.deallocate_all_locals,
            lift_associated_types,
            unbind_item_vars: options.unbind_item_vars,
            translate_all_methods: options.translate_all_methods,
            eager_vtables: options.eager_vtables,
            duplicate_defaulted_methods: options.duplicate_defaulted_methods,
            erase_body_lifetimes: options.erase_body_lifetimes,
            no_typecheck: options.no_typecheck,
            no_normalize: options.no_normalize,
            no_reorder_decls: options.no_reorder_decls,
            no_compute_layout_guarantees: options.no_compute_layout_guarantees,
            desugar_drops: options.desugar_drops,
            resugar_drops: options.resugar_drops,
            detect_drop_flags: options.detect_drop_flags,
            add_destruct_bounds: options.precise_drops,
        }
    }

    /// Find the opacity requested for the given name. This does not take into account
    /// `#[charon::opaque]` annotations, only cli parameters.
    #[tracing::instrument(skip(self, krate), ret)]
    pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
        // Builtin names (str, tuples) are always transparent.
        if name.is_builtin() {
            return ItemOpacity::Transparent;
        }
        // Find the most precise pattern that matches this name. There is always one since
        // the list contains the `_` pattern. If there are conflicting settings for this item, we
        // err on the side of being more opaque.
        let (_, opacity) = self
            .item_opacities
            .iter()
            .filter(|(pat, _)| pat.matches(krate, name))
            .max()
            .unwrap();
        *opacity
    }
}