blob: 4242f8d6079a46636ed0f3feb2942f0ae15c6914 (
plain)
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
|
open import Basic_classes
open import Bool
open import Maybe
open import Num
open import Bitstring
open import Error
open import Missing_pervasives
open import Show
open import String
open import Elf_file1
open import Elf_header
open import Elf_section_header_table
open import Elf_types
type elf32_linking_file2 =
<| elf32_linking_file2_header : elf32_header
; elf32_linking_file2_body : bitstring
; elf32_linking_file2_section_header_table : elf32_section_header_table
|>
class (HasElf32LinkingFile2 'a)
val get_elf32_linking_file2 : 'a -> elf32_linking_file2
end
instance (HasElf32LinkingFile2 elf32_linking_file2)
let get_elf32_linking_file2 f2 = f2
end
instance (HasElf32File1 elf32_linking_file2)
let get_elf32_file1 f2 =
<| elf32_file1_header = f2.elf32_linking_file2_header;
elf32_file1_body = f2.elf32_linking_file2_body |>
end
instance (HasElf32Header elf32_linking_file2)
let get_elf32_header f2 = f2.elf32_linking_file2_header
end
instance (HasElf32SectionHeaderTable elf32_linking_file2)
let get_elf32_section_header_table f2 = Just f2.elf32_linking_file2_section_header_table
end
type elf64_linking_file2 =
<| elf64_linking_file2_header : elf64_header
; elf64_linking_file2_body : bitstring
; elf64_linking_file2_section_header_table : elf64_section_header_table
|>
class (HasElf64LinkingFile2 'a)
val get_elf64_linking_file2 : 'a -> elf64_linking_file2
end
instance (HasElf64LinkingFile2 elf64_linking_file2)
let get_elf64_linking_file2 f2 = f2
end
instance (HasElf64File1 elf64_linking_file2)
let get_elf64_file1 f2 =
<| elf64_file1_header = f2.elf64_linking_file2_header;
elf64_file1_body = f2.elf64_linking_file2_body |>
end
instance (HasElf64Header elf64_linking_file2)
let get_elf64_header f2 = f2.elf64_linking_file2_header
end
instance (HasElf64SectionHeaderTable elf64_linking_file2)
let get_elf64_section_header_table f2 = Just f2.elf64_linking_file2_section_header_table
end
val refine_elf32_file1 : elf32_file1 -> error elf32_linking_file2
let refine_elf32_file1 f1 =
if not (is_linkable_elf32_file1 f1) then
fail "refine_elf32_file1: not a linkable file"
else
let hdr = f1.elf32_file1_header in
let endian = get_elf32_header_endianness hdr in
let bs1 = f1.elf32_file1_body in
let sentries = nat_of_elf32_half hdr.elf32_shnum in
let sentry_size = nat_of_elf32_half hdr.elf32_shentsize * 8 in
let ssize = sentries * sentry_size in
if ssize = 0 then
fail "refine_elf32_file1: section header table not present"
else
let soffset = nat_of_elf32_off hdr.elf32_shoff * 8 in
let (_, scut) = partition soffset bs1 in
let (sexact, _) = partition ssize scut in
(* Bitstring irrelevant below as exact size used... *)
read_elf32_section_header_table ssize endian sexact >>= fun (sht, _) ->
return <| elf32_linking_file2_header = hdr;
elf32_linking_file2_body = bs1;
elf32_linking_file2_section_header_table = sht |>
val read_elf32_linking_file2 : bitstring -> error elf32_linking_file2
let read_elf32_linking_file2 bs0 =
read_elf32_file1 bs0 >>= refine_elf32_file1
val string_of_elf32_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf32_linking_file2 -> string
let string_of_elf32_linking_file2 hdr_bdl sht_bdl f2 =
unlines [
"\n*Type elf32_linking_file2:"
; "**Header:"
; string_of_elf32_header hdr_bdl f2.elf32_linking_file2_header
; "**Program header table:"
; string_of_elf32_section_header_table sht_bdl f2.elf32_linking_file2_section_header_table
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf32_linking_file2_body)
]
val refine_elf64_file1 : elf64_file1 -> error elf64_linking_file2
let refine_elf64_file1 f1 =
if not (is_linkable_elf64_file1 f1) then
fail "refine_elf64_file1: not a linkable file"
else
let hdr = f1.elf64_file1_header in
let endian = get_elf64_header_endianness hdr in
let bs1 = f1.elf64_file1_body in
let sentries = nat_of_elf64_half hdr.elf64_shnum in
let sentry_size = nat_of_elf64_half hdr.elf64_shentsize * 8 in
let ssize = sentries * sentry_size in
if ssize = 0 then
fail "refine_elf64_file1: section header table not present"
else
let soffset = nat_of_elf64_off hdr.elf64_shoff * 8 in
let (_, scut) = partition soffset bs1 in
let (sexact, _) = partition ssize scut in
(* Bitstring irrelevant below as exact size used... *)
read_elf64_section_header_table ssize endian sexact >>= fun (sht, _) ->
return <| elf64_linking_file2_header = hdr;
elf64_linking_file2_body = bs1;
elf64_linking_file2_section_header_table = sht |>
val read_elf64_linking_file2 : bitstring -> error elf64_linking_file2
let read_elf64_linking_file2 bs0 =
read_elf64_file1 bs0 >>= refine_elf64_file1
val string_of_elf64_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf64_linking_file2 -> string
let string_of_elf64_linking_file2 hdr_bdl sht_bdl f2 =
unlines [
"\n*Type elf64_linking_file2:"
; "**Header:"
; string_of_elf64_header hdr_bdl f2.elf64_linking_file2_header
; "**Program header table:"
; string_of_elf64_section_header_table sht_bdl f2.elf64_linking_file2_section_header_table
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf64_linking_file2_body)
]
|
