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}