Add the source files in the translated crate

charon-ml/src/GAst.ml

@@ -424,5 +424,6 @@ type ('fun_body, 'global_body) gcrate = {
   global_decls : 'global_body gglobal_decl GlobalDeclId.Map.t;
   trait_decls : trait_decl TraitDeclId.Map.t;
   trait_impls : trait_impl TraitImplId.Map.t;
+  source_files : string list FileNameMap.t;
 }
 [@@deriving show]

charon-ml/src/GAstOfJson.ml

@@ -1520,6 +1520,7 @@ and gtranslated_crate_of_json
           ("crate_name", name);
           ("real_crate_name", _);
           ("id_to_file", id_to_file);
+          ("file_id_to_content", file_id_to_content);
           ("all_ids", _);
           ("item_names", _);
           ("type_decls", types);
@@ -1563,6 +1564,12 @@ and gtranslated_crate_of_json
             (trait_impl_of_json id_to_file)
             trait_impls
         in
+        let* source_files =
+          list_of_json
+            (key_value_pair_of_json file_id_of_json
+               (list_of_json string_of_json))
+            file_id_to_content
+        in
 
         let type_decls =
           TypeDeclId.Map.of_list
@@ -1586,6 +1593,15 @@ and gtranslated_crate_of_json
           TraitImplId.Map.of_list
             (List.map (fun (d : trait_impl) -> (d.def_id, d)) trait_impls)
         in
+        let source_files =
+          FileNameMap.of_list
+            (List.filter_map
+               (fun (file_id, content) ->
+                 Option.map
+                   (fun filename -> (filename, content))
+                   (FileId.Map.find_opt file_id id_to_file))
+               source_files)
+        in
 
         Ok
           {
@@ -1596,6 +1612,7 @@ and gtranslated_crate_of_json
             global_decls;
             trait_decls;
             trait_impls;
+            source_files;
           }
     | _ -> Error "")
 

charon-ml/src/LlbcOfJson.ml

@@ -232,5 +232,6 @@ let crate_of_json (js : json) : (crate, string) result =
         global_decls;
         trait_decls = crate.trait_decls;
         trait_impls = crate.trait_impls;
+        source_files = crate.source_files;
       }
   end

charon-ml/src/Meta.ml

@@ -118,3 +118,17 @@ and file_name =
   | Local of path_buf
       (** A local path (a file coming from the current crate for instance) *)
 [@@deriving show, ord]
+
+(** Ordered file name *)
+module OrderedFileName : Collections.OrderedType with type t = file_name =
+struct
+  type t = file_name
+
+  let compare = compare_file_name
+  let to_string s = show_file_name s
+  let pp_t fmt s = pp_file_name fmt s
+  let show_t s = show_file_name s
+end
+
+module FileNameSet = Collections.MakeSet (OrderedFileName)
+module FileNameMap = Collections.MakeMap (OrderedFileName)

charon-ml/src/OfJsonBasic.ml

