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, only consider `DefId` in files that match any of the glob patterns as trusted.
33    /// Patterns are checked relative to the location of the manifest file.
34    pub include_trusted: Option<Vec<String>>,
35    /// If present, only consider `DefId` in files that match any of the glob patterns as trusted_impl.
36    /// Patterns are checked relative to the location of the manifest file.
37    pub include_trusted_impl: Option<Vec<String>>,
38    /// If present, every function in the module is implicitly labeled with a `no_panic` by default.
39    /// This means that the only way a function can panic is if it calls an external function without this attribute.
40    pub no_panic: Option<bool>,
41    /// If present, enables lean mode
42    pub lean: Option<LeanMode>,
43    /// If present, dumps the fixpoint constraint to a file
44    pub dump_constraint: Option<bool>,
45}
46
47impl FluxMetadata {
48    pub fn into_flags(
49        self,
50        target_dir: &Utf8Path,
51        include_pattern_prefix: Option<&Utf8Path>,
52        only_check: Option<&str>,
53    ) -> Vec<String> {
54        let mut flags = vec![];
55        if let Some(true) = self.cache {
56            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
57        }
58        if let Some(v) = self.solver {
59            flags.push(format!("-Fsolver={v}"));
60        }
61        if let Some(v) = self.check_overflow {
62            flags.push(format!("-Fcheck-overflow={v}"));
63        }
64        if let Some(v) = self.lean {
65            flags.push(format!("-Flean={v}"));
66        }
67        if let Some(v) = self.dump_constraint {
68            flags.push(format!("-Fdump-constraint={v}"));
69        }
70        if let Some(v) = self.scrape_quals {
71            flags.push(format!("-Fscrape-quals={v}"));
72        }
73        if let Some(v) = self.smt_define_fun {
74            flags.push(format!("-Fsmt-define-fun={v}"));
75        }
76        if let Some(v) = self.default_trusted {
77            flags.push(format!("-Ftrusted={v}"));
78        }
79        if let Some(v) = self.no_panic {
80            flags.push(format!("-Fno-panic={v}"));
81        }
82        if let Some(v) = self.default_ignore {
83            flags.push(format!("-Fignore={v}"));
84        }
85        if let Some(v) = self.allow_uninterpreted_cast {
86            flags.push(format!("-Fallow-uninterpreted-cast={v}"));
87        }
88        if let Some(only_check) = only_check {
89            flags.push(format!("-Finclude={only_check}"));
90        } else if let Some(patterns) = self.include {
91            for pat in patterns {
92                if let Some(prefix) = include_pattern_prefix {
93                    flags.push(format!("-Finclude={}", prepend_prefix_to_pattern(prefix, &pat)));
94                } else {
95                    flags.push(format!("-Finclude={pat}"));
96                }
97            }
98        }
99        if let Some(patterns) = self.include_trusted {
100            for pat in patterns {
101                if let Some(glob_prefix) = include_pattern_prefix
102                    && !glob_prefix.as_str().is_empty()
103                {
104                    flags.push(format!("-Finclude-trusted={glob_prefix}/{pat}"));
105                } else {
106                    flags.push(format!("-Finclude-trusted={pat}"));
107                }
108            }
109        }
110        if let Some(patterns) = self.include_trusted_impl {
111            for pat in patterns {
112                if let Some(glob_prefix) = include_pattern_prefix
113                    && !glob_prefix.as_str().is_empty()
114                {
115                    flags.push(format!("-Finclude-trusted-impl={glob_prefix}/{pat}"));
116                } else {
117                    flags.push(format!("-Finclude-trusted-impl={pat}"));
118                }
119            }
120        }
121        flags
122    }
123}
124
125fn prepend_prefix_to_pattern(prefix: &Utf8Path, pat: &str) -> String {
126    // don't use the empty `prefix` as that makes the pattern hang off root!
127    if prefix.as_str().is_empty() {
128        return pat.to_string();
129    }
130    if pat.starts_with("def:") {
131        return pat.to_string();
132    }
133    // I haven't tested this on windows, but it should work because `globset`
134    // will normalize patterns to use `/` as separator.
135    if let Some(pat) = pat.strip_prefix("glob:") {
136        format!("glob:{prefix}/{pat}")
137    } else if let Some(pat) = pat.strip_prefix("span:") {
138        // span patterns are of the form `span:<file>:<line>:<column>""
139        format!("span:{prefix}/{pat}")
140    } else {
141        // no prefix defaults to glob patterns.
142        format!("{prefix}/{pat}")
143    }
144}
flux_bin/lib.rs

flux_bin/
lib.rs
