Merge pull request #470 from hacspec/feat-fstar-fsti-only

feat(engine/fstar): `--interfaces`: add option to extract only `fsti`

cli/options/src/lib.rs

@@ -125,20 +125,20 @@ pub struct FStarOptions {
     #[arg(long, default_value = "1")]
     ifuel: u32,
     /// Modules for which Hax should extract interfaces (`*.fsti`
-    /// files). By default we extract no interface. This flag expects
-    /// a space-separated list of inclusion clauses. An inclusion
-    /// clause is a Rust path prefixed with `+` or `-`. `-` excludes
-    /// any matched item, `+` includes any matched item. By default,
-    /// every item is included. Rust path chunks can be either a
-    /// concrete string, or a glob (just like bash globs, but with
-    /// Rust paths).
+    /// files) in supplement to implementations (`*.fst` files). By
+    /// default we extract no interface, only implementations. This
+    /// flag expects a space-separated list of inclusion clauses. An
+    /// inclusion clause is a Rust path prefixed with `+`, `+!` or
+    /// `-`. `-` means implementation only, `+!` means interface only
+    /// and `+` means implementation and interface. Rust path chunks
+    /// can be either a concrete string, or a glob (just like bash
+    /// globs, but with Rust paths).
     #[arg(
         long,
         value_parser = parse_inclusion_clause,
         value_delimiter = ' ',
         allow_hyphen_values(true)
     )]
-    // TODO: InclusionKind is a bit too expressive here, see https://github.com/hacspec/hax/issues/397
     interfaces: Vec<InclusionClause>,
 }
 
@@ -167,7 +167,7 @@ impl fmt::Display for Backend {
 
 #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)]
 enum InclusionKind {
-    Included { with_deps: bool },
+    Included { strict: bool },
     Excluded,
 }
 
@@ -187,12 +187,12 @@ fn parse_inclusion_clause(
     let (prefix, mut namespace) = s.split_at(1);
     let kind = match prefix {
         "+" => InclusionKind::Included {
-            with_deps: match namespace.split_at(1) {
+            strict: match namespace.split_at(1) {
                 ("!", rest) => {
                     namespace = rest;
-                    false
+                    true
                 }
-                _ => true,
+                _ => false,
             },
         },
         "-" => InclusionKind::Excluded,

engine/backends/fstar/fstar_backend.ml

@@ -1157,7 +1157,7 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
 
 let strings_of_item (bo : BackendOptions.t) m items (item : item) :
     [> `Impl of string | `Intf of string ] list =
-  let interface_mode =
+  let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
     |> List.find ~f:(fun (clause : Types.inclusion_clause) ->
            let namespace = clause.namespace in
@@ -1169,9 +1169,11 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) :
              }
            in
            Concrete_ident.matches_namespace namespace item.ident)
-    |> Option.map ~f:(fun (clause : Types.inclusion_clause) ->
-           match clause.kind with Types.Excluded -> false | _ -> true)
-    |> Option.value ~default:false
+    |> Option.map ~f:(fun (clause : Types.inclusion_clause) -> clause.kind)
+    |> Option.value ~default:(Types.Excluded : Types.inclusion_kind)
+  in
+  let interface_mode =
+    not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
   in
   let (module Print) =
     make m
@@ -1184,6 +1186,10 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) :
   let mk_impl = if interface_mode then fun i -> `Impl i else fun i -> `Impl i in
   let mk_intf = if interface_mode then fun i -> `Intf i else fun i -> `Impl i in
   Print.pitem item
+  |> (match interface_mode' with
+     | Types.Included { strict = true } ->
+         List.filter ~f:(function `Impl _ -> false | _ -> true)
+     | _ -> Fn.id)
   |> List.concat_map ~f:(function
        | `Impl i -> [ mk_impl (decl_to_string i) ]
        | `Intf i -> [ mk_intf (decl_to_string i) ]

engine/lib/dependencies.ml

@@ -245,7 +245,7 @@ module Make (F : Features.T) = struct
     let show_inclusion_clause Types.{ kind; namespace } =
       (match kind with
       | Excluded -> "-"
-      | Included { with_deps = true } -> "+"
+      | Included { strict = false } -> "+"
       | Included _ -> "+!")
       ^ (List.map
            ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s)
@@ -255,11 +255,11 @@ module Make (F : Features.T) = struct
     let apply_clause selection' (clause : Types.inclusion_clause) =
       let matches = Concrete_ident.matches_namespace clause.Types.namespace in
       let matched = Set.filter ~f:matches selection in
-      let with_deps =
-        [%matches? (Included { with_deps = true } : Types.inclusion_kind)]
+      let without_deps =
+        [%matches? (Included { strict = true } : Types.inclusion_kind)]
           clause.kind
       in
-      let matched = matched |> if with_deps then deps_of else Fn.id in
+      let matched = matched |> if without_deps then Fn.id else deps_of in
       Logs.info (fun m ->
           m "The clause [%s] will %s the following Rust items:\n%s"
             (show_inclusion_clause clause)