charon_lib/
export.rs

1use crate::ast::*;
2use crate::transform::TransformCtx;
3use serde::{Deserialize, Deserializer, Serialize};
4use std::fs::File;
5use std::path::Path;
6
7/// The data of a generic crate. We serialize this to pass it to `charon-ml`, so this must be as
8/// stable as possible. This is used for both ULLBC and LLBC.
9#[derive(Serialize, Deserialize)]
10#[serde(rename = "Crate")]
11pub struct CrateData {
12    /// The version of charon currently being used. `charon-ml` inspects this and errors if it is
13    /// trying to read an incompatible version (for now we compare versions for equality).
14    #[serde(deserialize_with = "ensure_version")]
15    pub charon_version: String,
16    pub translated: TranslatedCrate,
17    #[serde(skip)]
18    /// If there were errors, this contains only a partial description of the input crate.
19    pub has_errors: bool,
20}
21
22impl CrateData {
23    pub fn new(ctx: TransformCtx) -> Self {
24        CrateData {
25            charon_version: crate::VERSION.to_owned(),
26            has_errors: ctx.has_errors(),
27            translated: ctx.translated,
28        }
29    }
30
31    /// Export the translated definitions to a JSON file.
32    #[allow(clippy::result_unit_err)]
33    pub fn serialize_to_file(&self, target_filename: &Path) -> Result<(), ()> {
34        // Create the directory, if necessary (note that if the target directory
35        // is not specified, there is no need to create it: otherwise we
36        // couldn't have read the input file in the first place).
37        let target_dir = target_filename.parent().unwrap();
38        match std::fs::create_dir_all(target_dir) {
39            Ok(()) => (),
40            Err(_) => {
41                error!("Could not create the directory: {:?}", target_dir);
42                return Err(());
43            }
44        };
45
46        // Create the file.
47        let std::io::Result::Ok(outfile) = File::create(target_filename) else {
48            error!("Could not open: {:?}", target_filename);
49            return Err(());
50        };
51        // Write to the file.
52        match serde_json::to_writer(&outfile, self) {
53            Ok(()) => {}
54            Err(err) => {
55                error!("Could not write to `{target_filename:?}`: {err:?}");
56                return Err(());
57            }
58        }
59
60        // We canonicalize (i.e., make absolute) the path before printing it; this makes it clearer
61        // to the user where to find the file.
62        let target_filename = std::fs::canonicalize(target_filename).unwrap();
63        if self.has_errors {
64            info!(
65                "Generated the partial (because we encountered errors) file: {}",
66                target_filename.to_str().unwrap()
67            );
68        } else {
69            info!("Generated the file: {}", target_filename.to_str().unwrap());
70        }
71        Ok(())
72    }
73}
74
75fn ensure_version<'de, D: Deserializer<'de>>(d: D) -> Result<String, D::Error> {
76    use serde::de::Error;
77    let version = String::deserialize(d)?;
78    if version != crate::VERSION {
79        return Err(D::Error::custom(format!(
80            "Incompatible version of charon: \
81            this program supports llbc emitted by charon v{} \
82            but attempted to read a file emitted by charon v{}",
83            crate::VERSION,
84            version,
85        )));
86    }
87    Ok(version)
88}
charon_lib/export.rs

charon_lib/
export.rs
