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 directory.
63    #[arg(long = flux_arg!("cache"), value_name = "DIR")]
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    /// Enable the refinement suggestion engine. Items can opt out with `#[flux::no_suggestions]`.
223    #[arg(
224        long = flux_arg!("suggestions"),
225        num_args = 0..=1,
226        default_value_t = false,
227        default_missing_value = "true"
228    )]
229    pub suggestions: bool,
230    /// If `true` (the default), attach a note to each failing item with a copy-pasteable command to
231    /// re-run the check on just that item. Only applies when running under `cargo flux`.
232    #[arg(
233        long = flux_arg!("rerun-hint"),
234        num_args = 0..=1,
235        default_value = "true",
236        default_missing_value = "true"
237    )]
238    pub rerun_hint: bool,
239}
240
241impl Default for Flags {
242    fn default() -> Self {
243        Self {
244            log_dir: PathBuf::from("./log/"),
245            lean_dir: PathBuf::from("./"),
246            lean_project: "lean_proofs".to_string(),
247            dump_constraint: false,
248            dump_checker_trace: None,
249            dump_fhir: false,
250            dump_rty: false,
251            catch_bugs: false,
252            pointer_width: PointerWidth::default(),
253            include: None,
254            include_trusted: None,
255            include_trusted_impl: None,
256            cache: None,
257            check_overflow: OverflowMode::default(),
258            allow_raw_deref: RawDerefMode::default(),
259            uif_ops: UifOps::default(),
260            scrape_quals: false,
261            fixpoint_timeout: None,
262            allow_uninterpreted_cast: false,
263            solver: SmtSolver::default(),
264            annots: false,
265            timings: false,
266            summary: true,
267            verify: false,
268            full_compilation: false,
269            sysroot: None,
270            trusted_default: false,
271            ignore_default: false,
272            lean: LeanMode::default(),
273            no_panic: false,
274            std_extern_specs: false,
275            flux_verbose: false,
276            suggestions: false,
277            rerun_hint: true,
278        }
279    }
280}
281
282impl Flags {
283    // Convert this struct into what we'd need to pass in through the environment var
284    pub fn rustflags(matches: &ArgMatches) -> Vec<String> {
285        let spec = Flags::augment_args(Command::new("flux-flags"));
286        let mut out = Vec::new();
287        for arg in spec.get_arguments() {
288            let id = arg.get_id().as_str();
289            if matches.value_source(id) != Some(ValueSource::CommandLine) {
290                continue;
291            }
292            let Some(long) = arg.get_long() else { continue };
293            match matches.get_raw(id) {
294                Some(values) => {
295                    out.extend(values.map(|v| format!("-{long}={}", v.to_string_lossy())));
296                }
297                None => out.push(format!("-{long}")),
298            }
299        }
300        out
301    }
302}
303
304#[derive(Clone, Debug, Default)]
305pub struct FluxFlags(pub Vec<String>);
306
307impl FromArgMatches for FluxFlags {
308    fn from_arg_matches(m: &ArgMatches) -> Result<Self, clap::Error> {
309        Ok(FluxFlags(Flags::rustflags(m)))
310    }
311    fn update_from_arg_matches(&mut self, m: &ArgMatches) -> Result<(), clap::Error> {
312        self.0 = Flags::rustflags(m);
313        Ok(())
314    }
315}
316
317impl Args for FluxFlags {
318    fn augment_args(cmd: Command) -> Command {
319        Flags::augment_args(cmd)
320    }
321    fn augment_args_for_update(cmd: Command) -> Command {
322        Flags::augment_args_for_update(cmd)
323    }
324}
325
326pub(crate) static FLAGS: LazyLock<Flags> = LazyLock::new(|| {
327    let mut flags = Flags::default();
328    let mut includes: Vec<String> = Vec::new();
329    let mut trusteds: Vec<String> = Vec::new();
330    let mut trusted_impls: Vec<String> = Vec::new();
331    for arg in env::args() {
332        let Some((key, value)) = parse_flux_arg(&arg) else { continue };
333
334        let result = match key {
335            "log-dir" => parse_path_buf(&mut flags.log_dir, value),
336            "lean-dir" => parse_path_buf(&mut flags.lean_dir, value),
337            "lean-project" => parse_string(&mut flags.lean_project, value),
338            "dump-constraint" => parse_bool(&mut flags.dump_constraint, value),
339            "dump-checker-trace" => parse_opt_level(&mut flags.dump_checker_trace, value),
340            "dump-fhir" => parse_bool(&mut flags.dump_fhir, value),
341            "dump-rty" => parse_bool(&mut flags.dump_rty, value),
342            "catch-bugs" => parse_bool(&mut flags.catch_bugs, value),
343            "pointer-width" => parse_pointer_width(&mut flags.pointer_width, value),
344            "check-overflow" => parse_overflow(&mut flags.check_overflow, value),
345            "allow-raw-deref" => parse_raw_deref(&mut flags.allow_raw_deref, value),
346            "uif-ops" => parse_uif_ops(&mut flags.uif_ops, value),
347            "scrape-quals" => parse_bool(&mut flags.scrape_quals, value),
348            "fixpoint-timeout" => parse_opt_u64(&mut flags.fixpoint_timeout, value),
349            "allow-uninterpreted-cast" => parse_bool(&mut flags.allow_uninterpreted_cast, value),
350            "solver" => parse_solver(&mut flags.solver, value),
351            "annots" => parse_bool(&mut flags.annots, value),
352            "timings" => parse_bool(&mut flags.timings, value),
353            "summary" => parse_bool(&mut flags.summary, value),
354            "cache" => parse_opt_path_buf(&mut flags.cache, value),
355            "include" => parse_opt_include(&mut includes, value),
356            "include-trusted" => parse_opt_include(&mut trusteds, value),
357            "include-trusted-impl" => parse_opt_include(&mut trusted_impls, value),
358            "verify" => parse_bool(&mut flags.verify, value),
359            "full-compilation" => parse_bool(&mut flags.full_compilation, value),
360            "sysroot" => parse_opt_path_buf(&mut flags.sysroot, value),
361            "trusted" => parse_bool(&mut flags.trusted_default, value),
362            "ignore" => parse_bool(&mut flags.ignore_default, value),
363            "lean" => parse_lean_mode(&mut flags.lean, value),
364            "no-panic" => parse_bool(&mut flags.no_panic, value),
365            "std-extern-specs" => parse_bool(&mut flags.std_extern_specs, value),
366            "flux-verbose" => parse_bool(&mut flags.flux_verbose, value),
367            "suggestions" => parse_bool(&mut flags.suggestions, value),
368            "rerun-hint" => parse_bool(&mut flags.rerun_hint, value),
369            _ => {
370                eprintln!("error: unknown flux option: `{key}`");
371                process::exit(EXIT_FAILURE);
372            }
373        };
374        if let Err(reason) = result {
375            eprintln!("error: incorrect value for flux option `{key}` - `{reason}`");
376            process::exit(1);
377        }
378    }
379    if !includes.is_empty() {
380        let include = IncludePattern::new(includes).unwrap_or_else(|err| {
381            eprintln!("error: invalid include pattern: {err}");
382            process::exit(1);
383        });
384        flags.include = Some(include);
385    }
386    if !trusteds.is_empty() {
387        let trusted = IncludePattern::new(trusteds).unwrap_or_else(|err| {
388            eprintln!("error: invalid trusted pattern: {err}");
389            process::exit(1);
390        });
391        flags.include_trusted = Some(trusted);
392    }
393    if !trusted_impls.is_empty() {
394        let trusted_impl = IncludePattern::new(trusted_impls).unwrap_or_else(|err| {
395            eprintln!("error: invalid trusted-impl pattern: {err}");
396            process::exit(1);
397        });
398        flags.include_trusted_impl = Some(trusted_impl);
399    }
400    flags
401});
402
403pub fn is_flux_arg(arg: &str) -> bool {
404    parse_flux_arg(arg).is_some()
405}
406
407fn parse_flux_arg(arg: &str) -> Option<(&str, Option<&str>)> {
408    let arg = arg.strip_prefix(FLUX_FLAG_PREFIX)?;
409    if arg.is_empty() {
410        return None;
411    }
412    if let Some((k, v)) = arg.split_once('=') { Some((k, Some(v))) } else { Some((arg, None)) }
413}
414
415fn parse_bool(slot: &mut bool, v: Option<&str>) -> Result<(), &'static str> {
416    match v {
417        Some("y") | Some("yes") | Some("on") | Some("true") | None => {
418            *slot = true;
419            Ok(())
420        }
421        Some("n") | Some("no") | Some("off") | Some("false") => {
422            *slot = false;
423            Ok(())
424        }
425        _ => {
426            Err(
427                "expected no value or one of `y`, `yes`, `on`, `true`, `n`, `no`, `off`, or `false`",
428            )
429        }
430    }
431}
432
433fn parse_string(slot: &mut String, v: Option<&str>) -> Result<(), &'static str> {
434    match v {
435        Some(s) => {
436            *slot = s.to_string();
437            Ok(())
438        }
439        None => Err("expected a string"),
440    }
441}
442
443fn parse_opt_u64(slot: &mut Option<u64>, v: Option<&str>) -> Result<(), &'static str> {
444    match v.and_then(|s| s.parse().ok()) {
445        Some(n) => {
446            *slot = Some(n);
447            Ok(())
448        }
449        None => Err("expected a non-negative integer"),
450    }
451}
452
453fn parse_path_buf(slot: &mut PathBuf, v: Option<&str>) -> Result<(), &'static str> {
454    match v {
455        Some(s) => {
456            *slot = PathBuf::from(s);
457            Ok(())
458        }
459        None => Err("expected a path"),
460    }
461}
462
463fn parse_pointer_width(slot: &mut PointerWidth, v: Option<&str>) -> Result<(), &'static str> {
464    match v {
465        Some(s) => {
466            *slot = s.parse()?;
467            Ok(())
468        }
469        _ => Err(PointerWidth::ERROR),
470    }
471}
472
473fn parse_lean_mode(slot: &mut LeanMode, v: Option<&str>) -> Result<(), &'static str> {
474    match v {
475        Some(s) => {
476            *slot = s.parse()?;
477            Ok(())
478        }
479        _ => Err(LeanMode::ERROR),
480    }
481}
482
483fn parse_overflow(slot: &mut OverflowMode, v: Option<&str>) -> Result<(), &'static str> {
484    match v {
485        Some(s) => {
486            *slot = s.parse()?;
487            Ok(())
488        }
489        _ => Err(OverflowMode::ERROR),
490    }
491}
492
493fn parse_uif_ops(slot: &mut UifOps, v: Option<&str>) -> Result<(), &'static str> {
494    match v {
495        Some(s) => {
496            *slot = s.parse()?;
497            Ok(())
498        }
499        _ => Err(UifOps::ERROR),
500    }
501}
502
503fn parse_raw_deref(slot: &mut RawDerefMode, v: Option<&str>) -> Result<(), &'static str> {
504    match v {
505        Some(s) => {
506            *slot = s.parse()?;
507            Ok(())
508        }
509        _ => Err(RawDerefMode::ERROR),
510    }
511}
512
513fn parse_solver(slot: &mut SmtSolver, v: Option<&str>) -> Result<(), &'static str> {
514    match v {
515        Some(s) => {
516            *slot = s.parse()?;
517            Ok(())
518        }
519        _ => Err(SmtSolver::ERROR),
520    }
521}
522
523fn parse_opt_path_buf(slot: &mut Option<PathBuf>, v: Option<&str>) -> Result<(), &'static str> {
524    match v {
525        Some(s) => {
526            *slot = Some(PathBuf::from(s));
527            Ok(())
528        }
529        None => Err("expected a path"),
530    }
531}
532
533fn parse_opt_level(slot: &mut Option<Level>, v: Option<&str>) -> Result<(), &'static str> {
534    match v {
535        Some(s) => {
536            *slot = Some(Level::from_str(s).map_err(|_| "invalid level")?);
537            Ok(())
538        }
539        None => Err("a level"),
540    }
541}
542
543fn parse_opt_include(slot: &mut Vec<String>, v: Option<&str>) -> Result<(), &'static str> {
544    if let Some(include) = v {
545        slot.push(include.to_string());
546    }
547    Ok(())
548}
flux_config/flags.rs

flux_config/
flags.rs
