Merge branch 'feature/andre/json-cache-merge' into 'master'

add JSON cache and merge functions

See merge request frama-c/frama-c!2977

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 ../../.."

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

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
+
 }