Source file maingoblint.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
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
(** This is the main program! *)
open Prelude
open GobConfig
open Defaults
open Printf
open Goblintutil
let writeconffile = ref ""
(** Print version and bail. *)
let print_version ch =
let open Version in let open Config in
let f ch b = if b then fprintf ch "enabled" else fprintf ch "disabled" in
printf "Goblint version: 1.1.1 (%s)\n" goblint;
printf "Cil version: %s\n" Cil.cilVersion;
printf "Configuration: tracing %a\n" f tracing;
exit 0
(** Print helpful messages. *)
let print_help ch =
fprintf ch "Usage: goblint [options] source-files\nOptions\n";
fprintf ch " -v Prints more status information. \n";
fprintf ch " -o <file> Prints the output to file. \n";
fprintf ch " -I <dir> Add include directory. \n";
fprintf ch " -IK <dir> Add kernel include directory. \n\n";
fprintf ch " --help Prints this text \n";
fprintf ch " --version Print out current version information. \n\n";
fprintf ch " --conf <file> Merge the configuration from the <file>. \n";
fprintf ch " --writeconf <file> Write the effective configuration to <file> \n";
fprintf ch " --set <jpath> <jvalue> Set a configuration variable <jpath> to the specified <jvalue>.\n";
fprintf ch " --sets <jpath> <string> Set a configuration variable <jpath> to the string.\n";
fprintf ch " --enable <jpath> Set a configuration variable <jpath> to true. \n";
fprintf ch " --disable <jpath> Set a configuration variable <jpath> to false. \n\n";
fprintf ch " --print_options Print out commonly used configuration variables.\n";
fprintf ch " --print_all_options Print out all configuration variables. \n";
fprintf ch "\n";
fprintf ch "A <jvalue> is a string from the JSON language where single-quotes (')";
fprintf ch " are used instead of double-quotes (\").\n\n";
fprintf ch "A <jpath> is a path in a json structure. E.g. 'field.another_field[42]';\n";
fprintf ch "in addition to the normal syntax you can use 'field[+]' append to an array.\n\n";
exit 0
let create_temp_dir () =
if Sys.file_exists (get_string "tempDir") then
Goblintutil.tempDirName := get_string "tempDir"
else
let tmpDirRel = Filename.temp_file ~temp_dir:"" "goblint_temp_" "" in
Sys.remove tmpDirRel;
let tmpDirName = create_dir tmpDirRel in
Goblintutil.tempDirName := tmpDirName
let remove_temp_dir () =
if not (get_bool "keepcpp") then ignore (Goblintutil.rm_rf !Goblintutil.tempDirName)
(** [Arg] option specification *)
let option_spec_list =
let add_string l = let f str = l := str :: !l in Arg.String f in
let add_int l = let f str = l := str :: !l in Arg.Int f in
let set_trace sys =
let msg = "Goblint has been compiled without tracing, run ./scripts/trace_on.sh to recompile." in
if Config.tracing then Tracing.addsystem sys
else (prerr_endline msg; raise Exit)
in
let oil file =
set_string "ana.osek.oil" file;
set_auto "ana.activated" "['base','threadid','threadflag','escape','OSEK','OSEK2','stack_trace_set','fmode','flag','mallocWrapper']";
set_auto "mainfun" "[]"
in
let configure_html () =
if (get_string "outfile" = "") then
set_string "outfile" "result";
if get_string "exp.g2html_path" = "" then
set_string "exp.g2html_path" exe_dir;
set_bool "dbg.print_dead_code" true;
set_bool "exp.cfgdot" true;
set_bool "g2html" true;
set_string "result" "fast_xml"
in
let configure_sarif () =
if (get_string "outfile" = "") then
set_string "outfile" "goblint.sarif";
set_bool "dbg.print_dead_code" true;
set_string "result" "sarif"
in
let tmp_arg = ref "" in
[ "-o" , Arg.String (set_string "outfile"), ""
; "-v" , Arg.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), ""
; "-I" , Arg.String (set_string "includes[+]"), ""
; "-IK" , Arg.String (set_string "kernel_includes[+]"), ""
; "--set" , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> set_auto !tmp_arg x)], ""
; "--sets" , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> prerr_endline "--sets is deprecated, use --set instead."; set_string !tmp_arg x)], ""
; "--enable" , Arg.String (fun x -> set_bool x true), ""
; "--disable" , Arg.String (fun x -> set_bool x false), ""
; "--conf" , Arg.String merge_file, ""
; "--writeconf" , Arg.String (fun fn -> writeconffile := fn), ""
; "--version" , Arg.Unit print_version, ""
; "--print_options" , Arg.Unit (fun _ -> printCategory stdout Std; exit 0), ""
; "--print_all_options" , Arg.Unit (fun _ -> printAllCategories stdout; exit 0), ""
; "--trace" , Arg.String set_trace, ""
; "--tracevars" , add_string Tracing.tracevars, ""
; "--tracelocs" , add_int Tracing.tracelocs, ""
; "--help" , Arg.Unit (fun _ -> print_help stdout),""
; "--html" , Arg.Unit (fun _ -> configure_html ()),""
; "--sarif" , Arg.Unit (fun _ -> configure_sarif ()),""
; "--compare_runs" , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> set_auto "compare_runs" (sprintf "['%s','%s']" !tmp_arg x))], ""
; "--oil" , Arg.String oil, ""
; "--osekdefaults" , Arg.Unit (fun () -> set_bool "ana.osek.defaults" false), ""
; "--osektaskprefix" , Arg.String (set_string "ana.osek.taskprefix"), ""
; "--osekisrprefix" , Arg.String (set_string "ana.osek.isrprefix"), ""
; "--osektasksuffix" , Arg.String (set_string "ana.osek.tasksuffix"), ""
; "--osekisrsuffix" , Arg.String (set_string "ana.osek.isrsuffix"), ""
; "--osekcheck" , Arg.Unit (fun () -> set_bool "ana.osek.check" true), ""
; "--oseknames" , Arg.Set_string OilUtil.osek_renames, ""
; "--osekids" , Arg.Set_string OilUtil.osek_ids, ""
]
(** List of C files to consider. *)
let cFileNames = ref []
(** Parse arguments and fill [cFileNames] and [jsonFiles]. Print help if needed. *)
let parse_arguments () =
let jsonRegex = Str.regexp ".+\\.json$" in
let recordFile fname =
if Str.string_match jsonRegex fname 0
then Goblintutil.jsonFiles := fname :: !Goblintutil.jsonFiles
else cFileNames := fname :: !cFileNames
in
Arg.parse option_spec_list recordFile "Look up options using 'goblint --help'.";
if !writeconffile <> "" then (GobConfig.write_file !writeconffile; raise Exit)
(** Initialize some globals in other modules. *)
let handle_flags () =
let has_oil = get_string "ana.osek.oil" <> "" in
if has_oil then Osek.Spec.parse_oil ();
if get_bool "dbg.verbose" then (
Printexc.record_backtrace true;
Errormsg.debugFlag := true;
Errormsg.verboseFlag := true
);
match get_string "dbg.dump" with
| "" -> ()
| path ->
Messages.formatter := Format.formatter_of_out_channel (Legacy.open_out (Legacy.Filename.concat path "warnings.out"));
set_string "outfile" ""
(** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
let preprocess_one_file cppflags fname =
let nname = Filename.concat !Goblintutil.tempDirName (Filename.basename fname) in
if Sys.file_exists (get_string "tempDir") then
nname
else
let command = Config.cpp ^ " --undef __BLOCKS__ " ^ cppflags ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
if get_bool "dbg.verbose" then print_endline command;
let rm_and_exit () = remove_temp_dir (); raise Exit in
try match Unix.system command with
| Unix.WEXITED 0 -> nname
| _ -> eprintf "Goblint: Preprocessing failed."; rm_and_exit ()
with Unix.Unix_error (e, f, a) ->
eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a; rm_and_exit ()
(** Preprocess all files. Return list of preprocessed files and the temp directory name. *)
let preprocess_files () =
let cppflags = ref (get_string "cppflags") in
let custom_include_dirs =
get_string_list "custom_includes" @
Filename.concat exe_dir "includes" ::
Goblint_sites.includes
in
if get_bool "dbg.verbose" then (
print_endline "Custom include dirs:";
List.iteri (fun i custom_include_dir ->
Printf.printf " %d. %s (exists=%B)\n" (i + 1) custom_include_dir (Sys.file_exists custom_include_dir)
) custom_include_dirs
);
let custom_include_dirs = List.filter Sys.file_exists custom_include_dirs in
if custom_include_dirs = [] then
print_endline "Warning, cannot find goblint's custom include files.";
let find_custom_include subpath =
List.find_map (fun custom_include_dir ->
let path = Filename.concat custom_include_dir subpath in
if Sys.file_exists path then
Some path
else
None
) custom_include_dirs
in
let include_dirs = ref [] in
let include_files = ref [] in
let one_include_f f x = include_dirs := f x :: !include_dirs in
if get_string "ana.osek.oil" <> "" then include_files := Filename.concat !Goblintutil.tempDirName OilUtil.header :: !include_files;
get_string_list "includes" |> List.iter (one_include_f identity);
include_dirs := custom_include_dirs @ !include_dirs;
cFileNames := List.rev !cFileNames;
if !cFileNames <> [] then (
let firstFile = List.first !cFileNames in
if Filename.basename firstFile = "Makefile" then (
let makefile = firstFile in
let path = Filename.dirname makefile in
if not (Sys.file_exists makefile) then (
print_endline ("Given " ^ makefile ^ " does not exist!");
let configure = Filename.concat path "configure" in
if Sys.file_exists configure then (
print_endline ("Trying to run " ^ configure ^ " to generate Makefile");
let exit_code, output = MakefileUtil.exec_command ~path "./configure" in
print_endline (configure ^ MakefileUtil.string_of_process_status exit_code ^ ". Output: " ^ output);
if not (Sys.file_exists makefile) then failwith ("Running " ^ configure ^ " did not generate a Makefile - abort!")
) else failwith ("Could neither find given " ^ makefile ^ " nor " ^ configure ^ " - abort!")
);
let _ = MakefileUtil.run_cilly path in
let file = MakefileUtil.(find_file_by_suffix path comb_suffix) in
cFileNames := file :: (List.drop 1 !cFileNames);
);
);
if get_bool "custom_libc" then
cFileNames := find_custom_include "lib.c" :: !cFileNames;
if get_bool "ana.sv-comp.functions" then
cFileNames := find_custom_include "sv-comp.c" :: !cFileNames;
if get_bool "kernel" then (
let kernel_roots = [
get_string "kernel-root";
Filename.concat exe_dir "linux-headers";
]
in
let kernel_root = List.find Sys.file_exists kernel_roots in
let kernel_dir = kernel_root ^ "/include" in
let arch_dir = kernel_root ^ "/arch/x86/include" in
get_string_list "kernel_includes" |> List.iter (Filename.concat kernel_root |> one_include_f);
let preconf = find_custom_include "linux/goblint_preconf.h" in
let autoconf = Filename.concat kernel_dir "linux/kconfig.h" in
cppflags := "-D__KERNEL__ -U__i386__ -D__x86_64__ " ^ !cppflags;
include_files := preconf :: autoconf :: !include_files;
include_dirs := !include_dirs @ [
kernel_dir; kernel_dir ^ "/uapi"; kernel_dir ^ "include/generated/uapi";
arch_dir; arch_dir ^ "/generated"; arch_dir ^ "/uapi"; arch_dir ^ "/generated/uapi";
]
);
let includes =
String.join " " (List.map (fun include_dir -> "-I " ^ include_dir) !include_dirs) ^
" " ^
String.join " " (List.map (fun include_file -> "-include " ^ include_file) !include_files)
in
let cppflags = !cppflags ^ " " ^ includes in
if get_bool "dbg.verbose" then print_endline "Preprocessing files.";
List.rev_map (preprocess_one_file cppflags) !cFileNames
(** Possibly merge all postprocessed files *)
let merge_preprocessed cpp_file_names =
if get_bool "dbg.verbose" then print_endline "Parsing files.";
let files_AST = List.rev_map Cilfacade.getAST cpp_file_names in
remove_temp_dir ();
let cilout =
if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")
in
if not (get_bool "g2html" || get_string "outfile" = "") then Goblintutil.out := Legacy.open_out (get_string "outfile");
Errormsg.logChannel := Messages.get_out "cil" cilout;
let merged_AST =
match files_AST with
| [one] -> Cilfacade.callConstructors one
| [] -> prerr_endline "No arguments for Goblint?";
prerr_endline "Try `goblint --help' for more information.";
raise Exit
| xs -> Cilfacade.getMergedAST xs |> Cilfacade.callConstructors
in
Cilfacade.rmTemps merged_AST;
Cilfacade.createCFG merged_AST;
Cilfacade.current_file := merged_AST;
merged_AST
let do_stats () =
if get_bool "printstats" then (
print_newline ();
ignore (Pretty.printf "vars = %d evals = %d \n" !Goblintutil.vars !Goblintutil.evals);
print_newline ();
Stats.print (Messages.get_out "timing" Legacy.stderr) "Timings:\n";
flush_all ()
)
(** Perform the analysis over the merged AST. *)
let do_analyze change_info merged_AST =
let module L = Printable.Liszt (CilType.Fundec) in
if get_bool "justcil" then
Cilfacade.print merged_AST
else (
if get_bool "dbg.verbose" then print_endline "And now... the Goblin!";
let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in
if stf@exf@otf = [] then failwith "No suitable function to start from.";
if get_bool "dbg.verbose" then ignore (Pretty.printf "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n"
L.pretty stf L.pretty exf L.pretty otf);
let do_all_phases ast funs =
let do_one_phase ast p =
phase := p;
if get_bool "dbg.verbose" then (
let aa = String.concat ", " @@ get_string_list "ana.activated" in
let at = String.concat ", " @@ get_string_list "trans.activated" in
print_endline @@ "Activated analyses for phase " ^ string_of_int p ^ ": " ^ aa;
print_endline @@ "Activated transformations for phase " ^ string_of_int p ^ ": " ^ at
);
try Control.analyze change_info ast funs
with e ->
let backtrace = Printexc.get_raw_backtrace () in
let loc = !Tracing.current_loc in
Messages.error ~loc "About to crash!";
Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal")));
do_stats ();
print_newline ();
Printexc.raise_with_backtrace e backtrace
in
let num_phases =
let np,na,nt = Tuple3.mapn (List.length % get_list) ("phases", "ana.activated", "trans.activated") in
phase_config := np > 0;
if get_bool "dbg.verbose" then print_endline @@ "Using " ^ if !phase_config then "new" else "old" ^ " format for phases!";
if np = 0 && na = 0 && nt = 0 then failwith "No phases and no activated analyses or transformations!";
max np 1
in
ignore @@ Enum.iter (do_one_phase ast) (0 -- (num_phases - 1))
in
Stats.time "analysis" (do_all_phases merged_AST) funs
)
let do_html_output () =
let jar = Filename.concat (get_string "exp.g2html_path") "g2html.jar" in
if get_bool "g2html" then (
if Sys.file_exists jar then (
let command = "java -jar "^ jar ^" --result-dir "^ (get_string "outfile")^" "^ !Messages.xml_file_name in
try match Unix.system command with
| Unix.WEXITED 0 -> ()
| _ -> eprintf "HTML generation failed! Command: %s\n" command
with Unix.Unix_error (e, f, a) ->
eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a
) else
eprintf "Warning: jar file %s not found.\n" jar
)
let do_gobview () =
let create_symlink target link =
if not (Sys.file_exists link) then Unix.symlink target link
in
let gobview = GobConfig.get_bool "gobview" in
let goblint_root =
Filename.concat (Unix.getcwd ()) (Filename.dirname Sys.argv.(0))
in
let dist_dir = Filename.concat goblint_root "_build/default/gobview/dist" in
let js_file = Filename.concat dist_dir "main.js" in
if gobview then (
if Sys.file_exists js_file then (
let save_run = GobConfig.get_string "save_run" in
let run_dir = if save_run <> "" then save_run else "run" in
let dist_files =
Sys.files_of dist_dir
|> Enum.filter (fun n -> n <> "dune")
|> List.of_enum
in
List.iter (fun n ->
create_symlink
(Filename.concat dist_dir n)
(Filename.concat run_dir n)
) dist_files
)
else
eprintf "Warning: Cannot locate Gobview.\n"
)
let eprint_color m = eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr m)
let check_arguments () =
let warn m = eprint_color ("{yellow}Option warning: "^m) in
if get_bool "allfuns" && not (get_bool "exp.earlyglobs") then (set_bool "exp.earlyglobs" true; warn "allfuns enables exp.earlyglobs.\n");
if not @@ List.mem "escape" @@ get_string_list "ana.activated" then warn "Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!";
if get_string "ana.osek.oil" <> "" && not (get_string "exp.privatization" = "protection-vesal" || get_string "exp.privatization" = "protection-old") then (set_string "exp.privatization" "protection-vesal"; warn "oil requires protection-old/protection-vesal privatization");
if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr");
if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int");
if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.rename-load. Previous AST is loaded for diff and rename, but analyis results are not reused.")
let handle_extraspecials () =
let funs = get_string_list "exp.extraspecials" in
LibraryFunctions.add_lib_funs funs
let diff_and_rename current_file =
let change_info: Analyses.increment_data =
if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin
let warn m = eprint_color ("{yellow}Warning: "^m) in
warn "incremental.load is activated but no data exists that can be loaded."
end;
let (changes, old_file, version_map, max_ids) =
if Serialize.results_exist () && GobConfig.get_bool "incremental.load" then begin
let old_file = Serialize.load_data Serialize.CilFile in
let (version_map, changes, max_ids) = VersionLookup.load_and_update_map old_file current_file in
let max_ids = UpdateCil.update_ids old_file max_ids current_file version_map changes in
(changes, Some old_file, version_map, max_ids)
end else begin
let (version_map, max_ids) = VersionLookup.create_map current_file in
(CompareCIL.empty_change_info (), None, version_map, max_ids)
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)
else None
in
if GobConfig.get_bool "incremental.save" then begin
Serialize.store_data current_file Serialize.CilFile;
Serialize.store_data (version_map, max_ids) Serialize.VersionData
end;
let old_data = match old_file, solver_data with
| Some cil_file, Some solver_data -> Some ({cil_file; solver_data}: Analyses.analyzed_data)
| _, _ -> None
in
{Analyses.changes = changes; old_data; new_file = current_file}
in change_info
let () =
let open Sys in
catch_break true;
set_signal (Goblintutil.signal_of_string (get_string "dbg.backtrace-signal")) (Signal_handle (fun _ -> Printexc.get_callstack 999 |> Printexc.print_raw_backtrace Stdlib.stderr; print_endline "\n...\n"))
(** the main function *)
let main () =
try
Stats.reset Stats.SoftwareTimer;
parse_arguments ();
check_arguments ();
AfterConfig.run ();
Sys.set_signal (Goblintutil.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore;
(if GobConfig.get_bool "ana.sv-comp.enabled" && Svcomp.Specification.of_option () = NoOverflow then
set_bool "exp.lower-constants" false);
Cilfacade.init ();
handle_extraspecials ();
create_temp_dir ();
handle_flags ();
if get_bool "dbg.verbose" then (
print_endline (localtime ());
print_endline command;
);
let file = preprocess_files () |> merge_preprocessed in
let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
file|> do_analyze changeInfo;
do_stats ();
do_html_output ();
do_gobview ();
if !verified = Some false then exit 3;
with
| Exit ->
exit 1
| Sys.Break ->
eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
exit 131
| Timeout ->
eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!"));
exit 124