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

flux_config/
flags.rs
