From b4c95cbebdf3d108269b5d7c15fdbf4d8dfdc3cf Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 17 Oct 2024 18:41:09 +0200 Subject: [PATCH 1/4] feat(cli): add hidden subcommand `__json` This makes hax consume it's CLI flags as a JSON payload in an env var. --- cli/subcommands/src/cargo_hax.rs | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index a1952dc70..f704e0bfe 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -569,7 +569,23 @@ fn run_command(options: &Options, haxmeta_files: Vec) -> boo fn main() { let args: Vec = get_args("hax"); - let mut options = Options::parse_from(args.iter()); + let mut options = match &args[..] { + [_, kw] if kw == "__json" => serde_json::from_str( + &std::env::var(ENV_VAR_OPTIONS_FRONTEND).unwrap_or_else(|_| { + panic!( + "Cannot find environnement variable {}", + ENV_VAR_OPTIONS_FRONTEND + ) + }), + ) + .unwrap_or_else(|_| { + panic!( + "Invalid value for the environnement variable {}", + ENV_VAR_OPTIONS_FRONTEND + ) + }), + _ => Options::parse_from(args.iter()), + }; options.normalize_paths(); let (haxmeta_files, exit_code) = compute_haxmeta_files(&options); From 8a4e47c34c2e2dbd2014a7792ae3fff58c69ff67 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 17 Oct 2024 18:42:07 +0200 Subject: [PATCH 2/4] feat(hax-types): implement ToString for various types --- frontend/exporter/options/src/lib.rs | 30 ++++++++++++++++++++++++++++ hax-types/src/cli_options/mod.rs | 19 +++++++++++++++--- 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/frontend/exporter/options/src/lib.rs b/frontend/exporter/options/src/lib.rs index 28d0264bb..4cf830ae6 100644 --- a/frontend/exporter/options/src/lib.rs +++ b/frontend/exporter/options/src/lib.rs @@ -8,6 +8,16 @@ pub enum Glob { Many, // ** } +impl ToString for Glob { + fn to_string(&self) -> String { + match self { + Self::One => "*", + Self::Many => "**", + } + .to_string() + } +} + #[derive_group(Serializers)] #[derive(Debug, Clone, JsonSchema)] pub enum NamespaceChunk { @@ -15,6 +25,15 @@ pub enum NamespaceChunk { Exact(String), } +impl ToString for NamespaceChunk { + fn to_string(&self) -> String { + match self { + Self::Glob(glob) => glob.to_string(), + Self::Exact(string) => string.to_string(), + } + } +} + impl std::convert::From<&str> for NamespaceChunk { fn from(s: &str) -> Self { match s { @@ -31,6 +50,17 @@ pub struct Namespace { pub chunks: Vec, } +impl ToString for Namespace { + fn to_string(&self) -> String { + self.chunks + .iter() + .map(NamespaceChunk::to_string) + .collect::>() + .join("::") + .to_string() + } +} + impl std::convert::From for Namespace { fn from(s: String) -> Self { Namespace { diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index 6ef102e13..c3dc9d16c 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -215,9 +215,22 @@ enum InclusionKind { #[derive_group(Serializers)] #[derive(JsonSchema, Debug, Clone)] -struct InclusionClause { - kind: InclusionKind, - namespace: Namespace, +pub struct InclusionClause { + pub kind: InclusionKind, + pub namespace: Namespace, +} + +impl ToString for InclusionClause { + fn to_string(&self) -> String { + let kind = match self.kind { + InclusionKind::Included(DepsKind::Transitive) => "+", + InclusionKind::Included(DepsKind::Shallow) => "+~", + InclusionKind::Included(DepsKind::None) => "+!", + InclusionKind::SignatureOnly => "+:", + InclusionKind::Excluded => "-", + }; + format!("{kind}{}", self.namespace.to_string()) + } } fn parse_inclusion_clause( From 174775e7b04a1766d490f78f27c4333a6868a4b4 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 17 Oct 2024 18:42:31 +0200 Subject: [PATCH 3/4] fix(hax-types): make more items public --- hax-types/src/cli_options/extension.rs | 2 +- hax-types/src/cli_options/mod.rs | 20 ++++++++++---------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/hax-types/src/cli_options/extension.rs b/hax-types/src/cli_options/extension.rs index fa1084dc5..9a4970f4e 100644 --- a/hax-types/src/cli_options/extension.rs +++ b/hax-types/src/cli_options/extension.rs @@ -32,7 +32,7 @@ pub struct EmptyArgsExtension {} #[derive(JsonSchema, Subcommand, Debug, Clone)] pub enum EmptySubcommandExtension {} -pub trait Extension { +pub trait Extension: 'static { type Options: ArgsExtensionPoint; type Command: SubcommandExtensionPoint; type BackendOptions: ArgsExtensionPoint; diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index c3dc9d16c..5c2ab907f 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -127,7 +127,7 @@ pub struct ProVerifOptions { value_delimiter = ' ', allow_hyphen_values(true) )] - assume_items: Vec, + pub assume_items: Vec, } #[derive_group(Serializers)] @@ -135,13 +135,13 @@ pub struct ProVerifOptions { pub struct FStarOptions { /// Set the Z3 per-query resource limit #[arg(long, default_value = "15")] - z3rlimit: u32, + pub z3rlimit: u32, /// Number of unrolling of recursive functions to try #[arg(long, default_value = "0")] - fuel: u32, + pub fuel: u32, /// Number of unrolling of inductive datatypes to try #[arg(long, default_value = "1")] - ifuel: u32, + pub ifuel: u32, /// Modules for which Hax should extract interfaces (`*.fsti` /// files) in supplement to implementations (`*.fst` files). By /// default we extract no interface, only implementations. If a @@ -160,10 +160,10 @@ pub struct FStarOptions { value_delimiter = ' ', allow_hyphen_values(true) )] - interfaces: Vec, + pub interfaces: Vec, #[arg(long, default_value = "100", env = "HAX_FSTAR_LINE_WIDTH")] - line_width: u16, + pub line_width: u16, #[group(flatten)] pub cli_extension: E::FStarOptions, @@ -198,7 +198,7 @@ impl fmt::Display for Backend<()> { #[derive_group(Serializers)] #[derive(JsonSchema, Debug, Clone)] -enum DepsKind { +pub enum DepsKind { Transitive, Shallow, None, @@ -206,7 +206,7 @@ enum DepsKind { #[derive_group(Serializers)] #[derive(JsonSchema, Debug, Clone)] -enum InclusionKind { +pub enum InclusionKind { /// `+query` include the items selected by `query` Included(DepsKind), SignatureOnly, @@ -233,7 +233,7 @@ impl ToString for InclusionClause { } } -fn parse_inclusion_clause( +pub fn parse_inclusion_clause( s: &str, ) -> Result> { let s = s.trim(); @@ -303,7 +303,7 @@ pub struct TranslationOptions { value_delimiter = ' ', )] #[arg(short, allow_hyphen_values(true))] - include_namespaces: Vec, + pub include_namespaces: Vec, } #[derive_group(Serializers)] From f5f39f0e6db0c9738dfa2be50c22835d87c784d7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 13 Nov 2024 10:56:34 +0100 Subject: [PATCH 4/4] refactor(frontend/cli_options): factor the prefixes with constants --- hax-types/src/cli_options/mod.rs | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index 5c2ab907f..a351d0f26 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -220,14 +220,20 @@ pub struct InclusionClause { pub namespace: Namespace, } +const PREFIX_INCLUDED_TRANSITIVE: &str = "+"; +const PREFIX_INCLUDED_SHALLOW: &str = "+~"; +const PREFIX_INCLUDED_NONE: &str = "+!"; +const PREFIX_SIGNATURE_ONLY: &str = "+:"; +const PREFIX_EXCLUDED: &str = "-"; + impl ToString for InclusionClause { fn to_string(&self) -> String { let kind = match self.kind { - InclusionKind::Included(DepsKind::Transitive) => "+", - InclusionKind::Included(DepsKind::Shallow) => "+~", - InclusionKind::Included(DepsKind::None) => "+!", - InclusionKind::SignatureOnly => "+:", - InclusionKind::Excluded => "-", + InclusionKind::Included(DepsKind::Transitive) => PREFIX_INCLUDED_TRANSITIVE, + InclusionKind::Included(DepsKind::Shallow) => PREFIX_INCLUDED_SHALLOW, + InclusionKind::Included(DepsKind::None) => PREFIX_INCLUDED_NONE, + InclusionKind::SignatureOnly => PREFIX_SIGNATURE_ONLY, + InclusionKind::Excluded => PREFIX_EXCLUDED, }; format!("{kind}{}", self.namespace.to_string()) } @@ -248,11 +254,11 @@ pub fn parse_inclusion_clause( ) }; let kind = match &prefix[..] { - "+" => InclusionKind::Included(DepsKind::Transitive), - "+~" => InclusionKind::Included(DepsKind::Shallow), - "+!" => InclusionKind::Included(DepsKind::None), - "+:" => InclusionKind::SignatureOnly, - "-" => InclusionKind::Excluded, + PREFIX_INCLUDED_TRANSITIVE => InclusionKind::Included(DepsKind::Transitive), + PREFIX_INCLUDED_SHALLOW => InclusionKind::Included(DepsKind::Shallow), + PREFIX_INCLUDED_NONE => InclusionKind::Included(DepsKind::None), + PREFIX_SIGNATURE_ONLY => InclusionKind::SignatureOnly, + PREFIX_EXCLUDED => InclusionKind::Excluded, prefix => Err(format!( "Expected `+`, `+~`, `+!`, `+:` or `-`, got an `{prefix}`" ))?,