Merge pull request #981 from hacspec/make-options-extensible

Make options extensible

cli/subcommands/src/cargo_hax.rs

@@ -201,7 +201,7 @@ fn run_engine(
     haxmeta: HaxMeta<hax_frontend_exporter::ThirBody>,
     working_dir: PathBuf,
     manifest_dir: PathBuf,
-    backend: &BackendOptions,
+    backend: &BackendOptions<()>,
     message_format: MessageFormat,
 ) -> bool {
     let engine_options = EngineOptions {

engine/backends/fstar/fstar_backend.ml

@@ -68,7 +68,7 @@ end
 module AST = Ast.Make (InputLanguage)
 
 module BackendOptions = struct
-  type t = Hax_engine.Types.f_star_options
+  type t = Hax_engine.Types.f_star_options_for__null
 end
 
 open Ast

engine/backends/fstar/fstar_backend.mli

@@ -1,2 +1,2 @@
 open Hax_engine.Backend
-include T with type BackendOptions.t = Hax_engine.Types.f_star_options
+include T with type BackendOptions.t = Hax_engine.Types.f_star_options_for__null

engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

@@ -434,6 +434,16 @@ let exporters = {
             return {type, parse, to_json};
         },
     },
+    empty_struct: {
+        guard: def => (eq(keys(def), new Set(["type"])) && def.type == 'object'),
+        f: (name, _) => {
+            return {
+                type: `EmptyStruct${name}`,
+                parse: `EmptyStruct${name}`,
+                to_json: '`Null',
+            };
+        },
+    },
     // object is a *flat* record
     object: {
         guard: def => (eq(keys(def), new Set(["type", "required", "properties"]))
@@ -463,6 +473,14 @@ let exporters = {
         f: (name, o) => {
             assert(o.enum.every(x => typeof x == "string"), 'not every enum is a string');
 
+            if(o.enum.length == 0) {
+                return {
+                    type: '|',
+                    parse: 'failwith "cannot parse an empty type"',
+                    to_json: 'match o with _ -> .',
+                };
+            }
+
             let variants = o.enum.map(n => ({
                 Δ: n,
                 variant: ensureUnique('variant', variantNameOf(n)),

hax-types/src/cli_options/extension.rs

@@ -0,0 +1,50 @@
+/// This module defines a way to extend externally the CLI of hax, via
+/// the `Extension` trait. This trait defines one associated type per
+/// extension point.
+use crate::prelude::*;
+
+use clap::{Parser, Subcommand};
+
+macro_rules! trait_alias {
+    ($name:ident = $($base:tt)+) => {
+        pub trait $name: $($base)+ { }
+        impl<T: $($base)+> $name for T { }
+    };
+}
+
+trait_alias!(
+    ExtensionPoint =
+    bincode::Decode
+        + bincode::Encode
+        + std::fmt::Debug
+        + for<'a> serde::Deserialize<'a>
+        + serde::Serialize
+        + JsonSchema
+        + Clone
+        + for<'a> bincode::BorrowDecode<'a>
+);
+
+trait_alias!(SubcommandExtensionPoint = ExtensionPoint + clap::Subcommand);
+trait_alias!(ArgsExtensionPoint = ExtensionPoint + clap::Args);
+
+#[derive_group(Serializers)]
+#[derive(JsonSchema, Parser, Debug, Clone)]
+pub struct EmptyArgsExtension {}
+
+#[derive_group(Serializers)]
+#[derive(JsonSchema, Subcommand, Debug, Clone)]
+pub enum EmptySubcommandExtension {}
+
+pub trait Extension {
+    type Options: ArgsExtensionPoint;
+    type Command: SubcommandExtensionPoint;
+    type BackendOptions: ArgsExtensionPoint;
+    type FStarOptions: ArgsExtensionPoint;
+}
+
+impl Extension for () {
+    type Options = EmptyArgsExtension;
+    type Command = EmptySubcommandExtension;
+    type BackendOptions = EmptyArgsExtension;
+    type FStarOptions = EmptyArgsExtension;
+}

hax-types/src/cli_options.rs → hax-types/src/cli_options/mod.rs

@@ -4,6 +4,8 @@ use clap::{Parser, Subcommand, ValueEnum};
 use std::fmt;
 
 pub use hax_frontend_exporter_options::*;
+pub mod extension;
+use extension::Extension;
 
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Debug, Clone)]
@@ -130,7 +132,7 @@ pub struct ProVerifOptions {
 
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Parser, Debug, Clone)]
-pub struct FStarOptions {
+pub struct FStarOptions<E: Extension> {
     /// Set the Z3 per-query resource limit
     #[arg(long, default_value = "15")]
     z3rlimit: u32,
@@ -162,13 +164,16 @@ pub struct FStarOptions {
 
     #[arg(long, default_value = "100", env = "HAX_FSTAR_LINE_WIDTH")]
     line_width: u16,
+
+    #[group(flatten)]
+    pub cli_extension: E::FStarOptions,
 }
 
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Subcommand, Debug, Clone)]
-pub enum Backend {
+pub enum Backend<E: Extension> {
     /// Use the F* backend
-    Fstar(FStarOptions),
+    Fstar(FStarOptions<E>),
     /// Use the Coq backend
     Coq,
     /// Use the SSProve backend
@@ -179,7 +184,7 @@ pub enum Backend {
     ProVerif(ProVerifOptions),
 }
 
-impl fmt::Display for Backend {
+impl fmt::Display for Backend<()> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             Backend::Fstar(..) => write!(f, "fstar"),
@@ -290,9 +295,9 @@ pub struct TranslationOptions {
 
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Parser, Debug, Clone)]
-pub struct BackendOptions {
+pub struct BackendOptions<E: Extension> {
     #[command(subcommand)]
-    pub backend: Backend,
+    pub backend: Backend<E>,
 
     /// Don't write anything on disk. Output everything as JSON to stdout
     /// instead.
@@ -336,17 +341,20 @@ pub struct BackendOptions {
     /// Defaults to "<crate folder>/proofs/<backend>/extraction".
     #[arg(long)]
     pub output_dir: Option<PathBuf>,
+
+    #[group(flatten)]
+    pub cli_extension: E::BackendOptions,
 }
 
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Subcommand, Debug, Clone)]
-pub enum Command {
+pub enum Command<E: Extension> {
     /// Translate to a backend. The translated modules will be written
     /// under the directory `<PKG>/proofs/<BACKEND>/extraction`, where
     /// `<PKG>` is the translated cargo package name and `<BACKEND>`
     /// the name of the backend.
     #[clap(name = "into")]
-    Backend(BackendOptions),
+    Backend(BackendOptions<E>),
 
     /// Export directly as a JSON file
     JSON {
@@ -374,9 +382,12 @@ pub enum Command {
         #[arg(short = 'E', long = "include-extra", default_value = "false")]
         include_extra: bool,
     },
+
+    #[command(flatten)]
+    CliExtension(E::Command),
 }
 
-impl Command {
+impl<E: Extension> Command<E> {
     pub fn body_kinds(&self) -> Vec<ExportBodyKind> {
         match self {
             Command::JSON { kind, .. } => kind.clone(),
@@ -395,7 +406,7 @@ pub enum ExportBodyKind {
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Parser, Debug, Clone)]
 #[command(author, version = concat!("commit=", env!("HAX_GIT_COMMIT_HASH"), " ", "describe=", env!("HAX_GIT_DESCRIBE")), name = "hax", about, long_about = None)]
-pub struct Options {
+pub struct ExtensibleOptions<E: Extension> {
     /// Replace the expansion of each macro matching PATTERN by their
     /// invocation. PATTERN denotes a rust path (i.e. `A::B::c`) in
     /// which glob patterns are allowed. The glob pattern * matches
@@ -423,7 +434,7 @@ pub struct Options {
     pub cargo_flags: Vec<String>,
 
     #[command(subcommand)]
-    pub command: Command,
+    pub command: Command<E>,
 
     /// `cargo` caching is enable by default, this flag disables it.
     #[arg(long="disable-cargo-cache", action=clap::builder::ArgAction::SetFalse)]
@@ -447,16 +458,21 @@ pub struct Options {
     /// if not present.
     #[arg(long, default_value = "human")]
     pub message_format: MessageFormat,
+
+    #[group(flatten)]
+    pub extension: E::Options,
 }
 
+pub type Options = ExtensibleOptions<()>;
+
 #[derive_group(Serializers)]
 #[derive(JsonSchema, ValueEnum, Debug, Clone, Copy, Eq, PartialEq)]
 pub enum MessageFormat {
     Human,
     Json,
 }
 
-impl NormalizePaths for Command {
+impl<E: Extension> NormalizePaths for Command<E> {
     fn normalize_paths(&mut self) {
         use Command::*;
         match self {

hax-types/src/diagnostics/message.rs

@@ -21,7 +21,7 @@ pub enum HaxMessage {
     } = 2,
     CargoBuildFailure = 3,
     WarnExperimentalBackend {
-        backend: Backend,
+        backend: Backend<()>,
     } = 4,
 }
 

hax-types/src/engine_api.rs

@@ -6,7 +6,7 @@ type ThirBody = hax_frontend_exporter::ThirBody;
 #[derive_group(Serializers)]
 #[derive(JsonSchema, Debug, Clone)]
 pub struct EngineOptions {
-    pub backend: BackendOptions,
+    pub backend: BackendOptions<()>,
     pub input: Vec<hax_frontend_exporter::Item<ThirBody>>,
     pub impl_infos: Vec<(
         hax_frontend_exporter::DefId,