flux_config/
flags.rs

1use std::{env, path::PathBuf, process, sync::LazyLock};
2
3use globset::{Glob, GlobSet, GlobSetBuilder};
4use serde::Deserialize;
5pub use toml::Value;
6
7use crate::{PointerWidth, SmtSolver};
8
9const FLUX_FLAG_PREFIX: &str = "-F";
10
11/// Exit status code used for invalid flags.
12pub const EXIT_FAILURE: i32 = 2;
13
14pub struct Flags {
15    /// Sets the directory to dump data. Defaults to `./log/`.
16    pub log_dir: PathBuf,
17    /// Only checks definitions containing `name` as a substring
18    pub check_def: String,
19    /// If present, only check files matching a glob pattern. This flag can be specified multiple
20    /// times and a file will be checked if it matches any of the patterns. Patterns are checked
21    /// relative to the current working directory. For example, to check all the files in the
22    /// `ascii` module of a crate, you can `include` the pattern `"src/ascii/*"` (assuming that's
23    /// where the files are located).
24    pub include: Option<GlobSet>,
25    /// Set the pointer size (either `32` or `64`), used to determine if an integer cast is lossy
26    /// (default `64`).
27    pub pointer_width: PointerWidth,
28    /// If present switches on query caching and saves the cache in the provided path
29    pub cache: Option<PathBuf>,
30    pub verbose: bool,
31    /// Compute statistics about number and size of annotations. Dumps file to [`Self.log_dir`]
32    pub annots: bool,
33    /// Print statistics about time taked to analyze each fuction. Also dumps a file with the raw
34    /// times for each function.
35    pub timings: bool,
36    /// Default solver. Either `z3` or `cvc5`.
37    pub solver: SmtSolver,
38    /// Enables qualifier scrapping in fixpoint
39    pub scrape_quals: 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 true checks for over and underflow on arithmetic integer operations, default `false`. When
44    /// set to `false`, it still checks for underflow on unsigned integer subtraction.
45    pub check_overflow: bool,
46    /// Dump constraints generated for each function (debugging)
47    pub dump_constraint: bool,
48    /// Saves the checker's trace (debugging)
49    pub dump_checker_trace: bool,
50    /// Saves the `fhir` for each item (debugging)
51    pub dump_fhir: bool,
52    /// Saves the the `fhir` (debugging)
53    pub dump_rty: bool,
54    /// Saves the low-level MIR for each analyzed function (debugging)
55    pub dump_mir: bool,
56    /// Saves the low-level MIR for each analyzed function (debugging)
57    pub catch_bugs: bool,
58    /// Whether verification for the current crate is enabled. If false (the default), `flux-driver`
59    /// will behave exactly like `rustc`. This flag is managed by the `cargo flux` and `flux` binaries,
60    /// so you don't need to mess with it.
61    pub verify: bool,
62    /// If `true`, produce artifacts after analysis. This flag is managed by `cargo flux`, so you
63    /// don't typically have to set it manually.
64    pub full_compilation: bool,
65    /// 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.
66    pub trusted_default: bool,
67    /// 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.
68    pub ignore_default: bool,
69}
70
71impl Default for Flags {
72    fn default() -> Self {
73        Self {
74            log_dir: PathBuf::from("./log/"),
75            dump_constraint: false,
76            dump_checker_trace: false,
77            dump_fhir: false,
78            dump_rty: false,
79            dump_mir: false,
80            catch_bugs: false,
81            pointer_width: PointerWidth::default(),
82            check_def: String::new(),
83            include: None,
84            cache: None,
85            check_overflow: false,
86            scrape_quals: false,
87            solver: SmtSolver::default(),
88            smt_define_fun: false,
89            verbose: false,
90            annots: false,
91            timings: false,
92            verify: false,
93            full_compilation: false,
94            trusted_default: false,
95            ignore_default: false,
96        }
97    }
98}
99
100pub(crate) static FLAGS: LazyLock<Flags> = LazyLock::new(|| {
101    let mut flags = Flags::default();
102    let mut include: Option<GlobSetBuilder> = None;
103    for arg in env::args() {
104        let Some((key, value)) = parse_flux_arg(&arg) else { continue };
105
106        let result = match key {
107            "log-dir" => parse_path_buf(&mut flags.log_dir, value),
108            "dump-constraint" => parse_bool(&mut flags.dump_constraint, value),
109            "dump-checker-trace" => parse_bool(&mut flags.dump_checker_trace, value),
110            "dump-mir" => parse_bool(&mut flags.dump_mir, value),
111            "dump-fhir" => parse_bool(&mut flags.dump_fhir, value),
112            "dump-rty" => parse_bool(&mut flags.dump_rty, value),
113            "catch-bugs" => parse_bool(&mut flags.catch_bugs, value),
114            "pointer-width" => parse_pointer_width(&mut flags.pointer_width, value),
115            "check-overflow" => parse_bool(&mut flags.check_overflow, value),
116            "scrape-quals" => parse_bool(&mut flags.scrape_quals, value),
117            "solver" => parse_solver(&mut flags.solver, value),
118            "verbose" => parse_bool(&mut flags.verbose, value),
119            "smt-define-fun" => parse_bool(&mut flags.smt_define_fun, value),
120            "annots" => parse_bool(&mut flags.annots, value),
121            "timings" => parse_bool(&mut flags.timings, value),
122            "cache" => parse_opt_path_buf(&mut flags.cache, value),
123            "check-def" => parse_string(&mut flags.check_def, value),
124            "include" => parse_include(&mut include, value),
125            "verify" => parse_bool(&mut flags.verify, value),
126            "full-compilation" => parse_bool(&mut flags.full_compilation, value),
127            "trusted" => parse_bool(&mut flags.trusted_default, value),
128            "ignore" => parse_bool(&mut flags.ignore_default, value),
129            _ => {
130                eprintln!("error: unknown flux option: `{key}`");
131                process::exit(EXIT_FAILURE);
132            }
133        };
134        if let Err(reason) = result {
135            eprintln!("error: incorrect value for flux option `{key}` - `{reason}`");
136            process::exit(1);
137        }
138    }
139    if let Some(include) = include {
140        let include = include.build().unwrap_or_else(|err| {
141            eprintln!("error: invalid include pattern: {err:?}");
142            process::exit(1);
143        });
144        flags.include = Some(include);
145    }
146    flags
147});
148
149#[derive(Default)]
150pub struct Paths {
151    paths: Option<Vec<PathBuf>>,
152}
153
154impl Paths {
155    pub fn is_checked_file(&self, file: &str) -> bool {
156        self.paths
157            .as_ref()
158            .is_none_or(|p| p.iter().any(|p| p.to_str().unwrap() == file))
159    }
160}
161
162impl<'de> Deserialize<'de> for Paths {
163    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
164    where
165        D: serde::Deserializer<'de>,
166    {
167        let paths: Vec<PathBuf> = String::deserialize(deserializer)?
168            .split(",")
169            .map(str::trim)
170            .filter(|s| !s.is_empty())
171            .map(PathBuf::from)
172            .collect();
173
174        let paths = if paths.is_empty() { None } else { Some(paths) };
175
176        Ok(Paths { paths })
177    }
178}
179
180pub fn is_flux_arg(arg: &str) -> bool {
181    parse_flux_arg(arg).is_some()
182}
183
184fn parse_flux_arg(arg: &str) -> Option<(&str, Option<&str>)> {
185    let arg = arg.strip_prefix(FLUX_FLAG_PREFIX)?;
186    if arg.is_empty() {
187        return None;
188    }
189    if let Some((k, v)) = arg.split_once('=') { Some((k, Some(v))) } else { Some((arg, None)) }
190}
191
192fn parse_bool(slot: &mut bool, v: Option<&str>) -> Result<(), &'static str> {
193    match v {
194        Some("y") | Some("yes") | Some("on") | Some("true") | None => {
195            *slot = true;
196            Ok(())
197        }
198        Some("n") | Some("no") | Some("off") | Some("false") => {
199            *slot = false;
200            Ok(())
201        }
202        _ => {
203            Err(
204                "expected no value or one of `y`, `yes`, `on`, `true`, `n`, `no`, `off`, or `false`",
205            )
206        }
207    }
208}
209
210fn parse_path_buf(slot: &mut PathBuf, v: Option<&str>) -> Result<(), &'static str> {
211    match v {
212        Some(s) => {
213            *slot = PathBuf::from(s);
214            Ok(())
215        }
216        None => Err("a path"),
217    }
218}
219
220fn parse_pointer_width(slot: &mut PointerWidth, v: Option<&str>) -> Result<(), &'static str> {
221    match v {
222        Some(s) => {
223            *slot = s.parse()?;
224            Ok(())
225        }
226        _ => Err(PointerWidth::ERROR),
227    }
228}
229
230fn parse_solver(slot: &mut SmtSolver, v: Option<&str>) -> Result<(), &'static str> {
231    match v {
232        Some(s) => {
233            *slot = s.parse()?;
234            Ok(())
235        }
236        _ => Err(SmtSolver::ERROR),
237    }
238}
239
240fn parse_opt_path_buf(slot: &mut Option<PathBuf>, v: Option<&str>) -> Result<(), &'static str> {
241    match v {
242        Some(s) => {
243            *slot = Some(PathBuf::from(s));
244            Ok(())
245        }
246        None => Err("a path"),
247    }
248}
249
250fn parse_string(slot: &mut String, v: Option<&str>) -> Result<(), &'static str> {
251    match v {
252        Some(s) => {
253            *slot = s.to_string();
254            Ok(())
255        }
256        None => Err("a string"),
257    }
258}
259
260fn parse_include(slot: &mut Option<GlobSetBuilder>, v: Option<&str>) -> Result<(), &'static str> {
261    match v {
262        Some(s) => {
263            slot.get_or_insert_with(GlobSetBuilder::new)
264                .add(Glob::new(s.trim()).map_err(|_| "invalid glob pattern")?);
265            Ok(())
266        }
267        None => Err("a comma separated list of paths"),
268    }
269}
flux_config/flags.rs

flux_config/
flags.rs
