flux_config/
flags.rs

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

flux_config/
flags.rs
