package linksem

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(*Generated by Lem from elf_memory_image_of_elf64_file.lem.*)
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
(*import Set*)
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

(*val section_name_is_unique : string -> elf64_file -> bool*)
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
    ))

(*val create_unique_name_for_section_from_index : natural -> elf64_interpreted_section -> elf64_file -> string*)
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)

(*val create_unique_name_for_common_symbol_from_linkable_name : string -> elf64_symbol_table_entry -> string -> elf64_file -> string*)
let create_unique_name_for_common_symbol_from_linkable_name fname1 syment symname f:string=
     (
    (* FIXME: uniqueness? I suppose file names are unique. How to avoid overlapping with
     * section names? *)fname1 ^ ("_" ^ symname))

(*val get_unique_name_for_common_symbol_from_linkable_name : string -> elf64_symbol_table_entry -> string -> string*)
let get_unique_name_for_common_symbol_from_linkable_name fname1 syment symname:string=
     (
    (* FIXME: uniqueness? I suppose file names are unique. How to avoid overlapping with
     * section names? *)fname1 ^ ("_" ^ symname))

(*val elf_memory_image_of_elf64_file : forall 'abifeature. abi 'abifeature -> string -> elf64_file -> elf_memory_image*)
let elf_memory_image_of_elf64_file a fname1 f:(Abis.any_abi_feature)annotated_memory_image=
     (
    (* Do we have program headers? This decides whether we choose a
     * sectionwise or segmentwise view. *)(match f.elf64_file_program_header_table with
        [] ->   let extracted_symbols =  (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 ->
                    (* In principle, we can have unnamed sections. But
                     * don't add the dummy initial SHT entry. This is *not* in the
                     * list of interpreted sections. *)
                    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
                        (*let _ = errln ("In file " ^ fname ^ " created element name " ^ created_name ^ " for section idx " ^ (show i) ^ ", name " ^
                            isec.elf64_section_name_as_string)
                        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 _ = Missing_pervasives.errln ("Found " ^ (show (length common_symbols)) ^ " common symbols in file " ^ fname)
                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
                (* -- annotations are reloc sites, symbol defs, ELF sections/segments/headers, PLT/GOT/...
                 * Since we stripped the null SHT entry, mapMaybei would ideally index from one. We add one.  *)
                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
                                (* We have an annotation that doesn't apply to any range.
                                 * That's all right -- that's why the range is a maybe. *)
                                None
                            else if Nat_big_num.equal section_num shn_common then
                                (* Each common symbol becomes its own elemenet (\approx section).
                                 * We label *that element* with a (coextensive) symbol definition. *)
                                 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
                (* FIXME: should a common symbol be a reference too?
                 * I prefer to think of common symbols as mergeable sections.
                 * Under this interpretation, there's no need for a reference.
                 * BUT the GC behaviour might be different! What happens if
                 * a common symbol is not referenced? *)
                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)
                         (* GAH. We don't have an image.
                            If we pass an empty memory image, will we fail? Need to make it work *)
                        in
                          (* FIXME: for copy relocs, the size depends on the *definition*.
                             AHA! a copy reloc always *has* a symbol definition locally; it just gets its *value*
                             from the shared object's definition.
                             In other words, a copy reloc always references a defined symbol, and the amount
                             copied is the minimum of that symbol's size and the overridden (copied-from .so)'s
                             symbol's size. *)
                        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 _ = Missing_pervasives.errln ("Extracted " ^ (show (length all_reloc_sites)) ^ " reloc site tags from "
                    ^ "file " ^ fname ^ ": " ^ (show (List.map reloc_as_triple all_reloc_sites)))
                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 _ = Missing_pervasives.errln ("Re-reading: retrieved " ^ (show (length retrieved_reloc_sites)) ^ " reloc site tags from "
                    ^ "file " ^ fname ^ ": " ^ (show (List.map reloc_as_triple (let (fst, snd) = unzip retrieved_reloc_sites in zip snd fst))))
                in*)
                let elf_header = ([(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 _ = Missing_pervasives.errln ("ELF header contributes " ^ (show (List.length elf_header)) ^ " annotations.")
                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 _ = Missing_pervasives.errln ("total annotations: " ^ (show all_annotations_length))
                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) ->
                    (* We can now mark the relocation sites in the section contents as "subject to change". *)
                    (
                        name1,
                        {
                           startpos = (element1.startpos)
                         ; length1   = (element1.length1)
                         ; contents =
                            (
                            (*let _ = errln ("Reloc-relaxing section " ^ name ^ " in file " ^ fname ^ ": before, first 20 bytes: " ^
                                (show (take 20 element.contents)))
                            in*)let relaxed = (apply_content_relocations name1 element1.contents)
                            in
                            (*let _ = errln ("After, first 20 bytes: " ^  (show (take 20 relaxed)))
                            in*)
                            relaxed)

                         }
                    )
                  ) all_names_and_elements)
                in
                            (*
                            List.foldr (fun acc -> (fun  element.contents this_element_reloc_ranges
                            let (expand_and_relax : list (maybe byte) -> (natural * natural) -> list (maybe byte)) = fun pat -> (fun r -> (
                                relax_byte_pattern pat (expand_ranges r)
                            ))
                            in*)
                 {
                      elements = (Lem_map.fromList 
  (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) new_elements_list)
                      (* : memory_image -- the image elements, without annotation, i.e.
                        a map from string to (startpos, length, contents)
                        -- an element is the ELF header, PHT, SHT, section or segment
                        -- exploit the fact that section names beginning `.' are reserved, and
                           the reserved ones don't use caps: ".PHT", ".SHT", ".HDR"
                        -- what about ambiguous section names? use ".GENSYM_<...>" perhaps
                      *)
                    ; 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)))
                        (*  : multimap (elf_range_tag 'symdef 'reloc 'filefeature 'abifeature) (string * range)
                         -- annotations by *)
                  }
      | 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
                (* let annotations = *)
                 {
                      elements = (Lem_map.fromList 
  (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) segment_names_and_images)  (* : memory_image -- the image elements, without annotation, i.e.
                        a map from string to (startpos, length, contents)
                        -- an element is the ELF header, PHT, SHT, section or segment
                        -- exploit the fact that section names beginning `.' are reserved, and
                           the reserved ones don't use caps: ".PHT", ".SHT", ".HDR"
                        -- what about ambiguous section names? use ".GENSYM_<...>" perhaps
                      *)
                    ; by_range = (Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [])
                        (* : map element_range (list (elf_range_tag 'symdef 'reloc 'filefeature 'abifeature))
                         -- annotations are reloc sites, symbol defs, ELF sections/segments/headers, PLT/GOT/...  *)
                    ; by_tag = (Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [])
                        (*  : multimap (elf_range_tag 'symdef 'reloc 'filefeature 'abifeature) (string * range)
                         -- annotations by *)
                  }

    ))

(*val elf_memory_image_header : elf_memory_image -> elf64_header*)
let elf_memory_image_header 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"
    ))

(*val elf_memory_image_sht : elf_memory_image -> maybe elf64_section_header_table*)
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
    ))

