distributed_verification/
lib.rs

1use eyre::Result;
2use serde::{Deserialize, Serialize};
3
4#[macro_use]
5extern crate tracing;
6#[macro_use]
7extern crate eyre;
8
9pub mod db;
10pub mod diff;
11pub mod error_handling;
12pub mod kani_list;
13pub mod logger;
14pub mod statistics;
15
16pub type BoxStr = Box<str>;
17
18/// Kani proof kind.
19///
20/// Suppose each proof only belongs to single kind.
21#[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, Hash)]
22pub enum ProofKind {
23    /// `#[kani::proof]`
24    Standard,
25    /// `#[kani::proof_for_contract]`
26    Contract,
27}
28
29/// [`InstanceKind`], but remove Virtual idx and make Item as None to save space.
30///
31/// [`InstanceKind`]: https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/mono/enum.InstanceKind.html
32#[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, Hash)]
33pub enum InstKind {
34    Intrinsic,
35    Virtual,
36    Shim,
37}
38
39#[derive(Debug, Serialize, Deserialize, Clone)]
40pub struct Callee {
41    pub def_id: String,
42    pub func: SourceCode,
43}
44
45#[derive(Clone, Debug, Default, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, Hash)]
46pub struct SourceCode {
47    // A file path where src lies.
48    // The path is stripped with pwd or sysroot prefix.
49    pub file: String,
50
51    /// Function name.
52    pub name: String,
53
54    /// InstanceKind, but normal Item is represented as None.
55    #[serde(skip_serializing_if = "Option::is_none")]
56    #[serde(default)]
57    pub inst_kind: Option<InstKind>,
58
59    /// Potential kani proof kind: standard or contract.
60    /// This tool will never identify if a function is an auto harness.
61    #[serde(skip_serializing_if = "Option::is_none")]
62    #[serde(default)]
63    pub proof_kind: Option<ProofKind>,
64
65    /// Attributes are attached the function, but it seems that attributes
66    /// and function must be separated to query.
67    #[serde(skip_serializing_if = "Vec::is_empty")]
68    #[serde(default)]
69    pub attrs: Vec<String>,
70
71    /// Source that a stable_mir span points to.
72    pub src: String,
73
74    /// The count of macro backtraces.
75    #[serde(skip_serializing_if = "zero")]
76    #[serde(default)]
77    pub macro_backtrace_len: usize,
78
79    /// Is the stable_mir span from a macro expansion?
80    /// If it is from an expansion, what's the source code before expansion?
81    /// * Some(_) happens when the src (stable_mir) span comes from expansion, and tells
82    ///   the source before the expansion.
83    /// * None if the src is not from a macro expansion.
84    ///
85    /// Refer to [#31] to know sepecific cases.
86    ///
87    /// [#31]: https://github.com/os-checker/distributed-verification/issues/31
88    #[serde(skip_serializing_if = "Vec::is_empty")]
89    #[serde(default)]
90    pub macro_backtrace: Vec<MacroBacktrace>,
91}
92
93fn zero(n: &usize) -> bool {
94    *n == 0
95}
96
97#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, Hash)]
98pub struct MacroBacktrace {
99    pub callsite: String,
100    pub defsite: String,
101}
102
103/// A local path to kani's artifacts.
104///
105/// Choose the following if found
106/// * `$KANI_DIR`
107/// * or `$KANI_HOME/kani-{version}`
108/// * or `$HOME/.kani/kani-{version}`
109pub fn kani_path() -> String {
110    use std::env::var;
111    let path = if let Ok(path) = var("KANI_DIR") {
112        path
113    } else {
114        let kani = std::process::Command::new("kani").arg("--version").output().unwrap();
115        let kani_folder = std::str::from_utf8(&kani.stdout).unwrap().trim().replace(' ', "-");
116        let home = var("KANI_HOME").or_else(|_| var("HOME")).unwrap();
117        format!("{home}/.kani/{kani_folder}")
118    };
119    assert!(std::fs::exists(&path).unwrap());
120    path
121}
122
123#[derive(Debug, Default, Serialize, Deserialize, Clone)]
124pub struct SerFunction {
125    pub hash: Box<str>,
126    pub name: Box<str>,
127    pub file: Box<str>,
128    #[serde(skip_serializing_if = "Option::is_none")]
129    #[serde(default)]
130    pub proof_kind: Option<ProofKind>,
131}
132
133impl SerFunction {
134    /// Is this a kani proof?
135    pub fn is_proof(&self) -> bool {
136        self.proof_kind.is_some()
137    }
138}
distributed_verification/lib.rs

distributed_verification/
lib.rs
