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    /// Named builtin sets of options. Currently used only for dependent projects, eveentually
229    /// should be replaced with semantically-meaningful presets.
230    #[clap(long = "preset")]
231    #[arg(value_enum)]
232    pub preset: Option<Preset>,
233}
234
235/// The MIR stage to use. This is only relevant for the current crate: for dependencies, only mir
236/// optimized is available (or mir elaborated for consts).
237#[derive(
238    Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
239)]
240pub enum MirLevel {
241    /// The MIR just after MIR lowering.
242    #[default]
243    Built,
244    /// The MIR after const promotion. This is the MIR used by the borrow-checker.
245    Promoted,
246    /// The MIR after drop elaboration. This is the first MIR to include all the runtime
247    /// information.
248    Elaborated,
249    /// The MIR after optimizations. Charon disables all the optimizations it can, so this is
250    /// sensibly the same MIR as the elaborated MIR.
251    Optimized,
252}
253
254/// Presets to make it easier to tweak options without breaking dependent projects. Eventually we
255/// should define semantically-meaningful presets instead of project-specific ones.
256#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
257#[non_exhaustive]
258pub enum Preset {
259    /// The default translation used before May 2025. After that, many passes were made optional
260    /// and disabled by default.
261    OldDefaults,
262    Aeneas,
263    Eurydice,
264    Tests,
265}
266
267impl CliOpts {
268    pub fn apply_preset(&mut self) {
269        if let Some(preset) = self.preset {
270            match preset {
271                Preset::OldDefaults => {}
272                Preset::Aeneas => {
273                    self.remove_associated_types.push("*".to_owned());
274                    self.hide_marker_traits = true;
275                    self.remove_unused_self_clauses = true;
276                }
277                Preset::Eurydice => {
278                    self.remove_associated_types.push("*".to_owned());
279                }
280                Preset::Tests => {
281                    self.rustc_args.push("--edition=2021".to_owned());
282                }
283            }
284        }
285    }
286
287    /// Check that the options are meaningful
288    pub fn validate(&self) {
289        assert!(
290            !self.lib || self.bin.is_none(),
291            "Can't use --lib and --bin at the same time"
292        );
293
294        assert!(
295            !self.mir_promoted || !self.mir_optimized,
296            "Can't use --mir_promoted and --mir_optimized at the same time"
297        );
298
299        if self.input_file.is_some() {
300            display_unspanned_error(
301                Level::WARNING,
302                "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
303            )
304        }
305        if self.no_cargo {
306            display_unspanned_error(
307                Level::WARNING,
308                "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
309            )
310        }
311        if self.read_llbc.is_some() {
312            display_unspanned_error(
313                Level::WARNING,
314                "`--read_llbc` is deprecated, use `charon pretty-print <input file>` instead",
315            )
316        }
317        if self.use_polonius {
318            display_unspanned_error(
319                Level::WARNING,
320                "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead",
321            )
322        }
323        if self.mir_optimized {
324            display_unspanned_error(
325                Level::WARNING,
326                "`--mir_optimized` is deprecated, use `--mir optimized` instead",
327            )
328        }
329        if self.mir_promoted {
330            display_unspanned_error(
331                Level::WARNING,
332                "`--mir_promoted` is deprecated, use `--mir promoted` instead",
333            )
334        }
335        if self.lib {
336            display_unspanned_error(
337                Level::WARNING,
338                "`--lib` is deprecated, use `charon cargo -- --lib` instead",
339            )
340        }
341        if self.bin.is_some() {
342            display_unspanned_error(
343                Level::WARNING,
344                "`--bin` is deprecated, use `charon cargo -- --bin <name>` instead",
345            )
346        }
347        if self.dest_dir.is_some() {
348            display_unspanned_error(
349                Level::WARNING,
350                "`--dest` is deprecated, use `--dest-file` instead",
351            )
352        }
353    }
354}
355
356/// The options that control translation and transformation.
357pub struct TranslateOptions {
358    /// The level at which to extract the MIR
359    pub mir_level: MirLevel,
360    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
361    /// them all.
362    pub translate_all_methods: bool,
363    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
364    /// up.
365    pub hide_marker_traits: bool,
366    /// Remove unused `Self: Trait` clauses on method declarations.
367    pub remove_unused_self_clauses: bool,
368    /// Monomorphize functions.
369    pub monomorphize: bool,
370    /// Transforms ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls.
371    pub no_ops_to_function_calls: bool,
372    /// Do not merge the chains of gotos.
373    pub no_merge_goto_chains: bool,
374    /// Print the llbc just after control-flow reconstruction.
375    pub print_built_llbc: bool,
376    /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
377    /// field.
378    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
379    /// List of traits for which we transform associated types to type parameters.
380    pub remove_associated_types: Vec<NamePattern>,
381}
382
383impl TranslateOptions {
384    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
385        let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
386            Ok(p) => Ok(p),
387            Err(e) => {
388                raise_error!(
389                    error_ctx,
390                    crate(&TranslatedCrate::default()),
391                    Span::dummy(),
392                    "failed to parse pattern `{s}` ({e})"
393                )
394            }
395        };
396
397        let mir_level = if options.mir_optimized {
398            MirLevel::Optimized
399        } else if options.mir_promoted {
400            MirLevel::Promoted
401        } else {
402            options.mir.unwrap_or_default()
403        };
404
405        let item_opacities = {
406            use ItemOpacity::*;
407            let mut opacities = vec![];
408
409            // This is how to treat items that don't match any other pattern.
410            if options.extract_opaque_bodies {
411                opacities.push(("_".to_string(), Transparent));
412            } else {
413                opacities.push(("_".to_string(), Foreign));
414            }
415
416            // We always include the items from the crate.
417            opacities.push(("crate".to_owned(), Transparent));
418
419            for pat in options.include.iter() {
420                opacities.push((pat.to_string(), Transparent));
421            }
422            for pat in options.opaque.iter() {
423                opacities.push((pat.to_string(), Opaque));
424            }
425            for pat in options.exclude.iter() {
426                opacities.push((pat.to_string(), Invisible));
427            }
428
429            // We always hide this trait.
430            opacities.push((format!("core::alloc::Allocator"), Invisible));
431            opacities.push((
432                format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
433                Invisible,
434            ));
435
436            opacities
437                .into_iter()
438                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
439                .collect()
440        };
441
442        let remove_associated_types = options
443            .remove_associated_types
444            .iter()
445            .filter_map(|s| parse_pattern(&s).ok())
446            .collect();
447
448        TranslateOptions {
449            mir_level,
450            hide_marker_traits: options.hide_marker_traits,
451            remove_unused_self_clauses: options.remove_unused_self_clauses,
452            monomorphize: options.monomorphize,
453            no_merge_goto_chains: options.no_merge_goto_chains,
454            no_ops_to_function_calls: options.no_ops_to_function_calls,
455            print_built_llbc: options.print_built_llbc,
456            item_opacities,
457            remove_associated_types,
458            translate_all_methods: options.translate_all_methods,
459        }
460    }
461
462    /// Find the opacity requested for the given name. This does not take into account
463    /// `#[charon::opaque]` annotations, only cli parameters.
464    pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
465        // Find the most precise pattern that matches this name. There is always one since
466        // the list contains the `_` pattern. If there are conflicting settings for this item, we
467        // err on the side of being more opaque.
468        let (_, opacity) = self
469            .item_opacities
470            .iter()
471            .filter(|(pat, _)| pat.matches(krate, name))
472            .max()
473            .unwrap();
474        *opacity
475    }
476}