(*val elf_memory_image_section_ranges : elf_memory_image -> (list elf_range_tag * list element_range)*)
let elf_memory_image_section_ranges img2:((Abis.any_abi_feature)range_tag)list*(element_range)list=
     (
    (* find all element ranges labelled as ELF sections *)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))

(*val elf_memory_image_section_by_index : natural -> elf_memory_image -> maybe elf64_interpreted_section*)
let elf_memory_image_section_by_index idx1 img2:(elf64_interpreted_section)option=
     (
    (* find all element ranges labelled as ELF sections *)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" (*"(" ^ (show idx) ^ ")"*))
    ))

(*val elf_memory_image_element_coextensive_with_section : natural -> elf_memory_image -> maybe string*)
let elf_memory_image_element_coextensive_with_section idx1 img2:(string)option=
     (
    (* find all element ranges labelled as ELF sections *)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 =
                (
                (* HMM. This is complicated. Generally we like to ignore
                 * isec fields that are superseded by memory_image fields,
                 * here the element length. But we want to catch the case
                 * where there's an inconsistency, and we *might* want to allow the
                 * case where the element length is still vague (Nothing). *)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
                (* If any pair are unequal, then warn. *)
                (*let _ =
                if (range_len_matches_sec <> sec_matches_element_len
                 || sec_matches_element_len <> range_len_matches_element_len
                 || range_len_matches_sec <> range_len_matches_element_len)
                then errln ("Warning: section lengths do not agree: " ^ s.elf64_section_name_as_string)
                else ()
                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
            (* *)
            (* Sanity check: does the *)
            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))))
    ))


(*val name_of_elf_interpreted_section :
    elf64_interpreted_section -> elf64_interpreted_section -> maybe string*)
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
    ))

