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
|
(*Generated by Lem from elf_symbol_table.lem.*)
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_string
open Lem_tuple
open Bitstring_local
open Error
open Missing_pervasives
open Show
open Elf_types
open Endianness
open String_table
(** Undefined symbol index *)
let stn_undef : int =( 0)
(** Symbol binding *)
let stb_local : int =( 0)
let stb_global : int =( 1)
let stb_weak : int =( 2)
let stb_loos : int =( 10)
let stb_hios : int =( 12)
let stb_loproc : int =( 13)
let stb_hiproc : int =( 15)
(*val string_of_symbol_binding : nat -> (nat -> string) -> (nat -> string) -> string*)
let string_of_symbol_binding m os proc =
(if m = stb_local then
"STB_LOCAL"
else if m = stb_global then
"STB_GLOBAL"
else if m = stb_weak then
"STB_WEAK"
else if (m >= stb_loos) && (m <= stb_hios) then
os m
else if (m >= stb_loproc) && (m <= stb_hiproc) then
proc m
else
"Invalid symbol binding")
(** Symbol types *)
let stt_notype : int =( 0)
let stt_object : int =( 1)
let stt_func : int =( 2)
let stt_section : int =( 3)
let stt_file : int =( 4)
let stt_common : int =( 5)
let stt_tls : int =( 6)
let stt_loos : int =( 10)
let stt_hios : int =( 12)
let stt_loproc : int =( 13)
let stt_hiproc : int =( 15)
(*val string_of_symbol_type : nat -> (nat -> string) -> (nat -> string) -> string*)
let string_of_symbol_type m os proc =
(if m = stt_notype then
"STT_NOTYPE"
else if m = stt_object then
"STT_OBJECT"
else if m = stt_func then
"STT_FUNC"
else if m = stt_section then
"STT_SECTION"
else if m = stt_file then
"STT_FILE"
else if m = stt_common then
"STT_COMMON"
else if m = stt_tls then
"STT_TLS"
else if (m >= stt_loos) && (m <= stt_hios) then
os m
else if (m >= stt_loproc) && (m <= stt_hiproc) then
proc m
else
"Invalid symbol type")
(** Symbol visibility *)
let stv_default : int =( 0)
let stv_internal : int =( 1)
let stv_hidden : int =( 2)
let stv_protected : int =( 3)
(*val string_of_symbol_visibility : nat -> string*)
let string_of_symbol_visibility m =
(if m = stv_default then
"STV_DEFAULT"
else if m = stv_internal then
"STV_INTERNAL"
else if m = stv_hidden then
"STV_HIDDEN"
else if m = stv_protected then
"STV_PROTECTED"
else
"Invalid symbol visibility")
(** ELF32 symbol table type *)
type elf32_symbol_table_entry =
{ elf32_st_name : Uint32.t
; elf32_st_value : Uint32.t
; elf32_st_size : Uint32.t
; elf32_st_info : Uint32.t
; elf32_st_other : Uint32.t
; elf32_st_shndx : Uint32.t
}
(** Extraction of symbol table data *)
(* Functions below common to 32- and 64-bit! *)
(*val get_symbol_binding : unsigned_char -> nat*)
let get_symbol_binding entry =
(Uint32.to_int (Uint32.shift_right entry( 4)))
(*val get_symbol_type : unsigned_char -> nat*)
let get_symbol_type entry =
(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 15)))) (* 0xf *)
(*val get_symbol_info : unsigned_char -> unsigned_char -> nat*)
let get_symbol_info entry0 entry1 =
(Uint32.to_int (Uint32.add
(Uint32.shift_left entry0( 4)) (Uint32.logand entry1
(Uint32.of_int( 15))))) (*0xf*)
(*val get_symbol_visibility : unsigned_char -> nat*)
let get_symbol_visibility entry =
(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 3)))) (* 0x3*)
type symtab_print_bundle = (int -> string) * (int -> string)
(*val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string*)
let string_of_elf32_symbol_table_entry entry =
(unlines [
("\t" ^ ("Name: " ^ Uint32.to_string entry.elf32_st_name))
; ("\t" ^ ("Value: " ^ Uint32.to_string entry.elf32_st_value))
; ("\t" ^ ("Size: " ^ Uint32.to_string entry.elf32_st_size))
; ("\t" ^ ("Info: " ^ Uint32.to_string entry.elf32_st_info))
; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf32_st_other))
; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf32_st_shndx))
])
type elf32_symbol_table = elf32_symbol_table_entry list
(*val string_of_elf32_symbol_table : elf32_symbol_table -> string*)
let string_of_elf32_symbol_table symtab =
(unlines (List.map string_of_elf32_symbol_table_entry symtab))
type 'a hasElf32SymbolTable_class={
get_elf32_symbol_table_method : 'a -> elf32_symbol_table
}
(*val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring)*)
let read_elf32_symbol_table_entry endian bs0 =
(Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_name, bs0) ->
Ml_bindings.read_elf32_addr endian bs0 >>= (fun (st_value, bs0) ->
Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_size, bs0) ->
Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) ->
Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) ->
Ml_bindings.read_elf32_half endian bs0 >>= (fun (st_shndx, bs0) ->
return ({ elf32_st_name = st_name; elf32_st_value = st_value;
elf32_st_size = st_size; elf32_st_info = st_info;
elf32_st_other = st_other; elf32_st_shndx = st_shndx }, bs0))))))))
(*val read_elf32_symbol_table : endianness -> bitstring -> error elf32_symbol_table*)
let rec read_elf32_symbol_table endian bs0 =
(if Bitstring.bitstring_length bs0 = 0 then
return []
else
read_elf32_symbol_table_entry endian bs0 >>= (fun (head, bs0) ->
read_elf32_symbol_table endian bs0 >>= (fun tail ->
return (head::tail))))
(** ELF64 symbol table type *)
type elf64_symbol_table_entry =
{ elf64_st_name : Uint32.t
; elf64_st_info : Uint32.t
; elf64_st_other : Uint32.t
; elf64_st_shndx : Uint32.t
; elf64_st_value : Uint64.t
; elf64_st_size : Uint64.t
}
(*val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string*)
let string_of_elf64_symbol_table_entry entry =
(unlines [
("\t" ^ ("Name: " ^ Uint32.to_string entry.elf64_st_name))
; ("\t" ^ ("Info: " ^ Uint32.to_string entry.elf64_st_info))
; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf64_st_other))
; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf64_st_shndx))
; ("\t" ^ ("Value: " ^ Uint64.to_string entry.elf64_st_value))
; ("\t" ^ ("Size: " ^ Uint64.to_string entry.elf64_st_size))
])
type elf64_symbol_table = elf64_symbol_table_entry list
(*val string_of_elf64_symbol_table : elf64_symbol_table -> string*)
let string_of_elf64_symbol_table symtab =
(unlines (List.map string_of_elf64_symbol_table_entry symtab))
type 'a hasElf64SymbolTable_class={
get_elf64_symbol_table_method : 'a -> elf64_symbol_table
}
(*val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring)*)
let read_elf64_symbol_table_entry endian bs0 =
(Ml_bindings.read_elf64_word endian bs0 >>= (fun (st_name, bs0) ->
Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) ->
Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) ->
Ml_bindings.read_elf64_half endian bs0 >>= (fun (st_shndx, bs0) ->
Ml_bindings.read_elf64_addr endian bs0 >>= (fun (st_value, bs0) ->
Ml_bindings.read_elf64_xword endian bs0 >>= (fun (st_size, bs0) ->
return ({ elf64_st_name = st_name; elf64_st_info = st_info;
elf64_st_other = st_other; elf64_st_shndx = st_shndx;
elf64_st_value = st_value; elf64_st_size = st_size }, bs0))))))))
(*val read_elf64_symbol_table : endianness -> bitstring -> error elf64_symbol_table*)
let rec read_elf64_symbol_table endian bs0 =
(if Bitstring.bitstring_length bs0 = 0 then
return []
else
read_elf64_symbol_table_entry endian bs0 >>= (fun (head, bs0) ->
read_elf64_symbol_table endian bs0 >>= (fun tail ->
return (head::tail))))
(*val get_elf32_symbol_image_address : elf32_symbol_table -> string_table -> error (list (string * nat))*)
let get_elf32_symbol_image_address symtab strtab =
(mapM (fun entry ->
let name = (Uint32.to_int entry.elf32_st_name) in
let addr = (Uint32.to_int entry.elf32_st_value) in
String_table.get_string_at name strtab >>= (fun str ->
return (str, addr))
) symtab)
(*val get_elf64_symbol_image_address : elf64_symbol_table -> string_table -> error (list (string * nat))*)
let get_elf64_symbol_image_address symtab strtab =
(mapM (fun entry ->
let name = (Uint32.to_int entry.elf64_st_name) in
let addr = (Uint64.to_int entry.elf64_st_value) in
String_table.get_string_at name strtab >>= (fun str ->
return (str, addr))
) symtab)
|
