package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file mt_thread.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
(**************************************************************************)
(*                                                                        *)
(*  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 Cil_types
open Mt_types
open Mt_shared_vars_types
open Mt_cfg_types

(* -------------------------------------------------------------------------- *)
(* --- Threads                                                            --- *)
(* -------------------------------------------------------------------------- *)


type recompute_reason =
  | FirstIteration
  | NewMsgReceived
  | PotentialSharedVarsChanged
  | SharedVarsValuesChanged
  | InitialArgsChanged
  | InitialEnvChanged
  | InterferencesChanged
;;


module RecomputeReason = struct

  type t = recompute_reason

  let compare r1 r2 = match r1, r2 with
    | FirstIteration, FirstIteration
    | NewMsgReceived, NewMsgReceived
    | SharedVarsValuesChanged, SharedVarsValuesChanged
    | PotentialSharedVarsChanged, PotentialSharedVarsChanged
    | InitialArgsChanged, InitialArgsChanged
    | InitialEnvChanged, InitialEnvChanged
    | InterferencesChanged, InterferencesChanged
      -> 0
    | (FirstIteration | NewMsgReceived | SharedVarsValuesChanged
      | PotentialSharedVarsChanged | InitialArgsChanged | InitialEnvChanged
      | InterferencesChanged),
      _ ->
      Mt_lib.compare_tag r1 r2

  let pretty fmt = function
    | FirstIteration -> Format.fprintf fmt "first@ iteration"
    | NewMsgReceived -> Format.fprintf fmt "new@ message@ received"
    | SharedVarsValuesChanged ->
      Format.fprintf fmt "shared@ vars@ values@ changed"
    | PotentialSharedVarsChanged ->
      Format.fprintf fmt "potential@ shared@ vars@ changed"
    | InitialArgsChanged -> Format.fprintf fmt
                              "thread@ initial@ arguments@ changed"
    | InitialEnvChanged -> Format.fprintf fmt
                             "thread@ initial@ memory@ state@ changed"
    | InterferencesChanged -> Format.fprintf fmt "interferences@ changed"

end


module SetRecomputeReason = Set.Make(struct
    type t = recompute_reason
    let compare = RecomputeReason.compare
  end)

type priority = PDefault | PUnknown | PPriority of int

module Priority = Datatype.Make_with_collections(struct
    type t = priority
    let name = "Mt_thread.priority"
    let reprs = [PPriority 0; PDefault; PUnknown]

    include Datatype.Undefined
    let compare: t -> t -> int = Extlib.compare_basic
    let equal = Datatype.from_compare
    let hash = Hashtbl.hash
  end)

type thread = Thread.t

type thread_state = {
  th_eva_thread : Thread.t;
  th_parent : thread_state option;
  th_fun : kernel_function;
  th_stack : Callstack.t;
  mutable th_init_state : Cvalue.Model.t;
  mutable th_params : Cvalue.V.t list;
  mutable th_amap : Trace.t;
  mutable th_to_recompute: SetRecomputeReason.t;
  mutable th_read_written: AccessesByZone.map;
  mutable th_cfg: CfgNode.t;
  mutable th_read_written_cfg: AccessesByZoneNode.map;
  mutable th_values_written: Mt_memory.Types.state;
  mutable th_projects: Project.t list;
  mutable th_value_results: Eva_results.results option;
  mutable th_priority: priority;
}

module ThreadState = struct
  type t = thread_state

(*
  open Unmarshal

  let help =
    let l = t_list Locations.Location_Bytes.Datatype.descr in
    let rec descr = Structure (Sum [|
      [| Id.descr;
         Structure (Sum [| [| descr|] |]);
         Kernel_function.Datatype.descr;
         Stack.descr;
         Relations_type.Model.Datatype.descr;
         l;
         Trace.descr;
         t_bool;
         MapVarAccesses.Datatype.descr;
         CfgNode.descr
      |]  |]) in
    descr
*)

  let label th = Thread.label th.th_eva_thread
  let is_main th = Thread.is_main th.th_eva_thread
  let pretty fmt th = Thread.pretty fmt th.th_eva_thread
  let equal th1 th2 = Thread.equal th1.th_eva_thread th2.th_eva_thread

  let pretty_detailed fmt th =
    let pp_parent fmt = function
      | None -> ()
      | Some p ->
        Format.fprintf fmt ",@ parent %a,@ args %a"
          pretty p
          (Pretty_utils.pp_list ~sep:",@ " Cvalue.V.pretty) th.th_params
    in
    Format.fprintf fmt "%a,@ fun %s%a"
      pretty th
      (Kernel_function.get_name th.th_fun)
      pp_parent th.th_parent

  let one_creates_other th1 th2 =
    let creates thp ths =
      let rec in_parents ths' = match ths'.th_parent with
        | None -> `Unrelated
        | Some th when equal thp th -> `Creates (thp, ths)
        | Some th -> in_parents th
      in
      in_parents ths
    in
    match creates th1 th2 with
    | `Unrelated -> creates th2 th1
    | _ as r -> r

  let recompute_because th r =
    if not (SetRecomputeReason.equal th.th_to_recompute
              (SetRecomputeReason.singleton FirstIteration))
    (* Can happen if the control-flow leading to the thread creation
       is split by the value analysis *)
    then
      th.th_to_recompute <- SetRecomputeReason.add r th.th_to_recompute
end



(* -------------------------------------------------------------------------- *)
(* --- Thread analysis                                                    --- *)
(* -------------------------------------------------------------------------- *)


type threads_table = thread_state Thread.Hashtbl.t

type analysis_state = {
  all_threads : threads_table (* List of all threads. Is kept (and can thus
                                 increase) from one iteration to the next *);

  mutable all_mutexes: Mutex.Set.t; (** Set of all mutexes of the analysis *)

  mutable all_queues: Mqueue.Set.t; (** Set of all queues of the analysis *)

  mutable iteration: int (* Current iteration of the analysis *);

  mutable main_thread: thread_state (* Starting thread *);

  mutable curr_thread: thread_state (* Thread currently running. *);

  mutable curr_events_stack: Trace.t list (* Mthread events that have been
                                             found during the current analysis of the current thread. The list
                                             has the same height as [curr_stack]. The top of the list is the trace
                                             containing the events for the function being analyzed by Value, and
                                             so on until the top of the list. When the list is popped, the events
                                             of the callee are merged inside the trace of the caller. *);

  mutable memexec_cache: Trace.t Datatype.Int.Hashtbl.t
(* Cache for the results obtained during the analysis of the current
   thread *);

  mutable curr_stack: Callstack.t
(* stack of a multithread event. Asynchronously set by a callback and used
   by another, because of a slightly too restricted signature in the
   value analysis. *);

  mutable concurrent_accesses: Locations.Zone.t
(* Shared variables that have been detected in the analysis so far
   in a global manner *);

  mutable precise_concurrent_accesses: Locations.Zone.t
(* Shared variables that have been detected in the analysis so far,
   through the various cfgs. Subset of the previous field *);

  mutable concurrent_accesses_by_nodes:
    (Locations.Zone.t * SetNodeIdAccess.t) list
(* List of concurrent accesses that have been found. Used to
   compute the field [precise_concurrent_accesses] *);
}

(* Iterators on threads. We presave the current list of threads so that
   the iterators do not accidentally capture new added threads. (This is not
   important for correctness, but is slightly cleaner.). Threads are sorted,
   agains for cleanliness reasons. *)
let threads analysis =
  (* the main thread always have the least id and will always be in front of the
     list *)
  Thread.Hashtbl.fold_sorted
    (fun _ th l -> th :: l)
    analysis.all_threads []
  |> List.rev

let thread_state analysis th =
  try Thread.Hashtbl.find analysis.all_threads th
  with Not_found -> Mt_options.fatal "Unknown thread %a" Thread.pretty th

let fold_threads analysis v f =
  List.fold_left (fun acc th -> f th acc) v (threads analysis)
let iter_threads analysis f =
  List.iter (fun th -> f th) (threads analysis)


let calling_ki analysis = Callstack.top_callsite analysis.curr_stack
let current_fun analysis = Callstack.top_kf analysis.curr_stack

let curr_events analysis =
  match analysis.curr_events_stack with
  | [] -> Mt_options.fatal "Invalid analysis stack"
  | h :: _ -> h

let on_current_trace analysis f =
  match analysis.curr_events_stack with
  | [] -> Mt_options.fatal "Invalid analysis stack"
  | h :: q ->
    analysis.curr_events_stack <- f h q :: q

(* Store a mthread event into the state of our analysis. *)
let register_event analysis ?(top=Callstack.top_call analysis.curr_stack) evt =
  on_current_trace analysis
    (fun cur _ -> Trace.add_event cur top evt)
;;

let register_multiple_events analysis evts =
  on_current_trace analysis
    (fun cur _ -> Trace.union evts cur)
;;

(* Store the memory state for the function which we finished analyzing *)
let register_memory_states analysis ~before ~after =
  Mt_options.debug ~level:2 "Recording states for %a"
    Kernel_function.pretty (current_fun analysis);
  on_current_trace analysis (fun cur _ ->  Trace.add_states cur ~before ~after);
;;

let push_function_call analysis =
  analysis.curr_events_stack <- Trace.empty :: analysis.curr_events_stack

let pop_function_call analysis =
  let top = Callstack.top_call analysis.curr_stack in
  match analysis.curr_stack.stack with
  | [] ->
    assert (List.length analysis.curr_events_stack = 1);
    on_current_trace analysis (fun cur _ -> Trace.add_prefix top cur);
  | _ :: _ ->
    match analysis.curr_events_stack with
    | [] | [_] -> Mt_options.fatal "Invalid analysis stack when popping calling"
    | trace_callee :: trace_caller :: q ->
      let trace_callee' = Trace.add_prefix top trace_callee in
      let new_trace = Trace.union trace_caller trace_callee' in
      analysis.curr_events_stack <- new_trace :: q


module OrderedThreads = struct

  let family_tree analysis =
    let th_tbl = analysis.all_threads in
    (* The inheritance table has at most as many entries as the general
       thread table *)
    let tree = Thread.Hashtbl.(create (length th_tbl)) in
    Thread.Hashtbl.iter_sorted
      (fun th state ->
         match state.th_parent with
         | None -> () (* This is the main thread *)
         | Some parent ->
           let children =
             try Thread.Hashtbl.find tree parent.th_eva_thread
             with Not_found -> []
           in
           Thread.Hashtbl.replace tree parent.th_eva_thread (th :: children)
      ) th_tbl;
    tree
  ;;

  let creation_map analysis =
    let tree = family_tree analysis in
    (* Not really optimized, but we don't really care here. Mostly,
       threads are created by one single thread, the main one *)
    let rec all_children acc th =
      let immediate_children = try Thread.Hashtbl.find tree th with Not_found -> []
      and do_child acc th' =
        let acc' = Thread.Set.add th' acc in
        all_children acc' th'
      in
      List.fold_left do_child acc immediate_children
    in
    fold_threads analysis Thread.Map.empty
      (fun th map ->
         let children = all_children Thread.Set.empty th.th_eva_thread in
         Thread.Map.add th.th_eva_thread children map
      )

  (* Iter a function f over program threads following the an order compatible
     with the partial order induced by thread creation *)
  let ordered_iter analysis =
    let tree = family_tree analysis in
    fun f initial ->
      let rec do_thread value th =
        let v = f th value in
        try
          let children = Thread.Hashtbl.find tree th in
          List.iter (do_thread v) children;
        with Not_found -> ()

      in
      do_thread initial Thread.main
  ;;

  let ordered_fold f acc analysis =
    let tree = family_tree analysis in
    let rec do_thread_id_list acc thlist =
      match thlist with
      | [] -> acc
      | _ :: _ ->
        let new_acc, next_level =
          List.fold_left
            (fun (glob_acc, next_acc) th ->
               let children =
                 try Thread.Hashtbl.find tree th
                 with Not_found -> [] in
               (f glob_acc th, children @ next_acc)
            ) (acc, []) thlist in
        do_thread_id_list new_acc next_level
    in do_thread_id_list acc [Thread.main]
  ;;
end


let should_compute_thread th =
  (Thread.is_main th.th_eva_thread) ||
  (let name = ThreadState.label th in
   (not (Datatype.String.Set.mem name (Mt_options.SkipThreads.get ()))) &&
   let only = Mt_options.OnlyThreads.get () in
   Datatype.String.Set.is_empty only || Datatype.String.Set.mem name only
  )
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct