1use annotate_snippets::Level;
3use clap::ValueEnum;
4use indoc::indoc;
5use serde::{Deserialize, Serialize};
6use std::path::PathBuf;
7
8use crate::{
9 ast::*,
10 errors::{ErrorCtx, display_unspanned_error},
11 name_matcher::NamePattern,
12 raise_error, register_error,
13};
14
15pub const CHARON_ARGS: &str = "CHARON_ARGS";
18
19#[derive(Debug, Default, Clone, clap::Args, PartialEq, Eq, Serialize, Deserialize)]
28#[clap(name = "Charon")]
29#[charon::rename("cli_options")]
30pub struct CliOpts {
31 #[clap(long = "ullbc")]
33 #[serde(default)]
34 pub ullbc: bool,
35 #[clap(long = "lib")]
37 #[serde(default)]
38 pub lib: bool,
39 #[clap(long = "bin")]
41 #[serde(default)]
42 pub bin: Option<String>,
43 #[clap(long = "mir_promoted")]
45 #[serde(default)]
46 pub mir_promoted: bool,
47 #[clap(long = "mir_optimized")]
49 #[serde(default)]
50 pub mir_optimized: bool,
51 #[arg(long)]
54 pub mir: Option<MirLevel>,
55 #[clap(long = "input", value_parser)]
59 #[serde(default)]
60 pub input_file: Option<PathBuf>,
61 #[clap(long = "read-llbc", value_parser)]
63 #[serde(default)]
64 pub read_llbc: Option<PathBuf>,
65 #[clap(long = "dest", value_parser)]
68 #[serde(default)]
69 pub dest_dir: Option<PathBuf>,
70 #[clap(long = "dest-file", value_parser)]
73 #[serde(default)]
74 pub dest_file: Option<PathBuf>,
75 #[clap(long = "polonius")]
78 #[serde(default)]
79 pub use_polonius: bool,
80 #[clap(long = "skip-borrowck")]
82 #[serde(default)]
83 pub skip_borrowck: bool,
84 #[clap(long, visible_alias = "mono")]
88 #[serde(default)]
89 pub monomorphize: bool,
90 #[clap(
94 long,
95 value_name("INCLUDE_TYPES"),
96 num_args(0..=1),
97 require_equals(true),
98 default_missing_value("all"),
99 )]
100 #[serde(default)]
101 pub monomorphize_mut: Option<MonomorphizeMut>,
102 #[clap(long = "extract-opaque-bodies")]
105 #[serde(default)]
106 pub extract_opaque_bodies: bool,
107 #[clap(long = "translate-all-methods")]
110 #[serde(default)]
111 pub translate_all_methods: bool,
112 #[clap(
114 long = "include",
115 help = indoc!("
116 Whitelist of items to translate. These use the name-matcher syntax (note: this differs
117 a bit from the ocaml NameMatcher).
118
119 Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
120 built-in type. It is also not possible to filter a trait impl (this will only filter
121 its methods). Please report bugs or missing features.
122
123 Examples:
124 - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
125 submodules or trait methods);
126 - `crate::module1::module2::item::_`: refers only to the subitems of this item;
127 - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
128 very useful impl;
129
130 When multiple patterns in the `--include` and `--opaque` options match the same item,
131 the most precise pattern wins. E.g.: `charon --opaque crate::module --include
132 crate::module::_` makes the `module` opaque (we won't explore its contents), but the
133 items in it transparent (we will translate them if we encounter them.)
134 "))]
135 #[serde(default)]
136 #[charon::rename("included")]
137 pub include: Vec<String>,
138 #[clap(
140 long = "opaque",
141 help = "Blacklist of items to keep opaque. Works just like `--include`, see the doc there."
142 )]
143 #[serde(default)]
144 pub opaque: Vec<String>,
145 #[clap(
147 long = "exclude",
148 help = "Blacklist of items to not translate at all. Works just like `--include`, see the doc there."
149 )]
150 #[serde(default)]
151 pub exclude: Vec<String>,
152 #[clap(
154 long = "remove-associated-types",
155 help = "List of traits for which we transform associated types to type parameters. \
156 The syntax is like `--include`, see the doc there."
157 )]
158 #[serde(default)]
159 pub remove_associated_types: Vec<String>,
160 #[clap(long = "hide-marker-traits")]
163 #[serde(default)]
164 pub hide_marker_traits: bool,
165 #[clap(long)]
167 #[serde(default)]
168 pub hide_allocator: bool,
169 #[clap(long)]
174 #[serde(default)]
175 pub remove_unused_self_clauses: bool,
176 #[clap(long)]
179 #[serde(default)]
180 pub add_drop_bounds: bool,
181 #[clap(long = "start-from")]
185 #[serde(default)]
186 pub start_from: Vec<String>,
187 #[clap(long = "no-cargo")]
189 #[serde(default)]
190 pub no_cargo: bool,
191 #[clap(long = "rustc-flag", alias = "rustc-arg")]
193 #[serde(default)]
194 pub rustc_args: Vec<String>,
195 #[clap(long = "cargo-arg")]
197 #[serde(default)]
198 pub cargo_args: Vec<String>,
199 #[clap(long = "abort-on-error")]
201 #[serde(default)]
202 pub abort_on_error: bool,
203 #[clap(long = "error-on-warnings", help = "Consider any warnings as errors")]
205 #[serde(default)]
206 pub error_on_warnings: bool,
207 #[clap(
208 long = "no-serialize",
209 help = "Don't serialize the final (U)LLBC to a file."
210 )]
211 #[serde(default)]
212 pub no_serialize: bool,
213 #[clap(
214 long = "print-original-ullbc",
215 help = "Print the ULLBC immediately after extraction from MIR."
216 )]
217 #[serde(default)]
218 pub print_original_ullbc: bool,
219 #[clap(
220 long = "print-ullbc",
221 help = "Print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction)."
222 )]
223 #[serde(default)]
224 pub print_ullbc: bool,
225 #[clap(
226 long = "print-built-llbc",
227 help = "Print the LLBC just after we built it (i.e., immediately after loop reconstruction)."
228 )]
229 #[serde(default)]
230 pub print_built_llbc: bool,
231 #[clap(
232 long = "print-llbc",
233 help = "Print the final LLBC (after all the cleaning micro-passes)."
234 )]
235 #[serde(default)]
236 pub print_llbc: bool,
237 #[clap(
238 long = "no-merge-goto-chains",
239 help = "Do not merge the chains of gotos in the ULLBC control-flow graph."
240 )]
241 #[serde(default)]
242 pub no_merge_goto_chains: bool,
243
244 #[clap(
245 long = "no-ops-to-function-calls",
246 help = "Do not transform ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls for ULLBC"
247 )]
248 #[serde(default)]
249 pub no_ops_to_function_calls: bool,
250
251 #[clap(
252 long = "raw-boxes",
253 help = "Do not special-case the translation of `Box<T>` into a builtin ADT."
254 )]
255 #[serde(default)]
256 pub raw_boxes: bool,
257
258 #[clap(long = "preset")]
261 #[arg(value_enum)]
262 pub preset: Option<Preset>,
263}
264
265#[derive(
268 Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
269)]
270pub enum MirLevel {
271 #[default]
273 Built,
274 Promoted,
276 Elaborated,
279 Optimized,
282}
283
284#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
287#[non_exhaustive]
288pub enum Preset {
289 OldDefaults,
292 Aeneas,
293 Eurydice,
294 Soteria,
295 Tests,
296}
297
298#[derive(
299 Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
300)]
301pub enum MonomorphizeMut {
302 #[default]
304 All,
305 ExceptTypes,
307}
308
309impl CliOpts {
310 pub fn apply_preset(&mut self) {
311 if let Some(preset) = self.preset {
312 match preset {
313 Preset::OldDefaults => {
314 self.hide_allocator = !self.raw_boxes;
315 }
316 Preset::Aeneas => {
317 self.remove_associated_types.push("*".to_owned());
318 self.hide_marker_traits = true;
319 self.hide_allocator = true;
320 self.remove_unused_self_clauses = true;
321 self.exclude.push("core::ops::drop::Drop".to_owned());
324 self.exclude
325 .push("{impl core::ops::drop::Drop for _}".to_owned());
326 }
327 Preset::Eurydice => {
328 self.hide_allocator = true;
329 self.remove_associated_types.push("*".to_owned());
330 }
331 Preset::Soteria => {
332 self.extract_opaque_bodies = true;
333 self.monomorphize = true;
334 self.raw_boxes = true;
335 self.mir = Some(MirLevel::Elaborated);
336 self.ullbc = true;
337 }
338 Preset::Tests => {
339 self.hide_allocator = !self.raw_boxes;
340 self.rustc_args.push("--edition=2021".to_owned());
341 self.rustc_args
342 .push("-Zcrate-attr=feature(register_tool)".to_owned());
343 self.rustc_args
344 .push("-Zcrate-attr=register_tool(charon)".to_owned());
345 self.exclude.push("core::fmt::Formatter".to_owned());
346 }
347 }
348 }
349 }
350
351 pub fn validate(&self) {
353 assert!(
354 !self.lib || self.bin.is_none(),
355 "Can't use --lib and --bin at the same time"
356 );
357
358 assert!(
359 !self.mir_promoted || !self.mir_optimized,
360 "Can't use --mir_promoted and --mir_optimized at the same time"
361 );
362
363 if self.input_file.is_some() {
364 display_unspanned_error(
365 Level::WARNING,
366 "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
367 )
368 }
369 if self.no_cargo {
370 display_unspanned_error(
371 Level::WARNING,
372 "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
373 )
374 }
375 if self.read_llbc.is_some() {
376 display_unspanned_error(
377 Level::WARNING,
378 "`--read_llbc` is deprecated, use `charon pretty-print <input file>` instead",
379 )
380 }
381 if self.use_polonius {
382 display_unspanned_error(
383 Level::WARNING,
384 "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead",
385 )
386 }
387 if self.mir_optimized {
388 display_unspanned_error(
389 Level::WARNING,
390 "`--mir_optimized` is deprecated, use `--mir optimized` instead",
391 )
392 }
393 if self.mir_promoted {
394 display_unspanned_error(
395 Level::WARNING,
396 "`--mir_promoted` is deprecated, use `--mir promoted` instead",
397 )
398 }
399 if self.lib {
400 display_unspanned_error(
401 Level::WARNING,
402 "`--lib` is deprecated, use `charon cargo -- --lib` instead",
403 )
404 }
405 if self.bin.is_some() {
406 display_unspanned_error(
407 Level::WARNING,
408 "`--bin` is deprecated, use `charon cargo -- --bin <name>` instead",
409 )
410 }
411 if self.dest_dir.is_some() {
412 display_unspanned_error(
413 Level::WARNING,
414 "`--dest` is deprecated, use `--dest-file` instead",
415 )
416 }
417 }
418}
419
420pub struct TranslateOptions {
422 pub mir_level: MirLevel,
424 pub translate_all_methods: bool,
427 pub monomorphize_mut: Option<MonomorphizeMut>,
430 pub hide_marker_traits: bool,
433 pub hide_allocator: bool,
435 pub remove_unused_self_clauses: bool,
437 pub monomorphize_with_hax: bool,
439 pub no_ops_to_function_calls: bool,
441 pub no_merge_goto_chains: bool,
443 pub print_built_llbc: bool,
445 pub raw_boxes: bool,
447 pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
450 pub remove_associated_types: Vec<NamePattern>,
452}
453
454impl TranslateOptions {
455 pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
456 let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
457 Ok(p) => Ok(p),
458 Err(e) => {
459 raise_error!(
460 error_ctx,
461 crate(&TranslatedCrate::default()),
462 Span::dummy(),
463 "failed to parse pattern `{s}` ({e})"
464 )
465 }
466 };
467
468 let mir_level = if options.mir_optimized {
469 MirLevel::Optimized
470 } else if options.mir_promoted {
471 MirLevel::Promoted
472 } else {
473 options.mir.unwrap_or_default()
474 };
475
476 let item_opacities = {
477 use ItemOpacity::*;
478 let mut opacities = vec![];
479
480 if options.extract_opaque_bodies {
482 opacities.push(("_".to_string(), Transparent));
483 } else {
484 opacities.push(("_".to_string(), Foreign));
485 }
486
487 opacities.push(("crate".to_owned(), Transparent));
489
490 for pat in options.include.iter() {
491 opacities.push((pat.to_string(), Transparent));
492 }
493 for pat in options.opaque.iter() {
494 opacities.push((pat.to_string(), Opaque));
495 }
496 for pat in options.exclude.iter() {
497 opacities.push((pat.to_string(), Invisible));
498 }
499
500 if options.hide_allocator {
501 opacities.push((format!("core::alloc::Allocator"), Invisible));
502 opacities.push((
503 format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
504 Invisible,
505 ));
506 }
507
508 opacities
509 .into_iter()
510 .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
511 .collect()
512 };
513
514 let remove_associated_types = options
515 .remove_associated_types
516 .iter()
517 .filter_map(|s| parse_pattern(&s).ok())
518 .collect();
519
520 TranslateOptions {
521 mir_level,
522 monomorphize_mut: options.monomorphize_mut,
523 hide_marker_traits: options.hide_marker_traits,
524 hide_allocator: options.hide_allocator,
525 remove_unused_self_clauses: options.remove_unused_self_clauses,
526 monomorphize_with_hax: options.monomorphize,
527 no_merge_goto_chains: options.no_merge_goto_chains,
528 no_ops_to_function_calls: options.no_ops_to_function_calls,
529 print_built_llbc: options.print_built_llbc,
530 item_opacities,
531 raw_boxes: options.raw_boxes,
532 remove_associated_types,
533 translate_all_methods: options.translate_all_methods,
534 }
535 }
536
537 #[tracing::instrument(skip(self, krate), ret)]
540 pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
541 let (_, opacity) = self
545 .item_opacities
546 .iter()
547 .filter(|(pat, _)| pat.matches(krate, name))
548 .max()
549 .unwrap();
550 *opacity
551 }
552}