blob: edb97be4779b37726c032df5c542deb76e37bead (
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
|
open import Basic_classes
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_header
open import Elf_linking_file2
open import Elf_program_header_table
open import Elf_section_header_table
open import Elf_types
type elf32_linking_file3 =
<| elf32_linking_file3_header : elf32_header
; elf32_linking_file3_program_header_table : maybe elf32_program_header_table
; elf32_linking_file3_body : bitstring
; elf32_linking_file3_section_header_table : elf32_section_header_table
|>
class (HasElf32LinkingFile3 'a)
val get_elf32_linking_file3 : 'a -> elf32_linking_file3
end
instance (HasElf32LinkingFile3 elf32_linking_file3)
let get_elf32_linking_file3 f3 = f3
end
instance (HasElf32LinkingFile2 elf32_linking_file3)
let get_elf32_linking_file2 f3 =
<| elf32_linking_file2_header = f3.elf32_linking_file3_header;
elf32_linking_file2_body = f3.elf32_linking_file3_body;
elf32_linking_file2_section_header_table = f3.elf32_linking_file3_section_header_table |>
end
instance (HasElf32Header elf32_linking_file3)
let get_elf32_header f3 = f3.elf32_linking_file3_header
end
instance (HasElf32SectionHeaderTable elf32_linking_file3)
let get_elf32_section_header_table f3 = Just f3.elf32_linking_file3_section_header_table
end
instance (HasElf32ProgramHeaderTable elf32_linking_file3)
let get_elf32_program_header_table f3 = f3.elf32_linking_file3_program_header_table
end
val refine_elf32_linking_file2 : elf32_linking_file2 -> error elf32_linking_file3
let refine_elf32_linking_file2 f2 =
let hdr = f2.elf32_linking_file2_header in
let sht = f2.elf32_linking_file2_section_header_table in
let endian = get_elf32_header_endianness hdr in
let bs1 = f2.elf32_linking_file2_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
return <| elf32_linking_file3_header = hdr;
elf32_linking_file3_program_header_table = Nothing;
elf32_linking_file3_section_header_table = sht;
elf32_linking_file3_body = bs1 |>
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_linking_file3_header = hdr;
elf32_linking_file3_program_header_table = Just pht;
elf32_linking_file3_section_header_table = sht;
elf32_linking_file3_body = bs1 |>
val read_elf32_linking_file3 : bitstring -> error elf32_linking_file3
let read_elf32_linking_file3 bs0 =
read_elf32_linking_file2 bs0 >>= refine_elf32_linking_file2
val string_of_elf32_linking_file3 : hdr_print_bundle -> sht_print_bundle -> pht_print_bundle -> elf32_linking_file3 -> string
let string_of_elf32_linking_file3 hdr_bdl sht_bdl pht_bdl f3 =
let pht =
match f3.elf32_linking_file3_program_header_table with
| Nothing -> "\tNo program header table present"
| Just pht -> string_of_elf32_program_header_table pht_bdl pht
end
in
unlines [
"\n*Type elf32_linking_file3:"
; "**Header:"
; string_of_elf32_header hdr_bdl f3.elf32_linking_file3_header
; "**Program header table:"
; pht
; "**Section header table:"
; string_of_elf32_section_header_table sht_bdl f3.elf32_linking_file3_section_header_table
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf32_linking_file3_body)
]
type elf64_linking_file3 =
<| elf64_linking_file3_header : elf64_header
; elf64_linking_file3_program_header_table : maybe elf64_program_header_table
; elf64_linking_file3_body : bitstring
; elf64_linking_file3_section_header_table : elf64_section_header_table
|>
class (HasElf64LinkingFile3 'a)
val get_elf64_linking_file3 : 'a -> elf64_linking_file3
end
instance (HasElf64LinkingFile3 elf64_linking_file3)
let get_elf64_linking_file3 f3 = f3
end
instance (HasElf64LinkingFile2 elf64_linking_file3)
let get_elf64_linking_file2 f3 =
<| elf64_linking_file2_header = f3.elf64_linking_file3_header;
elf64_linking_file2_body = f3.elf64_linking_file3_body;
elf64_linking_file2_section_header_table = f3.elf64_linking_file3_section_header_table |>
end
instance (HasElf64Header elf64_linking_file3)
let get_elf64_header f3 = f3.elf64_linking_file3_header
end
instance (HasElf64SectionHeaderTable elf64_linking_file3)
let get_elf64_section_header_table f3 = Just f3.elf64_linking_file3_section_header_table
end
instance (HasElf64ProgramHeaderTable elf64_linking_file3)
let get_elf64_program_header_table f3 = f3.elf64_linking_file3_program_header_table
end
val refine_elf64_linking_file2 : elf64_linking_file2 -> error elf64_linking_file3
let refine_elf64_linking_file2 f2 =
let hdr = f2.elf64_linking_file2_header in
let sht = f2.elf64_linking_file2_section_header_table in
let endian = get_elf64_header_endianness hdr in
let bs1 = f2.elf64_linking_file2_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
return <| elf64_linking_file3_header = hdr;
elf64_linking_file3_program_header_table = Nothing;
elf64_linking_file3_section_header_table = sht;
elf64_linking_file3_body = bs1 |>
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_linking_file3_header = hdr;
elf64_linking_file3_program_header_table = Just pht;
elf64_linking_file3_section_header_table = sht;
elf64_linking_file3_body = bs1 |>
val read_elf64_linking_file3 : bitstring -> error elf64_linking_file3
let read_elf64_linking_file3 bs0 =
read_elf64_linking_file2 bs0 >>= refine_elf64_linking_file2
val string_of_elf64_linking_file3 : hdr_print_bundle -> sht_print_bundle -> pht_print_bundle -> elf64_linking_file3 -> string
let string_of_elf64_linking_file3 hdr_bdl sht_bdl pht_bdl f3 =
let pht =
match f3.elf64_linking_file3_program_header_table with
| Nothing -> "\tNo program header table present"
| Just pht -> string_of_elf64_program_header_table pht_bdl pht
end
in
unlines [
"\n*Type elf64_linking_file3:"
; "**Header:"
; string_of_elf64_header hdr_bdl f3.elf64_linking_file3_header
; "**Program header table:"
; pht
; "**Section header table:"
; string_of_elf64_section_header_table sht_bdl f3.elf64_linking_file3_section_header_table
; "**Body:"
; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_linking_file3_body)
]
|
