From d5bf025e17b7da98e19129cdc3aadc67cf8499b5 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 27 Nov 2024 15:03:33 +0100 Subject: [PATCH] Document and correct. --- engine/lib/import_thir.ml | 6 +++ hax-lib/macros/types/src/lib.rs | 2 +- ...oolchain__attribute-opaque into-fstar.snap | 40 +++++--------- .../toolchain__interface-only into-fstar.snap | 54 +++++++++---------- tests/attribute-opaque/src/lib.rs | 4 +- 5 files changed, 48 insertions(+), 58 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 36750dee1..20b37e25b 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1456,11 +1456,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = else let span = Span.of_thir item.span in let attrs = c_item_attrs item.attributes in + (* this is true if the user explicilty requested to erase using the `opaque` macro *) let erased_by_user attrs = Attr_payloads.payloads attrs |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)]) in let item_erased_by_user = erased_by_user attrs in + (* This is true if the item should be erased because we are in type-only mode + (Only certain kinds of items are erased in this case). *) let erased_by_type_only = type_only && @@ -1473,6 +1476,8 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = true | _ -> false in + (* If the item is erased in type-only mode we need to add the Erased attribute. + It is already present if the item is erased by user. *) let attrs = if erased_by_type_only && not item_erased_by_user then Attr_payloads.to_attr Erased span :: attrs @@ -1718,6 +1723,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let items = if erased then [ + (* Dummy associated item *) { ii_span = Span.of_thir item.span; ii_generics = { params = []; constraints = [] }; diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs index 0b12b90a8..34c6aa1c8 100644 --- a/hax-lib/macros/types/src/lib.rs +++ b/hax-lib/macros/types/src/lib.rs @@ -130,7 +130,7 @@ pub enum AttrPayload { PVConstructor, PVHandwritten, TraitMethodNoPrePost, - /// Make something opaque + /// Make an item opaque Erased, } diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index 6a0d0e065..9727c3f6d 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -23,23 +23,7 @@ info: - +** --- exit = 0 -stderr = ''' -warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead - --> attribute-opaque/src/lib.rs:1:3 - | -1 | #[hax_lib::opaque_type] - | ^^^^^^^^^^^^^^^^^^^^ - | - = note: `#[warn(deprecated)]` on by default - -warning: use of deprecated macro `hax_lib::opaque_type`: Please use 'opaque' instead - --> attribute-opaque/src/lib.rs:7:3 - | -7 | #[hax_lib::opaque_type] - | ^^^^^^^^^^^^^^^^^^^^ - -warning: `attribute-opaque` (lib) generated 2 warnings - Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs''' +stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs' [stdout] diagnostics = [] @@ -51,6 +35,11 @@ module Attribute_opaque open Core open FStar.Mul +assume +val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + +let f = f' + [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl_T_for_u8': t_T u8 @@ -61,11 +50,6 @@ assume val c': u8 let c = c' - -assume -val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) - -let f = f' ''' "Attribute_opaque.fsti" = ''' module Attribute_opaque @@ -73,20 +57,20 @@ module Attribute_opaque open Core open FStar.Mul +val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 + +val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 + +val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) + class t_T (v_Self: Type0) = { f_d_pre:Prims.unit -> Type0; f_d_post:Prims.unit -> Prims.unit -> Type0; f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result) } -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 - -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 - [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_T_for_u8:t_T u8 val c:u8 - -val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) ''' 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 ce2c3fe06..3aafed2bc 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -33,11 +33,31 @@ module Interface_only open Core open FStar.Mul -type t_Bar = | Bar : t_Bar +/// 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. +/// Expressions within type are still extracted, as well as pre- and +/// post-conditions. +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) -type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global } +assume +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) -type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } +let f = f' + +type t_Bar = | Bar : t_Bar /// Non-inherent implementations are extracted, their bodies are not /// dropped. This might be a bit surprising: see @@ -68,6 +88,8 @@ val from__from': u8 -> t_Bar let from__from = from__from' +type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global } + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit @@ -77,6 +99,8 @@ val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit let impl_2 = impl_2' +type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit @@ -85,28 +109,4 @@ assume val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit let impl_3 = impl_3' - -/// 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. -/// Expressions within type are still extracted, as well as pre- and -/// post-conditions. -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) - -assume -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) - -let f = f' ''' diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index 6e262cd1b..30030a143 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -1,10 +1,10 @@ -#[hax_lib::opaque_type] +#[hax_lib::opaque] struct OpaqueStruct { field: [T; X], other_field: U, } -#[hax_lib::opaque_type] +#[hax_lib::opaque] enum OpaqueEnum { A([T; X]), B(U),