Source file elf_memory_image_of_elf64_file.ml
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
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
open Lem_basic_classes
open Lem_function
open Lem_string
open Lem_tuple
open Lem_bool
open Lem_list
open Lem_sorting
open Lem_map
open Lem_num
open Lem_maybe
open Lem_assert_extra
open Byte_pattern
open Byte_sequence
open Default_printing
open Error
open Missing_pervasives
open Show
open Endianness
open Elf_header
open Elf_file
open Elf_interpreted_section
open Elf_interpreted_segment
open Elf_section_header_table
open Elf_program_header_table
open Elf_symbol_table
open Elf_types_native_uint
open Elf_relocation
open String_table
open Memory_image
open Memory_image_orderings
open Elf_memory_image
let section_name_is_unique name1 f:bool=
((match mapMaybe (fun sec ->
if name1 = sec.elf64_section_name_as_string then Some sec else None
) f.elf64_file_interpreted_sections
with
[_] -> true
| _ -> false
))
let create_unique_name_for_section_from_index idx1 s f:string=
(let secname1 = (s.elf64_section_name_as_string)
in if section_name_is_unique secname1 f then secname1 else gensym secname1)
let create_unique_name_for_common_symbol_from_linkable_name fname1 syment symname f:string=
(
fname1 ^ ("_" ^ symname))
let get_unique_name_for_common_symbol_from_linkable_name fname1 syment symname:string=
(
fname1 ^ ("_" ^ symname))
let elf_memory_image_of_elf64_file a fname1 f:(Abis.any_abi_feature)annotated_memory_image=
(
(match f.elf64_file_program_header_table with
[] -> let = (extract_definitions_from_symtab_of_type sht_symtab f)
in
let interpreted_sections_without_null = ((match f.elf64_file_interpreted_sections with
[] -> failwith "impossible: empty list of interpreted sections"
| null_entry :: more -> more
))
in
let section_names_and_elements = (mapMaybei (fun i -> (fun isec1 ->
if elf64_interpreted_section_equal isec1 null_elf64_interpreted_section then
(if Nat_big_num.equal i( (Nat_big_num.of_int 0)) then None else failwith "internal error: null interpreted section not at index 0")
else
if Nat_big_num.equal i( (Nat_big_num.of_int 0)) then failwith "internal error: non-null interpreted section at index 0"
else
let created_name = (create_unique_name_for_section_from_index i isec1 f)
in
Some (created_name, {
startpos = None
; length1 = (Some isec1.elf64_section_size)
; contents = (byte_pattern_of_byte_sequence isec1.elf64_section_body)
})
)) f.elf64_file_interpreted_sections)
in
let common_symbols = (List.filter (fun x -> Nat_big_num.equal (Uint32_wrapper.to_bigint (x.def_syment.elf64_st_shndx)) shn_common) extracted_symbols)
in
let common_symbol_names_and_elements = (mapMaybei (fun i -> (fun isym ->
let symlen = (Ml_bindings.nat_big_num_of_uint64 isym.def_syment.elf64_st_size)
in
Some (get_unique_name_for_common_symbol_from_linkable_name fname1 isym.def_syment isym.def_symname, {
startpos = None
; length1 = (Some symlen)
; contents = (Missing_pervasives.replicate0 symlen None)
})
)) common_symbols)
in
let all_names_and_elements = (List.rev_append (List.rev section_names_and_elements) common_symbol_names_and_elements)
in
let (elf_sections : ( element_range option * elf_range_tag) list) = (mapMaybei (fun secidx_minus_one -> (
(fun (isec1, (secname1, _)) ->
let (r : element_range option) = (Some(secname1, ( (Nat_big_num.of_int 0), isec1.elf64_section_size)))
in
Some (r, FileFeature(ElfSection( Nat_big_num.add secidx_minus_one( (Nat_big_num.of_int 1)), isec1)))
)))
(list_combine interpreted_sections_without_null section_names_and_elements))
in
let (symbol_defs : ( element_range option * elf_range_tag) list) = (mapMaybe
(fun x ->
let section_num = (Uint32_wrapper.to_bigint x.def_syment.elf64_st_shndx)
in
let labelled_range =
(if Nat_big_num.equal section_num shn_abs then
None
else if Nat_big_num.equal section_num shn_common then
let element_name = (get_unique_name_for_common_symbol_from_linkable_name
fname1 x.def_syment x.def_symname)
in
Some(element_name, ( (Nat_big_num.of_int 0), Ml_bindings.nat_big_num_of_uint64 x.def_syment.elf64_st_size))
else
let (section_name, _) = ((match Ml_bindings.list_index_big_int ( Nat_big_num.sub_nat section_num( (Nat_big_num.of_int 1))) section_names_and_elements with
Some x -> x
| None -> failwith ("symbol " ^ (x.def_symname ^ " references nonexistent section"))
))
in
Some(section_name, (Ml_bindings.nat_big_num_of_uint64 x.def_syment.elf64_st_value, Ml_bindings.nat_big_num_of_uint64 x.def_syment.elf64_st_size)))
in
Some (labelled_range, SymbolDef(x))
)
(extract_definitions_from_symtab_of_type sht_symtab f))
in
let (symbol_refs : ( element_range option * elf_range_tag) list) = (mapMaybe
(fun (x : symbol_reference) ->
Some (None, SymbolRef({ ref = x; maybe_reloc = None; maybe_def_bound_to = None }))
)
(extract_references_from_symtab_of_type sht_symtab f))
in
let (all_reloc_sites : (element_range * elf_range_tag) list) = (Lem_list.map
(fun (x : symbol_reference_and_reloc_site) ->
let rel = ((match x.maybe_reloc with
Some rel -> rel
| None -> failwith "impossible: reloc site has no reloc"
))
in
let (section_name, _) = ((match Ml_bindings.list_index_big_int ( Nat_big_num.sub_nat rel.ref_src_scn( (Nat_big_num.of_int 1))) section_names_and_elements with
Some y -> y
| None -> failwith "relocs came from nonexistent section"
))
in
let (rel_type1, _) = (a.parse_reloc_info rel.ref_relent.elf64_ra_info)
in
let (_, applyfn) = (a.reloc rel_type1)
in
let (width, calcfn) = (applyfn (get_empty_memory_image ())( (Nat_big_num.of_int 0)) x)
in
let (offset : Uint64_wrapper.uint64) = (rel.ref_relent.elf64_ra_offset)
in
((section_name, (Ml_bindings.nat_big_num_of_uint64 offset, width)), SymbolRef(x))
)
(extract_all_relocs_as_symbol_references fname1 f))
in
let all_reloc_pairs = (Lem_list.map (fun (el_range, r_tag) -> (Some el_range, r_tag)) all_reloc_sites)
in
let reloc_as_triple = (fun ((_ : bool Memory_image.range_tag), (x : bool Memory_image.range_tag)) -> ((match x with
SymbolRef(r) -> (match r.maybe_reloc with
Some rel -> (rel.ref_rel_scn, rel.ref_rel_idx, rel.ref_src_scn)
| None -> failwith "impossible: "
)
| _ -> failwith "unexpected tag"
)))
in
let retrieved_reloc_sites = (Multimap.lookupBy0
(instance_Basic_classes_Ord_Memory_image_range_tag_dict
Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_tup2_dict
Lem_string_extra.instance_Basic_classes_Ord_string_dict
(instance_Basic_classes_Ord_tup2_dict
instance_Basic_classes_Ord_Num_natural_dict
instance_Basic_classes_Ord_Num_natural_dict)) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_tup2_dict
instance_Basic_classes_SetType_var_dict
(instance_Basic_classes_SetType_tup2_dict
instance_Basic_classes_SetType_Num_natural_dict
instance_Basic_classes_SetType_Num_natural_dict)) (Memory_image_orderings.tagEquiv
Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
(SymbolRef(null_symbol_reference_and_reloc_site))
(let ((fst : (string * Memory_image.range) list), (snd : ( Abis.any_abi_feature Memory_image.range_tag) list)) = (List.split all_reloc_sites) in (Pset.from_list (pairCompare compare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) (list_combine snd fst))))
in
let = ([(Some("header", ( (Nat_big_num.of_int 0), Uint32_wrapper.to_bigint f.elf64_file_header.elf64_ehsize)), FileFeature(ElfHeader(f.elf64_file_header)))])
in
let all_annotations_list = (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev all_reloc_pairs) symbol_refs)) symbol_defs)) elf_sections)) elf_header)
in
let all_annotations_length = (List.length all_annotations_list)
in
let all_annotations = (Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) all_annotations_list)
in
let (apply_content_relocations : string -> byte_pattern -> byte_pattern) = (fun (name1 : string) -> (fun content ->
let this_element_reloc_sites = (List.filter (fun ((n, range1), _) -> name1 = n) all_reloc_sites)
in
let ((this_element_name_and_reloc_ranges : (string * (Nat_big_num.num * Nat_big_num.num)) list), _) = (List.split this_element_reloc_sites)
in
let (this_element_reloc_ranges : (Nat_big_num.num * Nat_big_num.num) list) = (snd (List.split this_element_name_and_reloc_ranges))
in
let (all_ranges_expanded : bool list) = (expand_unsorted_ranges this_element_reloc_ranges (byte_pattern_length content) [])
in
relax_byte_pattern content all_ranges_expanded
))
in
let new_elements_list = (Lem_list.map (fun (name1, element1) ->
(
name1,
{
startpos = (element1.startpos)
; length1 = (element1.length1)
; contents =
(
let relaxed = (apply_content_relocations name1 element1.contents)
in
relaxed)
}
)
) all_names_and_elements)
in
{
elements = (Lem_map.fromList
(instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) new_elements_list)
; by_range = all_annotations
; by_tag = (let (fst, snd) = (List.split all_annotations_list) in (Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) (list_combine snd fst)))
}
| pht -> let segment_names_and_images = (mapMaybei (fun i -> (fun seg ->
Some((gensym (hex_string_of_natural seg.elf64_segment_base) ^ ("_" ^ (hex_string_of_natural seg.elf64_segment_type))),
{
startpos = (Some seg.elf64_segment_base)
; length1 = (Some seg.elf64_segment_memsz)
; contents = (byte_pattern_of_byte_sequence seg.elf64_segment_body)
})
)) f.elf64_file_interpreted_segments)
in
{
elements = (Lem_map.fromList
(instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) segment_names_and_images)
; by_range = (Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [])
; by_tag = (Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [])
}
))
let img2:elf64_header=
((match unique_tag_matching
Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict (FileFeature(ElfHeader(null_elf_header))) img2 with
FileFeature(ElfHeader(x)) -> x
| _ -> failwith "impossible: no header"
))
let elf_memory_image_sht img2:((elf64_section_header_table_entry)list)option=
((match unique_tag_matching
Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict (FileFeature(null_section_header_table)) img2 with
FileFeature(ElfSectionHeaderTable(x)) -> Some x
| _ -> None
))
let elf_memory_image_section_ranges img2:((Abis.any_abi_feature)range_tag)list*(element_range)list=
(
let tagged_ranges = (tagged_ranges_matching_tag
Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict (FileFeature(ElfSection( (Nat_big_num.of_int 0), null_elf64_interpreted_section))) img2)
in
let (tags, maybe_ranges) = (List.split tagged_ranges)
in
(tags, make_ranges_definite maybe_ranges))
let elf_memory_image_section_by_index idx1 img2:(elf64_interpreted_section)option=
(
let (allSectionTags, allSectionElementRanges) = (elf_memory_image_section_ranges img2)
in
let matches = (mapMaybei (fun i -> (fun tag -> (match tag with
FileFeature(ElfSection(itsIdx, s)) -> if Nat_big_num.equal itsIdx idx1 then Some s else None
| _ -> failwith "impossible"
))) allSectionTags)
in
(match matches with
[] -> None
| [x] -> Some x
| x -> failwith ("impossible: more than one ELF section with same index" )
))
let elf_memory_image_element_coextensive_with_section idx1 img2:(string)option=
(
let (allSectionTags, allSectionElementRanges) = (elf_memory_image_section_ranges img2)
in
let matches = (mapMaybei (fun i -> (fun (tag, (elName, (rangeStart, rangeLen))) -> (match tag with
FileFeature(ElfSection(itsIdx, s)) ->
let el_rec = ((match Pmap.lookup elName img2.elements with
Some x -> x
| None -> failwith "impossible: element not found"
))
in
let size_matches =
(
let range_len_matches_sec = ( Nat_big_num.equal rangeLen s.elf64_section_size)
in
let sec_matches_element_len = ( (Lem.option_equal Nat_big_num.equal(Some(s.elf64_section_size)) el_rec.length1))
in
let range_len_matches_element_len = ( (Lem.option_equal Nat_big_num.equal(Some(rangeLen)) el_rec.length1))
in
range_len_matches_element_len)
in
if Nat_big_num.equal itsIdx idx1 && (Nat_big_num.equal rangeStart( (Nat_big_num.of_int 0))
&& size_matches)
then
Some elName
else None
| _ -> failwith "impossible"
))) (list_combine allSectionTags allSectionElementRanges))
in
(match matches with
[] -> None
| [x] -> Some x
| xs -> failwith ("impossible: more than one ELF section coextensive with section" ^ ((Nat_big_num.to_string idx1) ^ (", names: "
^ (string_of_list
instance_Show_Show_string_dict xs))))
))
let name_of_elf_interpreted_section s shstrtab:(string)option=
((match get_string_at s.elf64_section_name (string_table_of_byte_sequence shstrtab.elf64_section_body) with
Success(x) -> Some x
| Fail(e) -> None
))
let elf_memory_image_sections_with_indices img2:(elf64_interpreted_section*Nat_big_num.num)list=
(
let ((all_section_tags : elf_range_tag list), (all_section_ranges : element_range list))
= (elf_memory_image_section_ranges img2)
in
Lem_list.map (fun tag ->
(match tag with
FileFeature(ElfSection(idx1, i)) -> (i, idx1)
| _ -> failwith "impossible: non-section in list of sections"
)) all_section_tags)
let elf_memory_image_sections img2:(elf64_interpreted_section)list=
(let (secs, _) = (List.split (elf_memory_image_sections_with_indices img2))
in secs)
let elf_memory_image_sections_with_name name1 img2:(elf64_interpreted_section)list=
(let all_interpreted_sections = (elf_memory_image_sections img2)
in
let maybe_shstrtab = (elf_memory_image_section_by_index (Uint32_wrapper.to_bigint ((elf_memory_image_header img2).elf64_shstrndx)) img2)
in
let shstrtab = ((match maybe_shstrtab with
None -> failwith "no shtstrtab"
| Some x -> x
))
in
let all_section_names = (Lem_list.map (fun i ->
let (stringtab : string_table) = (string_table_of_byte_sequence (shstrtab.elf64_section_body)) in
(match get_string_at i.elf64_section_name stringtab with
Fail _ -> None
| Success x -> Some x
)) all_interpreted_sections)
in
mapMaybe (fun (n, i) -> if (Lem.option_equal (=) (Some(name1)) n) then Some i else None) (list_combine all_section_names all_interpreted_sections))
let elf_memory_image_symbol_def_ranges img2:((Abis.any_abi_feature)range_tag)list*((element_range)option)list=
(
let (tags, maybe_ranges) = (List.split (
tagged_ranges_matching_tag
Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict (SymbolDef(null_symbol_definition)) img2
))
in
(tags, maybe_ranges))
let name_of_symbol_def0 sym1:string= (sym1.def_symname)
let elf_memory_image_defined_symbols_and_ranges img2:((element_range)option*symbol_definition)list=
(Memory_image_orderings.defined_symbols_and_ranges
Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict img2)
let elf_memory_image_defined_symbols img2:(symbol_definition)list=
(let ((all_symbol_tags : elf_range_tag list), (all_symbol_ranges : ( element_range option) list))
= (elf_memory_image_symbol_def_ranges img2)
in
Lem_list.mapMaybe (fun tag ->
(match tag with
SymbolDef(ent) -> Some ent
| _ -> failwith "impossible: non-symbol def in list of symbol defs"
)) all_symbol_tags)
let name_of_elf_section sec img2:(string)option=
(
Some sec.elf64_section_name_as_string)
let name_of_elf_element feature img2:(string)option=
((match feature with
ElfSection(_, sec) -> name_of_elf_section sec img2
| _ -> None
))
let get_unique_name_for_section_from_index idx1 isec1 img2:string=
(
(match elf_memory_image_element_coextensive_with_section idx1 img2 with
Some n -> n
| None -> failwith "section does not have an element name"
))