From fd9962c44f99a01ec5881b61bd127b485aff4cd8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 2 Dec 2020 14:34:49 +0100
Subject: [PATCH] [Json] add JSON cache and merge functions
---
src/kernel_internals/runtime/special_hooks.ml | 9 ++
src/libraries/utils/json.mli | 64 +++++++++++++
src/libraries/utils/json.mll | 90 +++++++++++++++++++
3 files changed, 163 insertions(+)
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 9161ca6e6d6..de0cf6026b6 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -221,6 +221,15 @@ let run_list_all_plugin_options () =
else Cmdline.nop
let () = Cmdline.run_after_exiting_stage run_list_all_plugin_options
+(* Write JSON files to disk if required *)
+let flush_json_files () =
+ let written = Json.flush_cache () in
+ List.iter (fun fp ->
+ Kernel.feedback "Wrote: %a" Filepath.Normalized.pretty fp)
+ written
+
+let () = Cmdline.at_normal_exit (fun () -> flush_json_files ())
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index f374ebf853b..80ffaf64513 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -125,3 +125,67 @@ val field : string -> t -> t
[Null] is considered an empty object.
@raise Not_found if the field is absent from the object.
@raise Invalid_argument if the object is not an [Assoc] or [Null] object. *)
+
+(** The functions below read and write to JSON files asynchronously; they are
+ intended to be called at different times during execution.
+ To avoid reopening, re-reading and rewriting the same file several times,
+ they instead operate as following:
+ - Read the file on first use, and store it in memory;
+ - Perform merge operations using the in-memory representations;
+ - Flush the final form to disk before quitting Frama-C.
+ The latter is done via function [json_flush_cache] below, which is setup
+ to run with an [at_exit] trigger.
+
+ Note: no other functions should modify the contents of [path]; any
+ modifications will be overwritten when the cache is flushed.
+
+ @since Frama-C+dev
+*)
+
+(** Exception raised by the functions below when incompatible types are
+ merged. *)
+exception CannotMerge of string
+
+(**
+ [merge_object path json_obj] recursively merges the object [json_obj] into the
+ JSON file [path]. If [path] does not exist, it is created.
+ Merge consists in combining values with the same key, e.g. if [path]
+ already contains an object {"kernel": {"options": ["a"]}}, and
+ [json_obj] is {"kernel": {"options": ["b"]}}, the result will be
+ {"kernel": {"options": ["a", "b"]}}. Cannot merge heterogeneous
+ objects, i.e. in the previous example, if "options" were associated
+ with a string in [path], trying to merge an array into it would
+ raise [JsonCannotMerge].
+ The merged object is updated in the memory cache.
+
+ @raise [CannotMerge] if the objects have conflicting types for
+ the same keys, or if the root JSON element is not an object.
+ @since Frama-C+dev
+*)
+val merge_object : Filepath.Normalized.t -> Yojson.Basic.t -> unit
+
+(**
+ [merge_list path json_array] merges the array [json_array] into the
+ JSON file [path]. See [merge_object] for more details.
+ Unlike objects, arrays are merged by simply concatenating their list
+ of elements.
+
+ @raise [CannotMerge] if the root JSON element is not an array.
+ @since Frama-C+dev
+*)
+val merge_array : Filepath.Normalized.t -> Yojson.Basic.t -> unit
+
+(**
+ [from_file path] opens [path] and stores its JSON object in
+ a memory cache, to be used by the other related functions.
+ @since Frama-C+dev
+*)
+val from_file: Filepath.Normalized.t -> Yojson.Basic.t
+
+(**
+ Flushes the JSON objects in the cache. Returns the names of the written
+ files.
+
+ @since Frama-C+dev
+*)
+val flush_cache : unit -> Filepath.Normalized.t list
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index f17c82ac25d..7368c65f3e4 100644
--- a/src/libraries/utils/json.mll
+++ b/src/libraries/utils/json.mll
@@ -296,4 +296,94 @@ let of_list xs = `List xs
let of_array xs = `List (Array.to_list xs)
let of_fields m = `Assoc m
+
+(* JSON file cache and merging *)
+
+exception CannotMerge of string
+
+(* Table of filepaths to JSON arrays, to be written at the end of a run *)
+let json_tbl = Hashtbl.create 3
+
+let rec merge_assoc_lists la lb =
+ let cmp = fun (k1, _) (k2, _) -> String.compare k1 k2 in
+ let rec aux acc l1 l2 =
+ match l1, l2 with
+ | [], [] -> acc
+ | [], l | l, [] -> List.rev_append l acc
+ | e1 :: r1, e2 :: r2 ->
+ let c = cmp e1 e2 in
+ if c < 0 then aux (e1 :: acc) r1 l2
+ else if c > 0 then aux (e2 :: acc) l1 r2
+ else (* c = 0 *)
+ let (k1, v1) = e1 in
+ let (_, v2) = e2 in
+ match v1, v2 with
+ | `Assoc a1, `Assoc a2 ->
+ let v = `Assoc (merge_assoc_lists a1 a2) in
+ aux ((k1, v) :: acc) r1 r2
+ | `List l1, `List l2 ->
+ let v = `List (l1 @ l2) in
+ aux ((k1, v) :: acc) r1 r2
+ | o1, o2 ->
+ let pp = Yojson.Basic.pretty_to_string in
+ raise (CannotMerge
+ ("cannot merge heterogeneous objects '"
+ ^ pp o1 ^ "' and '" ^ pp o2 ^ "'"))
+ in
+ let r = aux [] (List.sort cmp la) (List.sort cmp lb) in
+ List.rev r
+
+let merge_object path json_root_obj =
+ let open Yojson.Basic.Util in
+ let existing_root_obj =
+ try
+ match Hashtbl.find json_tbl path with
+ | `Assoc _ as root -> root
+ | _ -> raise (CannotMerge "JSON root element should be an object")
+ with Not_found ->
+ `Assoc []
+ in
+ let existing_assoc = existing_root_obj |> to_assoc in
+ let new_assoc = json_root_obj |> to_assoc in
+ let merged = merge_assoc_lists existing_assoc new_assoc in
+ let merged_obj = `Assoc merged in
+ Hashtbl.replace json_tbl path merged_obj
+
+let merge_array path json_root_array =
+ let open Yojson.Basic.Util in
+ let existing_root_array =
+ try
+ match Hashtbl.find json_tbl path with
+ | `List _ as root -> root
+ | _ -> raise (CannotMerge "JSON root element should be an array")
+ with Not_found ->
+ `List []
+ in
+ let existing_list = existing_root_array |> to_list in
+ let new_list = json_root_array |> to_list in
+ let merged_list = `List (existing_list @ new_list) in
+ Hashtbl.replace json_tbl path merged_list
+
+let flush_cache () =
+ let written =
+ Hashtbl.fold (fun (path : Filepath.Normalized.t) json acc ->
+ let oc = open_out (path:>string) in
+ Yojson.Basic.pretty_to_channel oc json;
+ output_char oc '\n'; (* ensure JSON file terminates with a newline *)
+ path :: acc
+ ) json_tbl []
+ in
+ Hashtbl.clear json_tbl;
+ List.rev written
+
+let json_cache = Hashtbl.create 3
+
+let from_file (path : Filepath.Normalized.t) =
+ try
+ Hashtbl.find json_cache path
+ with Not_found ->
+ let json = Yojson.Basic.from_file (path:>string) in
+ Hashtbl.replace json_cache path json;
+ json
+
}
--
GitLab