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
|
(*Generated by Lem from elf_note.lem.*)
(** [elf_note] contains data types and functions for interpreting the .note
* section/segment of an ELF file, and extracting information from that
* section/segment.
*)
open Lem_basic_classes
open Lem_list
open Lem_num
open Lem_string
open Byte_sequence
open Endianness
open Error
open Missing_pervasives
open Show
open Elf_program_header_table
open Elf_section_header_table
open Elf_types_native_uint
(** [elf32_note] represents the contents of a .note section or segment.
*)
type elf32_note =
{ elf32_note_namesz : Uint32.uint32 (** The size of the name field. *)
; elf32_note_descsz : Uint32.uint32 (** The size of the description field. *)
; elf32_note_type : Uint32.uint32 (** The type of the note. *)
; elf32_note_name : char list (** The list of bytes (of length indicated above) corresponding to the name string. *)
; elf32_note_desc : char list (** The list of bytes (of length indicated above) corresponding to the desc string. *)
}
(** [elf64_note] represents the contents of a .note section or segment.
*)
type elf64_note =
{ elf64_note_namesz : Uint64.uint64 (** The size of the name field. *)
; elf64_note_descsz : Uint64.uint64 (** The size of the description field. *)
; elf64_note_type : Uint64.uint64 (** The type of the note. *)
; elf64_note_name : char list (** The list of bytes (of length indicated above) corresponding to the name string. *)
; elf64_note_desc : char list (** The list of bytes (of length indicated above) corresponding to the desc string. *)
}
(** [read_elf32_note endian bs0] transcribes an ELF note section from byte
* sequence [bs0] assuming endianness [endian]. May fail if transcription fails
* (i.e. if the byte sequence is not sufficiently long).
*)
(*val read_elf32_note : endianness -> byte_sequence -> error (elf32_note * byte_sequence)*)
let read_elf32_note endian bs0:(elf32_note*byte_sequence)error=
(read_elf32_word endian bs0 >>= (fun (namesz, bs0) ->
read_elf32_word endian bs0 >>= (fun (descsz, bs0) ->
read_elf32_word endian bs0 >>= (fun (typ, bs0) ->
repeatM' (Nat_big_num.of_string (Uint32.to_string namesz)) bs0 read_char >>= (fun (name1, bs0) ->
repeatM' (Nat_big_num.of_string (Uint32.to_string descsz)) bs0 read_char >>= (fun (desc, bs0) ->
return ({ elf32_note_namesz = namesz; elf32_note_descsz = descsz;
elf32_note_type = typ; elf32_note_name = name1; elf32_note_desc = desc },
bs0)))))))
(** [read_elf64_note endian bs0] transcribes an ELF note section from byte
* sequence [bs0] assuming endianness [endian]. May fail if transcription fails
* (i.e. if the byte sequence is not sufficiently long).
*)
(*val read_elf64_note : endianness -> byte_sequence -> error (elf64_note * byte_sequence)*)
let read_elf64_note endian bs0:(elf64_note*byte_sequence)error=
(read_elf64_xword endian bs0 >>= (fun (namesz, bs0) ->
read_elf64_xword endian bs0 >>= (fun (descsz, bs0) ->
read_elf64_xword endian bs0 >>= (fun (typ, bs0) ->
repeatM' (Ml_bindings.nat_big_num_of_uint64 namesz) bs0 read_char >>= (fun (name1, bs0) ->
repeatM' (Ml_bindings.nat_big_num_of_uint64 descsz) bs0 read_char >>= (fun (desc, bs0) ->
return ({ elf64_note_namesz = namesz; elf64_note_descsz = descsz;
elf64_note_type = typ; elf64_note_name = name1; elf64_note_desc = desc },
bs0)))))))
(** [obtain_elf32_note_sections endian sht bs0] returns all note sections present
* in an ELF file, as indicated by the file's section header table [sht], reading
* them from byte sequence [bs0] assuming endianness [endian]. May fail if
* transcription of a note section fails.
*)
(*val obtain_elf32_note_sections : endianness -> elf32_section_header_table ->
byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_sections endian sht bs0:((elf32_note)list)error=
(let note_sects =
(List.filter (fun x ->
x.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_note)
) sht)
in
mapM (fun x ->
let offset = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset)) in
let size2 = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_size)) in
Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
read_elf32_note endian rel >>= (fun (note, _) ->
return note))
) note_sects)
(** [obtain_elf64_note_sections endian sht bs0] returns all note sections present
* in an ELF file, as indicated by the file's section header table [sht], reading
* them from byte sequence [bs0] assuming endianness [endian]. May fail if
* transcription of a note section fails.
*)
(*val obtain_elf64_note_sections : endianness -> elf64_section_header_table ->
byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_sections endian sht bs0:((elf64_note)list)error=
(let note_sects =
(List.filter (fun x ->
x.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_note)
) sht)
in
mapM (fun x ->
let offset = (Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset)) in
let size2 = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in
Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
read_elf64_note endian rel >>= (fun (note, _) ->
return note))
) note_sects)
(** [obtain_elf32_note_segments endian pht bs0] returns all note segments present
* in an ELF file, as indicated by the file's program header table [pht], reading
* them from byte sequence [bs0] assuming endianness [endian]. May fail if
* transcription of a note section fails.
*)
(*val obtain_elf32_note_segments : endianness -> elf32_program_header_table ->
byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_segments endian pht bs0:((elf32_note)list)error=
(let note_segs =
(List.filter (fun x ->
x.elf32_p_type = Uint32.of_string (Nat_big_num.to_string elf_pt_note)
) pht)
in
mapM (fun x ->
let offset = (Nat_big_num.of_string (Uint32.to_string x.elf32_p_offset)) in
let size2 = (Nat_big_num.of_string (Uint32.to_string x.elf32_p_filesz)) in
Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
read_elf32_note endian rel >>= (fun (note, _) ->
return note))
) note_segs)
(** [obtain_elf64_note_segments endian pht bs0] returns all note segments present
* in an ELF file, as indicated by the file's program header table [pht], reading
* them from byte sequence [bs0] assuming endianness [endian]. May fail if
* transcription of a note section fails.
*)
(*val obtain_elf64_note_segments : endianness -> elf64_program_header_table ->
byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_segments endian pht bs0:((elf64_note)list)error=
(let note_segs =
(List.filter (fun x ->
x.elf64_p_type = Uint32.of_string (Nat_big_num.to_string elf_pt_note)
) pht)
in
mapM (fun x ->
let offset = (Nat_big_num.of_string (Uint64.to_string x.elf64_p_offset)) in
let size2 = (Ml_bindings.nat_big_num_of_uint64 x.elf64_p_filesz) in
Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
read_elf64_note endian rel >>= (fun (note, _) ->
return note))
) note_segs)
(** [obtain_elf32_note_section_and_segments endian pht sht bs0] returns all note
* sections and segments present in an ELF file, as indicated by the file's
* program header table [pht] and section header table [sht], reading
* them from byte sequence [bs0] assuming endianness [endian]. May fail if
* transcription of a note section or segment fails.
*)
(*val obtain_elf32_note_section_and_segments : endianness -> elf32_program_header_table ->
elf32_section_header_table -> byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_section_and_segments endian pht sht bs0:((elf32_note)list)error=
(obtain_elf32_note_segments endian pht bs0 >>= (fun pht_notes ->
obtain_elf32_note_sections endian sht bs0 >>= (fun sht_notes ->
return ( List.rev_append (List.rev pht_notes) sht_notes))))
(** [obtain_elf64_note_section_and_segments endian pht sht bs0] returns all note
* sections and segments present in an ELF file, as indicated by the file's
* program header table [pht] and section header table [sht], reading
* them from byte sequence [bs0] assuming endianness [endian]. May fail if
* transcription of a note section or segment fails.
*)
(*val obtain_elf64_note_section_and_segments : endianness -> elf64_program_header_table ->
elf64_section_header_table -> byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_section_and_segments endian pht sht bs0:((elf64_note)list)error=
(obtain_elf64_note_segments endian pht bs0 >>= (fun pht_notes ->
obtain_elf64_note_sections endian sht bs0 >>= (fun sht_notes ->
return ( List.rev_append (List.rev pht_notes) sht_notes))))
(** [name_string_of_elf32_note note] extracts the name string of an ELF note
* section, interpreting the section's uninterpreted name field as a string.
*)
(*val name_string_of_elf32_note : elf32_note -> string*)
let name_string_of_elf32_note note:string=
(let bs0 = (Byte_sequence.from_byte_lists [note.elf32_note_name]) in
Byte_sequence.string_of_byte_sequence bs0)
(** [name_string_of_elf64_note note] extracts the name string of an ELF note
* section, interpreting the section's uninterpreted name field as a string.
*)
(*val name_string_of_elf64_note : elf64_note -> string*)
let name_string_of_elf64_note note:string=
(let bs0 = (Byte_sequence.from_byte_lists [note.elf64_note_name]) in
Byte_sequence.string_of_byte_sequence bs0)
|
