Source file gobConfig.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
(** Configuration access. *)
(**
New, untyped, path-based configuration subsystem.
{v
path' ::== \epsilon (* *)
| . <field-name> path' (* field access *)
| [ <index-nr> ] path' (* array index access *)
| [ + ] path' (* cons to array *)
| [ - ] path' (* cons away from array *)
| [ * ] path' (* reset array *)
path ::== path' (* *)
| <field_name> path' (* you can leave out the first dot *)
v}
All functions [failwith] on error. Warnings are generated in [verbose] mode.
There is a "conf" [trace] option that traces setting.
*)
open Batteries
open Printf
exception ConfigError of string
let building_spec = ref false
module Validator = JsonSchema.Validator (struct let schema = Options.schema end)
module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Options.require_all end)
(** The type for [gobConfig] module. *)
module type S =
sig
(** Get JSON value at a given path. *)
val get_json : string -> Yojson.Safe.t
(** Directly set a JSON value; the result must conform to the schema. *)
val set_json : string -> Yojson.Safe.t -> unit
(** Equivalent to [get_json ""]. *)
val get_conf : unit -> Yojson.Safe.t
(** Equivalent to [set_conf ""]. *)
val set_conf : Yojson.Safe.t -> unit
(** Functions to query conf variable of type int. *)
val get_int : string -> int
(** Functions to modify conf variables of type int. *)
val set_int : string -> int -> unit
(** Functions to query conf variable of type bool. *)
val get_bool : string -> bool
(** Functions to modify conf variables of type bool. *)
val set_bool : string -> bool -> unit
(** Functions to query conf variable of type string. *)
val get_string : string -> string
(** Functions to modify conf variables of type string. *)
val set_string : string -> string -> unit
(** Functions to modify conf variables by trying to parse the value.
The second argument must be valid Json except single quotes represent double quotes. *)
val set_auto : string -> string -> unit
(** Get a list of values *)
val get_list : string -> Yojson.Safe.t list
(** Get a list of strings *)
val get_string_list : string -> string list
(** Set a list of values *)
val set_list : string -> Yojson.Safe.t list -> unit
(** Write the current configuration to [filename] *)
val write_file: Fpath.t -> unit
(** Merge configurations from a file with current. *)
val merge_file : Fpath.t -> unit
(** Merge configurations from a JSON object with current. *)
val merge : Yojson.Safe.t -> unit
(** Check whether modification of configuration is currently allowed. *)
val is_immutable : unit -> bool
(** Run the given computation with modification to configuration disabled. *)
val with_immutable_conf : (unit -> 'a) -> 'a
end
(** The implementation of the [gobConfig] module. *)
module Impl : S =
struct
(** raise when you cannot parse the path *)
exception PathParseError
(** raise when there is an type error *)
exception ConfTypeError
(** Type of the index *)
type index = Int of int (** and integer *)
| App (** prepend to the list *)
| Rem (** remove from the list *)
| New (** create a new list *)
(** Type of the path *)
type path = Here (** we are there *)
| Select of string * path (** we need to select an field *)
| Index of index * path (** we need to select an array index *)
let show_path p =
let rec helper = function
| Here -> []
| Select (s, p) -> Printf.sprintf ".%s" s :: helper p
| Index (Int i, p) -> Printf.sprintf "[%d]" i :: helper p
| Index (App, p) -> "[+]" :: helper p
| Index (Rem, p) -> "[-]" :: helper p
| Index (New, p) -> "[*]" :: helper p
in
String.concat "" (helper p)
(** raise when an attempt is made to modify the configuration while it is immutable *)
exception Immutable of path
let () =
Printexc.register_printer @@
function
| Immutable p -> Some (Printf.sprintf "Immutable(%s)" (show_path p))
| _ -> None
(** Helper function [split c1 c2 xs] that splits [xs] on [c1] or [c2] *)
let split c1 c2 xs =
let l = String.length xs in
let rec split' i =
if i<l then begin
if xs.[i]=c1 || xs.[i]=c2 then
(Str.first_chars xs i, Str.string_after xs i)
else
split' (i+1)
end else
(xs,"")
in
split' 0
(** Parse an index. *)
let parse_index s =
try if s = "+" then App
else if s = "*" then New
else if s = "-" then Rem
else Int (int_of_string s)
with Failure _ -> raise PathParseError
(** Parse a string path. *)
let rec parse_path' (s:string) : path =
if String.length s = 0 then Here else
match s.[0] with
| '.' ->
let fld, pth = split '.' '[' (String.lchop s) in
Select (fld, parse_path' pth)
| '[' ->
let idx, pth = String.split (String.lchop s) ~by:"]" in
Index (parse_index idx, parse_path' pth)
| _ -> raise PathParseError
(** Parse a string path, but you may ignore the first dot.
@raise Failure if path couldn't be parsed. *)
let parse_path (s:string) : path =
let s = String.trim s in
try
if String.length s = 0 then Here else begin
let fld, pth = split '.' '[' s in
if fld = ""
then parse_path' pth
else Select (fld, parse_path' pth)
end
with PathParseError ->
Logs.error "Error: Couldn't parse the json path '%s'" s;
failwith "parsing"
(** Here we store the actual configuration. *)
let json_conf : Yojson.Safe.t ref = ref `Null
(** Helper function to print the conf using [printf "%t"] and alike. *)
let print ch : unit =
GobYojson.print ch !json_conf
let write_file filename = File.with_file_out (Fpath.to_string filename) print
(** Main function to receive values from the conf. *)
let rec get_value (o : Yojson.Safe.t) pth =
match o, pth with
| o, Here -> o
| `Assoc m, Select (key,pth) ->
begin
try get_value (List.assoc key m) pth
with Not_found ->
try get_value (List.assoc Options.defaults_additional_field m) pth
with Not_found -> raise ConfTypeError
end
| `List a, Index (Int i, pth) ->
begin
try get_value (List.at a i) pth
with Invalid_argument _ -> raise ConfTypeError
end
| _, _ -> raise ConfTypeError
(** Recursively create the value for some new path. *)
let rec create_new v = function
| Here -> v
| Select (key,pth) -> `Assoc [(key,create_new v pth)]
| Index (_, pth) -> `List [create_new v pth]
(** Helper function to decide if types in the json conf have changed. *)
let json_type_equals x y =
match x, y with
| `String _, `String _
| `Int _, `Int _
| `Int _, `Intlit _
| `Intlit _, `Int _
| `Intlit _, `Intlit _
| `Assoc _, `Assoc _
| `List _, `List _
| `Bool _ , `Bool _
| `Null , `Null -> true
| _ -> false
exception TypeError of Yojson.Safe.t * Yojson.Safe.t
let () = Printexc.register_printer (function
| TypeError (o, new_v) ->
Some (sprintf2 "GobConfig.Impl.TypeError (%a, %a)" GobYojson.print o GobYojson.print new_v)
| _ -> None
)
(** (Global) flag to disallow modification of the configuration. *)
let immutable = ref false
let set_immutable = (:=) immutable
let is_immutable () = !immutable
let with_immutable_conf f =
if is_immutable () then f ()
else (
set_immutable true;
Fun.protect ~finally:(fun () -> set_immutable false) f
)
(** The main function to write new values into the conf. Use [set_value] to properly invalidate cache and check immutability.
@raise Failure
@raise TypeError
@raise Invalid_argument
@raise Json_encoding.Cannot_destruct *)
let unsafe_set_value v o orig_pth =
let rec set_value v o pth =
match o, pth with
| `Assoc m, Select (key,pth) ->
let rec modify = function
| [] ->
[(key, create_new v pth)]
| (key', v') :: kvs when key' = key ->
(key, set_value v v' pth) :: kvs
| (key', v') :: kvs ->
(key', v') :: modify kvs
in
`Assoc (modify m)
| `List a, Index (Int i, pth) ->
`List (List.modify_at i (fun o -> set_value v o pth) a)
| `List a, Index (App, pth) ->
`List (a @ [create_new v pth])
| `List a, Index (Rem, pth) ->
let original_list = a in
let excluded_elem = create_new v pth in
let filtered_list =
List.filter (fun elem ->
match (elem, excluded_elem) with
| (`String s1, `String s2) -> not (String.equal s1 s2)
| (_, _) -> failwith "At the moment it's only possible to remove a string from an array."
) original_list
in
`List filtered_list
| `List _, Index (New, pth) ->
`List [create_new v pth]
| `Null, _ ->
create_new v pth
| _ ->
let new_v = create_new v pth in
if not (json_type_equals o new_v) then
raise (TypeError (o, new_v));
new_v
in
o := set_value v !o orig_pth;
Validator.validate_exn !json_conf
(** Helper function for reading values. Handles error messages. *)
let get_path_string f st =
try
let st = String.trim st in
let x = get_value !json_conf (parse_path st) in
if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a." st GobYojson.pretty x;
try f x
with Yojson.Safe.Util.Type_error (s, _) ->
Logs.error "The value for '%s' has the wrong type: %s" st s;
failwith "get_path_string"
with ConfTypeError ->
Logs.Batteries.error "Cannot find value '%s' in\n%t\nDid You forget to add default values to options.schema.json?"
st print;
failwith "get_path_string"
let get_json : string -> Yojson.Safe.t = get_path_string Fun.id
let get_conf () = get_json ""
(** Convenience functions for reading values. *)
let memo gen = BatCache.make_ht ~gen ~init_size:5
let memog f = memo @@ get_path_string f
let memo_int = memog Yojson.Safe.Util.to_int
let memo_bool = memog Yojson.Safe.Util.to_bool
let memo_string = memog Yojson.Safe.Util.to_string
let memo_list = memog Yojson.Safe.Util.to_list
let drop_memo () =
let drop:'a. (string,'a) BatCache.manual_cache -> _ = fun m ->
let r = m.enum () in
BatEnum.force r; BatEnum.iter (fun (k,v) -> m.del k) r
in
drop memo_int; drop memo_bool; drop memo_string; drop memo_list
let wrap_get f x =
if !building_spec && Goblint_tracing.tracing then Goblint_tracing.trace "config" "get during building_spec: %s" x;
f x
let get_int = wrap_get memo_int.get
let get_bool = wrap_get memo_bool.get
let get_string = wrap_get memo_string.get
let get_list = wrap_get memo_list.get
let get_string_list = List.map Yojson.Safe.Util.to_string % get_list
(** Helper functions for writing values. *)
(** Sets a value, preventing changes when the configuration is immutable and invalidating the cache.
@raise Immutable *)
let set_value v o pth =
if is_immutable () then raise (Immutable pth);
drop_memo ();
unsafe_set_value v o pth
(** Helper function for writing values. Handles the tracing.
@raise Failure if path couldn't be parsed.
@raise Immutable
@raise TypeError
@raise Invalid_argument
@raise Json_encoding.Cannot_destruct *)
let set_path_string st v =
if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pretty v;
set_value v json_conf (parse_path st)
let set_json st j =
set_path_string st j;
ValidatorRequireAll.validate_exn !json_conf
let set_conf = set_json ""
(** Convenience functions for writing values. *)
let set_int st i = set_path_string st (`Int i)
let set_bool st i = set_path_string st (`Bool i)
let set_string st i = set_path_string st (`String i)
let set_list st l = set_path_string st (`List l)
(** The ultimate convenience function for writing values. *)
let one_quote = Str.regexp "\'"
let set_auto st s =
try
try
let s' = Str.global_replace one_quote "\"" s in
let v = Yojson.Safe.from_string s' in
set_path_string st v
with Yojson.Json_error _ | TypeError _ ->
set_string st s
with
| Failure _
| Immutable _
| TypeError _
| Invalid_argument _
| Json_encoding.Cannot_destruct _ as e ->
let bt = Printexc.get_raw_backtrace () in
Logs.error "Cannot set %s to '%s'." st s;
Printexc.raise_with_backtrace e bt
let merge json =
Validator.validate_exn json;
set_conf (GobYojson.merge !json_conf json)
(** Merge configurations form a file with current. *)
let merge_file fn =
let cwd = Fpath.v (Sys.getcwd ()) in
let config_dirs = cwd :: Fpath.(parent (v Sys.executable_name)) :: Goblint_sites.conf in
let file = List.find_map_opt (fun custom_include_dir ->
let path = Fpath.append custom_include_dir fn in
if Sys.file_exists (Fpath.to_string path) then
Some path
else
None
) config_dirs
in
match file with
| Some fn ->
let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in (Fpath.to_string fn) in
merge v;
if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a." GobFpath.pretty fn GobYojson.pretty !json_conf
| None -> raise (Sys_error (Printf.sprintf "%s: No such file or diretory" (Fpath.to_string fn)))
end
include Impl
let () = set_conf Options.defaults
(** Another hack to see if earlyglobs is enabled *)
let earlyglobs = ref false
let jobs () =
match get_int "jobs" with
| 0 -> Cpu.numcores ()
| n -> n