From 20e82bd28c557cdc5f196c65046a37842608185c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 18 Apr 2024 13:27:46 +0200 Subject: [PATCH 1/6] feat: include flag: allow for dropping bodies This PR adds the `+:` modifier to inclusion clauses. `-i '... +:some::glob::pattern'` will extract signature-only for the items matched by `some::glob::pattern`. --- cli/options/src/lib.rs | 23 +++++++---- engine/backends/fstar/fstar_backend.ml | 33 ++++++++++----- engine/bin/lib.ml | 31 ++++++++++++-- engine/lib/dependencies.ml | 6 ++- engine/lib/import_thir.ml | 40 ++++++++++++++----- engine/lib/import_thir.mli | 1 + engine/names/src/lib.rs | 4 ++ .../toolchain__interface-only into-fstar.snap | 39 ++++++++++++++++++ tests/Cargo.lock | 4 ++ tests/Cargo.toml | 1 + tests/cli/interface-only/Cargo.toml | 9 +++++ tests/cli/interface-only/src/lib.rs | 19 +++++++++ 12 files changed, 177 insertions(+), 33 deletions(-) create mode 100644 test-harness/src/snapshots/toolchain__interface-only into-fstar.snap create mode 100644 tests/cli/interface-only/Cargo.toml create mode 100644 tests/cli/interface-only/src/lib.rs diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index 6a9af7b39..be5d356f8 100644 --- a/cli/options/src/lib.rs +++ b/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::(), s.chars().skip_while(f).into_iter().collect::(), @@ -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 { @@ -239,13 +244,15 @@ 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 `-`. `-` + /// 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). + /// (without including dependencies) and `+:` includes only types + /// and signatures informations about 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). #[arg( value_parser = parse_inclusion_clause, value_delimiter = ' ', diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 870df9abe..c11524672 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -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,11 +1302,12 @@ 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) ] @@ -1313,9 +1315,10 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) : 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 diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 5e03c2351..91ae9e95d 100644 --- a/engine/bin/lib.ml +++ b/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,6 +67,7 @@ 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) -> @@ -51,6 +75,7 @@ let import_thir_items (include_clauses : Types.inclusion_clause list) items |> List.dedup_and_sort ~compare:Diagnostics.compare in + (* Report every error *) List.iter ~f:Diagnostics.Core.report reports; items diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index ca0a85acd..7c3aa6179 100644 --- a/engine/lib/dependencies.ml +++ b/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 diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 8555fa751..74c765309 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -215,6 +215,7 @@ end module Make (CTX : sig val is_core_item : bool + val drop_body : bool end) : EXPR = struct let c_binop (op : Thir.bin_op) (lhs : expr) (rhs : expr) (span : span) (typ : ty) = @@ -316,7 +317,7 @@ end) : EXPR = struct U.call' (`Concrete name) [ lhs; rhs ] span typ let rec c_expr (e : Thir.decorated_for__expr_kind) : expr = - try c_expr_unwrapped e + try (if CTX.drop_body then c_expr_drop_body else c_expr_unwrapped) e with Diagnostics.SpanFreeError.Exn (Data (ctx, kind)) -> let typ : ty = try c_ty e.span e.ty @@ -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 = @@ -1076,6 +1086,7 @@ end include struct open Make (struct let is_core_item = false + let drop_body = false end) let import_ty : Types.span -> Types.ty -> Ast.Rust.ty = c_ty @@ -1088,15 +1099,21 @@ include struct c_predicate_kind end -let make ~krate : (module EXPR) = +(** Instantiate the functor for translating expressions. Two options +can configured: the crate name (there are special handling related to +`core`) and `drop_body` (if enabled, original expressions are not +translated, and the dummy global variable `dropped_body` is used +instead) *) +let make ~krate ~drop_body : (module EXPR) = let is_core_item = String.(krate = "core" || krate = "core_hax_model") in let module M : EXPR = Make (struct let is_core_item = is_core_item + let drop_body = drop_body end) in (module M) -let c_trait_item (item : Thir.trait_item) : trait_item = - let open (val make ~krate:item.owner_id.krate : EXPR) in +let c_trait_item (item : Thir.trait_item) ~drop_body : trait_item = + let open (val make ~krate:item.owner_id.krate ~drop_body : EXPR) in let { params; constraints } = c_generics item.generics in (* TODO: see TODO in impl items *) let ti_ident = Concrete_ident.of_def_id Field item.owner_id in @@ -1224,16 +1241,16 @@ 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 = - let open (val make ~krate:item.owner_id.krate : EXPR) in +and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = + let open (val make ~krate:item.owner_id.krate ~drop_body : EXPR) in if should_skip item.attributes then [] else let span = Span.of_thir item.span in @@ -1390,7 +1407,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list = in let params = self :: params in let generics = { params; constraints } in - let items = List.map ~f:c_trait_item items in + let items = List.map ~f:(c_trait_item ~drop_body) items in mk @@ Trait { name; generics; items } | Trait (Yes, _, _, _, _) -> unimplemented [ item.span ] "Auto trait" | Trait (_, Unsafe, _, _, _) -> unimplemented [ item.span ] "Unsafe trait" @@ -1541,7 +1558,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list = | 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 = @@ -1550,6 +1567,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)) diff --git a/engine/lib/import_thir.mli b/engine/lib/import_thir.mli index 44a771a4c..2ab0c3e5e 100644 --- a/engine/lib/import_thir.mli +++ b/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) diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 6cf7ff9ef..6b582a365 100644 --- a/engine/names/src/lib.rs +++ b/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() {} diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap new file mode 100644 index 000000000..4fa8d55d6 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -0,0 +1,39 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: interface-only + manifest: cli/interface-only/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: "+:** -interface_only::Foo" + backend_options: ~ +--- +exit = 0 +stderr = ''' +Compiling interface-only v0.1.0 (WORKSPACE_ROOT/cli/interface-only) + Finished dev [unoptimized + debuginfo] target(s) in XXs''' + +[stdout] +diagnostics = [] + +[stdout.files] +"Interface_only.fsti" = ''' +module Interface_only +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +val f (x: u8) : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 610369e3c..6f242bd0d 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -364,6 +364,10 @@ dependencies = [ "hashbrown", ] +[[package]] +name = "interface-only" +version = "0.1.0" + [[package]] name = "itertools" version = "0.10.5" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 896e574ef..8dd33e0b7 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -29,6 +29,7 @@ members = [ "proverif-noise", "proverif-fn-to-letfun", "cli/include-flag", + "cli/interface-only", "recursion", ] resolver = "2" diff --git a/tests/cli/interface-only/Cargo.toml b/tests/cli/interface-only/Cargo.toml new file mode 100644 index 000000000..53b93ecba --- /dev/null +++ b/tests/cli/interface-only/Cargo.toml @@ -0,0 +1,9 @@ +[package] +name = "interface-only" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[package.metadata.hax-tests] +into."fstar" = { include-flag = "+:** -interface_only::Foo" } diff --git a/tests/cli/interface-only/src/lib.rs b/tests/cli/interface-only/src/lib.rs new file mode 100644 index 000000000..fdff9536f --- /dev/null +++ b/tests/cli/interface-only/src/lib.rs @@ -0,0 +1,19 @@ +#![allow(dead_code)] + +/// This item contains unsafe blocks and raw references, two features +/// not supported by hax. Thanks to the `-i` flag and the `+:` +/// modifier, `f` is still extractable as an interface. +fn f(x: u8) { + let y = x as *const i8; + + unsafe { + println!("{}", *y); + } +} + +/// This struct contains a field which uses raw pointers, which are +/// not supported by hax. This item cannot be extracted at all: we +/// need to exclude it with `-i '-*::Foo'`. +struct Foo { + unsupported_field: *const u8, +} From 84e258b89e5c85eb6eb18cd09105c1f1f6bcbcb4 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 22 Apr 2024 09:02:38 +0200 Subject: [PATCH 2/6] feat(cli): better help message for `-i` --- cli/options/src/lib.rs | 41 +++++++++++++++++++++++++++++++---------- 1 file changed, 31 insertions(+), 10 deletions(-) diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index be5d356f8..a4cef020a 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -243,16 +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) and `+:` includes only types - /// and signatures informations about 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). + /// 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, + /// exluding or including items. Ecah 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 = ' ', From a982f8231bb050238678abf323c4e8a7aed97146 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 22 Apr 2024 11:07:36 +0200 Subject: [PATCH 3/6] fix(cli): typo Co-authored-by: Franziskus Kiefer --- cli/options/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index a4cef020a..0cfbf01ce 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -257,7 +257,7 @@ pub struct TranslationOptions { /// By default, hax includes all items. Then, the patterns /// prefixed by modifiers are processed from left to right, - /// exluding or including items. Ecah pattern selects a number of + /// excluding or including items. Each pattern selects a number of /// item. The modifiers are: /// /// - `+`: includes the selected items with their dependencies, From dba74c62b96cea1946c1b19e9b2742b88e44c8fa Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 22 Apr 2024 11:50:44 +0200 Subject: [PATCH 4/6] fix: typo --- engine/backends/fstar/fstar_backend.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index c11524672..97cae64b3 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/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; } From 433511fa80dbfd08ed68643481e9503dd7c36762 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 22 Apr 2024 11:58:40 +0200 Subject: [PATCH 5/6] feat(engine): drop only _some_ bodies As @franziskuskiefer noted, some signature-relevant pieces of expressions were dropped: - constants within types (e.g. a function that returns `[u8; 4]`, `4` was dropped); - pre or post-condition on functions; - methods in implementations (see #616) This commit: - keeps expr translations on types and methods; - disables body drops when a function is marked with hax' attribute `AttrPayload::NeverDropBody` (see `hax-lib-macros/types/lib.rs`). --- engine/lib/import_thir.ml | 44 +++++++++---------- hax-lib-macros/src/lib.rs | 3 +- hax-lib-macros/src/utils.rs | 2 + hax-lib-macros/types/src/lib.rs | 4 ++ .../toolchain__interface-only into-fstar.snap | 8 +++- tests/Cargo.lock | 4 ++ tests/cli/interface-only/Cargo.toml | 2 + tests/cli/interface-only/src/lib.rs | 11 ++++- 8 files changed, 53 insertions(+), 25 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 74c765309..30ef7c73d 100644 --- a/engine/lib/import_thir.ml +++ b/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 @@ -215,7 +216,6 @@ end module Make (CTX : sig val is_core_item : bool - val drop_body : bool end) : EXPR = struct let c_binop (op : Thir.bin_op) (lhs : expr) (rhs : expr) (span : span) (typ : ty) = @@ -317,7 +317,7 @@ end) : EXPR = struct U.call' (`Concrete name) [ lhs; rhs ] span typ let rec c_expr (e : Thir.decorated_for__expr_kind) : expr = - try (if CTX.drop_body then c_expr_drop_body else c_expr_unwrapped) e + try c_expr_unwrapped e with Diagnostics.SpanFreeError.Exn (Data (ctx, kind)) -> let typ : ty = try c_ty e.span e.ty @@ -1086,7 +1086,6 @@ end include struct open Make (struct let is_core_item = false - let drop_body = false end) let import_ty : Types.span -> Types.ty -> Ast.Rust.ty = c_ty @@ -1099,21 +1098,18 @@ include struct c_predicate_kind end -(** Instantiate the functor for translating expressions. Two options -can configured: the crate name (there are special handling related to -`core`) and `drop_body` (if enabled, original expressions are not -translated, and the dummy global variable `dropped_body` is used -instead) *) -let make ~krate ~drop_body : (module EXPR) = +(** 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 let is_core_item = is_core_item - let drop_body = drop_body end) in (module M) -let c_trait_item (item : Thir.trait_item) ~drop_body : trait_item = - let open (val make ~krate:item.owner_id.krate ~drop_body : EXPR) in +let c_trait_item (item : Thir.trait_item) : trait_item = + let open (val make ~krate:item.owner_id.krate : EXPR) in let { params; constraints } = c_generics item.generics in (* TODO: see TODO in impl items *) let ti_ident = Concrete_ident.of_def_id Field item.owner_id in @@ -1250,15 +1246,21 @@ let rec c_item ~ident ~drop_body (item : Thir.item) : item list = [ make_hax_error_item span ident error ] and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = - let open (val make ~krate:item.owner_id.krate ~drop_body : EXPR) in + 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) -> @@ -1268,7 +1270,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 = { params = []; constraints = [] }; - body = c_expr body; + body = c_body body; params = []; } | TyAlias (ty, generics) -> @@ -1291,7 +1293,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; } | Enum (variants, generics, repr) -> @@ -1357,7 +1359,6 @@ and c_item_unwrapped ~ident ~drop_body (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 @@ -1407,7 +1408,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = in let params = self :: params in let generics = { params; constraints } in - let items = List.map ~f:(c_trait_item ~drop_body) items in + let items = List.map ~f:c_trait_item items in mk @@ Trait { name; generics; items } | Trait (Yes, _, _, _, _) -> unimplemented [ item.span ] "Auto trait" | Trait (_, Unsafe, _, _, _) -> unimplemented [ item.span ] "Unsafe trait" @@ -1552,7 +1553,6 @@ and c_item_unwrapped ~ident ~drop_body (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 _ -> diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 21413a1a0..4e4ad3611 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -145,7 +145,8 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { ); } } - quote! { #attr #item }.into() + use AttrPayload::NeverDropBody; + quote! { #attr #NeverDropBody #item }.into() } /* diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index 52ee9d5d9..4c9247b27 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -187,6 +187,7 @@ pub fn make_fn_decoration( } else { quote! {} }; + use AttrPayload::NeverDropBody; quote! { #[cfg(#DebugOrHaxCfgExpr)] #late_skip @@ -197,6 +198,7 @@ pub fn make_fn_decoration( #uid_attr #late_skip #[allow(unused)] + #NeverDropBody #decoration_sig { #phi } diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index f73f964f6..aa5fee516 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/hax-lib-macros/types/src/lib.rs @@ -71,6 +71,10 @@ pub enum AttrPayload { item: ItemUid, }, Uid(ItemUid), + /// Mark an item so that hax never drop its body (this is useful + /// for pre- and post- conditions of a function we dropped the + /// body of: pre and post are part of type signature) + NeverDropBody, /// Mark an item as a lemma statement to prove in the backend Lemma, Language, diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap index 4fa8d55d6..7e475d230 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -35,5 +35,11 @@ module Interface_only open Core open FStar.Mul -val f (x: u8) : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) +val f (x: u8) + : Prims.Pure (t_Array u8 (sz 4)) + (requires x <. 254uy) + (ensures + fun r -> + let r:t_Array u8 (sz 4) = r in + (r.[ sz 0 ] <: u8) >. x) ''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 6f242bd0d..aaaf2d857 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -367,6 +367,10 @@ dependencies = [ [[package]] name = "interface-only" version = "0.1.0" +dependencies = [ + "hax-lib", + "hax-lib-macros", +] [[package]] name = "itertools" diff --git a/tests/cli/interface-only/Cargo.toml b/tests/cli/interface-only/Cargo.toml index 53b93ecba..8d36bd687 100644 --- a/tests/cli/interface-only/Cargo.toml +++ b/tests/cli/interface-only/Cargo.toml @@ -4,6 +4,8 @@ version = "0.1.0" edition = "2021" [dependencies] +hax-lib-macros = { path = "../../../hax-lib-macros" } +hax-lib = { path = "../../../hax-lib" } [package.metadata.hax-tests] into."fstar" = { include-flag = "+:** -interface_only::Foo" } diff --git a/tests/cli/interface-only/src/lib.rs b/tests/cli/interface-only/src/lib.rs index fdff9536f..e28d48468 100644 --- a/tests/cli/interface-only/src/lib.rs +++ b/tests/cli/interface-only/src/lib.rs @@ -1,14 +1,23 @@ #![allow(dead_code)] +use hax_lib as hax; + /// This item contains unsafe blocks and raw references, two features /// not supported by hax. Thanks to the `-i` flag and the `+:` /// modifier, `f` is still extractable as an interface. -fn f(x: u8) { +/// +/// Expressions within type are still extracted, as well as pre- and +/// post-conditions. +#[hax::requires(x < 254)] +#[hax::ensures(|r| r[0] > x)] +fn f(x: u8) -> [u8; 4] { let y = x as *const i8; unsafe { println!("{}", *y); } + + [x + 1, x, x, x] } /// This struct contains a field which uses raw pointers, which are From 93b32fa73de11fe3ee0eae44906c158824cf2aa0 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 22 Apr 2024 12:17:31 +0200 Subject: [PATCH 6/6] feat(engine): more tests for dropping bodies --- .../toolchain__interface-only into-fstar.snap | 20 ++++++++++++++++++ tests/cli/interface-only/src/lib.rs | 21 +++++++++++++++++++ 2 files changed, 41 insertions(+) diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap index 7e475d230..9d392ab5e 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -42,4 +42,24 @@ val f (x: u8) fun r -> let r:t_Array u8 (sz 4) = r in (r.[ sz 0 ] <: u8) >. x) + +type t_Bar = | Bar : t_Bar + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: Core.Convert.t_From t_Bar Prims.unit = + { + f_from_pre = (fun ((): Prims.unit) -> true); + f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true); + f_from = fun ((): Prims.unit) -> Bar <: t_Bar + } + +val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl_1: Core.Convert.t_From t_Bar u8 = + { + f_from_pre = (fun (x: u8) -> true); + f_from_post = (fun (x: u8) (out: t_Bar) -> true); + f_from = fun (x: u8) -> from__from x + } ''' diff --git a/tests/cli/interface-only/src/lib.rs b/tests/cli/interface-only/src/lib.rs index e28d48468..8805b203a 100644 --- a/tests/cli/interface-only/src/lib.rs +++ b/tests/cli/interface-only/src/lib.rs @@ -26,3 +26,24 @@ fn f(x: u8) -> [u8; 4] { struct Foo { unsupported_field: *const u8, } + +struct Bar; + +/// Non-inherent implementations are extracted, their bodies are not +/// dropped. This might be a bit surprising: see +/// https://github.com/hacspec/hax/issues/616. +impl From<()> for Bar { + fn from((): ()) -> Self { + Bar + } +} + +/// If you need to drop the body of a method, please hoist it: +impl From for Bar { + fn from(x: u8) -> Self { + fn from(_: u8) -> Bar { + Bar + } + from(x) + } +}