123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132(*Generated by Lem from gnu_extensions/gnu_ext_abi.lem.*)openLem_basic_classesopenLem_functionopenLem_stringopenLem_tupleopenLem_boolopenLem_listopenLem_sortingopenLem_numopenLem_maybeopenLem_assert_extraopenShowopenMissing_pervasivesopenByte_sequence(* open import Abis *)openElf_fileopenElf_headeropenElf_interpreted_segmentopenElf_interpreted_sectionopenElf_program_header_tableopenElf_section_header_tableopenElf_symbol_tableopenElf_types_native_uintopenElf_relocationopenElf_types_native_uintopenMemory_image(** Optional, like [stt_func] but always points to a function or piece of
* executable code that takes no arguments and returns a function pointer.
*)letstt_gnu_ifunc:Nat_big_num.num=((Nat_big_num.of_int10))(*val gnu_extend: forall 'abifeature. abi 'abifeature -> abi 'abifeature*)letgnu_extenda:'abifeatureabi=({is_valid_elf_header=(a.is_valid_elf_header);make_elf_header=((* t -> entry -> shoff -> phoff -> phnum -> shnum -> shstrndx -> hdr *)funt->funentry->funshoff->funphoff->funphnum->funshnum->funshstrndx->letunmod=(a.make_elf_headertentryshoffphoffphnumshnumshstrndx)in{elf64_ident=((matchunmod.elf64_identwithi0::i1::i2::i3::i4::i5::i6::_::_::i9::i10::i11::i12::i13::i14::i15::[]->[i0;i1;i2;i3;i4;i5;i6;Uint32_wrapper.of_bigintelf_osabi_gnu;Uint32_wrapper.of_bigint((Nat_big_num.of_int1));i9;i10;i11;i12;i13;i14;i15]));elf64_type=(Uint32_wrapper.of_bigintt);elf64_machine=(unmod.elf64_machine);elf64_version=(unmod.elf64_version);elf64_entry=(unmod.elf64_entry);elf64_phoff=(Uint64_wrapper.of_bigintphoff);elf64_shoff=(Uint64_wrapper.of_bigintshoff);elf64_flags=(unmod.elf64_flags);elf64_ehsize=(unmod.elf64_ehsize);elf64_phentsize=(unmod.elf64_phentsize);elf64_phnum=(Uint32_wrapper.of_bigintphnum);elf64_shentsize=(unmod.elf64_shentsize);elf64_shnum=(Uint32_wrapper.of_bigintshnum);elf64_shstrndx=(Uint32_wrapper.of_bigintshstrndx)});reloc=(a.reloc);section_is_special=(funisec1->(funimg2->(a.section_is_specialisec1img2||((Lem.option_equal(=)(Ml_bindings.string_prefix(Nat_big_num.of_int(String.length".gnu.warning"))isec1.elf64_section_name_as_string)(Some(".gnu.warning"))))(* FIXME: This is a slight abuse. The GNU linker's treatment of
* ".gnu.warning.*" section is not really a function of the output
* ABI -- it's a function of the input ABI, or arguably perhaps just
* of the linker itself. We have to do something to make sure these
* sections get silently processed separately from the usual linker
* control script, because otherwise our link map output doesn't match
* the GNU linker's. By declaring these sections "special" we achieve
* this by saying they don't participate in linking proper, just like
* ".symtab" and similar sections don't. HMM. I suppose this is
* okay, in that although a non-GNU linker might happily link these
* sections, arguably that is a failure to understand the input files.
* But the issue about it being a per-input-file property remains.
* Q. What does the GNU linker do if a reloc input file whose OSABI
* is *not* GNU contains a .gnu.warning.* section? That would be a fair
* test about whether looking at the input ABI is worth doing. *))));section_is_large=(a.section_is_large);maxpagesize=(a.maxpagesize);minpagesize=(a.minpagesize);commonpagesize=(a.commonpagesize);symbol_is_generated_by_linker=(a.symbol_is_generated_by_linker);make_phdrs=(a.make_phdrs)(* FIXME: also make the GNU phdrs! *);max_phnum=(Nat_big_num.add((Nat_big_num.of_int1))a.max_phnum)(* FIXME: GNU_RELRO, GNU_STACK; what else? *);guess_entry_point=(a.guess_entry_point);pad_data=(a.pad_data);pad_code=(a.pad_code);generate_support=(funinput_fnames_and_imgs->letvanilla_support_img=(a.generate_supportinput_fnames_and_imgs)in(* also generate .note.gnu.build-id *)letnew_by_range=(Pset.add(Some(".note.gnu.build-id",((Nat_big_num.of_int0),(Nat_big_num.of_int24))),FileFeature(ElfSection((Nat_big_num.of_int4)(* HACK: calculate this *),{elf64_section_name=((Nat_big_num.of_int0))(* ignored *);elf64_section_type=sht_note;elf64_section_flags=shf_alloc;elf64_section_addr=((Nat_big_num.of_int0))(* ignored -- covered by element *);elf64_section_offset=((Nat_big_num.of_int0))(* ignored -- will be replaced when file offsets are assigned *);elf64_section_size=((Nat_big_num.of_int24))(* ignored? NO, we use it in linker_script to avoid plumbing through the element record *);elf64_section_link=((Nat_big_num.of_int0));elf64_section_info=((Nat_big_num.of_int0));elf64_section_align=((Nat_big_num.of_int4));elf64_section_entsize=((Nat_big_num.of_int0));elf64_section_body=Byte_sequence.empty(* ignored *);elf64_section_name_as_string=".note.gnu.build-id"})))vanilla_support_img.by_range)in{elements=(Pmap.add".note.gnu.build-id"{startpos=None;length1=(Some((Nat_big_num.of_int24)));contents=([])}(vanilla_support_img.elements));by_tag=(by_tag_from_by_range(instance_Basic_classes_SetType_Maybe_maybe_dict(instance_Basic_classes_SetType_tup2_dictinstance_Basic_classes_SetType_var_dict(instance_Basic_classes_SetType_tup2_dictinstance_Basic_classes_SetType_Num_natural_dictinstance_Basic_classes_SetType_Num_natural_dict)))instance_Basic_classes_SetType_var_dictnew_by_range);by_range=new_by_range});concretise_support=(a.concretise_support);get_reloc_symaddr=(a.get_reloc_symaddr);parse_reloc_info=(a.parse_reloc_info)})