flux_config/
lib.rs

1use globset::{Glob, GlobSet, GlobSetBuilder};
2pub use toml::Value;
3use tracing::Level;
4pub mod flags;
5
6use std::{
7    fmt,
8    io::Read,
9    path::{Path, PathBuf},
10    str::FromStr,
11    sync::LazyLock,
12    time::Duration,
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 uif_ops() -> UifOps {
94    FLAGS.uif_ops
95}
96
97fn allow_raw_deref() -> RawDerefMode {
98    FLAGS.allow_raw_deref
99}
100
101pub fn allow_uninterpreted_cast() -> bool {
102    FLAGS.allow_uninterpreted_cast
103}
104
105fn scrape_quals() -> bool {
106    FLAGS.scrape_quals
107}
108
109pub fn no_panic() -> bool {
110    FLAGS.no_panic
111}
112
113pub fn sysroot() -> Option<PathBuf> {
114    if let Some(p) = FLAGS.sysroot.as_deref() {
115        Some(p.to_path_buf())
116    } else {
117        let exe = std::env::current_exe().ok()?;
118        exe.parent().map(|p| p.to_path_buf())
119    }
120}
121
122fn solver() -> SmtSolver {
123    FLAGS.solver
124}
125
126pub fn catch_bugs() -> bool {
127    FLAGS.catch_bugs
128}
129
130pub fn annots() -> bool {
131    FLAGS.annots
132}
133
134pub fn timings() -> bool {
135    FLAGS.timings
136}
137
138pub fn verify() -> bool {
139    FLAGS.verify
140}
141
142pub fn summary() -> bool {
143    FLAGS.summary
144}
145
146pub fn full_compilation() -> bool {
147    FLAGS.full_compilation
148}
149
150pub fn std_extern_specs() -> bool {
151    FLAGS.std_extern_specs
152}
153
154pub fn verbose() -> bool {
155    FLAGS.flux_verbose
156}
157
158pub fn no_suggestions_default() -> bool {
159    FLAGS.no_suggestions_default
160}
161
162pub fn rerun_hint() -> bool {
163    FLAGS.rerun_hint
164}
165
166pub fn fixpoint_timeout() -> Option<Duration> {
167    FLAGS.fixpoint_timeout.map(Duration::from_secs)
168}
169
170/// Whether the driver is running under `cargo flux` (which sets `FLUX_CARGO=1`), as opposed to a
171/// direct `flux`/`flux-driver` invocation. Used to decide whether to emit the re-run hint.
172pub fn inside_cargo() -> bool {
173    std::env::var_os("FLUX_CARGO").is_some()
174}
175
176#[derive(Clone, Debug, Deserialize)]
177#[serde(try_from = "String")]
178pub struct Pos {
179    pub file: String,
180    pub line: usize,
181    pub column: usize,
182}
183
184impl FromStr for Pos {
185    type Err = &'static str;
186
187    fn from_str(s: &str) -> Result<Self, Self::Err> {
188        let s = s.trim();
189        let parts: Vec<&str> = s.split(':').collect();
190        if parts.len() != 3 {
191            return Err("span format should be '<file>:<line>:<column>'");
192        }
193        let file = parts[0].to_string();
194        let line = parts[1]
195            .parse::<usize>()
196            .map_err(|_| "invalid line number")?;
197        let column = parts[2]
198            .parse::<usize>()
199            .map_err(|_| "invalid column number")?;
200        Ok(Pos { file, line, column })
201    }
202}
203
204impl TryFrom<String> for Pos {
205    type Error = &'static str;
206
207    fn try_from(value: String) -> Result<Self, Self::Error> {
208        value.parse()
209    }
210}
211
212impl fmt::Display for IncludePattern {
213    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
214        write!(f, "[")?;
215        write!(f, "glob:{:?},", self.glob)?;
216        for def in &self.defs {
217            write!(f, "def:{},", def)?;
218        }
219        for pos in &self.spans {
220            write!(f, "span:{}:{}:{}", pos.file, pos.line, pos.column)?;
221        }
222        write!(f, "]")?;
223        Ok(())
224    }
225}
226/// This specifies which `DefId` should be checked. It can be specified via multiple patterns
227/// of the form `-Finclude=<pattern>` and the `DefId` is checked if it matches *any* of the patterns.
228/// Patterns are checked relative to the current working directory.
229#[derive(Clone)]
230pub struct IncludePattern {
231    /// files matching the glob pattern, e.g. `glob:src/ascii/*.rs` to check all files in the `ascii` module
232    pub glob: GlobSet,
233    /// defs (`fn`, `enum`, ...) matching the given function name as a substring, e.g. `def:watermelon`
234    pub defs: Vec<String>,
235    /// fn whose implementation overlaps the file, line, e.g. `span:tests/tests/pos/detached/detach00.rs:13:3`
236    pub spans: Vec<Pos>,
237}
238
239impl IncludePattern {
240    fn new(includes: Vec<String>) -> Result<Self, String> {
241        let mut defs = Vec::new();
242        let mut spans = Vec::new();
243        let mut glob = GlobSetBuilder::new();
244        for include in includes {
245            if let Some(suffix) = include.strip_prefix("def:") {
246                defs.push(suffix.to_string());
247            } else if let Some(suffix) = include.strip_prefix("span:") {
248                spans.push(Pos::from_str(suffix)?);
249            } else {
250                let suffix = include.strip_prefix("glob:").unwrap_or(&include);
251                let glob_pattern = Glob::new(suffix.trim()).map_err(|_| "invalid glob pattern")?;
252                glob.add(glob_pattern);
253            }
254        }
255        let glob = glob.build().map_err(|_| "failed to build glob set")?;
256        Ok(IncludePattern { glob, defs, spans })
257    }
258}
259
260impl FromStr for IncludePattern {
261    type Err = String;
262
263    fn from_str(s: &str) -> Result<Self, Self::Err> {
264        Self::new(vec![s.to_string()])
265    }
266}
267
268#[derive(Clone, Copy, Debug, Deserialize, Default)]
269#[serde(try_from = "String")]
270pub enum LeanMode {
271    /// Don't do anything with lean
272    #[default]
273    Off,
274    /// Emit the lean definitions and VCs for externally proven items
275    Emit,
276    /// (Emit and) Check the lean definitions and VCs for externally proven items
277    Check,
278}
279
280impl LeanMode {
281    const ERROR: &'static str = "expected one of `emit`, or `check`";
282
283    pub fn is_emit(self) -> bool {
284        matches!(self, LeanMode::Emit)
285    }
286
287    pub fn is_check(self) -> bool {
288        matches!(self, LeanMode::Check)
289    }
290}
291
292impl FromStr for LeanMode {
293    type Err = &'static str;
294
295    fn from_str(s: &str) -> Result<Self, Self::Err> {
296        let s = s.to_ascii_lowercase();
297        match s.as_str() {
298            "off" => Ok(LeanMode::Off),
299            "emit" => Ok(LeanMode::Emit),
300            "check" => Ok(LeanMode::Check),
301            _ => Err(Self::ERROR),
302        }
303    }
304}
305
306impl TryFrom<String> for LeanMode {
307    type Error = &'static str;
308
309    fn try_from(value: String) -> Result<Self, Self::Error> {
310        value.parse()
311    }
312}
313
314impl fmt::Display for LeanMode {
315    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
316        match self {
317            LeanMode::Off => write!(f, "off"),
318            LeanMode::Emit => write!(f, "emit"),
319            LeanMode::Check => write!(f, "check"),
320        }
321    }
322}
323
324/// A binary operator that can be encoded as an uninterpreted function, see [`InferOpts::uif_ops`].
325/// These mirror the arithmetic and bitwise operators of the surface syntax.
326#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
327pub enum UifOp {
328    Add,
329    Sub,
330    Mul,
331    Div,
332    Mod,
333    BitAnd,
334    BitOr,
335    BitXor,
336    BitShl,
337    BitShr,
338}
339
340impl UifOp {
341    /// Maps the surface syntax (token) of each operator to the operator.
342    const TOKENS: [(&'static str, UifOp); 10] = [
343        ("+", UifOp::Add),
344        ("-", UifOp::Sub),
345        ("*", UifOp::Mul),
346        ("/", UifOp::Div),
347        ("%", UifOp::Mod),
348        ("&", UifOp::BitAnd),
349        ("|", UifOp::BitOr),
350        ("^", UifOp::BitXor),
351        ("<<", UifOp::BitShl),
352        (">>", UifOp::BitShr),
353    ];
354
355    /// The operator written as `token` in the surface syntax, if any
356    pub fn from_token(token: &str) -> Option<UifOp> {
357        Self::TOKENS
358            .iter()
359            .find_map(|(tok, op)| (*tok == token).then_some(*op))
360    }
361
362    /// The surface syntax of the operator
363    fn token(self) -> &'static str {
364        match self {
365            UifOp::Add => "+",
366            UifOp::Sub => "-",
367            UifOp::Mul => "*",
368            UifOp::Div => "/",
369            UifOp::Mod => "%",
370            UifOp::BitAnd => "&",
371            UifOp::BitOr => "|",
372            UifOp::BitXor => "^",
373            UifOp::BitShl => "<<",
374            UifOp::BitShr => ">>",
375        }
376    }
377
378    fn bit(self) -> u16 {
379        1 << (self as u16)
380    }
381}
382
383/// A set of [`UifOp`]s. It is a bitset so [`InferOpts`] can be `Copy`. It is written as a comma
384/// separated list of operators, e.g., `*,/,%`.
385#[derive(Clone, Copy, PartialEq, Eq, Default, Deserialize)]
386#[serde(try_from = "String")]
387pub struct UifOps(u16);
388
389impl UifOps {
390    const ERROR: &'static str =
391        "expected a comma separated list of `+`, `-`, `*`, `/`, `%`, `&`, `|`, `^`, `<<`, or `>>`";
392
393    pub fn contains(self, op: UifOp) -> bool {
394        self.0 & op.bit() != 0
395    }
396
397    pub fn is_empty(self) -> bool {
398        self.0 == 0
399    }
400
401    pub fn insert(&mut self, op: UifOp) {
402        self.0 |= op.bit();
403    }
404
405    fn iter(self) -> impl Iterator<Item = UifOp> {
406        UifOp::TOKENS
407            .into_iter()
408            .map(|(_, op)| op)
409            .filter(move |op| self.contains(*op))
410    }
411}
412
413impl FromStr for UifOps {
414    type Err = &'static str;
415
416    fn from_str(s: &str) -> Result<Self, Self::Err> {
417        let mut ops = UifOps::default();
418        let tokens = s
419            .split(',')
420            .map(str::trim)
421            .filter(|token| !token.is_empty());
422        for token in tokens {
423            let op = UifOp::from_token(token).ok_or(Self::ERROR)?;
424            ops.insert(op);
425        }
426        Ok(ops)
427    }
428}
429
430impl TryFrom<String> for UifOps {
431    type Error = &'static str;
432
433    fn try_from(value: String) -> Result<Self, Self::Error> {
434        value.parse()
435    }
436}
437
438impl fmt::Display for UifOps {
439    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
440        let tokens: Vec<_> = self.iter().map(UifOp::token).collect();
441        write!(f, "{}", tokens.join(","))
442    }
443}
444
445impl fmt::Debug for UifOps {
446    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
447        write!(f, "UifOps({self})")
448    }
449}
450
451#[derive(Clone, Copy, Debug, Deserialize, Default)]
452#[serde(try_from = "String")]
453pub enum OverflowMode {
454    /// Strict-Underflow, No overflow checking
455    #[default]
456    None,
457    /// Lazy underflow, Lazy overflow checking; lose all information
458    /// unless values are known to be in valid range
459    Lazy,
460    /// Strict underflow, Lazy overflow checking; always check
461    /// unsignedness (non-negativity) but lazy for upper-bound
462    StrictUnder,
463    /// Strict underflow, Strict overflow checking; always check
464    /// values in valid range for type
465    Strict,
466}
467
468impl OverflowMode {
469    const ERROR: &'static str = "expected one of `none`, `lazy`, or `strict`";
470}
471impl FromStr for OverflowMode {
472    type Err = &'static str;
473
474    fn from_str(s: &str) -> Result<Self, Self::Err> {
475        let s = s.to_ascii_lowercase();
476        match s.as_str() {
477            "none" => Ok(OverflowMode::None),
478            "lazy" => Ok(OverflowMode::Lazy),
479            "strict" => Ok(OverflowMode::Strict),
480            "strict-under" => Ok(OverflowMode::StrictUnder),
481            _ => Err(Self::ERROR),
482        }
483    }
484}
485
486impl TryFrom<String> for OverflowMode {
487    type Error = &'static str;
488
489    fn try_from(value: String) -> Result<Self, Self::Error> {
490        value.parse()
491    }
492}
493
494impl fmt::Display for OverflowMode {
495    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
496        match self {
497            OverflowMode::None => write!(f, "none"),
498            OverflowMode::Lazy => write!(f, "lazy"),
499            OverflowMode::Strict => write!(f, "strict"),
500            OverflowMode::StrictUnder => write!(f, "strict-under"),
501        }
502    }
503}
504
505#[derive(Clone, Copy, Debug, Deserialize, Default)]
506#[serde(try_from = "String")]
507pub enum RawDerefMode {
508    /// Don't allow raw pointer dereferences (default)
509    #[default]
510    None,
511    /// Allow raw pointer dereferences
512    Ok,
513}
514
515impl RawDerefMode {
516    const ERROR: &'static str = "expected one of `none` or `ok`";
517}
518
519impl FromStr for RawDerefMode {
520    type Err = &'static str;
521
522    fn from_str(s: &str) -> Result<Self, Self::Err> {
523        let s = s.to_ascii_lowercase();
524        match s.as_str() {
525            "none" => Ok(RawDerefMode::None),
526            "ok" => Ok(RawDerefMode::Ok),
527            _ => Err(Self::ERROR),
528        }
529    }
530}
531
532impl TryFrom<String> for RawDerefMode {
533    type Error = &'static str;
534
535    fn try_from(value: String) -> Result<Self, Self::Error> {
536        value.parse()
537    }
538}
539
540impl fmt::Display for RawDerefMode {
541    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
542        match self {
543            RawDerefMode::None => write!(f, "none"),
544            RawDerefMode::Ok => write!(f, "ok"),
545        }
546    }
547}
548
549#[derive(Clone, Copy, Debug, Deserialize, Default)]
550#[serde(try_from = "String")]
551pub enum SmtSolver {
552    #[default]
553    Z3,
554    CVC5,
555}
556
557impl SmtSolver {
558    const ERROR: &'static str = "expected one of `z3` or `cvc5`";
559}
560
561impl FromStr for SmtSolver {
562    type Err = &'static str;
563
564    fn from_str(s: &str) -> Result<Self, Self::Err> {
565        let s = s.to_ascii_lowercase();
566        match s.as_str() {
567            "z3" => Ok(SmtSolver::Z3),
568            "cvc5" => Ok(SmtSolver::CVC5),
569            _ => Err(Self::ERROR),
570        }
571    }
572}
573
574impl TryFrom<String> for SmtSolver {
575    type Error = &'static str;
576
577    fn try_from(value: String) -> Result<Self, Self::Error> {
578        value.parse()
579    }
580}
581
582impl fmt::Display for SmtSolver {
583    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
584        match self {
585            SmtSolver::Z3 => write!(f, "z3"),
586            SmtSolver::CVC5 => write!(f, "cvc5"),
587        }
588    }
589}
590
591/// Options that change the behavior of refinement type inference locally
592#[derive(Clone, Copy, Debug)]
593pub struct InferOpts {
594    /// Enable overflow checking. This affects the signature of primitive operations and the
595    /// invariants assumed for primitive types.
596    pub check_overflow: OverflowMode,
597    /// Whether qualifiers should be scraped from the constraint.
598    pub scrape_quals: bool,
599    pub solver: SmtSolver,
600    /// Whether to allow uninterpreted casts (e.g., from some random `S` to `int`).
601    pub allow_uninterpreted_cast: bool,
602    /// Whether to allow raw pointer dereferences.
603    pub allow_raw_deref: RawDerefMode,
604    /// Binary operators that are encoded as uninterpreted functions (e.g. to avoid nonlinear arithmetic).
605    pub uif_ops: UifOps,
606}
607
608impl From<PartialInferOpts> for InferOpts {
609    fn from(opts: PartialInferOpts) -> Self {
610        InferOpts {
611            check_overflow: opts.check_overflow.unwrap_or_else(check_overflow),
612            scrape_quals: opts.scrape_quals.unwrap_or_else(scrape_quals),
613            solver: opts.solver.unwrap_or_else(solver),
614            allow_uninterpreted_cast: opts
615                .allow_uninterpreted_cast
616                .unwrap_or_else(allow_uninterpreted_cast),
617            allow_raw_deref: opts.allow_raw_deref.unwrap_or_else(allow_raw_deref),
618            uif_ops: opts.uif_ops.unwrap_or_else(uif_ops),
619        }
620    }
621}
622
623#[derive(Clone, Copy, Default, Deserialize, Debug)]
624pub struct PartialInferOpts {
625    pub check_overflow: Option<OverflowMode>,
626    pub scrape_quals: Option<bool>,
627    pub solver: Option<SmtSolver>,
628    pub allow_uninterpreted_cast: Option<bool>,
629    pub allow_raw_deref: Option<RawDerefMode>,
630    pub uif_ops: Option<UifOps>,
631}
632
633impl PartialInferOpts {
634    pub fn merge(&mut self, other: &Self) {
635        self.check_overflow = self.check_overflow.or(other.check_overflow);
636        self.allow_uninterpreted_cast = self
637            .allow_uninterpreted_cast
638            .or(other.allow_uninterpreted_cast);
639        self.scrape_quals = self.scrape_quals.or(other.scrape_quals);
640        self.solver = self.solver.or(other.solver);
641        self.allow_raw_deref = self.allow_raw_deref.or(other.allow_raw_deref);
642        self.uif_ops = self.uif_ops.or(other.uif_ops);
643    }
644}
645
646#[derive(Copy, Clone, Deserialize, Default)]
647pub enum PointerWidth {
648    W32,
649    #[default]
650    W64,
651}
652
653impl PointerWidth {
654    const ERROR: &str = "pointer width must be 32 or 64";
655
656    pub fn bits(self) -> u64 {
657        match self {
658            PointerWidth::W32 => 32,
659            PointerWidth::W64 => 64,
660        }
661    }
662}
663
664impl FromStr for PointerWidth {
665    type Err = &'static str;
666
667    fn from_str(s: &str) -> Result<Self, Self::Err> {
668        match s {
669            "32" => Ok(PointerWidth::W32),
670            "64" => Ok(PointerWidth::W64),
671            _ => Err(Self::ERROR),
672        }
673    }
674}
675
676fn config_path() -> Option<PathBuf> {
677    // find config file in current or parent directories
678    let mut path = std::env::current_dir().unwrap();
679    loop {
680        for name in ["flux.toml", ".flux.toml"] {
681            let file = path.join(name);
682            if file.exists() {
683                return Some(file);
684            }
685        }
686        if !path.pop() {
687            return None;
688        }
689    }
690}
691
692pub static CONFIG_FILE: LazyLock<Value> = LazyLock::new(|| {
693    if let Some(path) = config_path() {
694        let mut file = std::fs::File::open(path).unwrap();
695        let mut contents = String::new();
696        file.read_to_string(&mut contents).unwrap();
697        toml::from_str(&contents).unwrap()
698    } else {
699        toml::from_str("").unwrap()
700    }
701});
flux_config/lib.rs

flux_config/
lib.rs
