flux_config/
flags.rs

1use std::{env, path::PathBuf, process, str::FromStr, sync::LazyLock};
2
3use clap::{ArgMatches, Args, Command, FromArgMatches, parser::ValueSource};
4pub use toml::Value;
5use tracing::Level;
6
7use crate::{
8    IncludePattern, LeanMode, OverflowMode, PointerWidth, RawDerefMode, SmtSolver, UifOps,
9};
10
11const FLUX_FLAG_PREFIX: &str = "-F";
12
13macro_rules! flux_arg {
14    ($name:literal) => {
15        concat!("F", $name)
16    };
17}
18
19/// Exit status code used for invalid flags.
20pub const EXIT_FAILURE: i32 = 2;
21
22#[derive(Args)]
23#[command(next_help_heading = "Flux-Specific Flags")]
24pub struct Flags {
25    /// Sets the directory to dump data.
26    #[arg(
27        long = flux_arg!("log-dir"),
28        value_name = "PATH",
29        default_value = "./log/",
30    )]
31    pub log_dir: PathBuf,
32    /// Sets the directory to put all the emitted lean definitions and verification conditions.
33    #[arg(
34        long = flux_arg!("lean-dir"),
35        value_name = "PATH",
36        default_value = "./"
37    )]
38    pub lean_dir: PathBuf,
39    /// Name of the lean project.
40    #[arg(
41        long = flux_arg!("lean-project"),
42        value_name = "NAME",
43        default_value = "lean_proofs"
44    )]
45    pub lean_project: String,
46    /// If present, only check files matching the [`IncludePattern`] (a glob pattern).
47    #[arg(long = flux_arg!("include"), value_name = "PATTERN")]
48    pub include: Option<IncludePattern>,
49    /// If present, trust items matching [`IncludePattern`]. This implies `-Finclude`
50    #[arg(long = flux_arg!("include-trusted"), value_name = "PATTERN")]
51    pub include_trusted: Option<IncludePattern>,
52    /// If present, trust items matching [`IncludePattern`]. This implies `-Finclude`
53    #[arg(long = flux_arg!("include-trusted-impl"), value_name = "PATTERN")]
54    pub include_trusted_impl: Option<IncludePattern>,
55    /// Set the pointer size (either `32` or `64`), used to determine if an integer cast is lossy.
56    #[arg(
57        long = flux_arg!("pointer-width"),
58        value_name = "WIDTH",
59        default_value = "64"
60    )]
61    pub pointer_width: PointerWidth,
62    /// If present, switches on query caching and saves the cache in the provided path
63    #[arg(long = flux_arg!("cache"), value_name = "PATH")]
64    pub cache: Option<PathBuf>,
65    /// Compute statistics about number and size of annotations. Dumps file to [`Self::log_dir`].
66    #[arg(
67        long = flux_arg!("annots"),
68        num_args = 0..=1,
69        default_missing_value = "true"
70    )]
71    pub annots: bool,
72    /// Print statistics about time taken to analyze each function. Also dumps a file with the raw
73    /// times for each function.
74    #[arg(
75        long = flux_arg!("timings"),
76        num_args = 0..=1,
77        default_missing_value = "true"
78    )]
79    pub timings: bool,
80    /// Print statistics about number of functions checked, trusted, etc.
81    #[arg(
82        long = flux_arg!("summary"),
83        num_args = 0..=1,
84        default_value = "true",
85        default_missing_value = "true"
86    )]
87    pub summary: bool,
88    /// Default solver. Either `z3` or `cvc5`.
89    #[arg(
90        long = flux_arg!("solver"),
91        value_name = "SOLVER",
92        default_value = "z3"
93    )]
94    pub solver: SmtSolver,
95    /// Enables qualifier scrapping in fixpoint.
96    #[arg(
97        long = flux_arg!("scrape-quals"),
98        num_args = 0..=1,
99        default_missing_value = "true"
100    )]
101    pub scrape_quals: bool,
102    /// Timeout in seconds for each fixpoint query. If a query doesn't finish in time, fixpoint is
103    /// killed and an error is reported for the item being checked. Disabled by default.
104    #[arg(long = flux_arg!("fixpoint-timeout"), value_name = "SECONDS")]
105    pub fixpoint_timeout: Option<u64>,
106    /// Enables uninterpreted casts.
107    #[arg(
108        long = flux_arg!("allow-uninterpreted-cast"),
109        num_args = 0..=1,
110        default_missing_value = "true"
111    )]
112    pub allow_uninterpreted_cast: bool,
113    /// If `strict` checks for over and underflow on arithmetic integer operations,
114    /// If `lazy` checks for underflow and loses information if possible overflow,
115    /// If `none` (default), it still checks for underflow on unsigned integer subtraction.
116    #[arg(
117        long = flux_arg!("check-overflow"),
118        value_name = "MODE",
119        default_value = "none"
120    )]
121    pub check_overflow: OverflowMode,
122    /// Whether to allow raw pointer dereferences during refinement checking.
123    #[arg(
124        long = flux_arg!("allow-raw-deref"),
125        value_name = "MODE",
126        default_value = "none"
127    )]
128    pub allow_raw_deref: RawDerefMode,
129    /// Binary operators to encode as uninterpreted functions in the constraints, as a comma
130    /// separated list, e.g., `*,/,%`.
131    #[arg(long = flux_arg!("uif-ops"), value_name = "OPS", default_value = "")]
132    pub uif_ops: UifOps,
133    /// Dump constraints generated for each function (debugging).
134    #[arg(
135        long = flux_arg!("dump-constraint"),
136        num_args = 0..=1,
137        default_missing_value = "true"
138    )]
139    pub dump_constraint: bool,
140    /// Saves the checker's trace (debugging).
141    #[arg(long = flux_arg!("dump-checker-trace"), value_name = "LEVEL")]
142    pub dump_checker_trace: Option<tracing::Level>,
143    /// Saves the `fhir` for each item (debugging).
144    #[arg(
145        long = flux_arg!("dump-fhir"),
146        num_args = 0..=1,
147        default_missing_value = "true"
148    )]
149    pub dump_fhir: bool,
150    /// Saves the the `fhir` (debugging).
151    #[arg(
152        long = flux_arg!("dump-rty"),
153        num_args = 0..=1,
154        default_missing_value = "true"
155    )]
156    pub dump_rty: bool,
157    /// Optimistically keeps running flux even after errors are found to get as many errors as possible.
158    #[arg(
159        long = flux_arg!("catch-bugs"),
160        num_args = 0..=1,
161        default_missing_value = "true"
162    )]
163    pub catch_bugs: bool,
164    /// Whether verification for the current crate is enabled. If false (the default), `flux-driver`
165    /// will behave exactly like `rustc`. This flag is managed by the `cargo flux` and `flux` binaries,
166    /// so you don't need to mess with it.
167    #[arg(
168        long = flux_arg!("verify"),
169        num_args = 0..=1,
170        default_missing_value = "true"
171    )]
172    pub verify: bool,
173    /// If `true`, produce artifacts after analysis. This flag is managed by `cargo flux`, so you
174    /// don't typically have to set it manually.
175    #[arg(
176        long = flux_arg!("full-compilation"),
177        num_args = 0..=1,
178        default_missing_value = "true"
179    )]
180    pub full_compilation: bool,
181    /// Path to the Flux sysroot directory. If not set, the driver infers it from its own binary location.
182    #[arg(long = flux_arg!("sysroot"), value_name = "PATH")]
183    pub sysroot: Option<PathBuf>,
184    /// 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.
185    #[arg(
186        long = flux_arg!("trusted"),
187        num_args = 0..=1,
188        default_missing_value = "true"
189    )]
190    pub trusted_default: bool,
191    /// 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.
192    #[arg(
193        long = flux_arg!("ignore"),
194        num_args = 0..=1,
195        default_missing_value = "true"
196    )]
197    pub ignore_default: bool,
198    #[arg(long = flux_arg!("lean"), value_name = "MODE", default_value = "off")]
199    pub lean: LeanMode,
200    /// If `true`, every function is implicitly labeled with a `no_panic` by default.
201    #[arg(
202        long = flux_arg!("no-panic"),
203        num_args = 0..=1,
204        default_missing_value = "true"
205    )]
206    pub no_panic: bool,
207    /// If `true`, automatically inject `flux_core` and `flux_alloc` as force externs using paths
208    /// from `sysroot.toml`. Off by default.
209    #[arg(
210        long = flux_arg!("std-extern-specs"),
211        num_args = 0..=1,
212        default_missing_value = "true"
213    )]
214    pub std_extern_specs: bool,
215    /// If `true`, produce more detailed error messages (e.g. condition spans for fold errors).
216    #[arg(
217        long = flux_arg!("flux-verbose"),
218        num_args = 0..=1,
219        default_missing_value = "true"
220    )]
221    pub flux_verbose: bool,
222    /// If `true`, all code will have suggestions disabled.
223    #[arg(
224        long = flux_arg!("no-suggestions"),
225        num_args = 0..=1,
226        default_missing_value = "true"
227    )]
228    pub no_suggestions_default: bool,
229    /// If `true` (the default), attach a note to each failing item with a copy-pasteable command to
230    /// re-run the check on just that item. Only applies when running under `cargo flux`.
231    #[arg(
232        long = flux_arg!("rerun-hint"),
233        num_args = 0..=1,
234        default_value = "true",
235        default_missing_value = "true"
236    )]
237    pub rerun_hint: bool,
238}
239
240impl Default for Flags {
241    fn default() -> Self {
242        Self {
243            log_dir: PathBuf::from("./log/"),
244            lean_dir: PathBuf::from("./"),
245            lean_project: "lean_proofs".to_string(),
246            dump_constraint: false,
247            dump_checker_trace: None,
248            dump_fhir: false,
249            dump_rty: false,
250            catch_bugs: false,
251            pointer_width: PointerWidth::default(),
252            include: None,
253            include_trusted: None,
254            include_trusted_impl: None,
255            cache: None,
256            check_overflow: OverflowMode::default(),
257            allow_raw_deref: RawDerefMode::default(),
258            uif_ops: UifOps::default(),
259            scrape_quals: false,
260            fixpoint_timeout: None,
261            allow_uninterpreted_cast: false,
262            solver: SmtSolver::default(),
263            annots: false,
264            timings: false,
265            summary: true,
266            verify: false,
267            full_compilation: false,
268            sysroot: None,
269            trusted_default: false,
270            ignore_default: false,
271            lean: LeanMode::default(),
272            no_panic: false,
273            std_extern_specs: false,
274            flux_verbose: false,
275            no_suggestions_default: false,
276            rerun_hint: true,
277        }
278    }
279}
280
281impl Flags {
282    // Convert this struct into what we'd need to pass in through the environment var
283    pub fn rustflags(matches: &ArgMatches) -> Vec<String> {
284        let spec = Flags::augment_args(Command::new("flux-flags"));
285        let mut out = Vec::new();
286        for arg in spec.get_arguments() {
287            let id = arg.get_id().as_str();
288            if matches.value_source(id) != Some(ValueSource::CommandLine) {
289                continue;
290            }
291            let Some(long) = arg.get_long() else { continue };
292            match matches.get_raw(id) {
293                Some(values) => {
294                    out.extend(values.map(|v| format!("-{long}={}", v.to_string_lossy())))
295                }
296                None => out.push(format!("-{long}")),
297            }
298        }
299        out
300    }
301}
302
303#[derive(Clone, Debug, Default)]
304pub struct FluxFlags(pub Vec<String>);
305
306impl FromArgMatches for FluxFlags {
307    fn from_arg_matches(m: &ArgMatches) -> Result<Self, clap::Error> {
308        Ok(FluxFlags(Flags::rustflags(m)))
309    }
310    fn update_from_arg_matches(&mut self, m: &ArgMatches) -> Result<(), clap::Error> {
311        self.0 = Flags::rustflags(m);
312        Ok(())
313    }
314}
315
316impl Args for FluxFlags {
317    fn augment_args(cmd: Command) -> Command {
318        Flags::augment_args(cmd)
319    }
320    fn augment_args_for_update(cmd: Command) -> Command {
321        Flags::augment_args_for_update(cmd)
322    }
323}
324
325pub(crate) static FLAGS: LazyLock<Flags> = LazyLock::new(|| {
326    let mut flags = Flags::default();
327    let mut includes: Vec<String> = Vec::new();
328    let mut trusteds: Vec<String> = Vec::new();
329    let mut trusted_impls: Vec<String> = Vec::new();
330    for arg in env::args() {
331        let Some((key, value)) = parse_flux_arg(&arg) else { continue };
332
333        let result = match key {
334            "log-dir" => parse_path_buf(&mut flags.log_dir, value),
335            "lean-dir" => parse_path_buf(&mut flags.lean_dir, value),
336            "lean-project" => parse_string(&mut flags.lean_project, value),
337            "dump-constraint" => parse_bool(&mut flags.dump_constraint, value),
338            "dump-checker-trace" => parse_opt_level(&mut flags.dump_checker_trace, value),
339            "dump-fhir" => parse_bool(&mut flags.dump_fhir, value),
340            "dump-rty" => parse_bool(&mut flags.dump_rty, value),
341            "catch-bugs" => parse_bool(&mut flags.catch_bugs, value),
342            "pointer-width" => parse_pointer_width(&mut flags.pointer_width, value),
343            "check-overflow" => parse_overflow(&mut flags.check_overflow, value),
344            "allow-raw-deref" => parse_raw_deref(&mut flags.allow_raw_deref, value),
345            "uif-ops" => parse_uif_ops(&mut flags.uif_ops, value),
346            "scrape-quals" => parse_bool(&mut flags.scrape_quals, value),
347            "fixpoint-timeout" => parse_opt_u64(&mut flags.fixpoint_timeout, value),
348            "allow-uninterpreted-cast" => parse_bool(&mut flags.allow_uninterpreted_cast, value),
349            "solver" => parse_solver(&mut flags.solver, value),
350            "annots" => parse_bool(&mut flags.annots, value),
351            "timings" => parse_bool(&mut flags.timings, value),
352            "summary" => parse_bool(&mut flags.summary, value),
353            "cache" => parse_opt_path_buf(&mut flags.cache, value),
354            "include" => parse_opt_include(&mut includes, value),
355            "include-trusted" => parse_opt_include(&mut trusteds, value),
356            "include-trusted-impl" => parse_opt_include(&mut trusted_impls, value),
357            "verify" => parse_bool(&mut flags.verify, value),
358            "full-compilation" => parse_bool(&mut flags.full_compilation, value),
359            "sysroot" => parse_opt_path_buf(&mut flags.sysroot, value),
360            "trusted" => parse_bool(&mut flags.trusted_default, value),
361            "ignore" => parse_bool(&mut flags.ignore_default, value),
362            "lean" => parse_lean_mode(&mut flags.lean, value),
363            "no-panic" => parse_bool(&mut flags.no_panic, value),
364            "std-extern-specs" => parse_bool(&mut flags.std_extern_specs, value),
365            "flux-verbose" => parse_bool(&mut flags.flux_verbose, value),
366            "no-suggestions" => parse_bool(&mut flags.no_suggestions_default, value),
367            "rerun-hint" => parse_bool(&mut flags.rerun_hint, value),
368            _ => {
369                eprintln!("error: unknown flux option: `{key}`");
370                process::exit(EXIT_FAILURE);
371            }
372        };
373        if let Err(reason) = result {
374            eprintln!("error: incorrect value for flux option `{key}` - `{reason}`");
375            process::exit(1);
376        }
377    }
378    if !includes.is_empty() {
379        let include = IncludePattern::new(includes).unwrap_or_else(|err| {
380            eprintln!("error: invalid include pattern: {err}");
381            process::exit(1);
382        });
383        flags.include = Some(include);
384    }
385    if !trusteds.is_empty() {
386        let trusted = IncludePattern::new(trusteds).unwrap_or_else(|err| {
387            eprintln!("error: invalid trusted pattern: {err}");
388            process::exit(1);
389        });
390        flags.include_trusted = Some(trusted);
391    }
392    if !trusted_impls.is_empty() {
393        let trusted_impl = IncludePattern::new(trusted_impls).unwrap_or_else(|err| {
394            eprintln!("error: invalid trusted-impl pattern: {err}");
395            process::exit(1);
396        });
397        flags.include_trusted_impl = Some(trusted_impl);
398    }
399    flags
400});
401
402pub fn is_flux_arg(arg: &str) -> bool {
403    parse_flux_arg(arg).is_some()
404}
405
406fn parse_flux_arg(arg: &str) -> Option<(&str, Option<&str>)> {
407    let arg = arg.strip_prefix(FLUX_FLAG_PREFIX)?;
408    if arg.is_empty() {
409        return None;
410    }
411    if let Some((k, v)) = arg.split_once('=') { Some((k, Some(v))) } else { Some((arg, None)) }
412}
413
414fn parse_bool(slot: &mut bool, v: Option<&str>) -> Result<(), &'static str> {
415    match v {
416        Some("y") | Some("yes") | Some("on") | Some("true") | None => {
417            *slot = true;
418            Ok(())
419        }
420        Some("n") | Some("no") | Some("off") | Some("false") => {
421            *slot = false;
422            Ok(())
423        }
424        _ => {
425            Err(
426                "expected no value or one of `y`, `yes`, `on`, `true`, `n`, `no`, `off`, or `false`",
427            )
428        }
429    }
430}
431
432fn parse_string(slot: &mut String, v: Option<&str>) -> Result<(), &'static str> {
433    match v {
434        Some(s) => {
435            *slot = s.to_string();
436            Ok(())
437        }
438        None => Err("expected a string"),
439    }
440}
441
442fn parse_opt_u64(slot: &mut Option<u64>, v: Option<&str>) -> Result<(), &'static str> {
443    match v.and_then(|s| s.parse().ok()) {
444        Some(n) => {
445            *slot = Some(n);
446            Ok(())
447        }
448        None => Err("expected a non-negative integer"),
449    }
450}
451
452fn parse_path_buf(slot: &mut PathBuf, v: Option<&str>) -> Result<(), &'static str> {
453    match v {
454        Some(s) => {
455            *slot = PathBuf::from(s);
456            Ok(())
457        }
458        None => Err("expected a path"),
459    }
460}
461
462fn parse_pointer_width(slot: &mut PointerWidth, v: Option<&str>) -> Result<(), &'static str> {
463    match v {
464        Some(s) => {
465            *slot = s.parse()?;
466            Ok(())
467        }
468        _ => Err(PointerWidth::ERROR),
469    }
470}
471
472fn parse_lean_mode(slot: &mut LeanMode, v: Option<&str>) -> Result<(), &'static str> {
473    match v {
474        Some(s) => {
475            *slot = s.parse()?;
476            Ok(())
477        }
478        _ => Err(LeanMode::ERROR),
479    }
480}
481
482fn parse_overflow(slot: &mut OverflowMode, v: Option<&str>) -> Result<(), &'static str> {
483    match v {
484        Some(s) => {
485            *slot = s.parse()?;
486            Ok(())
487        }
488        _ => Err(OverflowMode::ERROR),
489    }
490}
491
492fn parse_uif_ops(slot: &mut UifOps, v: Option<&str>) -> Result<(), &'static str> {
493    match v {
494        Some(s) => {
495            *slot = s.parse()?;
496            Ok(())
497        }
498        _ => Err(UifOps::ERROR),
499    }
500}
501
502fn parse_raw_deref(slot: &mut RawDerefMode, v: Option<&str>) -> Result<(), &'static str> {
503    match v {
504        Some(s) => {
505            *slot = s.parse()?;
506            Ok(())
507        }
508        _ => Err(RawDerefMode::ERROR),
509    }
510}
511
512fn parse_solver(slot: &mut SmtSolver, v: Option<&str>) -> Result<(), &'static str> {
513    match v {
514        Some(s) => {
515            *slot = s.parse()?;
516            Ok(())
517        }
518        _ => Err(SmtSolver::ERROR),
519    }
520}
521
522fn parse_opt_path_buf(slot: &mut Option<PathBuf>, v: Option<&str>) -> Result<(), &'static str> {
523    match v {
524        Some(s) => {
525            *slot = Some(PathBuf::from(s));
526            Ok(())
527        }
528        None => Err("expected a path"),
529    }
530}
531
532fn parse_opt_level(slot: &mut Option<Level>, v: Option<&str>) -> Result<(), &'static str> {
533    match v {
534        Some(s) => {
535            *slot = Some(Level::from_str(s).map_err(|_| "invalid level")?);
536            Ok(())
537        }
538        None => Err("a level"),
539    }
540}
541
542fn parse_opt_include(slot: &mut Vec<String>, v: Option<&str>) -> Result<(), &'static str> {
543    if let Some(include) = v {
544        slot.push(include.to_string());
545    }
546    Ok(())
547}
flux_config/flags.rs

flux_config/
flags.rs
