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
|
open import Maybe
open import Num
open import Elf_executable_file3
open import Elf_header
open import Elf_program_header_table
open import Elf_section_header_table
open import Elf_types
open import String_table
open import Bitstring
open import Error
open import Missing_pervasives
open import Show
open import String
(** Type [elf32_executable_file4] represents the lazy unfolding of a 32-bit ELF
* file where the header, program header table and optional section header table
* have been filled in, along with the section header string table, with all
* other data being left uninterpreted.
*)
type elf32_executable_file4 =
<| elf32_executable_file4_header : elf32_header (** The ELF header (mandatory) *)
; elf32_executable_file4_program_header_table : elf32_program_header_table (** The program header table (mandatory) *)
; elf32_executable_file4_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *)
; elf32_executable_file4_section_header_string_table : string_table
; elf32_executable_file4_body : bitstring (** Uninterpreted body *)
|>
class (HasElf32ExecutableFile4 'a)
val get_elf32_executable_file4 : 'a -> elf32_executable_file4
end
instance (HasElf32ExecutableFile4 elf32_executable_file4)
let get_elf32_executable_file4 f4 = f4
end
instance (HasElf32ExecutableFile3 elf32_executable_file4)
let get_elf32_executable_file3 f4 =
<| elf32_executable_file3_header = f4.elf32_executable_file4_header;
elf32_executable_file3_program_header_table = f4.elf32_executable_file4_program_header_table;
elf32_executable_file3_section_header_table = f4.elf32_executable_file4_section_header_table;
elf32_executable_file3_body = f4.elf32_executable_file4_body |>
end
instance (HasElf32Header elf32_executable_file4)
let get_elf32_header f4 = f4.elf32_executable_file4_header
end
instance (HasElf32ProgramHeaderTable elf32_executable_file4)
let get_elf32_program_header_table f4 =
Just (f4.elf32_executable_file4_program_header_table)
end
instance (HasElf32SectionHeaderTable elf32_executable_file4)
let get_elf32_section_header_table f4 =
f4.elf32_executable_file4_section_header_table
end
instance (HasElf32SectionHeaderStringTable elf32_executable_file4)
let get_elf32_section_header_string_table f4 =
f4.elf32_executable_file4_section_header_string_table
end
(** Type [elf64_executable_file4] represents the lazy unfolding of a 64-bit ELF
* file where the header, program header table and optional section header table
* have been filled in, along with the section header string table, with all
* other data being left uninterpreted.
*)
type elf64_executable_file4 =
<| elf64_executable_file4_header : elf64_header (** The ELF header (mandatory) *)
; elf64_executable_file4_program_header_table : elf64_program_header_table (** The program header table (mandatory) *)
; elf64_executable_file4_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *)
; elf64_executable_file4_section_header_string_table : string_table
; elf64_executable_file4_body : bitstring (** Uninterpreted body *)
|>
class (HasElf64ExecutableFile4 'a)
val get_elf64_executable_file4 : 'a -> elf64_executable_file4
end
instance (HasElf64ExecutableFile4 elf64_executable_file4)
let get_elf64_executable_file4 f4 = f4
end
instance (HasElf64ExecutableFile3 elf64_executable_file4)
let get_elf64_executable_file3 f4 =
<| elf64_executable_file3_header = f4.elf64_executable_file4_header;
elf64_executable_file3_program_header_table = f4.elf64_executable_file4_program_header_table;
elf64_executable_file3_section_header_table = f4.elf64_executable_file4_section_header_table;
elf64_executable_file3_body = f4.elf64_executable_file4_body |>
end
instance (HasElf64Header elf64_executable_file4)
let get_elf64_header f4 = f4.elf64_executable_file4_header
end
instance (HasElf64ProgramHeaderTable elf64_executable_file4)
let get_elf64_program_header_table f4 =
Just (f4.elf64_executable_file4_program_header_table)
end
instance (HasElf64SectionHeaderTable elf64_executable_file4)
let get_elf64_section_header_table f4 =
f4.elf64_executable_file4_section_header_table
end
instance (HasElf64SectionHeaderStringTable elf64_executable_file4)
let get_elf64_section_header_string_table f4 =
f4.elf64_executable_file4_section_header_string_table
end
(** [refine_elf32_executable_file3 f3] refines an elf32_executable_file3 [f3], adding the
* section header string table, to obtain an elf32_executable_file4. May fail if
* the offset stored in the ELF header indicating where the string table is stored is
* invalid.
*)
val refine_elf32_executable_file3 : elf32_executable_file3 -> error elf32_executable_file4
let refine_elf32_executable_file3 f3 =
let hdr = f3.elf32_executable_file3_header in
let pht = f3.elf32_executable_file3_program_header_table in
let sht = f3.elf32_executable_file3_section_header_table in
let bs0 = f3.elf32_executable_file3_body in
match sht with
| Nothing ->
return <| elf32_executable_file4_header = hdr;
elf32_executable_file4_program_header_table = pht;
elf32_executable_file4_section_header_table = Nothing;
elf32_executable_file4_section_header_string_table = String_table.empty;
elf32_executable_file4_body = bs0 |>
| Just sht ->
let idx = nat_of_elf32_half hdr.elf32_shstrndx in
let sect = List.index sht idx in
match sect with
| Nothing -> Fail "refine_elf32_executable_file3: invalid offset into section header table"
| Just sect ->
let offset = nat_of_elf32_off sect.elf32_sh_offset * 8 in
let size = nat_of_elf32_word sect.elf32_sh_size * 8 in
let (_, cut) = Bitstring.partition offset bs0 in
let (rel, _) = Bitstring.partition size cut in
let strings = Bitstring.string_of_bitstring rel in
return <| elf32_executable_file4_header = hdr;
elf32_executable_file4_program_header_table = pht;
elf32_executable_file4_section_header_table = Just sht;
elf32_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char;
elf32_executable_file4_body = bs0 |>
end
end
(** [refine_elf64_executable_file3 f3] refines an elf64_executable_file3 [f3], adding the
* section header string table, to obtain an elf64_executable_file4. May fail if
* the offset stored in the ELF header indicating where the string table is stored is
* invalid.
*)
val refine_elf64_executable_file3 : elf64_executable_file3 -> error elf64_executable_file4
let refine_elf64_executable_file3 f3 =
let hdr = f3.elf64_executable_file3_header in
let pht = f3.elf64_executable_file3_program_header_table in
let sht = f3.elf64_executable_file3_section_header_table in
let bs0 = f3.elf64_executable_file3_body in
match sht with
| Nothing ->
return <| elf64_executable_file4_header = hdr;
elf64_executable_file4_program_header_table = pht;
elf64_executable_file4_section_header_table = Nothing;
elf64_executable_file4_section_header_string_table = String_table.empty;
elf64_executable_file4_body = bs0 |>
| Just sht ->
let idx = nat_of_elf64_half hdr.elf64_shstrndx in
let sect = List.index sht idx in
match sect with
| Nothing -> fail "refine_elf32_executable_file3: invalid offset into section header table"
| Just sect ->
let offset = nat_of_elf64_off sect.elf64_sh_offset * 8 in
let size = nat_of_elf64_xword sect.elf64_sh_size * 8 in
let (_, cut) = Bitstring.partition offset bs0 in
let (rel, _) = Bitstring.partition size cut in
let strings = Bitstring.string_of_bitstring rel in
return <| elf64_executable_file4_header = hdr;
elf64_executable_file4_program_header_table = pht;
elf64_executable_file4_section_header_table = Just sht;
elf64_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char;
elf64_executable_file4_body = bs0 |>
end
end
(** [read_elf32_executable_file4 bs0] reads an [elf32_executable_file4] in from
* bitstring [bs0].
*)
val read_elf32_executable_file4 : bitstring -> error elf32_executable_file4
let read_elf32_executable_file4 bs0 =
read_elf32_executable_file3 bs0 >>= refine_elf32_executable_file3
(** [read_elf64_executable_file4 bs0] reads an [elf64_executable_file4] in from
* bitstring [bs0].
*)
val read_elf64_executable_file4 : bitstring -> error elf64_executable_file4
let read_elf64_executable_file4 bs0 =
read_elf64_executable_file3 bs0 >>= refine_elf64_executable_file3
(** [string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string
* based representation of elf32_executable_file4 [f4].
*)
val string_of_elf32_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file4 -> string
let string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4 =
let sht =
match f4.elf32_executable_file4_section_header_table with
| Nothing -> "\tNo section header table present"
| Just sht -> string_of_elf32_section_header_table' sht_bdl f4.elf32_executable_file4_section_header_string_table sht
end
in
unlines [
"\n*Type elf32_executable_file4"
; "**Header"
; string_of_elf32_header hdr_bdl f4.elf32_executable_file4_header
; "**Program header table:"
; string_of_elf32_program_header_table pht_bdl f4.elf32_executable_file4_program_header_table
; "**Section header table:"
; sht
; "**Section header string table:"
; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf32_executable_file4_section_header_string_table))
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf32_executable_file4_body)
]
(** [string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string
* based representation of elf64_executable_file4 [f4].
*)
val string_of_elf64_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file4 -> string
let string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4 =
let sht =
match f4.elf64_executable_file4_section_header_table with
| Nothing -> "\tNo section header table present"
| Just sht -> string_of_elf64_section_header_table' sht_bdl f4.elf64_executable_file4_section_header_string_table sht
end
in
unlines [
"\n*Type elf64_executable_file4"
; "**Header"
; string_of_elf64_header hdr_bdl f4.elf64_executable_file4_header
; "**Program header table:"
; string_of_elf64_program_header_table pht_bdl f4.elf64_executable_file4_program_header_table
; "**Section header table:"
; sht
; "**Section header string table:"
; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf64_executable_file4_section_header_string_table))
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf64_executable_file4_body)
]
|
