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::{display_unspanned_error, ErrorCtx},
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, 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 code, replacing generics with their concrete types.
85    #[clap(long = "monomorphize")]
86    #[serde(default)]
87    pub monomorphize: bool,
88    /// Usually we skip the bodies of foreign methods and structs with private fields. When this
89    /// flag is on, we don't.
90    #[clap(long = "extract-opaque-bodies")]
91    #[serde(default)]
92    pub extract_opaque_bodies: bool,
93    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
94    /// them all.
95    #[clap(long = "translate-all-methods")]
96    #[serde(default)]
97    pub translate_all_methods: bool,
98    /// Whitelist of items to translate. These use the name-matcher syntax.
99    #[clap(
100        long = "include",
101        help = indoc!("
102            Whitelist of items to translate. These use the name-matcher syntax (note: this differs
103            a bit from the ocaml NameMatcher).
104
105            Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
106            built-in type. It is also not possible to filter a trait impl (this will only filter
107            its methods). Please report bugs or missing features.
108
109            Examples:
110              - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
111                  submodules or trait methods);
112              - `crate::module1::module2::item::_`: refers only to the subitems of this item;
113              - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
114                  very useful impl;
115
116            When multiple patterns in the `--include` and `--opaque` options match the same item,
117            the most precise pattern wins. E.g.: `charon --opaque crate::module --include
118            crate::module::_` makes the `module` opaque (we won't explore its contents), but the
119            items in it transparent (we will translate them if we encounter them.)
120    "))]
121    #[serde(default)]
122    #[charon::rename("included")]
123    pub include: Vec<String>,
124    /// Blacklist of items to keep opaque. These use the name-matcher syntax.
125    #[clap(
126        long = "opaque",
127        help = "Blacklist of items to keep opaque. Works just like `--include`, see the doc there."
128    )]
129    #[serde(default)]
130    pub opaque: Vec<String>,
131    /// Blacklist of items to not translate at all. These use the name-matcher syntax.
132    #[clap(
133        long = "exclude",
134        help = "Blacklist of items to not translate at all. Works just like `--include`, see the doc there."
135    )]
136    #[serde(default)]
137    pub exclude: Vec<String>,
138    /// List of traits for which we transform associated types to type parameters.
139    #[clap(
140        long = "remove-associated-types",
141        help = "List of traits for which we transform associated types to type parameters. \
142        The syntax is like `--include`, see the doc there."
143    )]
144    #[serde(default)]
145    pub remove_associated_types: Vec<String>,
146    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
147    /// up.
148    #[clap(long = "hide-marker-traits")]
149    #[serde(default)]
150    pub hide_marker_traits: bool,
151    /// Trait method declarations take a `Self: Trait` clause as parameter, so that they can be
152    /// reused by multiple trait impls. This however causes trait definitions to be mutually
153    /// recursive with their method declarations. This flag removes `Self` clauses that aren't used
154    /// to break this mutual recursion.
155    #[clap(long)]
156    #[serde(default)]
157    pub remove_unused_self_clauses: bool,
158    /// A list of item paths to use as starting points for the translation. We will translate these
159    /// items and any items they refer to, according to the opacity rules. When absent, we start
160    /// from the path `crate` (which translates the whole crate).
161    #[clap(long = "start-from")]
162    #[serde(default)]
163    pub start_from: Vec<String>,
164    /// Do not run cargo; instead, run the driver directly.
165    #[clap(long = "no-cargo")]
166    #[serde(default)]
167    pub no_cargo: bool,
168    /// Extra flags to pass to rustc.
169    #[clap(long = "rustc-flag", alias = "rustc-arg")]
170    #[serde(default)]
171    pub rustc_args: Vec<String>,
172    /// Extra flags to pass to cargo. Incompatible with `--no-cargo`.
173    #[clap(long = "cargo-arg")]
174    #[serde(default)]
175    pub cargo_args: Vec<String>,
176    /// Panic on the first error. This is useful for debugging.
177    #[clap(long = "abort-on-error")]
178    #[serde(default)]
179    pub abort_on_error: bool,
180    /// Print the errors as warnings
181    #[clap(long = "error-on-warnings", help = "Consider any warnings as errors")]
182    #[serde(default)]
183    pub error_on_warnings: bool,
184    #[clap(
185        long = "no-serialize",
186        help = "Don't serialize the final (U)LLBC to a file."
187    )]
188    #[serde(default)]
189    pub no_serialize: bool,
190    #[clap(
191        long = "print-original-ullbc",
192        help = "Print the ULLBC immediately after extraction from MIR."
193    )]
194    #[serde(default)]
195    pub print_original_ullbc: bool,
196    #[clap(
197        long = "print-ullbc",
198        help = "Print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction)."
199    )]
200    #[serde(default)]
201    pub print_ullbc: bool,
202    #[clap(
203        long = "print-built-llbc",
204        help = "Print the LLBC just after we built it (i.e., immediately after loop reconstruction)."
205    )]
206    #[serde(default)]
207    pub print_built_llbc: bool,
208    #[clap(
209        long = "print-llbc",
210        help = "Print the final LLBC (after all the cleaning micro-passes)."
211    )]
212    #[serde(default)]
213    pub print_llbc: bool,
214    #[clap(
215        long = "no-merge-goto-chains",
216        help = "Do not merge the chains of gotos in the ULLBC control-flow graph."
217    )]
218    #[serde(default)]
219    pub no_merge_goto_chains: bool,
220
221    #[clap(
222        long = "no-ops-to-function-calls",
223        help = "Do not transform ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls for ULLBC"
224    )]
225    #[serde(default)]
226    pub no_ops_to_function_calls: bool,
227
228    #[clap(
229        long = "raw-boxes",
230        help = "Do not special-case the translation of `Box<T>` into a builtin ADT."
231    )]
232    #[serde(default)]
233    pub raw_boxes: bool,
234
235    /// Named builtin sets of options. Currently used only for dependent projects, eveentually
236    /// should be replaced with semantically-meaningful presets.
237    #[clap(long = "preset")]
238    #[arg(value_enum)]
239    pub preset: Option<Preset>,
240}
241
242/// The MIR stage to use. This is only relevant for the current crate: for dependencies, only mir
243/// optimized is available (or mir elaborated for consts).
244#[derive(
245    Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
246)]
247pub enum MirLevel {
248    /// The MIR just after MIR lowering.
249    #[default]
250    Built,
251    /// The MIR after const promotion. This is the MIR used by the borrow-checker.
252    Promoted,
253    /// The MIR after drop elaboration. This is the first MIR to include all the runtime
254    /// information.
255    Elaborated,
256    /// The MIR after optimizations. Charon disables all the optimizations it can, so this is
257    /// sensibly the same MIR as the elaborated MIR.
258    Optimized,
259}
260
261/// Presets to make it easier to tweak options without breaking dependent projects. Eventually we
262/// should define semantically-meaningful presets instead of project-specific ones.
263#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
264#[non_exhaustive]
265pub enum Preset {
266    /// The default translation used before May 2025. After that, many passes were made optional
267    /// and disabled by default.
268    OldDefaults,
269    Aeneas,
270    Eurydice,
271    Tests,
272}
273
274impl CliOpts {
275    pub fn apply_preset(&mut self) {
276        if let Some(preset) = self.preset {
277            match preset {
278                Preset::OldDefaults => {}
279                Preset::Aeneas => {
280                    self.remove_associated_types.push("*".to_owned());
281                    self.hide_marker_traits = true;
282                    self.remove_unused_self_clauses = true;
283                }
284                Preset::Eurydice => {
285                    self.remove_associated_types.push("*".to_owned());
286                }
287                Preset::Tests => {
288                    self.rustc_args.push("--edition=2021".to_owned());
289                }
290            }
291        }
292    }
293
294    /// Check that the options are meaningful
295    pub fn validate(&self) {
296        assert!(
297            !self.lib || self.bin.is_none(),
298            "Can't use --lib and --bin at the same time"
299        );
300
301        assert!(
302            !self.mir_promoted || !self.mir_optimized,
303            "Can't use --mir_promoted and --mir_optimized at the same time"
304        );
305
306        if self.input_file.is_some() {
307            display_unspanned_error(
308                Level::WARNING,
309                "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
310            )
311        }
312        if self.no_cargo {
313            display_unspanned_error(
314                Level::WARNING,
315                "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
316            )
317        }
318        if self.read_llbc.is_some() {
319            display_unspanned_error(
320                Level::WARNING,
321                "`--read_llbc` is deprecated, use `charon pretty-print <input file>` instead",
322            )
323        }
324        if self.use_polonius {
325            display_unspanned_error(
326                Level::WARNING,
327                "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead",
328            )
329        }
330        if self.mir_optimized {
331            display_unspanned_error(
332                Level::WARNING,
333                "`--mir_optimized` is deprecated, use `--mir optimized` instead",
334            )
335        }
336        if self.mir_promoted {
337            display_unspanned_error(
338                Level::WARNING,
339                "`--mir_promoted` is deprecated, use `--mir promoted` instead",
340            )
341        }
342        if self.lib {
343            display_unspanned_error(
344                Level::WARNING,
345                "`--lib` is deprecated, use `charon cargo -- --lib` instead",
346            )
347        }
348        if self.bin.is_some() {
349            display_unspanned_error(
350                Level::WARNING,
351                "`--bin` is deprecated, use `charon cargo -- --bin <name>` instead",
352            )
353        }
354        if self.dest_dir.is_some() {
355            display_unspanned_error(
356                Level::WARNING,
357                "`--dest` is deprecated, use `--dest-file` instead",
358            )
359        }
360    }
361}
362
363/// The options that control translation and transformation.
364pub struct TranslateOptions {
365    /// The level at which to extract the MIR
366    pub mir_level: MirLevel,
367    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
368    /// them all.
369    pub translate_all_methods: bool,
370    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
371    /// up.
372    pub hide_marker_traits: bool,
373    /// Remove unused `Self: Trait` clauses on method declarations.
374    pub remove_unused_self_clauses: bool,
375    /// Monomorphize functions.
376    pub monomorphize: bool,
377    /// Transforms ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls.
378    pub no_ops_to_function_calls: bool,
379    /// Do not merge the chains of gotos.
380    pub no_merge_goto_chains: bool,
381    /// Print the llbc just after control-flow reconstruction.
382    pub print_built_llbc: bool,
383    /// Don't special-case the translation of `Box<T>`
384    pub raw_boxes: bool,
385    /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
386    /// field.
387    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
388    /// List of traits for which we transform associated types to type parameters.
389    pub remove_associated_types: Vec<NamePattern>,
390}
391
392impl TranslateOptions {
393    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
394        let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
395            Ok(p) => Ok(p),
396            Err(e) => {
397                raise_error!(
398                    error_ctx,
399                    crate(&TranslatedCrate::default()),
400                    Span::dummy(),
401                    "failed to parse pattern `{s}` ({e})"
402                )
403            }
404        };
405
406        let mir_level = if options.mir_optimized {
407            MirLevel::Optimized
408        } else if options.mir_promoted {
409            MirLevel::Promoted
410        } else {
411            options.mir.unwrap_or_default()
412        };
413
414        let item_opacities = {
415            use ItemOpacity::*;
416            let mut opacities = vec![];
417
418            // This is how to treat items that don't match any other pattern.
419            if options.extract_opaque_bodies {
420                opacities.push(("_".to_string(), Transparent));
421            } else {
422                opacities.push(("_".to_string(), Foreign));
423            }
424
425            // We always include the items from the crate.
426            opacities.push(("crate".to_owned(), Transparent));
427
428            for pat in options.include.iter() {
429                opacities.push((pat.to_string(), Transparent));
430            }
431            for pat in options.opaque.iter() {
432                opacities.push((pat.to_string(), Opaque));
433            }
434            for pat in options.exclude.iter() {
435                opacities.push((pat.to_string(), Invisible));
436            }
437
438            if !options.raw_boxes {
439                opacities.push((format!("core::alloc::Allocator"), Invisible));
440                opacities.push((
441                    format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
442                    Invisible,
443                ));
444            }
445
446            opacities
447                .into_iter()
448                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
449                .collect()
450        };
451
452        let remove_associated_types = options
453            .remove_associated_types
454            .iter()
455            .filter_map(|s| parse_pattern(&s).ok())
456            .collect();
457
458        TranslateOptions {
459            mir_level,
460            hide_marker_traits: options.hide_marker_traits,
461            remove_unused_self_clauses: options.remove_unused_self_clauses,
462            monomorphize: options.monomorphize,
463            no_merge_goto_chains: options.no_merge_goto_chains,
464            no_ops_to_function_calls: options.no_ops_to_function_calls,
465            print_built_llbc: options.print_built_llbc,
466            item_opacities,
467            raw_boxes: options.raw_boxes,
468            remove_associated_types,
469            translate_all_methods: options.translate_all_methods,
470        }
471    }
472
473    /// Find the opacity requested for the given name. This does not take into account
474    /// `#[charon::opaque]` annotations, only cli parameters.
475    pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
476        // Find the most precise pattern that matches this name. There is always one since
477        // the list contains the `_` pattern. If there are conflicting settings for this item, we
478        // err on the side of being more opaque.
479        let (_, opacity) = self
480            .item_opacities
481            .iter()
482            .filter(|(pat, _)| pat.matches(krate, name))
483            .max()
484            .unwrap();
485        *opacity
486    }
487}