From faa24621f70461fff39c8afb5f679654a1fa0660 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 26 Nov 2024 13:35:36 +0100 Subject: [PATCH] Unify (an extended version of) opaque and interface-only in a single erasure mechanism. --- engine/backends/fstar/fstar_ast.ml | 1 + engine/backends/fstar/fstar_backend.ml | 76 +++++----- engine/backends/proverif/proverif_backend.ml | 3 +- engine/bin/lib.ml | 4 +- engine/lib/import_thir.ml | 149 ++++++++++++------- engine/lib/import_thir.mli | 2 +- hax-lib/macros/src/dummy.rs | 1 + hax-lib/macros/src/implementation.rs | 13 +- hax-lib/macros/types/src/lib.rs | 4 +- hax-lib/src/proc_macros.rs | 4 +- 10 files changed, 153 insertions(+), 104 deletions(-) diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index 0ead59bd5..0906c846c 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/engine/backends/fstar/fstar_ast.ml @@ -9,6 +9,7 @@ module Ident = FStar_Ident let dummyRange = Range.dummyRange let id ident = Ident.mk_ident (ident, dummyRange) +let id_prime (ident : Ident.ident) = id (ident.idText ^ "'") let lid path = let init, last = List.(drop_last_exn path, last_exn path) in diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index f179ffe38..f70275899 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -874,6 +874,26 @@ struct | `VerbatimIntf of string * [ `NoNewline | `Newline ] | `Comment of string ] list = + let is_opaque = + Attrs.find_unique_attr e.attrs + ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ()) + |> Option.is_some + in + let opaque_impl name ty attrs = + let name' = F.id_prime name in + + [ + F.decl ~quals:[ Assumption ] ~fsti:false ~attrs + @@ F.AST.Assume (name', ty); + F.decl ~fsti:false + @@ F.AST.TopLevelLet + ( NoLetQualifier, + [ + ( F.pat @@ F.AST.PatVar (name, None, []), + F.term @@ F.AST.Var (F.lid_of_id @@ name') ); + ] ); + ] + in match e.v with | Alias { name; item } -> (* These should come from bundled items (in the case of cyclic module dependencies). @@ -938,7 +958,10 @@ struct in let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in - if interface_mode then [ impl; intf ] else [ full ] + + if is_opaque then intf :: opaque_impl name arrow_typ [] + else if interface_mode then [ impl; intf ] + else [ full ] | TyAlias { name; generics; ty } -> let pat = F.pat @@ -971,10 +994,7 @@ struct |> List.map ~f:to_pattern) ), ty ); ] ) - | Type { name; generics; _ } - when Attrs.find_unique_attr e.attrs - ~f:([%eq: Types.ha_payload] OpaqueType >> Fn.flip Option.some_if ()) - |> Option.is_some -> + | Type { name; generics; _ } when is_opaque -> if not ctx.interface_mode then Error.raise @@ { @@ -1471,18 +1491,13 @@ struct in let body = F.term @@ F.AST.Record (None, fields) in let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in - let has_type = - List.exists items ~f:(fun { ii_v; _ } -> - match ii_v with IIType _ -> true | _ -> false) - in - let impl_val = ctx.interface_mode && not has_type in let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in - if impl_val then + if is_opaque then let generics_binders = List.map ~f:FStarBinder.to_binder generics in let val_type = F.term @@ F.AST.Product (generics_binders, typ) in let v = F.AST.Val (name, val_type) in (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v) - @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl + @ opaque_impl name val_type [ tcinst ] else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl | Quote { quote; _ } -> let fstar_opts = @@ -1529,8 +1544,7 @@ let make (module M : Attrs.WITH_ITEMS) ctx = let ctx = ctx end) : S) -let strings_of_item ~signature_only (bo : BackendOptions.t) m items - (item : item) : +let strings_of_item (bo : BackendOptions.t) m items (item : item) : ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list = let interface_mode' : Types.inclusion_kind = List.rev bo.interfaces @@ -1548,8 +1562,7 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items |> Option.value ~default:(Types.Excluded : Types.inclusion_kind) in let interface_mode = - signature_only - || not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode') + not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode') in let (module Print) = make m @@ -1560,21 +1573,18 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items line_width = bo.line_width; } in - let mk_impl = if interface_mode then fun i -> `Impl i else fun i -> `Impl i in + let mk_impl 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' + [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode' in Print.pitem item |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true) |> List.concat_map ~f:(function | `Impl i -> [ (mk_impl (Print.decl_to_string i), `Newline) ] | `Intf i -> [ (mk_intf (Print.decl_to_string i), `Newline) ] - | `VerbatimIntf (s, nl) -> - [ ((if interface_mode then `Intf s else `Impl s), nl) ] - | `VerbatimImpl (s, nl) -> - [ ((if interface_mode then `Impl s else `Impl s), nl) ] + | `VerbatimIntf (s, nl) -> [ (mk_intf s, nl) ] + | `VerbatimImpl (s, nl) -> [ (`Impl s, nl) ] | `Comment s -> let s = "(* " ^ s ^ " *)" in if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ] @@ -1582,8 +1592,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items type rec_prefix = NonRec | FirstMutRec | MutRec -let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m - items : string * string = +let string_of_items ~mod_name ~bundles (bo : BackendOptions.t) m items : + string * string = let collect_trait_goal_idents = object inherit [_] Visitors.reduce as super @@ -1656,7 +1666,7 @@ let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m List.concat_map ~f:(fun item -> let recursivity_prefix = get_recursivity_prefix item in - let strs = strings_of_item ~signature_only bo m items item in + let strs = strings_of_item bo m items item in match (recursivity_prefix, item.v) with | FirstMutRec, Fn _ -> replace_in_strs ~pattern:"let" ~with_:"let rec" strs @@ -1709,20 +1719,8 @@ let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list 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 = module_name ns in - let impl, intf = - string_of_items ~signature_only ~mod_name ~bundles bo m items - in + let impl, intf = string_of_items ~mod_name ~bundles bo m items in let make ~ext body = if String.is_empty body then None else diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 3b1c6e56b..95778622b 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -630,8 +630,7 @@ module Make (Options : OPTS) : MAKE = struct if Attrs.find_unique_attr item.attrs ~f: - ([%eq: Types.ha_payload] OpaqueType - >> Fn.flip Option.some_if ()) + ([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ()) |> Option.is_some then default_lines else default_lines ^^ destructor_lines diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 944089d01..5695dd087 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -36,14 +36,14 @@ let import_thir_items (include_clauses : Types.inclusion_clause list) include_clauses |> List.last in - let drop_body = + let type_only = (* 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) + Import_thir.import_item ~type_only item) items |> List.map ~f:snd in diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index f1f2550db..34f9624a5 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1440,26 +1440,49 @@ let cast_of_enum typ_name generics typ thir_span in { v; span; ident; attrs = [] } -let rec c_item ~ident ~drop_body (item : Thir.item) : item list = +let rec c_item ~ident ~type_only (item : Thir.item) : item list = try Span.with_owner_hint item.owner_id (fun _ -> - c_item_unwrapped ~ident ~drop_body item) + c_item_unwrapped ~ident ~type_only 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 ~drop_body (item : Thir.item) : item list = +and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in if should_skip item.attributes then [] else let span = Span.of_thir item.span in let attrs = c_item_attrs item.attributes in + let erased_by_user = + Attr_payloads.payloads attrs + |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)]) + in + let erased_by_type_only = + type_only + && + match item.kind with + | Fn _ | Static _ -> true + | Impl { of_trait = Some _; items; _ } + when List.exists items ~f:(fun item -> + match item.kind with Type _ -> true | _ -> false) + |> not -> + true + | _ -> false + in + let attrs = + if erased_by_type_only && not erased_by_user then + Attr_payloads.to_attr Erased span :: attrs + else attrs + in + let erased = erased_by_user || erased_by_type_only in + let mk_one v = { span; v; ident; attrs } in let mk v = [ mk_one v ] in let drop_body = - drop_body + erased && Attr_payloads.payloads attrs |> List.exists ~f:(fst >> [%matches? (NeverDropBody : Types.ha_payload)]) @@ -1475,7 +1498,7 @@ and c_item_unwrapped ~ident ~drop_body (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 = []; safety = Safe; } @@ -1499,6 +1522,12 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = params = c_fn_params item.span params; safety = csafety safety; } + | (Enum (_, generics, _) | Struct (_, generics)) when erased -> + let generics = c_generics generics in + let is_struct = match item.kind with Struct _ -> true | _ -> false in + let def_id = Option.value_exn item.def_id in + let name = Concrete_ident.of_def_id Type def_id in + mk @@ Type { name; generics; variants = []; is_struct } | Enum (variants, generics, repr) -> let def_id = Option.value_exn item.def_id in let generics = c_generics generics in @@ -1681,11 +1710,65 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ~f:(fun { attributes; _ } -> not (should_skip attributes)) items in - let has_type = - List.exists items ~f:(fun item -> - match item.kind with Type _ -> true | _ -> false) + let items = + if erased then + [ + { + ii_span = Span.of_thir item.span; + ii_generics = { params = []; constraints = [] }; + ii_v = + IIFn + { + body = U.unit_expr span; + params = [ U.make_unit_param span ]; + }; + ii_ident = + Concrete_ident.of_name Value + Rust_primitives__hax__dropped_body; + ii_attrs = []; + }; + ] + else + List.map + ~f:(fun (item : Thir.impl_item) -> + (* TODO: introduce a Kind.TraitImplItem or + something. Otherwise we have to assume every + backend will see traits and impls as + records. See https://github.com/hacspec/hax/issues/271. *) + let ii_ident = Concrete_ident.of_def_id Field item.owner_id in + { + ii_span = Span.of_thir item.span; + ii_generics = c_generics item.generics; + ii_v = + (match (item.kind : Thir.impl_item_kind) with + | Fn { body; params; _ } -> + let params = + if List.is_empty params then + [ U.make_unit_param span ] + else List.map ~f:(c_param item.span) params + in + IIFn { body = c_expr body; params } + | Const (_ty, e) -> IIFn { body = c_expr e; params = [] } + | Type { ty; parent_bounds } -> + IIType + { + typ = c_ty item.span ty; + parent_bounds = + List.filter_map + ~f:(fun (clause, impl_expr, span) -> + let* bound = c_clause span clause in + match bound with + | GCType trait_goal -> + Some + (c_impl_expr span impl_expr, trait_goal) + | _ -> None) + parent_bounds; + }); + ii_ident; + ii_attrs = c_item_attrs item.attributes; + }) + items in - let c_e = if has_type then c_expr else c_body in mk @@ Impl { @@ -1695,49 +1778,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ( Concrete_ident.of_def_id Trait of_trait.def_id, List.map ~f:(c_generic_value item.span) of_trait.generic_args ); - items = - List.map - ~f:(fun (item : Thir.impl_item) -> - (* TODO: introduce a Kind.TraitImplItem or - something. Otherwise we have to assume every - backend will see traits and impls as - records. See https://github.com/hacspec/hax/issues/271. *) - let ii_ident = - Concrete_ident.of_def_id Field item.owner_id - in - { - ii_span = Span.of_thir item.span; - ii_generics = c_generics item.generics; - ii_v = - (match (item.kind : Thir.impl_item_kind) with - | Fn { body; params; _ } -> - let params = - if List.is_empty params then - [ U.make_unit_param span ] - else List.map ~f:(c_param item.span) params - in - IIFn { body = c_e body; params } - | Const (_ty, e) -> IIFn { body = c_e e; params = [] } - | Type { ty; parent_bounds } -> - IIType - { - typ = c_ty item.span ty; - parent_bounds = - List.filter_map - ~f:(fun (clause, impl_expr, span) -> - let* bound = c_clause span clause in - match bound with - | GCType trait_goal -> - Some - ( c_impl_expr span impl_expr, - trait_goal ) - | _ -> None) - parent_bounds; - }); - ii_ident; - ii_attrs = c_item_attrs item.attributes; - }) - items; + items; parent_bounds = List.filter_map ~f:(fun (clause, impl_expr, span) -> @@ -1787,7 +1828,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = | TraitAlias _ -> mk NotImplementedYet -let import_item ~drop_body (item : Thir.item) : +let import_item ~type_only (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 = @@ -1797,6 +1838,6 @@ let import_item ~drop_body (item : Thir.item) : >> U.Reducers.disambiguate_local_idents in Diagnostics.Core.capture (fun _ -> - c_item item ~ident ~drop_body |> List.map ~f) + c_item item ~ident ~type_only |> List.map ~f) in (ident, (r, reports)) diff --git a/engine/lib/import_thir.mli b/engine/lib/import_thir.mli index 42a5f2184..370af4c05 100644 --- a/engine/lib/import_thir.mli +++ b/engine/lib/import_thir.mli @@ -5,6 +5,6 @@ val import_clause : Types.span -> Types.clause -> Ast.Rust.generic_constraint option val import_item : - drop_body:bool -> + type_only:bool -> Types.item_for__decorated_for__expr_kind -> Concrete_ident.t * (Ast.Rust.item list * Diagnostics.t list) diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs index 5134763c6..8b40ac9b3 100644 --- a/hax-lib/macros/src/dummy.rs +++ b/hax-lib/macros/src/dummy.rs @@ -29,6 +29,7 @@ identity_proc_macro_attribute!( process_init, process_write, process_read, + opaque, opaque_type, refinement_type, fstar_replace, diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index f71f1891c..4874b1671 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -621,9 +621,18 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr /// type without revealing its definition. #[proc_macro_error] #[proc_macro_attribute] -pub fn opaque_type(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { +#[deprecated(note = "Please use 'opaque' instead")] +pub fn opaque_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + opaque(attr, item) +} + +/// Mark a struct or an enum opaque: the extraction will assume the +/// type without revealing its definition. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn opaque(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { let item: Item = parse_macro_input!(item); - let attr = AttrPayload::OpaqueType; + let attr = AttrPayload::Erased; quote! {#attr #item}.into() } diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs index bbb1d4575..0b12b90a8 100644 --- a/hax-lib/macros/types/src/lib.rs +++ b/hax-lib/macros/types/src/lib.rs @@ -130,8 +130,8 @@ pub enum AttrPayload { PVConstructor, PVHandwritten, TraitMethodNoPrePost, - /// Make a type opaque - OpaqueType, + /// Make something opaque + Erased, } pub const HAX_TOOL: &str = "_hax"; diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 866c7cfda..d5f0684a3 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -2,8 +2,8 @@ //! proc-macro crate cannot export anything but procedural macros. pub use hax_lib_macros::{ - attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type, - refinement_type, requires, trait_fn_decoration, + attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque, + opaque_type, refinement_type, requires, trait_fn_decoration, }; pub use hax_lib_macros::{