package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

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 (* The current stack must contain the call to the builting creating the thread *)
  | Kstmt stmt ->
    stmt, Option.get (Callstack.pop analysis.curr_stack)

(* -------------------------------------------------------------------------- *)
(* --- Specialized logging functions                                      --- *)
(* -------------------------------------------------------------------------- *)
(* To be used only inside hooks, as it makes pretty bold assumptions on
   the shape of the 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)

(* Auxiliary function that aborts a hook when a conversion of something
   into a proper value fails *)
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 ()

(* -------------------------------------------------------------------------- *)
(* --- Specialization of id function                                          *)
(* -------------------------------------------------------------------------- *)

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


(* -------------------------------------------------------------------------- *)
(* --- Constants written in memory to store states                        --- *)
(* -------------------------------------------------------------------------- *)
(* Currently not used, because we would need them inside pattern-matching *)

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


(* -------------------------------------------------------------------------- *)
(* --- Basic, per-thread, checking                                        --- *)
(* -------------------------------------------------------------------------- *)

(* This section is used to check the consistency of the information we store
   into the ids of threads, mutexes, etc. *)

(* Auxiliary function which extracts the information into the id and
   call dispatch functions, or return errors when the information is
   not of the proper form *)
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

(* -------------------------------------------------------------------------- *)
(* --- External values for shared zones                                   --- *)
(* -------------------------------------------------------------------------- *)

(* XXX: we should sync values only for the threads that may be alive at this
   point *)
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 ->
    (* As no thread is running, just skip the synchronization. *)
    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

(* -------------------------------------------------------------------------- *)
(* --- Creation of a thread                                               --- *)
(* -------------------------------------------------------------------------- *)

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 (
      (* Fields that are being joined *)
      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
    (* We clean the state that will be used by the created thread *)
    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);
    (* Thread is started as suspended *)
    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"
(* By typing, Frama_C_thread_create must receive at least those
   arguments *)


let update_initial_state analysis th state =
  (* From now on, at least two threads are running *)
  let state = thread_is_running state in
  (* Remove references local to the parent thread *)
  let state_started = Mt_memory.clear_non_globals state in
  (* Mutexes should be unlocked in the new threads *)
  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;
  (* Update the state of the creator too: more than one thread is running,
     and the values written by the thread just created become visible. *)
  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;
            (* TODO: add an event + add a recompute reason *)
            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 extract_action 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"


(* Auxiliary functions for the functions that act on mutexes (currently
   lock and release). [check] is the function that checks that the state
   of the information stored in the mutex is consistent with the action
   being performed, and the value with which to update the state.
   [evt] returns the corresponding mthread event. *)
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
      (* XXX: take which mutex is locked into account, and update only
         those values *)
      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))

  | _ -> (* really unlikely unless the code and/or the C binding
            are really strange *)
    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)

  | _ -> (* really unlikely unless the code and/or the C binding
            are really strange *)
    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                                                 --- *)
(* -------------------------------------------------------------------------- *)

(* All the Mthread builtin functions, together with their C name.
   The remainder of the conversion to the real type of the callback
   {Builtins.register_builtin} occurs in [Mt_main] *)
let mthread_builtins =
  [
    (* Threads *)
    "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;
    (* Mutexes *)
    "Frama_C_mutex_init", hook_init_mutex, `Pop;
    "Frama_C_mutex_lock", hook_lock_mutex, `Pop;
    "Frama_C_mutex_unlock", hook_release_mutex, `Pop;
    (* Message queues *)
    "Frama_C_queue_init", hook_queue_init, `Pop;
    "Frama_C_queue_send", hook_send_msg, `Pop;
    "Frama_C_queue_receive", hook_receive_msg, `Pop;
    (* Misc *)
    "Frama_C_mthread_show", hook_dummy_message, `NoPop;
    (* Shared values *)
    "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

(* Function to register as a callback of the Eva analysis if Mthread
   is enabled *)
let catch_functions_calls analysis (stack : Callstack.callstack) kf state kind =
  analysis.curr_stack <- stack;
  if Callstack.is_empty stack then
    (* This is the entry point of the analysis, the events stack needs to be
       empty. *)
    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 -> (* A thread function has been called as main, and we fail
                  immediately. In fact, this case should not happen,
                  because we reject calls to __FRAMA_C_* functions as
                  main or during thread spawning. We could detect when
                  the stack has only one element (ie. pthread_* has
                  been called has main, but the error message arrives
                  too late, and is not really readable *)
       Mt_options.abort "Thread function %s called as starting thread \
                         function" f

     | Some stack ->
       (* For mthread builtin functions, we may remove the top of the stack.
          This way, the mthread events appear at the level of the C
          function, instead of inside a function with a strange name *)
       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
    (* Beginning of the main thread (kf being the entry point). For the main
       thread, it might have not been registered yet if we are at the
       first iteration. *)
    let th = main_thread kf state in
    (* This call registers the main thread on the first run, and essentially
       does nothing afterwards *)
    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
      (* On the first run, the record [th] is created. It is not contained
         anywhere else, so we update the fields below. *)
      analysis.main_thread <- th;
      analysis.curr_thread <- th;
      (* We are currently computing this thread (the main one) and we have
         just started, no need to recompute it at the next iteration *)
      th.th_to_recompute <- SetRecomputeReason.empty;
      (* On the first iteration, also register the interrupt handlers *)
      let interrupt_handlers = Mt_options.InterruptHandlers.get () in
      let interrupts, state =
        Kernel_function.Set.fold
          (fun kf_interrupt (interrupts, state) ->
             (* Create and spawn the interrupt thread *)
             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
             (* Start the interrupt thread *)
             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
        (* If any interrupt handler has been registered, then their initial
           state and the initial state of the main thread need to be updated
           so that they all are considered running. *)
        List.iter
          (fun th ->
             let _ = update_initial_state analysis th.th_eva_thread state in ())
          (th :: interrupts)
      end
    end
  end;
  push_function_call analysis;
  (* If the function is a leaf one, we register the accesses that occur
     through \assigns ACSL specifications, then pop the stack. If there is a
     definition, the registering will be done by another hook, at the end of
     the execution of the function *)
  match kind with
  | `Spec | `Builtin ->
    Mt_shared_vars.register_concurrent_var_accesses analysis (`Leaf state);
    pop_function_call analysis;
  | `Body | `Reuse -> ()

(* Function registered by [Cvalue_callbacks.register_call_results_hook].
   Given the end states of a function with a definition, records the variable
   accesses it did. *)
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
    (* Merge the memoized results in the current analysis *)
    register_multiple_events analysis events;
    pop_function_call analysis;
  | `Builtin _ | `Spec _ -> ()
OCaml

Innovation. Community. Security.