diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index 484dde4e..6d2f3928 100644 --- a/charon-ml/src/GAst.ml +++ b/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] diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index e7bd45c0..61f42f10 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/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 "") diff --git a/charon-ml/src/LlbcOfJson.ml b/charon-ml/src/LlbcOfJson.ml index 803c14ea..23c5fbe0 100644 --- a/charon-ml/src/LlbcOfJson.ml +++ b/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 diff --git a/charon-ml/src/Meta.ml b/charon-ml/src/Meta.ml index e911f2a3..63cd40b7 100644 --- a/charon-ml/src/Meta.ml +++ b/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) diff --git a/charon-ml/src/OfJsonBasic.ml b/charon-ml/src/OfJsonBasic.ml index 03d9719c..ce52b6c8 100644 --- a/charon-ml/src/OfJsonBasic.ml +++ b/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) diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index e85a8128..fc9dde2c 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -96,6 +96,14 @@ pub struct TranslatedCrate { #[charon::opaque] pub file_to_id: HashMap, + /// 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::>")] + pub file_id_to_content: HashMap>, + /// All the ids, in the order in which we encountered them #[drive(skip)] pub all_ids: LinkedHashSet, diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index dd4d1f53..8b53b18b 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/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> { + 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::, _>>() + .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, diff --git a/charon/src/bin/generate-ml/templates/GAst.ml b/charon/src/bin/generate-ml/templates/GAst.ml index 742de9db..f0131244 100644 --- a/charon/src/bin/generate-ml/templates/GAst.ml +++ b/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] diff --git a/charon/src/bin/generate-ml/templates/GAstOfJson.ml b/charon/src/bin/generate-ml/templates/GAstOfJson.ml index 7e4f3f3f..5db9dc61 100644 --- a/charon/src/bin/generate-ml/templates/GAstOfJson.ml +++ b/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 "") diff --git a/charon/src/bin/generate-ml/templates/LlbcOfJson.ml b/charon/src/bin/generate-ml/templates/LlbcOfJson.ml index 45826868..15df0fce 100644 --- a/charon/src/bin/generate-ml/templates/LlbcOfJson.ml +++ b/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 diff --git a/charon/src/bin/generate-ml/templates/Meta.ml b/charon/src/bin/generate-ml/templates/Meta.ml index 35b1a0f2..56173ba3 100644 --- a/charon/src/bin/generate-ml/templates/Meta.ml +++ b/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)