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

flux_config/
lib.rs
