diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index a3b5a6cae..0ead59bd5 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/engine/backends/fstar/fstar_ast.ml @@ -117,3 +117,4 @@ let decl_of_string s = match decls_of_string s with [ d ] -> d | _ -> failwith "decl_of_string" let ascribe t e = term @@ AST.Ascribed (e, t, None, false) +let implies p q = AST.Op (id "==>", [ p; q ]) |> term diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 6e245ba43..000aed8fc 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -688,6 +688,10 @@ struct let ident = F.id ("x" ^ Int.to_string nth) in { kind = Explicit; ident; typ = pty span typ } + let of_named_typ span name typ : t = + let ident = plocal_ident name in + { kind = Explicit; ident; typ = pty span typ } + let to_pattern (x : t) : F.AST.pattern = let subpat = match x.kind with @@ -740,87 +744,6 @@ struct Error.assertion_failure span "pgeneric_constraint_bd:LIFETIME" | GCType { goal; name = _ } -> c_trait_goal span goal - let get_attr (type a) (name : string) (map : string -> a) (attrs : attrs) : - a option = - List.find_map - ~f:(fun attr -> - match attr.kind with - | Tool { path; tokens } when [%eq: string] path name -> - Some (map tokens) - | _ -> None) - attrs - - module UUID : sig - type t - - val of_attrs : attrs -> t option - val associated_items : ?kind:string -> t option -> item list - val associated_item : ?kind:string -> t option -> item option - end = struct - (* TODO: parse_quoted_string is incorrect *) - let parse_quoted_string = String.strip ~drop:([%eq: char] '"') - - let parse_associated_with s = - let uuid, kind = String.lsplit2 ~on:',' s |> Option.value_exn in - let uuid = parse_quoted_string uuid in - let kind = String.strip ~drop:([%eq: char] ' ') kind in - (uuid, kind) - - type t = string - - let of_attrs : attrs -> t option = get_attr "_hax::uuid" parse_quoted_string - - let associated_items ?kind (uuid : t option) : item list = - let ( let* ) x f = Option.bind ~f x in - Option.value ~default:[] - (let* uuid = uuid in - List.filter - ~f:(fun item -> - Option.value ~default:false - (let* uuid', kind' = - get_attr "_hax::associated_with" parse_associated_with - item.attrs - in - let kind_eq = - match kind with - | Some kind -> String.equal kind' kind - | None -> true - in - Some (kind_eq && String.equal uuid' uuid))) - ctx.items - |> Option.some) - - let associated_item ?kind (uuid : t option) : item option = - match associated_items ?kind uuid with - | [ i ] -> Some i - | [] -> None - | _ -> failwith "expected 0-1 items" - end - - (* TODO: incorrect *) - let fvar_of_params = function - | { pat = { p = PBinding { var; _ }; _ }; _ } -> var - | _ -> failwith "?? todo" - - let associated_refinement (free_variables : string list) (attrs : attrs) : - expr option = - UUID.associated_item ~kind:"refinement" (UUID.of_attrs attrs) - |> Option.map ~f:(function - | { v = Fn { params; body; _ }; _ } -> - let substs = - List.zip_exn - (List.map ~f:fvar_of_params params) - (List.map ~f:Local_ident.make_final free_variables) - in - let v = - U.Mappers.rename_local_idents (fun i -> - match List.find ~f:(fst >> [%eq: local_ident] i) substs with - | None -> i - | Some (_, i) -> i) - in - v#visit_expr () body - | _ -> failwith "expected associated_refinement") - let pmaybe_refined_ty span (free_variables : string list) (attrs : attrs) (binder_name : string) (ty : ty) : F.AST.term = match Attrs.associated_refinement_in_type free_variables attrs with @@ -1285,7 +1208,112 @@ struct let ty = F.term @@ F.AST.Product (inputs, ty_pre_post) in [ (F.id name, None, [], ty) ] | TIFn ty -> + let weakest = + let h kind = + Attrs.associated_fns kind i.ti_attrs |> List.hd + in + Option.first_some (h Ensures) (h Requires) + |> Option.map ~f:(fun (generics, params, expr) -> + let dummy_self = + List.find generics.params + ~f:[%matches? { kind = GPType _; _ }] + |> Option.value_or_thunk ~default:(fun () -> + Error.assertion_failure i.ti_span + ("Expected a first generic of type \ + `Self`. Instead generics params \ + are: " + ^ [%show: generic_param list] + generics.params)) + |> fun x -> x.ident + in + let self = + Local_ident.{ name = "Self"; id = mk_id Typ 0 } + in + let renamer = + let f (id : local_ident) = + if [%eq: string] dummy_self.name id.name then + self + else id + in + U.Mappers.rename_local_idents f + in + let generics = + renamer#visit_generics () generics + in + let params = + List.map ~f:(renamer#visit_param ()) params + in + let expr = renamer#visit_expr () expr in + (generics, params, expr)) + in let ty = pty e.span ty in + let ty = + let variables = + let idents_visitor = U.Reducers.collect_local_idents in + idents_visitor#visit_trait_item () i + :: (Option.map + ~f:(fun (generics, params, expr) -> + [ + idents_visitor#visit_generics () generics; + idents_visitor#visit_expr () expr; + ] + @ List.map + ~f:(idents_visitor#visit_param ()) + params) + weakest + |> Option.value ~default:[]) + |> Set.union_list (module Local_ident) + |> Set.to_list |> ref + in + let mk_fresh prefix = + let v = U.fresh_local_ident_in !variables prefix in + variables := v :: !variables; + v + in + let bindings = ref [] in + let f (p : param) = + let name = + match p.pat.p with + | PBinding { var; _ } -> var + | _ -> + let name = mk_fresh "x" in + let ({ span; typ; _ } : pat) = p.pat in + let expr = { e = LocalVar name; span; typ } in + bindings := (p.pat, expr) :: !bindings; + name + in + FStarBinder.of_named_typ p.pat.span name p.typ + in + weakest + |> Option.map ~f:(List.map ~f |> map_snd3) + |> Option.map + ~f:(fun (generics, binders, (expr : expr)) -> + let result_ident = mk_fresh "pred" in + let result_bd = + FStarBinder.of_named_typ expr.span result_ident + expr.typ + in + let typ = pty expr.span expr.typ in + let expr = U.make_lets !bindings expr in + let expr = pexpr expr in + let result = + F.term + @@ F.AST.Var + (plocal_ident result_ident |> F.lid_of_id) + in + let result = + F.AST.Refine + ( FStarBinder.to_binder result_bd, + F.implies result expr ) + |> F.term + in + F.AST.Product + ( List.map ~f:FStarBinder.to_binder binders, + result ) + |> F.term) + |> Option.value ~default:ty + in + let ty = F.term @@ F.AST.Product diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index c5dcba702..65aca6eb6 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -378,13 +378,6 @@ module Make (F : Features.T) = struct method! visit_local_ident () x = Set.singleton (module Local_ident) x end - let collect_local_idents = - object - inherit [_] Visitors.reduce as _super - inherit [_] Sets.Local_ident.monoid as _m - method! visit_local_ident () x = Set.singleton (module Local_ident) x - end - include struct open struct type env = Local_ident.t list @@ -742,6 +735,11 @@ module Make (F : Features.T) = struct if pat_is_expr lhs body then rhs else { body with e = Let { monadic = None; lhs; rhs; body } } + let make_lets (lbs : (pat * expr) list) (body : expr) = + List.fold_right ~init:body + ~f:(fun (pat, expr) body -> make_let pat expr body) + lbs + let make_var_pat (var : local_ident) (typ : ty) (span : span) : pat = { p = PBinding { mut = Immutable; mode = ByValue; var; typ; subpat = None }; diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml index 3789ada31..6f31247a2 100644 --- a/engine/lib/phases/phase_traits_specs.ml +++ b/engine/lib/phases/phase_traits_specs.ml @@ -28,8 +28,8 @@ module Make (F : Features.T) = let v = match item.v with | Trait { name; generics; items } -> - let f (item : trait_item) = - let mk kind = + let f attrs (item : trait_item) = + let mk role kind = let ti_ident = mk_name item.ti_ident kind in { item with @@ -38,15 +38,25 @@ module Make (F : Features.T) = [ Attr_payloads.to_attr TraitMethodNoPrePost item.ti_span; - ]; + ] + @ (List.filter + ~f: + [%matches? + Types.AssociatedItem { role = role'; _ }, _ when + [%eq: Types.ha_assoc_role] role role'] + attrs + |> List.map ~f:(uncurry Attr_payloads.to_attr)); } in match item.ti_v with | TIFn (TArrow (inputs, output)) -> [ - { (mk "pre") with ti_v = TIFn (TArrow (inputs, TBool)) }; { - (mk "post") with + (mk Types.Requires "pre") with + ti_v = TIFn (TArrow (inputs, TBool)); + }; + { + (mk Types.Ensures "post") with ti_v = TIFn (TArrow (inputs @ [ output ], TBool)); }; ] @@ -54,7 +64,22 @@ module Make (F : Features.T) = | TIType _ -> [ (* TODO REFINEMENTS FOR TYPES *) ] in let items = - List.concat_map ~f:(fun item -> f item @ [ item ]) items + List.concat_map + ~f:(fun item -> + let attrs = Attr_payloads.payloads item.ti_attrs in + let ti_attrs = + attrs + |> List.filter + ~f: + (fst + >> [%matches? + Types.AssociatedItem + { role = Ensures | Requires; _ }] + >> not) + |> List.map ~f:(uncurry Attr_payloads.to_attr) + in + f attrs item @ [ { item with ti_attrs } ]) + items in Trait { name; generics; items } | Impl { generics; self_ty; of_trait; items; parent_bounds } -> diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index f95291209..915c4736a 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -450,6 +450,8 @@ module Raw = struct let generics = pgeneric_params ti.ti_generics.params in let bounds = pgeneric_constraints ti.ti_span ti.ti_generics.constraints in let ident = !(Concrete_ident_view.to_definition_name ti.ti_ident) in + pattrs ti.ti_attrs + & match ti.ti_v with | TIType _ -> !"type " & ident & !": TodoPrintRustBoundsTyp;" | TIFn ty -> @@ -481,6 +483,8 @@ module Raw = struct let generics = pgeneric_params ii.ii_generics.params in let bounds = pgeneric_constraints span ii.ii_generics.constraints in let ident = !(Concrete_ident_view.to_definition_name ii.ii_ident) in + pattrs ii.ii_attrs + & match ii.ii_v with | IIType _ -> !"type " & ident & !": TodoPrintRustBoundsTyp;" | IIFn { body; params } -> diff --git a/hax-lib-macros/src/impl_fn_decoration.rs b/hax-lib-macros/src/impl_fn_decoration.rs new file mode 100644 index 000000000..da39b500c --- /dev/null +++ b/hax-lib-macros/src/impl_fn_decoration.rs @@ -0,0 +1,87 @@ +//! This module defines the `ImplFnDecoration` structure and utils +//! around it. + +use crate::prelude::*; +use crate::utils::*; + +/// Supporting structure that holds the data required by the internal +/// macro `impl_fn_decoration`. +pub struct ImplFnDecoration { + pub kind: FnDecorationKind, + pub phi: Expr, + pub generics: Generics, + pub self_ty: Type, +} + +/// The various strings allowed as decoration kinds. +pub const DECORATION_KINDS: &[&str] = &["decreases", "ensures", "requires"]; + +/// Expects a `Path` to be a decoration kind: `::hax_lib::`, +/// `hax_lib::` or `` in (with `KIND` in +/// `DECORATION_KINDS`). +pub fn expects_path_decoration(path: &Path) -> Result> { + let path_span = path.span(); + let path = path + .expect_simple_path() + .ok_or_else(|| Error::new(path_span, "Expected a simple path, with no `<...>`."))?; + Ok( + match path + .iter() + .map(|x| x.as_str()) + .collect::>() + .as_slice() + { + [kw] | ["", "hax_lib", kw] | ["hax_lib", kw] if DECORATION_KINDS.contains(kw) => { + Some(kw.to_string()) + } + _ => None, + }, + ) +} + +impl parse::Parse for ImplFnDecoration { + fn parse(input: parse::ParseStream) -> Result { + let parse_next = || -> Result<_> { + input.parse::()?; + let mut generics = input.parse::()?; + input.parse::()?; + generics.where_clause = input.parse::>()?; + input.parse::()?; + let self_ty = input.parse::()?; + input.parse::()?; + Ok((generics, self_ty)) + }; + + let path = input.parse::()?; + let path_span = path.span(); + let kind = match expects_path_decoration(&path)? { + Some(s) => match s.as_str() { + "decreases" => FnDecorationKind::Decreases, + "requires" => FnDecorationKind::Requires, + "ensures" => { + let (generics, self_ty) = parse_next()?; + let ExprClosure1 { arg, body } = input.parse::()?; + input.parse::()?; + return Ok(ImplFnDecoration { + kind: FnDecorationKind::Ensures { ret_binder: arg }, + phi: body, + generics, + self_ty, + }); + } + _ => unreachable!(), + } + None => Err(Error::new(path_span, "Expected `::hax_lib::`, `hax_lib::` or `` with `KIND` in {DECORATION_KINDS:?}"))?, + }; + + let (generics, self_ty) = parse_next()?; + let phi = input.parse::()?; + input.parse::()?; + Ok(ImplFnDecoration { + kind, + phi, + generics, + self_ty, + }) + } +} diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 01f2cb1e2..046c7c6d7 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -1,3 +1,4 @@ +mod impl_fn_decoration; mod quote; mod rewrite_self; mod syn_ext; @@ -18,6 +19,7 @@ mod prelude { pub type FnLike = syn::ImplItemFn; } +use impl_fn_decoration::*; use prelude::*; use utils::*; @@ -272,61 +274,14 @@ pub fn ensures(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream .into() } -struct ImplFnDecoration { - pub kind: FnDecorationKind, - pub phi: Expr, - pub generics: Generics, - pub self_ty: Type, -} - mod kw { + syn::custom_keyword!(hax_lib); syn::custom_keyword!(decreases); syn::custom_keyword!(ensures); syn::custom_keyword!(requires); syn::custom_keyword!(refine); } -impl parse::Parse for ImplFnDecoration { - fn parse(input: parse::ParseStream) -> Result { - let parse_next = || -> Result<_> { - input.parse::()?; - let mut generics = input.parse::()?; - input.parse::()?; - generics.where_clause = input.parse::>()?; - input.parse::()?; - let self_ty = input.parse::()?; - input.parse::()?; - Ok((generics, self_ty)) - }; - let kind = if let Ok(_) = input.parse::() { - FnDecorationKind::Decreases - } else if let Ok(_) = input.parse::() { - FnDecorationKind::Requires - } else if let Ok(_) = input.parse::() { - let (generics, self_ty) = parse_next()?; - let ExprClosure1 { arg, body } = input.parse::()?; - input.parse::()?; - return Ok(ImplFnDecoration { - kind: FnDecorationKind::Ensures { ret_binder: arg }, - phi: body, - generics, - self_ty, - }); - } else { - return Err(input.lookahead1().error()); - }; - let (generics, self_ty) = parse_next()?; - let phi = input.parse::()?; - input.parse::()?; - Ok(ImplFnDecoration { - kind, - phi, - generics, - self_ty, - }) - } -} - /// Internal macro for dealing with function decorations /// (`#[decreases(...)]`, `#[ensures(...)]`, `#[requires(...)]`) on /// `fn` items within an `impl` block. There is special handling since @@ -350,6 +305,28 @@ pub fn impl_fn_decoration(attr: pm::TokenStream, item: pm::TokenStream) -> pm::T quote! {#attr #item}.into() } +#[proc_macro_error] +#[proc_macro_attribute] +pub fn trait_fn_decoration(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let ImplFnDecoration { + kind, + phi, + generics, + self_ty, + } = parse_macro_input!(attr); + let mut item: syn::TraitItemFn = parse_macro_input!(item); + let (decoration, attr) = + make_fn_decoration(phi, item.sig.clone(), kind, Some(generics), Some(self_ty)); + let decoration = Stmt::Item(Item::Verbatim(decoration)); + item.sig + .generics + .where_clause + .get_or_insert(parse_quote! {where}) + .predicates + .push(parse_quote! {[(); {#decoration 0}]:}); + quote! {#attr #item}.into() +} + /// Enable the following attrubutes in the annotated item and sub-items: /// - (in a struct) `refine`: refine a type with a logical formula /// - (on a `fn` in an `impl`) `decreases`, `ensures`, `requires`: @@ -384,26 +361,75 @@ pub fn impl_fn_decoration(attr: pm::TokenStream, item: pm::TokenStream) -> pm::T pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { let item: Item = parse_macro_input!(item); - struct AttrVisitor {} + #[derive(Default)] + struct AttrVisitor { + extra_items: Vec, + } use syn::visit_mut; impl VisitMut for AttrVisitor { + fn visit_item_trait_mut(&mut self, item: &mut ItemTrait) { + let span = item.span(); + for ti in item.items.iter_mut() { + if let TraitItem::Fn(fun) = ti { + for attr in &mut fun.attrs { + let Meta::List(ml) = attr.meta.clone() else { + continue; + }; + let Ok(Some(decoration)) = expects_path_decoration(&ml.path) else { + continue; + }; + let decoration = syn::Ident::new(&decoration, ml.path.span()); + + let mut generics = item.generics.clone(); + let predicate = WherePredicate::Type(PredicateType { + lifetimes: None, + bounded_ty: parse_quote! {Self_}, + colon_token: Token![:](span), + bounds: item.supertraits.clone(), + }); + let mut where_clause = generics + .where_clause + .clone() + .unwrap_or(parse_quote! {where}); + where_clause.predicates.push(predicate.clone()); + generics.where_clause = Some(where_clause.clone()); + let self_ty: Type = parse_quote! {Self_}; + let tokens = ml.tokens.clone(); + let generics = merge_generics(parse_quote! {}, generics); + let ImplFnDecoration { + kind, phi, self_ty, .. + } = parse_quote! {#decoration, #generics, where, #self_ty, #tokens}; + let (decoration, relation_attr) = make_fn_decoration( + phi, + fun.sig.clone(), + kind, + Some(generics), + Some(self_ty), + ); + *attr = parse_quote! {#relation_attr}; + self.extra_items.push(decoration); + } + } + } + visit_mut::visit_item_trait_mut(self, item); + } + fn visit_type_mut(&mut self, _type: &mut Type) {} fn visit_item_impl_mut(&mut self, item: &mut ItemImpl) { for ii in item.items.iter_mut() { if let ImplItem::Fn(fun) = ii { for attr in fun.attrs.iter_mut() { if let Meta::List(ml) = &mut attr.meta { - let decoration = &ml.path; - if decoration.ends_with("requires") - || decoration.ends_with("ensures") - || decoration.ends_with("decreases") - { - let tokens = ml.tokens.clone(); - let (generics, self_ty) = (&item.generics, &item.self_ty); - let where_clause = &generics.where_clause; - ml.tokens = quote! {#decoration, #generics, #where_clause, #self_ty, #tokens}; - ml.path = parse_quote! {::hax_lib::impl_fn_decoration}; - } + let Ok(Some(decoration)) = expects_path_decoration(&ml.path) else { + continue; + }; + let decoration = syn::Ident::new(&decoration, ml.path.span()); + let tokens = ml.tokens.clone(); + let (generics, self_ty) = (&item.generics, &item.self_ty); + let where_clause = &generics.where_clause; + ml.tokens = + quote! {#decoration, #generics, #where_clause, #self_ty, #tokens}; + ml.path = parse_quote! {::hax_lib::impl_fn_decoration}; } } } @@ -474,11 +500,12 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr } } - let mut v = AttrVisitor {}; + let mut v = AttrVisitor::default(); let mut item = item; v.visit_item_mut(&mut item); + let extra_items = v.extra_items; - quote! { #item }.into() + quote! { #item #(#extra_items)* }.into() } /// Mark a struct or an enum opaque: the extraction will assume the diff --git a/hax-lib-macros/src/rewrite_self.rs b/hax-lib-macros/src/rewrite_self.rs index 8df936d22..364f4d88a 100644 --- a/hax-lib-macros/src/rewrite_self.rs +++ b/hax-lib-macros/src/rewrite_self.rs @@ -1,30 +1,82 @@ +use crate::syn_ext::*; use proc_macro2::Span; use syn::spanned::Spanned; use syn::*; +/// The `RewriteSelf` structure is hidden in a module so that only its +/// method can mutate its fields. mod rewrite_self { use super::*; + use std::collections::HashSet; + + /// Small & dirty wrapper around spans to make them `Eq`, + /// `PartialEq` and `Hash` + #[derive(Clone, Debug)] + struct SpanWrapper(Span); + const _: () = { + impl Eq for SpanWrapper {} + impl PartialEq for SpanWrapper { + fn eq(&self, other: &Self) -> bool { + format!("{self:?}") == format!("{other:?}") + } + } + use std::hash::*; + impl Hash for SpanWrapper { + fn hash(&self, state: &mut H) { + format!("{self:?}").hash(state) + } + } + }; + + /// A struct that carries informations for substituting `self` and + /// `Self`. Note `typ` is an option: + #[must_use] pub struct RewriteSelf { - self_detected: bool, typ: Option, ident: Ident, + self_spans: HashSet, } + impl RewriteSelf { - pub fn self_ident(&mut self) -> Ident { - self.self_detected = true; - self.ident.clone() + /// Consumes `RewriteSelf`, optionally outputing errors. + pub fn get_error(self) -> Option { + if self.typ.is_some() || self.self_spans.is_empty() { + return None; + } + + let mut error = Error::new(Span::call_site(), "This macro doesn't work on trait or impl items: you need to add a `#[hax_lib::attributes]` on the enclosing impl block or trait."); + for SpanWrapper(span) in self.self_spans { + let use_site = Error::new( + span, + "Here, the function you are trying to annotate has a `Self`.", + ); + error.combine(use_site); + } + Some(error.to_compile_error()) + } + + fn self_detected(&mut self, span: Span) { + self.self_spans.insert(SpanWrapper(span)); } + + /// Requests the ident with which `self` should be substituted. + pub fn self_ident(&mut self, span: Span) -> &Ident { + self.self_detected(span); + &self.ident + } + /// Requests the type with which `Self` should be substituted with. pub fn self_ty(&mut self, span: Span) -> Type { - self.self_detected = true; + self.self_detected(span); self.typ.clone().unwrap_or_else(|| { - Type::Verbatim(Error::new(span, "Detected a `self`").to_compile_error()) + parse_quote! {Self} }) } + /// Construct a rewritter pub fn new(ident: Ident, typ: Option) -> Self { Self { typ, ident, - self_detected: false, + self_spans: HashSet::new(), } } } @@ -32,47 +84,34 @@ mod rewrite_self { pub use rewrite_self::*; impl visit_mut::VisitMut for RewriteSelf { - fn visit_expr_path_mut(&mut self, i: &mut ExprPath) { - let ExprPath { - qself: None, - path: - Path { - leading_colon: None, - segments, - }, - .. - } = i - else { - return (); - }; - if segments.len() != 1 { - return (); + fn visit_expr_mut(&mut self, e: &mut Expr) { + visit_mut::visit_expr_mut(self, e); + if e.is_ident("self") { + let into = self.self_ident(e.span()).clone(); + *e = parse_quote! {#into} } - let Some(PathSegment { - ident, - arguments: PathArguments::None, - }) = segments.first_mut() - else { - return (); - }; - if ident.to_string() == "self" { - let into = self.self_ident().clone(); - *ident = parse_quote! {#into} + } + fn visit_type_mut(&mut self, ty: &mut Type) { + visit_mut::visit_type_mut(self, ty); + if ty.is_ident("Self") { + *ty = self.self_ty(ty.span()) } } fn visit_fn_arg_mut(&mut self, arg: &mut FnArg) { + visit_mut::visit_fn_arg_mut(self, arg); if let FnArg::Receiver(r) = arg { + let span = r.self_token.span(); *arg = FnArg::Typed(PatType { attrs: r.attrs.clone(), pat: Box::new(Pat::Ident(PatIdent { attrs: vec![], by_ref: None, mutability: None, - ident: self.self_ident().clone(), + ident: self.self_ident(span.clone()).clone(), subpat: None, })), colon_token: token::Colon(arg.span()), - ty: Box::new(self.self_ty(arg.span())), + ty: Box::new(self.self_ty(span.clone())), }); } } diff --git a/hax-lib-macros/src/syn_ext.rs b/hax-lib-macros/src/syn_ext.rs index bb37f84aa..83e8dd746 100644 --- a/hax-lib-macros/src/syn_ext.rs +++ b/hax-lib-macros/src/syn_ext.rs @@ -1,15 +1,16 @@ use crate::prelude::*; use syn::parse::*; +use syn::punctuated::Punctuated; /// A closure expression of arity 1, e.g. `|x| x + 3` pub struct ExprClosure1 { - pub arg: syn::Pat, - pub body: syn::Expr, + pub arg: Pat, + pub body: Expr, } impl Parse for ExprClosure1 { fn parse(ps: ParseStream) -> Result { - let closure: syn::ExprClosure = Parse::parse(ps as ParseStream)?; + let closure: ExprClosure = Parse::parse(ps as ParseStream)?; let inputs = closure.inputs; if inputs.len() != 1 { Err(Error::new(inputs.span(), "Expected exactly one argument"))?; @@ -27,15 +28,32 @@ pub trait PathExt { /// attribute from an attribute from another crate that share a /// common name. fn ends_with(&self, i: &str) -> bool; + + /// Expects a simple path (no `<...>`). + fn expect_simple_path(&self) -> Option>; } impl PathExt for Path { fn ends_with(&self, i: &str) -> bool { - matches!(self.segments.iter().last(), Some(syn::PathSegment { + matches!(self.segments.iter().last(), Some(PathSegment { ident, - arguments: syn::PathArguments::None, + arguments: PathArguments::None, }) if i == ident.to_string().as_str()) } + + fn expect_simple_path(&self) -> Option> { + let mut chunks = vec![]; + if self.leading_colon.is_some() { + chunks.push(String::new()) + } + for segment in &self.segments { + chunks.push(format!("{}", segment.ident)); + if !matches!(segment.arguments, PathArguments::None) { + return None; + } + } + return Some(chunks); + } } /// Utility trait to extract an `Ident` from various syn types @@ -57,7 +75,7 @@ impl ExpectIdent for Box { } } -fn expect_punctuated_1(x: &syn::punctuated::Punctuated) -> Option { +fn expect_punctuated_1(x: &Punctuated) -> Option { (x.len() == 1).then(|| x.first().unwrap().clone()) } @@ -70,10 +88,36 @@ impl ExpectIdent for Path { impl ExpectIdent for Expr { fn expect_ident(&self) -> Option { match self { - syn::Expr::Path(syn::ExprPath { + Expr::Path(ExprPath { qself: None, path, .. }) => path.expect_ident(), _ => None, } } } + +impl ExpectIdent for Type { + fn expect_ident(&self) -> Option { + match self { + Type::Path(TypePath { + qself: None, path, .. + }) => path.expect_ident(), + _ => None, + } + } +} + +impl ExpectIdent for Pat { + fn expect_ident(&self) -> Option { + match self { + Pat::Ident(PatIdent { + by_ref: None, + mutability: None, + ident, + subpat: None, + .. + }) => Some(ident.clone()), + _ => None, + } + } +} diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index 7015b9bb6..f1b9a5391 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -50,7 +50,7 @@ impl From for AssociationRole { } /// Merge two `syn::Generics`, respecting lifetime orders -fn merge_generics(x: Generics, y: Generics) -> Generics { +pub(crate) fn merge_generics(x: Generics, y: Generics) -> Generics { Generics { lt_token: x.lt_token.or(y.lt_token), gt_token: x.gt_token.or(y.gt_token), @@ -184,18 +184,24 @@ pub fn make_fn_decoration( mut phi: Expr, mut signature: Signature, kind: FnDecorationKind, - generics: Option, + mut generics: Option, self_type: Option, ) -> (TokenStream, AttrPayload) { let uid = ItemUid::fresh(); let mut_ref_inputs = unmut_references_in_inputs(&mut signature); let self_ident: Ident = syn::parse_quote! {self_}; - let mut rewriter = RewriteSelf::new(self_ident, self_type); - rewriter.visit_expr_mut(&mut phi); + let error = { + let mut rewriter = RewriteSelf::new(self_ident, self_type); + rewriter.visit_expr_mut(&mut phi); + rewriter.visit_signature_mut(&mut signature); + if let Some(generics) = generics.as_mut() { + rewriter.visit_generics_mut(generics); + } + rewriter.get_error() + }; let decoration = { let decoration_sig = { let mut sig = signature; - rewriter.visit_signature_mut(&mut sig); sig.ident = format_ident!("{}", kind.to_string()); if let FnDecorationKind::Ensures { ret_binder } = &kind { let output = match sig.output { @@ -276,5 +282,5 @@ pub fn make_fn_decoration( role: kind.into(), item: uid, }; - (decoration, assoc_attr) + (quote! {#error #decoration}, assoc_attr) } diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 7d87111f1..f96953222 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -3,7 +3,7 @@ pub use hax_lib_macros::{ attributes, ensures, exclude, impl_fn_decoration, include, lemma, opaque_type, refinement_type, - requires, + requires, trait_fn_decoration, }; pub use hax_lib_macros::{ diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index eccc12ba1..a3956122d 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -80,6 +80,78 @@ let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIn f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ] } ''' +"Attributes.Pre_post_on_traits_and_impls.fst" = ''' +module Attributes.Pre_post_on_traits_and_impls +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class t_Operation (v_Self: Type0) = { + f_double_pre:x: u8 + -> pred: + bool + { pred ==> + (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <= + (127 <: Hax_lib.Int.t_Int) }; + f_double_post:x: u8 -> result: u8 + -> pred: + bool + { pred ==> + ((Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) * (2 <: Hax_lib.Int.t_Int) + <: + Hax_lib.Int.t_Int) = + (Rust_primitives.Hax.Int.from_machine result <: Hax_lib.Int.t_Int) }; + f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result) +} + +class t_Identity (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_8099741844003281729:Core.Cmp.t_Eq v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_12632649257025169145:Core.Cmp.t_PartialEq v_Self + v_Self; + f_identity_pre:self___: v_Self -> pred: bool{pred ==> true}; + f_identity_post:self___: v_Self -> result: v_Self -> pred: bool{pred ==> result =. self___}; + f_identity:x0: v_Self + -> Prims.Pure v_Self (f_identity_pre x0) (fun result -> f_identity_post x0 result) +} + +type t_ViaAdd = | ViaAdd : t_ViaAdd + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: t_Operation t_ViaAdd = + { + f_double_pre + = + (fun (x: u8) -> + (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <= (127 <: Hax_lib.Int.t_Int)); + f_double_post + = + (fun (x: u8) (out: u8) -> + ((Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) * (2 <: Hax_lib.Int.t_Int) + <: + Hax_lib.Int.t_Int) = + (Rust_primitives.Hax.Int.from_machine out <: Hax_lib.Int.t_Int)); + f_double = fun (x: u8) -> x +! x + } + +type t_ViaMul = | ViaMul : t_ViaMul + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl_1: t_Operation t_ViaMul = + { + f_double_pre + = + (fun (x: u8) -> + (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <= (127 <: Hax_lib.Int.t_Int)); + f_double_post + = + (fun (x: u8) (out: u8) -> + ((Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) * (2 <: Hax_lib.Int.t_Int) + <: + Hax_lib.Int.t_Int) = + (Rust_primitives.Hax.Int.from_machine out <: Hax_lib.Int.t_Int)); + f_double = fun (x: u8) -> x *! 2uy + } +''' "Attributes.Refined_arithmetic.fst" = ''' module Attributes.Refined_arithmetic #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index 17e6a6ae8..a2f3db0b3 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -157,6 +157,46 @@ fn some_function() -> String { String::from("hello from Rust") } +mod pre_post_on_traits_and_impls { + use hax_lib::int::*; + + #[hax_lib::attributes] + trait Operation { + // we allow `hax_lib`, `::hax_lib` or no path at all + #[hax_lib::requires(x.lift() <= int!(127))] + #[ensures(|result| x.lift() * int!(2) == result.lift())] + fn double(x: u8) -> u8; + } + + struct ViaAdd; + struct ViaMul; + + #[hax_lib::attributes] + impl Operation for ViaAdd { + #[::hax_lib::requires(x.lift() <= int!(127))] + #[ensures(|result| x.lift() * int!(2) == result.lift())] + fn double(x: u8) -> u8 { + x + x + } + } + + #[hax_lib::attributes] + impl Operation for ViaMul { + #[requires(x.lift() <= int!(127))] + #[::hax_lib::ensures(|result| x.lift() * int!(2) == result.lift())] + fn double(x: u8) -> u8 { + x * 2 + } + } + + #[hax_lib::attributes] + trait Identity: Eq + PartialEq { + #[ensures(|result| result == self)] + #[requires(true)] + fn identity(&self) -> Self; + } +} + /// An minimal example of a model of math integers for F* mod int_model { use super::hax;