Source file text.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
(** Display the results of the analysis in a textual form. *)
open Mopsa_utils
open ArgExt
open Core.All
open Location
open Format
open Callstack
open Common
(** Command-line option to enable display of alarms call stacks *)
let opt_show_callstacks = ref false
(** Command-line option to specify the number of spaces to use for
printing tabs
*)
let opt_tw = ref 4
let print out fmt =
let formatter =
match out with
| None -> std_formatter
| Some file ->
let o = open_out file in
formatter_of_out_channel o
in
kasprintf (fun str ->
fprintf formatter "%s%!" str
) fmt
let compile_tab_columns tw s pos =
let rec doit i s =
try (match String.sub s 0 1, String.sub s 1 (String.length s - 1) with
| "\t", s -> (fun n -> (if n > i then (doit (i+1) s n) + tw - 1 else doit (i+1) s n))
| _, s -> doit (i+1) s
) with
| Invalid_argument _ -> fun i -> i
in
get_pos_column pos |> doit 0 s
let replace_tabs tw s =
let re = Str.regexp "\t" in
Str.global_replace re (String.make tw ' ') s
module AlarmKindSet = SetExt.Make(struct type t = alarm_kind let compare = compare_alarm_kind end)
let color_of_diag = function
| Safe -> Debug.green
| Unreachable -> Debug.gray
| Error -> Debug.red
| Warning -> Debug.orange
let icon_of_diag = function
| Safe -> "✔"
| Warning -> "⚠"
| Error -> "✗"
| Unreachable -> "🛇"
(** Highlight source code at a given location range *)
let highlight_range color fmt range =
if not @@ is_orig_range @@ untag_range range then ()
else
let start_pos = get_range_start range in
let end_pos = get_range_end range in
let file = get_pos_file start_pos in
assert (file = get_pos_file end_pos);
if not @@ Sys.file_exists file then () else
let is_bug_line i = i >= get_pos_line start_pos && i <= get_pos_line end_pos in
let f = open_in file in
let get_bug_lines i =
let rec iter i acc =
let ol = try Some (input_line f) with End_of_file -> None in
if is_bug_line i then
iter (i+1)
(match ol with
| None -> acc
| Some l -> (i, l)::acc)
else
match ol with
| None -> acc
| _ -> iter (i+1) acc in
List.rev @@ iter i []
in
let highlight_bug fmt (i,l) =
let get_tabbed_column = compile_tab_columns !opt_tw l in
let l = replace_tabs !opt_tw l in
let safe_sub l s e =
try String.sub l s e
with Invalid_argument _ ->
let () = Debug.warn_at range "issue on sub %s %d %d" l s e in
String.sub l (min 0 s) (max 0 (min e ((String.length l) - s))) in
let n = String.length l in
let c1 = get_tabbed_column start_pos in
let c2 = get_tabbed_column end_pos in
let s1,s2,s3 =
if i = get_pos_line start_pos && i = get_pos_line end_pos then
safe_sub l 0 c1,
safe_sub l c1 (c2-c1),
safe_sub l c2 (n-c2)
else if i = get_pos_line start_pos && i = get_pos_line end_pos then
safe_sub l 0 c1,
safe_sub l c1 (n-c1),
""
else if i = get_pos_line end_pos then
"",
safe_sub l 0 c2,
safe_sub l c2 (n-c2)
else
"",
l,
""
in
fprintf fmt "%a: %s%a%s" (Debug.bold pp_print_int) i s1 (Debug.color_str color) s2 s3
in
let underline_bug color fmt (i,l) =
let get_tabbed_column = compile_tab_columns !opt_tw l in
let l = replace_tabs !opt_tw l in
let n = string_of_int i |> String.length in
let c1 = get_tabbed_column start_pos + n + 2 in
let c2 = get_tabbed_column end_pos + n + 2 in
let c3 = String.length l + n + 2 in
let s1 = String.make c1 ' ' in
let s2 = String.make (c2 - c1) '^' in
let s3 = String.make (c3 - c2) ' ' in
fprintf fmt "@,%s%a%s" s1 (Debug.color_str color) s2 s3
in
let lines = get_bug_lines 1 in
close_in f;
pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,") highlight_bug fmt lines;
match lines with
| [bug] -> underline_bug color fmt bug
| _ -> ()
let pp_diagnostic out n diag callstacks kinds =
let file_name = get_range_relative_file diag.diag_range in
let fun_name = match CallstackSet.choose callstacks with
| c::_ -> Some c.call_fun_orig_name
| _ -> None in
let len = CallstackSet.cardinal callstacks in
print out "@.%a Check%s:%a@,@[<v 2>%a: %a: %a%a%a%a@]@.@."
(Debug.color_str (color_of_diag diag.diag_kind)) (icon_of_diag diag.diag_kind)
(if len <= 1 then Format.asprintf " #%d" (n+1) else Format.asprintf "s #%d-#%d" (n+1) (n+len))
(fun fmt -> function
| None -> ()
| Some f ->
fprintf fmt "@,%a: In function '%a':"
(Debug.bold pp_print_string) file_name
(Debug.bold pp_print_string) f
) fun_name
(Debug.bold pp_relative_range) diag.diag_range
(Debug.color (color_of_diag diag.diag_kind) pp_diagnostic_kind) diag.diag_kind
(Debug.color (color_of_diag diag.diag_kind) pp_check) diag.diag_check
(fun fmt range ->
let start_pos = get_range_start range in
let file = get_pos_file start_pos in
if not @@ Sys.file_exists file then () else
fprintf fmt "@,@,%a" (highlight_range (color_of_diag diag.diag_kind)) range
) diag.diag_range
(fun fmt -> function
| [] -> ()
| l ->
fprintf fmt "@,%a"
(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,") pp_alarm_kind) l
) kinds
(fun fmt callstacks ->
match CallstackSet.elements callstacks with
| [] -> ()
| [cs] when is_empty_callstack cs -> ()
| [cs] -> fprintf fmt "@,Callstack:@,@[%a@]" pp_callstack cs
| cs::tl ->
if not !opt_show_callstacks then
let others = List.length tl in
fprintf fmt "@,Callstack:@,@[%a@]@,+%d other callstack%a" pp_callstack cs others Debug.plurial_int others
else
let pp_numbered_callstack i fmt cs =
fprintf fmt "@,@[<v>Callstack%a:@,%a@]"
(fun fmt -> function
| None -> ()
| Some i -> fprintf fmt " %d" (i+1)
) i
pp_callstack cs
in
let csl' = List.mapi (fun i cs -> (i,cs)) (cs::tl) in
pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
(fun fmt (i,cs) -> pp_numbered_callstack (Some i) fmt cs)
fmt csl';
) callstacks
let incr_check_diag len check diag checks_map =
let (safe,error,warning) =
match CheckMap.find_opt check checks_map with
| Some x -> x
| None -> (0,0,0)
in
let total =
match diag with
| Safe -> safe+len,error,warning
| Unreachable -> safe,error,warning
| Error -> safe,error+len,warning
| Warning -> safe,error,warning+len
in
CheckMap.add check total checks_map
let construct_checks_summary ?(print=false) rep out =
let diag_groups = Alarm.group_diagnostics rep.report_diagnostics in
RangeDiagnosticWoCsMap.fold (fun (range, diagWoCs) css acc ->
let (i,safe,error,warning,checks_map) = acc in
let len = CallstackSet.cardinal css in
let checks_map' = incr_check_diag len diagWoCs.diag_check diagWoCs.diag_kind checks_map in
match diagWoCs.diag_kind with
| Unreachable ->
i, safe, error, warning, checks_map'
| Safe ->
if print && !opt_show_safe_checks then pp_diagnostic out i diagWoCs css [];
i+len, safe+len, error, warning, checks_map'
| Error | Warning ->
let kinds =
AlarmSet.fold
(fun a kinds ->
AlarmKindSet.add a.alarm_kind kinds
) diagWoCs.diag_alarms AlarmKindSet.empty in
let rec iter = function
| [] -> []
| hd::tl ->
let hd',tl' = iter_with hd tl in
hd'::iter tl'
and iter_with a = function
| [] -> a,[]
| hd::tl ->
match join_alarm_kind a hd with
| None ->
let a',tl' = iter_with a tl in
a',hd::tl'
| Some aa ->
let aa',tl' = iter_with aa tl in
aa',tl'
in
let kinds' = iter (AlarmKindSet.elements kinds) in
if print then pp_diagnostic out i diagWoCs css kinds';
let error',warning' =
if diagWoCs.diag_kind = Error then
error+len, warning
else
error, warning+len in
i+len, safe, error', warning', checks_map'
) diag_groups (0,0,0,0,CheckMap.empty)
let print_checks_summary checks_map total safe error warning out =
let pp diag singluar plural fmt n =
if n = 0 then () else
if n = 1 then fprintf fmt ", %a" (Debug.color (color_of_diag diag) (fun fmt n -> fprintf fmt "%s %d %s" (icon_of_diag diag) n singluar)) n
else fprintf fmt ", %a" (Debug.color (color_of_diag diag) (fun fmt n -> fprintf fmt "%s %d %s" (icon_of_diag diag) n plural)) n
in
print out "@[<v2>Checks summary: %a%a%a%a (selectivity: %.2f%%)@,%a@]@.@."
(Debug.bold (fun fmt total -> fprintf fmt "%d total" total)) total
(pp Safe "safe" "safe") safe
(pp Error "error" "errors") error
(pp Warning "warning" "warnings") warning
(float_of_int (100 * safe) /. (float_of_int @@ safe + error + warning))
(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
(fun fmt (check,(safe,error,warning)) ->
fprintf fmt "%a: %d total%a%a%a"
pp_check check
(safe+error+warning)
(pp Safe "safe" "safe") safe
(pp Error "error" "errors") error
(pp Warning "warning" "warnings") warning
)
) (CheckMap.bindings checks_map)
let report man flow ~time ~files ~out =
let rep = Flow.get_report flow in
if is_sound_report rep
then print out "%a@." (Debug.color_str Debug.green) "Analysis terminated successfully"
else print out "%a@." (Debug.color_str Debug.orange) "Analysis terminated successfully (with assumptions)";
if !opt_display_lastflow then
print out "Last flow =@[@\n%a@]@\n"
(format (Core.Flow.print man.lattice.print)) flow
;
if is_safe_report rep
then print out "%a No alarm@." ((Debug.color Debug.green) pp_print_string) "✔";
print out "Analysis time: %.3fs@." time;
let total, safe, error, warning, checks_map = construct_checks_summary ~print:true rep out in
print_checks_summary checks_map total safe error warning out
;
if not (is_sound_report rep) then
let nb = AssumptionSet.cardinal rep.report_assumptions in
print out "%d assumption%a:@, @[<v>%a@]@.@."
nb Debug.plurial_int nb
(pp_print_list
~pp_sep:(fun fmt () -> fprintf fmt "@,")
pp_assumption
) (AssumptionSet.elements rep.report_assumptions)
let panic exn ~btrace ~time ~files ~out continuation =
print out "%a@." (Debug.color_str Debug.red) "Analysis aborted";
let () =
match exn with
| Exceptions.Panic (msg, "") -> print out "panic: %s@." msg
| Exceptions.Panic (msg, loc) -> print out "panic raised in %s: %s@." loc msg
| Exceptions.PanicAtLocation (range, msg, "") -> print out "panic in %a: %s@." Location.pp_range range msg
| Exceptions.PanicAtLocation (range, msg, loc) -> print out "%a: panic raised in %s: %s@." Location.pp_range range loc msg
| Exceptions.PanicAtFrame (range, cs, msg, "") ->
print out "panic in %a: %s@\nTrace:@\n%a@." Location.pp_range range msg pp_callstack cs;
| Exceptions.PanicAtFrame (range, cs, msg, loc) -> print out "%a: panic raised in %s: %s@\nTrace:@\n%a@." Location.pp_range range loc msg pp_callstack cs
| Exceptions.SyntaxError (range, msg) -> print out "%a: syntax error: %s@." Location.pp_range range msg
| Exceptions.UnnamedSyntaxError range -> print out "%a: syntax error@." Location.pp_range range
| Exceptions.SyntaxErrorList l ->
print out "Syntax errors:@\n @[%a@]@."
(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@\n")
(fun fmt (range, msg) -> fprintf fmt "%a: %s" Location.pp_range range msg
)
) l
| Exceptions.UnnamedSyntaxErrorList l ->
print out "Syntax errors:@\n @[%a@]@."
(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@\n") Location.pp_range)
l
| _ -> print out "Uncaught exception: %s@." (Printexc.to_string exn)
in
let () =
if btrace = "" then ()
else print out "Backtrace:@\n%s" btrace
in
continuation ()
let group_args_by_category args =
let sorted = List.sort (fun arg1 arg2 ->
compare arg1.category arg2.category
) args
in
let grouped, _ = List.fold_right (fun arg (acc,cat) ->
if compare cat arg.category <> 0
then
(arg.category,[arg]) :: acc, arg.category
else
let (_, l) = List.hd acc in
(cat, arg :: l) :: (List.tl acc), cat
) sorted ([],"")
in
grouped
let help (args:ArgExt.arg list) ~out =
let print_default fmt d =
if d = "" then ()
else fprintf fmt " (default: %s)" d
in
let groups = group_args_by_category args in
print out "Options:@.";
List.iter (fun (cat, args) ->
print out " %s@." (String.uppercase_ascii cat);
List.iter (fun arg ->
match arg.spec with
| Symbol(l,_) ->
print out " %s={%a} %s%a@."
arg.key
(pp_print_list
~pp_sep:(fun fmt () -> pp_print_string fmt ",")
pp_print_string
) l
arg.doc
print_default arg.default
| _ ->
print out " %s %s%a@." arg.key arg.doc print_default arg.default
) (List.sort Stdlib.compare args)
) groups
let list_domains (domains:string list) ~out =
print out "Domains:@.";
List.iter (fun d -> print out " %s@." d) domains
let list_reductions (reductions:string list) ~out =
print out "Reductions:@.";
List.iter (fun d -> print out " %s@." d) reductions
let list_checks checks ~out =
print out "Checks:@.";
List.iter (fun chk -> print out " %a@." Core.Alarm.pp_check chk) checks
let list_hooks hooks ~out =
print out "Hooks:@.";
List.iter (fun h -> print out " %s@." h) hooks
let print printer ~range ~out =
if Debug.can_print "print" then
print out "%a@\n @[%a@]@."
Location.pp_relative_range range
pflush printer
else
()