hax_types/cli_options/
mod.rs

1use crate::prelude::*;
2
3use clap::{Parser, Subcommand, ValueEnum};
4use std::fmt;
5
6pub use hax_frontend_exporter_options::*;
7pub mod extension;
8use extension::Extension;
9
10#[derive_group(Serializers)]
11#[derive(JsonSchema, Debug, Clone, Eq, PartialEq)]
12pub enum DebugEngineMode {
13    File(PathOrDash),
14    Interactive,
15}
16
17impl std::convert::From<&str> for DebugEngineMode {
18    fn from(s: &str) -> Self {
19        match s {
20            "i" | "interactively" => DebugEngineMode::Interactive,
21            s => DebugEngineMode::File(s.strip_prefix("file:").unwrap_or(s).into()),
22        }
23    }
24}
25
26#[derive_group(Serializers)]
27#[derive(JsonSchema, Debug, Clone, Default)]
28pub struct ForceCargoBuild {
29    pub data: u64,
30}
31
32impl std::convert::From<&str> for ForceCargoBuild {
33    fn from(s: &str) -> Self {
34        use std::time::{SystemTime, UNIX_EPOCH};
35        if s == "false" {
36            let data = SystemTime::now()
37                .duration_since(UNIX_EPOCH)
38                .map(|r| r.as_millis())
39                .unwrap_or(0);
40            ForceCargoBuild { data: data as u64 }
41        } else {
42            ForceCargoBuild::default()
43        }
44    }
45}
46
47#[derive_group(Serializers)]
48#[derive(Debug, Clone, JsonSchema, Eq, PartialEq)]
49pub enum PathOrDash {
50    Dash,
51    Path(PathBuf),
52}
53
54impl std::convert::From<&str> for PathOrDash {
55    fn from(s: &str) -> Self {
56        match s {
57            "-" => PathOrDash::Dash,
58            _ => PathOrDash::Path(PathBuf::from(s)),
59        }
60    }
61}
62
63impl PathOrDash {
64    pub fn open_or_stdout(&self) -> Box<dyn std::io::Write> {
65        use std::io::BufWriter;
66        match self {
67            PathOrDash::Dash => Box::new(BufWriter::new(std::io::stdout())),
68            PathOrDash::Path(path) => {
69                Box::new(BufWriter::new(std::fs::File::create(&path).unwrap()))
70            }
71        }
72    }
73    pub fn map_path<F: FnOnce(&Path) -> PathBuf>(&self, f: F) -> Self {
74        match self {
75            PathOrDash::Path(path) => PathOrDash::Path(f(path)),
76            PathOrDash::Dash => PathOrDash::Dash,
77        }
78    }
79}
80
81fn absolute_path(path: impl AsRef<std::path::Path>) -> std::io::Result<std::path::PathBuf> {
82    use path_clean::PathClean;
83    let path = path.as_ref();
84
85    let absolute_path = if path.is_absolute() {
86        path.to_path_buf()
87    } else {
88        std::env::current_dir()?.join(path)
89    }
90    .clean();
91
92    Ok(absolute_path)
93}
94
95pub trait NormalizePaths {
96    fn normalize_paths(&mut self);
97}
98
99impl NormalizePaths for PathBuf {
100    fn normalize_paths(&mut self) {
101        *self = absolute_path(&self).unwrap();
102    }
103}
104impl NormalizePaths for PathOrDash {
105    fn normalize_paths(&mut self) {
106        match self {
107            PathOrDash::Path(p) => p.normalize_paths(),
108            PathOrDash::Dash => (),
109        }
110    }
111}
112
113#[derive_group(Serializers)]
114#[derive(JsonSchema, Parser, Debug, Hash, Clone, Eq, PartialEq)]
115pub struct ProVerifOptions {
116    /// Items for which hax should extract a default-valued process
117    /// macro with a corresponding type signature. This flag expects a
118    /// space-separated list of inclusion clauses. An inclusion clause
119    /// is a Rust path prefixed with `+`, `+!` or `-`. `-` means
120    /// implementation only, `+!` means interface only and `+` means
121    /// implementation and interface. Rust path chunks can be either a
122    /// concrete string, or a glob (just like bash globs, but with
123    /// Rust paths).
124    #[arg(
125        long,
126        value_parser = parse_inclusion_clause,
127        value_delimiter = ' ',
128        allow_hyphen_values(true)
129    )]
130    pub assume_items: Vec<InclusionClause>,
131}
132
133#[derive_group(Serializers)]
134#[derive(JsonSchema, Parser, Debug, Hash, Clone, Eq, PartialEq)]
135pub struct FStarOptions {
136    /// Set the Z3 per-query resource limit
137    #[arg(long, default_value = "15")]
138    pub z3rlimit: u32,
139    /// Number of unrolling of recursive functions to try
140    #[arg(long, default_value = "0")]
141    pub fuel: u32,
142    /// Number of unrolling of inductive datatypes to try
143    #[arg(long, default_value = "1")]
144    pub ifuel: u32,
145    /// Modules for which Hax should extract interfaces (`*.fsti`
146    /// files) in supplement to implementations (`*.fst` files). By
147    /// default we extract no interface, only implementations. If a
148    /// item is signature only (see the `+:` prefix of the
149    /// `--include_namespaces` flag of the `into` subcommand), then
150    /// its namespace is extracted with an interface. This flag
151    /// expects a space-separated list of inclusion clauses. An
152    /// inclusion clause is a Rust path prefixed with `+`, `+!` or
153    /// `-`. `-` means implementation only, `+!` means interface only
154    /// and `+` means implementation and interface. Rust path chunks
155    /// can be either a concrete string, or a glob (just like bash
156    /// globs, but with Rust paths).
157    #[arg(
158        long,
159        value_parser = parse_inclusion_clause,
160        value_delimiter = ' ',
161        allow_hyphen_values(true)
162    )]
163    pub interfaces: Vec<InclusionClause>,
164
165    #[arg(long, default_value = "100", env = "HAX_FSTAR_LINE_WIDTH")]
166    pub line_width: u16,
167}
168
169#[derive_group(Serializers)]
170#[derive(JsonSchema, Parser, Debug, Clone, Hash, Eq, PartialEq)]
171#[command(after_help = concat!("\
172TOOLS:
173  This backend runs `charon`, then `aeneas`, and scaffolds a Lean proof project.
174  Each tool is pinned; the pinned version is checked against the resolved binary
175  at runtime (a mismatch is a non-fatal warning).
176
177  charon   expected version   ", env!("HAX_CHARON_PIN_VERSION"), "
178           located at $HAX_CHARON_BINARY (absolute path) if set, else `charon` found in PATH
179  aeneas   expected commit     ", env!("HAX_AENEAS_PIN_VERSION"), "
180           located at $HAX_AENEAS_BINARY (absolute path) if set, else `aeneas` found in PATH
181  lean     expected toolchain  ", env!("HAX_LEAN_PIN_TOOLCHAIN"), "
182           used by the generated proof project (written to its `lean-toolchain`)
183
184  Install charon/aeneas with `install-aeneas.sh`.
185
186INVOCATION:
187  The tools are run with some fixed flags (to which any --charon-args/--aeneas-args
188  are appended). Pass `-v` (`cargo hax into -v lean`) to print the exact command
189  before each tool runs.
190
191  Overriding a flag that controls where output is written (aeneas's -backend,
192  -dest, -subdir, or -split-files, or charon's --dest-file) may break the extraction
193  or the generated proof project.
194
195ENVIRONMENT VARIABLES:
196  HAX_CHARON_BINARY  Path to the `charon` binary to use. Defaults to `charon` found in PATH.
197  HAX_AENEAS_BINARY  Path to the `aeneas` binary to use. Defaults to `aeneas` found in PATH."))]
198pub struct LeanOptions {
199    /// Generate a `lakefile.toml` and `lean-toolchain` in the
200    /// `proofs/lean/` directory, with a dependency on the Aeneas
201    /// Lean library. Existing files are not overwritten, so it is safe
202    /// to re-run with this flag after editing the lakefile.
203    #[arg(long)]
204    pub lakefile: bool,
205
206    /// Extra arguments forwarded to charon. Parsed with shell-style quoting,
207    /// so values containing spaces can be single- or double-quoted.
208    /// Example: --charon-args="--opaque '{impl Serialize for _}'"
209    #[arg(long)]
210    pub charon_args: Option<String>,
211
212    /// Extra arguments forwarded to aeneas. Parsed with shell-style quoting.
213    /// Example: --aeneas-args="-split-files"
214    #[arg(long)]
215    pub aeneas_args: Option<String>,
216}
217
218#[derive_group(Serializers)]
219#[derive(JsonSchema, Subcommand, Debug, Clone, Hash, Eq, PartialEq)]
220pub enum Backend {
221    /// Use the F* backend
222    Fstar(FStarOptions),
223    /// Use the legacy Lean backend (warning: experimental)
224    LegacyLean,
225    /// Use the Lean backend (charon + aeneas pipeline)
226    Lean(LeanOptions),
227    /// Use the Coq backend
228    Coq,
229    /// Use the SSProve backend
230    Ssprove,
231    /// Use the EasyCrypt backend (warning: work in progress!)
232    Easycrypt,
233    /// Use the ProVerif backend (warning: work in progress!)
234    #[clap(alias("proverif"))]
235    ProVerif(ProVerifOptions),
236    /// Use the Rust backend (warning: work in progress!)
237    #[clap(hide = true)]
238    Rust,
239    /// Extract `DefId`s of the crate as a Rust module tree.
240    /// This is a command that regenerates code for the rust engine.
241    #[clap(hide = true)]
242    GenerateRustEngineNames,
243    /// A debugger for the Rust engine
244    Debugger {
245        #[arg(long, short)]
246        interactive: bool,
247    },
248}
249
250impl fmt::Display for Backend {
251    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
252        BackendName::from(self).fmt(f)
253    }
254}
255
256#[derive_group(Serializers)]
257#[derive(JsonSchema, Debug, Hash, Clone, Eq, PartialEq)]
258pub enum DepsKind {
259    Transitive,
260    Shallow,
261    None,
262}
263
264#[derive_group(Serializers)]
265#[derive(JsonSchema, Debug, Hash, Clone, Eq, PartialEq)]
266pub enum InclusionKind {
267    /// `+query` include the items selected by `query`
268    Included(DepsKind),
269    SignatureOnly,
270    Excluded,
271}
272
273#[derive_group(Serializers)]
274#[derive(JsonSchema, Debug, Hash, Clone, Eq, PartialEq)]
275pub struct InclusionClause {
276    pub kind: InclusionKind,
277    pub namespace: Namespace,
278}
279
280const PREFIX_INCLUDED_TRANSITIVE: &str = "+";
281const PREFIX_INCLUDED_SHALLOW: &str = "+~";
282const PREFIX_INCLUDED_NONE: &str = "+!";
283const PREFIX_SIGNATURE_ONLY: &str = "+:";
284const PREFIX_EXCLUDED: &str = "-";
285
286impl ToString for InclusionClause {
287    fn to_string(&self) -> String {
288        let kind = match self.kind {
289            InclusionKind::Included(DepsKind::Transitive) => PREFIX_INCLUDED_TRANSITIVE,
290            InclusionKind::Included(DepsKind::Shallow) => PREFIX_INCLUDED_SHALLOW,
291            InclusionKind::Included(DepsKind::None) => PREFIX_INCLUDED_NONE,
292            InclusionKind::SignatureOnly => PREFIX_SIGNATURE_ONLY,
293            InclusionKind::Excluded => PREFIX_EXCLUDED,
294        };
295        format!("{kind}{}", self.namespace.to_string())
296    }
297}
298
299pub fn parse_inclusion_clause(
300    s: &str,
301) -> Result<InclusionClause, Box<dyn std::error::Error + Send + Sync + 'static>> {
302    let s = s.trim();
303    if s.is_empty() {
304        Err("Expected `-` or `+`, got an empty string")?
305    }
306    let (prefix, namespace) = {
307        let f = |&c: &char| matches!(c, '+' | '-' | '~' | '!' | ':');
308        (
309            s.chars().take_while(f).into_iter().collect::<String>(),
310            s.chars().skip_while(f).into_iter().collect::<String>(),
311        )
312    };
313    let kind = match &prefix[..] {
314        PREFIX_INCLUDED_TRANSITIVE => InclusionKind::Included(DepsKind::Transitive),
315        PREFIX_INCLUDED_SHALLOW => InclusionKind::Included(DepsKind::Shallow),
316        PREFIX_INCLUDED_NONE => InclusionKind::Included(DepsKind::None),
317        PREFIX_SIGNATURE_ONLY => InclusionKind::SignatureOnly,
318        PREFIX_EXCLUDED => InclusionKind::Excluded,
319        prefix => Err(format!(
320            "Expected `+`, `+~`, `+!`, `+:` or `-`, got an `{prefix}`"
321        ))?,
322    };
323    Ok(InclusionClause {
324        kind,
325        namespace: namespace.to_string().into(),
326    })
327}
328
329#[derive_group(Serializers)]
330#[derive(JsonSchema, Parser, Debug, Clone, Eq, PartialEq)]
331pub struct TranslationOptions {
332    /// Controls which Rust item should be extracted or not.
333    ///
334    /// This is a space-separated list of patterns prefixed with a
335    /// modifier, read from the left to the right.
336    ///
337    /// A pattern is a Rust path (say `mycrate::mymod::myfn`) where
338    /// globs are allowed: `*` matches any name
339    /// (e.g. `mycrate::mymod::myfn` is matched by
340    /// `mycrate::*::myfn`), while `**` matches any subpath, empty
341    /// included (e.g. `mycrate::mymod::myfn` is matched by
342    /// `**::myfn`).
343
344    /// By default, hax includes all items. Then, the patterns
345    /// prefixed by modifiers are processed from left to right,
346    /// excluding or including items. Each pattern selects a number of
347    /// item. The modifiers are:
348
349    /// {n}{n} - `+`: includes the selected items with their
350    /// dependencies, transitively (e.g. if function `f` calls `g`
351    /// which in turn calls `h`, then `+k::f` includes `f`, `g` and
352    /// `h`)
353
354    /// {n} - `+~`: includes the selected items with their direct
355    /// dependencies only (following the previous example, `+~k::f`
356    /// would select `f` and `g`, but not `h`)
357
358    /// {n} - `+!`: includes the selected items, without their
359    /// dependencies (`+!k::f` would only select `f`)
360
361    /// {n} - `+:`: only includes the type of the selected items (no
362    /// dependencies). This includes full struct and enums, but only
363    /// the type signature of functions and trait impls (except when
364    /// they contain associated types), dropping their bodies.
365    #[arg(
366        value_parser = parse_inclusion_clause,
367        value_delimiter = ' ',
368    )]
369    #[arg(short, allow_hyphen_values(true))]
370    pub include_namespaces: Vec<InclusionClause>,
371}
372
373#[derive_group(Serializers)]
374#[derive(JsonSchema, Parser, Debug, Clone, Eq, PartialEq)]
375pub struct BackendOptions<E: Extension> {
376    #[command(subcommand)]
377    pub backend: Backend,
378
379    /// Don't write anything on disk. Output everything as JSON to stdout
380    /// instead.
381    #[arg(long = "dry-run")]
382    pub dry_run: bool,
383
384    /// Verbose mode for the Hax engine. Set `-vv` for maximal verbosity.
385    #[arg(short, long, action = clap::ArgAction::Count)]
386    pub verbose: u8,
387
388    /// Prints statistics about how many items have been translated
389    /// successfully by the engine.
390    #[arg(long)]
391    pub stats: bool,
392
393    /// Enables profiling for the engine: for each phase of the
394    /// engine, time and memory usage are recorded and reported.
395    #[arg(long)]
396    pub profile: bool,
397
398    /// Prune Rust items that are not under the provided top-level module name.
399    /// This will effectively remove all items that don't match `*::<prune_haxmetadata>::**`.
400    /// This prunning occurs directly on the `haxmeta` file, in the frontend.
401    /// This is independent from any engine options.
402    #[arg(long)]
403    #[clap(hide = true)]
404    pub prune_haxmeta: Option<String>,
405
406    /// Enable engine debugging: dumps the AST at each phase.
407    ///
408    /// The value of `<DEBUG_ENGINE>` can be either:
409
410    /// {n}{n} - `interactive` (or `i`): enables debugging of the engine,
411    /// and visualize interactively in a webapp how a crate was
412    /// transformed by each phase, both in Rust-like syntax and
413    /// browsing directly the internal AST. By default, the webapp is
414    /// hosted on `http://localhost:8000`, the port can be override by
415    /// setting the `HAX_DEBUGGER_PORT` environment variable.
416
417    /// {n} - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
418    /// to `<FILE>`. `<FILE>` can be either [-] or a path.
419    #[arg(short, long = "debug-engine")]
420    pub debug_engine: Option<DebugEngineMode>,
421
422    /// Extract type aliases. This is disabled by default, since
423    /// extracted terms depends on expanded types rather than on type
424    /// aliases. Turning this option on is discouraged: Rust type
425    /// synonyms can ommit generic bounds, which are ususally
426    /// necessary in the hax backends, leading to typechecking
427    /// errors. For more details see
428    /// https://github.com/hacspec/hax/issues/708.
429    #[arg(long)]
430    pub extract_type_aliases: bool,
431
432    #[command(flatten)]
433    pub translation_options: TranslationOptions,
434
435    /// Where to put the output files resulting from the translation.
436    /// Defaults to "<crate folder>/proofs/<backend>/extraction".
437    #[arg(long)]
438    pub output_dir: Option<PathBuf>,
439
440    #[group(flatten)]
441    pub cli_extension: E::BackendOptions,
442}
443
444#[derive_group(Serializers)]
445#[derive(JsonSchema, Subcommand, Debug, Clone, Eq, PartialEq)]
446pub enum Command<E: Extension> {
447    /// Translate to a backend. The translated modules will be written
448    /// under the directory `<PKG>/proofs/<BACKEND>/extraction`, where
449    /// `<PKG>` is the translated cargo package name and `<BACKEND>`
450    /// the name of the backend.
451    #[clap(name = "into")]
452    Backend(BackendOptions<E>),
453
454    /// Export directly as a JSON file
455    JSON {
456        /// Path to the output JSON file, "-" denotes stdout.
457        #[arg(
458            short,
459            long = "output-file",
460            default_value = "hax_frontend_export.json"
461        )]
462        output_file: PathOrDash,
463        /// Whether the bodies are exported as THIR, built MIR, const
464        /// MIR, or a combination. Repeat this option to extract a
465        /// combination (e.g. `-k thir -k mir-built`). Pass `--kind`
466        /// alone with no value to disable body extraction.
467        #[arg(
468            value_enum,
469            short,
470            long = "kind",
471            num_args = 0..=3,
472            default_values_t = [ExportBodyKind::Thir]
473        )]
474        kind: Vec<ExportBodyKind>,
475
476        /// By default, `cargo hax json` outputs a JSON where every
477        /// piece of information is inlined. This however creates very
478        /// large JSON files. This flag enables the use of unique IDs
479        /// and outputs a map from IDs to actual objects.
480        #[arg(long)]
481        use_ids: bool,
482
483        /// Whether to include extra informations about `DefId`s.
484        #[arg(short = 'E', long = "include-extra", default_value = "false")]
485        include_extra: bool,
486    },
487
488    /// Serialize to a `haxmeta` file, the internal binary format used by hax to
489    /// store the ASTs produced by the hax exporter.
490    #[clap(hide = true)]
491    Serialize {
492        /// Whether the bodies are exported as THIR, built MIR, const
493        /// MIR, or a combination. Repeat this option to extract a
494        /// combination (e.g. `-k thir -k mir-built`). Pass `--kind`
495        /// alone with no value to disable body extraction.
496        #[arg(
497            value_enum,
498            short,
499            long = "kind",
500            num_args = 0..=3,
501            default_values_t = [ExportBodyKind::Thir]
502        )]
503        kind: Vec<ExportBodyKind>,
504
505        /// When extracting to a given backend, the exporter is called with different `cfg` options.
506        /// This option allows to set the same flags as `cargo hax into` would pick.
507        #[arg(short)]
508        backend: Option<BackendName>,
509    },
510
511    #[command(flatten)]
512    CliExtension(E::Command),
513}
514
515impl<E: Extension> Command<E> {
516    pub fn body_kinds(&self) -> Vec<ExportBodyKind> {
517        match self {
518            Command::JSON { kind, .. } => kind.clone(),
519            Command::Serialize { kind, .. } => kind.clone(),
520            Command::Backend { .. } | Command::CliExtension { .. } => vec![ExportBodyKind::Thir],
521        }
522    }
523    pub fn backend_name(&self) -> Option<BackendName> {
524        match self {
525            Command::Backend(backend_options) => Some((&backend_options.backend).into()),
526            Command::JSON { .. } => None,
527            Command::Serialize { backend, .. } => backend.clone(),
528            Command::CliExtension(_) => None,
529        }
530    }
531}
532
533#[derive_group(Serializers)]
534#[derive(JsonSchema, ValueEnum, Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
535pub enum ExportBodyKind {
536    Thir,
537    MirBuilt,
538}
539
540#[derive_group(Serializers)]
541#[derive(JsonSchema, Parser, Debug, Clone)]
542#[command(
543    author,
544    version = crate::HAX_VERSION,
545    long_version = concat!("\nversion=", env!("HAX_VERSION"), "\n", "commit=", env!("HAX_GIT_COMMIT_HASH")),
546    name = "hax",
547    about,
548    long_about = None
549)]
550pub struct ExtensibleOptions<E: Extension> {
551    /// Semi-colon terminated list of arguments to pass to the
552    /// `cargo build` invocation. For example, to apply this
553    /// program on a package `foo`, use `-C -p foo ;`. (make sure
554    /// to escape `;` correctly in your shell)
555    #[arg(default_values = Vec::<&str>::new(), short='C', allow_hyphen_values=true, num_args=1.., long="cargo-args", value_terminator=";")]
556    pub cargo_flags: Vec<String>,
557
558    #[command(subcommand)]
559    pub command: Command<E>,
560
561    /// `cargo` caching is enable by default, this flag disables it.
562    #[arg(long="disable-cargo-cache", action=clap::builder::ArgAction::SetFalse)]
563    pub force_cargo_build: ForceCargoBuild,
564
565    /// Apply the command to every local package of the dependency closure. By
566    /// default, the command is only applied to the primary packages (i.e. the
567    /// package(s) of the current directory, or the ones selected with cargo
568    /// options like `-C -p <PKG> ;`).
569    #[arg(long = "deps")]
570    pub deps: bool,
571
572    /// Provide a precomputed haxmeta file explicitly.
573    /// Setting this option bypasses rustc and the exporter altogether.
574    #[arg(long)]
575    #[clap(hide = true)]
576    pub haxmeta: Option<PathBuf>,
577
578    /// By default, hax uses `$CARGO_TARGET_DIR/hax` as target folder,
579    /// to avoid recompilation when working both with `cargo hax` and
580    /// `cargo build` (or, e.g. `rust-analyzer`). This option disables
581    /// this behavior.
582    #[arg(long)]
583    pub no_custom_target_directory: bool,
584
585    /// Diagnostic format. Sets `cargo`'s `--message-format` as well,
586    /// if not present.
587    #[arg(long, default_value = "human")]
588    pub message_format: MessageFormat,
589
590    /// Enables experimental FullDef format for items exported from the frontend
591    /// in the haxmeta file.
592    #[arg(long, env = "HAX_EXPERIMENTAL_FULL_DEF")]
593    pub experimental_full_def: bool,
594
595    #[group(flatten)]
596    pub extension: E::Options,
597}
598
599pub type Options = ExtensibleOptions<()>;
600
601#[derive_group(Serializers)]
602#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy, Eq, PartialEq)]
603pub enum MessageFormat {
604    Human,
605    Json,
606}
607
608impl<E: Extension> NormalizePaths for Command<E> {
609    fn normalize_paths(&mut self) {
610        use Command::*;
611        match self {
612            JSON { output_file, .. } => output_file.normalize_paths(),
613            _ => (),
614        }
615    }
616}
617
618impl NormalizePaths for Options {
619    fn normalize_paths(&mut self) {
620        self.command.normalize_paths()
621    }
622}
623
624impl From<Options> for hax_frontend_exporter_options::Options {
625    fn from(_opts: Options) -> hax_frontend_exporter_options::Options {
626        hax_frontend_exporter_options::Options {
627            inline_anon_consts: true,
628            bounds_options: hax_frontend_exporter_options::BoundsOptions {
629                resolve_destruct: false,
630                prune_sized: true,
631            },
632            item_ref_use_concrete_impl: false,
633        }
634    }
635}
636
637/// The subset of `Options` the frontend is sensible to.
638#[derive_group(Serializers)]
639#[derive(JsonSchema, Debug, Clone)]
640pub struct ExporterOptions {
641    pub deps: bool,
642    pub force_cargo_build: ForceCargoBuild,
643    /// When exporting, the driver sets `--cfg hax_backend_{backkend}`, thus we need this information.
644    pub backend: Option<BackendName>,
645    pub body_kinds: Vec<ExportBodyKind>,
646    pub experimental_full_def: bool,
647}
648
649#[derive_group(Serializers)]
650#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy, PartialEq, Eq, Hash)]
651pub enum BackendName {
652    Fstar,
653    Coq,
654    Ssprove,
655    Easycrypt,
656    #[clap(alias("proverif"))]
657    ProVerif,
658    LegacyLean,
659    Lean,
660    Rust,
661    GenerateRustEngineNames,
662    Debugger,
663}
664
665impl BackendName {
666    pub fn iter() -> impl Iterator<Item = Self> {
667        [
668            Self::Fstar,
669            Self::Coq,
670            Self::Ssprove,
671            Self::Easycrypt,
672            Self::ProVerif,
673            Self::LegacyLean,
674            Self::Lean,
675            Self::Rust,
676            Self::GenerateRustEngineNames,
677        ]
678        .into_iter()
679    }
680}
681
682impl fmt::Display for BackendName {
683    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
684        let name = match self {
685            BackendName::Fstar => "fstar",
686            BackendName::Coq => "coq",
687            BackendName::Ssprove => "ssprove",
688            BackendName::Easycrypt => "easycrypt",
689            BackendName::ProVerif => "proverif",
690            BackendName::LegacyLean => "legacy-lean",
691            BackendName::Lean => "lean",
692            BackendName::Rust => "rust",
693            BackendName::GenerateRustEngineNames => "generate_rust_engine_names",
694            BackendName::Debugger => "debugger",
695        };
696        write!(f, "{name}")
697    }
698}
699
700impl From<&Options> for ExporterOptions {
701    fn from(options: &Options) -> Self {
702        ExporterOptions {
703            deps: options.deps,
704            force_cargo_build: options.force_cargo_build.clone(),
705            backend: options.command.backend_name(),
706            body_kinds: options.command.body_kinds(),
707            experimental_full_def: options.experimental_full_def,
708        }
709    }
710}
711
712impl From<&Backend> for BackendName {
713    fn from(backend: &Backend) -> Self {
714        match backend {
715            Backend::Fstar { .. } => BackendName::Fstar,
716            Backend::Coq { .. } => BackendName::Coq,
717            Backend::Ssprove { .. } => BackendName::Ssprove,
718            Backend::Easycrypt { .. } => BackendName::Easycrypt,
719            Backend::ProVerif { .. } => BackendName::ProVerif,
720            Backend::LegacyLean { .. } => BackendName::LegacyLean,
721            Backend::Lean { .. } => BackendName::Lean,
722            Backend::Rust { .. } => BackendName::Rust,
723            Backend::GenerateRustEngineNames { .. } => BackendName::GenerateRustEngineNames,
724            Backend::Debugger { .. } => BackendName::Debugger,
725        }
726    }
727}
728
729pub const ENV_VAR_OPTIONS_FRONTEND: &str = "DRIVER_HAX_FRONTEND_OPTS";
730pub const ENV_VAR_OPTIONS_FULL: &str = "DRIVER_HAX_FRONTEND_FULL_OPTS";
hax_types/cli_options/mod.rs

hax_types/cli_options/
mod.rs
