flux_config/
lib.rs

1#![feature(if_let_guard)]
2pub use toml::Value;
3pub mod flags;
4
5use std::{
6    fmt,
7    io::Read,
8    path::{Path, PathBuf},
9    str::FromStr,
10    sync::LazyLock,
11};
12
13use flags::FLAGS;
14use serde::Deserialize;
15
16pub fn check_def() -> &'static str {
17    &FLAGS.check_def
18}
19
20pub fn dump_checker_trace() -> bool {
21    FLAGS.dump_checker_trace
22}
23
24pub fn dump_mir() -> bool {
25    FLAGS.dump_mir
26}
27
28pub fn dump_constraint() -> bool {
29    FLAGS.dump_constraint
30}
31
32pub fn dump_fhir() -> bool {
33    FLAGS.dump_fhir
34}
35
36pub fn dump_rty() -> bool {
37    FLAGS.dump_rty
38}
39
40pub fn pointer_width() -> PointerWidth {
41    FLAGS.pointer_width
42}
43
44pub fn log_dir() -> &'static PathBuf {
45    &FLAGS.log_dir
46}
47
48pub fn is_cache_enabled() -> bool {
49    FLAGS.cache.is_some()
50}
51
52pub fn trusted_default() -> bool {
53    FLAGS.trusted_default
54}
55
56pub fn ignore_default() -> bool {
57    FLAGS.ignore_default
58}
59
60pub fn is_checked_file(file: &str) -> bool {
61    FLAGS.check_files.is_checked_file(file)
62}
63
64pub fn cache_path() -> Option<&'static Path> {
65    FLAGS.cache.as_deref()
66}
67
68fn check_overflow() -> bool {
69    FLAGS.check_overflow
70}
71
72fn scrape_quals() -> bool {
73    FLAGS.scrape_quals
74}
75
76pub fn smt_define_fun() -> bool {
77    FLAGS.smt_define_fun
78}
79
80pub fn verbose() -> bool {
81    FLAGS.verbose
82}
83
84fn solver() -> SmtSolver {
85    FLAGS.solver
86}
87
88pub fn catch_bugs() -> bool {
89    FLAGS.catch_bugs
90}
91
92pub fn annots() -> bool {
93    FLAGS.annots
94}
95
96pub fn timings() -> bool {
97    FLAGS.timings
98}
99
100pub fn verify() -> bool {
101    FLAGS.verify
102}
103
104pub fn full_compilation() -> bool {
105    FLAGS.full_compilation
106}
107
108#[derive(Clone, Copy, Debug, Deserialize, Default)]
109#[serde(try_from = "String")]
110pub enum SmtSolver {
111    #[default]
112    Z3,
113    CVC5,
114}
115
116impl SmtSolver {
117    const ERROR: &'static str = "expected one of `z3` or `cvc5`";
118}
119
120impl FromStr for SmtSolver {
121    type Err = &'static str;
122
123    fn from_str(s: &str) -> Result<Self, Self::Err> {
124        let s = s.to_ascii_lowercase();
125        match s.as_str() {
126            "z3" => Ok(SmtSolver::Z3),
127            "cvc5" => Ok(SmtSolver::CVC5),
128            _ => Err(Self::ERROR),
129        }
130    }
131}
132
133impl TryFrom<String> for SmtSolver {
134    type Error = &'static str;
135
136    fn try_from(value: String) -> Result<Self, Self::Error> {
137        value.parse()
138    }
139}
140
141impl fmt::Display for SmtSolver {
142    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
143        match self {
144            SmtSolver::Z3 => write!(f, "z3"),
145            SmtSolver::CVC5 => write!(f, "cvc5"),
146        }
147    }
148}
149
150/// Options that change the behavior of refinement type inference locally
151#[derive(Clone, Copy, Debug)]
152pub struct InferOpts {
153    /// Enable overflow checking. This affects the signature of primitive operations and the
154    /// invariants assumed for primitive types.
155    pub check_overflow: bool,
156    /// Whether qualifiers should be scraped from the constraint.
157    pub scrape_quals: bool,
158    pub solver: SmtSolver,
159}
160
161impl From<PartialInferOpts> for InferOpts {
162    fn from(opts: PartialInferOpts) -> Self {
163        InferOpts {
164            check_overflow: opts.check_overflow.unwrap_or_else(check_overflow),
165            scrape_quals: opts.scrape_quals.unwrap_or_else(scrape_quals),
166            solver: opts.solver.unwrap_or_else(solver),
167        }
168    }
169}
170
171#[derive(Clone, Copy, Default, Deserialize, Debug)]
172pub struct PartialInferOpts {
173    pub check_overflow: Option<bool>,
174    pub scrape_quals: Option<bool>,
175    pub solver: Option<SmtSolver>,
176}
177
178impl PartialInferOpts {
179    pub fn merge(&mut self, other: &Self) {
180        self.check_overflow = self.check_overflow.or(other.check_overflow);
181        self.scrape_quals = self.scrape_quals.or(other.scrape_quals);
182        self.solver = self.solver.or(other.solver);
183    }
184}
185
186#[derive(Copy, Clone, Deserialize, Default)]
187pub enum PointerWidth {
188    W32,
189    #[default]
190    W64,
191}
192
193impl PointerWidth {
194    const ERROR: &str = "pointer width must be 32 or 64";
195
196    pub fn bits(self) -> u64 {
197        match self {
198            PointerWidth::W32 => 32,
199            PointerWidth::W64 => 64,
200        }
201    }
202}
203
204impl FromStr for PointerWidth {
205    type Err = &'static str;
206
207    fn from_str(s: &str) -> Result<Self, Self::Err> {
208        match s {
209            "32" => Ok(PointerWidth::W32),
210            "64" => Ok(PointerWidth::W64),
211            _ => Err(Self::ERROR),
212        }
213    }
214}
215
216fn config_path() -> Option<PathBuf> {
217    // find config file in current or parent directories
218    let mut path = std::env::current_dir().unwrap();
219    loop {
220        for name in ["flux.toml", ".flux.toml"] {
221            let file = path.join(name);
222            if file.exists() {
223                return Some(file);
224            }
225        }
226        if !path.pop() {
227            return None;
228        }
229    }
230}
231
232pub static CONFIG_FILE: LazyLock<Value> = LazyLock::new(|| {
233    if let Some(path) = config_path() {
234        let mut file = std::fs::File::open(path).unwrap();
235        let mut contents = String::new();
236        file.read_to_string(&mut contents).unwrap();
237        toml::from_str(&contents).unwrap()
238    } else {
239        toml::from_str("").unwrap()
240    }
241});
flux_config/lib.rs

flux_config/
lib.rs
