charon_lib/
options.rs

1//! The options that control charon behavior.
2use indoc::indoc;
3use serde::{Deserialize, Serialize};
4use std::path::PathBuf;
5
6use crate::{ast::*, errors::ErrorCtx, name_matcher::NamePattern, raise_error, register_error};
7
8/// The name of the environment variable we use to save the serialized Cli options
9/// when calling charon-driver from cargo-charon.
10pub const CHARON_ARGS: &str = "CHARON_ARGS";
11
12// This structure is used to store the command-line instructions.
13// We automatically derive a command-line parser based on this structure.
14// Note that the doc comments are used to generate the help message when using
15// `--help`.
16//
17// Note that because we need to transmit the options to the charon driver,
18// we store them in a file before calling this driver (hence the `Serialize`,
19// `Deserialize` options).
20#[derive(Debug, Default, Clone, clap::Args, Serialize, Deserialize)]
21#[clap(name = "Charon")]
22#[charon::rename("cli_options")]
23pub struct CliOpts {
24    /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow)
25    #[clap(long = "ullbc")]
26    #[serde(default)]
27    pub ullbc: bool,
28    /// Compile the package's library
29    #[clap(long = "lib")]
30    #[serde(default)]
31    pub lib: bool,
32    /// Compile the specified binary
33    #[clap(long = "bin")]
34    #[serde(default)]
35    pub bin: Option<String>,
36    /// Extract the promoted MIR instead of the built MIR
37    #[clap(long = "mir_promoted")]
38    #[serde(default)]
39    pub mir_promoted: bool,
40    /// Extract the optimized MIR instead of the built MIR
41    #[clap(long = "mir_optimized")]
42    #[serde(default)]
43    pub mir_optimized: bool,
44    /// The input file (the entry point of the crate to extract).
45    /// This is needed if you want to define a custom entry point (to only
46    /// extract part of a crate for instance).
47    #[clap(long = "input", value_parser)]
48    #[serde(default)]
49    pub input_file: Option<PathBuf>,
50    /// Read an llbc file and pretty-print it. This is a terrible API, we should use subcommands.
51    #[clap(long = "read-llbc", value_parser)]
52    #[serde(default)]
53    pub read_llbc: Option<PathBuf>,
54    /// The destination directory. Files will be generated as `<dest_dir>/<crate_name>.{u}llbc`,
55    /// unless `dest_file` is set. `dest_dir` defaults to the current directory.
56    #[clap(long = "dest", value_parser)]
57    #[serde(default)]
58    pub dest_dir: Option<PathBuf>,
59    /// The destination file. By default `<dest_dir>/<crate_name>.llbc`. If this is set we ignore
60    /// `dest_dir`.
61    #[clap(long = "dest-file", value_parser)]
62    #[serde(default)]
63    pub dest_file: Option<PathBuf>,
64    /// If activated, use Polonius' non-lexical lifetimes (NLL) analysis.
65    /// Otherwise, use the standard borrow checker.
66    #[clap(long = "polonius")]
67    #[serde(default)]
68    pub use_polonius: bool,
69    /// If activated, this skips borrow-checking of the crate.
70    #[clap(long = "skip-borrowck")]
71    #[serde(default)]
72    pub skip_borrowck: bool,
73    #[clap(
74        long = "no-code-duplication",
75        help = indoc!("
76            Check that no code duplication happens during control-flow reconstruction
77            of the MIR code.
78
79            This is only used to make sure the reconstructed code is of good quality.
80            For instance, if we have the following CFG in MIR:
81              ```
82              b0: switch x [true -> goto b1; false -> goto b2]
83              b1: y := 0; goto b3
84              b2: y := 1; goto b3
85              b3: return y
86              ```
87
88            We want to reconstruct the control-flow as:
89              ```
90              if x then { y := 0; } else { y := 1 };
91              return y;
92              ```
93
94            But if we don't do this reconstruction correctly, we might duplicate
95            the code starting at b3:
96              ```
97              if x then { y := 0; return y; } else { y := 1; return y; }
98              ```
99
100            When activating this flag, we check that no such things happen.
101
102            Also note that it is sometimes not possible to prevent code duplication,
103            if the original Rust looks like this for instance:
104              ```
105              match x with
106              | E1(y,_) | E2(_,y) => { ... } // Some branches are \"fused\"
107              | E3 => { ... }
108              ```
109
110            The reason is that assignments are introduced when desugaring the pattern
111            matching, and those assignments are specific to the variant on which we pattern
112            match (the `E1` branch performs: `y := (x as E1).0`, while the `E2` branch
113            performs: `y := (x as E2).1`). Producing a better reconstruction is non-trivial.
114    "))]
115    #[serde(default)]
116    pub no_code_duplication: bool,
117    /// Monomorphize the code, replacing generics with their concrete types.
118    #[clap(long = "monomorphize")]
119    #[serde(default)]
120    pub monomorphize: bool,
121    /// Usually we skip the bodies of foreign methods and structs with private fields. When this
122    /// flag is on, we don't.
123    #[clap(long = "extract-opaque-bodies")]
124    #[serde(default)]
125    pub extract_opaque_bodies: bool,
126    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
127    /// them all.
128    #[clap(long = "translate-all-methods")]
129    #[serde(default)]
130    pub translate_all_methods: bool,
131    /// Whitelist of items to translate. These use the name-matcher syntax.
132    #[clap(
133        long = "include",
134        help = indoc!("
135            Whitelist of items to translate. These use the name-matcher syntax (note: this differs
136            a bit from the ocaml NameMatcher).
137
138            Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
139            built-in type. It is also not possible to filter a trait impl (this will only filter
140            its methods). Please report bugs or missing features.
141
142            Examples:
143              - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
144                  submodules or trait methods);
145              - `crate::module1::module2::item::_`: refers only to the subitems of this item;
146              - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
147                  very useful impl;
148
149            When multiple patterns in the `--include` and `--opaque` options match the same item,
150            the most precise pattern wins. E.g.: `charon --opaque crate::module --include
151            crate::module::_` makes the `module` opaque (we won't explore its contents), but the
152            items in it transparent (we will translate them if we encounter them.)
153    "))]
154    #[serde(default)]
155    #[charon::rename("included")]
156    pub include: Vec<String>,
157    /// Blacklist of items to keep opaque. These use the name-matcher syntax.
158    #[clap(
159        long = "opaque",
160        help = "Blacklist of items to keep opaque. Works just like `--include`, see the doc there."
161    )]
162    #[serde(default)]
163    pub opaque: Vec<String>,
164    /// Blacklist of items to not translate at all. These use the name-matcher syntax.
165    #[clap(
166        long = "exclude",
167        help = "Blacklist of items to not translate at all. Works just like `--include`, see the doc there."
168    )]
169    #[serde(default)]
170    pub exclude: Vec<String>,
171    /// List of traits for which we transform associated types to type parameters.
172    #[clap(
173        long = "remove-associated-types",
174        help = "List of traits for which we transform associated types to type parameters. \
175        The syntax is like `--include`, see the doc there."
176    )]
177    #[serde(default)]
178    pub remove_associated_types: Vec<String>,
179    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
180    /// up.
181    #[clap(long = "hide-marker-traits")]
182    #[serde(default)]
183    pub hide_marker_traits: bool,
184    /// A list of item paths to use as starting points for the translation. We will translate these
185    /// items and any items they refer to, according to the opacity rules. When absent, we start
186    /// from the path `crate` (which translates the whole crate).
187    #[clap(long = "start-from")]
188    #[serde(default)]
189    pub start_from: Vec<String>,
190    /// Do not run cargo; instead, run the driver directly.
191    // FIXME: use a subcommand instead, when we update clap to support flattening.
192    #[clap(long = "no-cargo")]
193    #[serde(default)]
194    pub no_cargo: bool,
195    /// Extra flags to pass to rustc.
196    #[clap(long = "rustc-flag", alias = "rustc-arg")]
197    #[serde(default)]
198    pub rustc_args: Vec<String>,
199    /// Extra flags to pass to cargo. Incompatible with `--no-cargo`.
200    #[clap(long = "cargo-arg")]
201    #[serde(default)]
202    pub cargo_args: Vec<String>,
203    /// Panic on the first error. This is useful for debugging.
204    #[clap(long = "abort-on-error")]
205    #[serde(default)]
206    pub abort_on_error: bool,
207    /// Print the errors as warnings
208    #[clap(long = "error-on-warnings", help = "Consider any warnings as errors")]
209    #[serde(default)]
210    pub error_on_warnings: bool,
211    #[clap(
212        long = "no-serialize",
213        help = "Don't serialize the final (U)LLBC to a file."
214    )]
215    #[serde(default)]
216    pub no_serialize: bool,
217    #[clap(
218        long = "print-original-ullbc",
219        help = "Print the ULLBC immediately after extraction from MIR."
220    )]
221    #[serde(default)]
222    pub print_original_ullbc: bool,
223    #[clap(
224        long = "print-ullbc",
225        help = "Print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction)."
226    )]
227    #[serde(default)]
228    pub print_ullbc: bool,
229    #[clap(
230        long = "print-built-llbc",
231        help = "Print the LLBC just after we built it (i.e., immediately after loop reconstruction)."
232    )]
233    #[serde(default)]
234    pub print_built_llbc: bool,
235    #[clap(
236        long = "print-llbc",
237        help = "Print the final LLBC (after all the cleaning micro-passes)."
238    )]
239    #[serde(default)]
240    pub print_llbc: bool,
241    #[clap(
242        long = "no-merge-goto-chains",
243        help = indoc!("
244            Do not merge the chains of gotos in the ULLBC control-flow graph.
245    "))]
246    #[serde(default)]
247    pub no_merge_goto_chains: bool,
248}
249
250impl CliOpts {
251    /// Check that the options are meaningful
252    pub fn validate(&self) {
253        assert!(
254            !self.lib || self.bin.is_none(),
255            "Can't use --lib and --bin at the same time"
256        );
257
258        assert!(
259            !self.mir_promoted || !self.mir_optimized,
260            "Can't use --mir_promoted and --mir_optimized at the same time"
261        );
262    }
263}
264
265/// TODO: maybe we should always target MIR Built, this would make things
266/// simpler. In particular, the MIR optimized is very low level and
267/// reveals too many types and data-structures that we don't want to manipulate.
268#[derive(Clone, Copy, PartialEq, Eq)]
269pub enum MirLevel {
270    /// Original MIR, directly translated from HIR.
271    Built,
272    /// Not sure what this is. Not well tested.
273    Promoted,
274    /// MIR after optimization passes. The last one before codegen.
275    Optimized,
276}
277
278/// The options that control translation and transformation.
279pub struct TranslateOptions {
280    /// The level at which to extract the MIR
281    pub mir_level: MirLevel,
282    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
283    /// them all.
284    pub translate_all_methods: bool,
285    /// Error out if some code ends up being duplicated by the control-flow
286    /// reconstruction (note that because several patterns in a match may lead
287    /// to the same branch, it is node always possible not to duplicate code).
288    pub no_code_duplication: bool,
289    /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
290    /// up.
291    pub hide_marker_traits: bool,
292    /// Monomorphize functions.
293    pub monomorphize: bool,
294    /// Do not merge the chains of gotos.
295    pub no_merge_goto_chains: bool,
296    /// Print the llbc just after control-flow reconstruction.
297    pub print_built_llbc: bool,
298    /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
299    /// field.
300    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
301    /// List of traits for which we transform associated types to type parameters.
302    pub remove_associated_types: Vec<NamePattern>,
303}
304
305impl TranslateOptions {
306    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
307        let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
308            Ok(p) => Ok(p),
309            Err(e) => {
310                raise_error!(
311                    error_ctx,
312                    crate(&TranslatedCrate::default()),
313                    Span::dummy(),
314                    "failed to parse pattern `{s}` ({e})"
315                )
316            }
317        };
318
319        let mir_level = if options.mir_optimized {
320            MirLevel::Optimized
321        } else if options.mir_promoted {
322            MirLevel::Promoted
323        } else {
324            MirLevel::Built
325        };
326
327        let item_opacities = {
328            use ItemOpacity::*;
329            let mut opacities = vec![];
330
331            // This is how to treat items that don't match any other pattern.
332            if options.extract_opaque_bodies {
333                opacities.push(("_".to_string(), Transparent));
334            } else {
335                opacities.push(("_".to_string(), Foreign));
336            }
337
338            // We always include the items from the crate.
339            opacities.push(("crate".to_owned(), Transparent));
340
341            for pat in options.include.iter() {
342                opacities.push((pat.to_string(), Transparent));
343            }
344            for pat in options.opaque.iter() {
345                opacities.push((pat.to_string(), Opaque));
346            }
347            for pat in options.exclude.iter() {
348                opacities.push((pat.to_string(), Invisible));
349            }
350
351            // We always hide this trait.
352            opacities.push((format!("core::alloc::Allocator"), Invisible));
353            opacities.push((
354                format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
355                Invisible,
356            ));
357
358            opacities
359                .into_iter()
360                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
361                .collect()
362        };
363
364        let remove_associated_types = options
365            .remove_associated_types
366            .iter()
367            .filter_map(|s| parse_pattern(&s).ok())
368            .collect();
369
370        TranslateOptions {
371            mir_level,
372            no_code_duplication: options.no_code_duplication,
373            hide_marker_traits: options.hide_marker_traits,
374            monomorphize: options.monomorphize,
375            no_merge_goto_chains: options.no_merge_goto_chains,
376            print_built_llbc: options.print_built_llbc,
377            item_opacities,
378            remove_associated_types,
379            translate_all_methods: options.translate_all_methods,
380        }
381    }
382
383    /// Find the opacity requested for the given name. This does not take into account
384    /// `#[charon::opaque]` annotations, only cli parameters.
385    pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
386        // Find the most precise pattern that matches this name. There is always one since
387        // the list contains the `_` pattern. If there are conflicting settings for this item, we
388        // err on the side of being more opaque.
389        let (_, opacity) = self
390            .item_opacities
391            .iter()
392            .filter(|(pat, _)| pat.matches(krate, name))
393            .max()
394            .unwrap();
395        *opacity
396    }
397}
charon_lib/options.rs

charon_lib/
options.rs
