-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
14 changed files
with
1,467 additions
and
1,282 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,139 @@ | ||
| mod hax_paths; | ||
|
|
||
| use hax_paths::*; | ||
| use proc_macro::TokenStream; | ||
| use quote::quote; | ||
| use syn::{visit_mut::VisitMut, *}; | ||
|
|
||
| macro_rules! identity_proc_macro_attribute { | ||
| ($($name:ident,)*) => { | ||
| $( | ||
| #[proc_macro_attribute] | ||
| pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream { | ||
| item | ||
| } | ||
| )* | ||
| } | ||
| } | ||
|
|
||
| identity_proc_macro_attribute!( | ||
| fstar_options, | ||
| fstar_verification_status, | ||
| include, | ||
| exclude, | ||
| requires, | ||
| ensures, | ||
| pv_handwritten, | ||
| pv_constructor, | ||
| protocol_messages, | ||
| process_init, | ||
| process_write, | ||
| process_read, | ||
| opaque_type, | ||
| refinement_type, | ||
| fstar_replace, | ||
| coq_replace, | ||
| proverif_replace, | ||
| fstar_before, | ||
| coq_before, | ||
| proverif_before, | ||
| fstar_after, | ||
| coq_after, | ||
| proverif_after, | ||
| ); | ||
|
|
||
| #[proc_macro] | ||
| pub fn fstar_expr(_payload: TokenStream) -> TokenStream { | ||
| quote! { () }.into() | ||
| } | ||
| #[proc_macro] | ||
| pub fn coq_expr(_payload: TokenStream) -> TokenStream { | ||
| quote! { () }.into() | ||
| } | ||
| #[proc_macro] | ||
| pub fn proverif_expr(_payload: TokenStream) -> TokenStream { | ||
| quote! { () }.into() | ||
| } | ||
|
|
||
| #[proc_macro_attribute] | ||
| pub fn lemma(_attr: TokenStream, _item: TokenStream) -> TokenStream { | ||
| quote! {}.into() | ||
| } | ||
|
|
||
| fn unsafe_expr() -> TokenStream { | ||
| quote! { ::std::compile_error!("`hax_lib::unsafe_expr` has no meaning outside of hax extraction, please use it solely on hax only places.") }.into() | ||
| } | ||
|
|
||
| #[proc_macro] | ||
| pub fn fstar_unsafe_expr(_payload: TokenStream) -> TokenStream { | ||
| unsafe_expr() | ||
| } | ||
| #[proc_macro] | ||
| pub fn coq_unsafe_expr(_payload: TokenStream) -> TokenStream { | ||
| unsafe_expr() | ||
| } | ||
| #[proc_macro] | ||
| pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream { | ||
| unsafe_expr() | ||
| } | ||
|
|
||
| fn not_hax_attribute(attr: &syn::Attribute) -> bool { | ||
| if let Meta::List(ml) = &attr.meta { | ||
| !matches!(expects_path_decoration(&ml.path), Ok(Some(_))) | ||
| } else { | ||
| true | ||
| } | ||
| } | ||
|
|
||
| fn not_refine_attribute(attr: &syn::Attribute) -> bool { | ||
| if let Meta::List(ml) = &attr.meta { | ||
| !matches!(expects_refine(&ml.path), Ok(Some(_))) | ||
| } else { | ||
| true | ||
| } | ||
| } | ||
|
|
||
| #[proc_macro_attribute] | ||
| pub fn attributes(_attr: TokenStream, item: TokenStream) -> TokenStream { | ||
| let item: Item = parse_macro_input!(item); | ||
|
|
||
| struct AttrVisitor; | ||
|
|
||
| use syn::visit_mut; | ||
| impl VisitMut for AttrVisitor { | ||
| fn visit_item_trait_mut(&mut self, item: &mut ItemTrait) { | ||
| for ti in item.items.iter_mut() { | ||
| if let TraitItem::Fn(fun) = ti { | ||
| fun.attrs.retain(not_hax_attribute) | ||
| } | ||
| } | ||
| 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 { | ||
| fun.attrs.retain(not_hax_attribute) | ||
| } | ||
| } | ||
| visit_mut::visit_item_impl_mut(self, item); | ||
| } | ||
| fn visit_item_mut(&mut self, item: &mut Item) { | ||
| visit_mut::visit_item_mut(self, item); | ||
|
|
||
| match item { | ||
| Item::Struct(s) => { | ||
| for field in s.fields.iter_mut() { | ||
| field.attrs.retain(not_refine_attribute) | ||
| } | ||
| } | ||
| _ => (), | ||
| } | ||
| } | ||
| } | ||
|
|
||
| let mut item = item; | ||
| AttrVisitor.visit_item_mut(&mut item); | ||
|
|
||
| quote! { #item }.into() | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,55 @@ | ||
| //! This module defines the `ImplFnDecoration` structure and utils | ||
| //! around it. | ||
| use syn::spanned::Spanned; | ||
| use syn::*; | ||
|
|
||
| fn expect_simple_path(path: &Path) -> Option<Vec<String>> { | ||
| let mut chunks = vec![]; | ||
| if path.leading_colon.is_some() { | ||
| chunks.push(String::new()) | ||
| } | ||
| for segment in &path.segments { | ||
| chunks.push(format!("{}", segment.ident)); | ||
| if !matches!(segment.arguments, PathArguments::None) { | ||
| return None; | ||
| } | ||
| } | ||
| Some(chunks) | ||
| } | ||
|
|
||
| /// 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::<KIND>`, | ||
| /// `hax_lib::<KIND>` or `<KIND>` in (with `KIND` in | ||
| /// `DECORATION_KINDS`). | ||
| pub fn expects_path_decoration(path: &Path) -> Result<Option<String>> { | ||
| expects_hax_path(DECORATION_KINDS, path) | ||
| } | ||
|
|
||
| /// Expects a path to be `[[::]hax_lib]::refine` | ||
| pub fn expects_refine(path: &Path) -> Result<Option<String>> { | ||
| expects_hax_path(&["refine"], path) | ||
| } | ||
|
|
||
| /// Expects a `Path` to be a hax path: `::hax_lib::<KW>`, | ||
| /// `hax_lib::<KW>` or `<KW>` in (with `KW` in `allowlist`). | ||
| pub fn expects_hax_path(allowlist: &[&str], path: &Path) -> Result<Option<String>> { | ||
| let path_span = path.span(); | ||
| let path = expect_simple_path(path) | ||
| .ok_or_else(|| Error::new(path_span, "Expected a simple path, with no `<...>`."))?; | ||
| Ok( | ||
| match path | ||
| .iter() | ||
| .map(|x| x.as_str()) | ||
| .collect::<Vec<_>>() | ||
| .as_slice() | ||
| { | ||
| [kw] | ["", "hax_lib", kw] | ["hax_lib", kw] if allowlist.contains(kw) => { | ||
| Some(kw.to_string()) | ||
| } | ||
| _ => None, | ||
| }, | ||
| ) | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.