(*val elf_memory_image_sections_with_indices : elf_memory_image -> list (elf64_interpreted_section * natural)*)
let elf_memory_image_sections_with_indices img2:(elf64_interpreted_section*Nat_big_num.num)list=
     (
    (* We have to get all sections and their names,
     * because section names need not be unique. *)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)

(*val elf_memory_image_sections : elf_memory_image -> list elf64_interpreted_section*)
let elf_memory_image_sections img2:(elf64_interpreted_section)list=
     (let (secs, _) = (List.split (elf_memory_image_sections_with_indices img2))
    in secs)

(*val elf_memory_image_sections_with_name : string -> elf_memory_image -> list elf64_interpreted_section*)
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))
(*
val elf_memory_image_unique_section_with_name : string -> elf_memory_image -> elf64_interpreted_section
let elf_memory_image_unique_section_with_name name img =
    match Map.lookup name img.image with
        Just el -> match el with
            FileFeature(ElfSection(_, x)) -> x
            | _ -> failwith "impossible: section name does not name a section"
        end
        |
        | Nothing -> failwith ("no section named '" ^ name ^ "' but asserted unique")
    end
*)

(* FIXME: delete these symbol functions, because Memory_image_orderings
 * has generic ones. *)

(*val elf_memory_image_symbol_def_ranges : elf_memory_image -> (list elf_range_tag * list (maybe element_range))*)
let elf_memory_image_symbol_def_ranges img2:((Abis.any_abi_feature)range_tag)list*((element_range)option)list=
     (
    (* find all element ranges labelled as ELF symbols *)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
    (* some symbols, specifically ABS symbols, needn't label a range. *)
    (tags, maybe_ranges))

(*val name_of_symbol_def : symbol_definition -> string*)
let name_of_symbol_def0 sym1:string=  (sym1.def_symname)

(*val elf_memory_image_defined_symbols_and_ranges : elf_memory_image -> list ((maybe element_range) * symbol_definition)*)
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)

(*val elf_memory_image_defined_symbols : elf_memory_image -> list symbol_definition*)
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)

(*
val elf_memory_image_symbols_with_name : string -> elf_memory_image -> list symbol_definition
let elf_memory_image_symbols_with_name name img =
    let all_interpreted_sections = elf_memory_image_sections img
    in
    let maybe_shstrtab = elf_memory_image_section_by_index (natural_of_elf64_half ((elf_memory_image_header img).elf64_shstrndx)) img
    in
    let shstrtab = match maybe_shstrtab with
        Nothing -> failwith "no shtstrtab"
        | Just x -> x
    end
    in
    let all_section_names = 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 _ -> Nothing
            | Success x -> Just x
        end) all_interpreted_sections
    in
    mapMaybe (fun (n, i) -> if Just(name) = n then Just i else Nothing) (zip all_section_names all_interpreted_sections)
*)
(*
val elf_memory_image_unique_symbol_with_name : string -> elf_memory_image -> symbol_def
let elf_memory_image_unique_symbol_with_name name img =
    match Map.lookup name img.image with
        Just el -> match el with
            FileFeature(ElfSection(_, x)) -> x
            | _ -> failwith "impossible: section name does not name a section"
        end
        |
        | Nothing -> failwith ("no section named '" ^ name ^ "' but asserted unique")
    end
*)


(*val name_of_elf_section : elf64_interpreted_section -> elf_memory_image -> maybe string*)
let name_of_elf_section sec img2:(string)option=
    (
   (* let shstrndx = natural_of_elf64_half ((elf_memory_image_header img).elf64_shstrndx)
   in
   match elf_memory_image_section_by_index shstrndx img with
        Nothing -> Nothing
        | Just shstrtab -> name_of_elf_interpreted_section sec shstrtab
  end *)Some sec.elf64_section_name_as_string)

(*val name_of_elf_element : elf_file_feature -> elf_memory_image -> maybe string*)
let name_of_elf_element feature img2:(string)option=
     ((match feature with
        ElfSection(_, sec) -> name_of_elf_section sec img2
        | _ -> None (* FIXME *)
    ))

(*val get_unique_name_for_section_from_index : natural -> elf64_interpreted_section -> elf_memory_image -> string*)
let get_unique_name_for_section_from_index idx1 isec1 img2:string=
     (
    (* Don't call gensym just to retrieve the name *)(match elf_memory_image_element_coextensive_with_section idx1 img2 with
        Some n -> n
        | None -> failwith "section does not have an element name"
    ))
OCaml

Innovation. Community. Security.