Implement macros to allow using flux in a project with a stable compiler

book/.gitignore

@@ -1 +1 @@
-book/
+./book/

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.

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`.

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.

crates/flux-bin/src/bin/rustc-flux.rs

@@ -29,8 +29,6 @@ fn run() -> Result<i32> {
     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")

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<String> {
     Some(format!("{home}/toolchains/{toolchain}"))
 }
 
-/// Run Flux Rust and return the exit status code.
-pub fn run_compiler(args: Vec<String>, 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<Target = str>>(
+    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
 }

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
     }
 }
 

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 {

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! {