Source file mt_analysis_hooks.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
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
open Eva_ast
open Mt_lib
open Mt_cil
open Mt_memory.Types
open Mt_types
open Mt_shared_vars_types
open Mt_thread
let wrap_res res = Some (Mt_memory.int_to_value res)
let no_res = (None : value option)
type hook_sig = (exp * value) list -> state * value option
let current_loc analysis =
match Callstack.top_callsite analysis.curr_stack with
| Kglobal -> assert false
| Kstmt stmt ->
stmt, Option.get (Callstack.pop analysis.curr_stack)
let log_poly ?(pop_stack=true) ?(kind=Log.Result) analysis =
let stack = analysis.curr_stack in
let stack =
if not pop_stack || Mt_options.PopTopFunctionForCallbacks.get ()
then stack
else Option.value (Callstack.pop stack) ~default:stack
in
let ki = Callstack.top_callsite stack in
let source = kinstr_to_source ki in
let pp_callstack =
Mt_options.PrintCallstacks.get () || Mt_options.debug_level () > 1 in
let append = (fun fmt -> if pp_callstack then
Format.fprintf fmt "@.%a" Callstack.pretty stack)
in { ppp = fun fmt ->
Mt_options.MThread.log ~kind ~once:true ?source ~append
("@[" ^^ fmt ^^ "@]")
}
let log ?(pop_stack=true) ?(kind=Log.Result) analysis =
(log_poly ~pop_stack ~kind analysis).ppp
exception Hook_failure of int
let default_err_code = -255
let hook_fail ?(code=default_err_code) () =
raise (Hook_failure code)
let catch_conversion analysis msg_main v ?(pop_stack=true) ?(code=default_err_code) ?msg () =
let warn fm msg_end =
let msg = match msg with
| Some msg -> ":@ " ^^ msg
| None -> ""
in
log ~kind:Log.Warning analysis ~pop_stack "@[%(%)%(%).@ %t%(%)@]"
msg_main msg fm msg_end;
in
match v with
| `Success v -> v
| `WithWarning (w, v) ->
warn w "";
v
| `Failure w ->
warn w "@ Ignoring.";
hook_fail ~code ()
let find_failure kind id =
let pp fmt =
Format.fprintf fmt
"Id %d for %s does not exists@ (incrementation@ inside@ program?)."
id kind
in
`Failure pp
let find_thread id =
match Thread.find id with
| Some th -> `Success th
| None -> find_failure "thread" id
let find_mutex id =
match Mutex.find id with
| Some m -> `Success m
| None -> find_failure "mutex" id
let find_queue id =
match Mqueue.find id with
| Some q -> `Success q
| None -> find_failure "queue" id
let _s_thread_unknown = 0
let _s_thread_started = 1
let _s_thread_cancelled = 2
let _s_mutex_not_init = 0
let _s_mutex_init = 1
let _s_mutex_locked = 2
let _queue_not_init = 0
let _queue_init = 1
let check_id_content default_msg msg_int id state =
let pb pp v = default_msg.pf pp v in
let value = Mt_ids.read_id_state state id in
match Locations.Location_Bytes.fold_i (fun b i l -> (b,i) :: l) value [] with
| [Base.Null,i] ->
(try
let r = Abstract_interp.Int.to_int_exn (Ival.project_int i) in
try msg_int r
with Not_found -> pb Format.pp_print_int r
with Ival.Not_Singleton_Int -> pb Ival.pretty i
)
| _ -> pb Cvalue.V.pretty value
(** When a thread is created, it must not inherit from its creator the status
of mutexes. This function sets all mutexes passed as argument to 1
(unlocked). *)
let reset_mutexes mutexes state =
Mutex.Set.fold
(fun mutex state -> Mt_ids.replace_id_value state (Mt_ids.of_mutex mutex) ~before:2 ~after:1)
mutexes state
let _mutex_state fmt = function
| 0 -> Format.fprintf fmt "not initialized"
| 1 -> Format.fprintf fmt "unlocked"
| 2 -> Format.fprintf fmt "locked"
| k -> Format.fprintf fmt "in an@ unknown@ state (%d)" k
let _thread_state fmt = function
| 0 -> Format.fprintf fmt "not created"
| 1 -> Format.fprintf fmt "started"
| 2 -> Format.fprintf fmt "suspended"
| 3 -> Format.fprintf fmt "cancelled"
| k -> Format.fprintf fmt "in an@ unknown@ state (%d)" k
let check_thread_not_already_started warn th state =
check_id_content
{ pf = fun pp v -> warn.ppp
"Unable to determine that thread %a@ has not already been started.@ \
%a should be 0@." Thread.pretty th pp v;
}
(function
| 2 -> ()
| 0 ->
warn.ppp "Thread %a@ might not be created yet@." Thread.pretty th;
| 1 ->
warn.ppp "Thread %a@ might have already been started@ by the \
current thread.@." Thread.pretty th;
| 3 ->
warn.ppp "Thread %a@ might have been cancelled @ by the \
current thread.@." Thread.pretty th;
| _ -> raise Not_found)
(Mt_ids.of_thread th) state
let check_thread_not_already_suspended warn th state =
check_id_content
{ pf = fun pp v -> warn.ppp
"Unable to determine that thread %a@ has not already been suspended.@ \
%a should be 0@." Thread.pretty th pp v;
}
(function
| 1 -> ()
| 0 ->
warn.ppp "Thread %a@ might not be created yet@." Thread.pretty th;
| 2 ->
warn.ppp "Thread %a@ might have already been suspended@ by the \
current thread.@." Thread.pretty th;
| 3 ->
warn.ppp "Thread %a@ might have been cancelled @ by the \
current thread.@." Thread.pretty th;
| _ -> raise Not_found)
(Mt_ids.of_thread th) state
let check_thread_not_already_cancelled warn th state =
check_id_content
{ pf = fun pp v -> warn.ppp
"Unable to determine that thread %a@ has not already been cancelled.@ \
%a should be 0@." Thread.pretty th pp v;
}
(function
| 1 | 2 -> ()
| 0 ->
warn.ppp "Thread %a@ might not be created yet@." Thread.pretty th;
| 3 ->
warn.ppp "Thread %a@ might have been already cancelled @ by the \
current thread.@." Thread.pretty th;
| _ -> raise Not_found)
(Mt_ids.of_thread th) state
let check_mutex_not_already_initialized warn m state =
check_id_content
{ pf = fun pp v -> warn.ppp
"@[<hov>Unable to check that mutex %a@ has not been already \
initialized;@ %a should be 0@]@." Mutex.pretty m pp v }
(function
| 0 -> ()
| 1 -> warn.ppp "@[<hov>Mutex %a@ might be already initialized@]@."
Mutex.pretty m
| 2 -> warn.ppp "@[<hov>Mutex %a@ might be already initialized \
(and locked)@]@." Mutex.pretty m
| _ -> raise Not_found)
(Mt_ids.of_mutex m) state
let check_mutex_not_already_locked warn m state =
check_id_content
{ pf = fun pp v -> warn.ppp
"@[<hov>Unable to check that mutex %a@ has not already been locked;@ \
%a should be 1@]@." Mutex.pretty m pp v }
(function
| 1 -> ()
| 0 -> warn.ppp "@[<hov>Mutex %a@ might have not been initialized@]@."
Mutex.pretty m
| 2 -> warn.ppp "@[<hov>Mutex %a@ might have already been locked@]@."
Mutex.pretty m
| _ -> raise Not_found)
(Mt_ids.of_mutex m) state
let check_mutex_locked warn m state =
check_id_content
{ pf = fun pp v -> warn.ppp
"@[<hov>Unable to check that mutex %a@ has already been locked;@ \
%a should be 2@]@." Mutex.pretty m pp v }
(function
| 2 -> ()
| 0 -> warn.ppp "@[<hov>Mutex %a@ might be uninitialized@]@."
Mutex.pretty m
| 1 -> warn.ppp "@[<hov>Mutex %a@ might not be locked@]@."
Mutex.pretty m
| _ -> raise Not_found)
(Mt_ids.of_mutex m) state
let check_queue_not_already_initialized warn q state =
check_id_content
{ pf = fun pp v -> warn.ppp
"@[<hov>Unable to check that queue %a@ has not been already \
initialized;@ %a should be 0@]@." Mqueue.pretty q pp v }
(function
| 0 -> ()
| 1 -> warn.ppp "@[<hov>Queue %a@ might be@ already@ initialized@]@."
Mqueue.pretty q | _ -> raise Not_found)
(Mt_ids.of_queue q) state
let check_queue_already_initialized warn q state =
check_id_content
{ pf = fun pp v -> warn.ppp
"@[<hov>Unable to check that queue %a@ is@ already \
initialized;@ %a should be 0@]@." Mqueue.pretty q pp v }
(function
| 1 -> ()
| 0 -> warn.ppp "@[<hov>Queue %a@ might be@ uninitialized@]@."
Mqueue.pretty q
| _ -> raise Not_found)
(Mt_ids.of_queue q) state
let sync_values analysis state =
let join ~written ~state =
Cvalue.Model.fold
(fun b offsm state ->
let offsm' = Cvalue.Model.find_base_or_default b state in
match offsm' with
| `Top -> Mt_options.fatal "Top state"
| `Bottom -> state
| `Value offsm' ->
let offsm'' = Cvalue.V_Offsetmap.join offsm offsm' in
Cvalue.Model.add_base b offsm'' state)
written state
in
let v = Mt_shared_vars.var_thread_created () in
let value = Results.(in_cvalue_state state |> eval_var v |> as_cvalue) in
match Mt_memory.extract_int value with
| `Success 0 ->
state
| _ ->
fold_threads analysis state
(fun th state ->
match th.th_values_written with
| Cvalue.Model.Bottom -> state
| Cvalue.Model.Top -> Cvalue.Model.top
| Cvalue.Model.Map written ->
if not (ThreadState.equal analysis.curr_thread th) then
join ~written ~state
else state
)
let hook_sync analysis state : hook_sig = function _ ->
sync_values analysis state, no_res
let basic_thread eva_thread stack func state params parent = {
th_eva_thread = eva_thread;
th_stack = stack;
th_init_state = state;
th_fun = func;
th_params = params;
th_parent = parent;
th_to_recompute = SetRecomputeReason.empty;
th_read_written = AccessesByZone.empty_map;
th_amap = Trace.empty;
th_cfg = Mt_cfg_types.CfgNode.dead;
th_read_written_cfg = Mt_cfg_types.AccessesByZoneNode.empty_map;
th_values_written = Cvalue.Model.empty_map;
th_projects = [];
th_value_results = None;
th_priority= PDefault;
}
let spawn_thread analysis eva_thread stack func state params parent =
try
let th' = Thread.Hashtbl.find analysis.all_threads eva_thread in
if Option.equal ThreadState.equal parent th'.th_parent = false
then (
let pp_parent = Pretty_utils.pp_opt ~none:"<none>" ThreadState.pretty in
log ~kind:Log.Error analysis "Thread '%a' is launched@ by two different \
threads@ (%a and %a).@ Ignoring"
Thread.pretty eva_thread
pp_parent parent
pp_parent th'.th_parent;
hook_fail ())
else if Callstack.equal stack th'.th_stack = false then (
log ~kind:Log.Error analysis
"Thread '%a' is launched in two different contexts:@.\
Context 1:@.@[<hov 2> %a@]@.Context 2:@.@[<hov 2> %a@]@.Ignoring"
Thread.pretty eva_thread
Callstack.pretty stack
Callstack.pretty th'.th_stack;
hook_fail ())
else if Kernel_function.get_id func <> Kernel_function.get_id th'.th_fun
then (
log ~kind:Log.Error analysis
"Thread '%a' can be two different functions@ \
(%s and %s).@ Imprecise pointer?@ Ignoring."
Thread.pretty eva_thread
(Kernel_function.get_name func)
(Kernel_function.get_name th'.th_fun);
hook_fail ())
else (
let init_state', ris = Mt_memory.join_state th'.th_init_state state
and args, ra = Mt_memory.join_params th'.th_params params
in
th'.th_init_state <- init_state';
th'.th_params <- args;
if ris then ThreadState.recompute_because th' InitialEnvChanged;
if ra then ThreadState.recompute_because th' InitialArgsChanged;
let text =
if ris || ra then "New context for" else "Thread" in
log ~kind:Log.Result analysis "@[<hov 2>%s@ %a@]" text ThreadState.pretty_detailed th';
th'
)
with Not_found ->
let th = basic_thread eva_thread stack func state params parent in
th.th_to_recompute <- SetRecomputeReason.singleton FirstIteration;
Thread.Hashtbl.add analysis.all_threads eva_thread th;
log ~kind:Log.Result analysis "@[<hov>New thread: %a@]" ThreadState.pretty_detailed th;
th
let standalone_thread th kf initial_state =
match kf.Cil_types.fundec with
| Declaration (_, f, _, _) ->
Mt_options.fatal "Entry point '%s' has no definition : cannot run %a."
f.vname
Thread.pretty th
| Definition (fundec, _) ->
let formals = fundec.sformals in
let eval_arg vi =
Results.(in_cvalue_state initial_state |> eval_var vi |> as_cvalue)
in
let args = List.map eval_arg formals in
let stack = Callstack.init kf in
basic_thread th stack kf initial_state args None
let main_thread k_main initial_state =
standalone_thread Thread.main k_main initial_state
let interrupt_thread kf initial_state =
let th = Thread.interrupt_handler kf in
standalone_thread th kf initial_state
(** Set the global variable that indicates that at least one thread is running
to one *)
let thread_is_running state =
let p_thread_running = Mt_shared_vars.var_thread_created (), 0 in
Mt_memory.write_int_pointer p_thread_running 1 state
(** Hook registered in the value analysis for the creation of thread *)
let hook_thread_creation analysis state : hook_sig = function
| (_, name) :: (_, f) :: params ->
let conv v = catch_conversion analysis "During@ thread@ creation" v in
let kf = conv (Mt_memory.extract_fun f)
~msg:"invalid@ thread@ function" () in
let formals = Kernel_function.get_formals kf in
let rec trunc_params = function
| [], [] -> []
| _formal :: qf, param :: qp -> param :: trunc_params (qf, qp)
| [], (_ :: _ as params) ->
if Mt_options.ModerateWarnings.get () then
log ~kind:Log.Warning analysis
"@[During thread@ creation,@ mismatch@ between@ function \
'%s'@ signature and@ actual arguments.@ Ignoring@ last \
%d argument(s)@ and@ continuing.@]"
(Kernel_function.get_name kf) (List.length params);
[]
| _ :: _, [] ->
log ~kind:Log.Error analysis
"@[When creating@ thread@ from@ function %s:@ too@ few@ \
arguments,@ %d expected@ but@ %d given.@ Ignoring.@]"
(Kernel_function.get_name kf)
(List.length formals) (List.length params);
hook_fail ()
in
let params = List.map snd (trunc_params (formals, params)) in
let eva_thread =
let name = Concurrency.Name.of_cvalue name in
let aloc = current_loc analysis in
Thread.spawn aloc name kf params
in
ignore (spawn_thread analysis eva_thread analysis.curr_stack kf
Cvalue.Model.bottom params (Some analysis.curr_thread));
register_event analysis (CreateThread eva_thread);
Mt_ids.write_id_state state (Mt_ids.of_thread eva_thread) 2,
wrap_res (Thread.id eva_thread)
| _ -> Mt_options.fatal "Incorrect mthread binding for thread creation"
let update_initial_state analysis th state =
let state = thread_is_running state in
let state_started = Mt_memory.clear_non_globals state in
let state_started = reset_mutexes analysis.all_mutexes state_started in
let th = Thread.Hashtbl.find analysis.all_threads th in
let initial, changed = Mt_memory.join_state th.th_init_state state_started in
if changed then (
ThreadState.recompute_because th Mt_thread.InitialEnvChanged;
if Cvalue.Model.is_reachable th.th_init_state then
log ~kind:Log.Result analysis "@[<hov 2>New context for@ %a@]"
ThreadState.pretty_detailed th;
);
th.th_init_state <- initial;
sync_values analysis state
let hook_thread_start_suspend fname check v aux_state evt analysis state : hook_sig = function
| [_, offset] ->
let conv v = catch_conversion analysis ("During@ thread@ " ^^ fname) v in
let offset = conv (Mt_memory.extract_int offset)
~msg:"invalid@ thread@ id" () in
if offset <> 0 then
let th = conv (find_thread offset)
~msg:"unkonwn@ thread" () in
(check (log_poly ~kind:Log.Warning analysis) th state : unit);
let evt = evt th in
log ~kind:Log.Result analysis "@[%a@]" Event.pretty evt;
register_event analysis evt;
let state_started = aux_state analysis th (state:state) in
Mt_ids.write_id_state state_started (Mt_ids.of_thread th) v, wrap_res 0
else (
log ~kind:Log.Warning analysis
"Trying to@ %(%)@ unknown thread.@ Ignoring." fname;
hook_fail ~code:(-1) ())
| _ -> Mt_options.fatal "Incorrect mthread binding for thread %(%)" fname
(** Hook registered in the value analysis when a thread is started *)
let hook_thread_start =
hook_thread_start_suspend
"start" check_thread_not_already_started 1 update_initial_state
(fun i -> StartThread i)
let hook_thread_suspend =
hook_thread_start_suspend
"suspend" check_thread_not_already_suspended 2 (fun _ _ s -> s)
(fun i -> SuspendThread i)
let hook_thread_cancellation analysis state : hook_sig = function
| [_, offset] ->
let conv v = catch_conversion analysis "During@ thread@ cancellation" v in
let offset = conv (Mt_memory.extract_int offset)
~msg:"invalid@ thread@ id" () in
if offset <> 0 then
let th = conv (find_thread offset)
~msg:"unkonwn@ thread" () in
check_thread_not_already_cancelled
(log_poly ~kind:Log.Warning analysis) th state;
register_event analysis (CancelThread th);
Mt_ids.write_id_state state (Mt_ids.of_thread th) 2, wrap_res 0
else (
log ~kind:Log.Warning analysis
"Trying to@ cancel@ unknown thread.@ Ignoring.";
hook_fail ~code:(-1) ())
| _ -> Mt_options.fatal "Incorrect mthread binding for thread cancellation \
(only the thread id is expected)"
let hook_thread_exit analysis (_state: state) : hook_sig = function
| [_, v] ->
if ThreadState.is_main analysis.curr_thread then (
log ~kind:Log.Error analysis
"Call@ to@ thread@ exit@ primitive@ inside@ main@ thread. Ignoring";
hook_fail ())
else (
register_event analysis (ThreadExit v);
log ~kind:Log.Result analysis "Thread@ exiting@ with@ value %a"
Cvalue.V.pretty v;
Cvalue.Model.bottom, no_res)
| _ -> Mt_options.fatal "Incorrect mthread binding for thread exit \
(only the return value is expected)"
let hook_thread_id analysis state : hook_sig = fun _ ->
state, wrap_res (Thread.id analysis.curr_thread.th_eva_thread)
let hook_thread_priority analysis state : hook_sig = function
|[ _, p] ->
begin
let p = catch_conversion analysis
"During@ thread@ priority@ definition" (Mt_memory.extract_int p)
~msg:"invalid@ thread@ id" ()
in
begin
match analysis.curr_thread.th_priority with
| PPriority p' ->
if p <> p' then begin
log ~kind:Log.Warning analysis
"Conflicting priorities (previous: %d, new %d) for thread '%a'."
p
p'
ThreadState.pretty analysis.curr_thread;
analysis.curr_thread.th_priority <- PUnknown;
end
| PUnknown -> ()
| PDefault ->
log analysis "Setting priority to %d" p;
analysis.curr_thread.th_priority <- PPriority p;
end;
state, wrap_res 0
end
| _ -> Mt_options.fatal "Incorrect mthread binding for thread priority \
(only a non negative integer is expected)"
(** --- Hook registered in the value analysis related to messages --- *)
let hook_queue_init analysis state : hook_sig = function
| [_, name; _, size] ->
let conv v =
catch_conversion analysis "During@ queue@ initialization" v
in
let aloc = current_loc analysis
and name = Concurrency.Name.of_cvalue name
and size = conv (Mt_memory.extract_int size) ~msg:"invalid@ size" () in
let q = Mqueue.create aloc name in
analysis.all_queues <- Mqueue.Set.add q analysis.all_queues;
check_queue_not_already_initialized
(log_poly ~kind:Log.Warning analysis) q state;
let size = if size < 0 then None else Some size in
register_event analysis (CreateQueue (q, size));
Mt_ids.write_id_state state (Mt_ids.of_queue q) 1,
wrap_res (Mqueue.id q)
| _ -> Mt_options.fatal "Incorrect mthread binding for queue creation"
let hook_send_msg analysis state : hook_sig = function
| [(_, offset); (_exp_content, content); (_exp_size, size)] ->
let conv v = catch_conversion analysis "During@ message@ sending" v in
let offset = conv (Mt_memory.extract_int offset)
~msg:"invalid@ queue@ id" () in
if offset <> 0 then
let sbytes = conv (Mt_memory.extract_int size)
~msg:"invalid@ message@ size" () in
if sbytes <= 0 then
conv (`Failure (fun fmt -> Format.fprintf fmt
"Invalid message length %d." sbytes)) ();
let q = conv (find_queue offset) () in
let content = Mt_memory.read_slice ~p:content ~sbytes state in
check_queue_already_initialized
(log_poly ~kind:Log.Warning analysis) q state;
let action = SendMsg (q, (content, sbytes)) in
log ~kind:Log.Result analysis "@[%a@]" Event.pretty action;
register_event analysis action;
state, wrap_res 0
else (
log ~kind:Log.Warning analysis
"@[<hov>Trying to@ send@ message@ on@ uninitialized@ queue.@ \
Ignoring@]";
state, wrap_res (-1))
| _ -> Mt_options.fatal "Incorrect mthread binding for message sending"
let find_msg_content analysis q =
let th acc = function
| SendMsg (q', (v, size)) ->
if Mqueue.equal q q' then (th, v, size) :: acc else acc
| _ -> acc
in
fold_threads analysis []
(fun { th_eva_thread = th; th_amap = m } ->
Trace.fold' m (fun a r -> extract_action th r a))
let hook_receive_msg analysis state : hook_sig = function
| [(_,offset); (_e_size, size); (e_loc, loc)] ->
let conv v = catch_conversion analysis "During@ message@ reception" v in
let offset = conv (Mt_memory.extract_int offset)
~msg:"invalid@ queue@ id" () in
if offset <> 0 then
let smax = conv (Mt_memory.extract_int size) ~msg:"invalid@ size" ()
and p = conv (Mt_memory.extract_pointer loc)
~msg:"invalid@ destination@ buffer" () in
let q = conv (find_queue offset) () in
check_queue_already_initialized
(log_poly ~kind:Log.Warning analysis) q state;
let action = ReceiveMsg (q, p, smax) in
register_event analysis action;
let contents = find_msg_content analysis q in
let state, res, pp =
if contents <> [] then
let length, kept_mess, _, state =
List.fold_left
(fun (length, kept_mess, exact, state) (_, slice, smess as mess) ->
let sbytes = min smess smax in
let state' =
Mt_memory.write_slice ~p ~sbytes ~slice ~exact state
in
if Cvalue.Model.is_reachable state' then
let sbytes_val =
Cvalue.V.inject_ival (Ival.of_int sbytes) in
let length' = Cvalue.V.join sbytes_val length in
length', mess :: kept_mess, false, state'
else (
log ~kind:Log.Warning analysis
"Found message@ of length %d,@ which is@ too long@ \
for buffer '%a'. Execution@ will@ continue@ without@ \
those@ messages.@.(Ignore \"This path is assumed to \
be dead message if any\".)"
smess pp_exp e_loc;
length, kept_mess, exact, state)
)
(Cvalue.V.bottom, [], true, state) contents
in
match kept_mess with
| [] ->
Cvalue.Model.bottom,
no_res,
(fun fmt -> Format.fprintf fmt "No valid value@ to receive.")
| _ :: _ ->
let pp fmt =
Format.fprintf fmt "Possible %s values:@.%a"
(if List.length kept_mess = List.length contents
then "" else "valid ")
(Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@,"
(fun fmt (th, v, _) ->
Format.fprintf fmt "@[From thread %a:@ %a@]"
Thread.pretty th
Mt_memory.pretty_slice v
)) kept_mess
in
state, Some length, pp
else
Cvalue.Model.bottom,
no_res,
(fun fmt -> Format.fprintf fmt "No value@ to receive (yet?).")
in
log ~kind:Log.Result analysis "@[<hov>%a@ %t@]"
Event.pretty action pp;
state, res
else (
log ~kind:Log.Warning analysis
"Trying@ to@ receive@ value@ on@ non-initialized@ queue. Ignoring.";
state, wrap_res (-2))
| _ -> Mt_options.fatal "Incorrect mthread binding for message reception"
let aux_mutex ~operation:op ~check ~event analysis state : hook_sig = function
| [_, offset] ->
let f_check, value = check in
let conv v = catch_conversion analysis ("During@ mutex@ " ^^ op) v in
let offset, exact = conv (Mt_memory.extract_int_possibly_zero offset)
~msg:"invalid@ mutex@ id" () in
if exact = `WithZero then log ~kind:Log.Warning analysis
"@[<hov>Trying to@ %(%)@ a possibly@ uninitialized@ mutex.@]" op;
if offset <> 0 then
let m = conv (find_mutex offset) () in
f_check (log_poly ~kind:Log.Warning analysis) m state;
let evt : event = event m in
log ~kind:Log.Result analysis "%a" Event.pretty evt;
register_event analysis evt;
let state_op = Mt_ids.write_id_state state (Mt_ids.of_mutex m) value in
let with_external = sync_values analysis state_op in
with_external, wrap_res 0
else (
log ~kind:Log.Warning analysis
"@[<hov>Trying to@ %(%)@ uninitialized@ mutex.@ Ignoring@]" op;
state, wrap_res (-1))
| _ ->
Mt_options.fatal "Incorrect mthread binding for mutex function"
let hook_init_mutex analysis state : hook_sig = function
| [_, name] ->
let aloc = current_loc analysis
and name = Concurrency.Name.of_cvalue name in
let mutex = Mutex.create aloc name in
analysis.all_mutexes <- Mutex.Set.add mutex analysis.all_mutexes;
check_mutex_not_already_initialized
(log_poly ~kind:Log.Warning analysis) mutex state;
log ~kind:Log.Result analysis "Initializing mutex %a" Mutex.pretty mutex;
Mt_ids.write_id_state state (Mt_ids.of_mutex mutex) 1,
wrap_res (Mutex.id mutex)
| _ ->
Mt_options.fatal "Incorrect mthread binding for mutex function"
let hook_lock_mutex =
aux_mutex ~operation:"lock" ~check:(check_mutex_not_already_locked, 2)
~event:(fun id -> MutexLock id)
let hook_release_mutex =
aux_mutex ~operation:"unlock" ~check:(check_mutex_locked, 1)
~event:(fun id -> MutexRelease id)
(** --- Misc --- *)
let hook_dummy_message analysis state : hook_sig = function
| (_, name) :: args ->
let conv v = catch_conversion analysis ~pop_stack:false
"During@ unknown@ event" v in
let name = conv (Mt_memory.extract_constant_string name)
~msg:"invalid@ event@ name" () in
let evt = Dummy (name, List.map snd args) in
register_event analysis evt;
log ~pop_stack:false ~kind:Log.Result analysis
"Monitored event:@ %a" Event.pretty evt;
state, no_res
| _ -> Mt_options.fatal "Incorrect mthread binding for unknown event"
(** --- Main declarations --- *)
let mthread_builtins =
[
"Frama_C_thread_create", hook_thread_creation, `Pop;
"Frama_C_thread_start", hook_thread_start, `Pop;
"Frama_C_thread_suspend", hook_thread_suspend, `Pop;
"Frama_C_thread_cancel", hook_thread_cancellation, `Pop;
"Frama_C_thread_exit", hook_thread_exit, `Pop;
"Frama_C_thread_id", hook_thread_id, `Pop;
"Frama_C_thread_priority", hook_thread_priority, `Pop;
"Frama_C_mutex_init", hook_init_mutex, `Pop;
"Frama_C_mutex_lock", hook_lock_mutex, `Pop;
"Frama_C_mutex_unlock", hook_release_mutex, `Pop;
"Frama_C_queue_init", hook_queue_init, `Pop;
"Frama_C_queue_send", hook_send_msg, `Pop;
"Frama_C_queue_receive", hook_receive_msg, `Pop;
"Frama_C_mthread_show", hook_dummy_message, `NoPop;
"Frama_C_mthread_sync", hook_sync, `Pop;
]
;;
let is_mthread_builtin s =
try
let (_, _, pop) = List.find (fun (s', _, _) -> s = s') mthread_builtins in
pop
with Not_found -> `NotBuiltin
let mthread_builtins = List.map (fun (n, f, _) -> (n, f)) mthread_builtins
let catch_functions_calls analysis (stack : Callstack.callstack) kf state kind =
analysis.curr_stack <- stack;
if Callstack.is_empty stack then
analysis.curr_events_stack <- [];
let f = Kernel_function.get_name kf in
let built = is_mthread_builtin f in
(if built <> `NotBuiltin then
match Callstack.pop analysis.curr_stack with
| None ->
Mt_options.abort "Thread function %s called as starting thread \
function" f
| Some stack ->
if Mt_options.PopTopFunctionForCallbacks.get () && built = `Pop then
analysis.curr_stack <- stack;
);
if Callstack.is_empty analysis.curr_stack &&
Thread.is_main analysis.curr_thread.th_eva_thread then begin
let th = main_thread kf state in
let th = spawn_thread analysis th.th_eva_thread
th.th_stack th.th_fun th.th_init_state th.th_params None in
if analysis.main_thread != th then begin
analysis.main_thread <- th;
analysis.curr_thread <- th;
th.th_to_recompute <- SetRecomputeReason.empty;
let interrupt_handlers = Mt_options.InterruptHandlers.get () in
let interrupts, state =
Kernel_function.Set.fold
(fun kf_interrupt (interrupts, state) ->
let th = interrupt_thread kf_interrupt state in
let th =
spawn_thread analysis th.th_eva_thread th.th_stack th.th_fun
th.th_init_state th.th_params None
in
let state =
Mt_ids.write_id_state state (Mt_ids.of_thread th.th_eva_thread) 1
in
(th :: interrupts, state))
interrupt_handlers
([], state)
in
if interrupts != [] then begin
List.iter
(fun th ->
let _ = update_initial_state analysis th.th_eva_thread state in ())
(th :: interrupts)
end
end
end;
push_function_call analysis;
match kind with
| `Spec | `Builtin ->
Mt_shared_vars.register_concurrent_var_accesses analysis (`Leaf state);
pop_function_call analysis;
| `Body | `Reuse -> ()
let catch_functions_record analysis stack _kf _pre_state = function
| `Body (Cvalue_callbacks.{before_stmts; after_stmts}, i) ->
analysis.curr_stack <- stack;
let hbefore = Lazy.force before_stmts in
let hafter = Lazy.force after_stmts in
Mt_shared_vars.register_concurrent_var_accesses analysis (`Final hbefore);
register_memory_states analysis ~before:hbefore ~after:hafter;
let cur_events = curr_events analysis in
Datatype.Int.Hashtbl.add analysis.memexec_cache i cur_events;
pop_function_call analysis;
| `Reuse i ->
let events = Datatype.Int.Hashtbl.find analysis.memexec_cache i in
register_multiple_events analysis events;
pop_function_call analysis;
| `Builtin _ | `Spec _ -> ()