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: &Path) -> bool {
61    if let Some(globset) = &FLAGS.include { globset.is_match(file) } else { true }
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
72pub fn allow_uninterpreted_cast() -> bool {
73    FLAGS.allow_uninterpreted_cast
74}
75
76fn scrape_quals() -> bool {
77    FLAGS.scrape_quals
78}
79
80pub fn smt_define_fun() -> bool {
81    FLAGS.smt_define_fun
82}
83
84pub fn verbose() -> bool {
85    FLAGS.verbose
86}
87
88fn solver() -> SmtSolver {
89    FLAGS.solver
90}
91
92pub fn catch_bugs() -> bool {
93    FLAGS.catch_bugs
94}
95
96pub fn annots() -> bool {
97    FLAGS.annots
98}
99
100pub fn timings() -> bool {
101    FLAGS.timings
102}
103
104pub fn verify() -> bool {
105    FLAGS.verify
106}
107
108pub fn full_compilation() -> bool {
109    FLAGS.full_compilation
110}
111
112#[derive(Clone, Copy, Debug, Deserialize, Default)]
113#[serde(try_from = "String")]
114pub enum SmtSolver {
115    #[default]
116    Z3,
117    CVC5,
118}
119
120impl SmtSolver {
121    const ERROR: &'static str = "expected one of `z3` or `cvc5`";
122}
123
124impl FromStr for SmtSolver {
125    type Err = &'static str;
126
127    fn from_str(s: &str) -> Result<Self, Self::Err> {
128        let s = s.to_ascii_lowercase();
129        match s.as_str() {
130            "z3" => Ok(SmtSolver::Z3),
131            "cvc5" => Ok(SmtSolver::CVC5),
132            _ => Err(Self::ERROR),
133        }
134    }
135}
136
137impl TryFrom<String> for SmtSolver {
138    type Error = &'static str;
139
140    fn try_from(value: String) -> Result<Self, Self::Error> {
141        value.parse()
142    }
143}
144
145impl fmt::Display for SmtSolver {
146    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
147        match self {
148            SmtSolver::Z3 => write!(f, "z3"),
149            SmtSolver::CVC5 => write!(f, "cvc5"),
150        }
151    }
152}
153
154/// Options that change the behavior of refinement type inference locally
155#[derive(Clone, Copy, Debug)]
156pub struct InferOpts {
157    /// Enable overflow checking. This affects the signature of primitive operations and the
158    /// invariants assumed for primitive types.
159    pub check_overflow: bool,
160    /// Whether qualifiers should be scraped from the constraint.
161    pub scrape_quals: bool,
162    pub solver: SmtSolver,
163    /// Whether to allow uninterpreted casts (e.g., from some random `S` to `int`).
164    pub allow_uninterpreted_cast: bool,
165}
166
167impl From<PartialInferOpts> for InferOpts {
168    fn from(opts: PartialInferOpts) -> Self {
169        InferOpts {
170            check_overflow: opts.check_overflow.unwrap_or_else(check_overflow),
171            scrape_quals: opts.scrape_quals.unwrap_or_else(scrape_quals),
172            solver: opts.solver.unwrap_or_else(solver),
173            allow_uninterpreted_cast: opts
174                .allow_uninterpreted_cast
175                .unwrap_or_else(allow_uninterpreted_cast),
176        }
177    }
178}
179
180#[derive(Clone, Copy, Default, Deserialize, Debug)]
181pub struct PartialInferOpts {
182    pub check_overflow: Option<bool>,
183    pub scrape_quals: Option<bool>,
184    pub solver: Option<SmtSolver>,
185    pub allow_uninterpreted_cast: Option<bool>,
186}
187
188impl PartialInferOpts {
189    pub fn merge(&mut self, other: &Self) {
190        self.check_overflow = self.check_overflow.or(other.check_overflow);
191        self.allow_uninterpreted_cast = self
192            .allow_uninterpreted_cast
193            .or(other.allow_uninterpreted_cast);
194        self.scrape_quals = self.scrape_quals.or(other.scrape_quals);
195        self.solver = self.solver.or(other.solver);
196    }
197}
198
199#[derive(Copy, Clone, Deserialize, Default)]
200pub enum PointerWidth {
201    W32,
202    #[default]
203    W64,
204}
205
206impl PointerWidth {
207    const ERROR: &str = "pointer width must be 32 or 64";
208
209    pub fn bits(self) -> u64 {
210        match self {
211            PointerWidth::W32 => 32,
212            PointerWidth::W64 => 64,
213        }
214    }
215}
216
217impl FromStr for PointerWidth {
218    type Err = &'static str;
219
220    fn from_str(s: &str) -> Result<Self, Self::Err> {
221        match s {
222            "32" => Ok(PointerWidth::W32),
223            "64" => Ok(PointerWidth::W64),
224            _ => Err(Self::ERROR),
225        }
226    }
227}
228
229fn config_path() -> Option<PathBuf> {
230    // find config file in current or parent directories
231    let mut path = std::env::current_dir().unwrap();
232    loop {
233        for name in ["flux.toml", ".flux.toml"] {
234            let file = path.join(name);
235            if file.exists() {
236                return Some(file);
237            }
238        }
239        if !path.pop() {
240            return None;
241        }
242    }
243}
244
245pub static CONFIG_FILE: LazyLock<Value> = LazyLock::new(|| {
246    if let Some(path) = config_path() {
247        let mut file = std::fs::File::open(path).unwrap();
248        let mut contents = String::new();
249        file.read_to_string(&mut contents).unwrap();
250        toml::from_str(&contents).unwrap()
251    } else {
252        toml::from_str("").unwrap()
253    }
254});
flux_config/lib.rs

flux_config/
lib.rs
