Skip to main content

charon_lib/
options.rs

1//! The options that control charon behavior.
2use annotate_snippets::Level;
3use clap::ValueEnum;
4use indoc::indoc;
5use itertools::Itertools;
6use macros::EnumAsGetters;
7use serde::{Deserialize, Serialize};
8use std::path::PathBuf;
9
10use crate::{
11    ast::*,
12    errors::{ErrorCtx, display_unspanned_error},
13    name_matcher::NamePattern,
14    raise_error, register_error,
15};
16
17/// The name of the environment variable we use to save the serialized Cli options
18/// when calling charon-driver from cargo-charon.
19pub const CHARON_ARGS: &str = "CHARON_ARGS";
20
21// This structure is used to store the command-line instructions.
22// We automatically derive a command-line parser based on this structure.
23// Note that the doc comments are used to generate the help message when using
24// `--help`.
25//
26// Note that because we need to transmit the options to the charon driver,
27// we store them in a file before calling this driver (hence the `Serialize`,
28// `Deserialize` options).
29#[derive(Debug, Default, Clone, clap::Args, PartialEq, Eq, Serialize, Deserialize)]
30#[clap(name = "Charon")]
31#[charon::rename("cli_options")]
32pub struct CliOpts {
33    /// Extract the unstructured LLBC (i.e., don't reconstruct the control-flow)
34    #[clap(long)]
35    #[serde(default)]
36    pub ullbc: bool,
37    /// Whether to precisely translate drops and drop-related code. For this, we add explicit
38    /// `Destruct` bounds to all generic parameters, set the MIR level to at least `elaborated`,
39    /// and attempt to retrieve drop glue for all types.
40    ///
41    /// This option is known to cause panics inside rustc, because their drop handling is not
42    /// design to work on polymorphic types. To silence the warning, pass appropriate `--opaque
43    /// '{impl core::marker::Destruct for some::Type}'` options.
44    ///
45    /// Without this option, drops may be "conditional" and we may lack information about what code
46    /// is run on drop in a given polymorphic function body.
47    #[clap(long)]
48    #[serde(default)]
49    pub precise_drops: bool,
50    /// If activated, this skips borrow-checking of the crate.
51    #[clap(long)]
52    #[serde(default)]
53    pub skip_borrowck: bool,
54    /// The MIR stage to extract. This is only relevant for the current crate; for dpendencies only
55    /// MIR optimized is available.
56    #[arg(long)]
57    pub mir: Option<MirLevel>,
58    /// Extra flags to pass to rustc.
59    #[clap(long = "rustc-arg")]
60    #[serde(default)]
61    pub rustc_args: Vec<String>,
62    /// A list of target architectures to translate for. Charon will run the compiler once for each
63    /// target and aggregate the results, which is useful if the code includes `#[cfg(..)]`
64    /// filters.
65    /// Warning: this is an initial implementation which is extremely slow.
66    #[clap(long, value_delimiter = ',')]
67    #[serde(default)]
68    pub targets: Vec<String>,
69
70    /// Monomorphize the items encountered when possible. Generic items found in the crate are
71    /// skipped. To only translate a particular call graph, use `--start-from`. Note: this doesn't
72    /// currently support `dyn Trait`.
73    #[clap(long, visible_alias = "mono")]
74    #[serde(default)]
75    pub monomorphize: bool,
76    /// Partially monomorphize items to make it so that no item is ever monomorphized with a
77    /// mutable reference (or type containing one); said differently, so that the presence of
78    /// mutable references in a type is independent of its generics. This is used by Aeneas.
79    #[clap(
80        long,
81        value_name("INCLUDE_TYPES"),
82        num_args(0..=1),
83        require_equals(true),
84        default_missing_value("all"),
85    )]
86    #[serde(default)]
87    pub monomorphize_mut: Option<MonomorphizeMut>,
88
89    /// A list of item paths to use as starting points for the translation. We will translate these
90    /// items and any items they refer to, according to the opacity rules. When absent, we start
91    /// from the path `crate` (which translates the whole crate).
92    #[clap(long, value_delimiter = ',')]
93    #[serde(default)]
94    pub start_from: Vec<String>,
95    /// Same as --start-from, but won't raise an error if a pattern doesn't match any item. This is useful
96    /// when the patterns are generated by a build script and may be out of sync with the code.
97    #[clap(long, value_delimiter = ',')]
98    #[serde(default)]
99    pub start_from_if_exists: Vec<String>,
100    /// Use all the items annotated with the given attribute as starting points for translation
101    /// (except modules).
102    /// If an attribute name is not specified, `verify::start_from` is used.
103    #[clap(
104        long,
105        value_name("ATTRIBUTE"),
106        num_args(0..=1),
107        require_equals(true),
108        default_missing_value("verify::start_from"),
109    )]
110    #[serde(default)]
111    pub start_from_attribute: Option<String>,
112    /// Use all the `pub` items as starting points for translation (except modules).
113    #[clap(long)]
114    #[serde(default)]
115    pub start_from_pub: bool,
116
117    /// Whitelist of items to translate. These use the name-matcher syntax.
118    #[clap(
119        long,
120        help = indoc!("
121            Whitelist of items to translate. These use the name-matcher syntax (note: this differs
122            a bit from the ocaml NameMatcher).
123
124            Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
125            built-in type. It is also not possible to filter a trait impl (this will only filter
126            its methods). Please report bugs or missing features.
127
128            Examples:
129              - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
130                  submodules or trait methods);
131              - `crate::module1::module2::item::_`: refers only to the subitems of this item;
132              - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
133                  very useful impl;
134
135            When multiple patterns in the `--include` and `--opaque` options match the same item,
136            the most precise pattern wins. E.g.: `charon --opaque crate::module --include
137            crate::module::_` makes the `module` opaque (we won't explore its contents), but the
138            items in it transparent (we will translate them if we encounter them.)
139    "))]
140    #[serde(default)]
141    #[charon::rename("included")]
142    pub include: Vec<String>,
143    /// Blacklist of items to keep opaque. Works just like `--include`, see the doc there.
144    #[clap(long)]
145    #[serde(default)]
146    pub opaque: Vec<String>,
147    /// Blacklist of items to not translate at all. Works just like `--include`, see the doc there.
148    #[clap(long)]
149    #[serde(default)]
150    pub exclude: Vec<String>,
151    /// Usually we skip the bodies of foreign methods and structs with private fields. When this
152    /// flag is on, we don't.
153    #[clap(long)]
154    #[serde(default)]
155    pub extract_opaque_bodies: bool,
156    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
157    /// them all.
158    #[clap(long)]
159    #[serde(default)]
160    pub translate_all_methods: bool,
161
162    /// Transform the associate types of traits to be type parameters instead. This takes a list
163    /// of name patterns of the traits to transform, using the same syntax as `--include`.
164    #[clap(long, alias = "remove-associated-types")]
165    #[serde(default)]
166    pub lift_associated_types: Vec<String>,
167    /// Whether to hide various marker traits such as `Sized`, `Sync`, `Send` and `Destruct`
168    /// anywhere they show up. This can considerably speed up translation.
169    #[clap(long)]
170    #[serde(default)]
171    pub hide_marker_traits: bool,
172    /// Remove trait clauses from type declarations. Must be combined with
173    /// `--remove-associated-types` for type declarations that use trait associated types in their
174    /// fields, otherwise this will result in errors.
175    #[clap(long)]
176    #[serde(default)]
177    pub remove_adt_clauses: bool,
178    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
179    #[clap(long)]
180    #[serde(default)]
181    pub hide_allocator: bool,
182    /// Trait method declarations take a `Self: Trait` clause as parameter, so that they can be
183    /// reused by multiple trait impls. This however causes trait definitions to be mutually
184    /// recursive with their method declarations. This flag removes `Self` clauses that aren't used
185    /// to break this mutual recursion when possible.
186    #[clap(long)]
187    #[serde(default)]
188    pub remove_unused_self_clauses: bool,
189
190    /// Transform precise drops to the equivalent `drop_in_place(&raw mut p)` call.
191    #[clap(long)]
192    #[serde(default)]
193    pub desugar_drops: bool,
194    /// Transform array-to-slice unsizing, repeat expressions, and raw pointer construction into
195    /// builtin functions in ULLBC.
196    #[clap(long)]
197    #[serde(default)]
198    pub ops_to_function_calls: bool,
199    /// Transform array/slice indexing into builtin functions in ULLBC. Note that this may
200    /// introduce UB since it creates references that were not normally created, including when
201    /// indexing behind a raw pointer.
202    #[clap(long)]
203    #[serde(default)]
204    pub index_to_function_calls: bool,
205    /// Treat `Box<T>` as if it was a built-in type.
206    #[clap(long)]
207    #[serde(default)]
208    pub treat_box_as_builtin: bool,
209    /// Do not inline or evaluate constants.
210    #[clap(long)]
211    #[serde(default)]
212    pub raw_consts: bool,
213    /// Replace string literal constants with a constant u8 array that gets unsized,
214    /// expliciting the fact a string constant has a hidden reference.
215    #[clap(long)]
216    #[serde(default)]
217    pub unsized_strings: bool,
218    /// Replace "bound checks followed by UB-on-overflow operation" with the corresponding
219    /// panic-on-overflow operation. This loses unwinding information.
220    #[clap(long)]
221    #[serde(default)]
222    pub reconstruct_fallible_operations: bool,
223    /// Replace `if x { panic() }` with `assert(x)`.
224    #[clap(long)]
225    #[serde(default)]
226    pub reconstruct_asserts: bool,
227    /// Use `DeBruijnVar::Free` for the variables bound in item signatures, instead of
228    /// `DeBruijnVar::Bound` everywhere. This simplifies the management of generics for projects
229    /// that don't intend to manipulate them too much.
230    #[clap(long)]
231    #[serde(default)]
232    pub unbind_item_vars: bool,
233
234    /// Pretty-print the ULLBC immediately after extraction from MIR.
235    #[clap(long)]
236    #[serde(default)]
237    pub print_original_ullbc: bool,
238    /// Pretty-print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction).
239    #[clap(long)]
240    #[serde(default)]
241    pub print_ullbc: bool,
242    /// Pretty-print the LLBC just after we built it (i.e., immediately after loop reconstruction).
243    #[clap(long)]
244    #[serde(default)]
245    pub print_built_llbc: bool,
246    /// Pretty-print the final LLBC (after all the cleaning micro-passes).
247    #[clap(long)]
248    #[serde(default)]
249    pub print_llbc: bool,
250
251    /// The destination directory. Files will be generated as `<dest_dir>/<crate_name>.{u}llbc`,
252    /// unless `dest_file` is set. `dest_dir` defaults to the current directory.
253    #[clap(long = "dest", value_parser)]
254    #[serde(default)]
255    pub dest_dir: Option<PathBuf>,
256    /// The destination file. By default `<dest_dir>/<crate_name>.llbc`. If this is set we ignore
257    /// `dest_dir`.
258    #[clap(long, value_parser)]
259    #[serde(default)]
260    pub dest_file: Option<PathBuf>,
261    /// Don't deduplicate values (types, trait refs) in the .(u)llbc file. This makes the file easier to inspect.
262    #[clap(long)]
263    #[serde(default)]
264    pub no_dedup_serialized_ast: bool,
265    /// Don't serialize the final (U)LLBC to a file.
266    #[clap(long)]
267    #[serde(default)]
268    pub no_serialize: bool,
269    /// Panic on the first error. This is useful for debugging.
270    #[clap(long)]
271    #[serde(default)]
272    pub abort_on_error: bool,
273    /// Consider any warnings to be errors.
274    #[clap(long)]
275    #[serde(default)]
276    pub error_on_warnings: bool,
277
278    /// Named builtin sets of options.
279    #[clap(long)]
280    #[arg(value_enum)]
281    pub preset: Option<Preset>,
282}
283
284/// The MIR stage to use. This is only relevant for the current crate: for dependencies, only mir
285/// optimized is available (or mir elaborated for consts).
286#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
287pub enum MirLevel {
288    /// The MIR just after MIR lowering.
289    Built,
290    /// The MIR after const promotion. This is the MIR used by the borrow-checker.
291    Promoted,
292    /// The MIR after drop elaboration. This is the first MIR to include all the runtime
293    /// information.
294    Elaborated,
295    /// The MIR after optimizations. Charon disables all the optimizations it can, so this is
296    /// sensibly the same MIR as the elaborated MIR.
297    Optimized,
298}
299
300/// Presets to make it easier to tweak options without breaking dependent projects. Eventually we
301/// should define semantically-meaningful presets instead of project-specific ones.
302#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
303#[non_exhaustive]
304pub enum Preset {
305    /// The default translation used before May 2025. After that, many passes were made optional
306    /// and disabled by default.
307    OldDefaults,
308    /// Emit the MIR as unmodified as possible. This is very imperfect for now, we should make more
309    /// passes optional.
310    RawMir,
311    Aeneas,
312    Eurydice,
313    Soteria,
314    Tests,
315}
316
317#[derive(
318    Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
319)]
320pub enum MonomorphizeMut {
321    /// Monomorphize any item instantiated with `&mut`.
322    #[default]
323    All,
324    /// Monomorphize all non-typedecl items instantiated with `&mut`.
325    ExceptTypes,
326}
327
328impl CliOpts {
329    pub fn apply_preset(&mut self) {
330        if let Some(preset) = self.preset {
331            match preset {
332                Preset::OldDefaults => {
333                    self.treat_box_as_builtin = true;
334                    self.hide_allocator = true;
335                    self.ops_to_function_calls = true;
336                    self.index_to_function_calls = true;
337                    self.reconstruct_fallible_operations = true;
338                    self.reconstruct_asserts = true;
339                    self.unbind_item_vars = true;
340                }
341                Preset::RawMir => {
342                    self.extract_opaque_bodies = true;
343                    self.raw_consts = true;
344                    self.ullbc = true;
345                }
346                Preset::Aeneas => {
347                    self.lift_associated_types.push("*".to_owned());
348                    self.treat_box_as_builtin = true;
349                    self.ops_to_function_calls = true;
350                    self.index_to_function_calls = true;
351                    self.reconstruct_fallible_operations = true;
352                    self.reconstruct_asserts = true;
353                    self.hide_marker_traits = true;
354                    self.hide_allocator = true;
355                    self.remove_unused_self_clauses = true;
356                    self.remove_adt_clauses = true;
357                    self.unbind_item_vars = true;
358                    // Hide drop impls because they often involve nested borrows. which aeneas
359                    // doesn't handle yet.
360                    self.exclude.push("core::ops::drop::Drop".to_owned());
361                    self.exclude
362                        .push("{impl core::ops::drop::Drop for _}".to_owned());
363                }
364                Preset::Eurydice => {
365                    self.hide_allocator = true;
366                    self.treat_box_as_builtin = true;
367                    self.ops_to_function_calls = true;
368                    self.index_to_function_calls = true;
369                    self.reconstruct_fallible_operations = true;
370                    self.reconstruct_asserts = true;
371                    self.lift_associated_types.push("*".to_owned());
372                    self.unbind_item_vars = true;
373                    // Eurydice doesn't support opaque vtables it seems?
374                    self.include.push("core::marker::MetaSized".to_owned());
375                }
376                Preset::Soteria => {
377                    self.extract_opaque_bodies = true;
378                    self.monomorphize = true;
379                    self.mir = Some(MirLevel::Elaborated);
380                    self.ullbc = true;
381                }
382                Preset::Tests => {
383                    self.no_dedup_serialized_ast = true; // Helps debug
384                    self.treat_box_as_builtin = true;
385                    self.hide_allocator = true;
386                    self.reconstruct_fallible_operations = true;
387                    self.reconstruct_asserts = true;
388                    self.ops_to_function_calls = true;
389                    self.index_to_function_calls = true;
390                    self.rustc_args.push("--edition=2021".to_owned());
391                    self.rustc_args
392                        .push("-Zcrate-attr=feature(register_tool)".to_owned());
393                    self.rustc_args
394                        .push("-Zcrate-attr=register_tool(charon)".to_owned());
395                    self.exclude.push("core::fmt::Formatter".to_owned());
396                }
397            }
398        }
399    }
400
401    /// Check that the options are meaningful
402    pub fn validate(&self) -> anyhow::Result<()> {
403        if self.dest_dir.is_some() {
404            display_unspanned_error(
405                Level::WARNING,
406                "`--dest` is deprecated, use `--dest-file` instead",
407            )
408        }
409
410        if self.remove_adt_clauses && self.lift_associated_types.is_empty() {
411            anyhow::bail!(
412                "`--remove-adt-clauses` should be used with `--remove-associated-types='*'` \
413                to avoid missing clause errors",
414            )
415        }
416        if matches!(self.monomorphize_mut, Some(MonomorphizeMut::ExceptTypes))
417            && !self.remove_adt_clauses
418        {
419            anyhow::bail!(
420                "`--monomorphize-mut=except-types` should be used with `--remove-adt-clauses` \
421                to avoid generics mismatches"
422            )
423        }
424        Ok(())
425    }
426
427    pub fn target_filename(&self, crate_name: &str) -> PathBuf {
428        match self.dest_file.clone() {
429            Some(f) => f,
430            None => {
431                let mut target_filename = self.dest_dir.clone().unwrap_or_default();
432                let extension = if self.ullbc { "ullbc" } else { "llbc" };
433                target_filename.push(format!("{crate_name}.{extension}"));
434                target_filename
435            }
436        }
437    }
438}
439
440/// Predicates that determine wihch items to use as starting point for translation.
441#[derive(Debug, Clone, EnumAsGetters)]
442pub enum StartFrom {
443    /// Item identified by a pattern/path. If strict is true, then failing to
444    /// find an item matching the pattern is an error; otherwise, we just ignore this pattern.
445    Pattern { pattern: NamePattern, strict: bool },
446    /// Item annotated with the given attribute.
447    Attribute(String),
448    /// Item marked `pub`. Note that this does not take accessibility into account; a
449    /// non-reexported `pub` item will be included here.
450    Pub,
451}
452
453impl StartFrom {
454    pub fn matches(&self, ctx: &TranslatedCrate, item_meta: &ItemMeta) -> bool {
455        match self {
456            StartFrom::Pattern { pattern, .. } => pattern.matches(ctx, &item_meta.name),
457            StartFrom::Attribute(attr) => item_meta
458                .attr_info
459                .attributes
460                .iter()
461                .filter_map(|a| a.as_unknown())
462                .any(|raw_attr| raw_attr.path == *attr),
463            StartFrom::Pub => item_meta.attr_info.public,
464        }
465    }
466}
467
468/// The options that control translation and transformation.
469pub struct TranslateOptions {
470    /// Items from which to start translation.
471    pub start_from: Vec<StartFrom>,
472    /// The level at which to extract the MIR
473    pub mir_level: MirLevel,
474    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
475    /// them all.
476    pub translate_all_methods: bool,
477    /// If `Some(_)`, run the partial mutability monomorphization pass. The contained enum
478    /// indicates whether to partially monomorphize types.
479    pub monomorphize_mut: Option<MonomorphizeMut>,
480    /// Whether to hide various marker traits such as `Sized`, `Sync`, `Send` and `Destruct`
481    /// anywhere they show up.
482    pub hide_marker_traits: bool,
483    /// Remove trait clauses attached to type declarations.
484    pub remove_adt_clauses: bool,
485    /// Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
486    pub hide_allocator: bool,
487    /// Remove unused `Self: Trait` clauses on method declarations.
488    pub remove_unused_self_clauses: bool,
489    /// Monomorphize code using hax's instantiation mechanism.
490    pub monomorphize_with_hax: bool,
491    /// Transform array-to-slice unsizing, repeat expressions, and raw pointer construction into
492    /// builtin functions in ULLBC.
493    pub ops_to_function_calls: bool,
494    /// Transform array/slice indexing into builtin functions in ULLBC.
495    pub index_to_function_calls: bool,
496    /// Print the llbc just after control-flow reconstruction.
497    pub print_built_llbc: bool,
498    /// Treat `Box<T>` as if it was a built-in type.
499    pub treat_box_as_builtin: bool,
500    /// Don't inline or evaluate constants.
501    pub raw_consts: bool,
502    /// Replace string literal constants with a constant u8 array that gets unsized,
503    /// expliciting the fact a string constant has a hidden reference.
504    pub unsized_strings: bool,
505    /// Replace "bound checks followed by UB-on-overflow operation" with the corresponding
506    /// panic-on-overflow operation. This loses unwinding information.
507    pub reconstruct_fallible_operations: bool,
508    /// Replace `if x { panic() }` with `assert(x)`.
509    pub reconstruct_asserts: bool,
510    // Use `DeBruijnVar::Free` for the variables bound in item signatures.
511    pub unbind_item_vars: bool,
512    /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions`
513    /// field.
514    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
515    /// List of traits for which we transform associated types to type parameters.
516    pub lift_associated_types: Vec<NamePattern>,
517    /// Transform Drop to Call drop_in_place
518    pub desugar_drops: bool,
519    /// Add `Destruct` bounds to all generic params.
520    pub add_destruct_bounds: bool,
521    /// Translate drop glue for poly types, knowing that this may cause ICEs.
522    pub translate_poly_drop_glue: bool,
523}
524
525impl TranslateOptions {
526    pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
527        let mut parse_pattern = |s: &str| -> Result<_, Error> {
528            match NamePattern::parse(s) {
529                Ok(p) => Ok(p),
530                Err(e) => raise_error!(error_ctx, no_crate, "failed to parse pattern `{s}` ({e})"),
531            }
532        };
533
534        let mut mir_level = options.mir.unwrap_or(MirLevel::Promoted);
535        if options.precise_drops {
536            mir_level = std::cmp::max(mir_level, MirLevel::Elaborated);
537        }
538
539        let mut start_from = options
540            .start_from
541            .iter()
542            .filter_map(|path| parse_pattern(path).ok())
543            .map(|p| StartFrom::Pattern {
544                pattern: p,
545                strict: true,
546            })
547            .collect_vec();
548        start_from.extend(
549            options
550                .start_from_if_exists
551                .iter()
552                .filter_map(|path| parse_pattern(path).ok())
553                .map(|p| StartFrom::Pattern {
554                    pattern: p,
555                    strict: false,
556                }),
557        );
558        if let Some(attr) = options.start_from_attribute.clone() {
559            start_from.push(StartFrom::Attribute(attr));
560        }
561        if options.start_from_pub {
562            start_from.push(StartFrom::Pub);
563        }
564        if start_from.is_empty() {
565            start_from.push(StartFrom::Pattern {
566                pattern: parse_pattern("crate").unwrap(),
567                strict: true,
568            });
569        }
570
571        let item_opacities = {
572            use ItemOpacity::*;
573            let mut opacities = vec![];
574
575            // This is how to treat items that don't match any other pattern.
576            if options.extract_opaque_bodies {
577                opacities.push(("_".to_string(), Transparent));
578            } else {
579                opacities.push(("_".to_string(), Foreign));
580            }
581
582            // We always include the items from the crate.
583            opacities.push(("crate".to_owned(), Transparent));
584
585            for pat in options.include.iter() {
586                opacities.push((pat.to_string(), Transparent));
587            }
588            for pat in options.opaque.iter() {
589                opacities.push((pat.to_string(), Opaque));
590            }
591            for pat in options.exclude.iter() {
592                opacities.push((pat.to_string(), Invisible));
593            }
594
595            if options.hide_allocator {
596                opacities.push(("core::alloc::Allocator".to_string(), Invisible));
597                opacities.push((
598                    "alloc::alloc::{impl core::alloc::Allocator for _}".to_string(),
599                    Invisible,
600                ));
601            }
602
603            opacities
604                .into_iter()
605                .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
606                .collect()
607        };
608
609        let lift_associated_types = options
610            .lift_associated_types
611            .iter()
612            .filter_map(|s| parse_pattern(s).ok())
613            .collect();
614
615        TranslateOptions {
616            start_from,
617            mir_level,
618            monomorphize_mut: options.monomorphize_mut,
619            hide_marker_traits: options.hide_marker_traits,
620            remove_adt_clauses: options.remove_adt_clauses,
621            hide_allocator: options.hide_allocator,
622            remove_unused_self_clauses: options.remove_unused_self_clauses,
623            monomorphize_with_hax: options.monomorphize,
624            ops_to_function_calls: options.ops_to_function_calls,
625            index_to_function_calls: options.index_to_function_calls,
626            print_built_llbc: options.print_built_llbc,
627            item_opacities,
628            treat_box_as_builtin: options.treat_box_as_builtin,
629            raw_consts: options.raw_consts,
630            unsized_strings: options.unsized_strings,
631            reconstruct_fallible_operations: options.reconstruct_fallible_operations,
632            reconstruct_asserts: options.reconstruct_asserts,
633            lift_associated_types,
634            unbind_item_vars: options.unbind_item_vars,
635            translate_all_methods: options.translate_all_methods,
636            desugar_drops: options.desugar_drops,
637            add_destruct_bounds: options.precise_drops,
638            translate_poly_drop_glue: options.precise_drops,
639        }
640    }
641
642    /// Find the opacity requested for the given name. This does not take into account
643    /// `#[charon::opaque]` annotations, only cli parameters.
644    #[tracing::instrument(skip(self, krate), ret)]
645    pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
646        // Find the most precise pattern that matches this name. There is always one since
647        // the list contains the `_` pattern. If there are conflicting settings for this item, we
648        // err on the side of being more opaque.
649        let (_, opacity) = self
650            .item_opacities
651            .iter()
652            .filter(|(pat, _)| pat.matches(krate, name))
653            .max()
654            .unwrap();
655        *opacity
656    }
657}