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

flux_config/
lib.rs
