flux_config/
flags.rs

1use std::{env, path::PathBuf, process, str::FromStr, sync::LazyLock};
2
3pub use toml::Value;
4use tracing::Level;
5
6use crate::{IncludePattern, LeanMode, OverflowMode, PointerWidth, RawDerefMode, SmtSolver};
7
8const FLUX_FLAG_PREFIX: &str = "-F";
9
10/// Exit status code used for invalid flags.
11pub const EXIT_FAILURE: i32 = 2;
12
13pub struct Flags {
14    /// Sets the directory to dump data. Defaults to `./log/`.
15    pub log_dir: PathBuf,
16    /// Sets the directory to put all the emitted lean definitions and verification conditions. Defaults to `./`.
17    pub lean_dir: PathBuf,
18    /// Name of the lean project. Defaults to `lean_proofs`.
19    pub lean_project: String,
20    /// If present, only check files matching the [`IncludePattern`] a glob pattern.
21    pub include: Option<IncludePattern>,
22    /// If present, trust items matching [`IncludePattern`]. This implies `-Finclude`
23    pub include_trusted: Option<IncludePattern>,
24    /// If present, trust items matching [`IncludePattern`]. This implies `-Finclude`
25    pub include_trusted_impl: Option<IncludePattern>,
26    /// Set the pointer size (either `32` or `64`), used to determine if an integer cast is lossy
27    /// (default `64`).
28    pub pointer_width: PointerWidth,
29    /// If present switches on query caching and saves the cache in the provided path
30    pub cache: Option<PathBuf>,
31    /// Compute statistics about number and size of annotations. Dumps file to [`Self::log_dir`]
32    pub annots: bool,
33    /// Print statistics about time taken to analyze each fuction. Also dumps a file with the raw
34    /// times for each function.
35    pub timings: bool,
36    /// Print statistics about number of functions checked, trusted, etc.
37    pub summary: bool,
38    /// Default solver. Either `z3` or `cvc5`.
39    pub solver: SmtSolver,
40    /// Enables qualifier scrapping in fixpoint
41    pub scrape_quals: bool,
42    /// Enables uninterpreted casts
43    pub allow_uninterpreted_cast: bool,
44    /// Translates _monomorphic_ `defs` functions into SMT `define-fun` instead of inlining them
45    /// away inside `flux`.
46    pub smt_define_fun: bool,
47    /// If `strict` checks for over and underflow on arithmetic integer operations,
48    /// If `lazy` checks for underflow and loses information if possible overflow,
49    /// If `none` (default), it still checks for underflow on unsigned integer subtraction.
50    pub check_overflow: OverflowMode,
51    /// Whether to allow raw pointer dereferences during refinement checking.
52    pub allow_raw_deref: RawDerefMode,
53    /// Dump constraints generated for each function (debugging)
54    pub dump_constraint: bool,
55    /// Saves the checker's trace (debugging)
56    pub dump_checker_trace: Option<tracing::Level>,
57    /// Saves the `fhir` for each item (debugging)
58    pub dump_fhir: bool,
59    /// Saves the the `fhir` (debugging)
60    pub dump_rty: bool,
61    /// Optimistically keeps running flux even after errors are found to get as many errors as possible
62    pub catch_bugs: bool,
63    /// Whether verification for the current crate is enabled. If false (the default), `flux-driver`
64    /// will behave exactly like `rustc`. This flag is managed by the `cargo flux` and `flux` binaries,
65    /// so you don't need to mess with it.
66    pub verify: bool,
67    /// If `true`, produce artifacts after analysis. This flag is managed by `cargo flux`, so you
68    /// don't typically have to set it manually.
69    pub full_compilation: bool,
70    /// Path to the Flux sysroot directory. If not set, the driver infers it from its own binary location.
71    pub sysroot: Option<PathBuf>,
72    /// If `true`, all code is trusted by default. You can selectively untrust items by marking them with `#[trusted(no)]`. The default value of this flag is `false`, i.e., all code is untrusted by default.
73    pub trusted_default: bool,
74    /// If `true`, all code will be ignored by default. You can selectively unignore items by marking them with `#[ignore(no)]`. The default value of this flag is `false`, i.e., all code is unignored by default.
75    pub ignore_default: bool,
76    pub lean: LeanMode,
77    /// If `true`, every function is implicitly labeled with a `no_panic` by default.
78    pub no_panic: bool,
79    /// If `true`, automatically inject `flux_core` and `flux_alloc` as force externs using paths
80    /// from `sysroot.toml`. Off by default.
81    pub std_extern_specs: bool,
82    /// If `true`, produce more detailed error messages (e.g. condition spans for fold errors).
83    pub verbose: bool,
84}
85
86impl Default for Flags {
87    fn default() -> Self {
88        Self {
89            log_dir: PathBuf::from("./log/"),
90            lean_dir: PathBuf::from("./"),
91            lean_project: "lean_proofs".to_string(),
92            dump_constraint: false,
93            dump_checker_trace: None,
94            dump_fhir: false,
95            dump_rty: false,
96            catch_bugs: false,
97            pointer_width: PointerWidth::default(),
98            include: None,
99            include_trusted: None,
100            include_trusted_impl: None,
101            cache: None,
102            check_overflow: OverflowMode::default(),
103            allow_raw_deref: RawDerefMode::default(),
104            scrape_quals: false,
105            allow_uninterpreted_cast: false,
106            solver: SmtSolver::default(),
107            smt_define_fun: false,
108            annots: false,
109            timings: false,
110            summary: true,
111            verify: false,
112            full_compilation: false,
113            sysroot: None,
114            trusted_default: false,
115            ignore_default: false,
116            lean: LeanMode::default(),
117            no_panic: false,
118            std_extern_specs: false,
119            verbose: false,
120        }
121    }
122}
123
124pub(crate) static FLAGS: LazyLock<Flags> = LazyLock::new(|| {
125    let mut flags = Flags::default();
126    let mut includes: Vec<String> = Vec::new();
127    let mut trusteds: Vec<String> = Vec::new();
128    let mut trusted_impls: Vec<String> = Vec::new();
129    for arg in env::args() {
130        let Some((key, value)) = parse_flux_arg(&arg) else { continue };
131
132        let result = match key {
133            "log-dir" => parse_path_buf(&mut flags.log_dir, value),
134            "lean-dir" => parse_path_buf(&mut flags.lean_dir, value),
135            "lean-project" => parse_string(&mut flags.lean_project, value),
136            "dump-constraint" => parse_bool(&mut flags.dump_constraint, value),
137            "dump-checker-trace" => parse_opt_level(&mut flags.dump_checker_trace, value),
138            "dump-fhir" => parse_bool(&mut flags.dump_fhir, value),
139            "dump-rty" => parse_bool(&mut flags.dump_rty, value),
140            "catch-bugs" => parse_bool(&mut flags.catch_bugs, value),
141            "pointer-width" => parse_pointer_width(&mut flags.pointer_width, value),
142            "check-overflow" => parse_overflow(&mut flags.check_overflow, value),
143            "allow-raw-deref" => parse_raw_deref(&mut flags.allow_raw_deref, value),
144            "scrape-quals" => parse_bool(&mut flags.scrape_quals, value),
145            "allow-uninterpreted-cast" => parse_bool(&mut flags.allow_uninterpreted_cast, value),
146            "solver" => parse_solver(&mut flags.solver, value),
147            "smt-define-fun" => parse_bool(&mut flags.smt_define_fun, value),
148            "annots" => parse_bool(&mut flags.annots, value),
149            "timings" => parse_bool(&mut flags.timings, value),
150            "summary" => parse_bool(&mut flags.summary, value),
151            "cache" => parse_opt_path_buf(&mut flags.cache, value),
152            "include" => parse_opt_include(&mut includes, value),
153            "include-trusted" => parse_opt_include(&mut trusteds, value),
154            "include-trusted-impl" => parse_opt_include(&mut trusted_impls, value),
155            "verify" => parse_bool(&mut flags.verify, value),
156            "full-compilation" => parse_bool(&mut flags.full_compilation, value),
157            "sysroot" => parse_opt_path_buf(&mut flags.sysroot, value),
158            "trusted" => parse_bool(&mut flags.trusted_default, value),
159            "ignore" => parse_bool(&mut flags.ignore_default, value),
160            "lean" => parse_lean_mode(&mut flags.lean, value),
161            "no-panic" => parse_bool(&mut flags.no_panic, value),
162            "std-extern-specs" => parse_bool(&mut flags.std_extern_specs, value),
163            "verbose" => parse_bool(&mut flags.verbose, value),
164            _ => {
165                eprintln!("error: unknown flux option: `{key}`");
166                process::exit(EXIT_FAILURE);
167            }
168        };
169        if let Err(reason) = result {
170            eprintln!("error: incorrect value for flux option `{key}` - `{reason}`");
171            process::exit(1);
172        }
173    }
174    if !includes.is_empty() {
175        let include = IncludePattern::new(includes).unwrap_or_else(|err| {
176            eprintln!("error: invalid include pattern: {err}");
177            process::exit(1);
178        });
179        flags.include = Some(include);
180    }
181    if !trusteds.is_empty() {
182        let trusted = IncludePattern::new(trusteds).unwrap_or_else(|err| {
183            eprintln!("error: invalid trusted pattern: {err}");
184            process::exit(1);
185        });
186        flags.include_trusted = Some(trusted);
187    }
188    if !trusted_impls.is_empty() {
189        let trusted_impl = IncludePattern::new(trusted_impls).unwrap_or_else(|err| {
190            eprintln!("error: invalid trusted-impl pattern: {err}");
191            process::exit(1);
192        });
193        flags.include_trusted_impl = Some(trusted_impl);
194    }
195    flags
196});
197
198pub fn is_flux_arg(arg: &str) -> bool {
199    parse_flux_arg(arg).is_some()
200}
201
202fn parse_flux_arg(arg: &str) -> Option<(&str, Option<&str>)> {
203    let arg = arg.strip_prefix(FLUX_FLAG_PREFIX)?;
204    if arg.is_empty() {
205        return None;
206    }
207    if let Some((k, v)) = arg.split_once('=') { Some((k, Some(v))) } else { Some((arg, None)) }
208}
209
210fn parse_bool(slot: &mut bool, v: Option<&str>) -> Result<(), &'static str> {
211    match v {
212        Some("y") | Some("yes") | Some("on") | Some("true") | None => {
213            *slot = true;
214            Ok(())
215        }
216        Some("n") | Some("no") | Some("off") | Some("false") => {
217            *slot = false;
218            Ok(())
219        }
220        _ => {
221            Err(
222                "expected no value or one of `y`, `yes`, `on`, `true`, `n`, `no`, `off`, or `false`",
223            )
224        }
225    }
226}
227
228fn parse_string(slot: &mut String, v: Option<&str>) -> Result<(), &'static str> {
229    match v {
230        Some(s) => {
231            *slot = s.to_string();
232            Ok(())
233        }
234        None => Err("expected a string"),
235    }
236}
237
238fn parse_path_buf(slot: &mut PathBuf, v: Option<&str>) -> Result<(), &'static str> {
239    match v {
240        Some(s) => {
241            *slot = PathBuf::from(s);
242            Ok(())
243        }
244        None => Err("expected a path"),
245    }
246}
247
248fn parse_pointer_width(slot: &mut PointerWidth, v: Option<&str>) -> Result<(), &'static str> {
249    match v {
250        Some(s) => {
251            *slot = s.parse()?;
252            Ok(())
253        }
254        _ => Err(PointerWidth::ERROR),
255    }
256}
257
258fn parse_lean_mode(slot: &mut LeanMode, v: Option<&str>) -> Result<(), &'static str> {
259    match v {
260        Some(s) => {
261            *slot = s.parse()?;
262            Ok(())
263        }
264        _ => Err(LeanMode::ERROR),
265    }
266}
267
268fn parse_overflow(slot: &mut OverflowMode, v: Option<&str>) -> Result<(), &'static str> {
269    match v {
270        Some(s) => {
271            *slot = s.parse()?;
272            Ok(())
273        }
274        _ => Err(OverflowMode::ERROR),
275    }
276}
277
278fn parse_raw_deref(slot: &mut RawDerefMode, v: Option<&str>) -> Result<(), &'static str> {
279    match v {
280        Some(s) => {
281            *slot = s.parse()?;
282            Ok(())
283        }
284        _ => Err(RawDerefMode::ERROR),
285    }
286}
287
288fn parse_solver(slot: &mut SmtSolver, v: Option<&str>) -> Result<(), &'static str> {
289    match v {
290        Some(s) => {
291            *slot = s.parse()?;
292            Ok(())
293        }
294        _ => Err(SmtSolver::ERROR),
295    }
296}
297
298fn parse_opt_path_buf(slot: &mut Option<PathBuf>, v: Option<&str>) -> Result<(), &'static str> {
299    match v {
300        Some(s) => {
301            *slot = Some(PathBuf::from(s));
302            Ok(())
303        }
304        None => Err("expected a path"),
305    }
306}
307
308fn parse_opt_level(slot: &mut Option<Level>, v: Option<&str>) -> Result<(), &'static str> {
309    match v {
310        Some(s) => {
311            *slot = Some(Level::from_str(s).map_err(|_| "invalid level")?);
312            Ok(())
313        }
314        None => Err("a level"),
315    }
316}
317
318fn parse_opt_include(slot: &mut Vec<String>, v: Option<&str>) -> Result<(), &'static str> {
319    if let Some(include) = v {
320        slot.push(include.to_string());
321    }
322    Ok(())
323}
flux_config/flags.rs

flux_config/
flags.rs
