charon_lib/

options.rs

//! The options that control charon behavior.
use annotate_snippets::Level;
use clap::ValueEnum;
use indoc::indoc;
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";

// 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, clap::Args, PartialEq, Eq, Serialize, Deserialize)]
#[clap(name = "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,
    /// Whether to precisely translate drops and drop-related code. For this, we add explicit
    /// `Destruct` bounds to all generic parameters, set the MIR level to at least `elaborated`,
    /// and attempt to retrieve drop glue for all types.
    ///
    /// This option is known to cause panics inside rustc, because their drop handling is not
    /// design to work on polymorphic types. To silence the warning, pass appropriate `--opaque
    /// '{impl core::marker::Destruct for some::Type}'` options.
    ///
    /// 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,
    /// If activated, this skips borrow-checking of the crate.
    #[clap(long)]
    #[serde(default)]
    pub skip_borrowck: bool,
    /// The MIR stage to extract. This is only relevant for the current crate; for dpendencies 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>,
    /// 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>,
    /// 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)]
    #[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,

    /// Transforma 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)]
    #[serde(default)]
    pub remove_associated_types: Vec<String>,
    /// Whether to hide various marker traits such as `Sized`, `Sync`, `Send` and `Destruct`
    /// anywhere they show up. This can considerably speed up translation.
    #[clap(long)]
    #[serde(default)]
    pub hide_marker_traits: bool,
    /// Remove trait clauses from type declarations. Must be combined with
    /// `--remove-associated-types` for type declarations that use trait associated types in their
    /// fields, otherwise this will result in errors.
    #[clap(long)]
    #[serde(default)]
    pub remove_adt_clauses: bool,
    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
    #[clap(long)]
    #[serde(default)]
    pub hide_allocator: bool,
    /// Trait method declarations 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 method declarations. 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,

    /// Transform precise drops to the equivalent `drop_in_place(&raw mut p)` call.
    #[clap(long)]
    #[serde(default)]
    pub desugar_drops: bool,
    /// Transform array-to-slice unsizing, repeat expressions, and raw pointer construction into
    /// builtin functions in ULLBC.
    #[clap(long)]
    #[serde(default)]
    pub ops_to_function_calls: bool,
    /// Transform array/slice indexing into builtin functions in ULLBC. 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,
    /// Do not inline or evaluate constants. Note: this emits constants that the OCaml bindings
    /// can't parse; if you need this ping me so I can fix that.
    #[clap(long)]
    #[serde(default)]
    pub raw_consts: bool,
    /// 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 "if x { panic() }" with "assert(x)".
    #[clap(long)]
    #[serde(default)]
    pub reconstruct_asserts: 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,

    /// The destination directory. Files will be generated as `<dest_dir>/<crate_name>.{u}llbc`,
    /// 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 `<dest_dir>/<crate_name>.llbc`. If this is set we ignore
    /// `dest_dir`.
    #[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,
    /// Don't serialize the final (U)LLBC to a file.
    #[clap(long)]
    #[serde(default)]
    pub no_serialize: 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, ValueEnum, 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, ValueEnum, 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,
    Aeneas,
    Eurydice,
    Soteria,
    Tests,
}

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

