Source file elf_dynamic.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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
(** [elf_dynamic] module exports types and definitions relating to the dynamic
* section and dynamic linking functionality of an ELF file.
*)
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_string
open Byte_sequence
open Endianness
open Error
open Show
open String_table
open Elf_file
open Elf_header
open Elf_relocation
open Elf_section_header_table
open Elf_program_header_table
open Elf_types_native_uint
(** Validity checks *)
(** [is_elf32_valid_program_header_table_for_dynamic_linking pht] checks whether
* a program header table [pht] is a valid program header table for an ELF file
* that will be potentially dynamically linked. Returns true if there is exactly
* one segment header of type [elf_pt_interp], i.e. contains a string pointing
* to the requested dynamic interpreter.
*)
let pht:bool=
(List.length (List.filter (fun x -> Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_p_type) elf_pt_interp) pht) = 1)
(** [is_elf64_valid_program_header_table_for_dynamic_linking pht] checks whether
* a program header table [pht] is a valid program header table for an ELF file
* that will be potentially dynamically linked. Returns true if there is exactly
* one segment header of type [elf_pt_interp], i.e. contains a string pointing
* to the requested dynamic interpreter.
*)
let pht:bool=
(List.length (List.filter (fun x -> Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_p_type) elf_pt_interp) pht) = 1)
(** Dynamic section entry *)
(** [dyn_union] represents the C-union type used in the definition of [elf32_dyn]
* and [elf64_dyn] types below. Some section tags correspond to entries where
* the fields are either unspecified or ignored, hence the presence of the
* [D_Ignored] constructor.
*)
type( 'a, 'b) dyn_union
= D_Val of 'a
| D_Ptr of 'b
| D_Ignored of byte_sequence0
(** [elf32_dyn] captures the notion of an ELF32 dynamic section entry.
* Specialises the [dyn_union] type above to using [elf32_word] values and
* [elf32_addr] pointers.
*)
type elf32_dyn =
{ elf32_dyn_tag : Int32.t (** The type of the entry. *)
; elf32_dyn_d_un : (Uint32_wrapper.uint32, Uint32_wrapper.uint32) dyn_union (** The value of the entry, stored as a union. *)
}
(** [elf64_dyn] captures the notion of an ELF32 dynamic section entry.
* Specialises the [dyn_union] type above to using [elf64_xword] values and
* [elf64_addr] pointers.
*)
type elf64_dyn =
{ elf64_dyn_tag : Int64.t (** The type of the entry. *)
; elf64_dyn_d_un : (Uint64_wrapper.uint64, Uint64_wrapper.uint64) dyn_union (** The value of the entry, stored as a union. *)
}
(** Dynamic section tags *)
(** [dt_null] marks the end of the dynamic array *)
let dt_null : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** [dt_needed] holds the string table offset of a string containing the name of
* a needed library.
*)
let dt_needed : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** [dt_pltrelsz] holds the size in bytes of relocation entries associated with
* the PLT.
*)
let dt_pltrelsz : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** [dt_pltgot] holds an address associated with the PLT or GOT. *)
let dt_pltgot : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** [dt_hash] holds the address of a symbol-table hash. *)
let dt_hash : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** [dt_strtab] holds the address of the string table. *)
let dt_strtab : Nat_big_num.num= ( (Nat_big_num.of_int 5))
(** [dt_symtab] holds the address of a symbol table. *)
let dt_symtab : Nat_big_num.num= ( (Nat_big_num.of_int 6))
(** [dt_rela] holds the address of a relocation table. *)
let dt_rela : Nat_big_num.num= ( (Nat_big_num.of_int 7))
(** [dt_relasz] holds the size in bytes of the relocation table. *)
let dt_relasz : Nat_big_num.num= ( (Nat_big_num.of_int 8))
(** [dt_relaent] holds the size in bytes of a relocation table entry. *)
let dt_relaent : Nat_big_num.num= ( (Nat_big_num.of_int 9))
(** [dt_strsz] holds the size in bytes of the string table. *)
let dt_strsz : Nat_big_num.num= ( (Nat_big_num.of_int 10))
(** [dt_syment] holds the size in bytes of a symbol table entry. *)
let dt_syment : Nat_big_num.num= ( (Nat_big_num.of_int 11))
(** [dt_init] holds the address of the initialisation function. *)
let dt_init : Nat_big_num.num= ( (Nat_big_num.of_int 12))
(** [dt_fini] holds the address of the finalisation function. *)
let dt_fini : Nat_big_num.num= ( (Nat_big_num.of_int 13))
(** [dt_soname] holds the string table offset of a string containing the shared-
* object name.
*)
let dt_soname : Nat_big_num.num= ( (Nat_big_num.of_int 14))
(** [dt_rpath] holds the string table offset of a string containing the library
* search path.
*)
let dt_rpath : Nat_big_num.num= ( (Nat_big_num.of_int 15))
(** [dt_symbolic] alters the linker's symbol resolution algorithm so that names
* are resolved first from the shared object file itself, rather than the
* executable file.
*)
let dt_symbolic : Nat_big_num.num= ( (Nat_big_num.of_int 16))
(** [dt_rel] is similar to [dt_rela] except its table has implicit addends. *)
let dt_rel : Nat_big_num.num= ( (Nat_big_num.of_int 17))
(** [dt_relsz] holds the size in bytes of the [dt_rel] relocation table. *)
let dt_relsz : Nat_big_num.num= ( (Nat_big_num.of_int 18))
(** [dt_relent] holds the size in bytes of a [dt_rel] relocation entry. *)
let dt_relent : Nat_big_num.num= ( (Nat_big_num.of_int 19))
(** [dt_pltrel] specifies the type of relocation entry to which the PLT refers. *)
let dt_pltrel : Nat_big_num.num= ( (Nat_big_num.of_int 20))
(** [dt_debug] is used for debugging and its purpose is not specified in the ABI.
* Programs using this entry are not ABI-conformant.
*)
let dt_debug : Nat_big_num.num= ( (Nat_big_num.of_int 21))
(** [dt_textrel] absence of this entry indicates that no relocation entry should
* cause a modification to a non-writable segment. Otherwise, if present, one
* or more relocation entries may request modifications to a non-writable
* segment.
*)
let dt_textrel : Nat_big_num.num= ( (Nat_big_num.of_int 22))
(** [dt_jmprel]'s member holds the address of relocation entries associated with
* the PLT.
*)
let dt_jmprel : Nat_big_num.num= ( (Nat_big_num.of_int 23))
(** [dt_bindnow] instructs the linker to process all relocations for the object
* containing the entry before transferring control to the program.
*)
let dt_bindnow : Nat_big_num.num= ( (Nat_big_num.of_int 24))
(** [dt_init_array] holds the address to the array of pointers to initialisation
* functions.
*)
let dt_init_array : Nat_big_num.num= ( (Nat_big_num.of_int 25))
(** [dt_fini_array] holds the address to the array of pointers to finalisation
* functions.
*)
let dt_fini_array : Nat_big_num.num= ( (Nat_big_num.of_int 26))
(** [dt_init_arraysz] holds the size in bytes of the array of pointers to
* initialisation functions.
*)
let dt_init_arraysz : Nat_big_num.num= ( (Nat_big_num.of_int 27))
(** [dt_fini_arraysz] holds the size in bytes of the array of pointers to
* finalisation functions.
*)
let dt_fini_arraysz : Nat_big_num.num= ( (Nat_big_num.of_int 28))
(** [dt_runpath] holds an offset into the string table holding a string containing
* the library search path.
*)
let dt_runpath : Nat_big_num.num= ( (Nat_big_num.of_int 29))
(** [dt_flags] holds flag values specific to the object being loaded. *)
let dt_flags : Nat_big_num.num= ( (Nat_big_num.of_int 30))
let dt_encoding : Nat_big_num.num= ( (Nat_big_num.of_int 32))
(** [dt_preinit_array] holds the address to the array of pointers of pre-
* initialisation functions.
*)
let dt_preinit_array : Nat_big_num.num= ( (Nat_big_num.of_int 32))
(** [dt_preinit_arraysz] holds the size in bytes of the array of pointers of
* pre-initialisation functions.
*)
let dt_preinit_arraysz : Nat_big_num.num= ( (Nat_big_num.of_int 33))
(** [dt_loos] and [dt_hios]: this inclusive range is reserved for OS-specific
* semantics.
*)
let dt_loos : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 805306374)))( (Nat_big_num.of_int 1)))
let dt_hios : Nat_big_num.num= ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939522048)))
(** [dt_loproc] and [dt_hiproc]: this inclusive range is reserved for processor
* specific semantics.
*)
let dt_loproc : Nat_big_num.num= ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524096)))
let dt_hiproc : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 1073741823)))( (Nat_big_num.of_int 1)))
(** [string_of_dynamic_tag so t os proc] produces a string-based representation of
* dynamic section tag [t]. For tag values between LO_OS and HI_OS [os] is
* used to produce the resulting value. For tag values between LO_PROC and
* HI_PROC [proc] is used to produce the resulting value. Boolean flag [so]
* indicates whether the flag in question is derived from a shared object file,
* which alters the printing of ENCODING and PRE_INITARRAY flags.
*)
let string_of_dynamic_tag shared_object tag os_additional_ranges os proc:string=
(if Nat_big_num.equal tag dt_null then
"NULL"
else if Nat_big_num.equal tag dt_needed then
"NEEDED"
else if Nat_big_num.equal tag dt_pltrelsz then
"PLTRELSZ"
else if Nat_big_num.equal tag dt_pltgot then
"PLTGOT"
else if Nat_big_num.equal tag dt_hash then
"HASH"
else if Nat_big_num.equal tag dt_strtab then
"STRTAB"
else if Nat_big_num.equal tag dt_symtab then
"SYMTAB"
else if Nat_big_num.equal tag dt_rela then
"RELA"
else if Nat_big_num.equal tag dt_relasz then
"RELASZ"
else if Nat_big_num.equal tag dt_relaent then
"RELAENT"
else if Nat_big_num.equal tag dt_strsz then
"STRSZ"
else if Nat_big_num.equal tag dt_syment then
"SYMENT"
else if Nat_big_num.equal tag dt_init then
"INIT"
else if Nat_big_num.equal tag dt_fini then
"FINI"
else if Nat_big_num.equal tag dt_soname then
"SONAME"
else if Nat_big_num.equal tag dt_rpath then
"RPATH"
else if Nat_big_num.equal tag dt_symbolic then
"SYMBOLIC"
else if Nat_big_num.equal tag dt_rel then
"REL"
else if Nat_big_num.equal tag dt_relsz then
"RELSZ"
else if Nat_big_num.equal tag dt_relent then
"RELENT"
else if Nat_big_num.equal tag dt_pltrel then
"PLTREL"
else if Nat_big_num.equal tag dt_debug then
"DEBUG"
else if Nat_big_num.equal tag dt_textrel then
"TEXTREL"
else if Nat_big_num.equal tag dt_jmprel then
"JMPREL"
else if Nat_big_num.equal tag dt_bindnow then
"BIND_NOW"
else if Nat_big_num.equal tag dt_init_array then
"INIT_ARRAY"
else if Nat_big_num.equal tag dt_fini_array then
"FINI_ARRAY"
else if Nat_big_num.equal tag dt_init_arraysz then
"INIT_ARRAYSZ"
else if Nat_big_num.equal tag dt_fini_arraysz then
"FINI_ARRAYSZ"
else if Nat_big_num.equal tag dt_runpath then
"RUNPATH"
else if Nat_big_num.equal tag dt_flags then
"FLAGS"
else if Nat_big_num.equal tag dt_encoding then
if not shared_object then
"ENCODING"
else
"PREINIT_ARRAY"
else if Nat_big_num.equal tag dt_preinit_arraysz then
"PREINIT_ARRAYSZ"
else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
proc tag
else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
os tag
else if os_additional_ranges tag then
os tag
else
"Invalid dynamic section tag")
(** [tag_correspondence] is a type used to emulate the functionality of a C-union
* in Lem. The type records whether the union should be interpreted as a value,
* a pointer, or a "do not care" value. An accompanying function will map a
* dynamic section tag to a [tag_correspondence], so that transcription functions
* know how to properly use the [dyn_union] value in a dynamic section entry.
*)
type tag_correspondence
= C_Val (** [dyn_union] should be interpreted as a value. *)
| C_Ptr (** [dyn_union] should be interpreted as a pointer. *)
| C_Ignored (** [dyn_union] is irrelevant, so we do not care. *)
(** [tag_correspondence_of_tag tag os_additional_ranges os proc] produces a
* [tag_correspondence] value for a given dynamic tag, [tag]. Some tag values
* are reserved for interpretation by the OS or processor supplement (i.e. the
* ABI). We therefore also take in a predicate, [os_additional_ranges], that
* recognises when a tag is "special" for a given ABI, and a means of interpreting
* that tag, using [os] and [proc] functions.
*)
let tag_correspondence_of_tag shared_object tag os_additional_ranges os proc:(tag_correspondence)error=
(if Nat_big_num.equal tag dt_null then
return C_Ignored
else if Nat_big_num.equal tag dt_needed then
return C_Val
else if Nat_big_num.equal tag dt_pltrelsz then
return C_Val
else if Nat_big_num.equal tag dt_pltgot then
return C_Ptr
else if Nat_big_num.equal tag dt_hash then
return C_Ptr
else if Nat_big_num.equal tag dt_strtab then
return C_Ptr
else if Nat_big_num.equal tag dt_symtab then
return C_Ptr
else if Nat_big_num.equal tag dt_rela then
return C_Ptr
else if Nat_big_num.equal tag dt_relasz then
return C_Val
else if Nat_big_num.equal tag dt_relaent then
return C_Val
else if Nat_big_num.equal tag dt_strsz then
return C_Val
else if Nat_big_num.equal tag dt_syment then
return C_Val
else if Nat_big_num.equal tag dt_init then
return C_Ptr
else if Nat_big_num.equal tag dt_fini then
return C_Ptr
else if Nat_big_num.equal tag dt_soname then
return C_Val
else if Nat_big_num.equal tag dt_rpath then
return C_Val
else if Nat_big_num.equal tag dt_symbolic then
return C_Ignored
else if Nat_big_num.equal tag dt_rel then
return C_Ptr
else if Nat_big_num.equal tag dt_relsz then
return C_Val
else if Nat_big_num.equal tag dt_relent then
return C_Val
else if Nat_big_num.equal tag dt_pltrel then
return C_Val
else if Nat_big_num.equal tag dt_debug then
return C_Ptr
else if Nat_big_num.equal tag dt_textrel then
return C_Ignored
else if Nat_big_num.equal tag dt_jmprel then
return C_Ptr
else if Nat_big_num.equal tag dt_bindnow then
return C_Ignored
else if Nat_big_num.equal tag dt_init_array then
return C_Ptr
else if Nat_big_num.equal tag dt_fini_array then
return C_Ptr
else if Nat_big_num.equal tag dt_init_arraysz then
return C_Val
else if Nat_big_num.equal tag dt_fini_arraysz then
return C_Val
else if Nat_big_num.equal tag dt_runpath then
return C_Val
else if Nat_big_num.equal tag dt_flags then
return C_Val
else if Nat_big_num.equal tag dt_encoding then
if not shared_object then
return C_Ignored
else
return C_Ptr
else if Nat_big_num.equal tag dt_preinit_arraysz then
return C_Val
else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
proc tag
else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
os tag
else if os_additional_ranges tag then
os tag
else
fail ("tag_correspondence_of_tag: invalid dynamic section tag"))
(** [read_elf32_dyn endian bs0 so os_additional_ranges os proc] reads an [elf32_dyn]
* record from byte sequence [bs0], assuming endianness [endian]. As mentioned
* above some ABIs reserve additional tag values for their own purposes. These
* are recognised by the predicate [os_additional_ranges] and interpreted by
* the functions [os] and [proc]. Fails if the transcription of the record from
* [bs0] fails, or if [os] or [proc] fail.
*)
let read_elf32_dyn endian bs0 shared_object os_additional_ranges os proc:(elf32_dyn*Byte_sequence_wrapper.byte_sequence)error= (bind (read_elf32_sword endian bs0) (fun (tag0, bs1) ->
let tag = (Nat_big_num.abs (Nat_big_num.of_int32 tag0)) in bind (tag_correspondence_of_tag shared_object tag os_additional_ranges os proc) (fun corr ->
(match corr with
| C_Ptr -> bind (read_elf32_addr endian bs1) (fun (ptr, bs2) ->
return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ptr ptr) }, bs2))
| C_Val -> bind (read_elf32_word endian bs1) (fun (vl, bs2) ->
return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Val vl) }, bs2))
| C_Ignored ->
(match endian with
| Big -> bind (read_4_bytes_be bs1) (fun ((b1, b2, b3, b4), bs2) ->
let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4]]) in
return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ignored cut) }, bs2))
| Little -> bind (read_4_bytes_le bs1) (fun ((b1, b2, b3, b4), bs2) ->
let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4]]) in
return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ignored cut) }, bs2))
)
))))
(** [read_elf64_dyn endian bs0 os_additional_ranges os proc] reads an [elf64_dyn]
* record from byte sequence [bs0], assuming endianness [endian]. As mentioned
* above some ABIs reserve additional tag values for their own purposes. These
* are recognised by the predicate [os_additional_ranges] and interpreted by
* the functions [os] and [proc]. Fails if the transcription of the record from
* [bs0] fails, or if [os] or [proc] fail.
*)
let read_elf64_dyn endian bs0 shared_object os_additional_ranges os proc:(elf64_dyn*Byte_sequence_wrapper.byte_sequence)error= (bind (read_elf64_sxword endian bs0) (fun (tag0, bs1) ->
let tag = (Nat_big_num.abs (Nat_big_num.of_int64 tag0)) in bind (tag_correspondence_of_tag shared_object tag os_additional_ranges os proc) (fun corr ->
(match corr with
| C_Ptr -> bind (read_elf64_addr endian bs1) (fun (ptr, bs2) ->
return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ptr ptr) }, bs2))
| C_Val -> bind (read_elf64_xword endian bs1) (fun (vl, bs2) ->
return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Val vl) }, bs2))
| C_Ignored ->
(match endian with
| Big -> bind (read_8_bytes_be bs1) (fun ((b1, b2, b3, b4, b5, b6, b7, b8), bs2) ->
let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4; b5; b6; b7; b8]]) in
return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ignored cut) }, bs2))
| Little -> bind (read_8_bytes_le bs1) (fun ((b1, b2, b3, b4, b5, b6, b7, b8), bs2) ->
let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4; b5; b6; b7; b8]]) in
return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ignored cut) }, bs2))
)
))))
(** [obtain_elf32_dynamic_section_contents' endian bs0 os_additional_ranges os
* proc] exhaustively reads in [elf32_dyn] values from byte sequence [bs0],
* interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
* [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an
* [elf32_dyn] entry is not 0.
*)
let rec obtain_elf32_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc:((elf32_dyn)list)error=
(if Nat_big_num.equal (Byte_sequence.length0 bs0)( (Nat_big_num.of_int 0)) then
return []
else bind (read_elf32_dyn endian bs0 shared_object os_additional_ranges os proc) (fun (head, bs0) ->
if Nat_big_num.equal (Nat_big_num.of_int32 head.elf32_dyn_tag) ( dt_null) then
return [head]
else bind (obtain_elf32_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc) (fun tail ->
return (head::tail))))
(** [obtain_elf64_dynamic_section_contents' endian bs0 os_additional_ranges os
* proc] exhaustively reads in [elf64_dyn] values from byte sequence [bs0],
* interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
* [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an
* [elf64_dyn] entry is not 0.
*)
let rec obtain_elf64_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc:((elf64_dyn)list)error=
(if Nat_big_num.equal (Byte_sequence.length0 bs0)( (Nat_big_num.of_int 0)) then
return []
else bind (read_elf64_dyn endian bs0 shared_object os_additional_ranges os proc) (fun (head, bs0) ->
if Nat_big_num.equal (Nat_big_num.of_int64 head.elf64_dyn_tag) ( dt_null) then
return [head]
else bind (obtain_elf64_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc) (fun tail ->
return (head::tail))))
(** [obtain_elf32_dynamic_section_contents' f1 os_additional_ranges os
* proc bs0] exhaustively reads in [elf32_dyn] values from byte sequence [bs0],
* obtaining endianness and the section header table from [elf32_file] f1,
* interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
* [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an
* [elf32_dyn] entry is not 0.
*)
let obtain_elf32_dynamic_section_contents f1 os_additional_ranges os proc bs0:((elf32_dyn)list)error=
(let endian = (get_elf32_header_endianness f1.elf32_file_header) in
let sht = (f1.elf32_file_section_header_table) in
let shared_object = (is_elf32_shared_object_file f1.elf32_file_header) in
(match List.filter (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf32_sh_type) sht_dynamic) sht with
| [] -> fail "obtain_elf32_dynamic_section_contents: no SHT_DYNAMIC section header entries"
| [dyn] ->
let off = (Uint32_wrapper.to_bigint dyn.elf32_sh_offset) in
let siz = (Uint32_wrapper.to_bigint dyn.elf32_sh_size) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel ->
obtain_elf32_dynamic_section_contents' endian rel shared_object os_additional_ranges os proc)
| _ -> fail "obtain_elf32_dynamic_section_contents: multiple SHT_DYNAMIC section header entries"
))
(** [obtain_elf64_dynamic_section_contents' f1 os_additional_ranges os
* proc bs0] exhaustively reads in [elf64_dyn] values from byte sequence [bs0],
* obtaining endianness and the section header table from [elf64_file] f1,
* interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
* [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an
* [elf64_dyn] entry is not 0.
*)
let obtain_elf64_dynamic_section_contents f1 os_additional_ranges os proc bs0:((elf64_dyn)list)error=
(let endian = (get_elf64_header_endianness f1.elf64_file_header) in
let sht = (f1.elf64_file_section_header_table) in
let shared_object = (is_elf64_shared_object_file f1.elf64_file_header) in
(match List.filter (fun ent -> Nat_big_num.equal (Uint32_wrapper.to_bigint ent.elf64_sh_type) sht_dynamic) sht with
| [] -> fail "obtain_elf64_dynamic_section_contents: no SHT_DYNAMIC section header entries"
| [dyn] ->
let off = (Uint64_wrapper.to_bigint dyn.elf64_sh_offset) in
let siz = (Ml_bindings.nat_big_num_of_uint64 dyn.elf64_sh_size) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel ->
obtain_elf64_dynamic_section_contents' endian rel shared_object os_additional_ranges os proc)
| _ -> fail "obtain_elf64_dynamic_section_contents: multiple SHT_DYNAMIC section header entries"
))
(** DT Flags values *)
(** [df_origin] specific that the object being loaded may make reference to the
* $(ORIGIN) substitution string.
*)
let df_origin : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** [df_symbolic] changes the linker's symbol resolution algorithm, resolving
* symbols first from the shared object file rather than the executable file.
*)
let df_symbolic : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** [df_textrel] if this flag is not set then no relocation entry should cause
* modification to a non-writable segment.
*)
let df_textrel : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** [df_bindnow] if set this instructs the linker to process all relocation entries
* of the containing object before transferring control to the program.
*)
let df_bindnow : Nat_big_num.num= ( (Nat_big_num.of_int 8))
(** [df_static_tls] if set instructs the linker to reject all attempts to load
* the containing file dynamically.
*)
let df_static_tls : Nat_big_num.num= ( (Nat_big_num.of_int 16))
(** [check_flag] is a utility function for testing whether a flag is set.
* TODO: so simple it is probably unneccessary now.
*)
let check_flag m pos:bool= ( Nat_big_num.equal m pos)
(** [string_of_dt_flag f] produces a string-based representation of dynamic
* section flag [f].
*)
let string_of_dt_flag flag:string=
(if check_flag flag( (Nat_big_num.of_int 0)) then
"None"
else if check_flag flag df_origin then
"ORIGIN"
else if check_flag flag df_bindnow then
"BIND_NOW"
else if check_flag flag df_symbolic then
"SYMBOLIC"
else if check_flag flag df_textrel then
"TEXTREL"
else if check_flag flag df_static_tls then
"STATIC_TLS"
else if check_flag flag ( Nat_big_num.add df_bindnow df_static_tls) then
"BIND_NOW STATIC_TLS"
else if check_flag flag ( Nat_big_num.add df_static_tls df_symbolic) then
"SYMBOLIC STATIC_TLS"
else
"Invalid dynamic section flag")
(** [rel_type] represents the two types of relocation records potentially present
* in an ELF file: relocation, and relocation with addends.
*)
type rel_type
= Rel (** Plain relocation type. *)
| RelA (** Relocation with addends type. *)
(** [string_of_rel_type r] produces a string-based representation of [rel_type],
* [r].
*)
let string_of_rel_type r:string=
((match r with
| Rel -> "REL"
| RelA -> "RELA"
))
(** Type [dyn_value] represents the value of an ELF dynamic section entry. Values
* can represent various different types of objects (e.g. paths to libraries, or
* flags, or sizes of other entries in a file), and this type collates them all.
* Parameterised over two type variables so the type can be shared between ELF32
* and ELF64.
*)
type( 'addr, 'size) dyn_value
= Address of 'addr (** An address. *)
| Size of 'size (** A size (in bytes). *)
| FName of string (** A filename. *)
| SOName of string (** A shared object name. *)
| Path of string (** A path to some directory. *)
| RPath of string (** A "run path". *)
| RunPath of string (** A "run path". *)
| Library of string (** A library path. *)
| Flags1 of Nat_big_num.num (** Flags. *)
| Flags of Nat_big_num.num (** Flags. *)
| Numeric of Nat_big_num.num (** An uninterpreted numeric value. *)
| Checksum of Nat_big_num.num (** A checksum value *)
| RelType of rel_type (** A relocation entry type. *)
| Timestamp of Nat_big_num.num (** A timestamp value. *)
| Null (** A null (0) value. *)
| Ignored (** An ignored value. *)
(** [elf32_dyn_value] and [elf64_dyn_value] are specialisations of [dyn_value]
* fixing the correct types for the ['addr] and ['size] type variables.
*)
type elf32_dyn_value = (Uint32_wrapper.uint32, Uint32_wrapper.uint32) dyn_value
type elf64_dyn_value = (Uint64_wrapper.uint64, Uint64_wrapper.uint64) dyn_value
(** [get_string_table_of_elf32_dyn_section endian dyns sht bs0] searches through
* dynamic section entries [dyns] looking for one pointing to a string table, looks
* up the corresponding section header [sht] pointed to by that dynamic
* section entry, finds the section in [bs0] and decodes a string table from that
* section assuming endianness [endian]. May fail.
*)
let get_string_table_of_elf32_dyn_section endian dyns sht bs0:(string_table)error=
(let strtabs =
(List.filter (fun x -> Nat_big_num.equal
(Nat_big_num.of_int32 x.elf32_dyn_tag) ( dt_strtab)
) dyns)
in
(match strtabs with
| [strtab] ->
(match strtab.elf32_dyn_d_un with
| D_Val v -> fail "get_string_table_of_elf32_dyn_section: STRTAB must be a PTR"
| D_Ptr p ->
let sect =
(List.filter (fun s ->
(s.elf32_sh_addr = p) &&
(s.elf32_sh_type = Uint32_wrapper.of_bigint sht_strtab)
) sht)
in
(match sect with
| [] -> fail "get_string_table_of_elf32_dyn_section: no section entry with same address as STRTAB"
| [s] ->
let off = (Uint32_wrapper.to_bigint s.elf32_sh_offset) in
let siz = (Uint32_wrapper.to_bigint s.elf32_sh_size) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel ->
let strings = (Byte_sequence.string_of_byte_sequence rel) in
return (String_table.mk_string_table strings (Missing_pervasives.null_char)))
| _ -> fail "get_string_table_of_elf32_dyn_section: multiple section entries with same address as STRTAB"
)
| D_Ignored i -> fail "get_string_table_of_elf32_dyn_section: STRTAB must be a PTR"
)
| [] -> fail "get_string_table_of_elf32_dyn_section: no string table entry"
| _ -> fail "get_string_table_of_elf32_dyn_section: multiple string table entries"
))
(** [get_string_table_of_elf64_dyn_section endian dyns sht bs0] searches through
* dynamic section entries [dyns] looking for one pointing to a string table, looks
* up the corresponding section header [sht] pointed to by that dynamic
* section entry, finds the section in [bs0] and decodes a string table from that
* section assuming endianness [endian]. May fail.
*)
let get_string_table_of_elf64_dyn_section endian dyns sht bs0:(string_table)error=
(let strtabs =
(List.filter (fun x -> Nat_big_num.equal
(Nat_big_num.of_int64 x.elf64_dyn_tag) ( dt_strtab)
) dyns)
in
(match strtabs with
| [strtab] ->
(match strtab.elf64_dyn_d_un with
| D_Val v -> fail "get_string_table_of_elf64_dyn_section: STRTAB must be a PTR"
| D_Ptr p ->
let sect =
(List.filter (fun s ->
(s.elf64_sh_addr = p) &&
(s.elf64_sh_type = Uint32_wrapper.of_bigint sht_strtab)
) sht)
in
(match sect with
| [] -> fail "get_string_table_of_elf64_dyn_section: no section entry with same address as STRTAB"
| [s] ->
let off = (Uint64_wrapper.to_bigint s.elf64_sh_offset) in
let siz = (Ml_bindings.nat_big_num_of_uint64 s.elf64_sh_size) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel ->
let strings = (Byte_sequence.string_of_byte_sequence rel) in
return (String_table.mk_string_table strings Missing_pervasives.null_char))
| _ -> fail "get_string_table_of_elf64_dyn_section: multiple section entries with same address as STRTAB"
)
| D_Ignored i -> fail "get_string_table_of_elf64_dyn_section: STRTAB must be a PTR"
)
| [] -> fail "get_string_table_of_elf64_dyn_section: no string table entry"
| _ -> fail "get_string_table_of_elf64_dyn_section: multiple string table entries"
))
(** [get_value_of_elf32_dyn so dyn os_additional_ranges os proc stab] returns the value
* stored in a dynamic section entry [dyn], using [os_additional_ranges] and
* [os] to decode ABI-reserved tags. String table [stab] is used to correctly
* decode library and run paths, etc.
* May fail.
*)
let get_value_of_elf32_dyn shared_object dyn os_additional_ranges os proc stab:(((Uint32_wrapper.uint32),(Uint32_wrapper.uint32))dyn_value)error=
(let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in
if Nat_big_num.equal tag dt_null then
return Null
else if Nat_big_num.equal tag dt_needed then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: NEEDED must be a Val"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: NEEDED must be a Val"
) (fun off ->
let off = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
return (Library str)))
else if Nat_big_num.equal tag dt_pltrelsz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: PLTRELSZ must be a Val"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTRELSZ must be a Val"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_pltgot then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: PLTGOT must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTGOT must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_hash then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: HASH must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: HASH must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_strtab then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: STRTAB must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: STRTAB must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_symtab then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: SYMTAB must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SYMTAB must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_rela then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: RELA must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELA must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_relasz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELASZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELASZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_relaent then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELAENT must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELAENT must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_strsz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: STRSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: STRSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_syment then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: SYMENT must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SYMENT must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_init then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: INIT must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_fini then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: FINI must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_soname then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: SONAME must be a Val"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SONAME must be a Val"
) (fun off ->
let off = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
return (SOName str)))
else if Nat_big_num.equal tag dt_rpath then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RPATH must be a Val"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RPATH must be a Val"
) (fun off ->
let off = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
return (RPath str)))
else if Nat_big_num.equal tag dt_symbolic then
return Null
else if Nat_big_num.equal tag dt_rel then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: REL must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: REL must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_relsz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_relent then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELENT must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELENT must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_pltrel then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: PLTREL must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTREL must be a VAL"
) (fun r ->
if Nat_big_num.equal (Uint32_wrapper.to_bigint r) dt_rel then
return (RelType Rel)
else if Nat_big_num.equal (Uint32_wrapper.to_bigint r) dt_rela then
return (RelType RelA)
else
fail "get_value_of_elf32_dyn_entry: PLTREL neither REL nor RELA")
else if Nat_big_num.equal tag dt_debug then
return Null
else if Nat_big_num.equal tag dt_textrel then
return Null
else if Nat_big_num.equal tag dt_jmprel then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: JMPREL must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: JMPREL must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_bindnow then
return Ignored
else if Nat_big_num.equal tag dt_init_array then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAY must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAY must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_fini_array then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAY must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAY must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_init_arraysz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAYSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAYSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_fini_arraysz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAYSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAYSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_runpath then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RUNPATH must be a Val"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RUNPATH must be a Val"
) (fun off ->
let off = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
return (RunPath str)))
else if Nat_big_num.equal tag dt_flags then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: FLAGS must be a Val"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FLAGS must be a Val"
) (fun flags ->
return (Flags (Uint32_wrapper.to_bigint flags)))
else if Nat_big_num.equal tag dt_encoding then
if not shared_object then
return Ignored
else bind (match dyn.elf32_dyn_d_un with
| D_Val v -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAY must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAY must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_preinit_arraysz then bind (match dyn.elf32_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
) (fun sz ->
return (Checksum (Uint32_wrapper.to_bigint sz))) (** XXX: bug in readelf does not print this as a size! *)
else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
proc dyn stab
else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
os dyn stab
else if os_additional_ranges tag then
os dyn stab
else
fail "get_value_of_elf32_dyn: unrecognised tag type")
(** [get_value_of_elf64_dyn dyn os_additional_ranges os proc stab] returns the value
* stored in a dynamic section entry [dyn], using [os_additional_ranges] and
* [os] to decode ABI-reserved tags. String table [stab] is used to correctly
* decode library and run paths, etc.
* May fail.
*)
let get_value_of_elf64_dyn shared_object dyn os_additional_ranges os_dyn proc_dyn stab:(((Uint64_wrapper.uint64),(Uint64_wrapper.uint64))dyn_value)error=
(let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
if Nat_big_num.equal tag dt_null then
return Null
else if Nat_big_num.equal tag dt_needed then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: NEEDED must be a Val"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: NEEDED must be a Val"
) (fun off ->
let off = (Ml_bindings.nat_big_num_of_uint64 off) in bind (String_table.get_string_at off stab) (fun str ->
return (Library str)))
else if Nat_big_num.equal tag dt_pltrelsz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: PLTRELSZ must be a Val"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTRELSZ must be a Val"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_pltgot then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: PLTGOT must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTGOT must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_hash then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: HASH must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: HASH must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_strtab then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: STRTAB must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: STRTAB must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_symtab then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: SYMTAB must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SYMTAB must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_rela then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: RELA must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELA must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_relasz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELASZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELASZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_relaent then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELAENT must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELAENT must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_strsz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: STRSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: STRSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_syment then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: SYMENT must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SYMENT must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_init then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: INIT must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_fini then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: FINI must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_soname then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: SONAME must be a Val"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SONAME must be a Val"
) (fun off ->
let off = (Ml_bindings.nat_big_num_of_uint64 off) in bind (String_table.get_string_at off stab) (fun str ->
return (SOName str)))
else if Nat_big_num.equal tag dt_rpath then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RPATH must be a Val"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RPATH must be a Val"
) (fun off ->
let off = (Ml_bindings.nat_big_num_of_uint64 off) in bind (String_table.get_string_at off stab) (fun str ->
return (RPath str)))
else if Nat_big_num.equal tag dt_symbolic then
return Null
else if Nat_big_num.equal tag dt_rel then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: REL must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: REL must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_relsz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_relent then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELENT must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELENT must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_pltrel then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: PLTREL must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTREL must be a VAL"
) (fun r ->
if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 r) dt_rel then
return (RelType Rel)
else if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 r) dt_rela then
return (RelType RelA)
else
fail "get_value_of_elf64_dyn_entry: PLTREL neither REL nor RELA")
else if Nat_big_num.equal tag dt_debug then
return Null
else if Nat_big_num.equal tag dt_textrel then
return Null
else if Nat_big_num.equal tag dt_jmprel then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: JMPREL must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: JMPREL must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_bindnow then
return Ignored
else if Nat_big_num.equal tag dt_init_array then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAY must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAY must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_fini_array then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAY must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAY must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_init_arraysz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAYSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAYSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_fini_arraysz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAYSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAYSZ must be a VAL"
) (fun sz ->
return (Size sz))
else if Nat_big_num.equal tag dt_runpath then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RUNPATH must be a Val"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RUNPATH must be a Val"
) (fun off ->
let off = (Ml_bindings.nat_big_num_of_uint64 off) in bind (String_table.get_string_at off stab) (fun str ->
return (RunPath str)))
else if Nat_big_num.equal tag dt_flags then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: FLAGS must be a Val"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FLAGS must be a Val"
) (fun flags ->
return (Flags (Ml_bindings.nat_big_num_of_uint64 flags)))
else if Nat_big_num.equal tag dt_encoding then
if not shared_object then
return Ignored
else bind (match dyn.elf64_dyn_d_un with
| D_Val v -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAY must be a PTR"
| D_Ptr p -> return p
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAY must be a PTR"
) (fun ptr ->
return (Address ptr))
else if Nat_big_num.equal tag dt_preinit_arraysz then bind (match dyn.elf64_dyn_d_un with
| D_Val v -> return v
| D_Ptr p -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
| D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
) (fun sz ->
return (Checksum (Ml_bindings.nat_big_num_of_uint64 sz))) (** XXX: bug in readelf does not print this as a size! *)
else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
proc_dyn dyn stab
else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
os_dyn dyn stab
else if os_additional_ranges tag then
os_dyn dyn stab
else
fail "get_value_of_elf64_dyn: unrecognised tag type")