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(long = "preset")]
231 #[arg(value_enum)]
232 pub preset: Option<Preset>,
233}
234
235#[derive(
238 Debug, Default, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize,
239)]
240pub enum MirLevel {
241 #[default]
243 Built,
244 Promoted,
246 Elaborated,
249 Optimized,
252}
253
254#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum, Serialize, Deserialize)]
257#[non_exhaustive]
258pub enum Preset {
259 OldDefaults,
262 Aeneas,
263 Eurydice,
264 Tests,
265}
266
267impl CliOpts {
268 pub fn apply_preset(&mut self) {
269 if let Some(preset) = self.preset {
270 match preset {
271 Preset::OldDefaults => {}
272 Preset::Aeneas => {
273 self.remove_associated_types.push("*".to_owned());
274 self.hide_marker_traits = true;
275 self.remove_unused_self_clauses = true;
276 }
277 Preset::Eurydice => {
278 self.remove_associated_types.push("*".to_owned());
279 }
280 Preset::Tests => {
281 self.rustc_args.push("--edition=2021".to_owned());
282 }
283 }
284 }
285 }
286
287 pub fn validate(&self) {
289 assert!(
290 !self.lib || self.bin.is_none(),
291 "Can't use --lib and --bin at the same time"
292 );
293
294 assert!(
295 !self.mir_promoted || !self.mir_optimized,
296 "Can't use --mir_promoted and --mir_optimized at the same time"
297 );
298
299 if self.input_file.is_some() {
300 display_unspanned_error(
301 Level::WARNING,
302 "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
303 )
304 }
305 if self.no_cargo {
306 display_unspanned_error(
307 Level::WARNING,
308 "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] <input file>` instead",
309 )
310 }
311 if self.read_llbc.is_some() {
312 display_unspanned_error(
313 Level::WARNING,
314 "`--read_llbc` is deprecated, use `charon pretty-print <input file>` instead",
315 )
316 }
317 if self.use_polonius {
318 display_unspanned_error(
319 Level::WARNING,
320 "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead",
321 )
322 }
323 if self.mir_optimized {
324 display_unspanned_error(
325 Level::WARNING,
326 "`--mir_optimized` is deprecated, use `--mir optimized` instead",
327 )
328 }
329 if self.mir_promoted {
330 display_unspanned_error(
331 Level::WARNING,
332 "`--mir_promoted` is deprecated, use `--mir promoted` instead",
333 )
334 }
335 if self.lib {
336 display_unspanned_error(
337 Level::WARNING,
338 "`--lib` is deprecated, use `charon cargo -- --lib` instead",
339 )
340 }
341 if self.bin.is_some() {
342 display_unspanned_error(
343 Level::WARNING,
344 "`--bin` is deprecated, use `charon cargo -- --bin <name>` instead",
345 )
346 }
347 if self.dest_dir.is_some() {
348 display_unspanned_error(
349 Level::WARNING,
350 "`--dest` is deprecated, use `--dest-file` instead",
351 )
352 }
353 }
354}
355
356pub struct TranslateOptions {
358 pub mir_level: MirLevel,
360 pub translate_all_methods: bool,
363 pub hide_marker_traits: bool,
366 pub remove_unused_self_clauses: bool,
368 pub monomorphize: bool,
370 pub no_ops_to_function_calls: bool,
372 pub no_merge_goto_chains: bool,
374 pub print_built_llbc: bool,
376 pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
379 pub remove_associated_types: Vec<NamePattern>,
381}
382
383impl TranslateOptions {
384 pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self {
385 let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
386 Ok(p) => Ok(p),
387 Err(e) => {
388 raise_error!(
389 error_ctx,
390 crate(&TranslatedCrate::default()),
391 Span::dummy(),
392 "failed to parse pattern `{s}` ({e})"
393 )
394 }
395 };
396
397 let mir_level = if options.mir_optimized {
398 MirLevel::Optimized
399 } else if options.mir_promoted {
400 MirLevel::Promoted
401 } else {
402 options.mir.unwrap_or_default()
403 };
404
405 let item_opacities = {
406 use ItemOpacity::*;
407 let mut opacities = vec![];
408
409 if options.extract_opaque_bodies {
411 opacities.push(("_".to_string(), Transparent));
412 } else {
413 opacities.push(("_".to_string(), Foreign));
414 }
415
416 opacities.push(("crate".to_owned(), Transparent));
418
419 for pat in options.include.iter() {
420 opacities.push((pat.to_string(), Transparent));
421 }
422 for pat in options.opaque.iter() {
423 opacities.push((pat.to_string(), Opaque));
424 }
425 for pat in options.exclude.iter() {
426 opacities.push((pat.to_string(), Invisible));
427 }
428
429 opacities.push((format!("core::alloc::Allocator"), Invisible));
431 opacities.push((
432 format!("alloc::alloc::{{impl core::alloc::Allocator for _}}"),
433 Invisible,
434 ));
435
436 opacities
437 .into_iter()
438 .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
439 .collect()
440 };
441
442 let remove_associated_types = options
443 .remove_associated_types
444 .iter()
445 .filter_map(|s| parse_pattern(&s).ok())
446 .collect();
447
448 TranslateOptions {
449 mir_level,
450 hide_marker_traits: options.hide_marker_traits,
451 remove_unused_self_clauses: options.remove_unused_self_clauses,
452 monomorphize: options.monomorphize,
453 no_merge_goto_chains: options.no_merge_goto_chains,
454 no_ops_to_function_calls: options.no_ops_to_function_calls,
455 print_built_llbc: options.print_built_llbc,
456 item_opacities,
457 remove_associated_types,
458 translate_all_methods: options.translate_all_methods,
459 }
460 }
461
462 pub fn opacity_for_name(&self, krate: &TranslatedCrate, name: &Name) -> ItemOpacity {
465 let (_, opacity) = self
469 .item_opacities
470 .iter()
471 .filter(|(pat, _)| pat.matches(krate, name))
472 .max()
473 .unwrap();
474 *opacity
475 }
476}