-
Notifications
You must be signed in to change notification settings - Fork 77
/
Copy pathbasePriv.ml
2152 lines (1896 loc) · 76 KB
/
basePriv.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
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
open Batteries
open GoblintCil
open Analyses
open GobConfig
open BaseUtil
module Q = Queries
module IdxDom = ValueDomain.IndexDomain
module VD = BaseDomain.VD
module CPA = BaseDomain.CPA
module BaseComponents = BaseDomain.BaseComponents
open CommonPriv
module type S =
sig
module D: Lattice.S
module G: Lattice.S
module V: Printable.S
val startstate: unit -> D.t
val read_global: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> varinfo -> VD.t
(* [invariant]: Check if we should avoid producing a side-effect, such as updates to
* the state when following conditional guards. *)
val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> varinfo -> VD.t -> BaseComponents (D).t
val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseComponents (D).t
val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
val threadenter: Q.ask -> BaseComponents (D).t -> BaseComponents (D).t
val threadspawn: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit
val thread_join: ?force:bool -> Q.ask -> (V.t -> G.t) -> Cil.exp -> BaseComponents (D).t -> BaseComponents (D).t
val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> BaseComponents (D).t -> BaseComponents (D).t
val invariant_global: Q.ask -> (V.t -> G.t) -> V.t -> Invariant.t
val invariant_vars: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> varinfo list
val init: unit -> unit
val finalize: unit -> unit
end
module NoFinalize =
struct
let finalize () = ()
end
let old_threadenter (type d) ask (st: d BaseDomain.basecomponents_t) =
(* Copy-paste from Base make_entry *)
let globals = CPA.filter (fun k v -> is_global ask k) st.cpa in
(* let new_cpa = if !earlyglobs || ThreadFlag.is_multi man.ask then CPA.filter (fun k v -> is_private man.ask man.local k) globals else globals in *)
let new_cpa = globals in
{st with cpa = new_cpa}
let startstate_threadenter (type d) (startstate: unit -> d) ask (st: d BaseDomain.basecomponents_t) =
{st with cpa = CPA.bot (); priv = startstate ()}
(** Wrappers. *)
module type PrivatizationWrapper = functor(GBase:Lattice.S) ->
sig
module G: Lattice.S
val getg: Q.ask -> ('a -> G.t) -> 'a -> GBase.t
val sideg: Q.ask -> ('a -> G.t -> unit) -> 'a -> GBase.t -> unit
end
module NoWrapper:PrivatizationWrapper = functor (GBase:Lattice.S) ->
(struct
module G = GBase
let getg _ getg = getg
let sideg _ sideg = sideg
end)
module DigestWrapper(Digest: Digest):PrivatizationWrapper = functor (GBase:Lattice.S) ->
(struct
module G = MapDomain.MapBot_LiftTop (Digest) (GBase)
let getg ask getg x =
let vs = getg x in
G.fold (fun d v acc ->
if not (Digest.accounted_for ask ~current:(Digest.current ask) ~other:d) then
GBase.join v acc
else
acc) vs (GBase.bot ())
let sideg ask sideg x v =
let sidev = G.singleton (Digest.current ask) v in
sideg x sidev
end)
(** No Privatization. *)
module NonePriv: S =
struct
include NoFinalize
module G = VD
module V = VarinfoV
module D = Lattice.Unit
let init () = ()
let startstate () = ()
let lock ask getg st m = st
let unlock ask getg sideg st m = st
let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
getg x
let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
let v = (* Copied from MainFunctor.update_variable *)
if get_bool "exp.volatiles_are_top" && is_always_unknown x then (* TODO: why don't other privatizations do this? why in write_global, not read_global? why not in base directly? why not in other value analyses? *)
VD.top ()
else
v
in
if not invariant then
sideg x v;
st
let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
(* required for branched thread creation *)
CPA.fold (fun x v (st: BaseComponents (D).t) ->
if is_global ask x then (
sideg x v;
{st with cpa = CPA.remove x st.cpa}
)
else
st
) st.cpa st
in
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st
let escape ask getg sideg (st: BaseComponents (D).t) escaped =
let cpa' = CPA.fold (fun x v acc ->
if EscapeDomain.EscapedVars.mem x escaped then (
sideg x v;
CPA.remove x acc
)
else
acc
) st.cpa st.cpa
in
{st with cpa = cpa'}
let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
CPA.fold (fun x v (st: BaseComponents (D).t) ->
if is_global ask x then (
sideg x v;
{st with cpa = CPA.remove x st.cpa}
)
else
st
) st.cpa st
let threadenter ask st = st
let threadspawn ask get set st = st
let thread_join ?(force=false) ask get e st = st
let thread_return ask get set tid st = st
let iter_sys_vars getg vq vf =
match vq with
| VarQuery.Global g ->
vf g;
| _ -> ()
let invariant_global ask getg g =
ValueDomain.invariant_global getg g
let invariant_vars ask getg st = []
end
module PerMutexPrivBase =
struct
include NoFinalize
include ConfCheck.RequireMutexActivatedInit
include MutexGlobals
include Protection
module D = Lattice.Unit
module G = CPA
let startstate () = ()
let get_m_with_mutex_inits ask getg m =
let get_m = getg (V.mutex m) in
let get_mutex_inits = getg V.mutex_inits in
let is_in_Gm x _ = is_protected_by ask m x in
let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in
if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n get_m: %a\n get_mutex_inits: %a\n get_mutex_inits': %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits';
CPA.join get_m get_mutex_inits'
(** [get_m_with_mutex_inits] optimized for implementation-specialized [read_global]. *)
let get_mutex_global_x_with_mutex_inits getg x =
let get_mutex_global_x = getg (V.global x) in
let get_mutex_inits = getg V.mutex_inits in
match CPA.find_opt x get_mutex_global_x, CPA.find_opt x get_mutex_inits with
| Some v1, Some v2 -> Some (VD.join v1 v2)
| Some v, None
| None, Some v -> Some v
| None, None -> None
let read_unprotected_global getg x =
let get_mutex_global_x = get_mutex_global_x_with_mutex_inits getg x in
(* None is VD.top () *)
get_mutex_global_x |? VD.bot ()
let escape ask getg sideg (st: BaseComponents (D).t) escaped =
let escaped_cpa = CPA.filter (fun x _ -> EscapeDomain.EscapedVars.mem x escaped) st.cpa in
sideg V.mutex_inits escaped_cpa;
let cpa' = CPA.fold (fun x v acc ->
if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then (
if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
sideg (V.global x) (CPA.singleton x v);
CPA.remove x acc
)
else
acc
) st.cpa st.cpa
in
{st with cpa = cpa'}
let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
let global_cpa = CPA.filter (fun x _ -> is_global ask x) st.cpa in
sideg V.mutex_inits global_cpa;
let cpa' = CPA.fold (fun x v acc ->
if is_global ask x (* && is_unprotected ask x *) then (
if M.tracing then M.tracel "priv" "enter_multithreaded remove %a" CilType.Varinfo.pretty x;
if M.tracing then M.tracel "priv" "ENTER MULTITHREADED SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
sideg (V.global x) (CPA.singleton x v);
CPA.remove x acc
)
else
acc
) st.cpa st.cpa
in
{st with cpa = cpa'}
let threadenter = old_threadenter
let threadspawn ask get set st = st
let thread_join ?(force=false) ask get e st = st
let thread_return ask get set tid st = st
let invariant_global ask getg = function
| `Right g' -> (* global *)
ValueDomain.invariant_global (read_unprotected_global getg) g' (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *)
| _ -> (* mutex *)
Invariant.none
end
module PerMutexOplusPriv: S =
struct
include PerMutexPrivBase
let read_global ask getg (st: BaseComponents (D).t) x =
if is_unprotected ask x then
read_unprotected_global getg x
else
CPA.find x st.cpa
(* let read_global ask getg cpa x =
let (cpa', v) as r = read_global ask getg cpa x in
Logs.debug "READ GLOBAL %a (%a, %B) = %a" CilType.Varinfo.pretty x CilType.Location.pretty !Goblint_tracing.current_loc (is_unprotected ask x) VD.pretty v;
r *)
let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
let cpa' = CPA.add x v st.cpa in
if not invariant then
sideg (V.global x) (CPA.singleton x v);
(* Unlock after invariant will still side effect refined value from CPA, because cannot distinguish from non-invariant write. *)
{st with cpa = cpa'}
(* let write_global ask getg sideg cpa x v =
let cpa' = write_global ask getg sideg cpa x v in
Logs.debug "WRITE GLOBAL %a %a = %a" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa';
cpa' *)
let lock ask getg (st: BaseComponents (D).t) m =
if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
let get_m = get_m_with_mutex_inits ask getg m in
(* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
where our (necessary) original context still has the mutex,
so the query would be on the wrong lockset.
TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
Therefore, just use _without to exclude the mutex we shouldn't have.
In non-cond locks we don't have it anyway, so there's no difference.
No other privatization uses is_unprotected, so this hack is only needed here. *)
let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
let cpa' = CPA.filter is_in_V get_m in
if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pretty m CPA.pretty cpa';
{st with cpa = CPA.fold CPA.add cpa' st.cpa}
)
else
st (* sound w.r.t. recursive lock *)
let unlock ask getg sideg (st: BaseComponents (D).t) m =
let is_in_Gm x _ = is_protected_by ask m x in
let side_m_cpa = CPA.filter is_in_Gm st.cpa in
if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pretty m CPA.pretty side_m_cpa;
sideg (V.mutex m) side_m_cpa;
st
let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
(* required for branched thread creation *)
let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in
sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *)
(* TODO: this makes mutex-oplus less precise in 28-race_reach/10-ptrmunge_racefree and 28-race_reach/trylock2_racefree, why? *)
CPA.iter (fun x v ->
(* TODO: is_unprotected - why breaks 02/11 init_mainfun? *)
if is_global ask x && is_unprotected ask x then
sideg (V.global x) (CPA.singleton x v)
) st.cpa;
st
in
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st
let invariant_vars ask getg st = protected_vars ask
end
module PerMutexMeetPrivBase =
struct
include PerMutexPrivBase
let invariant_global (ask: Q.ask) getg = function
| `Left m' -> (* mutex *)
let atomic = LockDomain.MustLock.equal m' (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
if atomic || ask.f (GhostVarAvailable (Locked m')) then (
let cpa = get_m_with_mutex_inits ask getg m' in (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *)
let inv = CPA.fold (fun v _ acc ->
if ask.f (MustBeProtectedBy {mutex = m'; global = v; kind = Write; protection = Strong}) then
let inv = ValueDomain.invariant_global (fun g -> CPA.find g cpa) v in
Invariant.(acc && inv)
else
acc
) cpa Invariant.none
in
if atomic then
inv
else (
let var = WitnessGhost.to_varinfo (Locked m') in
Invariant.(of_exp (Lval (GoblintCil.var var)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
)
else
Invariant.none
| g -> (* global *)
invariant_global ask getg g
let invariant_vars ask getg (st: _ BaseDomain.basecomponents_t) =
(* Mutex-meet local states contain precisely the protected global variables,
so we can do fewer queries than {!protected_vars}. *)
CPA.fold (fun x v acc ->
if is_global ask x then
x :: acc
else
acc
) st.cpa []
end
module PerMutexMeetPriv: S =
struct
include PerMutexMeetPrivBase
let read_global ask getg (st: BaseComponents (D).t) x =
if is_unprotected ask x then (
(* If the global is unprotected, all appropriate information should come via the appropriate globals, local value may be too small due to stale values surviving widening *)
read_unprotected_global getg x
)
else
CPA.find x st.cpa
let read_global ask getg st x =
let v = read_global ask getg st x in
if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pretty x (is_unprotected ask x) CPA.pretty st.cpa VD.pretty v;
v
let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
let cpa' =
if is_unprotected ask x then
st.cpa
else
CPA.add x v st.cpa
in
if not invariant then (
if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
let side_cpa = CPA.singleton x v in
sideg (V.global x) side_cpa;
if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then
sideg V.mutex_inits side_cpa (* Also side to inits because with earlyglobs enter_multithreaded does not side everything to inits *)
(* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write. *)
);
{st with cpa = cpa'}
(* let write_global ask getg sideg cpa x v =
let cpa' = write_global ask getg sideg cpa x v in
Logs.debug "WRITE GLOBAL %a %a = %a" CilType.Varinfo.pretty x VD.pretty v CPA.pretty cpa';
cpa' *)
let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
let get_m = get_m_with_mutex_inits ask getg m in
(* Additionally filter get_m in case it contains variables it no longer protects. *)
let is_in_Gm x _ = is_protected_by ask m x in
let get_m = CPA.filter is_in_Gm get_m in
let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
let meet = long_meet st.cpa get_m in
if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet;
{st with cpa = meet}
)
else
st (* sound w.r.t. recursive lock *)
let unlock ask getg sideg (st: BaseComponents (D).t) m =
let is_in_Gm x _ = is_protected_by ask m x in
sideg (V.mutex m) (CPA.filter is_in_Gm st.cpa);
let cpa' = CPA.fold (fun x v cpa ->
if is_protected_by ask m x && is_unprotected_without ask x m then
CPA.remove x cpa
(* CPA.add x (VD.top ()) cpa *)
else
cpa
) st.cpa st.cpa
in
{st with cpa = cpa'}
let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
(* required for branched thread creation *)
let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in
sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *)
let cpa' = CPA.fold (fun x v cpa ->
if is_global ask x && is_unprotected ask x (* && not (VD.is_top v) *) then (
if M.tracing then M.tracel "priv" "SYNC SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
sideg (V.global x) (CPA.singleton x v);
CPA.remove x cpa
)
else (
if M.tracing then M.tracel "priv" "SYNC NOSIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
cpa
)
) st.cpa st.cpa
in
{st with cpa = cpa'}
in
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st
end
module PerMutexMeetTIDPriv (Digest: Digest): S =
struct
open Queries.Protection
include PerMutexMeetPrivBase
include PerMutexTidCommonNC (Digest) (CPA)
let iter_sys_vars getg vq vf =
match vq with
| VarQuery.Global g -> vf (V.global g)
| _ -> ()
let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2
let update_if_mem var value m =
if CPA.mem var m then
CPA.add var value m
else
m
let get_mutex_global_g_with_mutex_inits inits ask getg g =
let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
let r = if not inits then
get_mutex_global_g
else
let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
let get_mutex_inits' = CPA.singleton g (CPA.find g get_mutex_inits) in
CPA.join get_mutex_global_g get_mutex_inits'
in
r
let get_relevant_writes (ask:Q.ask) m v =
let current = Digest.current ask in
let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
GMutex.fold (fun k v acc ->
if not (Digest.accounted_for ask ~current ~other:k) then
CPA.join acc (CPA.filter is_in_Gm v)
else
acc
) v (CPA.bot ())
let get_m_with_mutex_inits inits ask getg m =
let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
let r =
if not inits then
get_m
else
let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in
CPA.join get_m get_mutex_inits'
in
r
let read_global ask getg (st: BaseComponents (D).t) x =
let _,lmust,l = st.priv in
let lm = LLock.global x in
let tmp = get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg x in
let local_m = BatOption.default (CPA.bot ()) (L.find_opt lm l) in
if is_unprotected ask ~protection:Weak x then
(* We can not rely upon the old value here, it may be too small due to reuse at widening points (and or nice bot/top confusion) in Base *)
CPA.find x (CPA.join tmp local_m)
else
CPA.find x (long_meet st.cpa (CPA.join tmp local_m))
let read_global ask getg st x =
let v = read_global ask getg st x in
if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pretty x (is_unprotected ~protection:Weak ask x) CPA.pretty st.cpa VD.pretty v;
v
let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
let w,lmust,l = st.priv in
let lm = LLock.global x in
let cpa' =
if is_unprotected ask ~protection:Weak x then
st.cpa
else
CPA.add x v st.cpa
in
if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
let digest = Digest.current ask in
let sidev = GMutex.singleton digest (CPA.singleton x v) in
let l' = L.add lm (CPA.singleton x v) l in
let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
let l' = if is_recovered_st then
(* update value of local record for all where it appears *)
L.map (update_if_mem x v) l'
else
l'
in
sideg (V.global x) (G.create_global sidev);
{st with cpa = cpa'; priv = (W.add x w,LMust.add lm lmust,l')}
let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
let _,lmust,l = st.priv in
let lm = LLock.mutex m in
let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
let local_m = BatOption.default (CPA.bot ()) (L.find_opt lm l) in
let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
let local_m = CPA.filter is_in_Gm local_m in
let r = CPA.join get_m local_m in
let meet = long_meet st.cpa r in
{st with cpa = meet}
)
else
st (* sound w.r.t. recursive lock *)
let unlock ask getg sideg (st: BaseComponents (D).t) m =
let w,lmust,l = st.priv in
let cpa' = CPA.fold (fun x v cpa ->
if is_protected_by ~protection:Weak ask m x && is_unprotected_without ~protection:Weak ask x m then
CPA.remove x cpa
else
cpa
) st.cpa st.cpa
in
let w' = W.filter (fun v -> not (is_unprotected_without ~protection:Weak ask v m)) w in
let side_needed = W.exists (fun v -> is_protected_by ~protection:Weak ask m v) w in
if not side_needed then
{st with cpa = cpa'; priv = (w',lmust,l)}
else
let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest (CPA.filter is_in_Gm st.cpa) in
sideg (V.mutex m) (G.create_mutex sidev);
let lm = LLock.mutex m in
let l' = L.add lm (CPA.filter is_in_Gm st.cpa) l in
{st with cpa = cpa'; priv = (w',LMust.add lm lmust,l')}
let thread_join ?(force=false) (ask:Q.ask) getg exp (st: BaseComponents (D).t) =
let w,lmust,l = st.priv in
let tids = ask.f (Q.EvalThread exp) in
if force then (
if ConcDomain.ThreadSet.is_top tids then (
M.info ~category:Unsound "Unknown thread ID assume-joined, privatization unsound"; (* TODO: something more sound *)
st (* cannot find all thread IDs to join them all *)
)
else (
(* fold throws if the thread set is top *)
let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
let lmust',l' = G.thread (getg (V.thread tid)) in
(LMust.union lmust' lmust, L.join l l')
) tids' (lmust, l)
in
{st with priv = (w, lmust', l')}
)
)
else (
if ConcDomain.ThreadSet.is_top tids then
st
else
match ConcDomain.ThreadSet.elements tids with
| [tid] ->
let lmust',l' = G.thread (getg (V.thread tid)) in
{st with priv = (w, LMust.union lmust' lmust, L.join l l')}
| _ ->
(* To match the paper more closely, one would have to join in the non-definite case too *)
(* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
st
)
let thread_return ask getg sideg tid (st: BaseComponents (D).t) =
let _,lmust,l = st.priv in
sideg (V.thread tid) (G.create_thread (lmust,l));
st
let sync (ask:Q.ask) getg sideg (st: BaseComponents (D).t) reason =
(* TODO: Is more needed here? *)
st
let escape ask getg sideg (st: BaseComponents (D).t) escaped =
let escaped_cpa = CPA.filter (fun x _ -> EscapeDomain.EscapedVars.mem x escaped) st.cpa in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest escaped_cpa in
sideg V.mutex_inits (G.create_mutex sidev);
let cpa' = CPA.fold (fun x v acc ->
if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then (
if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v;
let sidev = GMutex.singleton digest (CPA.singleton x v) in
sideg (V.global x) (G.create_global sidev);
CPA.remove x acc
)
else
acc
) st.cpa st.cpa
in
{st with cpa = cpa'}
let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
let cpa = st.cpa in
let cpa_side = CPA.filter (fun x _ -> is_global ask x) cpa in
let digest = Digest.current ask in
let sidev = GMutex.singleton digest cpa_side in
sideg V.mutex_inits (G.create_mutex sidev);
(* Introduction into local state not needed, will be read via initializer *)
(* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
(* or it will be locally overwitten and in LMust in which case these values are irrelevant anyway *)
let cpa_local = CPA.filter (fun x _ -> not @@ is_global ask x) cpa in
{st with cpa= cpa_local }
let threadenter ask (st: BaseComponents (D).t): BaseComponents (D).t =
let _,lmust,l = st.priv in
(* Thread starts without any mutexes, so the local state cannot contain any privatized things. The locals of the created thread are added later, *)
(* so the cpa component of st is bot. *)
{st with cpa = CPA.bot (); priv = (W.bot (),lmust,l)}
let threadspawn (ask:Queries.ask) get set (st: BaseComponents (D).t) =
let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in
let unprotected_after x = ask.f (Q.MayBePublic {global=x; kind=Write; protection=Weak}) in
if is_recovered_st then
(* Remove all things that are now unprotected *)
let cpa' = CPA.fold (fun x v cpa ->
(* recoverable is false as after this, we will be multi-threaded *)
if unprotected_after x then
CPA.remove x cpa
else
cpa
) st.cpa st.cpa
in
{st with cpa = cpa'}
else st
let read_unprotected_global getg x =
let get_mutex_global_x = merge_all @@ G.mutex @@ getg (V.global x) in
let get_mutex_global_x' = CPA.find x get_mutex_global_x in
let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
let get_mutex_inits' = CPA.find x get_mutex_inits in
VD.join get_mutex_global_x' get_mutex_inits'
let invariant_global ask getg = function
| `Middle g -> (* global *)
ValueDomain.invariant_global (read_unprotected_global getg) g (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *)
| `Left _
| `Right _ -> (* mutex or thread *)
Invariant.none
end
(** Vojdani privatization with eager reading. *)
module VojdaniPriv: S =
struct
include NoFinalize
include ConfCheck.RequireMutexActivatedInit
open Protection
module D = Lattice.Unit
module G = VD
module V = VarinfoV
let startstate () = ()
let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
if is_unprotected ask ~kind:ReadWrite x then
VD.join (CPA.find x st.cpa) (getg x)
else
CPA.find x st.cpa
let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
if not invariant then (
if is_unprotected ask ~kind:ReadWrite x then
sideg x v;
if !earlyglobs then (* earlyglobs workaround for 13/60 *)
sideg x v (* TODO: is this needed for anything? 13/60 doesn't work for other reasons *)
);
{st with cpa = CPA.add x v st.cpa}
let lock ask getg (st: BaseComponents (D).t) m =
let cpa' = CPA.mapi (fun x v ->
if is_protected_by ask ~kind:ReadWrite m x && is_unprotected ask ~kind:ReadWrite x then (* is_in_Gm *)
VD.join (CPA.find x st.cpa) (getg x)
else
v
) st.cpa
in
{st with cpa = cpa'}
let unlock ask getg sideg (st: BaseComponents (D).t) m =
CPA.iter (fun x v ->
if is_protected_by ask ~kind:ReadWrite m x then ( (* is_in_Gm *)
if is_unprotected_without ask ~kind:ReadWrite x m then (* is_in_V' *)
sideg x v
)
) st.cpa;
st
let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
(* required for branched thread creation *)
CPA.iter (fun x v ->
if is_global ask x && is_unprotected ask ~kind:ReadWrite x then
sideg x v
) st.cpa;
st
in
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st
let escape ask getg sideg (st: BaseComponents (D).t) escaped =
CPA.iter (fun x v ->
if EscapeDomain.EscapedVars.mem x escaped then
sideg x v
) st.cpa;
st
let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) =
CPA.iter (fun x v ->
if is_global ask x then
sideg x v
) st.cpa;
st
let threadenter ask st = st
let threadspawn ask get set st = st
let thread_join ?(force=false) ask get e st = st
let thread_return ask get set tid st = st
let iter_sys_vars getg vq vf =
match vq with
| VarQuery.Global g ->
vf g;
| _ -> ()
let invariant_global (ask: Q.ask) getg g =
let locks = ask.f (Q.MustProtectingLocks {global = g; kind = ReadWrite}) in
if LockDomain.MustLockset.is_all locks then
Invariant.none
else (
(* Only read g as protected, everything else (e.g. pointed to variables) may be unprotected.
See 56-witness/69-ghost-ptr-protection and https://github.com/goblint/analyzer/pull/1394#discussion_r1698136411. *)
let read_global g' = if CilType.Varinfo.equal g' g then getg g' else VD.top () in (* TODO: Could be more precise for at least those which might not have all same protecting locks? *)
let inv = ValueDomain.invariant_global read_global g in
(* Very conservative about multiple protecting mutexes: invariant is not claimed when any of them is held.
It should be possible to be more precise because writes only happen with all of them held,
but conjunction is unsound when one of the mutexes is temporarily unlocked.
Hypothetical read-protection is also somehow relevant. *)
LockDomain.MustLockset.fold (fun m acc ->
if LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) then
acc
else if ask.f (GhostVarAvailable (Locked m)) then (
let var = WitnessGhost.to_varinfo (Locked m) in
Invariant.(of_exp (Lval (GoblintCil.var var)) || acc) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
else
Invariant.none
) locks inv
)
let invariant_vars ask getg st = protected_vars ask
end
module type PerGlobalPrivParam =
sig
(** Whether to also check unprotectedness by reads for extra precision. *)
val check_read_unprotected: bool
include AtomicParam
end
(** Protection-Based Reading. *)
module ProtectionBasedV = struct
module VUnprot =
struct
include VarinfoV (* [g]' *)
let name () = "unprotected"
end
module VProt =
struct
include VarinfoV (* [g] *)
let name () = "protected"
end
module V =
struct
include Printable.Either (VUnprot) (VProt)
let unprotected x = `Left x
let protected x = `Right x
end
end
(** Protection-Based Reading. *)
module ProtectionBasedPriv (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
struct
include NoFinalize
include ConfCheck.RequireMutexActivatedInit
open Protection
module P =
struct
include MustVars
let name () = "P"
end
(* W is implicitly represented by CPA domain *)
module D = P
module Wrapper = Wrapper (VD)
module G = Wrapper.G
module V = ProtectionBasedV.V
let startstate () = P.empty ()
let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
let getg = Wrapper.getg ask getg in
if P.mem x st.priv then
CPA.find x st.cpa
else if Param.handle_atomic && ask.f MustBeAtomic then
VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
else if is_unprotected ask x then
getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
else
VD.join (CPA.find x st.cpa) (getg (V.protected x))
let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
let sideg = Wrapper.sideg ask sideg in
if not invariant then (
if not (Param.handle_atomic && ask.f MustBeAtomic) then
sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then (* earlyglobs workaround for 13/60 *)
sideg (V.protected x) v (* Also side to protected because with earlyglobs enter_multithreaded does not side everything to protected *)
(* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
);
if Param.handle_atomic && ask.f MustBeAtomic then
{st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
else if is_unprotected ask x then
st
else
{st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
let lock ask getg st m = st
let unlock ask getg sideg (st: BaseComponents (D).t) m =
let sideg = Wrapper.sideg ask sideg in
let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
(* TODO: what about G_m globals in cpa that weren't actually written? *)
CPA.fold (fun x v (st: BaseComponents (D).t) ->
if is_protected_by ask m x then ( (* is_in_Gm *)
(* Extra precision in implementation to pass tests:
If global is read-protected by multiple locks,
then inner unlock shouldn't yet publish. *)
if not Param.check_read_unprotected || is_unprotected_without ask ~kind:ReadWrite x m then
sideg (V.protected x) v;
if atomic then
sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
if is_unprotected_without ask x m then (* is_in_V' *)
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
else
st
)
else
st
) st.cpa st
let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
(* required for branched thread creation *)
let sideg = Wrapper.sideg ask sideg in
CPA.fold (fun x v (st: BaseComponents (D).t) ->
if is_global ask x && is_unprotected ask x then (
sideg (V.unprotected x) v;
sideg (V.protected x) v; (* must be like enter_multithreaded *)
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
)
else
st
) st.cpa st
in
match reason with
| `Join when ConfCheck.branched_thread_creation () ->
branched_sync ()
| `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
branched_sync ()
| `Join
| `JoinCall _
| `Return
| `Normal
| `Init
| `Thread ->
st
let escape ask getg sideg (st: BaseComponents (D).t) escaped =
let sideg = Wrapper.sideg ask sideg in
let cpa' = CPA.fold (fun x v acc ->
if EscapeDomain.EscapedVars.mem x escaped then (
sideg (V.unprotected x) v;
sideg (V.protected x) v;
CPA.remove x acc
)
else
acc
) st.cpa st.cpa