blob: 4c539294ccc7a4b4d4d72a2d03d066b838dd0d1e (
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
|
open import Basic_classes
open import Bool
open import Maybe
open import Num
open import String
open import Elf_file1
open import Elf_header
open import Elf_program_header_table
open import Elf_types
open import Bitstring
open import Error
open import Missing_pervasives
open import Show
(** Type [elf32_executable_file2] represents the lazy unfolding of a 32-bit ELF
* file where the structure of the header, program header table (mandatory).
*)
type elf32_executable_file2 =
<| elf32_executable_file2_header : elf32_header (** The ELF header (mandatory) *)
; elf32_executable_file2_program_header_table : elf32_program_header_table (** The program header table (mandatory) *)
; elf32_executable_file2_body : bitstring (** Uninterpreted data *)
|>
class (HasElf32ExecutableFile2 'a)
val get_elf32_executable_file2 : 'a -> elf32_executable_file2
end
instance (HasElf32ExecutableFile2 elf32_executable_file2)
let get_elf32_executable_file2 f2 = f2
end
instance (HasElf32File1 elf32_executable_file2)
let get_elf32_file1 f2 =
<| elf32_file1_header = f2.elf32_executable_file2_header;
elf32_file1_body = f2.elf32_executable_file2_body |>
end
instance (HasElf32Header elf32_executable_file2)
let get_elf32_header f2 = f2.elf32_executable_file2_header
end
instance (HasElf32ProgramHeaderTable elf32_executable_file2)
let get_elf32_program_header_table f2 = Just (f2.elf32_executable_file2_program_header_table)
end
(** Type [elf64_executable_file2] represents the lazy unfolding of a 64-bit ELF
* file where the structure of the header, program header table (mandatory).
*)
type elf64_executable_file2 =
<| elf64_executable_file2_header : elf64_header (** The ELF header (mandatory) *)
; elf64_executable_file2_program_header_table : elf64_program_header_table (** The program header table (mandatory) *)
; elf64_executable_file2_body : bitstring (** Uninterpreted data *)
|>
class (HasElf64ExecutableFile2 'a)
val get_elf64_executable_file2 : 'a -> elf64_executable_file2
end
instance (HasElf64ExecutableFile2 elf64_executable_file2)
let get_elf64_executable_file2 f2 = f2
end
instance (HasElf64File1 elf64_executable_file2)
let get_elf64_file1 f2 =
<| elf64_file1_header = f2.elf64_executable_file2_header;
elf64_file1_body = f2.elf64_executable_file2_body |>
end
instance (HasElf64Header elf64_executable_file2)
let get_elf64_header f2 = f2.elf64_executable_file2_header
end
instance (HasElf64ProgramHeaderTable elf64_executable_file2)
let get_elf64_program_header_table f2 = Just (f2.elf64_executable_file2_program_header_table)
end
(** [refine_elf32_file1 f1] refines the [elf31_file1] [f1] adding the
* mandatory program header table to [f1]'s header. Fails if [f1]'s header
* states that no program header table is present, or if there is some other
* transcription error when reading from [f1]'s body.
*)
val refine_elf32_file1 : elf32_file1 -> error elf32_executable_file2
let refine_elf32_file1 f1 =
if not (is_executable_elf32_file1 f1) then
Fail "refine_elf32_file1: not an executable file type"
else
let hdr = f1.elf32_file1_header in
let endian = get_elf32_header_endianness hdr in
let bs1 = f1.elf32_file1_body in
let pentries = nat_of_elf32_half hdr.elf32_phnum in
let pentry_size = nat_of_elf32_half hdr.elf32_phentsize * 8 in
let psize = pentries * pentry_size in
if psize = 0 then
Fail "refine_elf32_file1: program header table not present"
else
let poffset = nat_of_elf32_off hdr.elf32_phoff * 8 in
let (_, pcut) = partition poffset bs1 in
let (pexact, _) = partition psize pcut in
(* Bitstring irrelevant below as exact size used... *)
read_elf32_program_header_table psize endian pexact >>= fun (pht, _) ->
return <| elf32_executable_file2_header = hdr;
elf32_executable_file2_program_header_table = pht;
elf32_executable_file2_body = bs1 |>
(** [refine_elf64_file1 f1] refines the [elf31_file1] [f1] adding the
* mandatory program header table to [f1]'s header. Fails if [f1]'s header
* states that no program header table is present, or if there is some other
* transcription error when reading from [f1]'s body.
*)
val refine_elf64_file1 : elf64_file1 -> error elf64_executable_file2
let refine_elf64_file1 f1 =
if not (is_executable_elf64_file1 f1) then
Fail "refine_elf64_file1: not an executable file type"
else
let hdr = f1.elf64_file1_header in
let endian = get_elf64_header_endianness hdr in
let bs1 = f1.elf64_file1_body in
let pentries = nat_of_elf64_half hdr.elf64_phnum in
let pentry_size = nat_of_elf64_half hdr.elf64_phentsize * 8 in
let psize = pentries * pentry_size in
if psize = 0 then
Fail "refine_elf64_file1: program header table not present"
else
let poffset = nat_of_elf64_off hdr.elf64_phoff * 8 in
let (_, pcut) = partition poffset bs1 in
let (pexact, _) = partition psize pcut in
(* Bitstring irrelevant below as exact size used... *)
read_elf64_program_header_table psize endian pexact >>= fun (pht, _) ->
return <| elf64_executable_file2_header = hdr;
elf64_executable_file2_program_header_table = pht;
elf64_executable_file2_body = bs1 |>
(** [read_elf32_executable_file2 bs0] creates an [elf32_executable_file2] record
* directly from the bitstring [bs0].
*)
val read_elf32_executable_file2 : bitstring -> error elf32_executable_file2
let read_elf32_executable_file2 bs0 =
read_elf32_file1 bs0 >>= refine_elf32_file1
(** [read_elf64_executable_file2 bs0] creates an [elf64_executable_file2] record
* directly from the bitstring [bs0].
*)
val read_elf64_executable_file2 : bitstring -> error elf64_executable_file2
let read_elf64_executable_file2 bs0 =
read_elf64_file1 bs0 >>= refine_elf64_file1
(** [string_of_elf32_executable_file2 os proc f2] creates a string representation of [f2].
*)
val string_of_elf32_executable_file2 : hdr_print_bundle -> pht_print_bundle -> elf32_executable_file2 -> string
let string_of_elf32_executable_file2 hdr_bdl pht_bdl f2 =
unlines [
"\n*Type elf32_executable_file2:"
; "**Header:"
; string_of_elf32_header hdr_bdl f2.elf32_executable_file2_header
; "**Program header table:"
; string_of_elf32_program_header_table pht_bdl f2.elf32_executable_file2_program_header_table
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf32_executable_file2_body)
]
(** [string_of_elf64_executable_file2 os proc f2] creates a string representation of [f2].
*)
val string_of_elf64_executable_file2 : hdr_print_bundle -> pht_print_bundle -> elf64_executable_file2 -> string
let string_of_elf64_executable_file2 hdr_bdl pht_bdl f2 =
unlines [
"\n*Type elf64_executable_file2:"
; "**Header:"
; string_of_elf64_header hdr_bdl f2.elf64_executable_file2_header
; "**Program header table:"
; string_of_elf64_program_header_table pht_bdl f2.elf64_executable_file2_program_header_table
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf64_executable_file2_body)
]
|
