blob: 07a2fdc18927a77cd88de017525158fc99045c92 (
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
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
|
open import Basic_classes
open import Num
open import Maybe
open import String
open import Elf_executable_file2
open import Elf_header
open import Elf_types
open import Elf_section_header_table
open import Elf_program_header_table
open import Bitstring
open import Error
open import Missing_pervasives
open import Show
(** Type [elf32_executable_file3] 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, with all other data being left uninterpreted.
*)
type elf32_executable_file3 =
<| elf32_executable_file3_header : elf32_header (** The ELF header (mandatory) *)
; elf32_executable_file3_program_header_table : elf32_program_header_table (** The program header table (mandatory) *)
; elf32_executable_file3_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *)
; elf32_executable_file3_body : bitstring (** Uninterpreted body *)
|>
class (HasElf32ExecutableFile3 'a)
val get_elf32_executable_file3 : 'a -> elf32_executable_file3
end
instance (HasElf32ExecutableFile3 elf32_executable_file3)
let get_elf32_executable_file3 f3 = f3
end
instance (HasElf32ExecutableFile2 elf32_executable_file3)
let get_elf32_executable_file2 f3 =
<| elf32_executable_file2_header = f3.elf32_executable_file3_header;
elf32_executable_file2_program_header_table = f3.elf32_executable_file3_program_header_table;
elf32_executable_file2_body = f3.elf32_executable_file3_body |>
end
instance (HasElf32Header elf32_executable_file3)
let get_elf32_header f3 = f3.elf32_executable_file3_header
end
instance (HasElf32ProgramHeaderTable elf32_executable_file3)
let get_elf32_program_header_table f3 =
Just (f3.elf32_executable_file3_program_header_table)
end
instance (HasElf32SectionHeaderTable elf32_executable_file3)
let get_elf32_section_header_table f3 =
f3.elf32_executable_file3_section_header_table
end
(** Type [elf64_executable_file3] 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, with all other data being left uninterpreted.
*)
type elf64_executable_file3 =
<| elf64_executable_file3_header : elf64_header (** The ELF header (mandatory) *)
; elf64_executable_file3_program_header_table : elf64_program_header_table (** The program header table (mandatory) *)
; elf64_executable_file3_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *)
; elf64_executable_file3_body : bitstring (** Uninterpreted body *)
|>
class (HasElf64ExecutableFile3 'a)
val get_elf64_executable_file3 : 'a -> elf64_executable_file3
end
instance (HasElf64ExecutableFile3 elf64_executable_file3)
let get_elf64_executable_file3 f3 = f3
end
instance (HasElf64ExecutableFile2 elf64_executable_file3)
let get_elf64_executable_file2 f3 =
<| elf64_executable_file2_header = f3.elf64_executable_file3_header;
elf64_executable_file2_program_header_table = f3.elf64_executable_file3_program_header_table;
elf64_executable_file2_body = f3.elf64_executable_file3_body |>
end
instance (HasElf64Header elf64_executable_file3)
let get_elf64_header f3 = f3.elf64_executable_file3_header
end
instance (HasElf64ProgramHeaderTable elf64_executable_file3)
let get_elf64_program_header_table f3 =
Just (f3.elf64_executable_file3_program_header_table)
end
instance (HasElf64SectionHeaderTable elf64_executable_file3)
let get_elf64_section_header_table f3 =
f3.elf64_executable_file3_section_header_table
end
(** [refine_elf32_executable_file2 f2] refines an elf32_executable_file2 [f2] into
* an elf32_executable_file3 by adding the optional section header table.
*)
val refine_elf32_executable_file2 : elf32_executable_file2 -> error elf32_executable_file3
let refine_elf32_executable_file2 f2 =
let hdr = f2.elf32_executable_file2_header in
let pht = f2.elf32_executable_file2_program_header_table in
let endian = get_elf32_header_endianness hdr in
let bs1 = f2.elf32_executable_file2_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
return <| elf32_executable_file3_header = hdr;
elf32_executable_file3_program_header_table = pht;
elf32_executable_file3_section_header_table = Nothing;
elf32_executable_file3_body = bs1 |>
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_executable_file3_header = hdr;
elf32_executable_file3_program_header_table = pht;
elf32_executable_file3_section_header_table = Just sht;
elf32_executable_file3_body = bs1 |>
(** [refine_elf64_executable_file2 f2] refines an elf64_executable_file2 [f2] into
* an elf64_executable_file3 by adding the optional section header table.
*)
val refine_elf64_executable_file2 : elf64_executable_file2 -> error elf64_executable_file3
let refine_elf64_executable_file2 f2 =
let hdr = f2.elf64_executable_file2_header in
let pht = f2.elf64_executable_file2_program_header_table in
let endian = get_elf64_header_endianness hdr in
let bs1 = f2.elf64_executable_file2_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
return <| elf64_executable_file3_header = hdr;
elf64_executable_file3_program_header_table = pht;
elf64_executable_file3_section_header_table = Nothing;
elf64_executable_file3_body = bs1 |>
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_executable_file3_header = hdr;
elf64_executable_file3_program_header_table = pht;
elf64_executable_file3_section_header_table = Just sht;
elf64_executable_file3_body = bs1 |>
(** [read_elf32_executable_file3 bs0] reads an elf32_executable_file3 from
* bitstring [bs0].
*)
val read_elf32_executable_file3 : bitstring -> error elf32_executable_file3
let read_elf32_executable_file3 bs0 =
read_elf32_executable_file2 bs0 >>= refine_elf32_executable_file2
(** [read_elf64_executable_file3 bs0] reads an elf64_executable_file3 from
* bitstring [bs0].
*)
val read_elf64_executable_file3 : bitstring -> error elf64_executable_file3
let read_elf64_executable_file3 bs0 =
read_elf64_executable_file2 bs0 >>= refine_elf64_executable_file2
(** string_of_elf32_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3]
* creates a string representation of [f3].
*)
val string_of_elf32_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file3 -> string
let string_of_elf32_executable_file3 hdr_bdl pht_bdl sht_bdl f3 =
let sht =
match f3.elf32_executable_file3_section_header_table with
| Nothing -> "\tNo section header table present"
| Just sht -> string_of_elf32_section_header_table sht_bdl sht
end
in
unlines [
"\n*Type elf32_executable_file3:"
; "**Header:"
; string_of_elf32_header hdr_bdl f3.elf32_executable_file3_header
; "**Program header table:"
; string_of_elf32_program_header_table pht_bdl f3.elf32_executable_file3_program_header_table
; "**Section header table:"
; sht
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf32_executable_file3_body)
]
(** string_of_elf64_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3]
* creates a string representation of [f3].
*)
val string_of_elf64_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file3 -> string
let string_of_elf64_executable_file3 hdr_bdl pht_bdl sht_bdl f3 =
let sht =
match f3.elf64_executable_file3_section_header_table with
| Nothing -> "\tNo section header table present"
| Just sht -> string_of_elf64_section_header_table sht_bdl sht
end
in
unlines [
"\n*Type elf64_executable_file3:"
; "**Header:"
; string_of_elf64_header hdr_bdl f3.elf64_executable_file3_header
; "**Program header table:"
; string_of_elf64_program_header_table pht_bdl f3.elf64_executable_file3_program_header_table
; "**Section header table:"
; sht
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_executable_file3_body)
]
|
