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
|
open import Basic_classes
open import Bool
open import List
open import Maybe
open import String
open import Tuple
open import Bitstring
open import Error
open import Missing_pervasives
open import Show
open import Elf_types
open import Endianness
open import String_table
(** Undefined symbol index *)
let stn_undef : nat = 0
(** Symbol binding *)
let stb_local : nat = 0
let stb_global : nat = 1
let stb_weak : nat = 2
let stb_loos : nat = 10
let stb_hios : nat = 12
let stb_loproc : nat = 13
let stb_hiproc : nat = 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 : nat = 0
let stt_object : nat = 1
let stt_func : nat = 2
let stt_section : nat = 3
let stt_file : nat = 4
let stt_common : nat = 5
let stt_tls : nat = 6
let stt_loos : nat = 10
let stt_hios : nat = 12
let stt_loproc : nat = 13
let stt_hiproc : nat = 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 : nat = 0
let stv_internal : nat = 1
let stv_hidden : nat = 2
let stv_protected : nat = 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 : elf32_word
; elf32_st_value : elf32_addr
; elf32_st_size : elf32_word
; elf32_st_info : unsigned_char
; elf32_st_other : unsigned_char
; elf32_st_shndx : elf32_half
|>
(** 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 =
nat_of_unsigned_char (unsigned_char_rshift entry 4)
val get_symbol_type : unsigned_char -> nat
let get_symbol_type entry =
nat_of_unsigned_char (unsigned_char_land entry (unsigned_char_of_nat 15)) (* 0xf *)
val get_symbol_info : unsigned_char -> unsigned_char -> nat
let get_symbol_info entry0 entry1 =
nat_of_unsigned_char (unsigned_char_plus
(unsigned_char_lshift entry0 4) (unsigned_char_land entry1
(unsigned_char_of_nat 15))) (*0xf*)
val get_symbol_visibility : unsigned_char -> nat
let get_symbol_visibility entry =
nat_of_unsigned_char (unsigned_char_land entry (unsigned_char_of_nat 3)) (* 0x3*)
type symtab_print_bundle = (nat -> string) * (nat -> string)
val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string
let string_of_elf32_symbol_table_entry entry =
unlines [
"\t" ^ "Name: " ^ show entry.elf32_st_name
; "\t" ^ "Value: " ^ show entry.elf32_st_value
; "\t" ^ "Size: " ^ show entry.elf32_st_size
; "\t" ^ "Info: " ^ show entry.elf32_st_info
; "\t" ^ "Other: " ^ show entry.elf32_st_other
; "\t" ^ "Shndx: " ^ show entry.elf32_st_shndx
]
type elf32_symbol_table = list elf32_symbol_table_entry
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)
class (HasElf32SymbolTable 'a)
val get_elf32_symbol_table : 'a -> elf32_symbol_table
end
val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring)
let read_elf32_symbol_table_entry endian bs0 =
read_elf32_word endian bs0 >>= fun (st_name, bs0) ->
read_elf32_addr endian bs0 >>= fun (st_value, bs0) ->
read_elf32_word endian bs0 >>= fun (st_size, bs0) ->
read_unsigned_char endian bs0 >>= fun (st_info, bs0) ->
read_unsigned_char endian bs0 >>= fun (st_other, bs0) ->
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 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 : elf64_word
; elf64_st_info : unsigned_char
; elf64_st_other : unsigned_char
; elf64_st_shndx : elf64_half
; elf64_st_value : elf64_addr
; elf64_st_size : elf64_xword
|>
val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string
let string_of_elf64_symbol_table_entry entry =
unlines [
"\t" ^ "Name: " ^ show entry.elf64_st_name
; "\t" ^ "Info: " ^ show entry.elf64_st_info
; "\t" ^ "Other: " ^ show entry.elf64_st_other
; "\t" ^ "Shndx: " ^ show entry.elf64_st_shndx
; "\t" ^ "Value: " ^ show entry.elf64_st_value
; "\t" ^ "Size: " ^ show entry.elf64_st_size
]
type elf64_symbol_table = list elf64_symbol_table_entry
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)
class (HasElf64SymbolTable 'a)
val get_elf64_symbol_table : 'a -> elf64_symbol_table
end
val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring)
let read_elf64_symbol_table_entry endian bs0 =
read_elf64_word endian bs0 >>= fun (st_name, bs0) ->
read_unsigned_char endian bs0 >>= fun (st_info, bs0) ->
read_unsigned_char endian bs0 >>= fun (st_other, bs0) ->
read_elf64_half endian bs0 >>= fun (st_shndx, bs0) ->
read_elf64_addr endian bs0 >>= fun (st_value, bs0) ->
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 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 = nat_of_elf32_word entry.elf32_st_name in
let addr = nat_of_elf32_addr 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 = nat_of_elf64_word entry.elf64_st_name in
let addr = nat_of_elf64_addr entry.elf64_st_value in
String_table.get_string_at name strtab >>= fun str ->
return (str, addr)
) symtab
|
