|
| 1 | +# Flux |
| 2 | + |
| 3 | +[Flux](https://flux-rs.github.io/flux) is a refinement type checker |
| 4 | +that can be used to prove user-defined safety properties for Rust. |
| 5 | +Users can write their own properties via refinement type contracts |
| 6 | +(a generalization of pre- and post-conditions). Additionally, out of the |
| 7 | +box, Flux checks for various issues such as |
| 8 | + |
| 9 | +- arithmetic overflows |
| 10 | +- division by zero |
| 11 | +- array bounds violations |
| 12 | + |
| 13 | +Currently, Flux does not distinguish between logic errors (e.g., those that may cause a panic) |
| 14 | +and errors that can lead to undefined behavior. They both manifest |
| 15 | +as contract violations. |
| 16 | + |
| 17 | +## Installation |
| 18 | + |
| 19 | +See the [installation section of the Flux book](https://flux-rs.github.io/flux/install.html) |
| 20 | +to learn how to install and run Flux. |
| 21 | + |
| 22 | + |
| 23 | +## Usage |
| 24 | + |
| 25 | +(Adapted from the Kani documentation; see [the Flux book](https://flux-rs.github.io/flux) |
| 26 | +for many more examples.) |
| 27 | + |
| 28 | +Consider a Rust file `demo.rs` with a function that returns |
| 29 | +the absolute value of the difference between two integers. |
| 30 | +To *prove* that the function always returns a *non-negative* result, you write |
| 31 | +a Flux specification—above the function definition—that says the output |
| 32 | +is a refinement type `i32{v: 0 <= v}` denoting non-negative `i32` values. |
| 33 | + |
| 34 | + |
| 35 | +``` rust |
| 36 | +// demo.rs |
| 37 | +#[allow(dead_code)] |
| 38 | +#[cfg_attr(flux, flux::spec(fn(a: i32, b: i32) -> i32{v:0 <= v}))] |
| 39 | +fn test_abs(a:i32, b:i32) -> i32 { |
| 40 | + if a > b { |
| 41 | + a - b |
| 42 | + } else { |
| 43 | + b - a |
| 44 | + } |
| 45 | +} |
| 46 | +``` |
| 47 | + |
| 48 | +Now, if you run |
| 49 | + |
| 50 | +``` |
| 51 | +$ flux --crate-type=lib demo.rs |
| 52 | +``` |
| 53 | + |
| 54 | +Flux will return immediately with **no output** indicating the code is safe. |
| 55 | + |
| 56 | +This may be baffling for those with a keen understanding of arithmetic overflows: |
| 57 | +what if `a` is `INT_MAX` and `b` is `INT_MIN`? Indeed, Flux has overflow checking |
| 58 | +off by default but you can optionally switch it on for a function, module, or entire crate. |
| 59 | + |
| 60 | +``` rust |
| 61 | +// demo.rs |
| 62 | +#[allow(dead_code)] |
| 63 | +#[cfg_attr(flux, flux::opts(check_overflow = true))] |
| 64 | +#[cfg_attr(flux, flux::spec(fn(a: i32, b: i32) -> i32{v:0 <= v}))] |
| 65 | +fn test_abs(a:i32, b:i32) -> i32 { |
| 66 | + if a > b { |
| 67 | + a - b |
| 68 | + } else { |
| 69 | + b - a |
| 70 | + } |
| 71 | +} |
| 72 | +``` |
| 73 | + |
| 74 | +Now, when you run `flux` you see that |
| 75 | + |
| 76 | +``` |
| 77 | +$ flux --crate-type=lib demo.rs |
| 78 | +error[E0999]: arithmetic operation may overflow |
| 79 | + --> demo.rs:9:9 |
| 80 | + | |
| 81 | +9 | b - a |
| 82 | + | ^^^^^ |
| 83 | +
|
| 84 | +error[E0999]: arithmetic operation may overflow |
| 85 | + --> demo.rs:7:9 |
| 86 | + | |
| 87 | +7 | a - b |
| 88 | + | ^^^^^ |
| 89 | +
|
| 90 | +error: aborting due to 2 previous errors |
| 91 | +``` |
| 92 | + |
| 93 | +You might *fix* the errors, i.e., prove the function have no overflows, |
| 94 | +by requiring the *inputs* also be non-negative: |
| 95 | + |
| 96 | +```rust |
| 97 | +#[allow(dead_code)] |
| 98 | +#[cfg_attr(flux, flux::opts(check_overflow = true))] |
| 99 | +#[cfg_attr(flux, flux::spec(fn(a: i32{0 <= a}, b: i32{0 <= b}) -> i32{v: 0 <= v}))] |
| 100 | +fn test_abs(a:u32, b:u32) -> u32 { |
| 101 | + if a > b { |
| 102 | + a - b |
| 103 | + } else { |
| 104 | + b - a |
| 105 | + } |
| 106 | +} |
| 107 | +``` |
| 108 | + |
| 109 | +This time `flux --crate-type=lib demo.rs` finishes swiftly without reporting any errors. |
| 110 | + |
| 111 | +For a more detailed online interactive tutorial, with many more examples, see [the Flux book](https://flux-rs.github.io/flux). |
| 112 | + |
| 113 | +## Using Flux to verify the (model-checking fork of) the Rust Standard Library |
| 114 | + |
| 115 | +Currrently, we have configured Flux to run on the |
| 116 | +[model-checking fork](https://github.com/model-checking/verify-rust-std) |
| 117 | +of the Rust Standard Library. You can run Flux on |
| 118 | + |
| 119 | +1. a single function, |
| 120 | +2. a single file, |
| 121 | +3. a set of files matching a glob-pattern, or |
| 122 | +4. the entire crate. |
| 123 | + |
| 124 | +### Running on a Single Function |
| 125 | + |
| 126 | +Suppose the function is in a file inside `library/core/src/`, e.g., |
| 127 | +`library/core/src/ascii/ascii_char.rs`. |
| 128 | +For example, let's suppose `test_abs` was added to the end of that file, |
| 129 | +*with* the `check_overflow = true` and *without* the `flux::spec` contract. |
| 130 | +Then if you did |
| 131 | + |
| 132 | +```bash |
| 133 | +$ cd library/core |
| 134 | +$ FLUXFLAGS="-Fcheck-def=test_abs" cargo flux |
| 135 | +``` |
| 136 | + |
| 137 | +you should get some output like |
| 138 | + |
| 139 | +``` |
| 140 | + Checking core v0.0.0 (/verify-rust-std/library/core) |
| 141 | +
|
| 142 | +error[E0999]: arithmetic operation may overflow |
| 143 | + --> core/src/ascii/ascii_char.rs:635:9 |
| 144 | + | |
| 145 | +635 | b - a |
| 146 | + | ^^^^^ |
| 147 | +
|
| 148 | +error[E0999]: arithmetic operation may overflow |
| 149 | + --> core/src/ascii/ascii_char.rs:633:9 |
| 150 | + | |
| 151 | +633 | a - b |
| 152 | + | ^^^^^ |
| 153 | +
|
| 154 | +error: could not compile `core` (lib) due to 2 previous errors |
| 155 | +
|
| 156 | +Checking core v0.0.0 (/verify-rust-std/library/core) |
| 157 | +Finished `flux` profile [unoptimized + debuginfo] target(s) in 5.54s |
| 158 | +``` |
| 159 | + |
| 160 | + |
| 161 | +You can now fix the error by adding the non-negative input specification above the definition |
| 162 | +of `test_abs` |
| 163 | + |
| 164 | +```rust |
| 165 | +#[cfg_attr(flux, flux::spec(fn(a: i32{0 <= a}, b: i32{0 <= b}) -> i32{v: 0 <= v})] |
| 166 | +``` |
| 167 | + |
| 168 | +and when you re-run, it should finish with no warnings |
| 169 | + |
| 170 | +**NOTE** When checking inside `core`, we wrap the `flux` specification attributes |
| 171 | +in `#[cfg_attr(flux,...)]` so they are only read by flux. |
| 172 | + |
| 173 | +### Running on a Single File |
| 174 | + |
| 175 | +To run on a single _file_ you can just pass the name of that file to flux (relative from the |
| 176 | +crate root) as |
| 177 | + |
| 178 | +```bash |
| 179 | +$ cd library/core |
| 180 | +$ FLUXFLAGS="-Finclude=src/ascii/ascii_char.rs" cargo flux |
| 181 | +``` |
| 182 | + |
| 183 | +### Running on a Globset of Files |
| 184 | + |
| 185 | +To run on a comma-separated _globset of files_, e.g., an entire module, you can just pass |
| 186 | +the appropriate globset as |
| 187 | + |
| 188 | +```bash |
| 189 | +$ cd library/core |
| 190 | +$ FLUXFLAGS="-Finclude=src/ascii/*" cargo flux |
| 191 | +``` |
| 192 | + |
| 193 | +### Configuring Flux via `Cargo.toml` |
| 194 | + |
| 195 | +Flux can also be configured in the `Cargo.toml` under the |
| 196 | +`[package.metadata.flux]` section. |
| 197 | + |
| 198 | +You can add or remove things from the `include` declaration there |
| 199 | +to check other files. Currently, it is configured to only run on a |
| 200 | +tiny subset of the modules; you should comment out that line if you |
| 201 | +want to run on _all_ of `core`. |
| 202 | + |
| 203 | +You can run flux on all the parts of the `core` crate specified in `include` |
| 204 | +directive in the `Cargo.toml` by doing |
| 205 | + |
| 206 | +```bash |
| 207 | +$ cd library/core |
| 208 | +$ cargo flux |
| 209 | +``` |
| 210 | + |
| 211 | +### Running on the Entire Crate |
| 212 | + |
| 213 | +Currently the `core/Cargo.toml` is configured (see the `[package.metadata.flux]`) to |
| 214 | +only run on a tiny subset of the modules, you should comment out that line if you |
| 215 | +really want to run on _all_ of `core`, and then run |
| 216 | + |
| 217 | +```bash |
| 218 | +$ cd library/core |
| 219 | +$ cargo flux |
| 220 | +``` |
| 221 | + |
| 222 | +Sadly, various Rust features exercised by the crate are not currently supported by |
| 223 | +Flux making it crash ignominously. |
| 224 | + |
| 225 | +You can tell it to do a "best-effort" analysis by ignoring those crashes |
| 226 | +(as much as possible) by |
| 227 | + |
| 228 | +```bash |
| 229 | +$ FLUXFLAGS="-Fcatch-bugs" cargo flux |
| 230 | +``` |
| 231 | + |
| 232 | +in which case Flux will grind over the whole crate and point out nearly 300+ *possible* |
| 233 | +warnings about overflows, array bounds accesses etc., |
| 234 | +and also about 200+ ICE (places where it crashes!) To do this, you may also have |
| 235 | +to tell Flux to not check certain modules, e.g. by adding |
| 236 | +various `flux::trusted` annotations [as shown here](https://github.com/flux-rs/verify-rust-std/blob/fluxable/library/core/src/lib.rs) |
| 237 | + |
| 238 | + |
| 239 | +## More details |
| 240 | + |
| 241 | +You can find more information on using Flux—especially on how to write different |
| 242 | +kinds of specifications and configuration options—in [the Flux book](https://flux-rs.github.io/flux). |
| 243 | +Happy proving! |
| 244 | + |
| 245 | +## Caveats and Current Limitations |
| 246 | + |
| 247 | +Flux is aimed to be a lightweight verifier that is predictable and fully automated. To achieve this, |
| 248 | +it restricts refinement predicates to decidable fragments of first-order logic |
| 249 | +(i.e., without quantifiers). As a result, some properties (such as sortedness of arrays) may be |
| 250 | +hard to specify. |
| 251 | + |
| 252 | +Flux also has limited and conservative support for unsafe code. It can track properties of |
| 253 | +pointers (e.g., alignment and provenance) but not the values of data written through |
| 254 | +them. |
| 255 | + |
| 256 | +Lastly, Flux is under active development, and many Rust features are not yet supported. |
0 commit comments