charon_lib/
options.rs

1//! The options that control charon behavior.
2use annotate_snippets::Level;
3use clap::ValueEnum;
4use indoc::indoc;
5use serde::{Deserialize, Serialize};
6use std::path::PathBuf;
7
8use crate::{
9    ast::*,
10    errors::{ErrorCtx, display_unspanned_error},
11    name_matcher::NamePattern,
12    raise_error, register_error,
13};
14
15/// The name of the environment variable we use to save the serialized Cli options
16/// when calling charon-driver from cargo-charon.
17pub const CHARON_ARGS: &str = "CHARON_ARGS";
18
19// This structure is used to store the command-line instructions.
20// We automatically derive a command-line parser based on this structure.
21// Note that the doc comments are used to generate the help message when using
22// `--help`.
23//
24// Note that because we need to transmit the options to the charon driver,
25// we store them in a file before calling this driver (hence the `Serialize`,
26// `Deserialize` options).
27#[derive(Debug, Default, Clone, clap::Args, PartialEq, Eq, Serialize, Deserialize)]
28#[clap(name = "Charon")]
29#[charon::rename("cli_options")]
30pub struct CliOpts {
31    /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow)
32    #[clap(long = "ullbc")]
33    #[serde(default)]
34    pub ullbc: bool,
35    /// Compile the package's library
36    #[clap(long = "lib")]
37    #[serde(default)]
38    pub lib: bool,
39    /// Compile the specified binary
40    #[clap(long = "bin")]
41    #[serde(default)]
42    pub bin: Option<String>,
43    /// Deprecated: use `--mir promoted` instead.
44    #[clap(long = "mir_promoted")]
45    #[serde(default)]
46    pub mir_promoted: bool,
47    /// Deprecated: use `--mir optimized` instead.
48    #[clap(long = "mir_optimized")]
49    #[serde(default)]
50    pub mir_optimized: bool,
51    /// The MIR stage to extract. This is only relevant for the current crate; for dpendencies only
52    /// MIR optimized is available.
53    #[arg(long)]
54    pub mir: Option<MirLevel>,
55    /// The input file (the entry point of the crate to extract).
56    /// This is needed if you want to define a custom entry point (to only
57    /// extract part of a crate for instance).
58    #[clap(long = "input", value_parser)]
59    #[serde(default)]
60    pub input_file: Option<PathBuf>,
61    /// Read an llbc file and pretty-print it. This is a terrible API, we should use subcommands.
62    #[clap(long = "read-llbc", value_parser)]
63    #[serde(default)]
64    pub read_llbc: Option<PathBuf>,
65    /// The destination directory. Files will be generated as `<dest_dir>/<crate_name>.{u}llbc`,
66    /// unless `dest_file` is set. `dest_dir` defaults to the current directory.
67    #[clap(long = "dest", value_parser)]
68    #[serde(default)]
69    pub dest_dir: Option<PathBuf>,
70    /// The destination file. By default `<dest_dir>/<crate_name>.llbc`. If this is set we ignore
71    /// `dest_dir`.
72    #[clap(long = "dest-file", value_parser)]
73    #[serde(default)]
74    pub dest_file: Option<PathBuf>,
75    /// If activated, use Polonius' non-lexical lifetimes (NLL) analysis.
76    /// Otherwise, use the standard borrow checker.
77    #[clap(long = "polonius")]
78    #[serde(default)]
79    pub use_polonius: bool,
80    /// If activated, this skips borrow-checking of the crate.
81    #[clap(long = "skip-borrowck")]
82    #[serde(default)]
83    pub skip_borrowck: bool,
84    /// Monomorphize the items encountered when possible. Generic items found in the crate are
85    /// skipped. To only translate a particular call graph, use `--start-from`. Note: this doesn't
86    /// currently support `dyn Trait`.
87    #[clap(long, visible_alias = "mono")]
88    #[serde(default)]
89    pub monomorphize: bool,
90    /// Partially monomorphize items to make it so that no item is ever monomorphized with a
91    /// mutable reference (or type containing one); said differently, so that the presence of
92    /// mutable references in a type is independent of its generics. This is used by Aeneas.
93    #[clap(
94        long,
95        value_name("INCLUDE_TYPES"),
96        num_args(0..=1),
97        require_equals(true),
98        default_missing_value("all"),
99    )]
100    #[serde(default)]
101    pub monomorphize_mut: Option<MonomorphizeMut>,
102    /// Usually we skip the bodies of foreign methods and structs with private fields. When this
103    /// flag is on, we don't.
104    #[clap(long = "extract-opaque-bodies")]
105    #[serde(default)]
106    pub extract_opaque_bodies: bool,
107    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
108    /// them all.
109    #[clap(long = "translate-all-methods")]
110    #[serde(default)]
111    pub translate_all_methods: bool,
112    /// Whitelist of items to translate. These use the name-matcher syntax.
113    #[clap(
114        long = "include",
115        help = indoc!("
116            Whitelist of items to translate. These use the name-matcher syntax (note: this differs
117            a bit from the ocaml NameMatcher).
118
119            Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
120            built-in type. It is also not possible to filter a trait impl (this will only filter
121            its methods). Please report bugs or missing features.
122
123            Examples:
124              - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
125                  submodules or trait methods);
126              - `crate::module1::module2::item::_`: refers only to the subitems of this item;
127              - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
128                  very useful impl;
129
130            When multiple patterns in the `--include` and `--opaque` options match the same item,
131            the most precise pattern wins. E.g.: `charon --opaque crate::module --include
132            crate::module::_` makes the `module` opaque (we won't explore its contents), but the
133            items in it transparent (we will translate them if we encounter them.)
134    "))]
135    #[serde(default)]
136    #[charon::rename("included")]
137    pub include: Vec<String>,
138    /// Blacklist of items to keep opaque. These use the name-matcher syntax.
139    #[clap(
140        long = "opaque",
141        help = "Blacklist of items to keep opaque. Works just like `--include`, see the doc there."
142    )]
143    #[serde(default)]
144    pub opaque: Vec<String>,
145    /// Blacklist of items to not translate at all. These use the name-matcher syntax.
146    #[clap(
147        long = "exclude",
148        help = "Blacklist of items to not translate at all. Works just like `--include`, see the doc there."
149    )]
150    #[serde(default)]
151    pub exclude: Vec<String>,
152    /// List of traits for which we transform associated types to type parameters.
153    #[clap(
154        long = "remove-associated-types",
155        help = "List of traits for which we transform associated types to type parameters. \
156        The syntax is like `--include`, see the doc there."
157    )]
158    #[serde(default)]
159    pub remove_associated_types: Vec<String>,
160    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
161    /// up.
162    #[clap(long = "hide-marker-traits")]
163    #[serde(default)]
164    pub hide_marker_traits: bool,
165    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
166    #[clap(long)]
167    #[serde(default)]
168    pub hide_allocator: bool,
169    /// Trait method declarations take a `Self: Trait` clause as parameter, so that they can be
170    /// reused by multiple trait impls. This however causes trait definitions to be mutually
171    /// recursive with their method declarations. This flag removes `Self` clauses that aren't used
172    /// to break this mutual recursion.
173    #[clap(long)]
174    #[serde(default)]
175    pub remove_unused_self_clauses: bool,
176    /// Whether to add `Drop` bounds everywhere to enable proper tracking of what code runs on a
177    /// given `drop` call.
178    #[clap(long)]
179    #[serde(default)]
180    pub add_drop_bounds: bool,
181    /// A list of item paths to use as starting points for the translation. We will translate these
182    /// items and any items they refer to, according to the opacity rules. When absent, we start
183    /// from the path `crate` (which translates the whole crate).
184    #[clap(long = "start-from")]
185    #[serde(default)]
186    pub start_from: Vec<String>,
187    /// Do not run cargo; instead, run the driver directly.
188    #[clap(long = "no-cargo")]
189    #[serde(default)]
190    pub no_cargo: bool,
191    /// Extra flags to pass to rustc.
192    #[clap(long = "rustc-flag", alias = "rustc-arg")]
193    #[serde(default)]
194    pub rustc_args: Vec<String>,
195    /// Extra flags to pass to cargo. Incompatible with `--no-cargo`.
196    #[clap(long = "cargo-arg")]
197    #[serde(default)]
198    pub cargo_args: Vec<String>,
199    /// Panic on the first error. This is useful for debugging.
200    #[clap(long = "abort-on-error")]
201    #[serde(default)]
202    pub abort_on_error: bool,
203    /// Print the errors as warnings
204    #[clap(long = "error-on-warnings", help = "Consider any warnings as errors")]
205    #[serde(default)]
206    pub error_on_warnings: bool,
207    #[clap(
208        long = "no-serialize",
209        help = "Don't serialize the final (U)LLBC to a file."
210    )]
211    #[serde(default)]
212    pub no_serialize: bool,
213    #[clap(
214        long = "print-original-ullbc",
215        help = "Print the ULLBC immediately after extraction from MIR."
216    )]
217    #[serde(default)]
218    pub print_original_ullbc: bool,
219    #[clap(
220        long = "print-ullbc",
221        help = "Print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction)."
222    )]
223    #[serde(default)]
224    pub print_ullbc: bool,
225    #[clap(
226        long = "print-built-llbc",
227        help = "Print the LLBC just after we built it (i.e., immediately after loop reconstruction)."
228    )]
229    #[serde(default)]
230    pub print_built_llbc: bool,
231    #[clap(
232        long = "print-llbc",
233        help = "Print the final LLBC (after all the cleaning micro-passes)."
234    )]
235    #[serde(default)]
236    pub print_llbc: bool,
237    #[clap(
238        long = "no-merge-goto-chains",
239        help = "Do not merge the chains of gotos in the ULLBC control-flow graph."
240    )]
241    #[serde(default)]
242    pub no_merge_goto_chains: bool,
243
244    #[clap(
245        long = "no-ops-to-function-calls",
246        help = "Do not transform ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls for ULLBC"
247    )]
248    #[serde(default)]
249    pub no_ops_to_function_calls: bool,
250
251    #[clap(
252        long = "raw-boxes",
253        help = "Do not special-case the translation of `Box<T>` into a builtin ADT."
254    )]
255    #[serde(default)]
256    pub raw_boxes: bool,
257
258    /// Named builtin sets of options. Currently used only for dependent projects, eveentually
259    /// should be replaced with semantically-meaningful presets.
260    #[clap(long = "preset")]
261    #[arg(value_enum)]
262    pub preset: Option<Preset>,
263}
264
265/// The MIR stage to use. This is only relevant for the current crate: for dependencies, only mir
266/// optimized is available (or mir elaborated for consts).
267#[derive(
268    Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
269)]
270pub enum MirLevel {
271    /// The MIR just after MIR lowering.
272    #[default]
273    Built,
274    /// The MIR after const promotion. This is the MIR used by the borrow-checker.
275    Promoted,
276    /// The MIR after drop elaboration. This is the first MIR to include all the runtime
277    /// information.
278    Elaborated,
279    /// The MIR after optimizations. Charon disables all the optimizations it can, so this is
280    /// sensibly the same MIR as the elaborated MIR.
281    Optimized,
282}
283
284/// Presets to make it easier to tweak options without breaking dependent projects. Eventually we
285/// should define semantically-meaningful presets instead of project-specific ones.
286#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
287#[non_exhaustive]
288pub enum Preset {
289    /// The default translation used before May 2025. After that, many passes were made optional
290    /// and disabled by default.
291    OldDefaults,
292    Aeneas,
293    Eurydice,
294    Soteria,
295    Tests,
296}
297
298#[derive(
299    Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
300)]
301pub enum MonomorphizeMut {
302    /// Monomorphize any item instantiated with `&mut`.
303    #[default]
304    All,
305    /// Monomorphize all non-typedecl items instantiated with `&mut`.
306    ExceptTypes,
307}
308
309impl CliOpts {
310    pub fn apply_preset(&mut self) {
311        if let Some(preset) = self.preset {
312            match preset {
313                Preset::OldDefaults => {
314                    self.hide_allocator = !self.raw_boxes;
315                }
316                Preset::Aeneas => {
317                    self.remove_associated_types.push("*".to_owned());
318                    self.hide_marker_traits = true;
319                    self.hide_allocator = true;
320                    self.remove_unused_self_clauses = true;
321                    // Hide drop impls because they often involve nested borrows. which aeneas
322                    // doesn't handle yet.
323                    self.exclude.push("core::ops::drop::Drop".to_owned());
324                    self.exclude
325                        .push("{impl core::ops::drop::Drop for _}".to_owned());
326                }
327                Preset::Eurydice => {
328                    self.hide_allocator = true;
329                    self.remove_associated_types.push("*".to_owned());
330                }
331                Preset::Soteria => {
332                    self.extract_opaque_bodies = true;
333                    self.monomorphize = true;
334                    self.raw_boxes = true;
335                    self.mir = Some(MirLevel::Elaborated);
336                    self.ullbc = true;
337                }
338                Preset::Tests => {
339                    self.hide_allocator = !self.raw_boxes;
340                    self.rustc_args.push("--edition=2021".to_owned());
341                    self.rustc_args
342                        .push("-Zcrate-attr=feature(register_tool)".to_owned());
343                    self.rustc_args
344                        .push("-Zcrate-attr=register_tool(charon)".to_owned());
345                    self.exclude.push("core::fmt::Formatter".to_owned());
346                }
347            }
348        }
349    }
350
351    /// Check that the options are meaningful
352    pub fn validate(&self) {
353        assert!(
354            !self.lib || self.bin.is_none(),
355            "Can't use --lib and --bin at the same time"
356        );
357
358        assert!(
359            !self.mir_promoted || !self.mir_optimized,
360            "Can't use --mir_promoted and --mir_optimized at the same time"
361        );
362
363        if self.input_file.is_some() {
364            display_unspanned_error(
365                Level::WARNING,
366                "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
367            )
368        }
369        if self.no_cargo {
370            display_unspanned_error(
371                Level::WARNING,
372                "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
373            )
374        }
375        if self.read_llbc.is_some() {
376            display_unspanned_error(
377                Level::WARNING,
378                "`--read_llbc` is deprecated, use `charon pretty-print <input file>` instead",
379            )
380        }
381        if self.use_polonius {
382            display_unspanned_error(
383                Level::WARNING,
384                "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead",
385            )
386        }
387        if self.mir_optimized {
388            display_unspanned_error(
389                Level::WARNING,
390                "`--mir_optimized` is deprecated, use `--mir optimized` instead",
391            )
392        }
393        if self.mir_promoted {
394            display_unspanned_error(
395                Level::WARNING,
396                "`--mir_promoted` is deprecated, use `--mir promoted` instead",
397            )
398        }
399        if self.lib {
400            display_unspanned_error(
401                Level::WARNING,
402                "`--lib` is deprecated, use `charon cargo -- --lib` instead",
403            )
404        }
405        if self.bin.is_some() {
406            display_unspanned_error(
407                Level::WARNING,
408                "`--bin` is deprecated, use `charon cargo -- --bin <name>` instead",
409            )
410        }
411        if self.dest_dir.is_some() {
412            display_unspanned_error(
413                Level::WARNING,
414                "`--dest` is deprecated, use `--dest-file` instead",
415            )
416        }
417    }
418}
419
420/// The options that control translation and transformation.
421pub struct TranslateOptions {
422    /// The level at which to extract the MIR
423    pub mir_level: MirLevel,
424    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
425    /// them all.
426    pub translate_all_methods: bool,
427    /// If `Some(_)`, run the partial mutability monomorphization pass. The contained enum
428    /// indicates whether to partially monomorphize types.
429    pub monomorphize_mut: Option<MonomorphizeMut>,
430    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
431    /// up.
432    pub hide_marker_traits: bool,
433    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
434    pub hide_allocator: bool,
435    /// Remove unused `Self: Trait` clauses on method declarations.
436    pub remove_unused_self_clauses: bool,
437    /// Monomorphize code using hax's instantiation mechanism.
438    pub monomorphize_with_hax: bool,
439    /// Transforms ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls.
440    pub no_ops_to_function_calls: bool,
441    /// Do not merge the chains of gotos.
442    pub no_merge_goto_chains: bool,
443    /// Print the llbc just after control-flow reconstruction.
444    pub print_built_llbc: bool,
445    /// Don't special-case the translation of `Box<T>`
446    pub raw_boxes: bool,
447    /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
448    /// field.
449    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
450    /// List of traits for which we transform associated types to type parameters.
451    pub remove_associated_types: Vec<NamePattern>,
452}
453
454impl TranslateOptions {
455    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
456        let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
457            Ok(p) => Ok(p),
458            Err(e) => {
459                raise_error!(
460                    error_ctx,
461                    crate(&TranslatedCrate::default()),
462                    Span::dummy(),
463                    "failed to parse pattern `{s}` ({e})"
464                )
465            }
466        };
467
468        let mir_level = if options.mir_optimized {
469            MirLevel::Optimized
470        } else if options.mir_promoted {
471            MirLevel::Promoted
472        } else {
473            options.mir.unwrap_or_default()
474        };
475
476        let item_opacities = {
477            use ItemOpacity::*;
478            let mut opacities = vec![];
479
480            // This is how to treat items that don't match any other pattern.
481            if options.extract_opaque_bodies {
482                opacities.push(("_".to_string(), Transparent));
483            } else {
484                opacities.push(("_".to_string(), Foreign));
485            }
486
487            // We always include the items from the crate.
488            opacities.push(("crate".to_owned(), Transparent));
489
490            for pat in options.include.iter() {
491                opacities.push((pat.to_string(), Transparent));
492            }
493            for pat in options.opaque.iter() {
494                opacities.push((pat.to_string(), Opaque));
495            }
496            for pat in options.exclude.iter() {
497                opacities.push((pat.to_string(), Invisible));
498            }
499
500            if options.hide_allocator {
501                opacities.push((format!("core::alloc::Allocator"), Invisible));
502                opacities.push((
503                    format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
504                    Invisible,
505                ));
506            }
507
508            opacities
509                .into_iter()
510                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
511                .collect()
512        };
513
514        let remove_associated_types = options
515            .remove_associated_types
516            .iter()
517            .filter_map(|s| parse_pattern(&s).ok())
518            .collect();
519
520        TranslateOptions {
521            mir_level,
522            monomorphize_mut: options.monomorphize_mut,
523            hide_marker_traits: options.hide_marker_traits,
524            hide_allocator: options.hide_allocator,
525            remove_unused_self_clauses: options.remove_unused_self_clauses,
526            monomorphize_with_hax: options.monomorphize,
527            no_merge_goto_chains: options.no_merge_goto_chains,
528            no_ops_to_function_calls: options.no_ops_to_function_calls,
529            print_built_llbc: options.print_built_llbc,
530            item_opacities,
531            raw_boxes: options.raw_boxes,
532            remove_associated_types,
533            translate_all_methods: options.translate_all_methods,
534        }
535    }
536
537    /// Find the opacity requested for the given name. This does not take into account
538    /// `#[charon::opaque]` annotations, only cli parameters.
539    #[tracing::instrument(skip(self, krate), ret)]
540    pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
541        // Find the most precise pattern that matches this name. There is always one since
542        // the list contains the `_` pattern. If there are conflicting settings for this item, we
543        // err on the side of being more opaque.
544        let (_, opacity) = self
545            .item_opacities
546            .iter()
547            .filter(|(pat, _)| pat.matches(krate, name))
548            .max()
549            .unwrap();
550        *opacity
551    }
552}