-
Notifications
You must be signed in to change notification settings - Fork 2.1k
Expand file tree
/
Copy pathbufferOverrunModels.ml
More file actions
2407 lines (2081 loc) · 101 KB
/
bufferOverrunModels.ml
File metadata and controls
2407 lines (2081 loc) · 101 KB
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
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
module L = Logging
open AbsLoc
open! AbstractDomain.Types
module BoField = BufferOverrunField
module BoUtils = BufferOverrunUtils
module Dom = BufferOverrunDomain
module PO = BufferOverrunProofObligations
module Sem = BufferOverrunSemantics
module Trace = BufferOverrunTrace
open BoUtils.ModelEnv
open FuncArg
type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t
type check_fun = model_env -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t
type model = {exec: exec_fun; check: check_fun}
let no_check _model_env _mem cond_set = cond_set
let no_model =
let exec {pname; location} ~ret mem =
L.d_printfln_escaped "No model for %a" Procname.pp pname ;
Dom.Mem.add_unknown_from ret ~callee_pname:pname ~location mem
in
{exec; check= no_check}
let at ?(size = Int64.zero) array_exp index_exp =
(* TODO? use size *)
let exec {integer_type_widths} ~ret:(id, _) mem =
L.d_printfln_escaped "Using model std::array<_, %Ld>::at" size ;
Dom.Mem.add_stack (Loc.of_id id)
(Sem.eval_lindex integer_type_widths array_exp index_exp mem)
mem
and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem location
cond_set
in
{exec; check}
let eval_binop ~f e1 e2 =
let exec {integer_type_widths} ~ret:(id, _) mem =
let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in
let i2 = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in
let v = f i1 i2 |> Dom.Val.of_itv in
Dom.Mem.add_stack (Loc.of_id id) v mem
in
{exec; check= no_check}
let get_malloc_info_opt = function
| Exp.BinOp (Binop.Mult _, Exp.Sizeof {typ; nbytes}, length)
| Exp.BinOp (Binop.Mult _, length, Exp.Sizeof {typ; nbytes}) ->
Some (typ, nbytes, length, None)
(* In Java all arrays are dynamically allocated *)
| Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java ->
Some (typ, nbytes, arr_length, Some arr_length)
| Exp.Sizeof {typ; nbytes; dynamic_length} ->
Some (typ, nbytes, Exp.one, dynamic_length)
| _ ->
None
let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option =
fun x ->
get_malloc_info_opt x
|> IOption.if_none_eval ~f:(fun () -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None))
let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem cond_set =
let _, _, length0, _ = get_malloc_info size_exp in
let v_length = Sem.eval integer_type_widths length0 mem in
match Dom.Val.get_itv v_length with
| Bottom ->
cond_set
| NonBottom length ->
let traces = Dom.Val.get_traces v_length in
let latest_prune = Dom.Mem.get_latest_prune mem in
PO.ConditionSet.add_alloc_size location ~can_be_zero ~length traces latest_prune cond_set
let fgets str_exp num_exp =
let exec {integer_type_widths} ~ret:(id, _) mem =
let str_v = Sem.eval integer_type_widths str_exp mem in
let num_v = Sem.eval integer_type_widths num_exp mem in
let traces = Trace.Set.join (Dom.Val.get_traces str_v) (Dom.Val.get_traces num_v) in
let update_strlen1 allocsite arrinfo acc =
let strlen =
let offset = ArrayBlk.ArrInfo.get_offset arrinfo in
let num = Dom.Val.get_itv num_v in
Itv.plus offset (Itv.set_lb_zero (Itv.decr num))
in
Dom.Mem.set_first_idx_of_null (Loc.of_allocsite allocsite) (Dom.Val.of_itv ~traces strlen) acc
in
mem
|> Dom.Mem.update_mem (Sem.eval_locs str_exp mem) Dom.Val.Itv.zero_255
|> ArrayBlk.fold update_strlen1 (Dom.Val.get_array_blk str_v)
|> Dom.Mem.add_stack (Loc.of_id id) {str_v with itv= Itv.zero}
|> Dom.Mem.fgets_alias id (Dom.Val.get_all_locs str_v)
and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte integer_type_widths ~array_exp:str_exp ~byte_index_exp:num_exp
~last_included:true mem location cond_set
in
{exec; check}
let malloc ~can_be_zero size_exp =
let exec ({pname; caller_pname; node_hash; location; tenv; integer_type_widths} as model_env)
~ret:(id, _) mem =
let size_exp = BiabductionProp.exp_normalize_noabs tenv size_exp in
let typ, stride, length0, dyn_length = get_malloc_info size_exp in
let length = Sem.eval integer_type_widths length0 mem in
let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in
let path =
Dom.Mem.find_simple_alias id mem
|> List.find_map ~f:(fun (rhs, i) -> if IntLit.iszero i then Loc.get_path rhs else None)
in
let offset, size = (Itv.zero, Dom.Val.get_itv length) in
let represents_multiple_values = not (Itv.is_one size) in
let allocsite =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path
~represents_multiple_values
in
let mem =
if Config.bo_bottom_as_default then mem
else
let loc = Loc.of_allocsite allocsite in
match Dom.Mem.find_opt loc mem with
| None ->
(* If the allocsite is not present in the abstract state, write bot as a value of
allocsite. This effectively means that the first update of allocsite is strong
(the new value will be joined with bot).
That is, it relies on the assumption that an allocsite is fully initialized before
being read (e.g., all elements of an array are initialized before the array is read).*)
Dom.Mem.strong_update (PowLoc.singleton (Loc.of_allocsite allocsite)) Dom.Val.bot mem
| _ ->
(* If the allocsite is already in the abstract state, it means that we are in a loop.
The abstract allocsite represents multiple concrete allocsites and we need to retain
values already in the abstract state. The subsequent update of the allocsite will be
weak (the new value will be joined with the value in the abstract state). *)
mem
in
if Language.curr_language_is Java then
let internal_arr =
let allocsite =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
~represents_multiple_values
in
Dom.Val.of_java_array_alloc allocsite ~length:size ~traces
in
let arr_loc = Loc.of_allocsite allocsite in
mem
|> Dom.Mem.add_heap arr_loc internal_arr
|> Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_pow_loc ~traces (PowLoc.singleton arr_loc))
else
let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in
mem
|> Dom.Mem.add_stack (Loc.of_id id) v
|> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length
and check = check_alloc_size ~can_be_zero size_exp in
{exec; check}
let calloc size_exp stride_exp =
let byte_size_exp = Exp.BinOp (Binop.Mult (Some Typ.size_t), size_exp, stride_exp) in
malloc byte_size_exp
let memcpy dest_exp src_exp size_exp =
let exec _ ~ret:_ mem =
let dest_loc = Sem.eval_locs dest_exp mem in
let v = Dom.Mem.find_set (Sem.eval_locs src_exp mem) mem in
Dom.Mem.update_mem dest_loc v mem
and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp
~last_included:true mem location cond_set
|> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp
~last_included:true mem location
in
{exec; check}
let memset arr_exp size_exp =
let exec _ ~ret:_ mem = mem
and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp
~last_included:true mem location cond_set
in
{exec; check}
let strlen arr_exp =
let exec _ ~ret:(id, _) mem =
let v = Sem.eval_string_len arr_exp mem in
Dom.Mem.add_stack (Loc.of_id id) v mem
in
{exec; check= no_check}
let strcpy dest_exp src_exp =
let exec {integer_type_widths} ~ret:(id, _) mem =
let src_loc = Sem.eval_locs src_exp mem in
let dest_loc = Sem.eval_locs dest_exp mem in
mem
|> Dom.Mem.update_mem dest_loc (Dom.Mem.find_set src_loc mem)
|> Dom.Mem.update_mem (PowLoc.of_c_strlen dest_loc) (Dom.Mem.get_c_strlen src_loc mem)
|> Dom.Mem.add_stack (Loc.of_id id) (Sem.eval integer_type_widths dest_exp mem)
and check {integer_type_widths; location} mem cond_set =
let access_last_char =
let idx = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in
let latest_prune = Dom.Mem.get_latest_prune mem in
fun arr cond_set ->
BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune
location cond_set
in
cond_set
|> access_last_char (Sem.eval integer_type_widths dest_exp mem)
|> access_last_char (Sem.eval integer_type_widths src_exp mem)
in
{exec; check}
let strncpy dest_exp src_exp size_exp =
let {exec= memcpy_exec; check= memcpy_check} = memcpy dest_exp src_exp size_exp in
let exec model_env ~ret mem =
let dest_strlen_loc = PowLoc.of_c_strlen (Sem.eval_locs dest_exp mem) in
let strlen = Dom.Mem.find_set (PowLoc.of_c_strlen (Sem.eval_locs src_exp mem)) mem in
mem |> memcpy_exec model_env ~ret |> Dom.Mem.update_mem dest_strlen_loc strlen
in
{exec; check= memcpy_check}
let strcat dest_exp src_exp =
let exec {integer_type_widths} ~ret:(id, _) mem =
let src_loc = Sem.eval_locs src_exp mem in
let dest_loc = Sem.eval_locs dest_exp mem in
let new_contents =
let src_contents = Dom.Mem.find_set src_loc mem in
let dest_contents = Dom.Mem.find_set dest_loc mem in
Dom.Val.join dest_contents src_contents
in
let src_strlen = Dom.Mem.get_c_strlen src_loc mem in
let new_strlen =
let dest_strlen = Dom.Mem.get_c_strlen dest_loc mem in
Dom.Val.plus_a dest_strlen src_strlen
in
mem
|> Dom.Mem.update_mem dest_loc new_contents
|> Dom.Mem.update_mem (PowLoc.of_c_strlen dest_loc) new_strlen
|> Dom.Mem.add_stack (Loc.of_id id) (Sem.eval integer_type_widths dest_exp mem)
and check {integer_type_widths; location} mem cond_set =
let access_last_char arr idx cond_set =
let latest_prune = Dom.Mem.get_latest_prune mem in
BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location
cond_set
in
let src_strlen =
let str_loc = Sem.eval_locs src_exp mem in
Dom.Mem.get_c_strlen str_loc mem
in
let new_strlen =
let dest_strlen =
let dest_loc = Sem.eval_locs dest_exp mem in
Dom.Mem.get_c_strlen dest_loc mem
in
Dom.Val.plus_a dest_strlen src_strlen
in
cond_set
|> access_last_char (Sem.eval integer_type_widths dest_exp mem) new_strlen
|> access_last_char (Sem.eval integer_type_widths src_exp mem) src_strlen
in
{exec; check}
let realloc src_exp size_exp =
let exec ({location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem =
let size_exp = BiabductionProp.exp_normalize_noabs tenv size_exp in
let typ, _, length0, dyn_length = get_malloc_info size_exp in
let length = Sem.eval integer_type_widths length0 mem in
let v = Sem.eval integer_type_widths src_exp mem |> Dom.Val.set_array_length location ~length in
let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
Option.value_map dyn_length ~default:mem ~f:(fun dyn_length ->
let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in
BoUtils.Exec.set_dyn_length model_env typ (Dom.Val.get_array_locs v) dyn_length mem )
and check = check_alloc_size ~can_be_zero:false size_exp in
{exec; check}
let placement_new size_exp {exp= src_exp1; typ= t1} src_arg2_opt =
match (t1.Typ.desc, src_arg2_opt) with
| Tint _, None | Tint _, Some {typ= {Typ.desc= Tint _}} ->
malloc ~can_be_zero:true (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1))
| Tstruct (CppClass {name}), None
when [%equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] ->
malloc ~can_be_zero:true size_exp
| _, _ ->
let exec {integer_type_widths} ~ret:(id, _) mem =
let src_exp =
if Typ.is_pointer_to_void t1 then src_exp1
else
match src_arg2_opt with
| Some {exp= src_exp2; typ= t2} when Typ.is_pointer_to_void t2 ->
src_exp2
| _ ->
(* TODO: Raise an exception when given unexpected arguments. Before that, we need
to fix the frontend to parse user defined `new` correctly. *)
L.d_error "Unexpected types of arguments for __placement_new" ;
src_exp1
in
let v = Sem.eval integer_type_widths src_exp mem in
Dom.Mem.add_stack (Loc.of_id id) v mem
in
{exec; check= no_check}
let strndup src_exp length_exp =
let exec ({pname; caller_pname; node_hash; location; integer_type_widths} as model_env)
~ret:((id, _) as ret) mem =
let v =
let src_strlen = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in
let length = Sem.eval integer_type_widths length_exp mem in
let size = Itv.incr (Itv.min_sem (Dom.Val.get_itv src_strlen) (Dom.Val.get_itv length)) in
let allocsite =
let represents_multiple_values = not (Itv.is_one size) in
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
~represents_multiple_values
in
let traces =
Trace.Set.join (Dom.Val.get_traces src_strlen) (Dom.Val.get_traces length)
|> Trace.Set.add_elem location Trace.Through
|> Trace.Set.add_elem location ArrayDeclaration
in
Dom.Val.of_c_array_alloc allocsite
~stride:(Some (integer_type_widths.char_width / 8))
~offset:Itv.zero ~size ~traces
in
mem
|> Dom.Mem.add_stack (Loc.of_id id) v
|> (strncpy (Exp.Var id) src_exp length_exp).exec model_env ~ret
in
{exec; check= no_check}
let set_size {integer_type_widths; location} array_v size_exp mem =
let locs = Dom.Val.get_pow_loc array_v in
let length = Sem.eval integer_type_widths size_exp mem in
Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) locs mem
let model_by_value value id mem = Dom.Mem.add_stack (Loc.of_id id) value mem
let cast exp size_exp =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let v = Sem.eval integer_type_widths exp mem in
let v = match size_exp with Exp.Sizeof {typ} -> Dom.Val.cast typ v | _ -> v in
model_by_value v ret_id mem
in
{exec; check= no_check}
let id exp =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let v = Sem.eval integer_type_widths exp mem in
model_by_value v ret_id mem
in
{exec; check= no_check}
let by_value =
let exec ~value _ ~ret:(ret_id, _) mem = model_by_value value ret_id mem in
fun value -> {exec= exec ~value; check= no_check}
let bottom =
let exec _model_env ~ret:_ _mem = Dom.Mem.unreachable in
{exec; check= no_check}
let infer_print e =
let exec {location; integer_type_widths} ~ret:_ mem =
L.(debug BufferOverrun Medium)
"@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp
(Sem.eval integer_type_widths e mem) ;
mem
in
{exec; check= no_check}
let load_size_alias id arr_locs mem =
match PowLoc.is_singleton_or_more arr_locs with
| IContainer.Singleton loc ->
Dom.Mem.load_size_alias id loc mem
| IContainer.Empty | IContainer.More ->
mem
(* Java only *)
let get_array_length array_exp =
let exec _ ~ret:(ret_id, _) mem =
let arr_locs = Sem.eval_locs array_exp mem in
let result = Sem.eval_array_locs_length arr_locs mem in
model_by_value result ret_id mem |> load_size_alias ret_id arr_locs
in
{exec; check= no_check}
(* Clang only *)
let set_array_length {exp; typ} length_exp =
let exec {pname; caller_pname; node_hash; location; integer_type_widths} ~ret:_ mem =
match (exp, typ) with
| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {stride}} ->
let length = Sem.eval integer_type_widths length_exp mem in
let stride = Option.map ~f:IntLit.to_int_exn stride in
let path = Some (Symb.SymbolPath.of_pvar array_pvar) in
let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in
let size = Dom.Val.get_itv length in
let allocsite =
let represents_multiple_values = not (Itv.is_one size) in
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path
~represents_multiple_values
in
let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in
Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem
| _ ->
L.(die InternalError) "Unexpected type of first argument for __set_array_length() "
and check = check_alloc_size ~can_be_zero:false length_exp in
{exec; check}
let copy array_v ret_id mem =
let dest_loc = Loc.of_id ret_id |> PowLoc.singleton in
Dom.Mem.update_mem dest_loc array_v mem
(** Returns a fixed-size array with a given length backed by the specified array. *)
let copyOf array_exp length_exp =
let exec ({integer_type_widths} as model) ~ret:(id, _) mem =
let array_v = Sem.eval integer_type_widths array_exp mem in
copy array_v id mem |> set_size model array_v length_exp
in
{exec; check= no_check}
(** Creates a new array with the values from the given array.*)
let create_copy_array src_exp =
let exec {integer_type_widths} ~ret:(id, _) mem =
let array_v = Sem.eval integer_type_widths src_exp mem in
copy array_v id mem
in
{exec; check= no_check}
module StdArray = struct
let constructor _size =
let exec _model_env ~ret:_ mem =
mem
(* initialize? *)
in
{exec; check= no_check}
let at size {exp= array_exp} {exp= index_exp} = at ~size array_exp index_exp
let begin_ _size {exp= array_exp} =
let exec {location; integer_type_widths} ~ret:(id, _) mem =
let v =
Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location Itv.zero
in
Dom.Mem.add_stack (Loc.of_id id) v mem
in
{exec; check= no_check}
let end_ size {exp= array_exp} =
let exec {location; integer_type_widths} ~ret:(id, _) mem =
let v =
let offset = Itv.of_int_lit (IntLit.of_int64 size) in
Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset
in
Dom.Mem.add_stack (Loc.of_id id) v mem
in
{exec; check= no_check}
let back size {exp= array_exp} =
let exec {location; integer_type_widths} ~ret:(id, _) mem =
let v =
let offset = Itv.of_int_lit (IntLit.of_int64 Int64.(size - one)) in
Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset
in
Dom.Mem.add_stack (Loc.of_id id) v mem
in
{exec; check= no_check}
end
module Iterator = struct
(* This is used in C++11 where there is an intermediate step for linking iterator to a temp *)
let new_ beg_exp temp_exp =
let exec _ ~ret:_ mem =
let locs_b = Sem.eval_locs beg_exp mem in
let locs_t = Sem.eval_locs temp_exp mem in
let v = Dom.Mem.find_set locs_t mem |> Dom.Val.get_itv |> Dom.Val.of_itv in
let mem = Dom.Mem.update_mem locs_b v mem in
match (beg_exp, temp_exp) with
| Exp.Lvar new_pvar, Exp.Lvar existing_pvar ->
Dom.Mem.propagate_cpp_iter_begin_or_end_alias ~new_pvar ~existing_pvar mem
| _ ->
mem
in
{exec; check= no_check}
let copy dest src =
let exec _ ~ret:_ mem =
let dest_loc = Sem.eval_locs dest mem in
let v = Dom.Mem.find_set (Sem.eval_locs src mem) mem in
Dom.Mem.update_mem dest_loc v mem
in
{exec; check= no_check}
let begin_ exp =
let exec _ ~ret:_ mem =
let locs = Sem.eval_locs exp mem in
let mem = Dom.Mem.update_mem locs Dom.Val.Itv.zero mem in
match exp with Exp.Lvar pvar -> Dom.Mem.add_cpp_iter_begin_alias pvar mem | _ -> mem
in
{exec; check= no_check}
let end_ ~size_exec temp_exp =
let exec model_env ~ret:((ret_id, _) as ret) mem =
let mem = size_exec model_env ~ret mem in
let locs = Sem.eval_locs temp_exp mem in
let v = Dom.Mem.find (Loc.of_id ret_id) mem in
let mem = Dom.Mem.update_mem locs v mem in
match temp_exp with Exp.Lvar pvar -> Dom.Mem.add_cpp_iter_end_alias pvar mem | _ -> mem
in
{exec; check= no_check}
let iterator_ne lhs_exp rhs_exp =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let v = Sem.eval integer_type_widths (Exp.BinOp (Binop.Ne, lhs_exp, rhs_exp)) mem in
let mem =
match (lhs_exp, rhs_exp) with
| Exp.Lvar iter_lhs, Exp.Lvar iter_rhs ->
Dom.Mem.add_cpp_iterator_cmp_alias ret_id ~iter_lhs ~iter_rhs mem
| _, _ ->
mem
in
model_by_value v ret_id mem
in
{exec; check= no_check}
let iterator_incr iterator_exp =
let exec _ ~ret:_ mem =
let locs = Sem.eval_locs iterator_exp mem in
let v = Dom.Mem.find_set locs mem |> Dom.Val.get_itv |> Itv.incr |> Dom.Val.of_itv in
Dom.Mem.update_mem locs v mem
in
{exec; check= no_check}
end
module ArrObjCommon = struct
let deref_of {integer_type_widths} exp ~fn ?fn_typ mem =
let typ = Option.map fn_typ ~f:Typ.mk_ptr in
Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths exp mem) |> PowLoc.append_field ?typ ~fn
let eval_size model_env exp ~fn mem =
Sem.eval_array_locs_length (deref_of model_env exp ~fn mem) mem
let size_exec exp ~fn ?fn_typ ({integer_type_widths} as model_env) ~ret:(id, _) mem =
let locs = Sem.eval integer_type_widths exp mem |> Dom.Val.get_all_locs in
match PowLoc.is_singleton_or_more locs with
| Singleton (BoField.Prim (Loc.Allocsite (Allocsite.LiteralString s))) ->
model_by_value (Dom.Val.of_int (String.length s)) id mem
| _ ->
let arr_locs = deref_of model_env exp ~fn ?fn_typ mem in
let mem = Dom.Mem.add_stack (Loc.of_id id) (Sem.eval_array_locs_length arr_locs mem) mem in
load_size_alias id arr_locs mem
let at arr_exp ~fn ?fn_typ index_exp =
let exec ({pname; location} as model_env) ~ret:(id, typ) mem =
let array_v =
let locs = deref_of model_env arr_exp ~fn ?fn_typ mem in
if PowLoc.is_bot locs then Dom.Val.unknown_from typ ~callee_pname:(Some pname) ~location
else Dom.Mem.find_set locs mem
in
Dom.Mem.add_stack (Loc.of_id id) array_v mem
and check ({location; integer_type_widths} as model_env) mem cond_set =
let idx = Sem.eval integer_type_widths index_exp mem in
let arr = Dom.Mem.find_set (deref_of model_env arr_exp ~fn mem) mem in
let latest_prune = Dom.Mem.get_latest_prune mem in
BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location
cond_set
in
{exec; check}
let copy_constructor model_env deref_of_tgt ~fn ?fn_typ src_exp mem =
let deref_of_src = deref_of model_env src_exp ~fn ?fn_typ mem in
Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set deref_of_src mem) mem
let constructor_from_char_ptr ({integer_type_widths} as model_env) tgt_deref ~fn ?char_typ src mem
=
let elem_locs = PowLoc.append_field ?typ:(Option.map char_typ ~f:Typ.mk_ptr) tgt_deref ~fn in
match src with
| Exp.Const (Const.Cstr s) ->
BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem
| _ ->
let v = Sem.eval integer_type_widths src mem in
Dom.Mem.update_mem elem_locs v mem
let check_index ~last_included get_array_locs arr_id index_exp {location; integer_type_widths} mem
cond_set =
let arr =
let arr_locs = get_array_locs arr_id mem in
Dom.Mem.find_set arr_locs mem
in
let idx = Sem.eval integer_type_widths index_exp mem in
let latest_prune = Dom.Mem.get_latest_prune mem in
BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included ~latest_prune location
cond_set
end
module StdVector = struct
let append_field loc ~vec_typ ~elt_typ =
Loc.append_field ~typ:(Typ.mk_ptr elt_typ) loc (BufferOverrunField.cpp_vector_elem ~vec_typ)
let append_fields locs ~vec_typ ~elt_typ =
PowLoc.append_field ~typ:(Typ.mk_ptr elt_typ) locs
~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)
let deref_of model_env elt_typ {exp= vec_exp; typ= vec_typ} mem =
let fn = BufferOverrunField.cpp_vector_elem ~vec_typ in
ArrObjCommon.deref_of model_env vec_exp ~fn ~fn_typ:(Typ.mk_ptr elt_typ) mem
let set_size {location} locs new_size mem =
Dom.Mem.transform_mem locs mem ~f:(fun v ->
Dom.Val.set_array_length location ~length:new_size v )
(* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
let constructor_size elt_typ {exp= vec_exp; typ= vec_typ} size_exp =
let {exec= malloc_exec; check} = malloc ~can_be_zero:true size_exp in
let exec ({pname; caller_pname; node_hash; integer_type_widths; location} as model_env)
~ret:((id, _) as ret) mem =
let mem = malloc_exec model_env ~ret mem in
let vec_locs = Sem.eval_locs vec_exp mem in
let deref_of_vec =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
~represents_multiple_values:false
|> Loc.of_allocsite
in
let array_v =
Sem.eval integer_type_widths (Exp.Var id) mem
|> Dom.Val.add_assign_trace_elem location vec_locs
in
mem
|> Dom.Mem.update_mem vec_locs (Dom.Val.of_loc deref_of_vec)
|> Dom.Mem.add_heap (append_field deref_of_vec ~vec_typ ~elt_typ) array_v
in
{exec; check}
(* The (1) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
let constructor_empty elt_typ vec = constructor_size elt_typ vec Exp.zero
(* The (5) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
let constructor_copy elt_typ {exp= vec_exp; typ= vec_typ} src_exp =
let exec ({integer_type_widths} as model_env) ~ret:_ mem =
let vec_locs, traces =
let v = Sem.eval integer_type_widths vec_exp mem in
(Dom.Val.get_all_locs v, Dom.Val.get_traces v)
in
let deref_of_vec = append_fields vec_locs ~vec_typ ~elt_typ in
let fn = BufferOverrunField.cpp_vector_elem ~vec_typ in
mem
|> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec)
|> ArrObjCommon.copy_constructor model_env deref_of_vec ~fn ~fn_typ:(Typ.mk_ptr elt_typ)
src_exp
in
{exec; check= no_check}
(* The (10) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
let constructor_initializer_list elt_typ {exp= vec_exp; typ= vec_typ} lst_exp =
let exec {pname; caller_pname; node_hash; location} ~ret:_ mem =
let arr_blk =
let internal_locs =
Sem.eval_locs lst_exp mem |> PowLoc.append_field ~fn:BoField.cpp_collection_internal_array
in
Dom.Mem.find_set internal_locs mem |> Dom.Val.get_array_blk
in
let deref_of_vec =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
~represents_multiple_values:false
|> Loc.of_allocsite
in
let mem =
let vec_locs = Sem.eval_locs vec_exp mem in
Dom.Mem.update_mem vec_locs (Dom.Val.of_loc deref_of_vec) mem
in
let vec_arr_ploc = append_field deref_of_vec ~vec_typ ~elt_typ |> PowLoc.singleton in
let traces = Trace.Set.singleton location ArrayDeclaration in
let arr_as =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
~represents_multiple_values:true
in
let v =
Dom.Val.of_c_array_alloc arr_as ~stride:None ~offset:Itv.zero
~size:(ArrayBlk.get_size arr_blk) ~traces
in
let vec_elt_locs = arr_as |> Loc.of_allocsite |> PowLoc.singleton in
let lst_elem_v = Dom.Mem.find_set (ArrayBlk.get_pow_loc arr_blk) mem in
mem |> Dom.Mem.strong_update vec_arr_ploc v |> Dom.Mem.update_mem vec_elt_locs lst_elem_v
in
{exec; check= no_check}
let at elt_typ {exp= vec_exp; typ= vec_typ} index_exp =
ArrObjCommon.at vec_exp
~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)
~fn_typ:(Typ.mk_ptr elt_typ) index_exp
let empty elt_typ vec_arg =
let exec model_env ~ret:(id, _) mem =
let deref_of_vec = deref_of model_env elt_typ vec_arg mem in
let array_v = Dom.Mem.find_set deref_of_vec mem in
let traces = Dom.Val.get_traces array_v in
let size = ArrayBlk.get_size (Dom.Val.get_array_blk array_v) in
let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in
let mem = model_by_value empty id mem in
match PowLoc.is_singleton_or_more deref_of_vec with
| IContainer.Singleton loc ->
Dom.Mem.load_empty_alias id loc mem
| IContainer.(Empty | More) ->
mem
in
{exec; check= no_check}
let data elt_typ vec_arg =
let exec model_env ~ret:(id, _) mem =
let arr = Dom.Mem.find_set (deref_of model_env elt_typ vec_arg mem) mem in
model_by_value arr id mem
in
{exec; check= no_check}
let add_n_element ~n elt_typ vec_arg elt_exp =
let exec ({integer_type_widths} as model_env) ~ret:_ mem =
let arr_locs = deref_of model_env elt_typ vec_arg mem in
let mem =
let new_size =
Sem.eval integer_type_widths n mem
|> Dom.Val.plus_a (Sem.eval_array_locs_length arr_locs mem)
in
set_size model_env arr_locs new_size mem
in
let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in
let elt_v = Dom.Mem.find_set (Sem.eval_locs elt_exp mem) mem in
Dom.Mem.update_mem elt_locs elt_v mem
in
{exec; check= no_check}
let push_back = add_n_element ~n:Exp.one
let insert_n elt_typ vec_arg n elt_exp = add_n_element ~n elt_typ vec_arg elt_exp
let insert_initializer_list elt_typ vec_arg lst_exp =
let exec model_env ~ret:_ mem =
let arr_locs = deref_of model_env elt_typ vec_arg mem in
let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in
let internal_arr =
let internal_array_locs =
Sem.eval_locs lst_exp mem |> PowLoc.append_field ~fn:BoField.cpp_collection_internal_array
in
Dom.Mem.find_set internal_array_locs mem
in
let arr_blk = Dom.Val.get_array_blk internal_arr in
let lst_elet = Dom.Mem.find_set (ArrayBlk.get_pow_loc arr_blk) mem in
let add_cnt = arr_blk |> ArrayBlk.get_size |> Dom.Val.of_itv in
let new_size = add_cnt |> Dom.Val.plus_a (Sem.eval_array_locs_length arr_locs mem) in
mem |> set_size model_env arr_locs new_size |> Dom.Mem.update_mem elt_locs lst_elet
in
{exec; check= no_check}
let size elt_typ {exp= vec_exp; typ= vec_typ} =
let exec =
ArrObjCommon.size_exec vec_exp
~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)
~fn_typ:(Typ.mk_ptr elt_typ)
in
{exec; check= no_check}
let resize elt_typ vec_arg size_exp =
let exec ({integer_type_widths} as model_env) ~ret:_ mem =
let arr_locs = deref_of model_env elt_typ vec_arg mem in
let new_size = Sem.eval integer_type_widths size_exp mem in
set_size model_env arr_locs new_size mem
in
{exec; check= no_check}
module Iterator = struct
let end_ elt_typ vec temp_exp = Iterator.end_ ~size_exec:(size elt_typ vec).exec temp_exp
end
end
module Split = struct
let std_vector model_env ~adds_at_least_one ({typ= vector_typ} as vec_arg) mem =
match vector_typ with
| Typ.
{ desc=
Tptr
( {desc= Tstruct (CppClass {template_spec_info= Template {args= TType elt_typ :: _}})}
, _ ) } ->
let arr_locs = StdVector.deref_of model_env elt_typ vec_arg mem in
let size = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in
StdVector.set_size model_env arr_locs size mem
| _ ->
Logging.d_printfln_escaped "Could not find element type of vector" ;
mem
end
module Boost = struct
module Split = struct
let std_vector vector_arg =
let exec model_env ~ret:_ mem =
Split.std_vector model_env ~adds_at_least_one:true vector_arg mem
in
{exec; check= no_check}
end
end
module Folly = struct
module Split = struct
let std_vector vector_arg ignore_empty_opt =
let exec ({integer_type_widths} as model_env) ~ret:_ mem =
let adds_at_least_one =
match ignore_empty_opt with
| Some ignore_empty_exp ->
Sem.eval integer_type_widths ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false
| None ->
(* default: ignore_empty is false *)
true
in
Split.std_vector model_env ~adds_at_least_one vector_arg mem
in
{exec; check= no_check}
end
end
module StdBasicString = struct
let constructor_from_char_ptr char_typ {exp= tgt_exp; typ= tgt_typ} src ~len_opt =
let exec ({pname; caller_pname; node_hash} as model_env) ~ret mem =
let mem =
Option.value_map len_opt ~default:mem ~f:(fun len ->
let {exec= malloc_exec} = malloc ~can_be_zero:true len in
malloc_exec model_env ~ret mem )
in
let tgt_locs = Sem.eval_locs tgt_exp mem in
let tgt_deref =
let allocsite =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
~represents_multiple_values:false
in
PowLoc.singleton (Loc.of_allocsite allocsite)
in
let mem =
Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Trace.Set.bottom tgt_deref) mem
in
let fn = BufferOverrunField.cpp_vector_elem ~vec_typ:tgt_typ in
ArrObjCommon.constructor_from_char_ptr model_env tgt_deref src ~fn ~char_typ mem
in
let check ({location; integer_type_widths} as model_env) mem cond_set =
Option.value_map len_opt ~default:cond_set ~f:(fun len ->
let {check= malloc_check} = malloc ~can_be_zero:true len in
let cond_set = malloc_check model_env mem cond_set in
BoUtils.Check.lindex integer_type_widths ~array_exp:src ~index_exp:len ~last_included:true
mem location cond_set )
in
{exec; check}
(* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let constructor_from_char_ptr_with_len char_typ tgt_arg src len =
constructor_from_char_ptr char_typ tgt_arg src ~len_opt:(Some len)
(* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let constructor_from_char_ptr_without_len char_typ tgt_arg src =
constructor_from_char_ptr char_typ tgt_arg src ~len_opt:None
(* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
let copy_constructor = StdVector.constructor_copy
let empty = StdVector.empty
let length = StdVector.size
end
(** Java's integers are modeled with an indirection to a memory location that holds the actual
integer value *)
module JavaInteger = struct
let intValue exp =
let exec _ ~ret:(id, _) mem =
let powloc = Sem.eval_locs exp mem in
let v = if PowLoc.is_bot powloc then Dom.Val.Itv.top else Dom.Mem.find_set powloc mem in
model_by_value v id mem
in
{exec; check= no_check}
let valueOf exp =
let exec {pname; caller_pname; node_hash; location; integer_type_widths} ~ret:(id, _) mem =
let represents_multiple_values = false in
let int_allocsite =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:0 ~path:None
~represents_multiple_values
in
let v = Sem.eval integer_type_widths exp mem in
let int_loc = Loc.of_allocsite int_allocsite in
mem |> Dom.Mem.add_heap int_loc v
|> Dom.Mem.add_stack (Loc.of_id id)
( int_loc |> PowLoc.singleton
|> Dom.Val.of_pow_loc ~traces:Trace.(Set.singleton location JavaIntDecleration) )
in
{exec; check= no_check}
end
module type Lang = sig
val collection_internal_array_field : Fieldname.t
end
(* Abstract Collections are represented like arrays. But we don't care about the elements.
- when they are constructed, we set the size to 0
- each time we add an element, we increase the length of the array
- each time we delete an element, we decrease the length of the array *)
module AbstractCollection (Lang : Lang) = struct
let create_collection {pname; caller_pname; node_hash; location} ~ret:(id, _) mem ~length =
let represents_multiple_values = true in
let traces = Trace.(Set.singleton location ArrayDeclaration) in
let coll_allocsite =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
~represents_multiple_values
in
let internal_array =
let allocsite =
Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
~represents_multiple_values
in
Dom.Val.of_java_array_alloc allocsite ~length ~traces
in
let coll_loc = Loc.of_allocsite coll_allocsite in
let internal_array_loc = Loc.append_field coll_loc Lang.collection_internal_array_field in
mem
|> Dom.Mem.add_heap internal_array_loc internal_array
|> Dom.Mem.add_stack (Loc.of_id id) (coll_loc |> PowLoc.singleton |> Dom.Val.of_pow_loc ~traces)
let new_collection =
let exec = create_collection ~length:Itv.zero in
{exec; check= no_check}
let allocate size_exp =
let exec ({integer_type_widths} as env) ~ret mem =
let length = Sem.eval integer_type_widths size_exp mem |> Dom.Val.get_itv in
create_collection env ~ret mem ~length
in
{exec; check= no_check}