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

flux_config/
lib.rs
