Source file mt_shared_vars.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
open Cil_types
open Cil_datatype
open Visitor
open Locations
open Mt_cil
open Mt_memory.Types
open Mt_types
open Mt_shared_vars_types
open Mt_cfg_types
open Mt_thread
let () = Ast_attributes.register ~ignore:true (AttrName false) "FRAMA_C_MODEL"
let is_model_base b =
try
let vi = Base.to_varinfo b in
Ast_attributes.contains "FRAMA_C_MODEL" vi.vattr
with Base.Not_a_C_variable -> false
let keep_base b =
not (Base.is_any_formal_or_local b ||
Mt_memory.is_frama_c_base b ||
is_model_base b ||
(Mt_options.IgnoreNull.get () && Base.(equal b null))
)
let remove_uninteresting_variables_zone z =
Zone.filter_base keep_base z
let remove_uninteresting_variables_loc loc =
Locations.filter_base keep_base loc
let error_io_whole_memory op =
let source = fst (RW.loc op) in
Mt_options.error ~source ~once:true
"@[%a of the whole memory.@ Ignoring to allow Mthread to continue, \
but the analysis will not be correct.@]"
RW.pretty op
let filter_inout_memory =
let is_mthread_shared base =
try
let vi = Base.to_varinfo base in
String.equal vi.vorig_name "__fc_mthread_shared"
with Base.Not_a_C_variable ->
false
in
let filter_base base =
Base.is_global base && not (is_mthread_shared base)
in
Inout_memory.mk_filter ~filter_base
let read_written_by_thread ?(watch_only=Locations.Zone.top) sm th =
let open Current_loc.Operators in
let add stmt op zone acc =
if Locations.Zone.is_bottom zone then
acc
else if Locations.Zone.is_top zone then
let () = error_io_whole_memory op in
acc
else
let zone = remove_uninteresting_variables_zone zone in
let zone = Locations.Zone.narrow zone watch_only in
let state = AccessesByZone.Map acc in
let v = SetStmtIdAccess.inject_singleton (op, stmt, th) in
match AccessesByZone.add_binding state ~exact:false zone v with
| AccessesByZone.Bottom -> assert false
| AccessesByZone.Top -> assert false
| AccessesByZone.Map m -> m
in
Inout_memory.fold
~filter:filter_inout_memory
(fun aloc memory acc ->
match aloc with
| Global _ ->
acc
| Local (stmt, _) ->
let<> UpdatedCurrentLoc = Stmt.loc stmt in
if sm stmt then
acc
|> add stmt (ReadAloc aloc) memory.read
|> add stmt (WriteAloc aloc) memory.written
else
acc)
AccessesByZone.empty_map
(** In global mode, we do a rough analysis using the synthetic results of
Value. In local mode, we supply precise states for each statement of the
function. *)
type mode = VLocal | VGlobal
type collect_params = {
stmt_multithread: stmt -> bool;
thread: thread;
mode: mode;
iter_requests: stmt -> (Results.request -> unit) -> unit;
watch_only: Locations.Zone.t;
}
class do_it cp =
object(self)
inherit Visitor.frama_c_inplace as super
val mutable result = AccessesByZone.empty_map
method accesses = result
val visited = Cil_datatype.Kf.Hashtbl.create 17
method private mark_visited kf =
Cil_datatype.Kf.Hashtbl.add visited kf ()
method private already_visited kf =
try Cil_datatype.Kf.Hashtbl.find visited kf; true
with Not_found -> false
method private add_access op z =
if not (Locations.Zone.equal Locations.Zone.top z) then (
let stmt = self#cur_stmt in
if cp.stmt_multithread stmt then
let interesting = remove_uninteresting_variables_zone z in
let concurrent = Locations.Zone.narrow interesting cp.watch_only in
let state = AccessesByZone.Map result in
let v =
SetStmtIdAccess.inject_singleton (op, stmt, cp.thread)
in
match AccessesByZone.add_binding state ~exact:false concurrent v with
| AccessesByZone.Bottom -> assert false
| AccessesByZone.Top -> assert false
| AccessesByZone.Map m -> result <- m
) else
Mt_options.error ~current:true ~once:true
"@[%a@ of@ the@ whole@ memory.@ Ignoring@ to@ allow@ Mthread@ to@ \
continue,@ but@ the@ analysis@ will@ not@ be@ correct.@]"
RW.pretty op
method private cur_stmt =
match super#current_stmt with
| None -> Mt_options.abort "visiting without current statement"
| Some s -> s
method! vstmt_aux s =
if cp.stmt_multithread s then
match s.skind with
| UnspecifiedSequence seq ->
List.iter
(fun (stmt,_,_,_,_) ->
ignore(visitFramacStmt (self:>frama_c_visitor) stmt)) seq;
Cil.SkipChildren
| _ -> super#vstmt_aux s
else
Cil.DoChildren
method! vlval lv =
cp.iter_requests self#cur_stmt
(fun req -> self#add_access Read Results.(lval_deps lv req));
Cil.SkipChildren
method private do_assign lv =
cp.iter_requests self#cur_stmt
(fun request ->
let deps = Results.(address_deps lv request) in
self#add_access Read deps;
let loc = Results.(eval_address lv request |> as_location) in
if Location_Bits.(equal loc.loc top) then
Mt_options.warning ~current:true ~once:true
"Problem with %a: its writing location is completely unknown."
Printer.pp_lval lv;
let loc = remove_uninteresting_variables_loc loc in
let loc = Locations.(valid_part Write loc) in
let bits_loc = Locations.(enumerate_valid_bits Write loc) in
self#add_access (Write loc) bits_loc)
method private do_init v i =
let rec aux lv = function
| SingleInit e ->
self#do_assign lv;
ignore (visitFramacExpr (self:>frama_c_visitor) e)
| CompoundInit(ct,initl) ->
let doinit o i _ () = aux (Cil.addOffsetLval o lv) i in
Cil.foldLeftCompound ~implicit:true ~doinit ~ct ~initl ~acc:()
in
aux (Cil.var v) i
method private do_call exp =
cp.iter_requests self#cur_stmt (fun request ->
let deps = match exp.enode with
| Lval lv -> Results.address_deps lv request
| _ -> assert false
in
self#add_access Read deps;
if cp.mode = VGlobal then
let callees = Results.(eval_callee exp request |> default []) in
List.iter self#rw_fun callees
)
method! vinst i =
let visit_expr e = ignore (visitFramacExpr (self:>frama_c_visitor) e) in
if not (Results.is_reachable self#cur_stmt) then
Cil.SkipChildren
else
match i with
| Set (lv,exp,_) -> self#do_assign lv; visit_expr exp; Cil.SkipChildren
| Local_init(v, AssignInit i, _) -> self#do_init v i; Cil.SkipChildren
| Local_init(v, ConsInit (f, args, _), _) ->
self#do_assign (Cil.var v);
self#do_call (Cil.evar f);
List.iter visit_expr args;
Cil.SkipChildren
| Call (lv_opt,exp,args,_) ->
Option.iter self#do_assign lv_opt;
self#do_call exp;
List.iter visit_expr args;
Cil.SkipChildren
| _ -> Cil.DoChildren
method! vexpr exp =
match exp.enode with
| AddrOf lv | StartOf lv ->
cp.iter_requests self#cur_stmt
(fun request ->
let deps = Results.address_deps lv request in
self#add_access Read deps;
);
Cil.SkipChildren
| _ -> Cil.DoChildren
method rw_stmt stmt =
ignore (visitFramacStmt (self :> frama_c_visitor) stmt)
method private assigns_not_mthread = function
| WritesAny -> WritesAny
| Writes l ->
let aux (t, _) = match t.it_content.term_node with
| TLval (TVar { lv_name = name}, _) ->
name <> "__fc_mthread_shared"
| _ -> true
in
Writes (List.filter aux l)
method private compute_for_funspec kf =
let aux request =
let state = Results.get_cvalue_model request in
let behaviors = Logic_inout.valid_behaviors kf state in
let assigns = Ast_info.merge_assigns behaviors in
let assigns = self#assigns_not_mthread assigns in
(match assigns with
| WritesAny ->
let top = Locations.make_loc Location_Bits.top Int_Base.top in
self#add_access (Write top) Zone.top;
| Writes assigns' ->
let aux l =
try
let loc = Eva_results.eval_tlval_as_location state l in
let loc = remove_uninteresting_variables_loc loc in
let loc = Locations.(valid_part Write loc) in
let z = Locations.(enumerate_valid_bits Write loc) in
self#add_access (Write loc) z
with Logic_to_c.No_conversion ->
Mt_options.warning ~once:true
"unsupported@ assigns@ clause@ for@ function %a;@ Ignoring it."
Kernel_function.pretty kf;
in
List.iter
(fun ({it_content = loc}, _) ->
if not (Logic_utils.is_result loc) then aux loc
) assigns'
);
let read = Logic_inout.assigns_inputs_to_zone state assigns in
self#add_access Read read
in
match cp.mode with
| VGlobal ->
let requests =
Results.(at_start_of kf |> by_callstack |> List.map snd)
in
List.iter aux requests
| VLocal ->
cp.iter_requests self#cur_stmt aux
method rw_fun kf =
if not (self#already_visited kf) then (
self#mark_visited kf;
match Analysis.use_spec_instead_of_definition kf, kf.fundec with
| false, Definition (f,_) ->
ignore (visitFramacFunction (self:>frama_c_visitor) f)
| true, _ | _, Declaration _ -> self#compute_for_funspec kf
)
end
let aux_visitor sm th sa watch_only =
let cp = {
stmt_multithread = sm;
thread = th;
mode = (match sa with Global -> VGlobal | Local _ -> VLocal);
iter_requests = iter_requests sa;
watch_only = watch_only;
} in
new do_it cp
let read_written_by_function sm th sa ?(watch_only=Locations.Zone.top) kf ki =
let comp = aux_visitor sm th sa watch_only in
(match ki with
| Kglobal -> ()
| Kstmt s -> comp#push_stmt s
);
comp#rw_fun kf;
comp#accesses;
;;
let var_thread_created =
Mt_cil.mthread_global_var "__fc_mthread_threads_running"
exception Stmt_is_multithreaded
let stmt_is_multithreaded analysis sa =
let iter_requests = iter_requests sa in
let th = analysis.curr_thread in
if Thread.is_main th.th_eva_thread then
let v = var_thread_created () in
(fun stmt ->
try
iter_requests stmt (fun request ->
let value = Results.(eval_var v request |> as_cvalue) in
match Mt_memory.extract_int value with
| `Success 0 -> ()
| _ -> raise Stmt_is_multithreaded
);
false
with Stmt_is_multithreaded -> true
)
else (fun _ -> true)
module type Computer =
sig
module Access : Datatype.S
module Set: Lattice_type.Lattice_Set with type O.elt = Access.t
module ZoneMap: Lmap_bitwise.Location_map_bitwise with type v = Set.t
type list_accesses = (Locations.Zone.t * Set.t) list
val pretty_concurrent_accesses :
?f:Access.t Pretty_utils.formatter ->
unit -> Format.formatter -> list_accesses -> unit
val all_zones_accessed : list_accesses -> Locations.Zone.t
val concurrent_accesses_all_threads :
Mt_thread.ThreadState.t list ->
(list_accesses * list_accesses) * ZoneMap.map
end
module Aux(X:
sig
type info
module Access: Datatype.S with type t = rw * info * Thread.t
module Set: sig
include Lattice_type.Lattice_Set with type O.elt = Access.t
val pretty_aux: Access.t Pretty_utils.formatter -> t Pretty_utils.formatter
end
module ZoneMap: Lmap_bitwise.Location_map_bitwise with type v = Set.t
val thread_data: thread_state -> ZoneMap.map
val running_concurrently: thp:thread_state -> ths:thread_state -> infop:info -> bool
end) =
struct
include X
open Abstract_interp
let fold_location f m acc =
let module H = Datatype.Integer.Hashtbl in
let aux b itvs v acc =
try
let l = Int_Intervals.project_set itvs in
let by_size = H.create 4 in
let aux_itv (ib, ie) =
let loc = Location_Bits.inject b (Ival.inject_singleton ib) in
let size = Int.succ (Int.sub ie ib) in
try
let prev = H.find by_size size in
let loc = Location_Bits.join prev loc in
H.replace by_size size loc
with Not_found -> H.add by_size size loc
in
List.iter aux_itv l;
H.fold
(fun size loc acc ->
let loc = Locations.make_loc loc (Int_Base.inject size) in
f loc v acc
) by_size acc
with Abstract_interp.Error_Top ->
let locb = Location_Bits.inject b Ival.zero in
let size = Int_Base.top in
let loc = Locations.make_loc locb size in
f loc v acc
in
X.ZoneMap.fold_base
(fun base -> X.ZoneMap.LOffset.fold_fuse_same (aux base)) m acc
let consider_vars_accesses th1 th2 =
match ThreadState.one_creates_other th1 th2 with
| `Unrelated ->
(fun _ _ -> true)
| `Creates (thp, ths) ->
let before info = X.running_concurrently ~thp ~ths ~infop:info in
if ThreadState.equal thp th1 then
(fun (_, info, _ : X.Access.t) _ -> before info)
else
(fun _ (_, info, _ : X.Access.t) -> before info)
;;
let concurrent_accesses_sets consider s1 s2 =
X.Set.fold
(fun o1 acc -> X.Set.fold
(fun o2 s ->
Mt_options.debug ~level:2
"@[<hov>Possible concurrent accesss@ %a@ and %a@]"
X.Access.pretty o1 X.Access.pretty o2;
let is_concurrent = consider o1 o2 in
if is_concurrent then (
Mt_options.debug ~level:2 "@[Above access is concurrent@]";
X.Set.join s
(X.Set.join (X.Set.inject_singleton o1)
(X.Set.inject_singleton o2))
) else (
Mt_options.debug ~level:2 "@[Above access is not concurrent@]";
s)
) s2 acc
) s1 X.Set.bottom
;;
let concurrent_accesses_two_threads th1 th2 =
Mt_options.debug ~level:2 "Concurrent accessses in threads %a and %a"
ThreadState.pretty th1 ThreadState.pretty th2;
let consider = consider_vars_accesses th1 th2 in
let cache =
Hptmap_sig.TemporaryCache "Mt_shared_vars.concurrent_accesses_two_threads"
in
let empty_neutral = false in
let idempotent = false in
let symmetric = false in
let decide_fast _ _ = X.ZoneMap.LOffset.Recurse in
let map2 = X.ZoneMap.map2
~cache ~symmetric ~idempotent ~empty_neutral decide_fast in
map2
(fun s1 s2 -> concurrent_accesses_sets consider s1 s2)
(X.thread_data th1) (X.thread_data th2)
;;
let basic_merge_events =
let cache = Hptmap_sig.PersistentCache "Mt_shared_vars.basic_merge_events" in
let empty_neutral = true in
let idempotent = true in
let symmetric = true in
let decide_fast _ _ = X.ZoneMap.LOffset.Recurse in
X.ZoneMap.map2
~cache ~symmetric ~idempotent ~empty_neutral decide_fast X.Set.join
type list_accesses =
(Locations.Zone.t * X.Set.t) list
let concurrent_accesses_all_threads all_threads :
(list_accesses * list_accesses) * _ =
let rec aux acc = function
| [] -> acc
| th :: thq ->
let rec aux' acc = function
| [] -> acc
| th' :: thq' ->
let m = concurrent_accesses_two_threads th th' in
aux' (basic_merge_events m acc) thq'
in
aux (aux' acc thq) thq
in
let all = aux X.ZoneMap.empty_map all_threads in
X.ZoneMap.fold_fuse_same
(fun z s ((write_write_races, read_write_races) as acc) ->
let read_access, write_access = X.Set.fold
(fun (op, _, _) (read, write) ->
match op with
| Read -> (true, write)
| Write _ -> (read, true)
| ReadAloc _ -> (true, write)
| WriteAloc _ -> (read, true)
) s (false, false)
in match read_access, write_access with
| false, false -> acc
| true, false -> acc
| false, true ->
if Mt_options.WriteWriteRaces.get ()
then (z, s) :: write_write_races, read_write_races
else acc
| true, true ->
write_write_races, (z, s) :: read_write_races
) all ([], []),
all
let pretty_concurrent_accesses ?(f=(fun _fmt _ -> ())) () fmt
(l:list_accesses) =
if l = [] then Format.fprintf fmt "none"
else
Format.fprintf fmt "@[<v 1>%a@]"
(Pretty_utils.pp_list ~sep:"@ "
(fun fmt (z, s) -> Format.fprintf fmt "@[<v 0>%a:@ @[<hov>%a@]@]"
Locations.Zone.pretty z (X.Set.pretty_aux f) s
))
l
let all_zones_accessed (l: list_accesses) =
let aux acc (z, _) = Locations.Zone.join z acc in
List.fold_left aux Locations.Zone.bottom l
end
module Global = Aux(
struct
type info = stmt
let thread_data th = th.th_read_written
module Access = StmtIdAccess
module Set = SetStmtIdAccess
module ZoneMap = AccessesByZone
let running_concurrently ~thp:_ ~ths:_ ~infop:_ = true
end)
module Precise = struct
include Aux(
struct
type info = node
let thread_data th = th.th_read_written_cfg
module Access = NodeIdAccess
module Set = SetNodeIdAccess
module ZoneMap = AccessesByZoneNode
let running_concurrently ~thp:_ ~ths ~infop =
let context = infop.cfgn_context in
match ThreadPresence.find context.started_threads ths.th_eva_thread with
| NotPresent -> false
| MaybePresent | Present -> true
end)
let default_offsetmap validity =
let size = Cvalue.V_Offsetmap.size_from_validity validity in
let size = Lattice_bounds.Bottom.non_bottom size in
Cvalue.V_Offsetmap.create_isotropic ~size Cvalue.V_Or_Uninitialized.bottom
let node op loc state =
match loc.size with
| Int_Base.Top ->
Mt_options.warning ?source:(CfgNode.node_first_loc node)
"Ignoring imprecise %a at %a"
Mt_types.RW.pretty op Locations.pretty loc;
[]
| Int_Base.Value size ->
Location_Bits.fold_topset_ok
(fun base offs acc ->
let validity = Base.validity base in
if Base.Validity.equal Base.Invalid validity then
acc
else
let default = default_offsetmap validity in
let v = Cvalue.Model.find ~conflate_bottom:false state loc in
let r = Cvalue.V_Offsetmap.update
~validity:(Base.validity base)
~exact:true ~offsets:offs ~size
(Cvalue.V_Or_Uninitialized.C_init_noesc v)
default
in
match r with
| `Bottom -> acc
| `Value offsm -> (base, offsm)::acc
)
loc.loc
[]
let pp_stack fmt node =
Format.fprintf fmt "@ // %a" CfgNode.pretty_stmts node;
if Mt_options.DumpSharedVarsValues.get () > 1 then
Format.fprintf fmt "@ %a" Callstack.pretty node.cfgn_stack
let pp_access (op, node, th) base offsm =
if Mt_options.DumpSharedVarsValues.get () > 0 then
Mt_options.result ~once:true "@[%a %as @ @[%a%a@]@ %a@]"
Thread.pretty th Mt_types.RW.pretty op Base.pretty base
(Cvalue.V_Offsetmap.pretty_generic ?typ:(Base.typeof base) ()) offsm
pp_stack node
let display_shared_vars_value m =
fold_location
(fun loc s () ->
SetNodeIdAccess.fold
(fun (op, node, _thid as access) () ->
match op with
| ReadAloc _ | WriteAloc _ ->
Mt_options.not_yet_implemented ~current:true ~once:true
"MtSharedVars.Precise.display_shared_vars_value for ALoc"
| Write _ -> ()
| Read ->
let state = node.cfgn_value_state.state_before in
let shared = extract_shared_value node op loc state in
List.iter (fun (base, offsm) -> pp_access access base offsm) shared)
s
())
m
()
module WriteSeen =
Datatype.Triple_with_collections(CfgNode)(Thread)(Locations.Location)
let enumerate_written_vars_value m =
let aux _b _itvs s acc =
let aux_nodes (op, node, th as access) (seen, _wr as acc) =
match op with
| ReadAloc _ | WriteAloc _ ->
Mt_options.not_yet_implemented ~current:true ~once:true
"MtSharedVars.Precise.enumerate_written_vars_value for ALoc"
| Read -> acc
| Write loc ->
if not (WriteSeen.Set.mem (node, th, loc) seen) then
let state = node.cfgn_value_state.state_after in
let shared = extract_shared_value node op loc state in
List.fold_left (fun (seen,wr) (base, offsm) ->
pp_access access base offsm;
let seen = WriteSeen.Set.add (node, th, loc) seen in
(seen, (th, base, offsm) :: wr))
acc
shared
else acc
in
SetNodeIdAccess.fold aux_nodes s acc
in
let _seen, wr =
AccessesByZoneNode.fold_base
(fun base -> AccessesByZoneNode.LOffset.fold_fuse_same (aux base))
m (WriteSeen.Set.empty, [])
in
wr
let join_shared_values l =
let aux m (_id, base, offsm) =
try
let offsm' = Cvalue.Model.find_base base m in
match offsm' with
| `Top -> Mt_options.fatal "Top state"
| `Bottom -> m
| `Value offsm' ->
let join = Cvalue.V_Offsetmap.join offsm offsm' in
Cvalue.Model.add_base base join m
with Not_found ->
Cvalue.Model.add_base base offsm m
in
List.fold_left aux Cvalue.Model.empty_map l
let remove_non_concur_zones_from_cfg all_zones cfg =
let update_zones n =
let filtered = SetZoneAccess.filter
(fun (_, z) ->
not (Locations.Zone.equal Locations.Zone.bottom
(Locations.Zone.narrow all_zones z)))
n.cfgn_var_access.concur_accesses
in
let kind =
if SetZoneAccess.equal filtered SetZoneAccess.empty
then NotReallySharedVar
else SharedVarNonConcurrentAccess
in
n.cfgn_var_access <- { concur_accesses = filtered;
var_access_kind = kind }
in
CfgNode.iter ~f_before:update_zones cfg
;;
let mark_concur_access_in_cfg l =
let mark_useful (_z, s) =
SetNodeIdAccess.iter
(fun (_rw, n, _id) ->
n.cfgn_var_access <-
{ n.cfgn_var_access with var_access_kind = ConcurrentAccess }
) s
in
List.iter mark_useful l
end
let register_concurrent_var_accesses analysis states =
let kf = current_fun analysis in
let is_multithreaded = fun _ -> true in
let ki = calling_ki analysis in
let sa = match states with
| `Final h -> h
| `Leaf state ->
match ki with
| Kglobal -> assert false
| Kstmt s ->
let h = Stmt.Hashtbl.create 1 in
Stmt.Hashtbl.add h s state;
h
in
let accesses = read_written_by_function
is_multithreaded analysis.curr_thread.th_eva_thread (Local sa)
~watch_only:analysis.concurrent_accesses kf ki
in
AccessesByZone.fold
(fun z set () ->
SetStmtIdAccess.iter
(fun (rw, stmt, _id) ->
let top = Stack.access_to_var stmt in
Mt_thread.register_event analysis ~top (VarAccess (rw, z))
) set
) accesses ()