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

flux_config/
lib.rs
