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.verbose
156}
157
158#[derive(Clone, Debug, Deserialize)]
159#[serde(try_from = "String")]
160pub struct Pos {
161    pub file: String,
162    pub line: usize,
163    pub column: usize,
164}
165
166impl FromStr for Pos {
167    type Err = &'static str;
168
169    fn from_str(s: &str) -> Result<Self, Self::Err> {
170        let s = s.trim();
171        let parts: Vec<&str> = s.split(':').collect();
172        if parts.len() != 3 {
173            return Err("span format should be '<file>:<line>:<column>'");
174        }
175        let file = parts[0].to_string();
176        let line = parts[1]
177            .parse::<usize>()
178            .map_err(|_| "invalid line number")?;
179        let column = parts[2]
180            .parse::<usize>()
181            .map_err(|_| "invalid column number")?;
182        Ok(Pos { file, line, column })
183    }
184}
185
186impl TryFrom<String> for Pos {
187    type Error = &'static str;
188
189    fn try_from(value: String) -> Result<Self, Self::Error> {
190        value.parse()
191    }
192}
193
194impl fmt::Display for IncludePattern {
195    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
196        write!(f, "[")?;
197        write!(f, "glob:{:?},", self.glob)?;
198        for def in &self.defs {
199            write!(f, "def:{},", def)?;
200        }
201        for pos in &self.spans {
202            write!(f, "span:{}:{}:{}", pos.file, pos.line, pos.column)?;
203        }
204        write!(f, "]")?;
205        Ok(())
206    }
207}
208/// This specifies which `DefId` should be checked. It can be specified via multiple patterns
209/// of the form `-Finclude=<pattern>` and the `DefId` is checked if it matches *any* of the patterns.
210/// Patterns are checked relative to the current working directory.
211#[derive(Clone)]
212pub struct IncludePattern {
213    /// files matching the glob pattern, e.g. `glob:src/ascii/*.rs` to check all files in the `ascii` module
214    pub glob: GlobSet,
215    /// defs (`fn`, `enum`, ...) matching the given function name as a substring, e.g. `def:watermelon`
216    pub defs: Vec<String>,
217    /// fn whose implementation overlaps the file, line, e.g. `span:tests/tests/pos/detached/detach00.rs:13:3`
218    pub spans: Vec<Pos>,
219}
220
221impl IncludePattern {
222    fn new(includes: Vec<String>) -> Result<Self, String> {
223        let mut defs = Vec::new();
224        let mut spans = Vec::new();
225        let mut glob = GlobSetBuilder::new();
226        for include in includes {
227            if let Some(suffix) = include.strip_prefix("def:") {
228                defs.push(suffix.to_string());
229            } else if let Some(suffix) = include.strip_prefix("span:") {
230                spans.push(Pos::from_str(suffix)?);
231            } else {
232                let suffix = include.strip_prefix("glob:").unwrap_or(&include);
233                let glob_pattern = Glob::new(suffix.trim()).map_err(|_| "invalid glob pattern")?;
234                glob.add(glob_pattern);
235            }
236        }
237        let glob = glob.build().map_err(|_| "failed to build glob set")?;
238        Ok(IncludePattern { glob, defs, spans })
239    }
240}
241
242#[derive(Clone, Copy, Debug, Deserialize, Default)]
243#[serde(try_from = "String")]
244pub enum LeanMode {
245    /// Don't do anything with lean
246    #[default]
247    Off,
248    /// Emit the lean definitions and VCs for externally proven items
249    Emit,
250    /// (Emit and) Check the lean definitions and VCs for externally proven items
251    Check,
252}
253
254impl LeanMode {
255    const ERROR: &'static str = "expected one of `emit`, or `check`";
256
257    pub fn is_emit(self) -> bool {
258        matches!(self, LeanMode::Emit)
259    }
260
261    pub fn is_check(self) -> bool {
262        matches!(self, LeanMode::Check)
263    }
264}
265
266impl FromStr for LeanMode {
267    type Err = &'static str;
268
269    fn from_str(s: &str) -> Result<Self, Self::Err> {
270        let s = s.to_ascii_lowercase();
271        match s.as_str() {
272            "off" => Ok(LeanMode::Off),
273            "emit" => Ok(LeanMode::Emit),
274            "check" => Ok(LeanMode::Check),
275            _ => Err(Self::ERROR),
276        }
277    }
278}
279
280impl TryFrom<String> for LeanMode {
281    type Error = &'static str;
282
283    fn try_from(value: String) -> Result<Self, Self::Error> {
284        value.parse()
285    }
286}
287
288impl fmt::Display for LeanMode {
289    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
290        match self {
291            LeanMode::Off => write!(f, "off"),
292            LeanMode::Emit => write!(f, "emit"),
293            LeanMode::Check => write!(f, "check"),
294        }
295    }
296}
297
298#[derive(Clone, Copy, Debug, Deserialize, Default)]
299#[serde(try_from = "String")]
300pub enum OverflowMode {
301    /// Strict-Underflow, No overflow checking
302    #[default]
303    None,
304    /// Lazy underflow, Lazy overflow checking; lose all information
305    /// unless values are known to be in valid range
306    Lazy,
307    /// Strict underflow, Lazy overflow checking; always check
308    /// unsignedness (non-negativity) but lazy for upper-bound
309    StrictUnder,
310    /// Strict underflow, Strict overflow checking; always check
311    /// values in valid range for type
312    Strict,
313}
314
315impl OverflowMode {
316    const ERROR: &'static str = "expected one of `none`, `lazy`, or `strict`";
317}
318impl FromStr for OverflowMode {
319    type Err = &'static str;
320
321    fn from_str(s: &str) -> Result<Self, Self::Err> {
322        let s = s.to_ascii_lowercase();
323        match s.as_str() {
324            "none" => Ok(OverflowMode::None),
325            "lazy" => Ok(OverflowMode::Lazy),
326            "strict" => Ok(OverflowMode::Strict),
327            "strict-under" => Ok(OverflowMode::StrictUnder),
328            _ => Err(Self::ERROR),
329        }
330    }
331}
332
333impl TryFrom<String> for OverflowMode {
334    type Error = &'static str;
335
336    fn try_from(value: String) -> Result<Self, Self::Error> {
337        value.parse()
338    }
339}
340
341impl fmt::Display for OverflowMode {
342    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
343        match self {
344            OverflowMode::None => write!(f, "none"),
345            OverflowMode::Lazy => write!(f, "lazy"),
346            OverflowMode::Strict => write!(f, "strict"),
347            OverflowMode::StrictUnder => write!(f, "strict-under"),
348        }
349    }
350}
351
352#[derive(Clone, Copy, Debug, Deserialize, Default)]
353#[serde(try_from = "String")]
354pub enum RawDerefMode {
355    /// Don't allow raw pointer dereferences (default)
356    #[default]
357    None,
358    /// Allow raw pointer dereferences
359    Ok,
360}
361
362impl RawDerefMode {
363    const ERROR: &'static str = "expected one of `none` or `ok`";
364}
365
366impl FromStr for RawDerefMode {
367    type Err = &'static str;
368
369    fn from_str(s: &str) -> Result<Self, Self::Err> {
370        let s = s.to_ascii_lowercase();
371        match s.as_str() {
372            "none" => Ok(RawDerefMode::None),
373            "ok" => Ok(RawDerefMode::Ok),
374            _ => Err(Self::ERROR),
375        }
376    }
377}
378
379impl TryFrom<String> for RawDerefMode {
380    type Error = &'static str;
381
382    fn try_from(value: String) -> Result<Self, Self::Error> {
383        value.parse()
384    }
385}
386
387impl fmt::Display for RawDerefMode {
388    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
389        match self {
390            RawDerefMode::None => write!(f, "none"),
391            RawDerefMode::Ok => write!(f, "ok"),
392        }
393    }
394}
395
396#[derive(Clone, Copy, Debug, Deserialize, Default)]
397#[serde(try_from = "String")]
398pub enum SmtSolver {
399    #[default]
400    Z3,
401    CVC5,
402}
403
404impl SmtSolver {
405    const ERROR: &'static str = "expected one of `z3` or `cvc5`";
406}
407
408impl FromStr for SmtSolver {
409    type Err = &'static str;
410
411    fn from_str(s: &str) -> Result<Self, Self::Err> {
412        let s = s.to_ascii_lowercase();
413        match s.as_str() {
414            "z3" => Ok(SmtSolver::Z3),
415            "cvc5" => Ok(SmtSolver::CVC5),
416            _ => Err(Self::ERROR),
417        }
418    }
419}
420
421impl TryFrom<String> for SmtSolver {
422    type Error = &'static str;
423
424    fn try_from(value: String) -> Result<Self, Self::Error> {
425        value.parse()
426    }
427}
428
429impl fmt::Display for SmtSolver {
430    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
431        match self {
432            SmtSolver::Z3 => write!(f, "z3"),
433            SmtSolver::CVC5 => write!(f, "cvc5"),
434        }
435    }
436}
437
438/// Options that change the behavior of refinement type inference locally
439#[derive(Clone, Copy, Debug)]
440pub struct InferOpts {
441    /// Enable overflow checking. This affects the signature of primitive operations and the
442    /// invariants assumed for primitive types.
443    pub check_overflow: OverflowMode,
444    /// Whether qualifiers should be scraped from the constraint.
445    pub scrape_quals: bool,
446    pub solver: SmtSolver,
447    /// Whether to allow uninterpreted casts (e.g., from some random `S` to `int`).
448    pub allow_uninterpreted_cast: bool,
449    /// Whether to allow raw pointer dereferences.
450    pub allow_raw_deref: RawDerefMode,
451}
452
453impl From<PartialInferOpts> for InferOpts {
454    fn from(opts: PartialInferOpts) -> Self {
455        InferOpts {
456            check_overflow: opts.check_overflow.unwrap_or_else(check_overflow),
457            scrape_quals: opts.scrape_quals.unwrap_or_else(scrape_quals),
458            solver: opts.solver.unwrap_or_else(solver),
459            allow_uninterpreted_cast: opts
460                .allow_uninterpreted_cast
461                .unwrap_or_else(allow_uninterpreted_cast),
462            allow_raw_deref: opts.allow_raw_deref.unwrap_or_else(allow_raw_deref),
463        }
464    }
465}
466
467#[derive(Clone, Copy, Default, Deserialize, Debug)]
468pub struct PartialInferOpts {
469    pub check_overflow: Option<OverflowMode>,
470    pub scrape_quals: Option<bool>,
471    pub solver: Option<SmtSolver>,
472    pub allow_uninterpreted_cast: Option<bool>,
473    pub allow_raw_deref: Option<RawDerefMode>,
474}
475
476impl PartialInferOpts {
477    pub fn merge(&mut self, other: &Self) {
478        self.check_overflow = self.check_overflow.or(other.check_overflow);
479        self.allow_uninterpreted_cast = self
480            .allow_uninterpreted_cast
481            .or(other.allow_uninterpreted_cast);
482        self.scrape_quals = self.scrape_quals.or(other.scrape_quals);
483        self.solver = self.solver.or(other.solver);
484        self.allow_raw_deref = self.allow_raw_deref.or(other.allow_raw_deref);
485    }
486}
487
488#[derive(Copy, Clone, Deserialize, Default)]
489pub enum PointerWidth {
490    W32,
491    #[default]
492    W64,
493}
494
495impl PointerWidth {
496    const ERROR: &str = "pointer width must be 32 or 64";
497
498    pub fn bits(self) -> u64 {
499        match self {
500            PointerWidth::W32 => 32,
501            PointerWidth::W64 => 64,
502        }
503    }
504}
505
506impl FromStr for PointerWidth {
507    type Err = &'static str;
508
509    fn from_str(s: &str) -> Result<Self, Self::Err> {
510        match s {
511            "32" => Ok(PointerWidth::W32),
512            "64" => Ok(PointerWidth::W64),
513            _ => Err(Self::ERROR),
514        }
515    }
516}
517
518fn config_path() -> Option<PathBuf> {
519    // find config file in current or parent directories
520    let mut path = std::env::current_dir().unwrap();
521    loop {
522        for name in ["flux.toml", ".flux.toml"] {
523            let file = path.join(name);
524            if file.exists() {
525                return Some(file);
526            }
527        }
528        if !path.pop() {
529            return None;
530        }
531    }
532}
533
534pub static CONFIG_FILE: LazyLock<Value> = LazyLock::new(|| {
535    if let Some(path) = config_path() {
536        let mut file = std::fs::File::open(path).unwrap();
537        let mut contents = String::new();
538        file.read_to_string(&mut contents).unwrap();
539        toml::from_str(&contents).unwrap()
540    } else {
541        toml::from_str("").unwrap()
542    }
543});
flux_config/lib.rs

flux_config/
lib.rs
