flux_bin/
lib.rs

1use cargo_metadata::camino::Utf8Path;
2use flux_config::{LeanMode, OverflowMode, SmtSolver};
3use serde::Deserialize;
4
5pub mod cargo_flux_opts;
6pub mod cargo_style;
7pub mod utils;
8
9#[derive(Deserialize, Debug, Default)]
10#[serde(default, deny_unknown_fields)]
11pub struct FluxMetadata {
12    pub enabled: bool,
13    /// Enables fixpoint query caching. Saves cache in `target/FLUXCACHE`
14    pub cache: Option<bool>,
15    /// Set the default solver
16    pub solver: Option<SmtSolver>,
17    /// Enable qualifier scrapping in fixpoint
18    pub scrape_quals: Option<bool>,
19    /// Enable overflow checking
20    pub check_overflow: Option<OverflowMode>,
21    /// Enable uninterpreted casts
22    pub allow_uninterpreted_cast: Option<bool>,
23    /// Enable flux-defs to be defined as SMT functions
24    pub smt_define_fun: Option<bool>,
25    /// Set trusted to trusted
26    pub default_trusted: Option<bool>,
27    /// Set trusted to ignore
28    pub default_ignore: Option<bool>,
29    /// If present, only check files that match any of the glob patterns. Patterns are checked
30    /// relative to the location of the manifest file.
31    pub include: Option<Vec<String>>,
32    /// If present, every function in the module is implicitly labeled with a `no_panic` by default.
33    /// This means that the only way a function can panic is if it calls an external function without this attribute.
34    pub no_panic: Option<bool>,
35    /// If present, enables lean mode
36    pub lean: Option<LeanMode>,
37    /// If present, dumps the fixpoint constraint to a file
38    pub dump_constraint: Option<bool>,
39}
40
41impl FluxMetadata {
42    pub fn into_flags(
43        self,
44        target_dir: &Utf8Path,
45        inlude_pattern_prefix: Option<&Utf8Path>,
46    ) -> Vec<String> {
47        let mut flags = vec![];
48        if let Some(true) = self.cache {
49            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
50        }
51        if let Some(v) = self.solver {
52            flags.push(format!("-Fsolver={v}"));
53        }
54        if let Some(v) = self.check_overflow {
55            flags.push(format!("-Fcheck-overflow={v}"));
56        }
57        if let Some(v) = self.lean {
58            flags.push(format!("-Flean={v}"));
59        }
60        if let Some(v) = self.dump_constraint {
61            flags.push(format!("-Fdump-constraint={v}"));
62        }
63        if let Some(v) = self.scrape_quals {
64            flags.push(format!("-Fscrape-quals={v}"));
65        }
66        if let Some(v) = self.smt_define_fun {
67            flags.push(format!("-Fsmt-define-fun={v}"));
68        }
69        if let Some(v) = self.default_trusted {
70            flags.push(format!("-Ftrusted={v}"));
71        }
72        if let Some(v) = self.no_panic {
73            flags.push(format!("-Fno-panic={v}"));
74        }
75        if let Some(v) = self.default_ignore {
76            flags.push(format!("-Fignore={v}"));
77        }
78        if let Some(v) = self.allow_uninterpreted_cast {
79            flags.push(format!("-Fallow-uninterpreted-cast={v}"));
80        }
81        if let Some(patterns) = self.include {
82            for pat in patterns {
83                if let Some(prefix) = inlude_pattern_prefix {
84                    flags.push(format!("-Finclude={}", prepend_prefix_to_pattern(prefix, &pat)));
85                } else {
86                    flags.push(format!("-Finclude={pat}"));
87                }
88            }
89        }
90        flags
91    }
92}
93
94fn prepend_prefix_to_pattern(prefix: &Utf8Path, pat: &str) -> String {
95    // don't use the empty `prefix` as that makes the pattern hang off root!
96    if prefix.as_str().is_empty() {
97        return pat.to_string();
98    }
99    if pat.starts_with("def:") {
100        return pat.to_string();
101    }
102    // I haven't tested this on windows, but it should work because `globset`
103    // will normalize patterns to use `/` as separator.
104    if let Some(pat) = pat.strip_prefix("glob:") {
105        format!("glob:{prefix}/{pat}")
106    } else if let Some(pat) = pat.strip_prefix("span:") {
107        // span patterns are of the form `span:<file>:<line>:<column>""
108        format!("span:{prefix}/{pat}")
109    } else {
110        // no prefix defaults to glob patterns.
111        format!("{prefix}/{pat}")
112    }
113}
flux_bin/lib.rs

flux_bin/
lib.rs
