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
|
open import Basic_classes
open import Bool
open import Function
open import List
open import Maybe
open import Num
open import String
open import Elf_types
open import Endianness
open import Bitstring
open import Error
open import Missing_pervasives
open import Show
(** Segment types
*
* FIXME: Bug in Lem as Lem codebase uses [int] type throughout where [BigInt.t]
* is really needed, hence chokes on huge constants below, which is why they are
* written in the way that they are.
*)
(** Unused array element. All other members of the structure are undefined. *)
let elf_pt_null : nat = 0
(** A loadable segment. *)
let elf_pt_load : nat = 1
(** Dynamic linking information. *)
let elf_pt_dynamic : nat = 2
(** Specifies the location and size of a null-terminated path name to be used to
* invoke an interpreter.
*)
let elf_pt_interp : nat = 3
(** Specifies location and size of auxiliary information. *)
let elf_pt_note : nat = 4
(** Reserved but with unspecified semantics. If the file contains a segment of
* this type then it is to be regarded as non-conformant with the ABI.
*)
let elf_pt_shlib : nat = 5
(** Specifies the location and size of the program header table. *)
let elf_pt_phdr : nat = 6
(** Specifies the thread local storage (TLS) template. Need not be supported. *)
let elf_pt_tls : nat = 7
(** Start of reserved indices for operating system specific semantics. *)
let elf_pt_loos : nat = 128 * 128 * 128 * 256 * 3 (* 1610612736 (* 0x60000000 *) *)
(** End of reserved indices for operating system specific semantics. *)
let elf_pt_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *)
(** Start of reserved indices for processor specific semantics. *)
let elf_pt_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *)
(** End of reserved indices for processor specific semantics. *)
let elf_pt_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *)
(** [string_of_elf_segment_type os proc st] produces a string representation of
* the coding of an ELF segment type [st] using [os] and [proc] to render OS-
* and processor-specific codings.
*)
val string_of_elf_segment_type : (nat -> string) -> (nat -> string) -> nat -> string
let string_of_elf_segment_type os proc pt =
if pt = elf_pt_null then
"PT_NULL"
else if pt = elf_pt_load then
"PT_LOAD"
else if pt = elf_pt_dynamic then
"PT_DYNAMIC"
else if pt = elf_pt_interp then
"PT_INTERP"
else if pt = elf_pt_note then
"PT_NOTE"
else if pt = elf_pt_shlib then
"PT_SHLIB"
else if pt = elf_pt_phdr then
"PT_PHDR"
else if pt = elf_pt_tls then
"PT_TLS"
else if pt >= elf_pt_loos && pt <= elf_pt_hios then
os pt
else if pt >= elf_pt_loproc && pt <= elf_pt_hiproc then
proc pt
else
"Undefined or invalid segment type"
(** Program header table entry type *)
(** Type [elf32_program_header_table_entry] encodes a program header table entry
* for 32-bit platforms. Each entry describes a segment in an executable or
* shared object file.
*)
type elf32_program_header_table_entry =
<| elf32_p_type : elf32_word (** Type of the segment *)
; elf32_p_offset : elf32_off (** Offset from beginning of file for segment *)
; elf32_p_vaddr : elf32_addr (** Virtual address for segment in memory *)
; elf32_p_paddr : elf32_addr (** Physical address for segment *)
; elf32_p_filesz : elf32_word (** Size of segment in file, in bytes *)
; elf32_p_memsz : elf32_word (** Size of segment in memory image, in bytes *)
; elf32_p_flags : elf32_word (** Segment flags *)
; elf32_p_align : elf32_word (** Segment alignment memory for memory and file *)
|>
(** Type [elf64_program_header_table_entry] encodes a program header table entry
* for 64-bit platforms. Each entry describes a segment in an executable or
* shared object file.
*)
type elf64_program_header_table_entry =
<| elf64_p_type : elf64_word (** Type of the segment *)
; elf64_p_flags : elf64_word (** Segment flags *)
; elf64_p_offset : elf64_off (** Offset from beginning of file for segment *)
; elf64_p_vaddr : elf64_addr (** Virtual address for segment in memory *)
; elf64_p_paddr : elf64_addr (** Physical address for segment *)
; elf64_p_filesz : elf64_xword (** Size of segment in file, in bytes *)
; elf64_p_memsz : elf64_xword (** Size of segment in memory image, in bytes *)
; elf64_p_align : elf64_xword (** Segment alignment memory for memory and file *)
|>
(** [string_of_elf32_program_header_table_entry os proc et] produces a string
* representation of a 32-bit program header table entry using [os] and [proc]
* to render OS- and processor-specific entries.
*)
val string_of_elf32_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf32_program_header_table_entry -> string
let string_of_elf32_program_header_table_entry os proc entry =
unlines [
"\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf32_word entry.elf32_p_type)
; "\t" ^ "Offset: " ^ show entry.elf32_p_offset
; "\t" ^ "Virtual address: " ^ show entry.elf32_p_vaddr
; "\t" ^ "Physical address: " ^ show entry.elf32_p_paddr
; "\t" ^ "Segment size (bytes): " ^ show entry.elf32_p_filesz
; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf32_p_memsz
; "\t" ^ "Flags: " ^ show entry.elf32_p_flags
; "\t" ^ "Alignment: " ^ show entry.elf32_p_align
]
(** [string_of_elf64_program_header_table_entry os proc et] produces a string
* representation of a 64-bit program header table entry using [os] and [proc]
* to render OS- and processor-specific entries.
*)
val string_of_elf64_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf64_program_header_table_entry -> string
let string_of_elf64_program_header_table_entry os proc entry =
unlines [
"\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf64_word entry.elf64_p_type)
; "\t" ^ "Offset: " ^ show entry.elf64_p_offset
; "\t" ^ "Virtual address: " ^ show entry.elf64_p_vaddr
; "\t" ^ "Physical address: " ^ show entry.elf64_p_paddr
; "\t" ^ "Segment size (bytes): " ^ show entry.elf64_p_filesz
; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf64_p_memsz
; "\t" ^ "Flags: " ^ show entry.elf64_p_flags
; "\t" ^ "Alignment: " ^ show entry.elf64_p_align
]
(** [string_of_elf32_program_header_table_entry_default et] produces a string representation
* of table entry [et] where OS- and processor-specific entries are replaced with
* default strings.
*)
val string_of_elf32_program_header_table_entry_default : elf32_program_header_table_entry -> string
let string_of_elf32_program_header_table_entry_default =
string_of_elf32_program_header_table_entry
(const "*Default OS specific print*")
(const "*Default processor specific print*")
(** [string_of_elf64_program_header_table_entry_default et] produces a string representation
* of table entry [et] where OS- and processor-specific entries are replaced with
* default strings.
*)
val string_of_elf64_program_header_table_entry_default : elf64_program_header_table_entry -> string
let string_of_elf64_program_header_table_entry_default =
string_of_elf64_program_header_table_entry
(const "*Default OS specific print*")
(const "*Default processor specific print*")
instance (Show elf32_program_header_table_entry)
let show = string_of_elf32_program_header_table_entry_default
end
instance (Show elf64_program_header_table_entry)
let show = string_of_elf64_program_header_table_entry_default
end
(** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table
* entry from bitstring [bs0] assuming endianness [endian]. If [bs0] is larger
* than necessary, the excess is returned from the function, too.
*)
val read_elf32_program_header_table_entry : endianness -> bitstring -> error (elf32_program_header_table_entry * bitstring)
let read_elf32_program_header_table_entry endian bs =
read_elf32_word endian bs >>= fun (typ, bs) ->
read_elf32_off endian bs >>= fun (offset, bs) ->
read_elf32_addr endian bs >>= fun (vaddr, bs) ->
read_elf32_addr endian bs >>= fun (paddr, bs) ->
read_elf32_word endian bs >>= fun (filesz, bs) ->
read_elf32_word endian bs >>= fun (memsz, bs) ->
read_elf32_word endian bs >>= fun (flags, bs) ->
read_elf32_word endian bs >>= fun (align, bs) ->
return (<| elf32_p_type = typ; elf32_p_offset = offset;
elf32_p_vaddr = vaddr; elf32_p_paddr = paddr;
elf32_p_filesz = filesz; elf32_p_memsz = memsz;
elf32_p_flags = flags; elf32_p_align = align |>, bs)
val read_elf64_program_header_table_entry : endianness -> bitstring -> error (elf64_program_header_table_entry * bitstring)
let read_elf64_program_header_table_entry endian bs =
read_elf64_word endian bs >>= fun (typ, bs) ->
read_elf64_word endian bs >>= fun (flags, bs) ->
read_elf64_off endian bs >>= fun (offset, bs) ->
read_elf64_addr endian bs >>= fun (vaddr, bs) ->
read_elf64_addr endian bs >>= fun (paddr, bs) ->
read_elf64_xword endian bs >>= fun (filesz, bs) ->
read_elf64_xword endian bs >>= fun (memsz, bs) ->
read_elf64_xword endian bs >>= fun (align, bs) ->
return (<| elf64_p_type = typ; elf64_p_offset = offset;
elf64_p_vaddr = vaddr; elf64_p_paddr = paddr;
elf64_p_filesz = filesz; elf64_p_memsz = memsz;
elf64_p_flags = flags; elf64_p_align = align |>, bs)
(** Program header table type *)
(** Type [elf32_program_header_table] represents a program header table for 32-bit
* ELF files. A program header table is an array (implemented as a list, here)
* of program header table entries.
*)
type elf32_program_header_table =
list elf32_program_header_table_entry
class (HasElf32ProgramHeaderTable 'a)
val get_elf32_program_header_table : 'a -> maybe elf32_program_header_table
end
(** Type [elf64_program_header_table] represents a program header table for 64-bit
* ELF files. A program header table is an array (implemented as a list, here)
* of program header table entries.
*)
type elf64_program_header_table =
list elf64_program_header_table_entry
class (HasElf64ProgramHeaderTable 'a)
val get_elf64_program_header_table : 'a -> maybe elf64_program_header_table
end
(** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from
* bitstring [bs0] assuming endianness [endian]. The bitstring [bs0] is assumed
* to have exactly the correct size for the table. For internal use, only. Use
* [read_elf32_program_header_table] below instead.
*)
let rec read_elf32_program_header_table' endian bs0 =
if length bs0 = 0 then
return []
else
read_elf32_program_header_table_entry endian bs0 >>= fun (entry, bs1) ->
read_elf32_program_header_table' endian bs1 >>= fun tail ->
return (entry::tail)
(** [read_elf64_program_header_table' endian bs0] reads an ELF64 program header table from
* bitstring [bs0] assuming endianness [endian]. The bitstring [bs0] is assumed
* to have exactly the correct size for the table. For internal use, only. Use
* [read_elf32_program_header_table] below instead.
*)
let rec read_elf64_program_header_table' endian bs0 =
if length bs0 = 0 then
return []
else
read_elf64_program_header_table_entry endian bs0 >>= fun (entry, bs1) ->
read_elf64_program_header_table' endian bs1 >>= fun tail ->
return (entry::tail)
(** [read_elf32_program_header_table table_size endian bs0] reads an ELF32 program header
* table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
* This [table_size] argument should be equal to the number of entries in the
* table multiplied by the fixed entry size. Bitstring [bs0] may be larger than
* necessary, in which case the excess is returned.
*)
val read_elf32_program_header_table : nat -> endianness -> bitstring -> error (elf32_program_header_table * bitstring)
let read_elf32_program_header_table table_size endian bs0 =
let (eat, rest) = partition table_size bs0 in
read_elf32_program_header_table' endian eat >>= fun table ->
return (table, rest)
(** [read_elf64_program_header_table table_size endian bs0] reads an ELF64 program header
* table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
* This [table_size] argument should be equal to the number of entries in the
* table multiplied by the fixed entry size. Bitstring [bs0] may be larger than
* necessary, in which case the excess is returned.
*)
val read_elf64_program_header_table : nat -> endianness -> bitstring -> error (elf64_program_header_table * bitstring)
let read_elf64_program_header_table table_size endian bs0 =
let (eat, rest) = partition table_size bs0 in
read_elf64_program_header_table' endian eat >>= fun table ->
return (table, rest)
(** The [pht_print_bundle] type is used to tidy up other type signatures. Some of the
* top-level string_of_ functions require six or more functions passed to them,
* which quickly gets out of hand. This type is used to reduce that complexity.
* The first component of the type is an OS specific print function, the second is
* a processor specific print function.
*)
type pht_print_bundle = (nat -> string) * (nat -> string)
(** [string_of_elf32_program_header_table os proc tbl] produces a string representation
* of program header table [tbl] using [os] and [proc] to render OS- and processor-
* specific entries.
*)
val string_of_elf32_program_header_table : pht_print_bundle -> elf32_program_header_table -> string
let string_of_elf32_program_header_table (os, proc) tbl =
unlines (List.map (string_of_elf32_program_header_table_entry os proc) tbl)
(** [string_of_elf64_program_header_table os proc tbl] produces a string representation
* of program header table [tbl] using [os] and [proc] to render OS- and processor-
* specific entries.
*)
val string_of_elf64_program_header_table : pht_print_bundle -> elf64_program_header_table -> string
let string_of_elf64_program_header_table (os, proc) tbl =
unlines (List.map (string_of_elf64_program_header_table_entry os proc) tbl)
|
