Merge pull request #748 from goblint/issue_357_new

Store all incremental data into single file

Author: jerhard

src/framework/control.ml

@@ -312,11 +312,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 (Serialize.Cache.(get_data AnalysisData))
       else
         None
     in
@@ -475,7 +475,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 solver_data);
           if save_run_str <> "" then (
             let save_run = Fpath.v save_run_str in
             let analyses = Fpath.(save_run / "analyses.marshalled") in
@@ -691,8 +691,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 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,12 +1,8 @@
 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"
 
 type operation = Save | Load
 
@@ -21,9 +17,6 @@ let gob_directory op =
 let gob_results_dir op =
   Fpath.(gob_directory op / results_dir)
 
-let gob_results_tmp_dir op =
-  Fpath.(gob_directory op / results_tmp_dir)
-
 let server () = GobConfig.get_bool "server.enabled"
 
 let marshal obj fileName  =
@@ -43,49 +36,70 @@ 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 for the server mode *)
+module Cache = struct
+  type t = {
+    mutable solver_data: Obj.t option;
+    mutable analysis_data: Obj.t option;
+    mutable version_data: MaxIdUtil.max_ids option;
+    mutable cil_file: Cil.file option;
+  }
+
+  let data = ref {
+      solver_data = None;
+      analysis_data = None;
+      version_data = None;
+      cil_file = None;
+    }
+
+  (** GADT that may be used to query data from and pass data to the cache. *)
+  type _ data_query =
+    | SolverData : _ data_query
+    | CilFile : Cil.file data_query
+    | VersionData : MaxIdUtil.max_ids data_query
+    | AnalysisData : _ data_query
+
+  (** 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 incremental data in the in-memory cache *)
+  let update_data: type a. a data_query -> a -> unit = fun q d -> match q with
+    | SolverData -> !data.solver_data <- Some (Obj.repr d)
+    | AnalysisData -> !data.analysis_data <- Some (Obj.repr d)
+    | VersionData -> !data.version_data <- Some d
+    | CilFile -> !data.cil_file <- Some d
+
+  (** Reset some incremental data in the in-memory cache to [None]*)
+  let reset_data : type a. a data_query -> unit = function
+    | SolverData -> !data.solver_data <- None
+    | AnalysisData -> !data.analysis_data <- None
+    | VersionData -> !data.version_data <- None
+    | CilFile -> !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
+    | SolverData -> Option.map Obj.obj !data.solver_data
+    | AnalysisData -> Option.map Obj.obj !data.analysis_data
+    | VersionData -> !data.version_data
+    | CilFile -> !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. *)
+  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

@@ -512,9 +512,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 CilFile) 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 VersionData) in
         let max_ids = UpdateCil.update_ids old_file max_ids current_file changes in
         (changes, Some old_file, max_ids)
       end else begin
@@ -523,12 +524,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 SolverData)
       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 ({solver_data}: Analyses.analyzed_data)

src/util/server.ml

@@ -123,7 +123,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 SolverData with
   | Some solver_data when reparsed ->
     let changes = CompareCIL.compareCilFiles s.file file in
     let old_data = Some { Analyses.solver_data } in
@@ -142,8 +142,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 SolverData;
+    Serialize.Cache.reset_data AnalysisData);
   let increment_data, fresh = increment_data s file reparsed in
   Cilfacade.reset_lazy ();
   WideningThresholds.reset_lazy ();