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::{display_unspanned_error, ErrorCtx},
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, 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 = "monomorphize")]
86 #[serde(default)]
87 pub monomorphize: bool,
88 #[clap(long = "extract-opaque-bodies")]
91 #[serde(default)]
92 pub extract_opaque_bodies: bool,
93 #[clap(long = "translate-all-methods")]
96 #[serde(default)]
97 pub translate_all_methods: bool,
98 #[clap(
100 long = "include",
101 help = indoc!("
102 Whitelist of items to translate. These use the name-matcher syntax (note: this differs
103 a bit from the ocaml NameMatcher).
104
105 Note: This is very rough at the moment. E.g. this parses `u64` as a path instead of the
106 built-in type. It is also not possible to filter a trait impl (this will only filter
107 its methods). Please report bugs or missing features.
108
109 Examples:
110 - `crate::module1::module2::item`: refers to this item and all its subitems (e.g.
111 submodules or trait methods);
112 - `crate::module1::module2::item::_`: refers only to the subitems of this item;
113 - `core::convert::{impl core::convert::Into<_> for _}`: retrieve the body of this
114 very useful impl;
115
116 When multiple patterns in the `--include` and `--opaque` options match the same item,
117 the most precise pattern wins. E.g.: `charon --opaque crate::module --include
118 crate::module::_` makes the `module` opaque (we won't explore its contents), but the
119 items in it transparent (we will translate them if we encounter them.)
120 "))]
121 #[serde(default)]
122 #[charon::rename("included")]
123 pub include: Vec<String>,
124 #[clap(
126 long = "opaque",
127 help = "Blacklist of items to keep opaque. Works just like `--include`, see the doc there."
128 )]
129 #[serde(default)]
130 pub opaque: Vec<String>,
131 #[clap(
133 long = "exclude",
134 help = "Blacklist of items to not translate at all. Works just like `--include`, see the doc there."
135 )]
136 #[serde(default)]
137 pub exclude: Vec<String>,
138 #[clap(
140 long = "remove-associated-types",
141 help = "List of traits for which we transform associated types to type parameters. \
142 The syntax is like `--include`, see the doc there."
143 )]
144 #[serde(default)]
145 pub remove_associated_types: Vec<String>,
146 #[clap(long = "hide-marker-traits")]
149 #[serde(default)]
150 pub hide_marker_traits: bool,
151 #[clap(long)]
156 #[serde(default)]
157 pub remove_unused_self_clauses: bool,
158 #[clap(long = "start-from")]
162 #[serde(default)]
163 pub start_from: Vec<String>,
164 #[clap(long = "no-cargo")]
166 #[serde(default)]
167 pub no_cargo: bool,
168 #[clap(long = "rustc-flag", alias = "rustc-arg")]
170 #[serde(default)]
171 pub rustc_args: Vec<String>,
172 #[clap(long = "cargo-arg")]
174 #[serde(default)]
175 pub cargo_args: Vec<String>,
176 #[clap(long = "abort-on-error")]
178 #[serde(default)]
179 pub abort_on_error: bool,
180 #[clap(long = "error-on-warnings", help = "Consider any warnings as errors")]
182 #[serde(default)]
183 pub error_on_warnings: bool,
184 #[clap(
185 long = "no-serialize",
186 help = "Don't serialize the final (U)LLBC to a file."
187 )]
188 #[serde(default)]
189 pub no_serialize: bool,
190 #[clap(
191 long = "print-original-ullbc",
192 help = "Print the ULLBC immediately after extraction from MIR."
193 )]
194 #[serde(default)]
195 pub print_original_ullbc: bool,
196 #[clap(
197 long = "print-ullbc",
198 help = "Print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction)."
199 )]
200 #[serde(default)]
201 pub print_ullbc: bool,
202 #[clap(
203 long = "print-built-llbc",
204 help = "Print the LLBC just after we built it (i.e., immediately after loop reconstruction)."
205 )]
206 #[serde(default)]
207 pub print_built_llbc: bool,
208 #[clap(
209 long = "print-llbc",
210 help = "Print the final LLBC (after all the cleaning micro-passes)."
211 )]
212 #[serde(default)]
213 pub print_llbc: bool,
214 #[clap(
215 long = "no-merge-goto-chains",
216 help = "Do not merge the chains of gotos in the ULLBC control-flow graph."
217 )]
218 #[serde(default)]
219 pub no_merge_goto_chains: bool,
220
221 #[clap(
222 long = "no-ops-to-function-calls",
223 help = "Do not transform ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls for ULLBC"
224 )]
225 #[serde(default)]
226 pub no_ops_to_function_calls: bool,
227
228 #[clap(
229 long = "raw-boxes",
230 help = "Do not special-case the translation of `Box<T>` into a builtin ADT."
231 )]
232 #[serde(default)]
233 pub raw_boxes: bool,
234
235 #[clap(long = "preset")]
238 #[arg(value_enum)]
239 pub preset: Option<Preset>,
240}
241
242#[derive(
245 Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
246)]
247pub enum MirLevel {
248 #[default]
250 Built,
251 Promoted,
253 Elaborated,
256 Optimized,
259}
260
261#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
264#[non_exhaustive]
265pub enum Preset {
266 OldDefaults,
269 Aeneas,
270 Eurydice,
271 Tests,
272}
273
274impl CliOpts {
275 pub fn apply_preset(&mut self) {
276 if let Some(preset) = self.preset {
277 match preset {
278 Preset::OldDefaults => {}
279 Preset::Aeneas => {
280 self.remove_associated_types.push("*".to_owned());
281 self.hide_marker_traits = true;
282 self.remove_unused_self_clauses = true;
283 }
284 Preset::Eurydice => {
285 self.remove_associated_types.push("*".to_owned());
286 }
287 Preset::Tests => {
288 self.rustc_args.push("--edition=2021".to_owned());
289 }
290 }
291 }
292 }
293
294 pub fn validate(&self) {
296 assert!(
297 !self.lib || self.bin.is_none(),
298 "Can't use --lib and --bin at the same time"
299 );
300
301 assert!(
302 !self.mir_promoted || !self.mir_optimized,
303 "Can't use --mir_promoted and --mir_optimized at the same time"
304 );
305
306 if self.input_file.is_some() {
307 display_unspanned_error(
308 Level::WARNING,
309 "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
310 )
311 }
312 if self.no_cargo {
313 display_unspanned_error(
314 Level::WARNING,
315 "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
316 )
317 }
318 if self.read_llbc.is_some() {
319 display_unspanned_error(
320 Level::WARNING,
321 "`--read_llbc` is deprecated, use `charon pretty-print <input file>` instead",
322 )
323 }
324 if self.use_polonius {
325 display_unspanned_error(
326 Level::WARNING,
327 "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead",
328 )
329 }
330 if self.mir_optimized {
331 display_unspanned_error(
332 Level::WARNING,
333 "`--mir_optimized` is deprecated, use `--mir optimized` instead",
334 )
335 }
336 if self.mir_promoted {
337 display_unspanned_error(
338 Level::WARNING,
339 "`--mir_promoted` is deprecated, use `--mir promoted` instead",
340 )
341 }
342 if self.lib {
343 display_unspanned_error(
344 Level::WARNING,
345 "`--lib` is deprecated, use `charon cargo -- --lib` instead",
346 )
347 }
348 if self.bin.is_some() {
349 display_unspanned_error(
350 Level::WARNING,
351 "`--bin` is deprecated, use `charon cargo -- --bin <name>` instead",
352 )
353 }
354 if self.dest_dir.is_some() {
355 display_unspanned_error(
356 Level::WARNING,
357 "`--dest` is deprecated, use `--dest-file` instead",
358 )
359 }
360 }
361}
362
363pub struct TranslateOptions {
365 pub mir_level: MirLevel,
367 pub translate_all_methods: bool,
370 pub hide_marker_traits: bool,
373 pub remove_unused_self_clauses: bool,
375 pub monomorphize: bool,
377 pub no_ops_to_function_calls: bool,
379 pub no_merge_goto_chains: bool,
381 pub print_built_llbc: bool,
383 pub raw_boxes: bool,
385 pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
388 pub remove_associated_types: Vec<NamePattern>,
390}
391
392impl TranslateOptions {
393 pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
394 let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
395 Ok(p) => Ok(p),
396 Err(e) => {
397 raise_error!(
398 error_ctx,
399 crate(&TranslatedCrate::default()),
400 Span::dummy(),
401 "failed to parse pattern `{s}` ({e})"
402 )
403 }
404 };
405
406 let mir_level = if options.mir_optimized {
407 MirLevel::Optimized
408 } else if options.mir_promoted {
409 MirLevel::Promoted
410 } else {
411 options.mir.unwrap_or_default()
412 };
413
414 let item_opacities = {
415 use ItemOpacity::*;
416 let mut opacities = vec![];
417
418 if options.extract_opaque_bodies {
420 opacities.push(("_".to_string(), Transparent));
421 } else {
422 opacities.push(("_".to_string(), Foreign));
423 }
424
425 opacities.push(("crate".to_owned(), Transparent));
427
428 for pat in options.include.iter() {
429 opacities.push((pat.to_string(), Transparent));
430 }
431 for pat in options.opaque.iter() {
432 opacities.push((pat.to_string(), Opaque));
433 }
434 for pat in options.exclude.iter() {
435 opacities.push((pat.to_string(), Invisible));
436 }
437
438 if !options.raw_boxes {
439 opacities.push((format!("core::alloc::Allocator"), Invisible));
440 opacities.push((
441 format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
442 Invisible,
443 ));
444 }
445
446 opacities
447 .into_iter()
448 .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
449 .collect()
450 };
451
452 let remove_associated_types = options
453 .remove_associated_types
454 .iter()
455 .filter_map(|s| parse_pattern(&s).ok())
456 .collect();
457
458 TranslateOptions {
459 mir_level,
460 hide_marker_traits: options.hide_marker_traits,
461 remove_unused_self_clauses: options.remove_unused_self_clauses,
462 monomorphize: options.monomorphize,
463 no_merge_goto_chains: options.no_merge_goto_chains,
464 no_ops_to_function_calls: options.no_ops_to_function_calls,
465 print_built_llbc: options.print_built_llbc,
466 item_opacities,
467 raw_boxes: options.raw_boxes,
468 remove_associated_types,
469 translate_all_methods: options.translate_all_methods,
470 }
471 }
472
473 pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
476 let (_, opacity) = self
480 .item_opacities
481 .iter()
482 .filter(|(pat, _)| pat.matches(krate, name))
483 .max()
484 .unwrap();
485 *opacity
486 }
487}