Source file terminal.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
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
open Core.All
open Mopsa_utils
open Location
open Callstack
open Interface
open Format
open Breakpoint
open Toplevel
open Action
open Envdb
open Trace
module Make(Toplevel : TOPLEVEL) =
struct
let opt_show_var_scope = ref true
(** Commands *)
type terminal_command_kind =
| Break of string
(** Add a breakpoint *)
| Continue
(** Stop at next breakpoint *)
| MopsaBackTrace
(** Returns the current backtrace of Mopsa *)
| Next
(** Stop at next statement and skip function calls *)
| Step
(** Step into function calls *)
| Finish
(** Finish current function *)
| NextI
(** Stop at next statement and skip nodes in the interpretation sub-tree *)
| StepI
(** Step into interpretation sub-tree *)
| Print of (string * string option) list * (string * int) option
(** Print the abstract state or the value of variables *)
| Env of string list
(** Print the current abstract environment, associated to token T_cur,
eventually projected on a list of domains *)
| State
(** Print the current abstract state *)
| Where
(** Show current program point *)
| Info of info_command
(** Print extra information *)
| Enable of enable_command
(** Enable an option *)
| Disable of enable_command
(** Disable an option *)
| Set of set_command * string
(** Set an option *)
| Unset of set_command
(** Unset an option *)
| BackTrace
(** Print the callstack *)
| LoadScript of string
| Trace
| Backward
(** Information sub-commands *)
and info_command =
| Alarms
| Breakpoints
| Tokens
| Variables
| Context
(** Enable/Disable sub-commands *)
and enable_command =
| Hook of string
(** Set/Unset sub-commands *)
and set_command =
| Debug
| Script
| ShowVarScope
type terminal_command_redirection =
| Pipe of string
| File of string
(** Commands *)
type terminal_command = {
(** Kind of the command *)
kind: terminal_command_kind;
(** Optional flag *)
redirection: terminal_command_redirection option;
}
(** Print a command *)
let pp_terminal_command_kind fmt = function
| Break loc -> Format.fprintf fmt "break %s" loc
| MopsaBackTrace -> Format.fprintf fmt "mopsa_bt"
| Continue -> Format.pp_print_string fmt "continue"
| Next -> Format.pp_print_string fmt "next"
| Finish -> Format.pp_print_string fmt "finish"
| NextI -> Format.pp_print_string fmt "nexti"
| Step -> Format.pp_print_string fmt "step"
| StepI -> Format.pp_print_string fmt "stepi"
| Print([], None) -> Format.pp_print_string fmt "print"
| Print(vars, None) ->
Format.fprintf fmt "print %a"
(pp_print_list
~pp_sep:(fun fmt () -> pp_print_string fmt ",")
(fun fmt (v, o_f) ->
match o_f with
| None -> fprintf fmt "%s" v
| Some f -> fprintf fmt "%s:%s" v f)
) vars
| Print(vars, Some(file, line)) ->
Format.fprintf fmt "print@%s:%d %a"
file line
(pp_print_list
~pp_sep:(fun fmt () -> pp_print_string fmt ",")
(fun fmt (v, o_f) ->
match o_f with
| None -> fprintf fmt "%s" v
| Some f -> fprintf fmt "%s:%s" v f)
) vars
| Env [] -> Format.pp_print_string fmt "env"
| Env domains -> Format.fprintf fmt "env %a"
(pp_print_list
~pp_sep:(fun fmt () -> pp_print_string fmt ",")
pp_print_string
) domains
| State -> Format.pp_print_string fmt "state"
| Where -> Format.pp_print_string fmt "where"
| Info Alarms -> Format.pp_print_string fmt "info alarms"
| Info Breakpoints -> Format.pp_print_string fmt "info breakpoints"
| Info Tokens -> Format.pp_print_string fmt "info tokens"
| Info Variables -> Format.pp_print_string fmt "info variables"
| Info Context -> Format.pp_print_string fmt "info context"
| Enable (Hook h) -> Format.fprintf fmt "enable hook %s" h
| Disable (Hook h) -> Format.fprintf fmt "disable hook %s" h
| Set (Debug, d) -> Format.fprintf fmt "set debug %s" d
| Set (Script, d) -> Format.fprintf fmt "set script %s" d
| Set (ShowVarScope, d) -> Format.fprintf fmt "set showvarscope %s" d
| LoadScript s -> Format.fprintf fmt "load script %s" s
| Unset Debug -> Format.pp_print_string fmt "unset debug"
| Unset Script -> Format.pp_print_string fmt "unset script"
| Unset ShowVarScope -> Format.pp_print_string fmt "unset showvarscope"
| BackTrace -> Format.pp_print_string fmt "backtrace"
| Trace -> Format.pp_print_string fmt "trace"
| Backward -> Format.pp_print_string fmt "backward"
let pp_terminal_command_redirection fmt = function
| Pipe shell -> Format.fprintf fmt " | %s" shell
| File file -> Format.fprintf fmt " > %s" file
let pp_terminal_command fmt c =
Format.fprintf fmt "%a%a"
pp_terminal_command_kind c.kind
(Format.pp_print_option pp_terminal_command_redirection) c.redirection
(** Print help message *)
let print_usage () =
printf "Available commands:@.";
printf " b[reak] <[file:]line> add a breakpoint at a line@.";
printf " b[reak] <function> add a breakpoint at a function@.";
printf " b[reak] @name add a named breakpoint (will break when the analysis executes an S_break name)@.";
printf " b[reak] #a[larm] break at the next alarm (and go back at the statement generating the alarm)@.";
printf " c[ontinue] run until next breakpoint@.";
printf " n[ext] stop at next statement and skip function calls.@.";
printf " n[ext]i stop at next statement and skip nodes in the interpretation sub-tree@.";
printf " s[tep] step into function calls@.";
printf " s[tep]i step into interpretation sub-tree@.";
printf " f[inish] finish current function@.";
printf " b[ack]w[ard] go backward to the calling site@.";
printf " e[nable] h[hook] <h> enable a hook@.";
printf " d[isable] h[hook] <h> disable a hook@.";
printf " s[et] d[ebug] <d> set debug channels@.";
printf " u[nset] d[ebug] unset debug channels@.";
printf " s[et] script <file> store commands into a file@.";
printf " To be used in combination with load script <file>@.";
printf " u[nset] script do not store commands in file anymore@.";
printf " load script <file> reads script command from <file>@.";
printf " help print this message@.";
printf "The commands below support shell commands (`env | grep foo`, `mopsa_bt | tac`, ...):@.";
printf " p[rint] print the abstract state@.";
printf " p[rint] <vars> print the value of selected variables@.";
printf " For example, `p x,y:f,z:*` prints x in the current scope, y in the scope of f, and z in all scopes@.";
printf " p[rint] <vars> #<f>:<l> print the value of selected variables at the given program location@.";
printf " e[nv] print the current abstract environment@.";
printf " e[nv] <domain>,... print the current abstract environment of selected domains@.";
printf " state print the full abstract state (map from flow token to environment)@.";
printf " b[ack]t[race] print the current call stack@.";
printf " t[race] print the analysis trace@.";
printf " w[here] show current program point@.";
printf " i[info] a[larms] print the list of detected alarms@.";
printf " i[info] c[hecks] print the list of performed checks@.";
printf " i[info] b[reakpoints] print the list of registered breakpoints@.";
printf " i[info] t[okens] print the list of flow tokens@.";
printf " i[info] v[ariables] print the list of variables@.";
printf " i[info] c[on]t[e]x[t] print the flow-insensitive context@.";
printf " mopsa_bt shows the current backtrace of the analyzer@.";
printf "You can chain multiple commands with ';'@.";
()
(** Print input prompt *)
let print_prompt () =
printf "%a %a @?"
Debug.(color_str teal) "mopsa"
Debug.(color_str green) ">>"
(** Context of LineEdit library *)
let linedit_ctx = LineEdit.create_ctx ()
(** Reference to the last commands read from the prompt *)
let last_prompt_commands = ref []
(** Buffer of upcoming commands to execute *)
let commands_buffer = Queue.create ()
let script : out_channel option ref = ref None
let rec read_terminal_command_string () =
if not (Queue.is_empty commands_buffer) then
Queue.pop commands_buffer
else
let () = print_prompt () in
try
let input = LineEdit.read_line linedit_ctx |>
String.trim in
if String.length input > 0 && input.[0] = '#' then read_terminal_command_string ()
else
let parts = String.split_on_char ';' input |>
List.map String.trim |>
List.filter (function "" -> false | _ -> true) in
match parts, !last_prompt_commands with
| [], [] ->
read_terminal_command_string ()
| [], _ ->
let () = List.iter (fun c -> Queue.add c commands_buffer) !last_prompt_commands in
read_terminal_command_string ()
| _ ->
last_prompt_commands := parts;
List.iter (fun c -> Queue.add c commands_buffer) parts;
read_terminal_command_string ()
with End_of_file -> raise Exit
exception ReadNewCommand
let parse_command_kind s flow =
let parts = String.split_on_char ' ' s |>
List.map String.trim |>
List.filter (function "" -> false | _ -> true)
in
match parts with
| ["exit"] -> raise Exit
| ["continue" | "c"] -> Continue
| ["mopsa_bt"] -> MopsaBackTrace
| ["next" | "n"] -> Next
| ["step" | "s"] -> Step
| ["finish" | "f"] -> Finish
| ["nexti" |"ni"] -> NextI
| ["stepi" |"si"] -> StepI
| ["where" | "w"] -> Where
| ["backtrace"|"bt"] -> BackTrace
| ["break" | "b"; l]-> Break l
| ["backward" | "back" | "bw"] -> Backward
| ("env" | "e") :: domains ->
let domains =
List.fold_left
(fun acc s ->
let parts = String.split_on_char ',' s |>
List.filter (function "" -> false | _ -> true)
in
SetExt.StringSet.union acc (SetExt.StringSet.of_list parts)
) SetExt.StringSet.empty domains
in
Env (SetExt.StringSet.elements domains)
| ["state" ] -> State
| ["help" | "h"] ->
print_usage ();
raise ReadNewCommand
| ["info" |"i"; "tokens" | "t"] | ["it"] -> Info Tokens
| ["info" |"i"; "breakpoints" | "b"] | ["ib"] -> Info Breakpoints
| ["info" |"i"; "alarms" | "a"] | ["ia"] -> Info Alarms
| ["info" |"i"; "variables" | "vars" | "var" | "v"] | ["iv"] -> Info Variables
| ["info" |"i"; "context" | "ctx"] | ["ictx"] -> Info Context
| ["enable" | "en"; "hook" | "h"; h] | ["eh"; h] -> Enable (Hook h)
| ["disable"|"d"; "hook" | "h"; h] | ["dh"; h] -> Disable (Hook h)
| ["set" |"s"; "debug"| "d"; d] | ["sd"; d] -> Set (Debug, d)
| ["unset"|"u"; "debug"| "d"] | ["ud"] -> Unset Debug
| ["set" |"s"; "script"| "s"; d] | ["sc"; d] -> Set (Script, d)
| ["unset"|"u"; "script"| "s"] | ["uc"] -> Unset Script
| ["set"; "showvarscope" ] -> Set (ShowVarScope, "")
| ["unset"; "showvarscope"] -> Unset ShowVarScope
| ["load"; "script"; s] | ["ls"; s] -> LoadScript s
| ("print" | "p") :: vars ->
let cs = Flow.get_callstack flow in
let vars =
List.fold_left
(fun acc s ->
let parts = String.split_on_char ',' s |>
List.filter (function "" -> false | _ -> true) in
let parts = List.map (fun s ->
let l = String.split_on_char ':' s in
if List.length l = 1 then
if cs = [] then List.hd l, None
else List.hd l, Some (List.hd cs).call_fun_orig_name
else
let f = List.hd @@ List.tl l in
if String.compare f "*" = 0 then List.hd l, None
else (List.hd l, Some f)
) parts
in
parts @ acc
) [] vars
in
Print (vars, None)
| print::vars when Str.string_match (Str.regexp {|\(p\|print\)@\(.+\):\([0-9]+\)|}) print 0 ->
let file = Str.matched_group 2 print in
let line = Str.matched_group 3 print |> int_of_string in
let vars =
List.fold_left
(fun acc s ->
let parts = String.split_on_char ',' s |>
List.filter (function "" -> false | _ -> true)
in
let parts = List.map (fun s ->
let l = String.split_on_char ':' s in
if List.length l = 1 then List.hd l, None
else (List.hd l, Some (List.hd @@ List.tl l))) parts
in
parts @ acc)
[] vars
in
Print(vars, Some(file, line))
| ["trace"|"t"] -> Trace
| _ ->
printf "Unknown command %s@." s;
print_usage ();
raise ReadNewCommand
let parse_command_redirection s =
if Str.(string_match (regexp {|\([^|]+\)|\(.*\)|}) s 0) then
let cmd = Str.matched_group 1 s |> String.trim in
let redirect = Pipe (Str.matched_group 2 s |> String.trim) in
cmd, Some redirect
else
if Str.(string_match (regexp {|\([^>]+\)>\([^>]+\)|}) s 0) then
let cmd = Str.matched_group 1 s |> String.trim in
let redirect = File (Str.matched_group 2 s |> String.trim) in
cmd, Some redirect
else
s, None
(** Read the next command *)
let rec read_terminal_command logger flow =
let s = read_terminal_command_string () in
logger s;
let s, redirection = parse_command_redirection s in
try
let kind = parse_command_kind s flow in
{ kind; redirection }
with ReadNewCommand ->
read_terminal_command logger flow
(** {2 Pretty printers} *)
(** ******************* *)
module Addr =
struct
type t = addr
let compare = compare_addr
let print = unformat pp_addr
let from_expr e =
match ekind e with
| E_addr (addr, _) -> addr
| _ -> assert false
end
module AddrSet =
struct
include SetExt.Make(Addr)
let print printer s =
pp_list Addr.print printer (elements s) ~lopen:"{" ~lsep:"," ~lclose:"}"
end
let dummy_range = mk_fresh_range ()
(** Print value of variables *)
let pp_vars fmt action names man flow =
if man.lattice.is_bottom (Flow.get T_cur man.lattice flow) then
fprintf fmt "⊥@."
else
Ast.Var.force_print_uniq_with_uid false (fun () ->
let names =
match names with
| [] ->
List.map (fun v -> asprintf "%a" pp_var v, None) (action_line_vars action)
| _ -> names in
let names_global, names_by_func =
List.fold_left (fun (global_acc, func_acc) (name, o_f) ->
match o_f with
| None -> (name :: global_acc, func_acc)
| Some f -> (global_acc,
if MapExt.StringMap.mem f func_acc then
MapExt.StringMap.add f (name :: MapExt.StringMap.find f func_acc) func_acc
else
MapExt.StringMap.add f [name] func_acc)
) ([], MapExt.StringMap.empty) names in
let vars = ask_and_reduce man.ask
(Q_defined_variables None) flow in
let vmap =
List.fold_left
(fun acc v ->
let vname = asprintf "%a" pp_var v in
let old = OptionExt.default VarSet.empty
(MapExt.StringMap.find_opt vname acc) in
MapExt.StringMap.add vname (VarSet.add v old) acc)
MapExt.StringMap.empty vars
in
let addrs = ask_and_reduce man.ask Q_allocated_addresses flow in
let amap =
List.fold_left
(fun acc a ->
let aname = asprintf "%a" pp_addr a in
let old = OptionExt.default AddrSet.empty
(MapExt.StringMap.find_opt aname acc) in
MapExt.StringMap.add aname (AddrSet.add a old) acc)
MapExt.StringMap.empty addrs
in
let vfound, afound, not_found = List.fold_left
(fun (vfound,afound,not_found) name ->
match MapExt.StringMap.find_opt name vmap with
| Some vars -> (VarSet.elements vars)@vfound,afound,not_found
| None ->
match MapExt.StringMap.find_opt name amap with
| Some addrs -> vfound,(AddrSet.elements addrs)@afound,not_found
| None -> vfound,afound,name::not_found
) ([],[],[]) names_global in
let vfound, afound, not_found = MapExt.StringMap.fold
(fun func vs (vfound, afound, not_found) ->
let vars = ask_and_reduce man.ask (Q_defined_variables (Some func)) flow in
let vmap = List.fold_left
(fun acc v ->
let vname = asprintf "%a" pp_var v in
let old = OptionExt.default VarSet.empty
(MapExt.StringMap.find_opt vname acc) in
MapExt.StringMap.add vname (VarSet.add v old) acc)
MapExt.StringMap.empty vars in
List.fold_left (fun (vfound, afound, not_found) name ->
match MapExt.StringMap.find_opt name vmap with
| Some vars -> (VarSet.elements vars)@vfound,afound,not_found
| None ->
match MapExt.StringMap.find_opt name amap with
| Some addrs -> vfound,(AddrSet.elements addrs)@afound,not_found
| None -> vfound,afound,name::not_found
) (vfound, afound, not_found) vs
)
names_by_func (vfound, afound, not_found) in
let protect_print print_thunk =
if not @@ !opt_show_var_scope then
Core.Ast.Var.force_print_uniq_with_uid false (fun () -> print_thunk ())
else
print_thunk ()
in
let not_found' =
let printer = empty_printer () in
let found,not_found =
List.fold_left
(fun (found,not_found) v ->
try
let () =
if VarSet.cardinal @@ OptionExt.default VarSet.empty (MapExt.StringMap.find_opt (asprintf "%a" pp_var v) vmap) > 1 then
protect_print (fun () -> man.print_expr flow printer (mk_var v dummy_range))
else
man.print_expr flow printer (mk_var v dummy_range) in
true,not_found
with Not_found ->
let vname = asprintf "%a" pp_var v in
found,vname::not_found
) (false,[]) vfound
in
let found,not_found =
List.fold_left
(fun (found,not_found) a ->
try
let () = man.print_expr flow printer (mk_addr a dummy_range) in
true,not_found
with Not_found ->
let aname = asprintf "%a" pp_addr a in
found,aname::not_found
) (found,not_found) afound
in
if found then fprintf fmt "%a@." pflush printer;
not_found
in
( match not_found@not_found' with
| [] -> ()
| l ->
fprintf fmt "Variable%a %a not found@."
Debug.plurial_list not_found
(pp_print_list
~pp_sep:(fun fmt () -> pp_print_string fmt ", ")
(fun fmt vname -> fprintf fmt "'%s'" vname)
) l
))
let init () =
printf "@.%a@.Type '%a' to get the list of commands.@.@."
(Debug.bold pp_print_string) ("Welcome to Mopsa " ^ Version.version ^ "!")
(Debug.bold pp_print_string) "help"
let reach action man flow =
printf "%a@." Debug.(color fushia pp_relative_range) (action_range action);
pp_action_source_code std_formatter action;
printf "%a@." (pp_action ~truncate:true ~indent:0) action
let pp_alarms fmt alarms =
fprintf fmt "%d new alarm%a detected: @[<v>@."
(List.length alarms)
Debug.plurial_list alarms;
ignore(Output.Text.construct_checks_summary ~print:true (Alarm.alarms_to_report alarms) None);
fprintf fmt "@]@."
let alarm alarms action man flow =
pp_alarms Format.std_formatter alarms
let logger cmd_str =
if List.mem cmd_str ["us"; "unset script"; "unset s"] then
()
else
match !script with
| None -> ()
| Some ch ->
let file_fmt = formatter_of_out_channel ch in
Format.fprintf file_fmt "%s@." cmd_str
let pp_output_command action envdb man flow fmt = function
| BackTrace ->
let cs = Flow.get_callstack flow in
fprintf fmt "%a@." pp_callstack cs
| MopsaBackTrace ->
let (in_file_descr, out_file_descr) = Unix.pipe () in
let in_channel = Unix.in_channel_of_descr in_file_descr in
let out_channel = Unix.out_channel_of_descr out_file_descr in
Printexc.print_raw_backtrace out_channel (Printexc.get_callstack Int.max_int);
let buffer = Buffer.create 100 in
close_out out_channel;
let rec loop () =
match input_line in_channel with
| l -> Buffer.add_string buffer (l ^ "\n"); loop ()
| exception End_of_file -> Buffer.contents buffer
in
let r = loop () in
close_in in_channel;
fprintf fmt "%s@." r
| Print(names, loc) ->
let ctx = Flow.get_ctx flow in
let env =
match loc with
| None -> Some(action, flow)
| Some(file, line) ->
match find_envdb_opt file line envdb with
| None -> None
| Some(action', envs) ->
fprintf fmt "%a@." (pp_action ~truncate:false ~indent:0) action';
let env =
CallstackMap.fold
(fun _ -> man.lattice.join ctx)
envs man.lattice.bottom
in
Some(action', Flow.singleton ctx T_cur env)
in
( match env with
| None -> ()
| Some(action', flow') -> pp_vars fmt action' names man flow'
)
| Env [] ->
let env = Flow.get T_cur man.lattice flow in
fprintf fmt "%a@." (Print.format man.lattice.print) env
| Env domains ->
let env = Flow.get T_cur man.lattice flow in
let re =
List.map
(fun d ->
let d' = Str.global_replace (Str.regexp_string "_") ".*" d in
".*" ^ d' ^ ".*"
) domains |>
String.concat "\\|" |>
Str.regexp
in
let pobj = pbox man.lattice.print env in
let pobj' = match_print_object_keys re pobj in
fprintf fmt "%a@." pp_print_object pobj'
| State ->
fprintf fmt "%a@." (Print.format (Flow.print man.lattice.print)) flow
| Where ->
pp_action_source_code std_formatter action;
fprintf fmt "%a@." Debug.(color fushia pp_relative_range) (action_range action);
fprintf fmt "%a@." (pp_action ~truncate:false ~indent:0) action
| Info Tokens ->
let tokens = Flow.fold (fun acc tk _ -> tk::acc) [] flow in
fprintf fmt "%a@." (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n") pp_token) tokens
| Info Alarms ->
let report = Flow.get_report flow in
( if is_safe_report report
then printf "%a No alarm@." Debug.(color_str green) "✔";
let _ = Output.Text.construct_checks_summary ~print:true report None in
()
)
| Info Breakpoints ->
fprintf fmt "%a@." Breakpoint.pp_breakpoint_set !breakpoints
| Info Variables ->
let vars = ask_and_reduce man.ask (Q_defined_variables None) flow in
fprintf fmt "@[<v>%a@]@."
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
(fun fmt v -> Query.pp_var_with_type fmt (v,v.vtyp))
) vars
| Info Context ->
let ctx = Flow.get_ctx flow in
fprintf fmt "%a@." (pp_ctx man.lattice.print) ctx
| Trace ->
fprintf fmt "%a@." pp_trace state.trace
| _ -> assert false
let process_output_command cmd action envdb man flow =
match cmd.redirection with
| None ->
pp_output_command action envdb man flow Format.std_formatter cmd.kind
| Some(File file) ->
let old_print_color = !Debug.print_color in
Debug.print_color := false;
let output = asprintf "%a" (pp_output_command action envdb man flow) cmd.kind in
Debug.print_color := old_print_color;
let ch = open_out file in
output_string ch output;
flush ch;
close_out ch
| Some(Pipe shell) ->
let old_print_color = !Debug.print_color in
let output = asprintf "%a" (pp_output_command action envdb man flow) cmd.kind in
Debug.print_color := old_print_color;
let in_ch, out_ch = Unix.open_process shell in
output_string out_ch output;
flush out_ch;
close_out out_ch;
let rec iter () =
try
printf "%s@." (input_line in_ch);
iter ()
with End_of_file -> ()
in
iter ();
close_in in_ch
let rec read_command action envdb man flow =
let cmd =
try read_terminal_command logger flow
with Exit -> exit 0
in
match cmd.kind with
| Break loc ->
let () =
try
let default_file =
try get_range_file (action_range action)
with _ -> "" in
let bp = parse_breakpoint default_file loc in
breakpoints := BreakpointSet.add bp !breakpoints;
with Invalid_breakpoint_syntax -> printf "Invalid breakpoint syntax@." in
read_command action envdb man flow
| Continue ->
Interface.Continue
| Next ->
Next
| NextI ->
NextI
| Step ->
Step
| StepI ->
StepI
| Finish ->
Finish
| Backward ->
Backward
| Enable (Hook hook) ->
if not (Hook.mem_hook hook) then (
printf "Hook '%s' not found@." hook;
read_command action envdb man flow
) else (
Hook.activate_hook hook;
let ctx = Hook.init_hook hook (Flow.get_ctx flow) in
let flow = Flow.set_ctx ctx flow in
read_command action envdb man flow
)
| Disable (Hook hook) ->
if not (Hook.mem_hook hook) then (
printf "Hook '%s' not found@." hook
) else (
Hook.deactivate_hook hook man flow
);
read_command action envdb man flow
| Set (Debug, channel) ->
Debug.set_channels channel;
read_command action envdb man flow
| Unset Debug ->
Debug.set_channels "";
read_command action envdb man flow
| Set (Script, filename) ->
let ch = open_out filename in
script := Some ch;
read_command action envdb man flow
| Unset Script ->
let () = match !script with
| None -> ()
| Some ch ->
close_out ch;
script := None in
read_command action envdb man flow
| LoadScript s ->
let ch = open_in s in
let lines =
let rec process res =
try
process ((input_line ch) :: res)
with End_of_file ->
List.rev res
in process []
in
List.iter (fun l -> Queue.add l commands_buffer) lines;
close_in ch;
read_command action envdb man flow
| Set (ShowVarScope, _) ->
opt_show_var_scope := true;
read_command action envdb man flow
| Unset ShowVarScope ->
opt_show_var_scope := false;
read_command action envdb man flow
| BackTrace
| MopsaBackTrace
| Print _
| Env _
| State
| Where
| Info _
| Trace ->
process_output_command cmd action envdb man flow;
read_command action envdb man flow
let finish man flow =
()
let error ex =
printf "%a@\n%a@."
(Debug.color_str Debug.red) "Analysis aborted"
(fun fmt -> function
| Exceptions.Panic (msg, "") -> fprintf fmt "panic: %s@." msg
| Exceptions.Panic (msg, loc) -> fprintf fmt "panic raised in %s: %s@." loc msg
| Exceptions.PanicAtLocation (range, msg, "") -> fprintf fmt "panic in %a: %s@." Location.pp_range range msg
| Exceptions.PanicAtLocation (range, msg, loc) -> fprintf fmt "%a: panic raised in %s: %s@." Location.pp_range range loc msg
| Exceptions.PanicAtFrame (range, cs, msg, "") -> fprintf fmt "panic in %a: %s@\nTrace:@\n%a@." Location.pp_range range msg pp_callstack cs
| Exceptions.PanicAtFrame (range, cs, msg, loc) -> fprintf fmt "%a: panic raised in %s: %s@\nTrace:@\n%a@." Location.pp_range range loc msg pp_callstack cs
| Exceptions.SyntaxError (range, msg) -> fprintf fmt "%a: syntax error: %s@." Location.pp_range range msg
| Exceptions.UnnamedSyntaxError range -> fprintf fmt "%a: syntax error@." Location.pp_range range
| Exceptions.SyntaxErrorList l ->
fprintf fmt "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 ->
fprintf fmt "Syntax errors:@\n @[%a@]@."
(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@\n") Location.pp_range)
l
| ex -> fprintf fmt "Uncaught exception: %s@." (Printexc.to_string ex)
) ex
end