flux_config/
lib.rs

1#![feature(if_let_guard)]
2use globset::{Glob, GlobSet, GlobSetBuilder};
3pub use toml::Value;
4use tracing::Level;
5pub mod flags;
6
7use std::{
8    fmt,
9    io::Read,
10    path::{Path, PathBuf},
11    str::FromStr,
12    sync::LazyLock,
13};
14
15use flags::FLAGS;
16use serde::Deserialize;
17
18pub fn dump_checker_trace_info() -> bool {
19    match FLAGS.dump_checker_trace {
20        Some(l) => Level::INFO <= l,
21        None => false,
22    }
23}
24
25pub fn dump_checker_trace() -> Option<Level> {
26    FLAGS.dump_checker_trace
27}
28
29pub fn dump_constraint() -> bool {
30    FLAGS.dump_constraint
31}
32
33pub fn dump_fhir() -> bool {
34    FLAGS.dump_fhir
35}
36
37pub fn dump_rty() -> bool {
38    FLAGS.dump_rty
39}
40
41pub fn pointer_width() -> PointerWidth {
42    FLAGS.pointer_width
43}
44
45pub fn log_dir() -> &'static PathBuf {
46    &FLAGS.log_dir
47}
48
49pub fn lean_dir() -> &'static PathBuf {
50    &FLAGS.lean_dir
51}
52
53pub fn lean_project() -> &'static str {
54    &FLAGS.lean_project
55}
56
57pub fn is_cache_enabled() -> bool {
58    FLAGS.cache.is_some()
59}
60
61pub fn trusted_default() -> bool {
62    FLAGS.trusted_default
63}
64
65pub fn ignore_default() -> bool {
66    FLAGS.ignore_default
67}
68
69pub fn lean() -> LeanMode {
70    FLAGS.lean
71}
72
73pub fn cache_path() -> Option<&'static Path> {
74    FLAGS.cache.as_deref()
75}
76
77pub fn include_pattern() -> Option<&'static IncludePattern> {
78    FLAGS.include.as_ref()
79}
80
81pub fn trusted_pattern() -> Option<&'static IncludePattern> {
82    FLAGS.include_trusted.as_ref()
83}
84
85pub fn trusted_impl_pattern() -> Option<&'static IncludePattern> {
86    FLAGS.include_trusted_impl.as_ref()
87}
88
89fn check_overflow() -> OverflowMode {
90    FLAGS.check_overflow
91}
92
93fn allow_raw_deref() -> RawDerefMode {
94    FLAGS.allow_raw_deref
95}
96
97pub fn allow_uninterpreted_cast() -> bool {
98    FLAGS.allow_uninterpreted_cast
99}
100
101fn scrape_quals() -> bool {
102    FLAGS.scrape_quals
103}
104
105pub fn no_panic() -> bool {
106    FLAGS.no_panic
107}
108
109pub fn sysroot() -> Option<PathBuf> {
110    if let Some(p) = FLAGS.sysroot.as_deref() {
111        Some(p.to_path_buf())
112    } else {
113        let exe = std::env::current_exe().ok()?;
114        exe.parent().map(|p| p.to_path_buf())
115    }
116}
117
118pub fn smt_define_fun() -> bool {
119    FLAGS.smt_define_fun
120}
121
122fn solver() -> SmtSolver {
123    FLAGS.solver
124}
125
126pub fn catch_bugs() -> bool {
127    FLAGS.catch_bugs
128}
129
130pub fn annots() -> bool {
131    FLAGS.annots
132}
133
134pub fn timings() -> bool {
135    FLAGS.timings
136}
137
138pub fn verify() -> bool {
139    FLAGS.verify
140}
141
142pub fn summary() -> bool {
143    FLAGS.summary
144}
145
146pub fn full_compilation() -> bool {
147    FLAGS.full_compilation
148}
149
150pub fn std_extern_specs() -> bool {
151    FLAGS.std_extern_specs
152}
153
154pub fn verbose() -> bool {
155    FLAGS.flux_verbose
156}
157
158pub fn no_suggestions_default() -> bool {
159    FLAGS.no_suggestions_default
160}
161
162pub fn rerun_hint() -> bool {
163    FLAGS.rerun_hint
164}
165
166/// Whether the driver is running under `cargo flux` (which sets `FLUX_CARGO=1`), as opposed to a
167/// direct `flux`/`flux-driver` invocation. Used to decide whether to emit the re-run hint.
168pub fn inside_cargo() -> bool {
169    std::env::var_os("FLUX_CARGO").is_some()
170}
171
172#[derive(Clone, Debug, Deserialize)]
173#[serde(try_from = "String")]
174pub struct Pos {
175    pub file: String,
176    pub line: usize,
177    pub column: usize,
178}
179
180impl FromStr for Pos {
181    type Err = &'static str;
182
183    fn from_str(s: &str) -> Result<Self, Self::Err> {
184        let s = s.trim();
185        let parts: Vec<&str> = s.split(':').collect();
186        if parts.len() != 3 {
187            return Err("span format should be '<file>:<line>:<column>'");
188        }
189        let file = parts[0].to_string();
190        let line = parts[1]
191            .parse::<usize>()
192            .map_err(|_| "invalid line number")?;
193        let column = parts[2]
194            .parse::<usize>()
195            .map_err(|_| "invalid column number")?;
196        Ok(Pos { file, line, column })
197    }
198}
199
200impl TryFrom<String> for Pos {
201    type Error = &'static str;
202
203    fn try_from(value: String) -> Result<Self, Self::Error> {
204        value.parse()
205    }
206}
207
208impl fmt::Display for IncludePattern {
209    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
210        write!(f, "[")?;
211        write!(f, "glob:{:?},", self.glob)?;
212        for def in &self.defs {
213            write!(f, "def:{},", def)?;
214        }
215        for pos in &self.spans {
216            write!(f, "span:{}:{}:{}", pos.file, pos.line, pos.column)?;
217        }
218        write!(f, "]")?;
219        Ok(())
220    }
221}
222/// This specifies which `DefId` should be checked. It can be specified via multiple patterns
223/// of the form `-Finclude=<pattern>` and the `DefId` is checked if it matches *any* of the patterns.
224/// Patterns are checked relative to the current working directory.
225#[derive(Clone)]
226pub struct IncludePattern {
227    /// files matching the glob pattern, e.g. `glob:src/ascii/*.rs` to check all files in the `ascii` module
228    pub glob: GlobSet,
229    /// defs (`fn`, `enum`, ...) matching the given function name as a substring, e.g. `def:watermelon`
230    pub defs: Vec<String>,
231    /// fn whose implementation overlaps the file, line, e.g. `span:tests/tests/pos/detached/detach00.rs:13:3`
232    pub spans: Vec<Pos>,
233}
234
235impl IncludePattern {
236    fn new(includes: Vec<String>) -> Result<Self, String> {
237        let mut defs = Vec::new();
238        let mut spans = Vec::new();
239        let mut glob = GlobSetBuilder::new();
240        for include in includes {
241            if let Some(suffix) = include.strip_prefix("def:") {
242                defs.push(suffix.to_string());
243            } else if let Some(suffix) = include.strip_prefix("span:") {
244                spans.push(Pos::from_str(suffix)?);
245            } else {
246                let suffix = include.strip_prefix("glob:").unwrap_or(&include);
247                let glob_pattern = Glob::new(suffix.trim()).map_err(|_| "invalid glob pattern")?;
248                glob.add(glob_pattern);
249            }
250        }
251        let glob = glob.build().map_err(|_| "failed to build glob set")?;
252        Ok(IncludePattern { glob, defs, spans })
253    }
254}
255
256#[derive(Clone, Copy, Debug, Deserialize, Default)]
257#[serde(try_from = "String")]
258pub enum LeanMode {
259    /// Don't do anything with lean
260    #[default]
261    Off,
262    /// Emit the lean definitions and VCs for externally proven items
263    Emit,
264    /// (Emit and) Check the lean definitions and VCs for externally proven items
265    Check,
266}
267
268impl LeanMode {
269    const ERROR: &'static str = "expected one of `emit`, or `check`";
270
271    pub fn is_emit(self) -> bool {
272        matches!(self, LeanMode::Emit)
273    }
274
275    pub fn is_check(self) -> bool {
276        matches!(self, LeanMode::Check)
277    }
278}
279
280impl FromStr for LeanMode {
281    type Err = &'static str;
282
283    fn from_str(s: &str) -> Result<Self, Self::Err> {
284        let s = s.to_ascii_lowercase();
285        match s.as_str() {
286            "off" => Ok(LeanMode::Off),
287            "emit" => Ok(LeanMode::Emit),
288            "check" => Ok(LeanMode::Check),
289            _ => Err(Self::ERROR),
290        }
291    }
292}
293
294impl TryFrom<String> for LeanMode {
295    type Error = &'static str;
296
297    fn try_from(value: String) -> Result<Self, Self::Error> {
298        value.parse()
299    }
300}
301
302impl fmt::Display for LeanMode {
303    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
304        match self {
305            LeanMode::Off => write!(f, "off"),
306            LeanMode::Emit => write!(f, "emit"),
307            LeanMode::Check => write!(f, "check"),
308        }
309    }
310}
311
312#[derive(Clone, Copy, Debug, Deserialize, Default)]
313#[serde(try_from = "String")]
314pub enum OverflowMode {
315    /// Strict-Underflow, No overflow checking
316    #[default]
317    None,
318    /// Lazy underflow, Lazy overflow checking; lose all information
319    /// unless values are known to be in valid range
320    Lazy,
321    /// Strict underflow, Lazy overflow checking; always check
322    /// unsignedness (non-negativity) but lazy for upper-bound
323    StrictUnder,
324    /// Strict underflow, Strict overflow checking; always check
325    /// values in valid range for type
326    Strict,
327}
328
329impl OverflowMode {
330    const ERROR: &'static str = "expected one of `none`, `lazy`, or `strict`";
331}
332impl FromStr for OverflowMode {
333    type Err = &'static str;
334
335    fn from_str(s: &str) -> Result<Self, Self::Err> {
336        let s = s.to_ascii_lowercase();
337        match s.as_str() {
338            "none" => Ok(OverflowMode::None),
339            "lazy" => Ok(OverflowMode::Lazy),
340            "strict" => Ok(OverflowMode::Strict),
341            "strict-under" => Ok(OverflowMode::StrictUnder),
342            _ => Err(Self::ERROR),
343        }
344    }
345}
346
347impl TryFrom<String> for OverflowMode {
348    type Error = &'static str;
349
350    fn try_from(value: String) -> Result<Self, Self::Error> {
351        value.parse()
352    }
353}
354
355impl fmt::Display for OverflowMode {
356    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
357        match self {
358            OverflowMode::None => write!(f, "none"),
359            OverflowMode::Lazy => write!(f, "lazy"),
360            OverflowMode::Strict => write!(f, "strict"),
361            OverflowMode::StrictUnder => write!(f, "strict-under"),
362        }
363    }
364}
365
366#[derive(Clone, Copy, Debug, Deserialize, Default)]
367#[serde(try_from = "String")]
368pub enum RawDerefMode {
369    /// Don't allow raw pointer dereferences (default)
370    #[default]
371    None,
372    /// Allow raw pointer dereferences
373    Ok,
374}
375
376impl RawDerefMode {
377    const ERROR: &'static str = "expected one of `none` or `ok`";
378}
379
380impl FromStr for RawDerefMode {
381    type Err = &'static str;
382
383    fn from_str(s: &str) -> Result<Self, Self::Err> {
384        let s = s.to_ascii_lowercase();
385        match s.as_str() {
386            "none" => Ok(RawDerefMode::None),
387            "ok" => Ok(RawDerefMode::Ok),
388            _ => Err(Self::ERROR),
389        }
390    }
391}
392
393impl TryFrom<String> for RawDerefMode {
394    type Error = &'static str;
395
396    fn try_from(value: String) -> Result<Self, Self::Error> {
397        value.parse()
398    }
399}
400
401impl fmt::Display for RawDerefMode {
402    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
403        match self {
404            RawDerefMode::None => write!(f, "none"),
405            RawDerefMode::Ok => write!(f, "ok"),
406        }
407    }
408}
409
410#[derive(Clone, Copy, Debug, Deserialize, Default)]
411#[serde(try_from = "String")]
412pub enum SmtSolver {
413    #[default]
414    Z3,
415    CVC5,
416}
417
418impl SmtSolver {
419    const ERROR: &'static str = "expected one of `z3` or `cvc5`";
420}
421
422impl FromStr for SmtSolver {
423    type Err = &'static str;
424
425    fn from_str(s: &str) -> Result<Self, Self::Err> {
426        let s = s.to_ascii_lowercase();
427        match s.as_str() {
428            "z3" => Ok(SmtSolver::Z3),
429            "cvc5" => Ok(SmtSolver::CVC5),
430            _ => Err(Self::ERROR),
431        }
432    }
433}
434
435impl TryFrom<String> for SmtSolver {
436    type Error = &'static str;
437
438    fn try_from(value: String) -> Result<Self, Self::Error> {
439        value.parse()
440    }
441}
442
443impl fmt::Display for SmtSolver {
444    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
445        match self {
446            SmtSolver::Z3 => write!(f, "z3"),
447            SmtSolver::CVC5 => write!(f, "cvc5"),
448        }
449    }
450}
451
452/// Options that change the behavior of refinement type inference locally
453#[derive(Clone, Copy, Debug)]
454pub struct InferOpts {
455    /// Enable overflow checking. This affects the signature of primitive operations and the
456    /// invariants assumed for primitive types.
457    pub check_overflow: OverflowMode,
458    /// Whether qualifiers should be scraped from the constraint.
459    pub scrape_quals: bool,
460    pub solver: SmtSolver,
461    /// Whether to allow uninterpreted casts (e.g., from some random `S` to `int`).
462    pub allow_uninterpreted_cast: bool,
463    /// Whether to allow raw pointer dereferences.
464    pub allow_raw_deref: RawDerefMode,
465}
466
467impl From<PartialInferOpts> for InferOpts {
468    fn from(opts: PartialInferOpts) -> Self {
469        InferOpts {
470            check_overflow: opts.check_overflow.unwrap_or_else(check_overflow),
471            scrape_quals: opts.scrape_quals.unwrap_or_else(scrape_quals),
472            solver: opts.solver.unwrap_or_else(solver),
473            allow_uninterpreted_cast: opts
474                .allow_uninterpreted_cast
475                .unwrap_or_else(allow_uninterpreted_cast),
476            allow_raw_deref: opts.allow_raw_deref.unwrap_or_else(allow_raw_deref),
477        }
478    }
479}
480
481#[derive(Clone, Copy, Default, Deserialize, Debug)]
482pub struct PartialInferOpts {
483    pub check_overflow: Option<OverflowMode>,
484    pub scrape_quals: Option<bool>,
485    pub solver: Option<SmtSolver>,
486    pub allow_uninterpreted_cast: Option<bool>,
487    pub allow_raw_deref: Option<RawDerefMode>,
488}
489
490impl PartialInferOpts {
491    pub fn merge(&mut self, other: &Self) {
492        self.check_overflow = self.check_overflow.or(other.check_overflow);
493        self.allow_uninterpreted_cast = self
494            .allow_uninterpreted_cast
495            .or(other.allow_uninterpreted_cast);
496        self.scrape_quals = self.scrape_quals.or(other.scrape_quals);
497        self.solver = self.solver.or(other.solver);
498        self.allow_raw_deref = self.allow_raw_deref.or(other.allow_raw_deref);
499    }
500}
501
502#[derive(Copy, Clone, Deserialize, Default)]
503pub enum PointerWidth {
504    W32,
505    #[default]
506    W64,
507}
508
509impl PointerWidth {
510    const ERROR: &str = "pointer width must be 32 or 64";
511
512    pub fn bits(self) -> u64 {
513        match self {
514            PointerWidth::W32 => 32,
515            PointerWidth::W64 => 64,
516        }
517    }
518}
519
520impl FromStr for PointerWidth {
521    type Err = &'static str;
522
523    fn from_str(s: &str) -> Result<Self, Self::Err> {
524        match s {
525            "32" => Ok(PointerWidth::W32),
526            "64" => Ok(PointerWidth::W64),
527            _ => Err(Self::ERROR),
528        }
529    }
530}
531
532fn config_path() -> Option<PathBuf> {
533    // find config file in current or parent directories
534    let mut path = std::env::current_dir().unwrap();
535    loop {
536        for name in ["flux.toml", ".flux.toml"] {
537            let file = path.join(name);
538            if file.exists() {
539                return Some(file);
540            }
541        }
542        if !path.pop() {
543            return None;
544        }
545    }
546}
547
548pub static CONFIG_FILE: LazyLock<Value> = LazyLock::new(|| {
549    if let Some(path) = config_path() {
550        let mut file = std::fs::File::open(path).unwrap();
551        let mut contents = String::new();
552        file.read_to_string(&mut contents).unwrap();
553        toml::from_str(&contents).unwrap()
554    } else {
555        toml::from_str("").unwrap()
556    }
557});
flux_config/lib.rs

flux_config/
lib.rs