@@ -74,3 +74,13 @@ let option_of_json (a_of_json : json -> ('a, string) result) (js : json) :
 let string_option_of_json (js : json) : (string option, string) result =
   combine_error_msgs js "string_option_of_json"
     (option_of_json string_of_json js)
+
+let key_value_pair_of_json (a_of_json : json -> ('a, string) result)
+    (b_of_json : json -> ('b, string) result) (js : json) :
+    ('a * 'b, string) result =
+  match js with
+  | `Assoc [ ("key", a); ("value", b) ] ->
+      let* a = a_of_json a in
+      let* b = b_of_json b in
+      Ok (a, b)
+  | _ -> Error ("key_value_pair_of_json failed on: " ^ show js)

charon/src/ast/krate.rs

@@ -96,6 +96,14 @@ pub struct TranslatedCrate {
     #[charon::opaque]
     pub file_to_id: HashMap<FileName, FileId>,
 
+    /// File id to content.
+    ///
+    /// Note that we leave the slots for the virtual files as empty: the non-empty slots
+    /// are for the "real" files that we managed to read.
+    #[drive(skip)]
+    #[serde(with = "HashMapToArray::<FileId, Vec<String>>")]
+    pub file_id_to_content: HashMap<FileId, Vec<String>>,
+
     /// All the ids, in the order in which we encountered them
     #[drive(skip)]
     pub all_ids: LinkedHashSet<AnyTransId>,

charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs

@@ -1,6 +1,7 @@
 use super::get_mir::extract_constants_at_top_level;
 use super::translate_ctx::*;
 use charon_lib::ast::krate::*;
+use charon_lib::ast::meta::FileName;
 use charon_lib::common::*;
 use charon_lib::options::CliOpts;
 use charon_lib::transform::ctx::TransformOptions;
@@ -360,6 +361,29 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
     }
 }
 
+/// Read and return the content of a source file.
+fn read_file_content(filename: &FileName) -> Option<Vec<String>> {
+    use std::fs::File;
+    use std::io::prelude::*;
+    use std::io::BufReader;
+    use FileName::*;
+    match filename {
+        Local(path) => {
+            let file = File::open(path).ok()?;
+            BufReader::new(file)
+                .lines()
+                .into_iter()
+                .collect::<Result<Vec<String>, _>>()
+                .ok()
+        }
+        Virtual(_) => {
+            // TODO: we should be able to retrieve the file content here
+            None
+        }
+        NotReal(_) => None,
+    }
+}
+
 #[tracing::instrument(skip(tcx))]
 pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformCtx<'tcx> {
     let hax_state = hax::state::State::new(
@@ -458,6 +482,15 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC
         no_merge_goto_chains: options.no_merge_goto_chains,
         item_opacities: ctx.options.item_opacities,
     };
+
+    // Read the source files
+    ctx.translated.file_id_to_content = ctx
+        .translated
+        .id_to_file
+        .iter_indexed()
+        .filter_map(|(id, filename)| (read_file_content(filename).map(|file| (id, file))))
+        .collect();
+
     // Return the context, dropping the hax state and rustc `tcx`.
     TransformCtx {
         options: transform_options,

charon/src/bin/generate-ml/templates/GAst.ml

@@ -70,6 +70,7 @@ type 'body gglobal_decl = {
 [@@deriving show]
 
 (* Hand-written because the rust equivalent isn't generic *)
+
 (** A crate *)
 type ('fun_body, 'global_body) gcrate = {
   name : string;
@@ -79,5 +80,6 @@ type ('fun_body, 'global_body) gcrate = {
   global_decls : 'global_body gglobal_decl GlobalDeclId.Map.t;
   trait_decls : trait_decl TraitDeclId.Map.t;
   trait_impls : trait_impl TraitImplId.Map.t;
+  source_files : string list FileNameMap.t;
 }
 [@@deriving show]

charon/src/bin/generate-ml/templates/GAstOfJson.ml

@@ -142,6 +142,7 @@ and gtranslated_crate_of_json
           ("crate_name", name);
           ("real_crate_name", _);
           ("id_to_file", id_to_file);
+          ("file_id_to_content", file_id_to_content);
           ("all_ids", _);
           ("item_names", _);
           ("type_decls", types);
@@ -185,6 +186,11 @@ and gtranslated_crate_of_json
             (trait_impl_of_json id_to_file)
             trait_impls
         in
+        let* source_files =
+          list_of_json
+            (key_value_pair_of_json file_id_of_json (list_of_json string_of_json))
+            file_id_to_content
+        in
 
         let type_decls =
           TypeDeclId.Map.of_list
@@ -208,6 +214,15 @@ and gtranslated_crate_of_json
           TraitImplId.Map.of_list
             (List.map (fun (d : trait_impl) -> (d.def_id, d)) trait_impls)
         in
+        let source_files =
+          FileNameMap.of_list
+            (List.filter_map
+               (fun (file_id, content) ->
+                 Option.map
+                   (fun filename -> (filename, content))
+                   (FileId.Map.find_opt file_id id_to_file))
+               source_files)
+        in
 
         Ok
           {
@@ -218,6 +233,7 @@ and gtranslated_crate_of_json
             global_decls;
             trait_decls;
             trait_impls;
+            source_files;
           }
     | _ -> Error "")
 

charon/src/bin/generate-ml/templates/LlbcOfJson.ml

@@ -112,5 +112,6 @@ let crate_of_json (js : json) : (crate, string) result =
         global_decls;
         trait_decls = crate.trait_decls;
         trait_impls = crate.trait_impls;
+        source_files = crate.source_files;
       }
   end

charon/src/bin/generate-ml/templates/Meta.ml

@@ -14,3 +14,17 @@ type path_buf = string
 
 (* __REPLACE0__ *)
 [@@deriving show, ord]
+
+(** Ordered file name *)
+module OrderedFileName : Collections.OrderedType with type t = file_name =
+struct
+  type t = file_name
+
+  let compare = compare_file_name
+  let to_string s = show_file_name s
+  let pp_t fmt s = pp_file_name fmt s
+  let show_t s = show_file_name s
+end
+
+module FileNameSet = Collections.MakeSet (OrderedFileName)
+module FileNameMap = Collections.MakeMap (OrderedFileName)