1use 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 type_tree: HashMap<TypeDeclId, HashSet<TypeDeclId>>,
33 ambiguous_types: HashMap<TypeDeclId, (String, String)>,
36 current_module: Option<String>,
38 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#[derive(Clone, Copy)]
81enum GenerationKind {
82 OfJson,
83 OfPostcard,
84 TypeDecl(Option<DeriveVisitors>),
85}
86
87struct GenerateCodeFor {
89 template: PathBuf,
90 target: PathBuf,
91 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(); if !reuse_llbc {
136 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 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 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")); 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 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 (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 (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 (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}