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

flux_config/
lib.rs
