Store all incremental data into single file

src/framework/control.ml

@@ -304,11 +304,11 @@ struct
 
     GU.global_initialization := true;
     GU.earlyglobs := get_bool "exp.earlyglobs";
-    let marshal =
+    let marshal: Spec.marshal option =
       if get_string "load_run" <> "" then
         Some (Serialize.unmarshal Fpath.(v (get_string "load_run") / "spec_marshal"))
       else if Serialize.results_exist () && get_bool "incremental.load" then
-        Some (Serialize.load_data Serialize.AnalysisData)
+        Some (Obj.obj (Serialize.Cache.(get_data AnalysisDataRequest)))
       else
         None
     in
@@ -469,7 +469,7 @@ struct
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
           let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' in
           if GobConfig.get_bool "incremental.save" then
-            Serialize.store_data solver_data Serialize.SolverData;
+            Serialize.Cache.(update_data (SolverData (Obj.repr solver_data)));
           if save_run_str <> "" then (
             let save_run = Fpath.v save_run_str in
             let analyses = Fpath.(save_run / "analyses.marshalled") in
@@ -677,8 +677,8 @@ struct
       Serialize.marshal marshal Fpath.(v save_run / "spec_marshal")
     );
     if get_bool "incremental.save" then (
-      Serialize.store_data marshal Serialize.AnalysisData;
-      Serialize.move_tmp_results_to_results ()
+      Serialize.Cache.(update_data (AnalysisData (Obj.repr marshal)));
+      Serialize.Cache.store_data ()
     );
     if get_bool "dbg.verbose" && get_string "result" <> "none" then print_endline ("Generating output: " ^ get_string "result");
     Result.output (lazy local_xml) gh make_global_fast_xml file

src/incremental/maxIdUtil.ml

@@ -28,7 +28,3 @@ let get_file_max_ids (new_file: Cil.file) =
   let vid_max = ref 0 in
   Cil.iterGlobals new_file (fun g -> update_max_ids ~sid_max ~vid_max g);
   {max_sid = !sid_max; max_vid = !vid_max}
-
-(** Loads the max sid and vid from a previous run *)
-let load_max_ids () =
-  Serialize.load_data Serialize.VersionData

src/incremental/serialize.ml

@@ -1,10 +1,7 @@
 open Prelude
 
 (* TODO: GoblintDir *)
-let version_map_filename = "version.data"
-let cil_file_name = "ast.data"
-let solver_data_file_name = "solver.data"
-let analysis_data_file_name = "analysis.data"
+let incremental_data_file_name = "analysis.data"
 let results_dir = "results"
 let results_tmp_dir = "results_tmp"
 
@@ -43,49 +40,78 @@ let results_exist () =
   let r_str = Fpath.to_string r in
   Sys.file_exists r_str && Sys.is_directory r_str
 
