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

flux_config/
lib.rs
