diff --git a/book/.gitignore b/book/.gitignore index 3006b271da..5311c2a064 100644 --- a/book/.gitignore +++ b/book/.gitignore @@ -1 +1 @@ -book/ +./book/ diff --git a/book/src/dev/develop.md b/book/src/dev/develop.md index 22d74c2edc..fdd88cbcd5 100644 --- a/book/src/dev/develop.md +++ b/book/src/dev/develop.md @@ -82,12 +82,12 @@ You can also pass `-Ztrack-diagnostics=y` to enable it if you are not using `car ## Running outside the project -To run Flux in a package outside the flux respo you need to install the binaries globally. You can +To run Flux in a package outside the flux repo you need to install the binaries globally. You can do that using `cargo xtask install`. If you are continuously testing new changes it could be annoying to do it each time. To deal with this, you can set the `FLUX_SYSROOT` environment variable to change the location where `cargo-flux` and `rustc-flux` load the `flux-driver`. You can set it globally to point to the `target/debug` directory inside your local copy of the repo. This way you won't have to run -`cargo xtask install` after every change and you can be sure you'll be using the latest local debug +`cargo xtask install` after every change, and you can be sure you'll be using the latest local debug build. Just be aware that the `rustc-flux` and `cargo-flux` binaries are built for a specific toolchain, and you will get a dynamic linking error if the `flux-driver` was compiled with a different one. This is to say, you should at least run `cargo xtask install` every time after the toolchain is updated. diff --git a/book/src/guide/install.md b/book/src/guide/install.md index 41b90ba69d..3c2af15290 100644 --- a/book/src/guide/install.md +++ b/book/src/guide/install.md @@ -29,6 +29,6 @@ Next, run the following to build and install `flux` binaries cargo xtask install ``` -This will the binaries `rustc-flux` and `cargo-flux` in your cargo home. These two binaries should be used +This will install two binaries `rustc-flux` and `cargo-flux` in your cargo home. These two binaries should be used respectively to run flux on either a single file or on a project using cargo. The installation process will also copy some files to `$HOME/.flux`. diff --git a/book/src/guide/run.md b/book/src/guide/run.md index e7d7340b82..e61bc0d2b1 100644 --- a/book/src/guide/run.md +++ b/book/src/guide/run.md @@ -38,9 +38,6 @@ to register the `flux` tool in order to add refinement annotations to functions. ```rust -#![feature(register_tool)] -#![register_tool(flux)] - #[flux::sig(fn(x: i32) -> i32{v: x < v})] pub fn inc(x: i32) -> i32 { x - 1 @@ -57,9 +54,9 @@ you should see in your output ```text error[FLUX]: postcondition might not hold - --> test0.rs:6:5 + --> test0.rs:3:5 | -6 | x - 1 +3 | x - 1 | ^^^^^ ``` @@ -99,18 +96,6 @@ Add this to the workspace settings i.e. `.vscode/settings.json` } ``` -If you want to change the `flux-driver` used by `cargo-flux`, then also specify the -`FLUX_PATH` like in the example below, which uses the version generated when you -run `cargo build`. - -``` json -{ - "rust-analyzer.check.extraEnv": { - "FLUX_DRIVER_PATH": "/path/to/flux-repo/target/debug/flux-driver", - } -} -``` - **Note:** Make sure to edit the paths in the above snippet to point to the correct locations on your machine. ## Configuration @@ -121,10 +106,10 @@ You can set various `env` variables to customize the behavior of `flux`. * `FLUX_CONFIG` tells `flux` where to find a config file for these settings. * By default, `flux` searches its directory for a `flux.toml` or `.flux.toml`. -* `FLUX_DRIVER_PATH=path/to/flux-driver` tells `cargo-flux` and `rustc-flux` where to find the `flux` binary. - * Defaults to the default `flux-driver` installation (typically found in `~/.cargo/bin`). -* `FLUX_LOG_DIR=path/to/log/` with default `./log/` -* `FLUX_DUMP_CONSTRAINT=1` sets the directory where constraints, timing and cache are saved. +* `FLUX_SYSROOT` tells `cargo-flux` and `rustc-flux` where to find the `flux-driver` binary. + * Defaults to the default installation location in `~/.flux`. +* `FLUX_LOG_DIR=path/to/log/` sets the directory where constraints, timing and cache are saved. Defaults to `./log/`. +* `FLUX_DUMP_CONSTRAINT=1` tell `flux` to dump constraints generated for each function. * `FLUX_DUMP_CHECKER_TRACE=1` saves the checker's trace (useful for debugging!) * `FLUX_DUMP_TIMINGS=1` saves the profile information * `FLUX_DUMP_MIR=1` saves the low-level MIR for each analyzed function @@ -166,12 +151,12 @@ was overridden by setting the environment variable `FLUX_DUMP_MIR=0`. ### Crate Config Some flags can be configured on a per-crate basis using the custom inner attribute `#![flux::cfg]`. -This can only be used in nightly and requires enabling the feature `custom_inner_attributes` +This annotation relies on the unstable custom inner attributes feature. To be able to use with a +non-nightly compiler you have to put it under a `cfg_attr`. For example, to enable overflow checking: ```rust -#![feature(custom_inner_attributes)] -#![flux:cfg(check_overflow = true)] +#![cfg_attr(flux, flux::cfg(check_overflow = true))] ``` The only flag supported now is overflow checking. diff --git a/crates/flux-bin/src/bin/rustc-flux.rs b/crates/flux-bin/src/bin/rustc-flux.rs index 7c1aeefc55..f0f0663b99 100644 --- a/crates/flux-bin/src/bin/rustc-flux.rs +++ b/crates/flux-bin/src/bin/rustc-flux.rs @@ -29,8 +29,6 @@ fn run() -> Result { let exit_code = Command::new(flux_driver_path) // Skip the invocation of rustc-flux itself .args(env::args().skip(1)) - .arg("-Zcrate-attr=feature(register_tool,custom_inner_attributes)") - .arg("-Zcrate-attr=register_tool(flux)") .arg("-L") .arg(sysroot_dir()) .arg("--extern") diff --git a/crates/flux-driver/src/bin/main.rs b/crates/flux-driver/src/bin/main.rs index 902559e07f..df31458a8b 100644 --- a/crates/flux-driver/src/bin/main.rs +++ b/crates/flux-driver/src/bin/main.rs @@ -2,7 +2,7 @@ extern crate rustc_driver; -use std::{env, io, process::exit}; +use std::{env, io, ops::Deref, process::exit}; use flux_driver::callbacks::FluxCallbacks; use rustc_driver::{catch_with_exit_code, RunCompiler}; @@ -14,6 +14,18 @@ fn main() -> io::Result<()> { // CODESYNC(flux-cargo) Check if we are being called from cargo. let in_cargo = env::var("FLUX_CARGO").is_ok(); + let primary_package = env::var("CARGO_PRIMARY_PACKAGE").is_ok(); + + // TODO(nilehmann): we should also run flux on dependencies with flux annotations to produce metadata. + // The idea is to opt in to that in the metadata table of the Cargo.toml. Something like + // ``` + // [package.metadata.flux] + // export = true + // ``` + // If we are being called from cargo but this is not the primary package, then we just call rustc. + if in_cargo && !primary_package { + rustc_driver::main(); + } // HACK(nilehmann) // Disable incremental compilation because that makes the borrow checker to not run @@ -33,12 +45,16 @@ fn main() -> io::Result<()> { args.push(arg); } } - // Add the sysroot path to the arguments. + args.push("--sysroot".into()); args.push(sysroot().expect("Flux Rust requires rustup to be built.")); args.push("-Coverflow-checks=off".to_string()); + args.push("-Zcrate-attr=feature(register_tool, custom_inner_attributes)".to_string()); + args.push("-Zcrate-attr=register_tool(flux)".to_string()); + args.push("-Zcrate-attr=register_tool(flux_tool)".to_string()); + args.push("--cfg=flux".to_string()); - let exit_code = run_compiler(args, in_cargo); + let exit_code = catch_with_exit_code(move || RunCompiler::new(&args, &mut FluxCallbacks).run()); resolve_logs()?; exit(exit_code) } @@ -51,11 +67,24 @@ fn sysroot() -> Option { Some(format!("{home}/toolchains/{toolchain}")) } -/// Run Flux Rust and return the exit status code. -pub fn run_compiler(args: Vec, in_cargo: bool) -> i32 { - // HACK(nilehmann) When running flux we want to stop compilation after analysis - // to avoid creating a binary. However, stopping compilation messes up with cargo so we - // pass full_compilation=true if we detect we are being called from cargo - let mut callbacks = FluxCallbacks::new(in_cargo); - catch_with_exit_code(move || RunCompiler::new(&args, &mut callbacks).run()) +/// If a command-line option matches `find_arg`, then apply the predicate `pred` on its value. If +/// true, then return it. The parameter is assumed to be either `--arg=value` or `--arg value`. +pub fn arg_value<'a, T: Deref>( + args: &'a [T], + find_arg: &str, + pred: impl Fn(&str) -> bool, +) -> Option<&'a str> { + let mut args = args.iter().map(Deref::deref); + while let Some(arg) = args.next() { + let mut arg = arg.splitn(2, '='); + if arg.next() != Some(find_arg) { + continue; + } + + match arg.next().or_else(|| args.next()) { + Some(v) if pred(v) => return Some(v), + _ => {} + } + } + None } diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs index c90405f6bb..474bb74ce1 100644 --- a/crates/flux-driver/src/callbacks.rs +++ b/crates/flux-driver/src/callbacks.rs @@ -24,15 +24,8 @@ use crate::{ DEFAULT_LOCALE_RESOURCES, }; -pub struct FluxCallbacks { - full_compilation: bool, -} - -impl FluxCallbacks { - pub fn new(full_compilation: bool) -> Self { - FluxCallbacks { full_compilation } - } -} +#[derive(Default)] +pub struct FluxCallbacks; impl Callbacks for FluxCallbacks { fn config(&mut self, config: &mut rustc_interface::interface::Config) { @@ -70,11 +63,7 @@ impl Callbacks for FluxCallbacks { sess.finish_diagnostics(); }); - if self.full_compilation { - Compilation::Continue - } else { - Compilation::Stop - } + Compilation::Stop } } diff --git a/crates/flux-driver/src/collector.rs b/crates/flux-driver/src/collector.rs index fa81064adb..14b12d3ad0 100644 --- a/crates/flux-driver/src/collector.rs +++ b/crates/flux-driver/src/collector.rs @@ -249,7 +249,7 @@ impl<'tcx, 'a> SpecCollector<'tcx, 'a> { self.specs.structs.insert( owner_id, - surface::StructDef { refined_by, generics, fields, opaque, invariants }, + surface::StructDef { generics, refined_by, fields, opaque, invariants }, ); Ok(()) @@ -347,7 +347,14 @@ impl<'tcx, 'a> SpecCollector<'tcx, 'a> { .filter_map(|attr| { if let AttrKind::Normal(attr_item, ..) = &attr.kind { match &attr_item.item.path.segments[..] { - [first, ..] if first.ident.as_str() == "flux" => Some(attr_item), + [first, ..] => { + let ident = first.ident.as_str(); + if ident == "flux" || ident == "flux_tool" { + Some(attr_item) + } else { + None + } + } _ => None, } } else { diff --git a/lib/flux-attrs/src/ast.rs b/lib/flux-attrs/src/ast.rs index 9c8a2f64bf..35a69d52fa 100644 --- a/lib/flux-attrs/src/ast.rs +++ b/lib/flux-attrs/src/ast.rs @@ -809,7 +809,7 @@ impl ToTokens for ItemFn { #[cfg(flux_sysroot)] { let flux_sig = ToTokensFlux(sig); - quote!(#[flux::sig(#flux_sig)]).to_tokens(tokens); + quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens); } let rust_sig = ToTokensRust(sig); quote! { @@ -825,7 +825,7 @@ impl ToTokens for ItemType { let flux_type = ToTokensFlux(self); let rust_type = ToTokensRust(self); quote! { - #[flux::alias(#flux_type)] + #[flux_tool::alias(#flux_type)] #rust_type } .to_tokens(tokens); @@ -907,7 +907,7 @@ impl ToTokens for ImplItemFn { #[cfg(flux_sysroot)] { let flux_sig = ToTokensFlux(sig); - quote!(#[flux::sig(#flux_sig)]).to_tokens(tokens); + quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens); } let rust_sig = ToTokensRust(sig); quote! { diff --git a/lib/flux-attrs/src/extern_spec.rs b/lib/flux-attrs/src/extern_spec.rs new file mode 100644 index 0000000000..1ccca5eaec --- /dev/null +++ b/lib/flux-attrs/src/extern_spec.rs @@ -0,0 +1,334 @@ +use std::mem; + +use proc_macro2::TokenStream; +use quote::{format_ident, quote, quote_spanned, ToTokens, TokenStreamExt}; +use syn::{ + braced, + parse::{Parse, ParseStream}, + parse_quote_spanned, + punctuated::Punctuated, + spanned::Spanned, + token::Brace, + Attribute, Expr, FnArg, GenericArgument, GenericParam, Generics, ItemStruct, Signature, Token, + Type, +}; + +enum ExternItem { + Struct(syn::ItemStruct), + Fn(ExternFn), + Impl(ExternItemImpl), +} + +struct ExternFn { + attrs: Vec, + sig: Signature, + block: Option, +} + +struct ExternItemImpl { + impl_token: Token![impl], + generics: Generics, + self_ty: Box, + brace_token: Brace, + items: Vec, + mod_path: Option, + dummy_ident: Option, +} + +impl ExternItem { + fn replace_attrs(&mut self, new: Vec) -> Vec { + match self { + ExternItem::Struct(ItemStruct { attrs, .. }) + | ExternItem::Fn(ExternFn { attrs, .. }) => mem::replace(attrs, new), + ExternItem::Impl(ExternItemImpl { .. }) => vec![], + } + } +} + +impl ExternItemImpl { + fn prepare(&mut self, mod_path: Option) -> syn::Result<()> { + self.mod_path = mod_path; + self.dummy_ident = + Some(create_dummy_ident(&mut "__FluxExternImplStruct".to_string(), &self.self_ty)?); + for item in &mut self.items { + item.prepare(&self.mod_path, Some(&self.self_ty), false); + } + Ok(()) + } + + fn dummy_struct(&self) -> syn::ItemStruct { + let self_ty = &self.self_ty; + let struct_field: syn::FieldsUnnamed = if let Some(mod_path) = &self.mod_path { + parse_quote_spanned!(self_ty.span()=> ( #mod_path :: #self_ty ) ) + } else { + parse_quote_spanned!(self_ty.span()=> ( #self_ty ) ) + }; + + syn::ItemStruct { + attrs: vec![], + vis: syn::Visibility::Inherited, + struct_token: syn::token::Struct { span: self.impl_token.span }, + ident: self.dummy_ident.as_ref().unwrap().clone(), + generics: self.generics.clone(), + fields: syn::Fields::Unnamed(struct_field), + semi_token: Some(syn::token::Semi { spans: [self.impl_token.span] }), + } + } +} + +impl ToTokens for ExternItemImpl { + fn to_tokens(&self, tokens: &mut TokenStream) { + let dummy_struct = self.dummy_struct(); + dummy_struct.to_tokens(tokens); + let (impl_generics, ty_generics, where_clause) = self.generics.split_for_impl(); + self.impl_token.to_tokens(tokens); + impl_generics.to_tokens(tokens); + let dummy_ident = self.dummy_ident.as_ref().unwrap(); + quote!(#dummy_ident #ty_generics).to_tokens(tokens); + where_clause.to_tokens(tokens); + self.brace_token.surround(tokens, |tokens| { + for item in &self.items { + item.to_tokens(tokens); + } + }); + } +} + +impl ExternFn { + fn prepare(&mut self, mod_path: &Option, self_ty: Option<&syn::Type>, mangle: bool) { + self.fill_body(mod_path, self_ty); + if mangle { + self.sig.ident = format_ident!("__flux_extern_spec_{}", self.sig.ident); + } + } + + fn fill_body(&mut self, mod_path: &Option, self_ty: Option<&syn::Type>) { + let ident = &self.sig.ident; + let fn_path = match (mod_path, self_ty) { + (None, None) => quote_spanned! { ident.span() => #ident }, + (Some(mod_path), None) => quote_spanned!(ident.span()=> #mod_path :: #ident ), + (None, Some(self_ty)) => quote_spanned!(ident.span()=> < #self_ty > :: #ident ), + (Some(mod_path), Some(self_ty)) => { + quote_spanned!(ident.span()=> < #mod_path :: #self_ty > :: #ident ) + } + }; + let generic_args = generic_params_to_args(&self.sig.generics.params); + let args = params_to_args(&self.sig.inputs); + self.block = Some(quote!( { #fn_path :: <#generic_args> ( #args ) } )); + } +} + +impl ToTokens for ExternFn { + fn to_tokens(&self, tokens: &mut TokenStream) { + debug_assert!(self.block.is_some()); + quote!(#[flux::extern_spec]).to_tokens(tokens); + tokens.append_all(&self.attrs); + self.sig.to_tokens(tokens); + self.block.to_tokens(tokens); + } +} + +impl Parse for ExternItem { + fn parse(input: ParseStream) -> syn::Result { + let attrs = input.call(Attribute::parse_outer)?; + let lookahead = input.lookahead1(); + let mut item = if lookahead.peek(Token![fn]) { + ExternItem::Fn(input.parse()?) + } else if lookahead.peek(Token![impl]) { + ExternItem::Impl(input.parse()?) + } else if lookahead.peek(Token![struct]) { + ExternItem::Struct(input.parse()?) + } else { + return Err(lookahead.error()); + }; + item.replace_attrs(attrs); + Ok(item) + } +} + +impl Parse for ExternFn { + fn parse(input: ParseStream) -> syn::Result { + let attrs = input.call(Attribute::parse_outer)?; + let sig = input.parse()?; + input.parse::()?; + Ok(ExternFn { attrs, sig, block: None }) + } +} + +impl Parse for ExternItemImpl { + fn parse(input: ParseStream) -> syn::Result { + let impl_token = input.parse()?; + let generics = input.parse()?; + let self_ty = input.parse()?; + let content; + let brace_token = braced!(content in input); + let mut items = Vec::new(); + while !content.is_empty() { + items.push(content.parse()?); + } + + Ok(ExternItemImpl { + impl_token, + generics, + self_ty, + brace_token, + items, + mod_path: None, + dummy_ident: None, + }) + } +} + +pub(crate) fn transform_extern_spec( + attr: TokenStream, + tokens: TokenStream, +) -> syn::Result { + let mod_path: Option = + if !attr.is_empty() { Some(syn::parse2(attr)?) } else { None }; + match syn::parse2::(tokens)? { + ExternItem::Struct(item_struct) => create_dummy_struct(mod_path, item_struct), + ExternItem::Fn(mut extern_fn) => { + extern_fn.prepare(&mod_path, None, true); + Ok(extern_fn.into_token_stream()) + } + ExternItem::Impl(mut extern_item_impl) => { + extern_item_impl.prepare(mod_path)?; + Ok(extern_item_impl.into_token_stream()) + } + } +} + +fn create_dummy_ident(dummy_prefix: &mut String, ty: &syn::Type) -> syn::Result { + use syn::Type::*; + match ty { + Reference(ty_ref) => { + if ty_ref.mutability.is_some() { + dummy_prefix.push_str("Mut"); + }; + dummy_prefix.push_str("Ref"); + create_dummy_ident(dummy_prefix, ty_ref.elem.as_ref()) + } + Slice(ty_slice) => { + dummy_prefix.push_str("Slice"); + create_dummy_ident(dummy_prefix, ty_slice.elem.as_ref()) + } + Path(ty_path) => create_dummy_ident_from_path(dummy_prefix, &ty_path.path), + _ => { + Err(syn::Error::new( + ty.span(), + format!("invalid extern_spec: unsupported type {:?}", ty), + )) + } + } +} + +fn create_dummy_ident_from_path(dummy_prefix: &str, path: &syn::Path) -> syn::Result { + // For paths, we mangle the last identifier + if let Some(path_segment) = path.segments.last() { + // Mangle the identifier using the dummy_prefix + let ident = syn::Ident::new( + &format!("{}{}", dummy_prefix, path_segment.ident), + path_segment.ident.span(), + ); + Ok(ident) + } else { + Err(syn::Error::new(path.span(), format!("invalid extern_spec: empty Path {:?}", path))) + } +} + +/// Create a dummy struct with a single unnamed field that is the external struct. +/// +/// Example: +/// +/// ```ignore +/// #[extern_spec(std::vec)] +/// #[flux::refined_by(n: int)] +/// struct Vec; +/// +/// => +/// +/// #[flux::extern_spec] +/// #[allow(unused, dead_code)] +/// #[flux::refined_by(n: int)] +/// struct FluxExternStructVec(std::vec::Vec); +/// ``` +fn create_dummy_struct( + mod_path: Option, + item_struct: syn::ItemStruct, +) -> syn::Result { + let item_struct_span = item_struct.span(); + let fields_span = item_struct.fields.span(); + let syn::Fields::Unit = item_struct.fields else { + return Err(syn::Error::new( + fields_span, + "invalid extern spec: extern specs on structs cannot have fields, i.e. they must look like struct Vec;", + )); + }; + let mut dummy_struct = item_struct.clone(); + let ident = item_struct.ident; + let generics = item_struct.generics; + dummy_struct.ident = format_ident!("__FluxExternStruct{}", ident); + dummy_struct.semi_token = None; + let dummy_field: syn::FieldsUnnamed = if let Some(mod_path) = mod_path { + parse_quote_spanned! {item_struct_span => + ( #mod_path :: #ident #generics ) + } + } else { + parse_quote_spanned! {item_struct_span => + ( #ident #generics ) + } + }; + dummy_struct.fields = syn::Fields::Unnamed(dummy_field); + let dummy_struct_with_attrs: syn::ItemStruct = parse_quote_spanned! { item_struct_span => + #[flux::extern_spec] + #[allow(unused, dead_code)] + #dummy_struct + }; + Ok(dummy_struct_with_attrs.to_token_stream()) +} + +// Cribbed from Prusti's extern_spec_rewriter +fn generic_params_to_args( + generic_params: &Punctuated, +) -> Punctuated { + generic_params + .iter() + .flat_map(|param| -> Option { + let span = param.span(); + match param { + GenericParam::Type(syn::TypeParam { ident, .. }) => { + Some(parse_quote_spanned! { span => #ident }) + } + GenericParam::Lifetime(_) => None, + GenericParam::Const(syn::ConstParam { ident, .. }) => { + Some(parse_quote_spanned! {span => #ident }) + } + } + }) + .collect() +} + +// Cribbed from Prusti's extern_spec_rewriter +fn params_to_args(params: &Punctuated) -> Punctuated { + params + .iter() + .map(|param| -> Expr { + let span = param.span(); + match param { + FnArg::Typed(pat_type) => { + match pat_type.pat.as_ref() { + syn::Pat::Ident(ident) => { + parse_quote_spanned! {span => #ident } + } + _ => { + unimplemented!( + "extern specs don't support patterns other than simple identifiers" + ) + } + } + } + FnArg::Receiver(_) => parse_quote_spanned! {span => self}, + } + }) + .collect() +} diff --git a/lib/flux-attrs/src/lib.rs b/lib/flux-attrs/src/lib.rs index 335e145988..187c97d0fe 100644 --- a/lib/flux-attrs/src/lib.rs +++ b/lib/flux-attrs/src/lib.rs @@ -1,341 +1,116 @@ mod ast; +mod extern_spec; -use std::mem; - -use proc_macro2::TokenStream; -use quote::{format_ident, quote, quote_spanned, ToTokens, TokenStreamExt}; -use syn::{ - braced, - parse::{Parse, ParseStream}, - parse_quote_spanned, - punctuated::Punctuated, - spanned::Spanned, - token::Brace, - Attribute, Expr, FnArg, GenericArgument, GenericParam, Generics, ItemStruct, Signature, Token, - Type, -}; +use proc_macro2::{Ident, TokenStream, TokenTree}; +use quote::{quote, quote_spanned, ToTokens}; +use syn::{parse_quote_spanned, spanned::Spanned, Attribute, ItemEnum, ItemStruct}; pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream { - transform_extern_spec(attr, tokens).unwrap_or_else(|err| err.to_compile_error()) -} - -pub fn flux(tokens: TokenStream) -> TokenStream { - syn::parse2::(tokens) - .map_or_else(|err| err.to_compile_error(), ToTokens::into_token_stream) -} -enum ExternItem { - Struct(syn::ItemStruct), - Fn(ExternFn), - Impl(ExternItemImpl), -} - -struct ExternFn { - attrs: Vec, - sig: Signature, - block: Option, -} - -struct ExternItemImpl { - impl_token: Token![impl], - generics: Generics, - self_ty: Box, - brace_token: Brace, - items: Vec, - mod_path: Option, - dummy_ident: Option, -} - -impl ExternItem { - fn replace_attrs(&mut self, new: Vec) -> Vec { - match self { - ExternItem::Struct(ItemStruct { attrs, .. }) - | ExternItem::Fn(ExternFn { attrs, .. }) => mem::replace(attrs, new), - ExternItem::Impl(ExternItemImpl { .. }) => vec![], - } - } -} - -impl ExternItemImpl { - fn prepare(&mut self, mod_path: Option) -> syn::Result<()> { - self.mod_path = mod_path; - self.dummy_ident = - Some(create_dummy_ident(&mut "__FluxExternImplStruct".to_string(), &self.self_ty)?); - for item in &mut self.items { - item.prepare(&self.mod_path, Some(&self.self_ty), false); + extern_spec::transform_extern_spec(attr, tokens).unwrap_or_else(|err| err.to_compile_error()) +} + +pub fn flux_tool_item_attr(name: &str, attr: TokenStream, item: TokenStream) -> TokenStream { + // I don't really know what I'm doing here, but spanning the quote with the item's span seems + // to behave correctly. + let span = item.span(); + let name = TokenTree::Ident(Ident::new(name, span)); + if attr.is_empty() { + quote_spanned! {span=> + #[flux_tool::#name] + #item } - Ok(()) - } - - fn dummy_struct(&self) -> syn::ItemStruct { - let self_ty = &self.self_ty; - let struct_field: syn::FieldsUnnamed = if let Some(mod_path) = &self.mod_path { - parse_quote_spanned!(self_ty.span()=> ( #mod_path :: #self_ty ) ) - } else { - parse_quote_spanned!(self_ty.span()=> ( #self_ty ) ) - }; - - syn::ItemStruct { - attrs: vec![], - vis: syn::Visibility::Inherited, - struct_token: syn::token::Struct { span: self.impl_token.span }, - ident: self.dummy_ident.as_ref().unwrap().clone(), - generics: self.generics.clone(), - fields: syn::Fields::Unnamed(struct_field), - semi_token: Some(syn::token::Semi { spans: [self.impl_token.span] }), + } else { + quote_spanned! {span=> + #[flux_tool::#name(#attr)] + #item } } } -impl ToTokens for ExternItemImpl { - fn to_tokens(&self, tokens: &mut TokenStream) { - let dummy_struct = self.dummy_struct(); - dummy_struct.to_tokens(tokens); - let (impl_generics, ty_generics, where_clause) = self.generics.split_for_impl(); - self.impl_token.to_tokens(tokens); - impl_generics.to_tokens(tokens); - let dummy_ident = self.dummy_ident.as_ref().unwrap(); - quote!(#dummy_ident #ty_generics).to_tokens(tokens); - where_clause.to_tokens(tokens); - self.brace_token.surround(tokens, |tokens| { - for item in &self.items { - item.to_tokens(tokens); - } - }); - } -} +pub fn refined_by(attr: TokenStream, item: TokenStream) -> TokenStream { + let span = item.span(); + let mut item = match syn::parse2::(item) { + Ok(item) => item, + Err(err) => return err.to_compile_error(), + }; -impl ExternFn { - fn prepare(&mut self, mod_path: &Option, self_ty: Option<&syn::Type>, mangle: bool) { - self.fill_body(mod_path, self_ty); - if mangle { - self.sig.ident = format_ident!("__flux_extern_spec_{}", self.sig.ident); + match &mut item { + syn::Item::Enum(item_enum) => { + if let Err(err) = refined_by_enum(item_enum) { + return err.into_compile_error(); + } } - } - - fn fill_body(&mut self, mod_path: &Option, self_ty: Option<&syn::Type>) { - let ident = &self.sig.ident; - let fn_path = match (mod_path, self_ty) { - (None, None) => quote_spanned! { ident.span() => #ident }, - (Some(mod_path), None) => quote_spanned!(ident.span()=> #mod_path :: #ident ), - (None, Some(self_ty)) => quote_spanned!(ident.span()=> < #self_ty > :: #ident ), - (Some(mod_path), Some(self_ty)) => { - quote_spanned!(ident.span()=> < #mod_path :: #self_ty > :: #ident ) + syn::Item::Struct(item_struct) => { + if let Err(err) = refined_by_struct(item_struct) { + return err.into_compile_error(); } - }; - let generic_args = generic_params_to_args(&self.sig.generics.params); - let args = params_to_args(&self.sig.inputs); - self.block = Some(quote!( { #fn_path :: <#generic_args> ( #args ) } )); + } + _ => return syn::Error::new(span, "expected struct or enum").to_compile_error(), } -} -impl ToTokens for ExternFn { - fn to_tokens(&self, tokens: &mut TokenStream) { - debug_assert!(self.block.is_some()); - quote!(#[flux::extern_spec]).to_tokens(tokens); - tokens.append_all(&self.attrs); - self.sig.to_tokens(tokens); - self.block.to_tokens(tokens); + if cfg!(flux_sysroot) { + quote_spanned! {span=> + #[flux_tool::refined_by(#attr)] + #item + } + } else { + item.to_token_stream() } } -impl Parse for ExternItem { - fn parse(input: ParseStream) -> syn::Result { - let attrs = input.call(Attribute::parse_outer)?; - let lookahead = input.lookahead1(); - let mut item = if lookahead.peek(Token![fn]) { - ExternItem::Fn(input.parse()?) - } else if lookahead.peek(Token![impl]) { - ExternItem::Impl(input.parse()?) - } else if lookahead.peek(Token![struct]) { - ExternItem::Struct(input.parse()?) - } else { - return Err(lookahead.error()); - }; - item.replace_attrs(attrs); - Ok(item) +fn refined_by_enum(item_enum: &mut ItemEnum) -> syn::Result<()> { + for variant in &mut item_enum.variants { + flux_tool_attrs(&mut variant.attrs, "variant")?; } + Ok(()) } -impl Parse for ExternFn { - fn parse(input: ParseStream) -> syn::Result { - let attrs = input.call(Attribute::parse_outer)?; - let sig = input.parse()?; - input.parse::()?; - Ok(ExternFn { attrs, sig, block: None }) +fn refined_by_struct(item_struct: &mut ItemStruct) -> syn::Result<()> { + for field in &mut item_struct.fields { + flux_tool_attrs(&mut field.attrs, "field")?; } + Ok(()) } -impl Parse for ExternItemImpl { - fn parse(input: ParseStream) -> syn::Result { - let impl_token = input.parse()?; - let generics = input.parse()?; - let self_ty = input.parse()?; - let content; - let brace_token = braced!(content in input); - let mut items = Vec::new(); - while !content.is_empty() { - items.push(content.parse()?); +fn flux_tool_attrs(attrs: &mut Vec, name: &str) -> syn::Result<()> { + let mut j = 0; + for i in 0..attrs.len() { + if cfg!(flux_sysroot) { + if attrs[i].meta.path().is_ident(name) { + attrs[i] = flux_tool_attr(&attrs[i])?; + attrs.swap(i, j); + j += 1; + } + } else if !attrs[i].meta.path().is_ident(name) { + attrs.swap(i, j); + j += 1; } - - Ok(ExternItemImpl { - impl_token, - generics, - self_ty, - brace_token, - items, - mod_path: None, - dummy_ident: None, - }) } -} - -fn transform_extern_spec(attr: TokenStream, tokens: TokenStream) -> syn::Result { - let mod_path: Option = - if !attr.is_empty() { Some(syn::parse2(attr)?) } else { None }; - match syn::parse2::(tokens)? { - ExternItem::Struct(item_struct) => create_dummy_struct(mod_path, item_struct), - ExternItem::Fn(mut extern_fn) => { - extern_fn.prepare(&mod_path, None, true); - Ok(extern_fn.into_token_stream()) - } - ExternItem::Impl(mut extern_item_impl) => { - extern_item_impl.prepare(mod_path)?; - Ok(extern_item_impl.into_token_stream()) - } + if !cfg!(flux_sysroot) { + attrs.truncate(j); } + Ok(()) } -fn create_dummy_ident(dummy_prefix: &mut String, ty: &syn::Type) -> syn::Result { - use syn::Type::*; - match ty { - Reference(ty_ref) => { - if ty_ref.mutability.is_some() { - dummy_prefix.push_str("Mut"); - }; - dummy_prefix.push_str("Ref"); - create_dummy_ident(dummy_prefix, ty_ref.elem.as_ref()) - } - Slice(ty_slice) => { - dummy_prefix.push_str("Slice"); - create_dummy_ident(dummy_prefix, ty_slice.elem.as_ref()) - } - Path(ty_path) => create_dummy_ident_from_path(dummy_prefix, &ty_path.path), - _ => { - Err(syn::Error::new( - ty.span(), - format!("invalid extern_spec: unsupported type {:?}", ty), - )) - } - } +fn flux_tool_attr(attr: &Attribute) -> syn::Result { + let metalist = &attr.meta.require_list()?; + let tokens = &metalist.tokens; + let path = &metalist.path; + let span = attr.span(); + Ok(parse_quote_spanned!(span=>#[flux_tool::#path(#tokens)])) } -fn create_dummy_ident_from_path(dummy_prefix: &str, path: &syn::Path) -> syn::Result { - // For paths, we mangle the last identifier - if let Some(path_segment) = path.segments.last() { - // Mangle the identifier using the dummy_prefix - let ident = syn::Ident::new( - &format!("{}{}", dummy_prefix, path_segment.ident), - path_segment.ident.span(), - ); - Ok(ident) - } else { - Err(syn::Error::new(path.span(), format!("invalid extern_spec: empty Path {:?}", path))) - } +pub fn flux(tokens: TokenStream) -> TokenStream { + syn::parse2::(tokens) + .map_or_else(|err| err.to_compile_error(), ToTokens::into_token_stream) } -/// Create a dummy struct with a single unnamed field that is the external struct. -/// -/// Example: -/// -/// ```ignore -/// #[extern_spec(std::vec)] -/// #[flux::refined_by(n: int)] -/// struct Vec; -/// -/// => -/// -/// #[flux::extern_spec] -/// #[allow(unused, dead_code)] -/// #[flux::refined_by(n: int)] -/// struct FluxExternStructVec(std::vec::Vec); -/// ``` -fn create_dummy_struct( - mod_path: Option, - item_struct: syn::ItemStruct, -) -> syn::Result { - let item_struct_span = item_struct.span(); - let fields_span = item_struct.fields.span(); - let syn::Fields::Unit = item_struct.fields else { - return Err(syn::Error::new( - fields_span, - "invalid extern spec: extern specs on structs cannot have fields, i.e. they must look like struct Vec;", - )); - }; - let mut dummy_struct = item_struct.clone(); - let ident = item_struct.ident; - let generics = item_struct.generics; - dummy_struct.ident = format_ident!("__FluxExternStruct{}", ident); - dummy_struct.semi_token = None; - let dummy_field: syn::FieldsUnnamed = if let Some(mod_path) = mod_path { - parse_quote_spanned! {item_struct_span => - ( #mod_path :: #ident #generics ) +pub fn defs(tokens: TokenStream) -> TokenStream { + quote! { + mod flux_defs { + #![flux::defs { + #tokens + }] } - } else { - parse_quote_spanned! {item_struct_span => - ( #ident #generics ) - } - }; - dummy_struct.fields = syn::Fields::Unnamed(dummy_field); - let dummy_struct_with_attrs: syn::ItemStruct = parse_quote_spanned! { item_struct_span => - #[flux::extern_spec] - #[allow(unused, dead_code)] - #dummy_struct - }; - Ok(dummy_struct_with_attrs.to_token_stream()) -} - -// Cribbed from Prusti's extern_spec_rewriter -fn generic_params_to_args( - generic_params: &Punctuated, -) -> Punctuated { - generic_params - .iter() - .flat_map(|param| -> Option { - let span = param.span(); - match param { - GenericParam::Type(syn::TypeParam { ident, .. }) => { - Some(parse_quote_spanned! { span => #ident }) - } - GenericParam::Lifetime(_) => None, - GenericParam::Const(syn::ConstParam { ident, .. }) => { - Some(parse_quote_spanned! {span => #ident }) - } - } - }) - .collect() -} - -// Cribbed from Prusti's extern_spec_rewriter -fn params_to_args(params: &Punctuated) -> Punctuated { - params - .iter() - .map(|param| -> Expr { - let span = param.span(); - match param { - FnArg::Typed(pat_type) => { - match pat_type.pat.as_ref() { - syn::Pat::Ident(ident) => { - parse_quote_spanned! {span => #ident } - } - _ => { - unimplemented!( - "extern specs don't support patterns other than simple identifiers" - ) - } - } - } - FnArg::Receiver(_) => parse_quote_spanned! {span => self}, - } - }) - .collect() + } } diff --git a/lib/flux-rs/src/lib.rs b/lib/flux-rs/src/lib.rs index 9b980b0127..bc8ace0746 100644 --- a/lib/flux-rs/src/lib.rs +++ b/lib/flux-rs/src/lib.rs @@ -1,19 +1,114 @@ -// When running without flux, all macros are pass-through +#[cfg(not(flux_sysroot))] +use attr_dummy as attr_impl; +#[cfg(flux_sysroot)] +use attr_sysroot as attr_impl; use proc_macro::TokenStream; -#[cfg(not(flux_sysroot))] #[proc_macro_attribute] -pub fn extern_spec(_attrs: TokenStream, _tokens: TokenStream) -> TokenStream { - TokenStream::new() +pub fn alias(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::alias(attr, tokens) } -#[cfg(flux_sysroot)] #[proc_macro_attribute] -pub fn extern_spec(attrs: TokenStream, tokens: TokenStream) -> TokenStream { - flux_attrs::extern_spec(attrs.into(), tokens.into()).into() +pub fn sig(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::sig(attr, tokens) +} + +#[proc_macro_attribute] +pub fn qualifiers(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::qualifiers(attr, tokens) +} + +#[proc_macro_attribute] +pub fn refined_by(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::refined_by(attr, tokens) +} + +#[proc_macro_attribute] +pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::invariant(attr, tokens) +} + +#[proc_macro_attribute] +pub fn constant(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::constant(attr, tokens) +} + +#[proc_macro_attribute] +pub fn opaque(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::opaque(attr, tokens) +} + +#[proc_macro_attribute] +pub fn trusted(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::trusted(attr, tokens) } #[proc_macro] pub fn flux(tokens: TokenStream) -> TokenStream { flux_attrs::flux(tokens.into()).into() } + +#[proc_macro] +pub fn defs(tokens: TokenStream) -> TokenStream { + attr_impl::defs(tokens) +} + +#[proc_macro_attribute] +pub fn extern_spec(attrs: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::extern_spec(attrs, tokens) +} + +#[cfg(flux_sysroot)] +mod attr_sysroot { + use super::*; + + pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream { + flux_attrs::extern_spec(attr.into(), tokens.into()).into() + } + + pub fn refined_by(attr: TokenStream, item: TokenStream) -> TokenStream { + flux_attrs::refined_by(attr.into(), item.into()).into() + } + + pub fn defs(tokens: TokenStream) -> TokenStream { + flux_attrs::defs(tokens.into()).into() + } + + macro_rules! flux_tool_attrs { + ($($name:ident),+ $(,)?) => { + $( + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + flux_attrs::flux_tool_item_attr(stringify!($name), attr.into(), item.into()).into() + } + )* + }; + } + + flux_tool_attrs!(alias, sig, qualifiers, constant, invariant, opaque, trusted); +} + +#[cfg(not(flux_sysroot))] +mod attr_dummy { + use super::*; + + pub fn refined_by(attr: TokenStream, item: TokenStream) -> TokenStream { + flux_attrs::refined_by(attr.into(), item.into()).into() + } + + pub fn defs(_tokens: TokenStream) -> TokenStream { + TokenStream::new() + } + + macro_rules! no_op { + ($($name:ident),+ $(,)?) => { + $( + pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream { + item + } + )+ + }; + } + + no_op!(alias, sig, qualifiers, invariant, constant, opaque, trusted, extern_spec); +} diff --git a/tools/cargo-flux b/tools/cargo-flux deleted file mode 100755 index 1a656f3269..0000000000 --- a/tools/cargo-flux +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/bash - -CARGO_INCREMENTAL=0 RUSTUP_TOOLCHAIN=nightly-2022-12-30 DYLD_FALLBACK_LIBRARY_PATH=~/.rustup/toolchains/nightly-2022-12-30-x86_64-aarch64-apple-darwin/lib RUSTC_WRAPPER=~/research/flux/target/release/flux cargo $@ diff --git a/tools/flux.sh b/tools/flux.sh deleted file mode 100755 index e8c8a593f7..0000000000 --- a/tools/flux.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/bash - -# Path to root of flux repository -FLUX=/Users/rjhala/research/rust/flux - -CWD=`pwd` -cd $FLUX -TOOLCHAIN=`rustup show active-toolchain | cut -d' ' -f 1` - -cd "$CWD" -rustup run "$TOOLCHAIN" cargo run --manifest-path "$FLUX/Cargo.toml" -- $@ - diff --git a/tools/install.sh b/tools/install.sh deleted file mode 100755 index e078b56cda..0000000000 --- a/tools/install.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash - -cargo install --path crates/flux --offline -cargo install --path crates/flux-bin --offline