diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index 4058cd4d1..d77a0b50f 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -596,7 +596,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); 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/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 7c2df7549..f84795be7 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, @@ -215,12 +215,31 @@ enum InclusionKind { #[derive_group(Serializers)] #[derive(JsonSchema, Debug, Clone)] -struct InclusionClause { - kind: InclusionKind, - namespace: Namespace, +pub struct InclusionClause { + pub kind: InclusionKind, + pub namespace: Namespace, } -fn parse_inclusion_clause( +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) => 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()) + } +} + +pub fn parse_inclusion_clause( s: &str, ) -> Result> { let s = s.trim(); @@ -235,11 +254,11 @@ 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}`" ))?, @@ -290,7 +309,7 @@ pub struct TranslationOptions { value_delimiter = ' ', )] #[arg(short, allow_hyphen_values(true))] - include_namespaces: Vec, + pub include_namespaces: Vec, } #[derive_group(Serializers)]