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

flux_config/
lib.rs
