Running Flux

You can run flux on a single file or entire crate.

Running on a File: `flux`

You can use flux as you would use rustc. For example, the following command checks the file test.rs.

flux path/to/test.rs

The flux binary accepts the same flags as rustc. You could for example check a file as a library instead of a binary like so

flux --crate-type=lib path/to/test.rs

When running flux on a file with flux path/to/test.rs, refinement annotations should be prefixed with flux::.

For example, the refinement below will only work when running flux which is intended for use on a single file.

#![allow(unused)]
fn main() {
#[flux::sig(fn(x: i32) -> i32{v: x < v})]
fn inc(x: i32) -> i32 {
    x - 1
}
}

Running on a package: `cargo-flux`

Flux is integrated with cargo and can be invoked in a package as follows:

cargo flux

By default, Flux won't verify a package unless it's explicitly enabled in the manifest. To do so add the following to Cargo.toml:

[package.metadata.flux]
enabled = true

Adding refinement annotations to cargo projects is simple. You can add flux-rs as a dependency in Cargo.toml

[dependencies]
flux-rs = { git  = "https://github.com/flux-rs/flux.git" }

Then, import attributes from flux_rs and add the appropriate refinement annoations.

#![allow(unused)]
fn main() {
use flux_rs::*;

#[sig(fn(x: i32) -> i32{v: x < v)]
fn inc(x: i32) -> i32 {
    x - 1
}
}

The following example declares a function inc that returns an integer greater than the input. We use the nightly feature register_tool to register the flux tool in order to add refinement annotations to functions.

#![allow(unused)]
fn main() {
#[flux::sig(fn(x: i32) -> i32{v: x < v})]
pub fn inc(x: i32) -> i32 {
    x - 1
}
}

You can save the above snippet in say test0.rs and then run

flux --crate-type=lib path/to/test0.rs

you should see in your output

error[FLUX]: postcondition might not hold
 --> test0.rs:3:5
  |
3 |     x - 1
  |     ^^^^^

as indeed x - 1 is not greater than x as required by the output refinement i32{v: x < v}.

If you fix the error by replacing x - 1 with x + 1, you should get no errors in the output (the output may be empty, but in this case no output is a good thing).

Read these chapters to learn more about what you specify and verify with flux.

A note about the flux-driver binary

The flux-driver binary is a rustc driver (similar to how clippy works) meaning it uses rustc as a library to "drive" compilation performing additional analysis along the way. Running the binary requires dynamically linking a correct version of librustc. Thus, to avoid the hassle you should never execute it directly. Instead, use flux or cargo-flux.

Editor Support

This section assumes you have installed cargo-flux.

Rust-Analyzer in VSCode

Add this to the workspace settings i.e. .vscode/settings.json

{
  "rust-analyzer.check.overrideCommand": [
    "cargo",
    "flux",
    "--workspace",
    "--message-format=json-diagnostic-rendered-ansi"
  ]
}

Note: Make sure to edit the paths in the above snippet to point to the correct locations on your machine.

Configuration

Flux Flags

The flux binary accepts configuration flags in the format -Fname=value. For boolean flags, the value can be one of y, yes, on, true, n, no, off, false. Alternatively, the value can be omitted which will default to true. For example, to set the solver to cvc5 and enable qualifier scrapping:

flux -Fsolver=cvc5 -Fscrape-quals path/to/file.rs

For all avilable flags, see https://flux-rs.github.io/flux/doc/flux_config/flags/struct.Flags.html

Cargo Projects

When working with a Cargo project, some of the flags can be configured in the [package.metadata.flux] table in Cargo.toml. For example, to enable query caching and set cvc5 as the solver:

# Cargo.toml
[package.metadata.flux]
enabled = true
cache = true
solver = "cvc5"

Additionally, cargo flux searches for a configuration file called flux.toml with the same format as the metadata table. The content of flux.toml takes precedence and it's merged with the content of the metadata table. Note that the content of flux.toml will override the metadata for all crates, including dependencies. This behavior is likely to change in the future as we figure out what configurations make sense to have per package and which should only affect the current execution of cargo flux.

You can see the format of the metadata in https://flux-rs.github.io/flux/doc/flux_bin/struct.FluxMetadata.html.

`FLUXFLAGS` Environement Variable

When running cargo flux, flags defined in FLUXFLAGS will be passed to all flux invocations, for example, to print timing information for all crates checked by Flux:

FLUXFLAGS="-Ftimings" cargo flux

Flux Documentation