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    ) -> Vec<String> {
53        let mut flags = vec![];
54        if let Some(true) = self.cache {
55            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
56        }
57        if let Some(v) = self.solver {
58            flags.push(format!("-Fsolver={v}"));
59        }
60        if let Some(v) = self.check_overflow {
61            flags.push(format!("-Fcheck-overflow={v}"));
62        }
63        if let Some(v) = self.lean {
64            flags.push(format!("-Flean={v}"));
65        }
66        if let Some(v) = self.dump_constraint {
67            flags.push(format!("-Fdump-constraint={v}"));
68        }
69        if let Some(v) = self.scrape_quals {
70            flags.push(format!("-Fscrape-quals={v}"));
71        }
72        if let Some(v) = self.smt_define_fun {
73            flags.push(format!("-Fsmt-define-fun={v}"));
74        }
75        if let Some(v) = self.default_trusted {
76            flags.push(format!("-Ftrusted={v}"));
77        }
78        if let Some(v) = self.no_panic {
79            flags.push(format!("-Fno-panic={v}"));
80        }
81        if let Some(v) = self.default_ignore {
82            flags.push(format!("-Fignore={v}"));
83        }
84        if let Some(v) = self.allow_uninterpreted_cast {
85            flags.push(format!("-Fallow-uninterpreted-cast={v}"));
86        }
87        if let Some(patterns) = self.include {
88            for pat in patterns {
89                if let Some(prefix) = include_pattern_prefix {
90                    flags.push(format!("-Finclude={}", prepend_prefix_to_pattern(prefix, &pat)));
91                } else {
92                    flags.push(format!("-Finclude={pat}"));
93                }
94            }
95        }
96        if let Some(patterns) = self.include_trusted {
97            for pat in patterns {
98                if let Some(glob_prefix) = include_pattern_prefix
99                    && !glob_prefix.as_str().is_empty()
100                {
101                    flags.push(format!("-Finclude-trusted={glob_prefix}/{pat}"));
102                } else {
103                    flags.push(format!("-Finclude-trusted={pat}"));
104                }
105            }
106        }
107        if let Some(patterns) = self.include_trusted_impl {
108            for pat in patterns {
109                if let Some(glob_prefix) = include_pattern_prefix
110                    && !glob_prefix.as_str().is_empty()
111                {
112                    flags.push(format!("-Finclude-trusted-impl={glob_prefix}/{pat}"));
113                } else {
114                    flags.push(format!("-Finclude-trusted-impl={pat}"));
115                }
116            }
117        }
118        flags
119    }
120}
121
122fn prepend_prefix_to_pattern(prefix: &Utf8Path, pat: &str) -> String {
123    // don't use the empty `prefix` as that makes the pattern hang off root!
124    if prefix.as_str().is_empty() {
125        return pat.to_string();
126    }
127    if pat.starts_with("def:") {
128        return pat.to_string();
129    }
130    // I haven't tested this on windows, but it should work because `globset`
131    // will normalize patterns to use `/` as separator.
132    if let Some(pat) = pat.strip_prefix("glob:") {
133        format!("glob:{prefix}/{pat}")
134    } else if let Some(pat) = pat.strip_prefix("span:") {
135        // span patterns are of the form `span:<file>:<line>:<column>""
136        format!("span:{prefix}/{pat}")
137    } else {
138        // no prefix defaults to glob patterns.
139        format!("{prefix}/{pat}")
140    }
141}
flux_bin/lib.rs

flux_bin/
lib.rs
