Skip to main content

generate_ml/
main.rs

1//! Generate ocaml deserialization code for our types.
2//!
3//! This binary runs charon on itself and generates the appropriate `<type>_of_json` functions for
4//! our types. The generated functions are inserted into `./generate-ml/GAstOfJson.template.ml` to
5//! construct the final `GAstOfJson.ml`.
6//!
7//! To run it, call `cargo run --bin generate-ml`. It is also run by `make generate-ml` in the
8//! crate root. Don't forget to format the output code after regenerating.
9
10use anyhow::{Context, Result, bail};
11use assert_cmd::cargo::CommandCargoExt;
12use charon_lib::ast::*;
13use charon_lib::options::SerializationFormat;
14use itertools::Itertools;
15use std::collections::{HashMap, HashSet};
16use std::fs;
17use std::path::PathBuf;
18use std::process::Command;
19
20use crate::to_ocaml_ty::DeriveVisitors;
21use crate::util::*;
22
23mod of_json;
24mod of_postcard;
25mod to_ocaml_ty;
26mod util;
27
28struct GenerateCtx<'a> {
29    crate_data: &'a TranslatedCrate,
30    name_to_type: HashMap<String, &'a TypeDecl>,
31    /// For each type, list the types it contains.
32    type_tree: HashMap<TypeDeclId, HashSet<TypeDeclId>>,
33    /// For types that may be ambiguous in OCaml, the generated module name to prefix to them,
34    /// along with the "short" module name for other generators
35    ambiguous_types: HashMap<TypeDeclId, (String, String)>,
36    /// The current module name being compiled.
37    current_module: Option<String>,
38    /// The list of types currently being generated.
39    current_ids: Vec<TypeDeclId>,
40}
41
42impl<'a> GenerateCtx<'a> {
43    fn new(crate_data: &'a TranslatedCrate, ambiguous_types: &[(&str, (&str, &str))]) -> Self {
44        let mut name_to_type: HashMap<String, &TypeDecl> = Default::default();
45        let mut type_tree = HashMap::default();
46        for ty in &crate_data.type_decls {
47            let long_name = repr_name(&ty.item_meta.name);
48            if long_name.starts_with("charon_lib") {
49                let short_name = ty.item_meta.name.short_str().unwrap().to_string();
50                name_to_type.insert(short_name, ty);
51            }
52            name_to_type.insert(long_name, ty);
53
54            let mut contained = HashSet::new();
55            ty.dyn_visit(|id: &TypeDeclId| {
56                contained.insert(*id);
57            });
58            type_tree.insert(ty.def_id, contained);
59        }
60
61        let mut ctx = GenerateCtx {
62            crate_data,
63            name_to_type,
64            type_tree,
65            ambiguous_types: Default::default(),
66            current_module: None,
67            current_ids: vec![],
68        };
69
70        ctx.ambiguous_types = ambiguous_types
71            .iter()
72            .map(|(name, (m1, m2))| (ctx.id_from_name(name), (m1.to_string(), m2.to_string())))
73            .collect();
74
75        ctx
76    }
77}
78
79/// The kind of code generation to perform.
80#[derive(Clone, Copy)]
81enum GenerationKind {
82    OfJson,
83    OfPostcard,
84    TypeDecl(Option<DeriveVisitors>),
85}
86
87/// Replace markers in `template` with auto-generated code.
88struct GenerateCodeFor {
89    template: PathBuf,
90    target: PathBuf,
91    /// Each list corresponds to a marker. We replace the ith `__REPLACE{i}__` marker with
92    /// generated code for each definition in the ith list.
93    ///
94    /// Eventually we should reorder definitions so the generated ones are all in one block.
95    /// Keeping the order is important while we migrate away from hand-written code.
96    markers: Vec<(GenerationKind, HashSet<TypeDeclId>)>,
97}
98
99impl GenerateCodeFor {
100    fn generate(&self, ctx: &mut GenerateCtx) -> Result<()> {
101        ctx.current_module = self
102            .target
103            .file_prefix()
104            .and_then(|s| s.to_str())
105            .map(|s| s.to_string());
106
107        let mut template = fs::read_to_string(&self.template)
108            .with_context(|| format!("Failed to read template file {}", self.template.display()))?;
109        for (i, (kind, names)) in self.markers.iter().enumerate() {
110            let tys = names
111                .iter()
112                .map(|&id| &ctx.crate_data[id])
113                .sorted_by_key(|tdecl| (tdecl.item_meta.name.short_str().unwrap(), tdecl.def_id))
114                .collect::<Vec<_>>();
115            ctx.current_ids = names.iter().copied().collect();
116            let generated = match kind {
117                GenerationKind::OfJson => ctx.type_decls_to_json(tys),
118                GenerationKind::OfPostcard => ctx.type_decls_to_postcard(tys),
119                GenerationKind::TypeDecl(visitors) => ctx.type_decls_to_ocaml(visitors, tys),
120            };
121            let placeholder = format!("(* __REPLACE{i}__ *)");
122            template = template.replace(&placeholder, &generated);
123        }
124
125        fs::write(&self.target, template)
126            .with_context(|| format!("Failed to write generated file {}", self.target.display()))?;
127        Ok(())
128    }
129}
130
131fn main() -> Result<()> {
132    let dir = PathBuf::from("src/bin/generate-ml");
133    let charon_llbc = dir.join("charon-itself.ullbc");
134    let reuse_llbc = std::env::var("CHARON_ML_REUSE_LLBC").is_ok(); // Useful when developping
135    if !reuse_llbc {
136        // Call charon on itself
137        let mut cmd = Command::cargo_bin("charon")?;
138        cmd.arg("cargo");
139        cmd.arg("--hide-marker-traits");
140        cmd.arg("--hide-allocator");
141        cmd.arg("--treat-box-as-builtin");
142        cmd.arg("--ullbc");
143        cmd.arg("--start-from=charon_lib::ast::krate::TranslatedCrate");
144        cmd.arg("--start-from=charon_lib::ast::ullbc_ast::BodyContents");
145        cmd.arg("--exclude=charon_lib::common::hash_by_addr::HashByAddr");
146        cmd.arg("--unbind-item-vars");
147        cmd.arg("--sysroot=default");
148        cmd.arg("--dest-file");
149        cmd.arg(&charon_llbc);
150        cmd.arg("--");
151        cmd.arg("--lib");
152        cmd.arg("--features");
153        cmd.arg("charon_on_charon");
154        let output = cmd.output()?;
155
156        if !output.status.success() {
157            let stderr = String::from_utf8(output.stderr.clone())?;
158            bail!("Compilation failed: {stderr}")
159        }
160    }
161
162    let crate_data: TranslatedCrate =
163        charon_lib::deserialize_llbc_with_format(&charon_llbc, SerializationFormat::Json)?;
164    let output_dir = if std::env::var("IN_CI").as_deref() == Ok("1") {
165        dir.join("generated")
166    } else {
167        dir.join("../../../../charon-ml/src/generated")
168    };
169    generate_ml(crate_data, dir.join("templates"), output_dir)
170}
171
172fn generate_ml(
173    crate_data: TranslatedCrate,
174    template_dir: PathBuf,
175    output_dir: PathBuf,
176) -> anyhow::Result<()> {
177    // Types for which we don't want to generate a type at all.
178    let dont_generate_ty = &[
179        "TraitTypeConstraintId",
180        "charon_lib::ids::index_vec::IndexVec",
181        "charon_lib::ids::index_map::IndexMap",
182    ];
183
184    #[rustfmt::skip]
185    let ambiguous_types = &[
186        ("charon_lib::ast::ullbc_ast::Statement", ("Generated_UllbcAst", "Ullbc")),
187        ("charon_lib::ast::ullbc_ast::StatementKind", ("Generated_UllbcAst", "Ullbc")),
188        ("charon_lib::ast::ullbc_ast::SwitchTargets", ("Generated_UllbcAst", "Ullbc")),
189        ("charon_lib::ast::ullbc_ast::BlockData", ("Generated_UllbcAst", "Ullbc")),
190        ("charon_lib::ast::ullbc_ast::BlockId", ("Generated_UllbcAst", "Ullbc")),
191        ("charon_lib::ast::llbc_ast::Statement", ("Generated_LlbcAst", "Llbc")),
192        ("charon_lib::ast::llbc_ast::StatementKind", ("Generated_LlbcAst", "Llbc")),
193        ("charon_lib::ast::llbc_ast::Switch", ("Generated_LlbcAst", "Llbc")),
194        ("charon_lib::ast::llbc_ast::Block", ("Generated_LlbcAst", "Llbc")),
195    ];
196
197    let mut ctx = GenerateCtx::new(&crate_data, ambiguous_types);
198
199    // Compute type sets for json deserializers.
200    let mut gast_types: HashSet<TypeDeclId> = HashSet::new();
201    let mut llbc_types: HashSet<TypeDeclId> = HashSet::new();
202    let mut ullbc_types: HashSet<TypeDeclId> = HashSet::new();
203    let mut full_ast_types: HashSet<TypeDeclId> = HashSet::new();
204    {
205        let mut all_types: HashSet<_> = ctx.children_of("TranslatedCrate");
206        all_types.insert(ctx.id_from_name("indexmap::map::IndexMap")); // Add this one foreign type
207        all_types.remove(&ctx.id_from_name("charon_lib::ids::index_map::IndexMap"));
208        let all_llbc_types: HashSet<_> =
209            ctx.children_of_many(&["charon_lib::ast::llbc_ast::Block"]);
210        let all_ullbc_types: HashSet<_> = ctx.children_of_many(&[
211            "charon_lib::ast::ullbc_ast::BlockData",
212            "charon_lib::ast::ullbc_ast::BlockId",
213        ]);
214        all_types.into_iter().for_each(|ty| {
215            let in_llbc = all_llbc_types.contains(&ty);
216            let in_ullbc = all_ullbc_types.contains(&ty);
217            match (in_llbc, in_ullbc) {
218                (true, false) => llbc_types.insert(ty),
219                (false, true) => ullbc_types.insert(ty),
220                (true, true) => gast_types.insert(ty),
221                (false, false) => full_ast_types.insert(ty),
222            };
223        });
224    };
225
226    let mut processed_tys: HashSet<TypeDeclId> = dont_generate_ty
227        .iter()
228        .map(|name| ctx.id_from_name(name))
229        .collect();
230    // Each call to this will return the children of the listed types that haven't been returned
231    // yet. By calling it in dependency order, this allows to organize types into files without
232    // having to list them all.
233    let mut markers_from_children = |ctx: &GenerateCtx, markers: &[_]| {
234        markers
235            .iter()
236            .copied()
237            .map(|(kind, type_names)| {
238                let unprocessed_types: HashSet<_> = ctx
239                    .children_of_many(type_names)
240                    .into_iter()
241                    .filter(|&id| processed_tys.insert(id))
242                    .collect();
243                (kind, unprocessed_types)
244            })
245            .collect_vec()
246    };
247
248    #[rustfmt::skip]
249    let generate_code_for = vec![
250        GenerateCodeFor {
251            template: template_dir.join("Meta.ml"),
252            target: output_dir.join("Generated_Meta.ml"),
253            markers: markers_from_children(&ctx, &[
254                (GenerationKind::TypeDecl(None), &[
255                    "File",
256                    "Span",
257                    "AttrInfo",
258                ]),
259            ]),
260        },
261        GenerateCodeFor {
262            template: template_dir.join("Values.ml"),
263            target: output_dir.join("Generated_Values.ml"),
264            markers: markers_from_children(&ctx, &[
265                (GenerationKind::TypeDecl(Some(DeriveVisitors {
266                    ancestors: &["big_int"],
267                    name: "literal",
268                    reduce: true,
269                    extra_types: &["char_value"],
270                })), &[
271                    "Literal",
272                    "IntegerTy",
273                    "LiteralTy",
274                ]),
275            ]),
276        },
277        GenerateCodeFor {
278            template: template_dir.join("Types.ml"),
279            target: output_dir.join("Generated_Types.ml"),
280            markers: markers_from_children(&ctx, &[
281                (GenerationKind::TypeDecl(Some(DeriveVisitors {
282                    ancestors: &["literal"],
283                    name: "type_vars",
284                    reduce: true,
285                    extra_types: &[],
286                })), &[
287                    "TypeVarId",
288                    "TraitClauseId",
289                    "DeBruijnVar",
290                    "ItemId",
291                ]),
292                // Can't merge into above because aeneas uses the above alongside their own partial
293                // copy of `ty`, which causes method type clashes.
294                (GenerationKind::TypeDecl(Some(DeriveVisitors {
295                    ancestors: &["ty_base"],
296                    name: "ty",
297                    reduce: false,
298                    extra_types: &[],
299                })), &[
300                    "ConstantExpr",
301                    "TyKind",
302                    "TraitImplRef",
303                    "FunDeclRef",
304                    "GlobalDeclRef",
305                ]),
306                // TODO: can't merge into above because of field name clashes (`types`, `regions` etc).
307                (GenerationKind::TypeDecl(Some(DeriveVisitors {
308                    ancestors: &["ty"],
309                    name: "type_decl",
310                    reduce: false,
311                    extra_types: &[
312                        "attr_info"
313                    ],
314                })), &[
315                    "Binder",
316                    "TypeDecl",
317                ]),
318            ]),
319        },
320        GenerateCodeFor {
321            template: template_dir.join("Expressions.ml"),
322            target: output_dir.join("Generated_Expressions.ml"),
323            markers: markers_from_children(&ctx, &[
324                (GenerationKind::TypeDecl(Some(DeriveVisitors {
325                    ancestors: &["type_decl"],
326                    name: "rvalue",
327                    reduce: false,
328                    extra_types: &[],
329                })), &[
330                    "Rvalue",
331                ]),
332            ]),
333        },
334        GenerateCodeFor {
335            template: template_dir.join("GAst.ml"),
336            target: output_dir.join("Generated_GAst.ml"),
337            markers: markers_from_children(&ctx, &[
338                (GenerationKind::TypeDecl(Some(DeriveVisitors {
339                    ancestors: &["rvalue"],
340                    name: "fun_sig",
341                    reduce: false,
342                    extra_types: &[],
343                })), &[
344                    "Call",
345                    "DropKind",
346                    "Assert",
347                    "ItemSource",
348                    "Locals",
349                    "FunSig",
350                    "CopyNonOverlapping",
351                    "Error",
352                    "AbortKind",
353                ]),
354                // These have to be kept separate to avoid field name clashes
355                (GenerationKind::TypeDecl(Some(DeriveVisitors {
356                    ancestors: &["fun_sig"],
357                    name: "global_decl",
358                    reduce: false,
359                    extra_types: &[],
360                })), &[
361                    "GlobalDecl",
362                ]),
363                (GenerationKind::TypeDecl(Some(DeriveVisitors {
364                    ancestors: &["trait_decl_base"],
365                    name: "trait_decl",
366                    reduce: false,
367                    extra_types: &[],
368                })), &[
369                    "TraitDecl",
370                ]),
371                (GenerationKind::TypeDecl(Some(DeriveVisitors {
372                    ancestors: &["trait_decl"],
373                    name: "trait_impl",
374                    reduce: false,
375                    extra_types: &[],
376                })), &[
377                    "TraitImpl",
378                    "GExprBody",
379                ]),
380            ]),
381        },
382        GenerateCodeFor {
383            template: template_dir.join("LlbcAst.ml"),
384            target: output_dir.join("Generated_LlbcAst.ml"),
385            markers: markers_from_children(&ctx, &[
386                (GenerationKind::TypeDecl(Some(DeriveVisitors {
387                    name: "statement_base",
388                    ancestors: &["trait_impl"],
389                    reduce: false,
390                    extra_types: &[],
391                })), &[
392                    "charon_lib::ast::llbc_ast::Statement",
393                ]),
394            ]),
395        },
396        GenerateCodeFor {
397            template: template_dir.join("UllbcAst.ml"),
398            target: output_dir.join("Generated_UllbcAst.ml"),
399            markers: markers_from_children(&ctx, &[
400                (GenerationKind::TypeDecl(Some(DeriveVisitors {
401                    ancestors: &["trait_impl"],
402                    name: "ullbc_ast",
403                    reduce: false,
404                    extra_types: &[],
405                })), &[
406                    "charon_lib::ast::ullbc_ast::BodyContents",
407                ]),
408            ]),
409        },
410        GenerateCodeFor {
411            template: template_dir.join("FullAst.ml"),
412            target: output_dir.join("Generated_FullAst.ml"),
413            markers: markers_from_children(&ctx, &[
414                (GenerationKind::TypeDecl(None), &[
415                    "FunDecl",
416                    "Body",
417                    "CliOpts",
418                    "DeclarationGroup",
419                    "TranslatedCrate",
420                ]),
421            ]),
422        },
423        GenerateCodeFor {
424            template: template_dir.join("OfJson.ml"),
425            target: output_dir.join("Generated_OfJson.ml"),
426            markers: vec![
427                (GenerationKind::OfJson, gast_types.clone()),
428                (GenerationKind::OfJson, ullbc_types.clone()),
429                (GenerationKind::OfJson, llbc_types.clone()),
430                (GenerationKind::OfJson, full_ast_types.clone()),
431            ],
432        },
433        GenerateCodeFor {
434            template: template_dir.join("OfPostcard.ml"),
435            target: output_dir.join("Generated_OfPostcard.ml"),
436            markers: vec![
437                (GenerationKind::OfPostcard, gast_types),
438                (GenerationKind::OfPostcard, ullbc_types),
439                (GenerationKind::OfPostcard, llbc_types),
440                (GenerationKind::OfPostcard, full_ast_types),
441            ],
442        },
443    ];
444    for file in generate_code_for {
445        file.generate(&mut ctx)?;
446    }
447    Ok(())
448}