package frama-c

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

Source file mt_analysis_fixpoint.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
(**************************************************************************)
(*                                                                        *)
(*  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 Mt_types
open Mt_shared_vars_types
open Mt_mutexes_types
open Mt_thread


(* If the thread sends more messages than before, we flag all the threads
   receiving messages on those queues as needed to be recomputed *)
let mark_new_messages_received analysis =
  let th = analysis.curr_thread in
  let is_send = function SendMsg _ -> true | _ -> false in
  let send_before = Trace.find_events is_send th.th_amap
  and send_after = Trace.find_events is_send (curr_events analysis) in
  (* YYY Not monotonic *)
  let diff = EventsSet.diff send_after send_before in
  if not (EventsSet.is_empty diff) then
    let queues = EventsSet.fold
        (fun evt queues -> match evt with
           | SendMsg (q, _) -> Mqueue.Set.add q queues
           | _ -> queues) diff Mqueue.Set.empty
    in
    Mt_options.debug "@[New message(s) sent@ on@ queue(s) %a@]"
      (Pretty_utils.pp_iter Mqueue.Set.iter Mqueue.pretty) queues;
    iter_threads analysis
      (fun th ->
         let should_recompute _stack = function
           | ReceiveMsg (q, _, _) -> Mqueue.Set.mem q queues
           | _ -> false
         in
         if Trace.exists th.th_amap should_recompute
         then (Mt_options.debug "Marking %a as having received new message(s)"
                 ThreadState.pretty th;
               ThreadState.recompute_because th NewMsgReceived)
      );
;;

let record_end_of_thread_analysis analysis =
  let th = analysis.curr_thread in

  (* We save the state of the analysis *)
  Mt_options.feedback ~level:2
    "* Starting to save the state of the value analysis";

  let results = Eva_results.get_results () in
  th.th_value_results <- Some results;

  if Mt_options.ToDisk.get () then
    let th = ThreadState.label th |> Mt_lib.sanitize_filename in
    let name = Format.sprintf "%s%s_iteration_%d.sav"
        (Mt_options.ToDiskPrefix.get ())
        th analysis.iteration in
    Project.save (Filepath.of_string name)
  else begin
    let p = lazy(
      let pname = Format.asprintf "%a, iteration %d"
          ThreadState.pretty th analysis.iteration
      in
      Project.create_by_copy ~last:false pname)
    in
    match Mt_options.KeepProjects.get () with
    | "all" ->
      th.th_projects <- Lazy.force p :: th.th_projects
    | "last" ->
      List.iter (fun project -> Project.remove ~project ()) th.th_projects;
      th.th_projects <- [Lazy.force p]
    | "none" -> ()
    | _ -> assert false (* checked by the command-line *)
  end;
  Mt_options.feedback ~level:2 "* state saved";

  mark_new_messages_received analysis;

  (* We compute the globals variables accessed by the thread *)
  Mt_options.feedback ~level:2 "* Computing shared variables";
  let state_accesser = Mt_memory.Types.Global in
  let read_written =
    Mt_shared_vars.read_written_by_thread
      (Mt_shared_vars.stmt_is_multithreaded analysis state_accesser)
      th.th_eva_thread
  in
  th.th_read_written <- read_written;
  Mt_options.result ~level:3 "@[<v 0>Globals accessed by thread:@ %a@]"
    AccessesByZone.pretty_map read_written;
  Mt_options.feedback ~level:2 "* shared variables computed";

  (* We compute interferences *)
  Mt_interferences.add_last_analysis analysis;

  (* We update the multithread events of the thread for its next iteration *)
  th.th_amap <- curr_events analysis;

  (* Compute the concurrent graph of this thread *)
  Mt_options.feedback ~level:2 "* Computing cfg";
  th.th_cfg <- Mt_cfg.make_cfg th;
  th.th_read_written_cfg <- Mt_cfg.cfg_accesses th.th_eva_thread th.th_cfg;
  Mt_options.feedback ~level:2 "* Cfg computed";
;;


(* We compute a value analysis for the given thread *)
let compute_thread analysis th =
  let time = Sys.time () in
  Project.clear
    ~selection:(State_selection.with_dependencies Messages.self) ();
  Messages.reset_once_flag ();

  Mt_options.feedback ~level:2 "* Computing value analysis for thread %a"
    Thread.pretty th.th_eva_thread;
  Mt_options.debug "@[<hov>Arguments@ %a@]"
    (Pretty_utils.pp_list Cvalue.V.pretty) th.th_params;
  Mt_options.debug ~level:2 "Initial state %a"
    Cvalue.Model.pretty th.th_init_state;

  (* We set the values that depend on the thread analysed *)
  analysis.curr_thread <- th;
  analysis.curr_events_stack <- [];
  Datatype.Int.Hashtbl.clear analysis.memexec_cache;

  (* We reset the concurrent value analysis (necessary because sometimes,
     only the hooks have changed, and this is not captured by the project
     infrastructure) *)
  Mt_lib.clear_value_results ();

  (* We set the parameters for the value analysis *)
  Globals.set_entry_point (Kernel_function.get_name th.th_fun) false;
  Eva_results.set_initial_state th.th_init_state;
  Eva_results.set_main_args th.th_params;
  Thread.set_current th.th_eva_thread;

  Analysis.compute ();

  if Mt_options.ShowTime.get () then
    Mt_options.feedback ~level:2
      "* Value analysis computed for thread %a, %f sec"
      ThreadState.pretty th (Sys.time () -. time);
;;

let recompute_shared_vars_changed analysis before =
  iter_threads analysis
    (fun th ->
       try AccessesByZone.fold
             (fun z _ () ->
                if not (Locations.Zone.is_included z before) then raise Exit)
             th.th_read_written ()
       with Exit -> ThreadState.recompute_because th PotentialSharedVarsChanged
    )
;;

(** Recompute all the threads that are not [th], and that read a value
    that has changed between [before] and [now] *)
let recompute_shared_vars_values_changed analysis th before now =
  let changed_zone b offsm z =
    (* b is present in [now] but not in [before], or has changed: add the
       entire base to the changed_zone *)
    let default () =
      let zb = Locations.Zone.inject b Int_Intervals.top in
      Locations.Zone.join z zb
    in
    try
      match Cvalue.Model.find_base b before with
      | `Top | `Bottom -> assert false
      | `Value offsm' ->
        if Cvalue.V_Offsetmap.equal offsm offsm' then z
        else default ()
    with Not_found -> default ()
  in
  match now with
  | Cvalue.Model.Top | Cvalue.Model.Bottom -> assert false
  | Cvalue.Model.Map now ->
    (* Over-approximation of the zones changed from [before] to [now] *)
    let z_changed =
      Cvalue.Model.fold changed_zone now Locations.Zone.bottom
    in
    iter_threads analysis
      (fun th' ->
         if not (ThreadState.equal th' th) then
           try
             AccessesByZone.fold
               (fun z accesses () ->
                  if Locations.Zone.intersects z_changed z &&
                     (* YYY: recompute also threads that only write the variable?*)
                     (SetStmtIdAccess.exists
                        (fun (op, _, _) -> RW.is_read op)
                        accesses)
                  then begin
                    ThreadState.recompute_because th' SharedVarsValuesChanged;
                    raise Exit (* Speed up things, th' will be recomputed *)
                  end)
               th'.th_read_written ()
           with Exit -> ()
      )
;;


let compute_shared_vars analysis =
  let _imprecise =
    Mt_options.feedback "***** Computing shared variables";
    let (ww_accesses, rw_accesses), _ =
      Mt_shared_vars.Global.concurrent_accesses_all_threads
        (threads analysis) in
    let accesses = ww_accesses @ rw_accesses in
    Mt_options.debug ~level:2 "Global concurrent var accesses:@.%a"
      (Mt_shared_vars.Global.pretty_concurrent_accesses ()) accesses;
    let all_zones = Mt_shared_vars.Global.all_zones_accessed accesses in
    Mt_options.result ~level:3 "@[<hov 2>Imprecise locations to watch: %a@]"
      Locations.Zone.pretty all_zones;

    (* Detect changes *)
    if not (Locations.Zone.equal all_zones analysis.concurrent_accesses)
    then (
      let before = analysis.concurrent_accesses in
      Mt_options.feedback ~level:2 "@[<v>Concurrent imprecise accesses have \
                                    changed: before@ @[<hov 2>  %a@]@ vs.@ @[<hov 2>  %a@]"
        Locations.Zone.pretty before Locations.Zone.pretty all_zones;
      let after = Locations.Zone.join before all_zones in
      analysis.concurrent_accesses <- after;
      recompute_shared_vars_changed analysis before;
    )
  in

  (* Precise computation. Very similar to the above code, we just compute,
     store and print things differently *)
  let precise =
    let (ww_accesses, rw_accesses), zmap =
      Mt_shared_vars.Precise.concurrent_accesses_all_threads
        (threads analysis) in
    if Mt_options.DumpSharedVarsValues.get () > 0 then
      Mt_shared_vars.Precise.display_shared_vars_value zmap;
    let written = Mt_shared_vars.Precise.enumerate_written_vars_value zmap in
    let all_accesses = ww_accesses @ rw_accesses in
    let header fmt = Format.fprintf fmt "Possible read/write data races:" in
    Mt_options.printf ~level:1 ~header "  @[<v 0>%a@]"
      Mt_mutexes.pretty_with_mutexes rw_accesses;
    if Mt_options.WriteWriteRaces.get () then begin
      let header fmt = Format.fprintf fmt "Possible write/write data races:" in
      Mt_options.printf ~level:1 ~header "  @[<v 0>%a@]"
        Mt_mutexes.pretty_with_mutexes ww_accesses;
    end;
    let all_zones = Mt_shared_vars.Precise.all_zones_accessed (ww_accesses @ rw_accesses) in
    Mt_options.result ~level:2 "@[<hov 2>Shared memory:@ %a@]"
      Locations.Zone.pretty all_zones;

    (* Detect changes *)
    if not (Locations.Zone.equal all_zones analysis.precise_concurrent_accesses)
    then (
      let before = analysis.precise_concurrent_accesses in
      Mt_options.feedback ~level:2
        "@[<v>Concurrent precise var accesses have changed: before@ \
         @[<hov 2>  %a@]@ \
         vs.@ \
         @[<hov 2>  %a@]@]"
        Locations.Zone.pretty before Locations.Zone.pretty all_zones;
      (* let after = Locations.Zone.join before all_zones in *)
      analysis.precise_concurrent_accesses <- all_zones;
      (* No need to recompute for the moment, this field is not used by
         the analysis *)
    );
    all_accesses, written
  in
  precise
;;

(* Update the th_values_written field of all the threads, using the
   list of concurrent accesses that is returned by the shared var analysis.

   This function must be called once the [th_read_written] fields have been
   updated to ensure correct convergence *)
let store_written_value analysis lw =
  let aux th =
    let l = List.filter (fun (id, _, _) -> Thread.equal id th.th_eva_thread) lw in
    let old_written = th.th_values_written in
    let written = Mt_shared_vars.Precise.join_shared_values l in
    (* XXX: temporary *)
    let priority, hint =
      Widen_type.hints_from_keys Cil.dummyStmt (Widen_type.default ())
    in
    let written = Cvalue.Model.widen ~priority ~hint old_written written in
    let changed = not (Cvalue.Model.equal written old_written) in
    if changed then
      recompute_shared_vars_values_changed analysis th old_written written;
    if Mt_options.DumpSharedVarsValues.get () > 0 &&
       not (Cvalue.Model.equal Cvalue.Model.empty_map written)
    then
      Mt_options.result "@[Write summary for %a%t:@ %a@]"
        ThreadState.pretty th
        (fun fmt -> if changed then Format.fprintf fmt " (updated)")
        Cvalue.Model.pretty written;
    th.th_values_written <- written
  in
  iter_threads analysis aux


(* Function that does one pass of value analysis on all the threads
   that are marked as needed to be recomputed. Returns the values
   written by each thread recomputed*)
let one_iteration analysis =
  iter_threads analysis
    (fun th ->
       if not (SetRecomputeReason.is_empty th.th_to_recompute) then (
         if Mt_thread.should_compute_thread th then
           if Cvalue.Model.is_reachable th.th_init_state then (
             Mt_options.feedback
               "@[<hov 2>*** Computing thread %a,@ iteration %d@ (%a)@]"
               ThreadState.pretty th analysis.iteration
               (Pretty_utils.pp_iter ~sep:",@ "
                  SetRecomputeReason.iter RecomputeReason.pretty)
               th.th_to_recompute;

             compute_thread analysis th;

             (* We save all our results *)
             record_end_of_thread_analysis analysis;
             Mt_options.feedback "*** Thread %a computed" ThreadState.pretty th;
           ) else (
             Mt_options.feedback "@[<hov 2>*** Thread %a has been@ created but@ \
                                  not started. Skipping.@]"  ThreadState.pretty th
           )
         else (
           Mt_options.feedback "*** Skipping thread %a as requested"
             ThreadState.pretty th;
         );
         th.th_to_recompute <- SetRecomputeReason.empty;
       ) else
         Mt_options.debug "No need to recompute thread %a" ThreadState.pretty th
    );
  Mt_options.feedback "***** Threads computed for iteration %d."
    analysis.iteration;

  (* We update the locked mutexes and started threads information of the
     cfg. This must obviously be done before shared variables are computed,
     but it supposes the thread creation structure is completely known.
     Hence, it is safer to do this at the end of a full iteration, instead
     of at the end of a thread *)
  Mt_options.feedback ~level:2 "* Computing live threads and locked mutexes";
  iter_threads analysis (Mt_cfg.update_cfg_contexts analysis);
  Mt_options.feedback ~level:2 "* threads and mutexes computed";

  let precise_accesses, written = compute_shared_vars analysis in
  analysis.concurrent_accesses_by_nodes <- precise_accesses;
  store_written_value analysis written;

  let mutexes = Mt_mutexes.mutexes_protecting_zones' precise_accesses in
  Mt_options.result "@[<v 0>Mutexes for concurrent accesses:@ %a@]"
    MutexesByZone.pretty mutexes;
  if Mt_options.CheckProtections.get () then begin
    let protections = Mt_mutexes.check_protection analysis precise_accesses in
    Mt_options.result "Detailed shared zones protections@.%a"
      Mt_mutexes.pretty_protections protections;
    let ill_protected = Mt_mutexes.ill_protected precise_accesses protections in
    let need_sync = Mt_mutexes.need_sync ill_protected in
    if need_sync <> [] then begin
      let pp fmt (stmt, z) =
        Format.fprintf fmt "@[%a (for %a)@]"
          Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc stmt)
          Locations.Zone.pretty z
      in
      Mt_options.result "Statements needing manual synchronisation@.%a"
        (Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@ " ~suf:"@]" pp) need_sync
    end;
  end;
  Mt_options.feedback "***** Shared variables computed";

  fold_threads analysis false
    (fun th v -> v || not (SetRecomputeReason.is_empty th.th_to_recompute))
;;


(* Remove "white" nodes in the cfg, ie accesses to variables that
   are not concurrent at all. Done at the very end of the analysis
   because
   - those nodes are needed before to reach the fixpoint
   - the marking of nodes by colors is not used by the analysis
     YYY: this can endanger restarting the analysis from the last point
     (the fixpoint may not be reached immediately, or we might reach a wrong
     one concerning shared variables). This should probably be done in
     a copy of the cfgs, but this means rewriting a fair amount of other
     analysis structures too *)
let mark_shared_nodes_kind analysis =
  let precise_accesses = analysis.concurrent_accesses_by_nodes in
  let shared_vars = Mt_shared_vars.Precise.all_zones_accessed precise_accesses in
  (* Update the informations in the cfgs *)
  iter_threads analysis
    (fun th -> Mt_shared_vars.Precise.remove_non_concur_zones_from_cfg
        shared_vars th.th_cfg
    );
  Mt_shared_vars.Precise.mark_concur_access_in_cfg precise_accesses;
  if (not (Mt_options.KeepWhiteNodes.get ()) ||
      not (Mt_options.KeepGreenNodes.get ()))
  && not (Mt_options.FullCfg.get ())
  then
    iter_threads analysis
      (fun th ->
         let keep =
           match Mt_options.KeepWhiteNodes.get (),
                 Mt_options.KeepGreenNodes.get () with
           | false, false -> Mt_cfg_types.ConcurrentAccess
           | false, true  -> Mt_cfg_types.SharedVarNonConcurrentAccess
           | true,  true  -> Mt_cfg_types.NotReallySharedVar
           | true,  false ->
             Mt_options.warning ~once:true
               "Incoherent@ combination@ of@ options@ %s@ \
                and@ %s.@ Only@ non-shared@ variables@ will@ be@ removed."
               Mt_options.KeepWhiteNodes.option_name
               Mt_options.KeepGreenNodes.option_name;
             Mt_cfg_types.SharedVarNonConcurrentAccess
         in
         let cfg = Mt_cfg.remove_superfluous_nodes ~keep th.th_cfg in
         th.th_cfg <- cfg;
      );
;;


(* Auxiliary function iterating the analysis until the fixpoint is reached *)
let reach_fixpoint analysis =
  Mt_options.feedback "******* Starting to iterate";
  let rec aux i =
    Mt_options.feedback "***** Iteration %d" i;
    analysis.iteration <- i;
    let continue = one_iteration analysis in
    if continue && i < Mt_options.StopAfter.get () then aux (i+1)
    else (* Stop iteration *)
    if continue then
      Mt_options.feedback
        "@[<v 0>\
         @[<hov 2>******* Analysis stopped after@ \
         %d iterations.@ Remaining@ to@ do:@]@ \
         %a@]" i
        (fun fmt () -> iter_threads analysis
            (fun th -> if not (SetRecomputeReason.is_empty th.th_to_recompute) then
                Format.fprintf fmt "@[<hov 2>Thread %a:@ %a@]@ "
                  ThreadState.pretty_detailed th
                  (Pretty_utils.pp_iter ~sep:",@ " ~pre:"" ~suf:""
                     SetRecomputeReason.iter RecomputeReason.pretty)
                  th.th_to_recompute
            )
        ) ()
    else
      Mt_options.feedback "******* Analysis performed, %d iterations" i
  in
  aux 1
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