package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file serialize.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
(** Serialization/deserialization of incremental analysis data. *)

open Batteries

(* TODO: GoblintDir *)
let incremental_data_file_name = "analysis.data"
let results_dir = "results"

type operation = Save | Load

(** Returns the name of the directory used for loading/saving incremental data *)
let incremental_dirname op = match op with
  | Load -> GobConfig.get_string "incremental.load-dir"
  | Save -> GobConfig.get_string "incremental.save-dir"

let gob_directory op =
  GobFpath.cwd_append (Fpath.v (incremental_dirname op))

let gob_results_dir op =
  Fpath.(gob_directory op / results_dir)

let server () = GobConfig.get_bool "server.enabled"

let marshal obj fileName  =
  let chan = open_out_bin (Fpath.to_string fileName) in
  Marshal.output chan obj;
  close_out chan

let unmarshal fileName =
  Logs.debug "Unmarshalling %s... If type of content changed, this will result in a segmentation fault!" (Fpath.to_string fileName);
  Marshal.input (open_in_bin (Fpath.to_string fileName))

let results_exist () =
  (* If Goblint did not crash irregularly, the existence of the result directory indicates that there are results *)
  let r = gob_results_dir Load in
  let r_str = Fpath.to_string r in
  Sys.file_exists r_str && Sys.is_directory r_str

(** 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: GoblintCil.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 : GoblintCil.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_dir Save in
    GobSys.mkdir_or_exists d;
    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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct