diff options
| author | Alasdair Armstrong | 2018-01-18 18:16:45 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-18 18:31:26 +0000 |
| commit | 0fa42d315e20f819af93c2a822ab1bc032dc4535 (patch) | |
| tree | 7ef4ea3444ba5938457e7c852f9ad9957055fe41 /lib/ocaml_rts/linksem/gnu_extensions | |
| parent | 24dc13511053ab79ccb66ae24e3b8ffb9cad0690 (diff) | |
Modified ocaml backend to use ocamlfind for linksem and lem
Fixed test cases for ocaml backend and interpreter
Diffstat (limited to 'lib/ocaml_rts/linksem/gnu_extensions')
8 files changed, 0 insertions, 1686 deletions
diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_abi.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_abi.ml deleted file mode 100644 index 7371547f..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_abi.ml +++ /dev/null @@ -1,131 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_abi.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_num -open Lem_maybe -open Lem_assert_extra -open Show -open Missing_pervasives - -open Byte_sequence - -(* open import Abis *) - -open Elf_file -open Elf_header -open Elf_interpreted_segment -open Elf_interpreted_section -open Elf_program_header_table -open Elf_section_header_table -open Elf_symbol_table -open Elf_types_native_uint -open Elf_relocation -open Elf_types_native_uint -open Memory_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. - *) -let stt_gnu_ifunc : Nat_big_num.num= (Nat_big_num.of_int 10) - -(*val gnu_extend: forall 'abifeature. abi 'abifeature -> abi 'abifeature*) -let gnu_extend a:'abifeature abi= - ({ is_valid_elf_header = (a.is_valid_elf_header) - ; make_elf_header = -( (* t -> entry -> shoff -> phoff -> phnum -> shnum -> shstrndx -> hdr *)fun t -> fun entry -> fun shoff -> fun phoff -> fun phnum -> fun shnum -> fun shstrndx -> - let unmod = (a.make_elf_header t entry shoff phoff phnum shnum shstrndx) - in - { elf64_ident = ((match unmod.elf64_ident with - i0 :: i1 :: i2 :: i3 :: i4 :: i5 :: i6 :: - _ :: _ :: i9 :: i10 :: i11 :: i12 :: i13 :: i14 :: i15 :: [] - -> [i0; i1; i2; i3; i4; i5; i6; - Uint32.of_string (Nat_big_num.to_string elf_osabi_gnu); - Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1)); - i9; i10; i11; i12; i13; i14; i15] - )) - ; elf64_type = (Uint32.of_string (Nat_big_num.to_string t)) - ; elf64_machine = (unmod.elf64_machine) - ; elf64_version = (unmod.elf64_version) - ; elf64_entry = (unmod.elf64_entry) - ; elf64_phoff = (Uint64.of_string (Nat_big_num.to_string phoff)) - ; elf64_shoff = (Uint64.of_string (Nat_big_num.to_string shoff)) - ; elf64_flags = (unmod.elf64_flags) - ; elf64_ehsize = (unmod.elf64_ehsize) - ; elf64_phentsize= (unmod.elf64_phentsize) - ; elf64_phnum = (Uint32.of_string (Nat_big_num.to_string phnum)) - ; elf64_shentsize= (unmod.elf64_shentsize) - ; elf64_shnum = (Uint32.of_string (Nat_big_num.to_string shnum)) - ; elf64_shstrndx = (Uint32.of_string (Nat_big_num.to_string shstrndx)) - }) - ; reloc = (a.reloc) - ; section_is_special = (fun isec1 -> (fun img2 -> ( - a.section_is_special isec1 img2 - || ( -(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_int 1) 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 = (fun input_fnames_and_imgs -> - let vanilla_support_img = (a.generate_support input_fnames_and_imgs) in - (* also generate .note.gnu.build-id *) - let new_by_range = (Pset.add (Some(".note.gnu.build-id", (Nat_big_num.of_int 0,Nat_big_num.of_int 24)), FileFeature(ElfSection(Nat_big_num.of_int 4 (* HACK: calculate this *), - { elf64_section_name =(Nat_big_num.of_int 0) (* ignored *) - ; elf64_section_type = sht_note - ; elf64_section_flags = shf_alloc - ; elf64_section_addr =(Nat_big_num.of_int 0) (* ignored -- covered by element *) - ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored -- will be replaced when file offsets are assigned *) - ; elf64_section_size =(Nat_big_num.of_int 24) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *) - ; elf64_section_link =(Nat_big_num.of_int 0) - ; elf64_section_info =(Nat_big_num.of_int 0) - ; elf64_section_align =(Nat_big_num.of_int 4) - ; elf64_section_entsize =(Nat_big_num.of_int 0) - ; 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_int 24)) - ; contents = ([]) - } (vanilla_support_img.elements)) - ; by_tag = (by_tag_from_by_range - (instance_Basic_classes_SetType_Maybe_maybe_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))) instance_Basic_classes_SetType_var_dict new_by_range) - ; by_range = new_by_range - }) - ; concretise_support = (a.concretise_support) - ; get_reloc_symaddr = (a.get_reloc_symaddr) - }) diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_dynamic.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_dynamic.ml deleted file mode 100644 index e2957380..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_dynamic.ml +++ /dev/null @@ -1,531 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_dynamic.lem.*) -(** [gnu_ext_dynamic] contains GNU extension specific definitions related to the - * .dynamic section of an ELF file. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_num -open Lem_string - -open Error -open Show -open String_table - -open Elf_dynamic -open Elf_types_native_uint - -(** Additional dynamic entries, see LSB section 11.3.2.2. - * All values taken from elf.c from binutils and GLIBC as the LSB does not - * specify them. - * - * 98 #define OLD_DT_LOOS 0x60000000 - * 99 #define DT_LOOS 0x6000000d - * 100 #define DT_HIOS 0x6ffff000 - * 101 #define DT_VALRNGLO 0x6ffffd00 - * 102 #define DT_VALRNGHI 0x6ffffdff - * 103 #define DT_ADDRRNGLO 0x6ffffe00 - * 104 #define DT_ADDRRNGHI 0x6ffffeff - * 105 #define DT_VERSYM 0x6ffffff0 - * 106 #define DT_RELACOUNT 0x6ffffff9 - * 107 #define DT_RELCOUNT 0x6ffffffa - * 108 #define DT_FLAGS_1 0x6ffffffb - * 109 #define DT_VERDEF 0x6ffffffc - * 110 #define DT_VERDEFNUM 0x6ffffffd - * 111 #define DT_VERNEED 0x6ffffffe - * 112 #define DT_VERNEEDNUM 0x6fffffff - * 113 #define OLD_DT_HIOS 0x6fffffff - * 114 #define DT_LOPROC 0x70000000 - * 115 #define DT_HIPROC 0x7fffffff - *) - -let elf_dt_gnu_addrrnghi : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523967)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffeff*) -let elf_dt_gnu_addrrnglo : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 939523840)(Nat_big_num.of_int 2)) (*0x6ffffe00*) -let elf_dt_gnu_auxiliary : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 1073741822)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x7ffffffd*) -let elf_dt_gnu_filter : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 1073741823)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x7fffffff*) -(** The following is "specified" in the LSB document but is not present in the - * elf.c file so taken from elf.h from GLIBC: - *) -let elf_dt_gnu_num : Nat_big_num.num= (Nat_big_num.of_int 32) (** ??? This should match something *) -let elf_dt_gnu_posflag_1 : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523838)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffdfd*) -let elf_dt_gnu_relcount : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 939524093)(Nat_big_num.of_int 2)) (*0x6ffffffa*) -let elf_dt_gnu_relacount : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524092)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6FFFFFF9*) -let elf_dt_gnu_syminent : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523839)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffdff*) -let elf_dt_gnu_syminfo : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523967)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffeff*) -let elf_dt_gnu_syminsz : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 939523839)(Nat_big_num.of_int 2)) (*0x6ffffdfe*) -let elf_dt_gnu_valrnghi : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523839)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffdff*) -let elf_dt_gnu_valrnglo : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 939523712)(Nat_big_num.of_int 2)) (*0x6ffffd00*) -let elf_dt_gnu_verdef : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 939524094)(Nat_big_num.of_int 2)) (*0x6ffffffc*) -let elf_dt_gnu_verdefnum : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524094)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffffd*) -let elf_dt_gnu_verneed : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 939524095)(Nat_big_num.of_int 2)) (*0x6ffffffe*) -let elf_dt_gnu_verneednum : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524095)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6fffffff*) -let elf_dt_gnu_versym : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 939524088)(Nat_big_num.of_int 2)) (*0x6ffffff0*) - -(** Not present in the LSB but turns up in "real" ELF files... *) - -let elf_dt_gnu_hash : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939523962)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffef5*) -let elf_dt_gnu_flags_1 : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 939524093)(Nat_big_num.of_int 2))(Nat_big_num.of_int 1)) (*0x6ffffffb*) -let elf_dt_gnu_checksum : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 939523836)(Nat_big_num.of_int 2)) (* 0x6FFFFDF8 *) -let elf_dt_gnu_prelinked : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939523834))(Nat_big_num.of_int 1)) (* 0x6FFFFDF5 *) - -(** Extended DT flags for FLAGS_1 dynamic section types. Taken from GLibC source - * as they appear to be completely unspecified! - *) - -let gnu_df_1_now : Nat_big_num.num= (Nat_big_num.of_int 1) (*0x00000001*) -let gnu_df_1_global : Nat_big_num.num= (Nat_big_num.of_int 2) (*0x00000002*) -let gnu_df_1_group : Nat_big_num.num= (Nat_big_num.of_int 4) (*0x00000004*) -let gnu_df_1_nodelete : Nat_big_num.num= (Nat_big_num.of_int 8) (*0x00000008*) -let gnu_df_1_loadfltr : Nat_big_num.num= (Nat_big_num.of_int 16) (*0x00000010*) -let gnu_df_1_initfirst : Nat_big_num.num= (Nat_big_num.of_int 32) (*0x00000020*) -let gnu_df_1_noopen : Nat_big_num.num= (Nat_big_num.of_int 64) (*0x00000040*) -let gnu_df_1_origin : Nat_big_num.num= (Nat_big_num.of_int 128) (*0x00000080*) -let gnu_df_1_direct : Nat_big_num.num= (Nat_big_num.of_int 256) (*0x00000100*) -let gnu_df_1_trans : Nat_big_num.num= (Nat_big_num.of_int 512) (*0x00000200*) -let gnu_df_1_interpose : Nat_big_num.num= (Nat_big_num.of_int 1024) (*0x00000400*) -let gnu_df_1_nodeflib : Nat_big_num.num= (Nat_big_num.of_int 2048) (*0x00000800*) -let gnu_df_1_nodump : Nat_big_num.num= (Nat_big_num.of_int 4096) (*0x00001000*) -let gnu_df_1_confalt : Nat_big_num.num= (Nat_big_num.of_int 8192) (*0x00002000*) -let gnu_df_1_endfiltee : Nat_big_num.num= (Nat_big_num.of_int 16384) (*0x00004000*) -let gnu_df_1_dispreldne : Nat_big_num.num= (Nat_big_num.of_int 32768) (*0x00008000*) -let gnu_df_1_disprelpnd : Nat_big_num.num= (Nat_big_num.of_int 65536) (*0x00010000*) - -(** [gnu_string_of_dt_flag1 m] produces a string based representation of GNU - * extensions flag_1 value [m]. - *) -(*val gnu_string_of_dt_flag_1 : natural -> string*) -let gnu_string_of_dt_flag_1 flag:string= - (if check_flag flag(Nat_big_num.of_int 0) then - "None" - else if check_flag flag gnu_df_1_now then - "NOW" - else if check_flag flag gnu_df_1_global then - "GLOBAL" - else if check_flag flag gnu_df_1_group then - "GROUP" - else if check_flag flag gnu_df_1_nodelete then - "NODELETE" - else if check_flag flag gnu_df_1_loadfltr then - "LOADFLTR" - else if check_flag flag gnu_df_1_initfirst then - "INITFIRST" - else if check_flag flag gnu_df_1_noopen then - "NOOPEN" - else if check_flag flag gnu_df_1_origin then - "ORIGIN" - else if check_flag flag gnu_df_1_direct then - "DIRECT" - else if check_flag flag gnu_df_1_trans then - "TRANS" - else if check_flag flag gnu_df_1_interpose then - "INTERPOSE" - else if check_flag flag gnu_df_1_nodeflib then - "NODEFLIB" - else if check_flag flag gnu_df_1_nodump then - "NODUMP" - else if check_flag flag gnu_df_1_confalt then - "CONFALT" - else if check_flag flag gnu_df_1_endfiltee then - "ENDFILTEE" - else if check_flag flag gnu_df_1_dispreldne then - "DISPRELDNE" - else if check_flag flag gnu_df_1_disprelpnd then - "DISPRELPND" - else if check_flag flag ( Nat_big_num.add gnu_df_1_nodelete gnu_df_1_now) then - "NOW NODELETE" - else if check_flag flag ( Nat_big_num.add gnu_df_1_nodelete gnu_df_1_initfirst) then - "NODELETE INITFIRST" - else (* XXX: add more as necessary *) - "Invalid GNU dynamic flag") - -(** [gnu_ext_os_additional_ranges m] checks whether dynamic section type [m] - * lies within the ranges set aside for GNU specific functionality. - * NB: quite ad hoc as this is not properly specified anywhere. - *) -(*val gnu_ext_os_additional_ranges : natural -> bool*) -let gnu_ext_os_additional_ranges m:bool= - (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then - true - else Nat_big_num.equal (* ad hoc extensions go here... *) - m elf_dt_gnu_verneed || (Nat_big_num.equal - m elf_dt_gnu_verneednum || (Nat_big_num.equal - m elf_dt_gnu_versym || (Nat_big_num.equal - m elf_dt_gnu_verdef || (Nat_big_num.equal - m elf_dt_gnu_verdefnum || (Nat_big_num.equal - m elf_dt_gnu_flags_1 || (Nat_big_num.equal - m elf_dt_gnu_relcount || (Nat_big_num.equal - m elf_dt_gnu_relacount || (Nat_big_num.equal - m elf_dt_gnu_checksum || Nat_big_num.equal - m elf_dt_gnu_prelinked))))))))) - -(** [gnu_ext_tag_correspondence_of_tag0 m] produces a tag correspondence for the - * extended GNU-specific dynamic section types [m]. Used to provide the ABI - * specific functionality expected of the corresponding function in the elf_dynamic - * module. - *) -(*val gnu_ext_tag_correspondence_of_tag0 : natural -> error tag_correspondence*) -let gnu_ext_tag_correspondence_of_tag0 m:(tag_correspondence)error= - (if Nat_big_num.equal m elf_dt_gnu_hash then - return C_Ptr - else if Nat_big_num.equal m elf_dt_gnu_flags_1 then - return C_Val - else if Nat_big_num.equal m elf_dt_gnu_versym then - return C_Ptr - else if Nat_big_num.equal m elf_dt_gnu_verneednum then - return C_Val - else if Nat_big_num.equal m elf_dt_gnu_verneed then - return C_Ptr - else if Nat_big_num.equal m elf_dt_gnu_verdef then - return C_Ptr - else if Nat_big_num.equal m elf_dt_gnu_verdefnum then - return C_Val - else if Nat_big_num.equal m elf_dt_gnu_relcount then - return C_Val - else if Nat_big_num.equal m elf_dt_gnu_relacount then - return C_Val - else if Nat_big_num.equal m elf_dt_gnu_checksum then - return C_Val - else if Nat_big_num.equal m elf_dt_gnu_prelinked then - return C_Val - else - fail "gnu_ext_tag_correspondence_of_tag0: invalid dynamic tag") - -(** [gnu_ext_tag_correspondence_of_tag m] produces a tag correspondence for the - * extended GNU-specific dynamic section types [m]. Used to provide the ABI - * specific functionality expected of the corresponding function in the elf_dynamic - * module. - * TODO: examine whether this and the function above really need separating into - * two functions. - *) -(*val gnu_ext_tag_correspondence_of_tag : natural -> error tag_correspondence*) -let gnu_ext_tag_correspondence_of_tag m:(tag_correspondence)error= - (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then - return C_Ptr - else if Nat_big_num.greater_equal m elf_dt_gnu_valrnglo && Nat_big_num.less_equal m elf_dt_gnu_valrnghi then - return C_Val - else if gnu_ext_os_additional_ranges m then - gnu_ext_tag_correspondence_of_tag0 m - else if Nat_big_num.equal m elf_dt_gnu_syminsz then - return C_Val (** unsure *) - else if Nat_big_num.equal m elf_dt_gnu_syminfo then - return C_Ptr (** unsure *) - else if Nat_big_num.equal m elf_dt_gnu_syminent then - return C_Val (** unsure *) - else if Nat_big_num.equal m elf_dt_gnu_posflag_1 then - return C_Val (** unsure *) - else if Nat_big_num.equal m elf_dt_gnu_num then - return C_Ignored - else if Nat_big_num.equal m elf_dt_gnu_filter then - return C_Val (** unsure *) - else if Nat_big_num.equal m elf_dt_gnu_auxiliary then - return C_Val (** unsure *) - else - fail ("gnu_ext_tag_correspondence_of_tag: unrecognised GNU dynamic tag")) - -(** [gnu_ext_elf32_value_of_elf32_dyn0 dyn] extracts a dynamic value from the - * dynamic section entry [dyn] under the assumption that its type is a GNU - * extended dynamic section type. Fails otherwise. Used to provide the - * ABI-specific functionality expected of the corresponding functions in - * elf_dynamic.lem. - *) -(*val gnu_ext_elf32_value_of_elf32_dyn0 : elf32_dyn -> string_table -> error elf32_dyn_value*) -let gnu_ext_elf32_value_of_elf32_dyn0 dyn stbl:(((Uint32.uint32),(Uint32.uint32))dyn_value)error= - (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in - if Nat_big_num.equal tag elf_dt_gnu_hash then - (match dyn.elf32_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_HASH must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_HASH must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_flags_1 then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: FLAGS_1 must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: FlAGS_1 must be a Val" - ) >>= (fun f -> - return (Flags1 (Nat_big_num.of_string (Uint32.to_string f)))) - else if Nat_big_num.equal tag elf_dt_gnu_versym then - (match dyn.elf32_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERSYM must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERSYM must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_verdef then - (match dyn.elf32_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEF must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEF must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_verdefnum then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEFNUM must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEFNUM must be a Val" - ) >>= (fun sz -> - return (Numeric (Nat_big_num.of_string (Uint32.to_string sz)))) - else if Nat_big_num.equal tag elf_dt_gnu_verneednum then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEEDNUM must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEEDNUM must be a Val" - ) >>= (fun sz -> - return (Numeric (Nat_big_num.of_string (Uint32.to_string sz)))) - else if Nat_big_num.equal tag elf_dt_gnu_verneed then - (match dyn.elf32_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEED must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEED must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_relcount then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELCOUNT must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELCOUNT must be a Val" - ) >>= (fun sz -> - return (Numeric (Nat_big_num.of_string (Uint32.to_string sz)))) - else if Nat_big_num.equal tag elf_dt_gnu_relacount then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELACOUNT must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELACOUNT must be a Val" - ) >>= (fun sz -> - return (Numeric (Nat_big_num.of_string (Uint32.to_string sz)))) - else if Nat_big_num.equal tag elf_dt_gnu_checksum then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: CHECKSUM must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: CHECKSUM must be a Val" - ) >>= (fun sz -> - return (Checksum (Nat_big_num.of_string (Uint32.to_string sz)))) - else if Nat_big_num.equal tag elf_dt_gnu_prelinked then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_PRELINKED must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_PRELINKED must be a Val" - ) >>= (fun off -> - return (Timestamp (Nat_big_num.of_string (Uint32.to_string off)))) - else - fail "gnu_ext_elf32_value_of_elf32_dyn0: unrecognised GNU dynamic tag") - -(** [gnu_ext_elf64_value_of_elf64_dyn0 dyn] extracts a dynamic value from the - * dynamic section entry [dyn] under the assumption that its type is a GNU - * extended dynamic section type. Fails otherwise. Used to provide the - * ABI-specific functionality expected of the corresponding functions in - * elf_dynamic.lem. - *) -(*val gnu_ext_elf64_value_of_elf64_dyn0 : elf64_dyn -> string_table -> error elf64_dyn_value*) -let gnu_ext_elf64_value_of_elf64_dyn0 dyn stbl:(((Uint64.uint64),(Uint64.uint64))dyn_value)error= - (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in - if Nat_big_num.equal tag elf_dt_gnu_hash then - (match dyn.elf64_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_HASH must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_HASH must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_flags_1 then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: FLAGS_1 must be a Val" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: FlAGS_1 must be a Val" - ) >>= (fun f -> - return (Flags1 (Ml_bindings.nat_big_num_of_uint64 f))) - else if Nat_big_num.equal tag elf_dt_gnu_versym then - (match dyn.elf64_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERSYM must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERSYM must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_verdef then - (match dyn.elf64_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERDEF must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERDEF must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_verdefnum then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf64_dyn: VERDEFNUM must be a Val" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf64_dyn: VERDEFNUM must be a Val" - ) >>= (fun sz -> - return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz))) - else if Nat_big_num.equal tag elf_dt_gnu_verneednum then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEEDNUM must be a Val" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEEDNUM must be a Val" - ) >>= (fun sz -> - return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz))) - else if Nat_big_num.equal tag elf_dt_gnu_verneed then - (match dyn.elf64_dyn_d_un with - | D_Val v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEED must be a PTR" - | D_Ptr p -> return p - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEED must be a PTR" - ) >>= (fun addr -> - return (Address addr)) - else if Nat_big_num.equal tag elf_dt_gnu_relcount then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELCOUNT must be a Val" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELCOUNT must be a Val" - ) >>= (fun sz -> - return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz))) - else if Nat_big_num.equal tag elf_dt_gnu_relacount then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELACOUNT must be a Val" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELACOUNT must be a Val" - ) >>= (fun sz -> - return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz))) - else if Nat_big_num.equal tag elf_dt_gnu_checksum then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: CHECKSUM must be a Val" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: CHECKSUM must be a Val" - ) >>= (fun sz -> - return (Checksum (Ml_bindings.nat_big_num_of_uint64 sz))) - else if Nat_big_num.equal tag elf_dt_gnu_prelinked then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_PRELINKED must be a Val" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_PRELINKED must be a Val" - ) >>= (fun off -> - return (Timestamp (Ml_bindings.nat_big_num_of_uint64 off))) - else - fail "gnu_ext_elf64_value_of_elf64_dyn0: unrecognised GNU dynamic tag") - -(** [gnu_ext_elf32_value_of_elf32_dyn dyn] extracts a dynamic value from the - * dynamic section entry [dyn] under the assumption that its type is a GNU - * extended dynamic section type. Fails otherwise. Used to provide the - * ABI-specific functionality expected of the corresponding functions in - * elf_dynamic.lem. - * TODO: some of these cases are missing as they have never come up in "real" - * ELF files that have been processed as part of validation. Try and find some - * files that do actually exhibit these. - *) -(*val gnu_ext_elf32_value_of_elf32_dyn : elf32_dyn -> string_table -> error elf32_dyn_value*) -let gnu_ext_elf32_value_of_elf32_dyn dyn stbl:(elf32_dyn_value)error= - (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in - if gnu_ext_os_additional_ranges tag then (* this should cover valrngs and addrrngs *) - gnu_ext_elf32_value_of_elf32_dyn0 dyn stbl - else if Nat_big_num.equal tag elf_dt_gnu_syminsz then - (match dyn.elf32_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf32_value_of_elf32_dyn: SYMINSZ must be a VAL" - | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: SYMINSZ must be a VAL" - ) >>= (fun sz -> - return (Size sz)) - else if Nat_big_num.equal tag elf_dt_gnu_syminfo then - fail "SYMINFO" (* XXX: never seen in 32-bit ELF *) - else if Nat_big_num.equal tag elf_dt_gnu_syminent then - fail "SYMINENT" (* XXX: never seen in 32-bit ELF *) - else if Nat_big_num.equal tag elf_dt_gnu_posflag_1 then - fail "POSFLAG_1" (* XXX: never seen in 32-bit ELF *) - else if Nat_big_num.equal tag elf_dt_gnu_num then - fail "NUM" (* XXX: never seen in 32-bit ELF *) - else if Nat_big_num.equal tag elf_dt_gnu_filter then - fail "FILTER" (* XXX: never seen in 32-bit ELF *) - else if Nat_big_num.equal tag elf_dt_gnu_auxiliary then - fail "AUXILIARY" (* XXX: never seen in 32-bit ELF *) - else - fail "gnu_ext_elf32_value_of_elf32_dyn: unrecognised GNU dynamic tag") - -(** [gnu_ext_elf64_value_of_elf64_dyn dyn] extracts a dynamic value from the - * dynamic section entry [dyn] under the assumption that its type is a GNU - * extended dynamic section type. Fails otherwise. Used to provide the - * ABI-specific functionality expected of the corresponding functions in - * elf_dynamic.lem. - * TODO: some of these cases are missing as they have never come up in "real" - * ELF files that have been processed as part of validation. Try and find some - * files that do actually exhibit these. - *) -(*val gnu_ext_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*) -let gnu_ext_elf64_value_of_elf64_dyn dyn stbl:(elf64_dyn_value)error= - (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in - if gnu_ext_os_additional_ranges tag then (* this should cover valrngs and addrrngs *) - gnu_ext_elf64_value_of_elf64_dyn0 dyn stbl - else if Nat_big_num.equal tag elf_dt_gnu_syminsz then - (match dyn.elf64_dyn_d_un with - | D_Val v -> return v - | D_Ptr p -> fail "gnu_ext_elf64_value_of_elf64_dyn: SYMINSZ must be a VAL" - | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: SYMINSZ must be a VAL" - ) >>= (fun sz -> - return (Size sz)) - else if Nat_big_num.equal tag elf_dt_gnu_syminfo then - fail "SYMINFO" (* XXX: fill in as seen *) - else if Nat_big_num.equal tag elf_dt_gnu_syminent then - fail "SYMINENT" (* XXX: fill in as seen *) - else if Nat_big_num.equal tag elf_dt_gnu_posflag_1 then - fail "POSFLAG_1" (* XXX: fill in as seen *) - else if Nat_big_num.equal tag elf_dt_gnu_num then - fail "NUM" (* XXX: fill in as seen *) - else if Nat_big_num.equal tag elf_dt_gnu_filter then - fail "FILTER" (* XXX: fill in as seen *) - else if Nat_big_num.equal tag elf_dt_gnu_auxiliary then - fail "AUXILIARY" (* XXX: fill in as seen *) - else - fail "gnu_ext_elf64_value_of_elf64_dyn: unrecognised GNU dynamic tag") - -(** [string_of_gnu_ext_dynamic_tag0 m] produces a string based representation of - * GNU extensions dynamic tag value [m]. - *) -(*val string_of_gnu_ext_dynamic_tag0 : natural -> string*) -let string_of_gnu_ext_dynamic_tag0 m:string= - (if Nat_big_num.equal m elf_dt_gnu_hash then - "GNU_HASH" - else if Nat_big_num.equal m elf_dt_gnu_flags_1 then - "FLAGS_1" - else if Nat_big_num.equal m elf_dt_gnu_versym then - "VERSYM" - else if Nat_big_num.equal m elf_dt_gnu_verneednum then - "VERNEEDNUM" - else if Nat_big_num.equal m elf_dt_gnu_verneed then - "VERNEED" - else if Nat_big_num.equal m elf_dt_gnu_relcount then - "RELCOUNT" - else if Nat_big_num.equal m elf_dt_gnu_relacount then - "RELACOUNT" - else if Nat_big_num.equal m elf_dt_gnu_verdefnum then - "VERDEFNUM" - else if Nat_big_num.equal m elf_dt_gnu_verdef then - "VERDEF" - else if Nat_big_num.equal m elf_dt_gnu_checksum then - "CHECKSUM" - else if Nat_big_num.equal m elf_dt_gnu_prelinked then - "GNU_PRELINKED" - else - "Invalid dynamic tag") - -(** [string_of_gnu_ext_dynamic_tag m] produces a string based representation of - * GNU extensions dynamic tag value [m]. - *) -(*val string_of_gnu_ext_dynamic_tag : natural -> string*) -let string_of_gnu_ext_dynamic_tag m:string= - (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then - string_of_gnu_ext_dynamic_tag0 m - else if Nat_big_num.greater_equal m elf_dt_gnu_valrnglo && Nat_big_num.less_equal m elf_dt_gnu_valrnghi then - string_of_gnu_ext_dynamic_tag0 m - else if gnu_ext_os_additional_ranges m then - string_of_gnu_ext_dynamic_tag0 m - else if Nat_big_num.equal m elf_dt_gnu_syminsz then - "SYMINSZ" - else if Nat_big_num.equal m elf_dt_gnu_syminfo then - "SYMINFO" - else if Nat_big_num.equal m elf_dt_gnu_syminent then - "SYMINENT" - else if Nat_big_num.equal m elf_dt_gnu_posflag_1 then - "POSFLAG_1" - else if Nat_big_num.equal m elf_dt_gnu_num then - "NUM" - else if Nat_big_num.equal m elf_dt_gnu_filter then - "FILTER" - else if Nat_big_num.equal m elf_dt_gnu_auxiliary then - "AUXILIARY" - else - "Invalid dynamic tag") diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_note.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_note.ml deleted file mode 100644 index f8f4328f..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_note.ml +++ /dev/null @@ -1,268 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_note.lem.*) -(** [gnu_ext_note] contains GNU extension specific definitions relating to the - * .note section/segment of an ELF file. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_list -open Lem_maybe -open Lem_string - -open Byte_sequence -open Endianness -open Error -open Missing_pervasives -open String_table - -open Elf_note -open Elf_section_header_table -open Elf_types_native_uint - -open Gnu_ext_section_header_table - -(** The following two functions are utility functions to convert a list of bytes - * into words, ready for further processing into strings. - *) - -(*val group_elf32_words : endianness -> list byte -> error (list elf32_word)*) -let rec group_elf32_words endian xs:((Uint32.uint32)list)error= - ((match xs with - | [] -> return [] - | x1::x2::x3::x4::xs -> - let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in - read_elf32_word endian bs0 >>= (fun (w, _) -> - group_elf32_words endian xs >>= (fun ws -> - return (w::ws))) - | xs -> fail "group_elf32_words: the impossible happened" - )) - -(*val group_elf64_words : endianness -> list byte -> error (list elf64_word)*) -let rec group_elf64_words endian xs:((Uint32.uint32)list)error= - ((match xs with - | [] -> return [] - | x1::x2::x3::x4::xs -> - let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in - read_elf64_word endian bs0 >>= (fun (w, _) -> - group_elf64_words endian xs >>= (fun ws -> - return (w::ws))) - | xs -> fail "group_elf64_words: the impossible happened" - )) - -(** [gnu_ext_check_elf32_abi_note_tag_section endain sht stbl bs0] checks the - * .note.ABI-tag section of an ELF file to ensure conformance with the GNU - * extensions. The string in this note should contain the string "GNU". - *) -(*val gnu_ext_check_elf32_abi_note_tag_section : endianness -> elf32_section_header_table -> - string_table -> byte_sequence -> bool*) -let gnu_ext_check_elf32_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool= - (let abi_note_sects = -(List.filter (fun x -> - if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_type)) sht_note then - let nm = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name)) in - (match String_table.get_string_at nm sect_hdr_tbl with - | Success name1 -> name1 = ".note.ABI-tag" - | Fail _ -> false - ) - else - false - ) sht) - in - (match abi_note_sects with - | [note] -> - let off = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_offset)) in - let siz = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_size)) in - let abi_tag = -(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> - Elf_note.read_elf32_note endian rel >>= (fun (abi_tag, _) -> - return abi_tag))) - in - (match abi_tag with - | Fail _ -> false - | Success abi_tag -> - let str = (name_string_of_elf32_note abi_tag) in - if str = "GNU\000" then - if Nat_big_num.greater_equal (Nat_big_num.of_string (Uint32.to_string abi_tag.elf32_note_descsz))(Nat_big_num.of_int 16) then - let take2 = (Lem_list.take( 16) abi_tag.elf32_note_desc) in - if List.length take2 < 16 then - false - else - true - else - false - else - false - ) - | _ -> - false - )) - -(** [gnu_ext_check_elf64_abi_note_tag_section endain sht stbl bs0] checks the - * .note.ABI-tag section of an ELF file to ensure conformance with the GNU - * extensions. The string in this note should contain the string "GNU". - *) -(*val gnu_ext_check_elf64_abi_note_tag_section : endianness -> elf64_section_header_table -> - string_table -> byte_sequence -> bool*) -let gnu_ext_check_elf64_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool= - (let abi_note_sects = -(List.filter (fun x -> - if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_type)) sht_note then - let nm = (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name)) in - (match String_table.get_string_at nm sect_hdr_tbl with - | Success name1 -> name1 = ".note.ABI-tag" - | Fail _ -> false - ) - else - false - ) sht) - in - (match abi_note_sects with - | [note] -> - let off = (Nat_big_num.of_string (Uint64.to_string note.elf64_sh_offset)) in - let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in - let abi_tag = -(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> - Elf_note.read_elf64_note endian rel >>= (fun (abi_tag, _) -> - return abi_tag))) - in - (match abi_tag with - | Fail _ -> false - | Success abi_tag -> - let str = (name_string_of_elf64_note abi_tag) in - if str = "GNU\000" then - if Nat_big_num.greater_equal (Ml_bindings.nat_big_num_of_uint64 abi_tag.elf64_note_descsz)(Nat_big_num.of_int 16) then - let take2 = (Lem_list.take( 16) abi_tag.elf64_note_desc) in - if List.length take2 < 16 then - false - else - true - else - false - else - false - ) - | _ -> - false - )) - -(** [gnu_ext_extract_elf32_earliest_compatible_kernel end sht stab bs0] extracts - * the earliest compatible Linux kernel with the given ELF file from its section - * header table [sht], and string table [stbl], assuming endianness [endian]. - * NB: marked as OCaml only as need to extract a string from integers. - * TODO: implement some string parsing functions in Isabelle/HOL so things like - * this can be extracted. - *) -(*val gnu_ext_extract_elf32_earliest_compatible_kernel : endianness -> elf32_section_header_table -> - string_table -> byte_sequence -> error string*) -let gnu_ext_extract_elf32_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error= - (let abi_note_sects = -(List.filter (fun x -> - if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_type)) sht_note then - let nm = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name)) in - (match String_table.get_string_at nm sect_hdr_tbl with - | Success name1 -> name1 = ".note.ABI-tag" - | Fail _ -> false - ) - else - false - ) sht) - in - (match abi_note_sects with - | [note] -> - let off = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_offset)) in - let siz = (Nat_big_num.of_string (Uint32.to_string note.elf32_sh_size)) in - let abi_tag = -(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> - Elf_note.read_elf32_note endian rel >>= (fun (abi_tag, _) -> - return abi_tag))) - in - (match abi_tag with - | Fail _ -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: parsing of NOTE section failed" - | Success abi_tag -> - let str = (name_string_of_elf32_note abi_tag) in - if str = "GNU\000" then - if Nat_big_num.greater_equal (Nat_big_num.of_string (Uint32.to_string abi_tag.elf32_note_descsz))(Nat_big_num.of_int 16) then - let take2 = (Lem_list.take( 16) abi_tag.elf32_note_desc) in - if List.length take2 < 16 then - fail "gnu_ext_extract_elf32_earliest_compatible_kernel: the impossible happened" - else - (match group_elf32_words endian take2 with - | Fail err -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: word grouping failed" - | Success ss -> - (match ss with - | c1::c2::c3::cs -> - let c1 = (Uint32.to_string c1) in - let c2 = (Uint32.to_string c2) in - let c3 = (Uint32.to_string c3) in - return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "") - | _ -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: kernel version must have three components" - ) - ) - else - fail "gnu_ext_extract_elf32_earliest_compatible_kernel: .note.ABI-tag description size not required length" - else - fail "gnu_ext_extract_elf32_earliest_compatible_kernel: required GNU string not present" - ) - | _ -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: more than one .note.ABI-tag section present" - )) - -(** [gnu_ext_extract_elf64_earliest_compatible_kernel end sht stab bs0] extracts - * the earliest compatible Linux kernel with the given ELF file from its section - * header table [sht], and string table [stbl], assuming endianness [endian]. - * NB: marked as OCaml only as need to extract a string from integers. - * TODO: implement some string parsing functions in Isabelle/HOL so things like - * this can be extracted. - *) -(*val gnu_ext_extract_elf64_earliest_compatible_kernel : endianness -> elf64_section_header_table -> - string_table -> byte_sequence -> error string*) -let gnu_ext_extract_elf64_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error= - (let abi_note_sects = -(List.filter (fun x -> - if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_type)) sht_note then - let nm = (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name)) in - (match String_table.get_string_at nm sect_hdr_tbl with - | Success name1 -> name1 = ".note.ABI-tag" - | Fail _ -> false - ) - else - false - ) sht) - in - (match abi_note_sects with - | [note] -> - let off = (Nat_big_num.of_string (Uint64.to_string note.elf64_sh_offset)) in - let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in - let abi_tag = -(Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> - Elf_note.read_elf64_note endian rel >>= (fun (abi_tag, _) -> - return abi_tag))) - in - (match abi_tag with - | Fail _ -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: parsing of NOTE section failed" - | Success abi_tag -> - let str = (name_string_of_elf64_note abi_tag) in - if str = "GNU\000" then - if Nat_big_num.greater_equal (Ml_bindings.nat_big_num_of_uint64 abi_tag.elf64_note_descsz)(Nat_big_num.of_int 16) then - let take2 = (Lem_list.take( 16) abi_tag.elf64_note_desc) in - if List.length take2 < 16 then - fail "gnu_ext_extract_elf64_earliest_compatible_kernel: the impossible happened" - else - (match group_elf64_words endian take2 with - | Fail err -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: word grouping failed" - | Success ss -> - (match ss with - | c1::c2::c3::cs -> - let c1 = (Uint32.to_string c1) in - let c2 = (Uint32.to_string c2) in - let c3 = (Uint32.to_string c3) in - return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "") - | _ -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: kernel version must have three components" - ) - ) - else - fail "gnu_ext_extract_elf64_earliest_compatible_kernel: .note.ABI-tag description size not required length" - else - fail "gnu_ext_extract_elf64_earliest_compatible_kernel: required GNU string not present" - ) - | _ -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: more than one .note.ABI-tag section present" - )) diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_program_header_table.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_program_header_table.ml deleted file mode 100644 index 4c5b78c1..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_program_header_table.ml +++ /dev/null @@ -1,34 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_program_header_table.lem.*) -(** [gnu_ext_program_header_table] contains GNU extension specific functionality - * related to the program header table. - *) - -open Lem_basic_classes -open Lem_num - -(** GNU extensions, as defined in the LSB, see section 11.2. *) - -(** The element specifies the location and size of a segment that may be made - * read-only after relocations have been processed. - *) -let elf_pt_gnu_relro : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 421345620))(Nat_big_num.of_int 2)) (* 0x6474e552 *) -(** The [p_flags] member specifies the permissions of the segment containing the - * stack and is used to indicate whether the stack should be executable. - *) -let elf_pt_gnu_stack : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 421345620))(Nat_big_num.of_int 1)) (* 0x6474e551 *) -(** Element specifies the location and size of exception handling information. *) -let elf_pt_gnu_eh_frame : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 421345620)) (* 0x6474e550 *) - -(** [string_of_gnu_ext_segment_type m] produces a string representation of - * GNU extension segment type [m]. - *) -(*val string_of_gnu_ext_segment_type : natural -> string*) -let string_of_gnu_ext_segment_type pt:string= - (if Nat_big_num.equal pt elf_pt_gnu_relro then - "GNU_RELRO" - else if Nat_big_num.equal pt elf_pt_gnu_stack then - "GNU_STACK" - else if Nat_big_num.equal pt elf_pt_gnu_eh_frame then - "GNU_EH_FRAME" - else - "Invalid GNU EXT segment type") diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_header_table.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_header_table.ml deleted file mode 100644 index 98faa8e4..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_header_table.ml +++ /dev/null @@ -1,151 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_section_header_table.lem.*) -(** The module [gnu_ext_section_header_table] implements function, definitions - * and types relating to the GNU extensions to the standard ELF section header - * table. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_map -open Lem_maybe -open Lem_num -open Lem_string - -open Hex_printing - -open Error -open String_table -open Show - -open Elf_section_header_table -open Elf_interpreted_section - -(** GNU extended section types *) - -(** [GNU_HASH] does not appear to be defined in the LSB but is present in - * several ELF binaries collected in the wild... - * - * TODO: find out where this comes from? - * ANSW: a mailing list apparently! See here: - * https://sourceware.org/ml/binutils/2006-10/msg00377.html - *) -let sht_gnu_hash : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524091)) (* 0x6FFFFFF6 *) - -(** The following are all defined in Section 10.2.2.2 of the LSB as additional - * section types over the ones defined in the SCO ELF spec. - *) - -(** [sht_gnu_verdef] contains the symbol versions that are provided. - *) -let sht_gnu_verdef : Nat_big_num.num= (Nat_big_num.sub_nat ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095))(Nat_big_num.of_int 1)) (* 0x6ffffffd *) -(** [sht_gnu_verneed] contains the symbol versions that are required. - *) -let sht_gnu_verneed : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095)) (* 0x6ffffffe *) -(** [sht_gnu_versym] contains the symbol version table. - *) -let sht_gnu_versym : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095))(Nat_big_num.of_int 1)) (* 0x6fffffff *) -(** [sht_gnu_liblist] appears to be undocumented but appears in PowerPC 64 ELF - * binaries in "the wild". - *) -let sht_gnu_liblist : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524091))(Nat_big_num.of_int 1)) (* 0x6FFFFFF7 *) - -(** [string_of_gnu_ext_section_type m] produces a string based representation of - * GNU extension section type [m]. - *) -(*val string_of_gnu_ext_section_type : natural -> string*) -let string_of_gnu_ext_section_type i:string= - (if Nat_big_num.equal i sht_gnu_hash then - "GNU_HASH" - else if Nat_big_num.equal i sht_gnu_verdef then - "VERDEF" - else if Nat_big_num.equal i sht_gnu_verneed then - "VERNEED" - else if Nat_big_num.equal i sht_gnu_versym then - "VERSYM" - else if Nat_big_num.equal i sht_gnu_liblist then - "GNU_LIBLIST" - else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then - let diff = (Nat_big_num.sub_nat i sht_loos) in - let suff = (unsafe_hex_string_of_natural( 0) diff) in - "LOOS+" ^ suff - else - "Invalid GNU EXT section type: " ^ Nat_big_num.to_string i) - -(** [gnu_ext_additionall_special_sections] records additional section names that - * map appear in GNU ELF binaries and their required associated types and - * attributes. See Section 10.3.1.1 of the LSB and the related map - * [elf_special_sections] in [Elf_section_header_table] which records section - * names and their required types and attributes that all ELF binaries share. - *) -(*val gnu_ext_additional_special_sections : Map.map string (natural * natural)*) -let gnu_ext_additional_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map= - (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [ - (".ctors", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".data.rel.ro", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".dtors", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".eh_frame", (sht_progbits, shf_alloc)) - ; (".eh_frame_hdr", (sht_progbits, shf_alloc)) - ; (".gcc_execpt_table", (sht_progbits, shf_alloc)) - ; (".gnu.version", (sht_gnu_versym, shf_alloc)) - ; (".gnu.version_d", (sht_gnu_verdef, shf_alloc)) - ; (".gnu.version_r", (sht_gnu_verneed, shf_alloc)) - ; (".got.plt", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".jcr", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".note.ABI-tag", (sht_note, shf_alloc)) - ; (".stab", (sht_progbits,Nat_big_num.of_int 0)) - ; (".stabstr", (sht_strtab,Nat_big_num.of_int 0)) - ]) - -(** [is_valid_gnu_ext_elf32_section_header_table_entry scts stbl] checks whether - * sections [scts] conforms with the contents of the special sections table. - * Fails otherwise. - *) -(*val is_valid_gnu_ext_elf32_section_header_table_entry : elf32_interpreted_section -> - string_table -> bool*) -let is_valid_gnu_ext_elf32_section_header_table_entry ent stbl:bool= - ((match String_table.get_string_at ent.elf32_section_name stbl with - | Fail f -> false - | Success name1 -> - (match Pmap.lookup name1 gnu_ext_additional_special_sections with - | None -> - is_valid_elf32_section_header_table_entry ent stbl - | Some (typ, flags) -> Nat_big_num.equal - typ ent.elf32_section_type && Nat_big_num.equal flags ent.elf32_section_flags - ) - )) - -(** [is_valid_gnu_ext_elf32_section_header_table sht stbl] checks whether every - * member of the section header table [sht] conforms with the special sections - * table. - *) -(*val is_valid_gnu_ext_elf32_section_header_table : list elf32_interpreted_section -> - string_table -> bool*) -let is_valid_gnu_ext_elf32_section_header_table ents stbl:bool= - (List.for_all (fun x -> is_valid_gnu_ext_elf32_section_header_table_entry x stbl) ents) - -(** [is_valid_gnu_ext_elf64_section_header_table_entry scts stbl] checks whether - * sections [scts] conforms with the contents of the special sections table. - * Fails otherwise. - *) -(*val is_valid_gnu_ext_elf64_section_header_table_entry : elf64_interpreted_section -> - string_table -> bool*) -let is_valid_gnu_ext_elf64_section_header_table_entry ent stbl:bool= - ((match String_table.get_string_at ent.elf64_section_name stbl with - | Fail f -> false - | Success name1 -> - (match Pmap.lookup name1 gnu_ext_additional_special_sections with - | None -> - is_valid_elf64_section_header_table_entry ent stbl - | Some (typ, flags) -> Nat_big_num.equal - typ ent.elf64_section_type && Nat_big_num.equal flags ent.elf64_section_flags - ) - )) - -(** [is_valid_gnu_ext_elf64_section_header_table sht stbl] checks whether every - * member of the section header table [sht] conforms with the special sections - * table. - *) -(*val is_valid_gnu_ext_elf64_section_header_table : list elf64_interpreted_section -> - string_table -> bool*) -let is_valid_gnu_ext_elf64_section_header_table ents stbl:bool= - (List.for_all (fun x -> is_valid_gnu_ext_elf64_section_header_table_entry x stbl) ents) diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_to_segment_mapping.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_to_segment_mapping.ml deleted file mode 100644 index 86a5c5ed..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_section_to_segment_mapping.ml +++ /dev/null @@ -1,265 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_section_to_segment_mapping.lem.*) -(** [gnu_ext_section_to_segment_mapping] contains (GNU specific) functionality - * relating to calculating the section to segment mapping for an ELF file. In - * particular, the test over whether a section is inside a segment is ABI - * specific. This module provides that test. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_num - -open Elf_header -open Elf_program_header_table -open Elf_section_header_table -open Elf_types_native_uint - -open Lem_string -open Show - -open Gnu_ext_program_header_table - -(** [elf32_section_in_segment sec_hdr segment] implements the - * ELF_SECTION_IN_SEGMENT1 macro from readelf. Note the macro is always used - * with [check_vma] and [strict] set to 1. - * - #define ELF_SECTION_IN_SEGMENT_1(sec_hdr, segment, check_vma, strict) \ - ((/* Only PT_LOAD, PT_GNU_RELRO and PT_TLS segments can contain \ - SHF_TLS sections. */ \ - ((((sec_hdr)->sh_flags & SHF_TLS) != 0) \ - && ((segment)->p_type == PT_TLS \ - || (segment)->p_type == PT_GNU_RELRO \ - || (segment)->p_type == PT_LOAD)) \ - /* PT_TLS segment contains only SHF_TLS sections, PT_PHDR no \ - sections at all. */ \ - || (((sec_hdr)->sh_flags & SHF_TLS) == 0 \ - && (segment)->p_type != PT_TLS \ - && (segment)->p_type != PT_PHDR)) \ - /* PT_LOAD and similar segments only have SHF_ALLOC sections. */ \ - && !(((sec_hdr)->sh_flags & SHF_ALLOC) == 0 \ - && ((segment)->p_type == PT_LOAD \ - || (segment)->p_type == PT_DYNAMIC \ - || (segment)->p_type == PT_GNU_EH_FRAME \ - || (segment)->p_type == PT_GNU_RELRO \ - || (segment)->p_type == PT_GNU_STACK)) \ - /* Any section besides one of type SHT_NOBITS must have file \ - offsets within the segment. */ \ - && ((sec_hdr)->sh_type == SHT_NOBITS \ - || ((bfd_vma) (sec_hdr)->sh_offset >= (segment)->p_offset \ - && (!(strict) \ - || ((sec_hdr)->sh_offset - (segment)->p_offset \ - <= (segment)->p_filesz - 1)) \ - && (((sec_hdr)->sh_offset - (segment)->p_offset \ - + ELF_SECTION_SIZE(sec_hdr, segment)) \ - <= (segment)->p_filesz))) \ - /* SHF_ALLOC sections must have VMAs within the segment. */ \ - && (!(check_vma) \ - || ((sec_hdr)->sh_flags & SHF_ALLOC) == 0 \ - || ((sec_hdr)->sh_addr >= (segment)->p_vaddr \ - && (!(strict) \ - || ((sec_hdr)->sh_addr - (segment)->p_vaddr \ - <= (segment)->p_memsz - 1)) \ - && (((sec_hdr)->sh_addr - (segment)->p_vaddr \ - + ELF_SECTION_SIZE(sec_hdr, segment)) \ - <= (segment)->p_memsz))) \ - /* No zero size sections at start or end of PT_DYNAMIC. */ \ - && ((segment)->p_type != PT_DYNAMIC \ - || (sec_hdr)->sh_size != 0 \ - || (segment)->p_memsz == 0 \ - || (((sec_hdr)->sh_type == SHT_NOBITS \ - || ((bfd_vma) (sec_hdr)->sh_offset > (segment)->p_offset \ - && ((sec_hdr)->sh_offset - (segment)->p_offset \ - < (segment)->p_filesz))) \ - && (((sec_hdr)->sh_flags & SHF_ALLOC) == 0 \ - || ((sec_hdr)->sh_addr > (segment)->p_vaddr \ - && ((sec_hdr)->sh_addr - (segment)->p_vaddr \ - < (segment)->p_memsz)))))) - * - * From [internal.h] of readelf's source code. - *) - -(*val elf32_section_flags : elf32_section_header_table_entry -> natural -> bool*) -let elf32_section_flags0 sec_hdr typ:bool= (not ((Uint32.logand sec_hdr.elf32_sh_flags (Uint32.of_string (Nat_big_num.to_string typ))) = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) - -(*val elf64_section_flags : elf64_section_header_table_entry -> natural -> bool*) -let elf64_section_flags0 sec_hdr typ:bool= (not ((Uint64.logand sec_hdr.elf64_sh_flags (Uint64.of_string (Nat_big_num.to_string typ))) = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) - -(*val elf32_section_of_type : elf32_section_header_table_entry -> natural -> bool*) -let elf32_section_of_type sec_hdr typ:bool= - (sec_hdr.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string typ)) - -(*val elf64_section_of_type : elf64_section_header_table_entry -> natural -> bool*) -let elf64_section_of_type sec_hdr typ:bool= - (sec_hdr.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string typ)) - -(*val elf32_segment_of_type : elf32_program_header_table_entry -> natural -> bool*) -let elf32_segment_of_type segment typ:bool= - (segment.elf32_p_type = Uint32.of_string (Nat_big_num.to_string typ)) - -(*val elf64_segment_of_type : elf64_program_header_table_entry -> natural -> bool*) -let elf64_segment_of_type segment typ:bool= - (segment.elf64_p_type = Uint32.of_string (Nat_big_num.to_string typ)) - -(** Only PT_LOAD, PT_GNU_RELRO and PT_TLS segments can contain SHF_TLS sections - * and PT_TLS segment contains only SHF_TLS sections, PT_PHDR no sections at all - *) -(*val elf32_section_in_segment1 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let elf32_section_in_segment1 sec_hdr segment:bool= - ((elf32_section_flags0 sec_hdr shf_tls && - (elf32_segment_of_type segment elf_pt_tls || -(elf32_segment_of_type segment elf_pt_gnu_relro || - elf32_segment_of_type segment elf_pt_load))) || - (not (elf32_section_flags0 sec_hdr shf_tls) - && (not (elf32_segment_of_type segment elf_pt_tls) - && not (elf32_segment_of_type segment elf_pt_phdr)))) - -(*val elf64_section_in_segment1 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let elf64_section_in_segment1 sec_hdr segment:bool= - ((elf64_section_flags0 sec_hdr shf_tls && - (elf64_segment_of_type segment elf_pt_tls || -(elf64_segment_of_type segment elf_pt_gnu_relro || - elf64_segment_of_type segment elf_pt_load))) || - (not (elf64_section_flags0 sec_hdr shf_tls) - && (not (elf64_segment_of_type segment elf_pt_tls) - && not (elf64_segment_of_type segment elf_pt_phdr)))) - -(** PT_LOAD and similar segments only have SHF_ALLOC sections *) - -(*val elf32_section_in_segment2 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let elf32_section_in_segment2 sec_hdr segment:bool= - (not ((not (elf32_section_flags0 sec_hdr shf_alloc)) && - (elf32_segment_of_type segment elf_pt_load || -(elf32_segment_of_type segment elf_pt_dynamic || -(elf32_segment_of_type segment elf_pt_gnu_eh_frame || -(elf32_segment_of_type segment elf_pt_gnu_relro || - elf32_segment_of_type segment elf_pt_gnu_stack)))))) - -(*val elf64_section_in_segment2 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let elf64_section_in_segment2 sec_hdr segment:bool= - (not ((not (elf64_section_flags0 sec_hdr shf_alloc)) && - (elf64_segment_of_type segment elf_pt_load || -(elf64_segment_of_type segment elf_pt_dynamic || -(elf64_segment_of_type segment elf_pt_gnu_eh_frame || -(elf64_segment_of_type segment elf_pt_gnu_relro || - elf64_segment_of_type segment elf_pt_gnu_stack)))))) - - -(** Any section besides one of type SHT_NOBITS must have file offsets within - * the segment. - *) - -(*val elf32_sect_size : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> natural*) -let elf32_sect_size hdr sec_hdr segment:Nat_big_num.num= - (if is_elf32_tbss_special sec_hdr segment then Nat_big_num.of_int 0 - else - Nat_big_num.of_string (Uint32.to_string (hdr.elf32_shentsize))) - -(*val elf64_sect_size : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> natural*) -let elf64_sect_size hdr sec_hdr segment:Nat_big_num.num= - (if is_elf64_tbss_special sec_hdr segment then Nat_big_num.of_int 0 - else - Nat_big_num.of_string (Uint32.to_string (hdr.elf64_shentsize))) - -(*val elf32_section_in_segment3 : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let elf32_section_in_segment3 hdr sec_hdr segment:bool= - (let sec_off = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_offset))) in - let seg_off = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_offset))) in - let seg_fsz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_filesz))) in - let sec_siz = ((elf32_sect_size hdr sec_hdr segment)) in - elf32_section_of_type sec_hdr sht_nobits || - ( Nat_big_num.greater_equal sec_off seg_off && -(( Nat_big_num.less_equal( Nat_big_num.sub sec_off seg_off) ( Nat_big_num.sub seg_fsz(Nat_big_num.of_int 1))) && - ( Nat_big_num.less_equal (Nat_big_num.sub sec_off ( Nat_big_num.add seg_off sec_siz)) seg_fsz)))) - -(*val elf64_section_in_segment3 : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let elf64_section_in_segment3 hdr sec_hdr segment:bool= - (let sec_off = ((Nat_big_num.of_string (Uint64.to_string sec_hdr.elf64_sh_offset))) in - let seg_off = ((Nat_big_num.of_string (Uint64.to_string segment.elf64_p_offset))) in - let seg_fsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_filesz)) in - let sec_siz = ((elf64_sect_size hdr sec_hdr segment)) in - elf64_section_of_type sec_hdr sht_nobits || - ( Nat_big_num.greater_equal sec_off seg_off && -(( Nat_big_num.less_equal( Nat_big_num.sub sec_off seg_off) ( Nat_big_num.sub seg_fsz(Nat_big_num.of_int 1))) && - ( Nat_big_num.less_equal (Nat_big_num.sub sec_off ( Nat_big_num.add seg_off sec_siz)) seg_fsz)))) - -(** SHF_ALLOC sections must have VMAs within the segment - *) - -(*val elf32_section_in_segment4 : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let elf32_section_in_segment4 hdr sec_hdr segment:bool= - (let sec_addr = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_addr))) in - let seg_vadr = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_vaddr))) in - let seg_mmsz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_memsz))) in - let sec_size = ((elf32_sect_size hdr sec_hdr segment)) in - (not (elf32_section_flags0 sec_hdr shf_alloc) || Nat_big_num.greater_equal - sec_addr seg_vadr) && (Nat_big_num.less_equal (Nat_big_num.sub - sec_addr seg_vadr) (Nat_big_num.sub seg_mmsz(Nat_big_num.of_int 1)) && Nat_big_num.less_equal (Nat_big_num.sub - sec_addr ( Nat_big_num.add seg_vadr sec_size)) seg_mmsz)) - -(*val elf64_section_in_segment4 : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let elf64_section_in_segment4 hdr sec_hdr segment:bool= - (let sec_addr = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_addr)) in - let seg_vadr = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_vaddr)) in - let seg_mmsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_memsz)) in - let sec_size = ((elf64_sect_size hdr sec_hdr segment)) in - (not (elf64_section_flags0 sec_hdr shf_alloc) || Nat_big_num.greater_equal - sec_addr seg_vadr) && (Nat_big_num.less_equal (Nat_big_num.sub - sec_addr seg_vadr) (Nat_big_num.sub seg_mmsz(Nat_big_num.of_int 1)) && Nat_big_num.less_equal (Nat_big_num.sub - sec_addr ( Nat_big_num.add seg_vadr sec_size)) seg_mmsz)) - -(** No zero size sections at start or end of PT_DYNAMIC *) - -(*val elf32_section_in_segment5 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let elf32_section_in_segment5 sec_hdr segment:bool= - (let sec_siz = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_size))) in - let seg_msz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_memsz))) in - let sec_off = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_offset))) in - let seg_off = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_offset))) in - let seg_fsz = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_filesz))) in - let sec_adr = ((Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_addr))) in - let seg_vad = ((Nat_big_num.of_string (Uint32.to_string segment.elf32_p_vaddr))) in - (not (elf32_segment_of_type segment elf_pt_dynamic)) || (not (Nat_big_num.equal sec_siz(Nat_big_num.of_int 0)) || (Nat_big_num.equal - seg_msz(Nat_big_num.of_int 0) || - ((elf32_section_of_type sec_hdr sht_nobits || - ( Nat_big_num.greater sec_off seg_off && Nat_big_num.less (Nat_big_num.sub - sec_off seg_off) seg_fsz)) && - (not (elf32_section_flags0 sec_hdr shf_alloc) || - ( Nat_big_num.greater sec_adr seg_vad && Nat_big_num.less (Nat_big_num.sub - sec_adr seg_vad) seg_msz)))))) - -(*val elf64_section_in_segment5 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let elf64_section_in_segment5 sec_hdr segment:bool= - (let sec_siz = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_size)) in - let seg_msz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_memsz)) in - let sec_off = ((Nat_big_num.of_string (Uint64.to_string sec_hdr.elf64_sh_offset))) in - let seg_off = ((Nat_big_num.of_string (Uint64.to_string segment.elf64_p_offset))) in - let seg_fsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_filesz)) in - let sec_adr = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_addr)) in - let seg_vad = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_vaddr)) in - (not (elf64_segment_of_type segment elf_pt_dynamic)) || (not (Nat_big_num.equal sec_siz(Nat_big_num.of_int 0)) || (Nat_big_num.equal - seg_msz(Nat_big_num.of_int 0) || - ((elf64_section_of_type sec_hdr sht_nobits || - ( Nat_big_num.greater sec_off seg_off && Nat_big_num.less (Nat_big_num.sub - sec_off seg_off) seg_fsz)) && - (not (elf64_section_flags0 sec_hdr shf_alloc) || - ( Nat_big_num.greater sec_adr seg_vad && Nat_big_num.less (Nat_big_num.sub - sec_adr seg_vad) seg_msz)))))) - -(** The final section in segment tests, bringing all the above together. - *) - -(*val elf32_section_in_segment : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let elf32_section_in_segment hdr sec_hdr segment:bool= - (elf32_section_in_segment1 sec_hdr segment && -(elf32_section_in_segment2 sec_hdr segment && -(elf32_section_in_segment3 hdr sec_hdr segment && -(elf32_section_in_segment4 hdr sec_hdr segment && - elf32_section_in_segment5 sec_hdr segment)))) - -(*val elf64_section_in_segment : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let elf64_section_in_segment hdr sec_hdr segment:bool= - (elf64_section_in_segment1 sec_hdr segment && -(elf64_section_in_segment2 sec_hdr segment && -(elf64_section_in_segment3 hdr sec_hdr segment && -(elf64_section_in_segment4 hdr sec_hdr segment && - elf64_section_in_segment5 sec_hdr segment)))) diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_symbol_versioning.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_symbol_versioning.ml deleted file mode 100644 index fe9382b0..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_symbol_versioning.ml +++ /dev/null @@ -1,294 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_symbol_versioning.lem.*) -(** The [gnu_ext_symbol_versioning] defines constants, types and functions - * relating to the GNU symbol versioning extensions (i.e. contents of - * GNU_VERSYM sections). - * - * TODO: work out what is going on with symbol versioning. The specification - * is completely opaque. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_list -open Lem_maybe -open Lem_num -open Lem_string - -open Byte_sequence -open Endianness -open Error - -open Elf_dynamic -open Elf_file -open Elf_header -open Elf_section_header_table -open Elf_symbol_table -open Elf_types_native_uint - -open Missing_pervasives -open Show - -open Gnu_ext_dynamic -open Gnu_ext_section_header_table - -(** [gnu_ext_elf32_symbol_version_table] is an array (linked list, here) of - * [elf32_half] entries. - *) -type gnu_ext_elf32_symbol_version_table = Uint32.uint32 - list - -type gnu_ext_elf64_symbol_version_table = Uint32.uint32 - list - -(*val obtain_gnu_ext_elf32_symbol_version_table : elf32_file -> byte_sequence -> error gnu_ext_elf32_symbol_version_table*) -let obtain_gnu_ext_elf32_symbol_version_table f1 bs0:((Uint32.uint32)list)error= - (let sht = (f1.elf32_file_section_header_table) in - let endian = (get_elf32_header_endianness f1.elf32_file_header) in - let vers = (List.filter (fun ent -> - ent.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_gnu_versym) - ) sht) - in - (match vers with - | [] -> return [] - | [ver] -> - let off = (Nat_big_num.of_string (Uint32.to_string ver.elf32_sh_offset)) in - let siz = (Nat_big_num.of_string (Uint32.to_string ver.elf32_sh_size)) in - let lnk = (Nat_big_num.of_string (Uint32.to_string ver.elf32_sh_link)) in - get_elf32_symbol_table_by_index f1 lnk >>= (fun symtab -> - let dlen = (Nat_big_num.of_int (List.length symtab)) in - Byte_sequence.offset_and_cut off siz bs0 >>= (fun ver -> - Error.repeatM' dlen bs0 (read_elf32_half endian) >>= (fun (ver, _) -> - return ver))) - | _ -> fail "obtain_gnu_ext_elf32_symbol_version_table: multiple sections of type .gnu_versym present in file" - )) - -(*val obtain_gnu_ext_elf64_symbol_version_table : endianness -> elf64_section_header_table -> elf64_symbol_table -> byte_sequence -> error gnu_ext_elf64_symbol_version_table*) -let obtain_gnu_ext_elf64_symbol_version_table endian sht dynsym bs0:((Uint32.uint32)list)error= - (let dlen = (Nat_big_num.of_int (List.length dynsym)) in - if Nat_big_num.equal dlen(Nat_big_num.of_int 0) then - return [] - else - let vers = (List.filter (fun ent -> - ent.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_gnu_versym) - ) sht) - in - (match vers with - | [] -> return [] - | [ver] -> - let off = (Nat_big_num.of_string (Uint64.to_string ver.elf64_sh_offset)) in - let siz = (Ml_bindings.nat_big_num_of_uint64 ver.elf64_sh_size) in - Byte_sequence.offset_and_cut off siz bs0 >>= (fun ver -> - Error.repeatM' dlen bs0 (read_elf64_half endian) >>= (fun (ver, _) -> - return ver)) - | _ -> fail "obtain_gnu_ext_elf64_symbol_version_table: multiple sections of type .gnu_versym present in file" - )) - -type gnu_ext_elf32_verdef = - { gnu_ext_elf32_vd_version : Uint32.uint32 - ; gnu_ext_elf32_vd_flags : Uint32.uint32 - ; gnu_ext_elf32_vd_ndx : Uint32.uint32 - ; gnu_ext_elf32_vd_cnt : Uint32.uint32 - ; gnu_ext_elf32_vd_hash : Uint32.uint32 - ; gnu_ext_elf32_vd_aux : Uint32.uint32 - ; gnu_ext_elf32_vd_next : Uint32.uint32 - } - -type gnu_ext_elf64_verdef = - { gnu_ext_elf64_vd_version : Uint32.uint32 - ; gnu_ext_elf64_vd_flags : Uint32.uint32 - ; gnu_ext_elf64_vd_ndx : Uint32.uint32 - ; gnu_ext_elf64_vd_cnt : Uint32.uint32 - ; gnu_ext_elf64_vd_hash : Uint32.uint32 - ; gnu_ext_elf64_vd_aux : Uint32.uint32 - ; gnu_ext_elf64_vd_next : Uint32.uint32 - } - -(*val string_of_gnu_ext_elf32_verdef : gnu_ext_elf32_verdef -> string*) -let string_of_gnu_ext_elf32_verdef verdef:string= - (unlines [ -("Version: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_version) - ; ("Flags: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_flags) - ; ("Index: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_ndx) - ; ("Count: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_cnt) - ; ("Hash: " ^ Uint32.to_string verdef.gnu_ext_elf32_vd_hash) - ]) - -(*val string_of_gnu_ext_elf64_verdef : gnu_ext_elf64_verdef -> string*) -let string_of_gnu_ext_elf64_verdef verdef:string= - (unlines [ -("Version: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_version) - ; ("Flags: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_flags) - ; ("Index: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_ndx) - ; ("Count: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_cnt) - ; ("Hash: " ^ Uint32.to_string verdef.gnu_ext_elf64_vd_hash) - ]) - -(*val read_gnu_ext_elf32_verdef : endianness -> byte_sequence -> error (gnu_ext_elf32_verdef * byte_sequence)*) -let read_gnu_ext_elf32_verdef endian bs0:(gnu_ext_elf32_verdef*byte_sequence)error= - (read_elf32_half endian bs0 >>= (fun (ver, bs0) -> - read_elf32_half endian bs0 >>= (fun (flg, bs0) -> - read_elf32_half endian bs0 >>= (fun (ndx, bs0) -> - read_elf32_half endian bs0 >>= (fun (cnt, bs0) -> - read_elf32_word endian bs0 >>= (fun (hsh, bs0) -> - read_elf32_word endian bs0 >>= (fun (aux, bs0) -> - read_elf32_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf32_vd_version = ver; gnu_ext_elf32_vd_flags = flg; - gnu_ext_elf32_vd_ndx = ndx; gnu_ext_elf32_vd_cnt = cnt; - gnu_ext_elf32_vd_hash = hsh; gnu_ext_elf32_vd_aux = aux; - gnu_ext_elf32_vd_next = nxt }, bs0))))))))) - -(*val read_gnu_ext_elf64_verdef : endianness -> byte_sequence -> error (gnu_ext_elf64_verdef * byte_sequence)*) -let read_gnu_ext_elf64_verdef endian bs0:(gnu_ext_elf64_verdef*byte_sequence)error= - (read_elf64_half endian bs0 >>= (fun (ver, bs0) -> - read_elf64_half endian bs0 >>= (fun (flg, bs0) -> - read_elf64_half endian bs0 >>= (fun (ndx, bs0) -> - read_elf64_half endian bs0 >>= (fun (cnt, bs0) -> - read_elf64_word endian bs0 >>= (fun (hsh, bs0) -> - read_elf64_word endian bs0 >>= (fun (aux, bs0) -> - read_elf64_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf64_vd_version = ver; gnu_ext_elf64_vd_flags = flg; - gnu_ext_elf64_vd_ndx = ndx; gnu_ext_elf64_vd_cnt = cnt; - gnu_ext_elf64_vd_hash = hsh; gnu_ext_elf64_vd_aux = aux; - gnu_ext_elf64_vd_next = nxt }, bs0))))))))) - -(*val gnu_ext_elf32_verdef_size : natural*) -let gnu_ext_elf32_verdef_size:Nat_big_num.num= (Nat_big_num.of_int 160) - -(*val gnu_ext_elf64_verdef_size : natural*) -let gnu_ext_elf64_verdef_size:Nat_big_num.num= (Nat_big_num.of_int 256) - -type gnu_ext_elf32_veraux = - { gnu_ext_elf32_vda_name : Uint32.uint32 - ; gnu_ext_elf32_vda_next : Uint32.uint32 - } - -type gnu_ext_elf64_veraux = - { gnu_ext_elf64_vda_name : Uint32.uint32 - ; gnu_ext_elf64_vda_next : Uint32.uint32 - } - -(*val gnu_ext_elf32_veraux_size : natural*) -let gnu_ext_elf32_veraux_size:Nat_big_num.num= (Nat_big_num.of_int 64) - -(*val gnu_ext_elf64_veraux_size : natural*) -let gnu_ext_elf64_veraux_size:Nat_big_num.num= (Nat_big_num.of_int 128) - -(*val read_gnu_ext_elf32_veraux : endianness -> byte_sequence -> error (gnu_ext_elf32_veraux * byte_sequence)*) -let read_gnu_ext_elf32_veraux endian bs0:(gnu_ext_elf32_veraux*byte_sequence)error= - (read_elf32_word endian bs0 >>= (fun (nme, bs0) -> - read_elf32_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf32_vda_name = nme; gnu_ext_elf32_vda_next = nxt }, bs0)))) - -(*val read_gnu_ext_elf64_veraux : endianness -> byte_sequence -> error (gnu_ext_elf64_veraux * byte_sequence)*) -let read_gnu_ext_elf64_veraux endian bs0:(gnu_ext_elf64_veraux*byte_sequence)error= - (read_elf64_word endian bs0 >>= (fun (nme, bs0) -> - read_elf64_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf64_vda_name = nme; gnu_ext_elf64_vda_next = nxt }, bs0)))) - -type gnu_ext_elf32_verneed = - { gnu_ext_elf32_vn_version : Uint32.uint32 - ; gnu_ext_elf32_vn_cnt : Uint32.uint32 - ; gnu_ext_elf32_vn_file : Uint32.uint32 - ; gnu_ext_elf32_vn_aux : Uint32.uint32 - ; gnu_ext_elf32_vn_next : Uint32.uint32 - } - -type gnu_ext_elf64_verneed = - { gnu_ext_elf64_vn_version : Uint32.uint32 - ; gnu_ext_elf64_vn_cnt : Uint32.uint32 - ; gnu_ext_elf64_vn_file : Uint32.uint32 - ; gnu_ext_elf64_vn_aux : Uint32.uint32 - ; gnu_ext_elf64_vn_next : Uint32.uint32 - } - -(*val gnu_ext_elf32_verneed_size : natural*) -let gnu_ext_elf32_verneed_size:Nat_big_num.num= (Nat_big_num.of_int 128) - -(*val gnu_ext_elf64_verneed_size : natural*) -let gnu_ext_elf64_verneed_size:Nat_big_num.num= (Nat_big_num.of_int 224) - -(*val read_gnu_ext_elf32_verneed : endianness -> byte_sequence -> error (gnu_ext_elf32_verneed * byte_sequence)*) -let read_gnu_ext_elf32_verneed endian bs0:(gnu_ext_elf32_verneed*byte_sequence)error= - (read_elf32_half endian bs0 >>= (fun (ver, bs0) -> - read_elf32_half endian bs0 >>= (fun (cnt, bs0) -> - read_elf32_word endian bs0 >>= (fun (fle, bs0) -> - read_elf32_word endian bs0 >>= (fun (aux, bs0) -> - read_elf32_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf32_vn_version = ver; gnu_ext_elf32_vn_cnt = cnt; - gnu_ext_elf32_vn_file = fle; gnu_ext_elf32_vn_aux = aux; - gnu_ext_elf32_vn_next = nxt }, bs0))))))) - -(*val read_gnu_ext_elf64_verneed : endianness -> byte_sequence -> error (gnu_ext_elf64_verneed * byte_sequence)*) -let read_gnu_ext_elf64_verneed endian bs0:(gnu_ext_elf64_verneed*byte_sequence)error= - (read_elf64_half endian bs0 >>= (fun (ver, bs0) -> - read_elf64_half endian bs0 >>= (fun (cnt, bs0) -> - read_elf64_word endian bs0 >>= (fun (fle, bs0) -> - read_elf64_word endian bs0 >>= (fun (aux, bs0) -> - read_elf64_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf64_vn_version = ver; gnu_ext_elf64_vn_cnt = cnt; - gnu_ext_elf64_vn_file = fle; gnu_ext_elf64_vn_aux = aux; - gnu_ext_elf64_vn_next = nxt }, bs0))))))) - -type gnu_ext_elf32_vernaux = - { gnu_ext_elf32_vna_hash : Uint32.uint32 - ; gnu_ext_elf32_vna_flags : Uint32.uint32 - ; gnu_ext_elf32_vna_other : Uint32.uint32 - ; gnu_ext_elf32_vna_name : Uint32.uint32 - ; gnu_ext_elf32_vna_next : Uint32.uint32 - } - -type gnu_ext_elf64_vernaux = - { gnu_ext_elf64_vna_hash : Uint32.uint32 - ; gnu_ext_elf64_vna_flags : Uint32.uint32 - ; gnu_ext_elf64_vna_other : Uint32.uint32 - ; gnu_ext_elf64_vna_name : Uint32.uint32 - ; gnu_ext_elf64_vna_next : Uint32.uint32 - } - -(*val string_of_gnu_ext_elf32_vernaux : gnu_ext_elf32_vernaux -> string*) -let string_of_gnu_ext_elf32_vernaux vernaux:string= - (unlines [ -("Hash: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_hash) - ; ("Flags: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_flags) - ; ("Other: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_other) - ; ("Name: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_name) - ; ("Next: " ^ Uint32.to_string vernaux.gnu_ext_elf32_vna_next) - ]) - -(*val string_of_gnu_ext_elf64_vernaux : gnu_ext_elf64_vernaux -> string*) -let string_of_gnu_ext_elf64_vernaux vernaux:string= - (unlines [ -("Hash: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_hash) - ; ("Flags: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_flags) - ; ("Other: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_other) - ; ("Name: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_name) - ; ("Next: " ^ Uint32.to_string vernaux.gnu_ext_elf64_vna_next) - ]) - -(*val gnu_ext_elf32_vernaux_size : natural*) -let gnu_ext_elf32_vernaux_size:Nat_big_num.num= (Nat_big_num.of_int 16) - -(*val gnu_ext_elf64_vernaux_size : natural*) -let gnu_ext_elf64_vernaux_size:Nat_big_num.num= (Nat_big_num.of_int 224) - -(*val read_gnu_ext_elf32_vernaux : endianness -> byte_sequence -> error (gnu_ext_elf32_vernaux * byte_sequence)*) -let read_gnu_ext_elf32_vernaux endian bs0:(gnu_ext_elf32_vernaux*byte_sequence)error= - (read_elf32_word endian bs0 >>= (fun (hsh, bs0) -> - read_elf32_half endian bs0 >>= (fun (flg, bs0) -> - read_elf32_half endian bs0 >>= (fun (otr, bs0) -> - read_elf32_word endian bs0 >>= (fun (nme, bs0) -> - read_elf32_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf32_vna_hash = hsh; gnu_ext_elf32_vna_flags = flg; - gnu_ext_elf32_vna_other = otr; gnu_ext_elf32_vna_name = nme; - gnu_ext_elf32_vna_next = nxt }, bs0))))))) - -(*val read_gnu_ext_elf64_vernaux : endianness -> byte_sequence -> error (gnu_ext_elf64_vernaux * byte_sequence)*) -let read_gnu_ext_elf64_vernaux endian bs0:(gnu_ext_elf64_vernaux*byte_sequence)error= - (read_elf64_word endian bs0 >>= (fun (hsh, bs0) -> - read_elf64_half endian bs0 >>= (fun (flg, bs0) -> - read_elf64_half endian bs0 >>= (fun (otr, bs0) -> - read_elf64_word endian bs0 >>= (fun (nme, bs0) -> - read_elf64_word endian bs0 >>= (fun (nxt, bs0) -> - return ({ gnu_ext_elf64_vna_hash = hsh; gnu_ext_elf64_vna_flags = flg; - gnu_ext_elf64_vna_other = otr; gnu_ext_elf64_vna_name = nme; - gnu_ext_elf64_vna_next = nxt }, bs0))))))) diff --git a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_types_native_uint.ml b/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_types_native_uint.ml deleted file mode 100644 index ec4be185..00000000 --- a/lib/ocaml_rts/linksem/gnu_extensions/gnu_ext_types_native_uint.ml +++ /dev/null @@ -1,12 +0,0 @@ -(*Generated by Lem from gnu_extensions/gnu_ext_types_native_uint.lem.*) -(** [gnu_ext_types_native_uint] provides extended types defined by the GNU - * extensions over and above the based ELF types. - *) - -open Missing_pervasives -open Elf_types_native_uint - -(** LSB section 9.2.1.1: in addition to SCO ELF spec types GNU defines an - * additional 1-byte integral type. - *) -type gnu_ext_byte = char |