-(* Convenience enumeration of the different data types we store for incremental analysis, so file-name logic is concentrated in one place *)
-type incremental_data_kind = SolverData | CilFile | VersionData | AnalysisData
-
-let type_to_file_name = function
-  | SolverData -> solver_data_file_name
-  | CilFile -> cil_file_name
-  | VersionData -> version_map_filename
-  | AnalysisData -> analysis_data_file_name
-
-(** Used by the server mode to avoid serializing the solver state to the filesystem *)
-let server_solver_data : Obj.t option ref = ref None
-let server_analysis_data : Obj.t option ref = ref None
-
-(** Loads data for incremental runs from the appropriate file *)
-let load_data (data_type: incremental_data_kind) =
-  if server () then
-    match data_type with
-    | SolverData -> !server_solver_data |> Option.get |> Obj.obj
-    | AnalysisData -> !server_analysis_data |> Option.get |> Obj.obj
-    | _ -> failwith "Can only load solver and analysis data"
-  else
-    let p = Fpath.(gob_results_dir Load / type_to_file_name data_type) in
-    unmarshal p
-
-(** Stores data for future incremental runs at the appropriate file, given the data and what kind of data it is. *)
-let store_data (data : 'a) (data_type : incremental_data_kind) =
-  if server () then
-    match data_type with
-    | SolverData -> server_solver_data := Some (Obj.repr data)
-    | AnalysisData -> server_analysis_data := Some (Obj.repr data)
-    | _ -> ()
-  else (
+(** Module to cache the data for incremental analaysis during a run, before it is stored to disk, as well as the server mode *)
+module Cache = struct
+  type t = {
+    solver_data: Obj.t option ref;
+    analysis_data: Obj.t option ref;
+    version_data: MaxIdUtil.max_ids option ref;
+    cil_file: Cil.file option ref;
+  }
+
+  let data = ref {
+      solver_data = ref None ;
+      analysis_data = ref None ;
+      version_data = ref None ;
+      cil_file = ref None ;
+    }
+
+  (* GADT that may be used to query data from the cache *)
+  type _ data_query =
+    | SolverDataRequest : Obj.t data_query
+    | CilFileRequest : Cil.file data_query
+    | VersionDataRequest : MaxIdUtil.max_ids data_query
+    | AnalysisDataRequest : Obj.t data_query
+
+  (* Data type to pass incremental data into the cache *)
+  type incremental_data =
+    | SolverData of Obj.t
+    | CilFile of Cil.file
+    | VersionData of MaxIdUtil.max_ids
+    | AnalysisData of Obj.t
+
+  (** Loads data for incremental runs from the appropriate file *)
+  let load_data () =
+    let p = Fpath.(gob_results_dir Load / incremental_data_file_name) in
+    let loaded_data = unmarshal p in
+    data := loaded_data
+
+  (** Stores data for future incremental runs at the appropriate file. *)
+  let store_data () =
     GobSys.mkdir_or_exists (gob_directory Save);
-    let d = gob_results_tmp_dir Save in
+    let d = gob_results_dir Save in
     GobSys.mkdir_or_exists d;
-    let p = Fpath.(d / type_to_file_name data_type) in
-    marshal data p)
-
-(** Deletes previous analysis results and moves the freshly created results there.*)
-let move_tmp_results_to_results () =
-  let op = Save in
-  if not (server ()) then (
-    if Sys.file_exists (Fpath.to_string (gob_results_dir op)) then begin
-      Goblintutil.rm_rf (gob_results_dir op);
-    end;
-    Sys.rename (Fpath.to_string (gob_results_tmp_dir op)) (Fpath.to_string (gob_results_dir op)))
+    let p = Fpath.(d / incremental_data_file_name) in
+    marshal !data p
+
+  (** Update the some incremental data in the in-memory cache *)
+  let update_data (d : incremental_data) = match d with
+    | SolverData s -> !data.solver_data := Some s
+    | AnalysisData a -> !data.analysis_data := Some a
+    | VersionData v -> !data.version_data := Some v
+    | CilFile c -> !data.cil_file := Some c
+
+  (** Reset some incremental data in the in-memory cache to [None]*)
+  let reset_data : type a. a data_query -> unit = function
+    | SolverDataRequest -> !data.solver_data := None
+    | AnalysisDataRequest -> !data.analysis_data := None
+    | VersionDataRequest -> !data.version_data := None
+    | CilFileRequest -> !data.cil_file := None
+
+  (** Get incremental data from the in-memory cache wrapped in an optional.
+      To populate the in-memory cache with data, call [load_data] first. *)
+  let get_opt_data : type a. a data_query -> a option = function
+    | SolverDataRequest -> !(!data.solver_data)
+    | AnalysisDataRequest -> !(!data.analysis_data)
+    | VersionDataRequest -> !(!data.version_data)
+    | CilFileRequest -> !(!data.cil_file)
+
+  (** Get incremental data from the in-memory cache.
+      Same as [get_opt_data], except not yielding an optional and failing when the requested data is not present.
+      To populate the in-memory cache with data, call [load_data] first. *)
+  let get_data : type a. a data_query -> a =
+    fun a ->
+    match get_opt_data a with
+    | Some d -> d
+    | None -> failwith "Requested data is not loaded."
+end

src/maingoblint.ml

@@ -532,9 +532,10 @@ let diff_and_rename current_file =
     end;
     let (changes, old_file, max_ids) =
       if Serialize.results_exist () && GobConfig.get_bool "incremental.load" then begin
-        let old_file = Serialize.load_data Serialize.CilFile in
+        Serialize.Cache.load_data ();
+        let old_file = Serialize.Cache.(get_data CilFileRequest) in
         let changes = CompareCIL.compareCilFiles old_file current_file in
-        let max_ids = MaxIdUtil.load_max_ids () in
+        let max_ids = Serialize.Cache.(get_data VersionDataRequest) in
         let max_ids = UpdateCil.update_ids old_file max_ids current_file changes in
         (changes, Some old_file, max_ids)
       end else begin
@@ -543,12 +544,12 @@ let diff_and_rename current_file =
       end
     in
     let solver_data = if Serialize.results_exist () && GobConfig.get_bool "incremental.load" && not (GobConfig.get_bool "incremental.only-rename")
-      then Some (Serialize.load_data Serialize.SolverData)
+      then Some Serialize.Cache.(get_data SolverDataRequest)
       else None
     in
     if GobConfig.get_bool "incremental.save" then begin
-      Serialize.store_data current_file Serialize.CilFile;
-      Serialize.store_data max_ids Serialize.VersionData
+      Serialize.Cache.(update_data (CilFile current_file));
+      Serialize.Cache.(update_data (VersionData max_ids));
     end;
     let old_data = match old_file, solver_data with
       | Some cil_file, Some solver_data -> Some ({cil_file; solver_data}: Analyses.analyzed_data)

src/util/server.ml

@@ -126,7 +126,7 @@ let virtual_changes file =
   in
   CompareCIL.compareCilFiles ~eq file file
 
-let increment_data (s: t) file reparsed = match !Serialize.server_solver_data with
+let increment_data (s: t) file reparsed = match Serialize.Cache.get_opt_data SolverDataRequest with
   | Some solver_data when reparsed ->
     let changes = CompareCIL.compareCilFiles s.file file in
     let old_data = Some { Analyses.cil_file = s.file; solver_data } in
@@ -145,8 +145,8 @@ let analyze ?(reset=false) (s: t) =
   if reset then (
     let max_ids = MaxIdUtil.get_file_max_ids file in
     s.max_ids <- max_ids;
-    Serialize.server_solver_data := None;
-    Serialize.server_analysis_data := None);
+    Serialize.Cache.reset_data SolverDataRequest;
+    Serialize.Cache.reset_data AnalysisDataRequest);
   let increment_data, fresh = increment_data s file reparsed in
   Cilfacade.reset_lazy ();
   WideningThresholds.reset_lazy ();