Merge branch 'main' into charon_traits_merge

cli/options/src/lib.rs

@@ -145,8 +145,11 @@ pub struct FStarOptions {
     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. This
-    /// flag expects a space-separated list of inclusion clauses. An
+    /// default we extract no interface, only implementations. If a
+    /// item is signature only (see the `+:` prefix of the
+    /// `--include_namespaces` flag of the `into` subcommand), then
+    /// its namespace is extracted with an interface. 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
@@ -198,6 +201,7 @@ enum DepsKind {
 enum InclusionKind {
     /// `+query` include the items selected by `query`
     Included(DepsKind),
+    SignatureOnly,
     Excluded,
 }
 
@@ -215,7 +219,7 @@ fn parse_inclusion_clause(
         Err("Expected `-` or `+`, got an empty string")?
     }
     let (prefix, namespace) = {
-        let f = |&c: &char| matches!(c, '+' | '-' | '~' | '!');
+        let f = |&c: &char| matches!(c, '+' | '-' | '~' | '!' | ':');
         (
             s.chars().take_while(f).into_iter().collect::<String>(),
             s.chars().skip_while(f).into_iter().collect::<String>(),
@@ -225,9 +229,10 @@ fn parse_inclusion_clause(
         "+" => InclusionKind::Included(DepsKind::Transitive),
         "+~" => InclusionKind::Included(DepsKind::Shallow),
         "+!" => InclusionKind::Included(DepsKind::None),
+        "+:" => InclusionKind::SignatureOnly,
         "-" => InclusionKind::Excluded,
         prefix => Err(format!(
-            "Expected `-`, `+~`, `+!` or `-`, got an `{prefix}`"
+            "Expected `+`, `+~`, `+!`, `+:` or `-`, got an `{prefix}`"
         ))?,
     };
     Ok(InclusionClause {
@@ -238,14 +243,37 @@ fn parse_inclusion_clause(
 
 #[derive(JsonSchema, Parser, Debug, Clone, Serialize, Deserialize)]
 pub struct TranslationOptions {
-    /// Space-separated list of inclusion clauses. An inclusion clause
-    /// is a Rust path prefixed with `+`, `+~`, `+!` or `-`. `-`
-    /// excludes any matched item, `+` includes any matched item and
-    /// their dependencies, `+~` includes any matched item and their
-    /// direct dependencies, `+!` includes any matched item strictly
-    /// (without including dependencies). 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).
+    /// Controls which Rust item should be extracted or not.
+    ///
+    /// This is a space-separated list of patterns prefixed with a
+    /// modifier, read from the left to the right.
+    ///
+    /// A pattern is a Rust path (say `mycrate::mymod::myfn`) where
+    /// globs are allowed: `*` matches any name
+    /// (e.g. `mycrate::mymod::myfn` is matched by
+    /// `mycrate::*::myfn`), while `**` matches any subpath, empty
+    /// included (e.g. `mycrate::mymod::myfn` is matched by
+    /// `**::myfn`).
+
+    /// By default, hax includes all items. Then, the patterns
+    /// prefixed by modifiers are processed from left to right,
+    /// excluding or including items. Each pattern selects a number of
+    /// item. The modifiers are:
+    ///
+    ///  - `+`: includes the selected items with their dependencies,
+    /// transitively (e.g. if function `f` calls `g` which in turn
+    /// calls `h`, then `+k::f` includes `f`, `g` and `h`)
+
+    /// {n} - `+~`: includes the selected items with their direct
+    /// dependencies only (following the previous example, `+~k::f`
+    /// would select `f` and `g`, but not `h`)
+
+    /// {n} - `+!`: includes the selected items, without their
+    /// dependencies (`+!k::f` would only select `f`)
+
+    /// {n} - `+:`: only includes the type of the selected items (no
+    /// dependencies). This includes full struct and enums, but only
+    /// the type signature of functions, dropping their bodies.
     #[arg(
         value_parser = parse_inclusion_clause,
         value_delimiter = ' ',

engine/backends/fstar/fstar_backend.ml

@@ -902,8 +902,8 @@ struct
                  AttributeRejected
                    {
                      reason =
-                       "a type cannot be opaque if it's module is not \
-                        extracted as an interface";
+                       "a type cannot be opaque if its module is not extracted \
+                        as an interface";
                    };
                span = e.span;
              }
@@ -1271,8 +1271,8 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
               let ctx = ctx
             end) : S)
 
-let strings_of_item (bo : BackendOptions.t) m items (item : item) :
-    [> `Impl of string | `Intf of string ] list =
+let strings_of_item ~signature_only (bo : BackendOptions.t) m items
+    (item : item) : [> `Impl of string | `Intf of string ] list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
     |> List.find ~f:(fun (clause : Types.inclusion_clause) ->
@@ -1289,7 +1289,8 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) :
     |> Option.value ~default:(Types.Excluded : Types.inclusion_kind)
   in
   let interface_mode =
-    not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
+    signature_only
+    || not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
   in
   let (module Print) =
     make m
@@ -1301,21 +1302,23 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) :
   in
   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
+  let no_impl =
+    signature_only
+    || [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
+  in
   Print.pitem item
-  |> (match interface_mode' with
-     | Types.Included None' ->
-         List.filter ~f:(function `Impl _ -> false | _ -> true)
-     | _ -> Fn.id)
+  |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
        | `Impl i -> [ mk_impl (decl_to_string i) ]
        | `Intf i -> [ mk_intf (decl_to_string i) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
 
-let string_of_items (bo : BackendOptions.t) m items : string * string =
+let string_of_items ~signature_only (bo : BackendOptions.t) m items :
+    string * string =
   let strings =
-    List.concat_map ~f:(strings_of_item bo m items) items
+    List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
     |> List.map ~f:(function
          | `Impl s -> `Impl (String.strip s)
          | `Intf s -> `Intf (String.strip s))
@@ -1343,13 +1346,23 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) :
   U.group_items_by_namespace items
   |> Map.to_alist
   |> List.concat_map ~f:(fun (ns, items) ->
+         let signature_only =
+           let is_dropped_body =
+             Concrete_ident.eq_name Rust_primitives__hax__dropped_body
+           in
+           let contains_dropped_body =
+             U.Reducers.collect_concrete_idents#visit_item ()
+             >> Set.exists ~f:is_dropped_body
+           in
+           List.exists ~f:contains_dropped_body items
+         in
          let mod_name =
            String.concat ~sep:"."
              (List.map
                 ~f:(map_first_letter String.uppercase)
                 (fst ns :: snd ns))
          in
-         let impl, intf = string_of_items bo m items in
+         let impl, intf = string_of_items ~signature_only bo m items in
          let make ~ext body =
            if String.is_empty body then None
            else

engine/bin/lib.ml

@@ -27,13 +27,36 @@ module Attrs = Attr_payloads.MakeBase (Error)
 let import_thir_items (include_clauses : Types.inclusion_clause list)
     (items : Types.item_for__decorated_for__expr_kind list) : Ast.Rust.item list
     =
-  let result = List.map ~f:Import_thir.import_item items |> List.map ~f:snd in
-  let items = List.concat_map ~f:fst result in
+  let imported_items =
+    List.map
+      ~f:(fun item ->
+        let ident = Concrete_ident.(of_def_id Kind.Value item.owner_id) in
+        let most_precise_clause =
+          (* Computes the include clause that apply to `item`, if any *)
+          List.filter
+            ~f:(fun clause ->
+              Concrete_ident.matches_namespace clause.Types.namespace ident)
+            include_clauses
+          |> List.last
+        in
+        let drop_body =
+          (* Shall we drop the body? *)
+          Option.map
+            ~f:(fun clause -> [%matches? Types.SignatureOnly] clause.kind)
+            most_precise_clause
+          |> Option.value ~default:false
+        in
+        Import_thir.import_item ~drop_body item)
+      items
+    |> List.map ~f:snd
+  in
+  let items = List.concat_map ~f:fst imported_items in
+  (* Build a map from idents to error reports *)
   let ident_to_reports =
     List.concat_map
       ~f:(fun (items, reports) ->
         List.map ~f:(fun (item : Ast.Rust.item) -> (item.ident, reports)) items)
-      result
+      imported_items
     |> Map.of_alist_exn (module Concrete_ident)
   in
   let items = Deps.filter_by_inclusion_clauses include_clauses items in
@@ -44,13 +67,15 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
       items
   in
   let items = Deps.sort items in
+  (* Extract error reports for the items we actually extract *)
   let reports =
     List.concat_map
       ~f:(fun (item : Ast.Rust.item) ->
         Map.find_exn ident_to_reports item.ident)
       items
     |> List.dedup_and_sort ~compare:Diagnostics.compare
   in
+  (* Report every error *)
   List.iter ~f:Diagnostics.Core.report reports;
   items
 

engine/lib/dependencies.ml

@@ -249,6 +249,7 @@ module Make (F : Features.T) = struct
     let show_inclusion_clause Types.{ kind; namespace } =
       (match kind with
       | Excluded -> "-"
+      | SignatureOnly -> "+:"
       | Included deps_kind -> (
           match deps_kind with
           | Transitive -> "+"
@@ -270,6 +271,7 @@ module Make (F : Features.T) = struct
         | Included Transitive -> (true, false)
         | Included Shallow -> (true, true)
         | Included None' -> (false, false)
+        | SignatureOnly -> (false, true)
         | Excluded -> (false, false)
       in
       let matched = matched0 |> if with_deps then deps_of else Fn.id in
@@ -282,7 +284,9 @@ module Make (F : Features.T) = struct
             (match clause.kind with Excluded -> "remove" | _ -> "add")
           @@ show_ident_set matched);
       let set_op =
-        match clause.kind with Included _ -> Set.union | Excluded -> Set.diff
+        match clause.kind with
+        | Included _ | SignatureOnly -> Set.union
+        | Excluded -> Set.diff
       in
       let result = set_op selection' matched in
       result

engine/lib/import_thir.ml

@@ -200,6 +200,7 @@ let cast_name_for_type typ_name =
 
 module type EXPR = sig
   val c_expr : Thir.decorated_for__expr_kind -> expr
+  val c_expr_drop_body : Thir.decorated_for__expr_kind -> expr
   val c_ty : Thir.span -> Thir.ty -> ty
   val c_generic_value : Thir.span -> Thir.generic_arg -> generic_value
   val c_generics : Thir.generics -> generics
@@ -326,6 +327,15 @@ end) : EXPR = struct
       U.hax_failure_expr' span typ (ctx, kind)
         ([%show: Thir.decorated_for__expr_kind] e)
 
+  (** Extracts an expression as the global name `dropped_body`: this
+      drops the computational part of the expression, but keeps a
+      correct type and span. *)
+  and c_expr_drop_body (e : Thir.decorated_for__expr_kind) : expr =
+    let typ = c_ty e.span e.ty in
+    let span = Span.of_thir e.span in
+    let v = Global_ident.of_name Value Rust_primitives__hax__dropped_body in
+    { span; typ; e = GlobalVar v }
+
   and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr =
     (* TODO: eliminate that `call`, use the one from `ast_utils` *)
     let call f args =
@@ -1092,6 +1102,9 @@ include struct
     c_predicate_kind
 end
 
+(** Instantiate the functor for translating expressions. The crate
+name can be configured (there are special handling related to `core`)
+*)
 let make ~krate : (module EXPR) =
   let is_core_item = String.(krate = "core" || krate = "core_hax_model") in
   let module M : EXPR = Make (struct
@@ -1228,24 +1241,30 @@ let cast_of_enum typ_name generics typ thir_span
   in
   { v; span; ident; attrs = [] }
 
-let rec c_item ~ident (item : Thir.item) : item list =
-  try c_item_unwrapped ~ident item
+let rec c_item ~ident ~drop_body (item : Thir.item) : item list =
+  try c_item_unwrapped ~ident ~drop_body item
   with Diagnostics.SpanFreeError.Exn payload ->
     let context, kind = Diagnostics.SpanFreeError.payload payload in
     let error = Diagnostics.pretty_print_context_kind context kind in
     let span = Span.of_thir item.span in
     [ make_hax_error_item span ident error ]
 
-and c_item_unwrapped ~ident (item : Thir.item) : item list =
+and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
   let open (val make ~krate:item.owner_id.krate : EXPR) in
   if should_skip item.attributes then []
   else
     let span = Span.of_thir item.span in
-    let mk_one v =
-      let attrs = c_item_attrs item.attributes in
-      { span; v; ident; attrs }
-    in
+    let attrs = c_item_attrs item.attributes in
+    let mk_one v = { span; v; ident; attrs } in
     let mk v = [ mk_one v ] in
+    let drop_body =
+      drop_body
+      && Attr_payloads.payloads attrs
+         |> List.exists
+              ~f:(fst >> [%matches? (NeverDropBody : Types.ha_payload)])
+         |> not
+    in
+    let c_body = if drop_body then c_expr_drop_body else c_expr in
     (* TODO: things might be unnamed (e.g. constants) *)
     match (item.kind : Thir.item_kind) with
     | Const (_, body) ->
@@ -1255,7 +1274,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                name =
                  Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
                generics = { params = []; constraints = [] };
-               body = c_expr body;
+               body = c_body body;
                params = [];
              }
     | TyAlias (ty, generics) ->
@@ -1278,7 +1297,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                name =
                  Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
                generics = c_generics generics;
-               body = c_expr body;
+               body = c_body body;
                params;
              }
     | Enum (variants, generics, repr) ->
@@ -1344,7 +1363,6 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
         let def_id = Option.value_exn item.def_id in
         let is_struct = true in
         (* repeating the attributes of the item in the variant: TODO is that ok? *)
-        let attrs = c_item_attrs item.attributes in
         let v =
           let kind = Concrete_ident.Kind.Constructor { is_struct } in
           let name = Concrete_ident.of_def_id kind def_id in
@@ -1539,13 +1557,12 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                 ];
           }
         in
-        let attrs = c_item_attrs item.attributes in
         [ { span; v; ident = Concrete_ident.of_def_id Value def_id; attrs } ]
     | ExternCrate _ | Static _ | Macro _ | Mod _ | ForeignMod _ | GlobalAsm _
     | OpaqueTy _ | Union _ | TraitAlias _ ->
         mk NotImplementedYet
 
-let import_item (item : Thir.item) :
+let import_item ~drop_body (item : Thir.item) :
     concrete_ident * (item list * Diagnostics.t list) =
   let ident = Concrete_ident.of_def_id Value item.owner_id in
   let r, reports =
@@ -1554,6 +1571,7 @@ let import_item (item : Thir.item) :
         (true, Hashtbl.create (module String))
       >> U.Reducers.disambiguate_local_idents
     in
-    Diagnostics.Core.capture (fun _ -> c_item item ~ident |> List.map ~f)
+    Diagnostics.Core.capture (fun _ ->
+        c_item item ~ident ~drop_body |> List.map ~f)
   in
   (ident, (r, reports))

engine/lib/import_thir.mli

@@ -5,5 +5,6 @@ val import_predicate_kind :
   Types.span -> Types.predicate_kind -> Ast.Rust.trait_goal option
 
 val import_item :
+  drop_body:bool ->
   Types.item_for__decorated_for__expr_kind ->
   Concrete_ident.t * (Ast.Rust.item list * Diagnostics.t list)

engine/names/src/lib.rs

@@ -144,6 +144,10 @@ mod hax {
     fn array_of_list() {}
     fn never_to_any() {}
 
+    /// The engine uses this `dropped_body` symbol as a marker value
+    /// to signal that a item was extracted without body.
+    fn dropped_body() {}
+
     mod control_flow_monad {
         trait ControlFlowMonad {
             fn lift() {}