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)]
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)]
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, Clone)]
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, Clone)]
135pub struct FStarOptions<E: Extension> {
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    #[group(flatten)]
169    pub cli_extension: E::FStarOptions,
170}
171
172#[derive_group(Serializers)]
173#[derive(JsonSchema, Subcommand, Debug, Clone)]
174pub enum Backend<E: Extension> {
175    /// Use the F* backend
176    Fstar(FStarOptions<E>),
177    /// Use the Coq backend
178    Coq,
179    /// Use the SSProve backend
180    Ssprove,
181    /// Use the EasyCrypt backend (warning: work in progress!)
182    Easycrypt,
183    /// Use the ProVerif backend (warning: work in progress!)
184    ProVerif(ProVerifOptions),
185    /// Use the Lean backend (warning: work in progress!)
186    #[clap(hide = true)]
187    Lean,
188    /// Use the Rust backend (warning: work in progress!)
189    #[clap(hide = true)]
190    Rust,
191    /// Extract `DefId`s of the crate as a Rust module tree.
192    /// This is a command that regenerates code for the rust engine.
193    #[clap(hide = true)]
194    GenerateRustEngineNames,
195}
196
197impl fmt::Display for Backend<()> {
198    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
199        match self {
200            Backend::Fstar { .. } => write!(f, "fstar"),
201            Backend::Coq { .. } => write!(f, "coq"),
202            Backend::Ssprove { .. } => write!(f, "ssprove"),
203            Backend::Easycrypt { .. } => write!(f, "easycrypt"),
204            Backend::ProVerif { .. } => write!(f, "proverif"),
205            Backend::Lean { .. } => write!(f, "lean"),
206            Backend::Rust { .. } => write!(f, "rust"),
207            Backend::GenerateRustEngineNames { .. } => write!(f, "generate_rust_engine_names"),
208        }
209    }
210}
211
212#[derive_group(Serializers)]
213#[derive(JsonSchema, Debug, Clone)]
214pub enum DepsKind {
215    Transitive,
216    Shallow,
217    None,
218}
219
220#[derive_group(Serializers)]
221#[derive(JsonSchema, Debug, Clone)]
222pub enum InclusionKind {
223    /// `+query` include the items selected by `query`
224    Included(DepsKind),
225    SignatureOnly,
226    Excluded,
227}
228
229#[derive_group(Serializers)]
230#[derive(JsonSchema, Debug, Clone)]
231pub struct InclusionClause {
232    pub kind: InclusionKind,
233    pub namespace: Namespace,
234}
235
236const PREFIX_INCLUDED_TRANSITIVE: &str = "+";
237const PREFIX_INCLUDED_SHALLOW: &str = "+~";
238const PREFIX_INCLUDED_NONE: &str = "+!";
239const PREFIX_SIGNATURE_ONLY: &str = "+:";
240const PREFIX_EXCLUDED: &str = "-";
241
242impl ToString for InclusionClause {
243    fn to_string(&self) -> String {
244        let kind = match self.kind {
245            InclusionKind::Included(DepsKind::Transitive) => PREFIX_INCLUDED_TRANSITIVE,
246            InclusionKind::Included(DepsKind::Shallow) => PREFIX_INCLUDED_SHALLOW,
247            InclusionKind::Included(DepsKind::None) => PREFIX_INCLUDED_NONE,
248            InclusionKind::SignatureOnly => PREFIX_SIGNATURE_ONLY,
249            InclusionKind::Excluded => PREFIX_EXCLUDED,
250        };
251        format!("{kind}{}", self.namespace.to_string())
252    }
253}
254
255pub fn parse_inclusion_clause(
256    s: &str,
257) -> Result<InclusionClause, Box<dyn std::error::Error + Send + Sync + 'static>> {
258    let s = s.trim();
259    if s.is_empty() {
260        Err("Expected `-` or `+`, got an empty string")?
261    }
262    let (prefix, namespace) = {
263        let f = |&c: &char| matches!(c, '+' | '-' | '~' | '!' | ':');
264        (
265            s.chars().take_while(f).into_iter().collect::<String>(),
266            s.chars().skip_while(f).into_iter().collect::<String>(),
267        )
268    };
269    let kind = match &prefix[..] {
270        PREFIX_INCLUDED_TRANSITIVE => InclusionKind::Included(DepsKind::Transitive),
271        PREFIX_INCLUDED_SHALLOW => InclusionKind::Included(DepsKind::Shallow),
272        PREFIX_INCLUDED_NONE => InclusionKind::Included(DepsKind::None),
273        PREFIX_SIGNATURE_ONLY => InclusionKind::SignatureOnly,
274        PREFIX_EXCLUDED => InclusionKind::Excluded,
275        prefix => Err(format!(
276            "Expected `+`, `+~`, `+!`, `+:` or `-`, got an `{prefix}`"
277        ))?,
278    };
279    Ok(InclusionClause {
280        kind,
281        namespace: namespace.to_string().into(),
282    })
283}
284
285#[derive_group(Serializers)]
286#[derive(JsonSchema, Parser, Debug, Clone)]
287pub struct TranslationOptions {
288    /// Controls which Rust item should be extracted or not.
289    ///
290    /// This is a space-separated list of patterns prefixed with a
291    /// modifier, read from the left to the right.
292    ///
293    /// A pattern is a Rust path (say `mycrate::mymod::myfn`) where
294    /// globs are allowed: `*` matches any name
295    /// (e.g. `mycrate::mymod::myfn` is matched by
296    /// `mycrate::*::myfn`), while `**` matches any subpath, empty
297    /// included (e.g. `mycrate::mymod::myfn` is matched by
298    /// `**::myfn`).
299
300    /// By default, hax includes all items. Then, the patterns
301    /// prefixed by modifiers are processed from left to right,
302    /// excluding or including items. Each pattern selects a number of
303    /// item. The modifiers are:
304
305    /// {n}{n} - `+`: includes the selected items with their
306    /// dependencies, transitively (e.g. if function `f` calls `g`
307    /// which in turn calls `h`, then `+k::f` includes `f`, `g` and
308    /// `h`)
309
310    /// {n} - `+~`: includes the selected items with their direct
311    /// dependencies only (following the previous example, `+~k::f`
312    /// would select `f` and `g`, but not `h`)
313
314    /// {n} - `+!`: includes the selected items, without their
315    /// dependencies (`+!k::f` would only select `f`)
316
317    /// {n} - `+:`: only includes the type of the selected items (no
318    /// dependencies). This includes full struct and enums, but only
319    /// the type signature of functions and trait impls (except when
320    /// they contain associated types), dropping their bodies.
321    #[arg(
322        value_parser = parse_inclusion_clause,
323        value_delimiter = ' ',
324    )]
325    #[arg(short, allow_hyphen_values(true))]
326    pub include_namespaces: Vec<InclusionClause>,
327}
328
329#[derive_group(Serializers)]
330#[derive(JsonSchema, Parser, Debug, Clone)]
331pub struct BackendOptions<E: Extension> {
332    #[command(subcommand)]
333    pub backend: Backend<E>,
334
335    /// Don't write anything on disk. Output everything as JSON to stdout
336    /// instead.
337    #[arg(long = "dry-run")]
338    pub dry_run: bool,
339
340    /// Verbose mode for the Hax engine. Set `-vv` for maximal verbosity.
341    #[arg(short, long, action = clap::ArgAction::Count)]
342    pub verbose: u8,
343
344    /// Prints statistics about how many items have been translated
345    /// successfully by the engine.
346    #[arg(long)]
347    pub stats: bool,
348
349    /// Enables profiling for the engine: for each phase of the
350    /// engine, time and memory usage are recorded and reported.
351    #[arg(long)]
352    pub profile: bool,
353
354    /// Enable engine debugging: dumps the AST at each phase.
355    ///
356    /// The value of `<DEBUG_ENGINE>` can be either:
357
358    /// {n}{n} - `interactive` (or `i`): enables debugging of the engine,
359    /// and visualize interactively in a webapp how a crate was
360    /// transformed by each phase, both in Rust-like syntax and
361    /// browsing directly the internal AST. By default, the webapp is
362    /// hosted on `http://localhost:8000`, the port can be override by
363    /// setting the `HAX_DEBUGGER_PORT` environment variable.
364
365    /// {n} - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
366    /// to `<FILE>`. `<FILE>` can be either [-] or a path.
367    #[arg(short, long = "debug-engine")]
368    pub debug_engine: Option<DebugEngineMode>,
369
370    /// Extract type aliases. This is disabled by default, since
371    /// extracted terms depends on expanded types rather than on type
372    /// aliases. Turning this option on is discouraged: Rust type
373    /// synonyms can ommit generic bounds, which are ususally
374    /// necessary in the hax backends, leading to typechecking
375    /// errors. For more details see
376    /// https://github.com/hacspec/hax/issues/708.
377    #[arg(long)]
378    pub extract_type_aliases: bool,
379
380    #[command(flatten)]
381    pub translation_options: TranslationOptions,
382
383    /// Where to put the output files resulting from the translation.
384    /// Defaults to "<crate folder>/proofs/<backend>/extraction".
385    #[arg(long)]
386    pub output_dir: Option<PathBuf>,
387
388    #[group(flatten)]
389    pub cli_extension: E::BackendOptions,
390}
391
392#[derive_group(Serializers)]
393#[derive(JsonSchema, Subcommand, Debug, Clone)]
394pub enum Command<E: Extension> {
395    /// Translate to a backend. The translated modules will be written
396    /// under the directory `<PKG>/proofs/<BACKEND>/extraction`, where
397    /// `<PKG>` is the translated cargo package name and `<BACKEND>`
398    /// the name of the backend.
399    #[clap(name = "into")]
400    Backend(BackendOptions<E>),
401
402    /// Export directly as a JSON file
403    JSON {
404        /// Path to the output JSON file, "-" denotes stdout.
405        #[arg(
406            short,
407            long = "output-file",
408            default_value = "hax_frontend_export.json"
409        )]
410        output_file: PathOrDash,
411        /// Whether the bodies are exported as THIR, built MIR, const
412        /// MIR, or a combination. Repeat this option to extract a
413        /// combination (e.g. `-k thir -k mir-built`). Pass `--kind`
414        /// alone with no value to disable body extraction.
415        #[arg(
416            value_enum,
417            short,
418            long = "kind",
419            num_args = 0..=3,
420            default_values_t = [ExportBodyKind::Thir]
421        )]
422        kind: Vec<ExportBodyKind>,
423
424        /// By default, `cargo hax json` outputs a JSON where every
425        /// piece of information is inlined. This however creates very
426        /// large JSON files. This flag enables the use of unique IDs
427        /// and outputs a map from IDs to actual objects.
428        #[arg(long)]
429        use_ids: bool,
430
431        /// Whether to include extra informations about `DefId`s.
432        #[arg(short = 'E', long = "include-extra", default_value = "false")]
433        include_extra: bool,
434    },
435
436    #[command(flatten)]
437    CliExtension(E::Command),
438}
439
440impl<E: Extension> Command<E> {
441    pub fn body_kinds(&self) -> Vec<ExportBodyKind> {
442        match self {
443            Command::JSON { kind, .. } => kind.clone(),
444            _ => vec![ExportBodyKind::Thir],
445        }
446    }
447}
448
449#[derive_group(Serializers)]
450#[derive(JsonSchema, ValueEnum, Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
451pub enum ExportBodyKind {
452    Thir,
453    MirBuilt,
454}
455
456#[derive_group(Serializers)]
457#[derive(JsonSchema, Parser, Debug, Clone)]
458#[command(
459    author,
460    version = crate::HAX_VERSION,
461    long_version = concat!("\nversion=", env!("HAX_VERSION"), "\n", "commit=", env!("HAX_GIT_COMMIT_HASH")),
462    name = "hax",
463    about,
464    long_about = None
465)]
466pub struct ExtensibleOptions<E: Extension> {
467    /// Replace the expansion of each macro matching PATTERN by their
468    /// invocation. PATTERN denotes a rust path (i.e. `A::B::c`) in
469    /// which glob patterns are allowed. The glob pattern * matches
470    /// any name, the glob pattern ** matches zero, one or more
471    /// names. For instance, `A::B::C::D::X` and `A::E::F::D::Y`
472    /// matches `A::**::D::*`.
473    #[arg(
474        short = 'i',
475        long = "inline-macro-call",
476        value_name = "PATTERN",
477        value_parser,
478        value_delimiter = ',',
479        default_values = [
480            "hacspec_lib::array::array", "hacspec_lib::array::public_bytes", "hacspec_lib::array::bytes",
481            "hacspec_lib::math_integers::public_nat_mod", "hacspec_lib::math_integers::unsigned_public_integer",
482        ],
483    )]
484    pub inline_macro_calls: Vec<Namespace>,
485
486    /// Semi-colon terminated list of arguments to pass to the
487    /// `cargo build` invocation. For example, to apply this
488    /// program on a package `foo`, use `-C -p foo ;`. (make sure
489    /// to escape `;` correctly in your shell)
490    #[arg(default_values = Vec::<&str>::new(), short='C', allow_hyphen_values=true, num_args=1.., long="cargo-args", value_terminator=";")]
491    pub cargo_flags: Vec<String>,
492
493    #[command(subcommand)]
494    pub command: Command<E>,
495
496    /// `cargo` caching is enable by default, this flag disables it.
497    #[arg(long="disable-cargo-cache", action=clap::builder::ArgAction::SetFalse)]
498    pub force_cargo_build: ForceCargoBuild,
499
500    /// Apply the command to every local package of the dependency closure. By
501    /// default, the command is only applied to the primary packages (i.e. the
502    /// package(s) of the current directory, or the ones selected with cargo
503    /// options like `-C -p <PKG> ;`).
504    #[arg(long = "deps")]
505    pub deps: bool,
506
507    /// By default, hax uses `$CARGO_TARGET_DIR/hax` as target folder,
508    /// to avoid recompilation when working both with `cargo hax` and
509    /// `cargo build` (or, e.g. `rust-analyzer`). This option disables
510    /// this behavior.
511    #[arg(long)]
512    pub no_custom_target_directory: bool,
513
514    /// Diagnostic format. Sets `cargo`'s `--message-format` as well,
515    /// if not present.
516    #[arg(long, default_value = "human")]
517    pub message_format: MessageFormat,
518
519    #[group(flatten)]
520    pub extension: E::Options,
521}
522
523pub type Options = ExtensibleOptions<()>;
524
525#[derive_group(Serializers)]
526#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy, Eq, PartialEq)]
527pub enum MessageFormat {
528    Human,
529    Json,
530}
531
532impl<E: Extension> NormalizePaths for Command<E> {
533    fn normalize_paths(&mut self) {
534        use Command::*;
535        match self {
536            JSON { output_file, .. } => output_file.normalize_paths(),
537            _ => (),
538        }
539    }
540}
541
542impl NormalizePaths for Options {
543    fn normalize_paths(&mut self) {
544        self.command.normalize_paths()
545    }
546}
547
548impl From<Options> for hax_frontend_exporter_options::Options {
549    fn from(_opts: Options) -> hax_frontend_exporter_options::Options {
550        hax_frontend_exporter_options::Options {
551            inline_anon_consts: true,
552            bounds_options: hax_frontend_exporter_options::BoundsOptions {
553                resolve_drop: false,
554                prune_sized: true,
555            },
556        }
557    }
558}
559
560pub const ENV_VAR_OPTIONS_FRONTEND: &str = "DRIVER_HAX_FRONTEND_OPTS";
hax_types/cli_options/mod.rs

hax_types/cli_options/
mod.rs
