rem_verification/exports/
impls.rs

1use std::ffi::OsStr;
2use std::path::PathBuf;
3
4use crate::verify::coq_verification;
5
6use super::utils::*;
7use super::create_crates::*;
8use super::create_tempdir::*;
9use super::run_charon::*;
10use super::run_aeneas::*;
11
12#[derive(Debug)]
13pub struct VerificationError {
14    pub msg: String,
15}
16
17impl std::fmt::Display for VerificationError {
18    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
19        write!(f, "VerificationError: {}", self.msg)
20    }
21}
22
23impl std::error::Error for VerificationError {}
24
25impl From<Box<dyn std::error::Error>> for VerificationError {
26    fn from(err: Box<dyn std::error::Error>) -> Self {
27        VerificationError {
28            msg: err.to_string(),
29        }
30    }
31}
32
33
34// We don't necessarily have a success if we get a VerificationReturn
35#[derive(Debug)]
36pub struct VerificationReturn {
37    pub success: bool,
38}
39
40#[derive(Debug)]
41pub struct ProgramPaths {
42    pub charon: PathBuf,
43    pub aeneas: PathBuf,
44}
45
46impl std::fmt::Display for ProgramPaths {
47    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
48        write!(f, "Charon Path: {}, Aeneas Path: {}", self.charon.display(), self.aeneas.display())
49    }
50}
51
52impl ProgramPaths {
53    pub fn new(charon: PathBuf, aeneas: PathBuf) -> Self {
54        Self { charon, aeneas }
55    }
56
57    pub fn new_from_directory(base_dir: &PathBuf) -> Result<Self, VerificationError> {
58        let charon = base_dir.join("charon");
59        let aeneas = base_dir.join("aeneas");
60
61        // Ensure the paths exist?
62        if !charon.exists() {
63            return Err(VerificationError { msg: format!("Charon path does not exist: {}", charon.display()) });
64        }
65        if !aeneas.exists() {
66            return Err(VerificationError { msg: format!("Aeneas path does not exist: {}", aeneas.display()) });
67        }
68
69        Ok( Self { charon, aeneas } )
70    }
71}
72
73
74#[derive(Debug)]
75pub struct FileContent {
76    pub path: PathBuf,
77    pub content: String,
78}
79
80impl FileContent {
81    pub fn new(path: PathBuf, content: String) -> Self {
82        Self { path, content }
83    }
84
85    pub fn from_path(path: PathBuf) -> Result<Self, VerificationError> {
86        let content = std::fs::read_to_string(&path)
87            .map_err(|e| VerificationError { msg: format!("Failed to read file {}: {}", path.display(), e) })?;
88        Ok(Self { path, content })
89    }
90}
91
92#[derive(Debug)]
93pub struct VerificationInput {
94    original_file: FileContent,
95    refactored_file: FileContent,
96    fn_name: String,
97    programs: ProgramPaths,
98}
99
100impl VerificationInput {
101    pub fn new( original_file: FileContent, refactored_file: FileContent, fn_name: String, programs: ProgramPaths ) -> Self {
102        Self {
103            original_file,
104            refactored_file,
105            fn_name,
106            programs,
107        }
108    }
109}
110
111pub fn call_verifier(
112    input: VerificationInput,
113) -> Result<VerificationReturn, VerificationError> {
114
115    // We will need to gather the following logic from around this crate:
116    // 1) Create the two virtual crates we are operating on - work out what the
117    //    crate is based on the file paths (the paths should be the same its
118    //    just the content that is different) - but we need to create two "fake"
119    //    crates that are as minimal as possible
120    // 2) Invoke charon on both crates to get the llbc representation
121    // 3) Invoke aeneas on the two llbc files to get the two coq files
122    // 4) Build out the coq project and proof scripts to verify equivalence of
123    //    the two functions
124    // 5) Run coq to check the proof
125    // 6) Return success/failure based on the proof result
126
127    // Get the minmal crate for the path
128    let input_path = &input.original_file.path;
129    let manifest_path = find_manifest_for(input_path)
130        .ok_or_else(|| VerificationError {
131            msg: format!(
132                "Could not find Cargo.toml for path: {}",
133                input_path.display()
134            ),
135        })?;
136
137    // Now that we know what the crate is, we can create the virtual crates
138    // with the modified file contents. One will be an exact copy of the
139    // original crate, the other will have the refactored file content swapped
140    // in.
141    // We do need physical copies of these crates on disk for charon to work
142    // with them, so we will create temporary directories for them, and copy
143    // them over.
144    let refactored_content = &input.refactored_file.content;
145    let twin_crates: TwinCrates = TwinCrates::new(
146        &manifest_path,
147        &input.original_file.path,
148        refactored_content,
149    )?;
150
151    // create a shared temp dir for all the verification artifacts
152    let temp_dir: SharedTempDir = SharedTempDir::new("rem_verification")?;
153    let _llbc_dir: PathBuf = temp_dir.subdir("llbc")?;
154    let coq_dir: PathBuf = temp_dir.subdir("coq")?;
155
156    let empty_args: [&OsStr; 0] = [];
157
158    // invoke charon on both crates to get the llbc files
159    let (orig_llbc_path, _o1) = run_charon_on_crate(
160        &input.programs,
161        &twin_crates.original.manifest,
162        &temp_dir,
163        "original",
164        &empty_args,
165    )?;
166    let (ref_llbc_path, _o2) = run_charon_on_crate(
167        &input.programs,
168        &twin_crates.refactored.manifest,
169        &temp_dir,
170        "refactored",
171        &empty_args,
172    )?;
173
174    // invoke aeneas on both llbc files to get the coq files
175    let (orig_v_path, _a1) = run_aeneas_llbc_to_coq(
176        &input.programs,
177        &orig_llbc_path,
178        &temp_dir,
179        &empty_args
180    )?;
181
182    let (ref_v_path, _a2) = run_aeneas_llbc_to_coq(
183        &input.programs,
184        &ref_llbc_path,
185        &temp_dir,
186        &empty_args
187    )?;
188
189    // ensure we have a Primitives.v file in the coq dir as well
190    ensure_primitives_file(&coq_dir)?;
191
192    // now run the coq verification (this also generates the coq project and
193    // equivcheck files)
194    let (_coq_project, _equivcheck, _primitives, success) = coq_verification(
195        &orig_v_path,
196        &ref_v_path,
197        &input.fn_name,
198    )?;
199
200    // Ensure the crates are alive until the end of the function. The crates
201    // will be `dropped` at the end of their scope.
202    let _ = twin_crates;
203    let _ = temp_dir;
204
205    Ok( VerificationReturn { success } )
206}
rem_verification/exports/impls.rs

rem_verification/exports/
impls.rs