impl CliOpts {
    pub fn apply_preset(&mut self) {
        if let Some(preset) = self.preset {
            match preset {
                Preset::OldDefaults => {
                    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.unbind_item_vars = true;
                }
                Preset::RawMir => {
                    self.extract_opaque_bodies = true;
                    self.raw_consts = true;
                    self.ullbc = true;
                }
                Preset::Aeneas => {
                    self.remove_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_asserts = true;
                    self.hide_marker_traits = true;
                    self.hide_allocator = true;
                    self.remove_unused_self_clauses = true;
                    self.unbind_item_vars = true;
                    // Hide drop impls because they often involve nested borrows. which aeneas
                    // doesn't handle yet.
                    self.exclude.push("core::ops::drop::Drop".to_owned());
                    self.exclude
                        .push("{impl core::ops::drop::Drop for _}".to_owned());
                }
                Preset::Eurydice => {
                    self.hide_allocator = true;
                    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_asserts = true;
                    self.remove_associated_types.push("*".to_owned());
                    self.unbind_item_vars = true;
                    // Eurydice doesn't support opaque vtables it seems?
                    self.include.push("core::marker::MetaSized".to_owned());
                }
                Preset::Soteria => {
                    self.extract_opaque_bodies = true;
                    self.monomorphize = true;
                    self.mir = Some(MirLevel::Elaborated);
                    self.ullbc = true;
                }
                Preset::Tests => {
                    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_asserts = true;
                    self.ops_to_function_calls = true;
                    self.index_to_function_calls = 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::Formatter".to_owned());
                }
            }
        }
    }

    /// 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.remove_associated_types.is_empty() {
            anyhow::bail!(
                "`--remove-adt-clauses` should be used with `--remove-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"
            )
        }
        Ok(())
    }
}

/// The options that control translation and transformation.
pub struct TranslateOptions {
    /// 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,
    /// 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`, `Sync`, `Send` and `Destruct`
    /// anywhere they show up.
    pub hide_marker_traits: bool,
    /// Remove trait clauses attached to type declarations.
    pub remove_adt_clauses: bool,
    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
    pub hide_allocator: bool,
    /// Remove unused `Self: Trait` clauses on method declarations.
    pub remove_unused_self_clauses: bool,
    /// Monomorphize code using hax's instantiation mechanism.
    pub monomorphize_with_hax: bool,
    /// Transform array-to-slice unsizing, repeat expressions, and raw pointer construction into
    /// builtin functions in ULLBC.
    pub ops_to_function_calls: bool,
    /// Transform array/slice indexing into builtin functions in ULLBC.
    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,
    /// Don't inline or evaluate constants.
    pub raw_consts: bool,
    /// 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 "if x { panic() }" with "assert(x)".
    pub reconstruct_asserts: 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 remove_associated_types: Vec<NamePattern>,
    /// Transform Drop to Call drop_in_place
    pub desugar_drops: bool,
    /// Add `Destruct` bounds to all generic params.
    pub add_destruct_bounds: bool,
    /// Translate drop glue for poly types, knowing that this may cause ICEs.
    pub translate_poly_drop_glue: bool,
}

impl TranslateOptions {
    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
        let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
            Ok(p) => Ok(p),
            Err(e) => {
                raise_error!(
                    error_ctx,
                    crate(&TranslatedCrate::default()),
                    Span::dummy(),
                    "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 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));
            }

            // 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));
            }
            for pat in options.exclude.iter() {
                opacities.push((pat.to_string(), Invisible));
            }

            if options.hide_allocator {
                opacities.push((format!("core::alloc::Allocator"), Invisible));
                opacities.push((
                    format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
                    Invisible,
                ));
            }

            opacities
                .into_iter()
                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
                .collect()
        };

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

        TranslateOptions {
            mir_level,
            monomorphize_mut: options.monomorphize_mut,
            hide_marker_traits: options.hide_marker_traits,
            remove_adt_clauses: options.remove_adt_clauses,
            hide_allocator: options.hide_allocator,
            remove_unused_self_clauses: options.remove_unused_self_clauses,
            monomorphize_with_hax: options.monomorphize,
            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,
            raw_consts: options.raw_consts,
            reconstruct_fallible_operations: options.reconstruct_fallible_operations,
            reconstruct_asserts: options.reconstruct_asserts,
            remove_associated_types,
            unbind_item_vars: options.unbind_item_vars,
            translate_all_methods: options.translate_all_methods,
            desugar_drops: options.desugar_drops,
            add_destruct_bounds: options.precise_drops,
            translate_poly_drop_glue: 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 {
        // 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
    }
}