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

charon_lib/
options.rs
