charon_lib/
export.rs

1use crate::ast::*;
2use crate::transform::TransformCtx;
3use serde::{Deserialize, Deserializer, Serialize};
4use serde_state::{DeserializeState, SerializeState};
5use std::fs::File;
6use std::path::Path;
7
8/// The data of a generic crate. We serialize this to pass it to `charon-ml`, so this must be as
9/// stable as possible. This is used for both ULLBC and LLBC.
10#[derive(SerializeState, DeserializeState)]
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_state(stateless)]
15    pub charon_version: CharonVersion,
16    pub translated: TranslatedCrate,
17    #[serde_state(stateless)]
18    #[charon::opaque] // Don't change, this would break version detection for old charon-ml
19    /// If there were errors, this contains only a partial description of the input crate.
20    pub has_errors: bool,
21}
22
23impl Serialize for CrateData {
24    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
25    where
26        S: serde::Serializer,
27    {
28        if self.translated.options.no_dedup_serialized_ast {
29            self.serialize_state(&(), serializer)
30        } else {
31            let state = HashConsDedupSerializer::default();
32            self.serialize_state(&state, serializer)
33        }
34    }
35}
36
37impl<'de> Deserialize<'de> for CrateData {
38    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
39    where
40        D: Deserializer<'de>,
41    {
42        // Always provide the state, just in case.
43        let state = HashConsDedupSerializer::default();
44        Self::deserialize_state(&state, deserializer)
45    }
46}
47
48#[derive(Serialize)]
49pub struct CharonVersion(pub String);
50
51impl<'de> Deserialize<'de> for CharonVersion {
52    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
53    where
54        D: Deserializer<'de>,
55    {
56        use serde::de::Error;
57        let version = String::deserialize(deserializer)?;
58        if version != crate::VERSION {
59            return Err(D::Error::custom(format!(
60                "Incompatible version of charon: \
61                this program supports llbc emitted by charon v{} \
62                but attempted to read a file emitted by charon v{}",
63                crate::VERSION,
64                version,
65            )));
66        }
67        Ok(CharonVersion(version))
68    }
69}
70
71impl CrateData {
72    pub fn new(ctx: TransformCtx) -> Self {
73        CrateData {
74            charon_version: CharonVersion(crate::VERSION.to_owned()),
75            has_errors: ctx.has_errors(),
76            translated: ctx.translated,
77        }
78    }
79
80    /// Export the translated definitions to a JSON file.
81    #[allow(clippy::result_unit_err)]
82    pub fn serialize_to_file(&self, target_filename: &Path) -> Result<(), ()> {
83        // Create the directory, if necessary (note that if the target directory
84        // is not specified, there is no need to create it: otherwise we
85        // couldn't have read the input file in the first place).
86        let target_dir = target_filename.parent().unwrap();
87        match std::fs::create_dir_all(target_dir) {
88            Ok(()) => (),
89            Err(_) => {
90                error!("Could not create the directory: {:?}", target_dir);
91                return Err(());
92            }
93        };
94
95        // Create the file.
96        let std::io::Result::Ok(outfile) = File::create(target_filename) else {
97            error!("Could not open: {:?}", target_filename);
98            return Err(());
99        };
100        // Write to the file.
101        let res = serde_json::to_writer(&outfile, self);
102        match res {
103            Ok(()) => {}
104            Err(err) => {
105                error!("Could not serialize to `{target_filename:?}`: {err:?}");
106                return Err(());
107            }
108        }
109
110        // We canonicalize (i.e., make absolute) the path before printing it; this makes it clearer
111        // to the user where to find the file.
112        let target_filename = std::fs::canonicalize(target_filename).unwrap();
113        if self.has_errors {
114            info!(
115                "Generated the partial (because we encountered errors) file: {}",
116                target_filename.to_str().unwrap()
117            );
118        } else {
119            info!("Generated the file: {}", target_filename.to_str().unwrap());
120        }
121        Ok(())
122    }
123}
charon_lib/export.rs

charon_lib/
export.rs
