diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_section_header_table.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_section_header_table.ml | 1187 |
1 files changed, 0 insertions, 1187 deletions
diff --git a/lib/ocaml_rts/linksem/elf_section_header_table.ml b/lib/ocaml_rts/linksem/elf_section_header_table.ml deleted file mode 100644 index b750c103..00000000 --- a/lib/ocaml_rts/linksem/elf_section_header_table.ml +++ /dev/null @@ -1,1187 +0,0 @@ -(*Generated by Lem from elf_section_header_table.lem.*) -(** [elf_section_header_table] provides types, functions and other definitions - * for working with section header tables and their entries. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_function -open Lem_list -open Lem_map -open Lem_maybe -open Lem_num -open Lem_string - -open Byte_sequence -open Error -open Missing_pervasives -open Show - -open Endianness -open String_table - -open Elf_header -open Elf_types_native_uint -open Elf_program_header_table - -(** Special section indices. *) - -(** See elf_header.lem for shn_undef *) - -(** [shn_loreserve]: this specifies the lower bound of the range of reserved - * indices. - *) -let shn_loreserve : Nat_big_num.num= (Nat_big_num.of_int 65280) (* 0xff00 *) -(** [shn_loproc]: start of the range reserved for processor-specific semantics. - *) -let shn_loproc : Nat_big_num.num= (Nat_big_num.of_int 65280) (* 0xff00 *) -(** [shn_hiproc]: end of the range reserved for processor-specific semantics. - *) -let shn_hiproc : Nat_big_num.num= (Nat_big_num.of_int 65311) (* 0xff1f *) -(** [shn_loos]: start of the range reserved for operating system-specific - * semantics. - *) -let shn_loos : Nat_big_num.num= (Nat_big_num.of_int 65312) (* 0xff20 *) -(** [shn_hios]: end of the range reserved for operating system-specific - * semantics. - *) -let shn_hios : Nat_big_num.num= (Nat_big_num.of_int 65343) (* 0xff3f *) -(** [shn_abs]: specifies the absolute values for the corresponding reference. - * Symbols defined relative to section number [shn_abs] have absolute values - * and are not affected by relocation. - *) -let shn_abs : Nat_big_num.num= (Nat_big_num.of_int 65521) (* 0xfff1 *) -(** [shn_common]: symbols defined relative to this index are common symbols, - * such as unallocated C external variables. - *) -let shn_common : Nat_big_num.num= (Nat_big_num.of_int 65522) (* 0xfff2 *) - -(** See elf_header.lem for shn_xindex. *) - -(** [shn_hireserve]: specifies the upper-bound of reserved values. - *) -let shn_hireserve : Nat_big_num.num= (Nat_big_num.of_int 65535) (* 0xffff *) - -(** [string_of_special_section_index m] produces a string-based representation - * of a section header entry's special section index, [m]. - *) -(*val string_of_special_section_index : natural -> string*) -let string_of_special_section_index i:string= - (if Nat_big_num.equal i shn_undef then - "SHN_UNDEF" - else if Nat_big_num.equal i shn_loreserve then - "SHN_LORESERVE" - else if Nat_big_num.greater_equal i shn_loproc && Nat_big_num.less_equal i shn_hiproc then - "SHN_PROCESSOR_SPECIFIC" - else if Nat_big_num.greater_equal i shn_loos && Nat_big_num.less_equal i shn_hios then - "SHN_OS_SPECIFIC" - else if Nat_big_num.equal i shn_abs then - "SHN_ABS" - else if Nat_big_num.equal i shn_common then - "SHN_COMMON" - else if Nat_big_num.equal i shn_xindex then - "SHN_XINDEX" - else if Nat_big_num.equal i shn_hireserve then - "SHN_HIRESERVE" - else - "SHN UNDEFINED") - -(** Section types. *) - -(** Marks the section header as being inactive. *) -let sht_null : Nat_big_num.num= (Nat_big_num.of_int 0) -(** Section holds information defined by the program. *) -let sht_progbits : Nat_big_num.num= (Nat_big_num.of_int 1) -(** The following two section types hold a symbol table. An object file may only - * have one symbol table of each of the respective types. The symtab provides - * a place for link editing, whereas the dynsym section holds a minimal set of - * dynamic linking symbols - *) -let sht_symtab : Nat_big_num.num= (Nat_big_num.of_int 2) -let sht_dynsym : Nat_big_num.num= (Nat_big_num.of_int 11) -(** Section holds a string table *) -let sht_strtab : Nat_big_num.num= (Nat_big_num.of_int 3) -(** Section holds relocation entries with explicit addends. An object file may - * have multiple section of this type. - *) -let sht_rela : Nat_big_num.num= (Nat_big_num.of_int 4) -(** Section holds a symbol hash table. An object file may only have a single - * hash table. - *) -let sht_hash : Nat_big_num.num= (Nat_big_num.of_int 5) -(** Section holds information for dynamic linking. An object file may only have - * a single dynamic section. - *) -let sht_dynamic : Nat_big_num.num= (Nat_big_num.of_int 6) -(** Section holds information that marks the file in some way. *) -let sht_note : Nat_big_num.num= (Nat_big_num.of_int 7) -(** Section occupies no space in the file but otherwise resembles a progbits - * section. - *) -let sht_nobits : Nat_big_num.num= (Nat_big_num.of_int 8) -(** Section holds relocation entries without explicit addends. An object file - * may have multiple section of this type. - *) -let sht_rel : Nat_big_num.num= (Nat_big_num.of_int 9) -(** Section type is reserved but has an unspecified meaning. *) -let sht_shlib : Nat_big_num.num= (Nat_big_num.of_int 10) -(** Section contains an array of pointers to initialisation functions. Each - * pointer is taken as a parameterless function with a void return type. - *) -let sht_init_array : Nat_big_num.num= (Nat_big_num.of_int 14) -(** Section contains an array of pointers to termination functions. Each - * pointer is taken as a parameterless function with a void return type. - *) -let sht_fini_array : Nat_big_num.num= (Nat_big_num.of_int 15) -(** Section contains an array of pointers to initialisation functions that are - * invoked before all other initialisation functions. Each - * pointer is taken as a parameterless function with a void return type. - *) -let sht_preinit_array : Nat_big_num.num= (Nat_big_num.of_int 16) -(** Section defines a section group, i.e. a set of sections that are related and - * must be treated especially by the linker. May only appear in relocatable - * objects. - *) -let sht_group : Nat_big_num.num= (Nat_big_num.of_int 17) -(** Section is associated with sections of type SHT_SYMTAB and is required if - * any of the section header indices referenced by that symbol table contains - * the escape value SHN_XINDEX. - * - * FIXME: Lem bug as [int] type used throughout Lem codebase, rather than - * [BigInt.t], so Lem chokes on these large constants below, hence the weird - * way in which they are written. - *) -let sht_symtab_shndx : Nat_big_num.num= (Nat_big_num.of_int 18) - -(** The following ranges are reserved solely for OS-, processor- and user- - * specific semantics, respectively. - *) -let sht_loos : Nat_big_num.num= (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul(Nat_big_num.of_int 3)(Nat_big_num.of_int 1024))(Nat_big_num.of_int 1024))(Nat_big_num.of_int 512)) (* 1610612736 (* 0x60000000 *) *) -let sht_hios : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 469762047)(Nat_big_num.of_int 4))(Nat_big_num.of_int 3)) (* 1879048191 (* 0x6fffffff *) *) -let sht_loproc : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 469762048)(Nat_big_num.of_int 4)) (* 1879048192 (* 0x70000000 *) *) -let sht_hiproc : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 536870911)(Nat_big_num.of_int 4))(Nat_big_num.of_int 3)) (* 2147483647 (* 0x7fffffff *) *) -let sht_louser : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 536870912)(Nat_big_num.of_int 4)) (* 2147483648 (* 0x80000000 *) *) -let sht_hiuser : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 603979775)(Nat_big_num.of_int 4))(Nat_big_num.of_int 3)) (* 2415919103 (* 0x8fffffff *) *) - -(** [string_of_section_type os proc user i] produces a string-based representation - * of section type [i]. Some section types are defined by ABI-specific supplements - * in reserved ranges, in which case the functions [os], [proc] and [user] are - * used to produce the string. - *) -(*val string_of_section_type : (natural -> string) -> (natural -> string) -> - (natural -> string) -> natural -> string*) -let string_of_section_type os proc user i:string= - (if Nat_big_num.equal i sht_null then - "NULL" - else if Nat_big_num.equal i sht_progbits then - "PROGBITS" - else if Nat_big_num.equal i sht_symtab then - "SYMTAB" - else if Nat_big_num.equal i sht_strtab then - "STRTAB" - else if Nat_big_num.equal i sht_rela then - "RELA" - else if Nat_big_num.equal i sht_hash then - "HASH" - else if Nat_big_num.equal i sht_dynamic then - "DYNAMIC" - else if Nat_big_num.equal i sht_note then - "NOTE" - else if Nat_big_num.equal i sht_nobits then - "NOBITS" - else if Nat_big_num.equal i sht_rel then - "REL" - else if Nat_big_num.equal i sht_shlib then - "SHLIB" - else if Nat_big_num.equal i sht_dynsym then - "DYNSYM" - else if Nat_big_num.equal i sht_init_array then - "INIT_ARRAY" - else if Nat_big_num.equal i sht_fini_array then - "FINI_ARRAY" - else if Nat_big_num.equal i sht_preinit_array then - "PREINIT_ARRAY" - else if Nat_big_num.equal i sht_group then - "GROUP" - else if Nat_big_num.equal i sht_symtab_shndx then - "SYMTAB_SHNDX" - else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then - os i - else if Nat_big_num.greater_equal i sht_loproc && Nat_big_num.less_equal i sht_hiproc then - proc i - else if Nat_big_num.greater_equal i sht_louser && Nat_big_num.less_equal i sht_hiuser then - user i - else - "Undefined or invalid section type") - -(** Section flag numeric values. *) - -(** The section contains data that should be writable during program execution. - *) -let shf_write : Nat_big_num.num= (Nat_big_num.of_int 1) -(** The section occupies memory during program execution. - *) -let shf_alloc : Nat_big_num.num= (Nat_big_num.of_int 2) -(** The section contains executable instructions. - *) -let shf_execinstr : Nat_big_num.num= (Nat_big_num.of_int 4) -(** The data in the section may be merged to reduce duplication. Each section - * is compared based on name, type and flags set with sections with identical - * values at run time being mergeable. - *) -let shf_merge : Nat_big_num.num= (Nat_big_num.of_int 16) -(** The section contains null-terminated character strings. - *) -let shf_strings : Nat_big_num.num= (Nat_big_num.of_int 32) -(** The [info] field of this section header contains a section header table - * index. - *) -let shf_info_link : Nat_big_num.num= (Nat_big_num.of_int 64) -(** Adds special link ordering for link editors. - *) -let shf_link_order : Nat_big_num.num= (Nat_big_num.of_int 128) -(** This section requires special OS-specific processing beyond the standard - * link rules. - *) -let shf_os_nonconforming : Nat_big_num.num= (Nat_big_num.of_int 256) -(** This section is a member (potentially the only member) of a link group. - *) -let shf_group : Nat_big_num.num= (Nat_big_num.of_int 512) -(** This section contains Thread Local Storage (TLS) meaning that each thread of - * execution has its own instance of this data. - *) -let shf_tls : Nat_big_num.num= (Nat_big_num.of_int 1024) -(** This section contains compressed data. Compressed data may not be marked as - * allocatable. - *) -let shf_compressed : Nat_big_num.num= (Nat_big_num.of_int 2048) -(** All bits included in these masks are reserved for OS and processor specific - * semantics respectively. - *) -let shf_mask_os : Nat_big_num.num= (Nat_big_num.of_int 267386880) (* 0x0ff00000 *) -let shf_mask_proc : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 1006632960)) (* 0xf0000000 *) - -(** [string_of_section_flags os proc f] produces a string based representation - * of section flag [f]. Some section flags are defined by the ABI and are in - * reserved ranges, in which case the flag string is produced by functions - * [os] and [proc]. - * TODO: add more as validation tests require them. - *) -(*val string_of_section_flags : (natural -> string) -> (natural -> string) -> - natural -> string*) -let string_of_section_flags os proc f:string= - (if Nat_big_num.equal f shf_write then - "W" - else if Nat_big_num.equal f shf_alloc then - " A" - else if Nat_big_num.equal f shf_execinstr then - " X" - else if Nat_big_num.equal f (Nat_big_num.add shf_alloc shf_execinstr) then - " AX" - else if Nat_big_num.equal f (Nat_big_num.add shf_write shf_alloc) then - " WA" - else if Nat_big_num.equal f shf_merge then - " M " - else if Nat_big_num.equal f (Nat_big_num.add shf_merge shf_alloc) then - " AM" - else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_merge shf_alloc) shf_strings) then - "AMS" - else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_alloc shf_execinstr) shf_group) then - "AXG" - else if Nat_big_num.equal f shf_strings then - " S" - else if Nat_big_num.equal f (Nat_big_num.add shf_merge shf_strings) then - " MS" - else if Nat_big_num.equal f shf_tls then - " T" - else if Nat_big_num.equal f (Nat_big_num.add shf_tls shf_alloc) then - " AT" - else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_write shf_alloc) shf_tls) then - "WAT" - else if Nat_big_num.equal f shf_info_link then - " I" - else if Nat_big_num.equal f (Nat_big_num.add shf_alloc shf_info_link) then - " AI" - else - " ") - -(** Section compression. *) - -(** Type [elf32_compression_header] provides information about the compression and - * decompression of compressed sections. All compressed sections on ELF32 begin - * with an [elf32_compression_header] entry. - *) -type elf32_compression_header = - { elf32_chdr_type : Uint32.uint32 (** Specifies the compression algorithm *) - ; elf32_chdr_size : Uint32.uint32 (** Size in bytes of the uncompressed data *) - ; elf32_chdr_addralign : Uint32.uint32 (** Specifies the required alignment of the uncompressed data *) - } - -(** Type [elf64_compression_header] provides information about the compression and - * decompression of compressed sections. All compressed sections on ELF64 begin - * with an [elf64_compression_header] entry. - *) -type elf64_compression_header = - { elf64_chdr_type : Uint32.uint32 (** Specified the compression algorithm *) - ; elf64_chdr_reserved : Uint32.uint32 (** Reserved. *) - ; elf64_chdr_size : Uint64.uint64 (** Size in bytes of the uncompressed data *) - ; elf64_chdr_addralign : Uint64.uint64 (** Specifies the required alignment of the uncompressed data *) - } - -(** This section is compressed with the ZLIB algorithm. The compressed data begins - * at the first byte immediately following the end of the compression header. - *) -let elfcompress_zlib : Nat_big_num.num= (Nat_big_num.of_int 1) - -(** Values in these ranges are reserved for OS-specific semantics. - *) -let elfcompress_loos : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 402653184)) (* 0x60000000 *) -let elfcompress_hios : 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 *) - -(** Values in these ranges are reserved for processor-specific semantics. - *) -let elfcompress_loproc : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 469762048)) (* 0x70000000 *) -let elfcompress_hiproc : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 1073741823))(Nat_big_num.of_int 1)) (* 0x7fffffff *) - -(** [read_elf32_compression_header ed bs0] reads an [elf32_compression_header] - * entry from byte sequence [bs0], interpreting [bs0] with endianness [ed]. - * Also returns the suffix of [bs0] after reading in the compression header. - * Fails if the header cannot be read. - *) -(*val read_elf32_compression_header : endianness -> byte_sequence -> - error (elf32_compression_header * byte_sequence)*) -let read_elf32_compression_header ed bs0:(elf32_compression_header*byte_sequence)error= - (read_elf32_word ed bs0 >>= (fun (typ, bs1) -> - read_elf32_word ed bs1 >>= (fun (siz, bs2) -> - read_elf32_word ed bs2 >>= (fun (ali, bs3) -> - return ({ elf32_chdr_type = typ; elf32_chdr_size = siz; - elf32_chdr_addralign = ali }, bs3))))) - -(** [read_elf64_compression_header ed bs0] reads an [elf64_compression_header] - * entry from byte sequence [bs0], interpreting [bs0] with endianness [ed]. - * Also returns the suffix of [bs0] after reading in the compression header. - * Fails if the header cannot be read. - *) -(*val read_elf64_compression_header : endianness -> byte_sequence -> - error (elf64_compression_header * byte_sequence)*) -let read_elf64_compression_header ed bs0:(elf64_compression_header*byte_sequence)error= - (read_elf64_word ed bs0 >>= (fun (typ, bs1) -> - read_elf64_word ed bs1 >>= (fun (res, bs2) -> - read_elf64_xword ed bs2 >>= (fun (siz, bs3) -> - read_elf64_xword ed bs3 >>= (fun (ali, bs4) -> - return ({ elf64_chdr_type = typ; elf64_chdr_reserved = res; - elf64_chdr_size = siz; elf64_chdr_addralign = ali }, bs4)))))) - -(** Section header table entry type. *) - -(** [elf32_section_header_table_entry] is the type of entries in the section - * header table in 32-bit ELF files. Each entry in the table details a section - * in the body of the ELF file. - *) -type elf32_section_header_table_entry = - { elf32_sh_name : Uint32.uint32 (** Name of the section *) - ; elf32_sh_type : Uint32.uint32 (** Type of the section and its semantics *) - ; elf32_sh_flags : Uint32.uint32 (** Flags associated with the section *) - ; elf32_sh_addr : Uint32.uint32 (** Address of first byte of section in memory image *) - ; elf32_sh_offset : Uint32.uint32 (** Offset from beginning of file of first byte of section *) - ; elf32_sh_size : Uint32.uint32 (** Section size in bytes *) - ; elf32_sh_link : Uint32.uint32 (** Section header table index link *) - ; elf32_sh_info : Uint32.uint32 (** Extra information, contents depends on type of section *) - ; elf32_sh_addralign : Uint32.uint32 (** Alignment constraints for section *) - ; elf32_sh_entsize : Uint32.uint32 (** Size of each entry in table, if section is one *) - } - -let elf32_null_section_header:elf32_section_header_table_entry= - ({ elf32_sh_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_type = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_flags = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_addr = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_offset = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_size = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_link = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_info = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_addralign = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf32_sh_entsize = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - }) - -(** [compare_elf32_section_header_table_entry ent1 ent2] is an ordering comparison - * function on section header table entries suitable for use in constructing - * sets, finite maps and other ordered data types. - *) -(*val compare_elf32_section_header_table_entry : elf32_section_header_table_entry -> - elf32_section_header_table_entry -> ordering*) -let compare_elf32_section_header_table_entry h1 h2:int= - (lexicographic_compare Nat_big_num.compare - [Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_name); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_type); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_flags); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_addr); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_offset); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_size); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_link); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_info); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_addralign); - Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_entsize)] - [Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_name); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_type); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_flags); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_addr); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_offset); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_size); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_link); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_info); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_addralign); - Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_entsize)]) - -let instance_Basic_classes_Ord_Elf_section_header_table_elf32_section_header_table_entry_dict:(elf32_section_header_table_entry)ord_class= ({ - - compare_method = compare_elf32_section_header_table_entry; - - isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_section_header_table_entry f1 f2) (-1)))); - - isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_section_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0]))); - - isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_section_header_table_entry f1 f2) 1))); - - isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_section_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))}) - -(** [elf64_section_header_table_entry] is the type of entries in the section - * header table in 64-bit ELF files. Each entry in the table details a section - * in the body of the ELF file. - *) -type elf64_section_header_table_entry = - { elf64_sh_name : Uint32.uint32 (** Name of the section *) - ; elf64_sh_type : Uint32.uint32 (** Type of the section and its semantics *) - ; elf64_sh_flags : Uint64.uint64 (** Flags associated with the section *) - ; elf64_sh_addr : Uint64.uint64 (** Address of first byte of section in memory image *) - ; elf64_sh_offset : Uint64.uint64 (** Offset from beginning of file of first byte of section *) - ; elf64_sh_size : Uint64.uint64 (** Section size in bytes *) - ; elf64_sh_link : Uint32.uint32 (** Section header table index link *) - ; elf64_sh_info : Uint32.uint32 (** Extra information, contents depends on type of section *) - ; elf64_sh_addralign : Uint64.uint64 (** Alignment constraints for section *) - ; elf64_sh_entsize : Uint64.uint64 (** Size of each entry in table, if section is one *) - } - -let elf64_null_section_header:elf64_section_header_table_entry= - ({ elf64_sh_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_type = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_flags = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_addr = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_offset = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_size = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_link = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_info = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_addralign = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_sh_entsize = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - }) - -(** [compare_elf64_section_header_table_entry ent1 ent2] is an ordering comparison - * function on section header table entries suitable for use in constructing - * sets, finite maps and other ordered data types. - *) -(*val compare_elf64_section_header_table_entry : elf64_section_header_table_entry -> - elf64_section_header_table_entry -> ordering*) -let compare_elf64_section_header_table_entry h1 h2:int= - (lexicographic_compare Nat_big_num.compare - [Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_name); - Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_type); - Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_flags; - Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_addr; - Nat_big_num.of_string (Uint64.to_string h1.elf64_sh_offset); - Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_size; - Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_link); - Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_info); - Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_addralign; - Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_entsize] - [Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_name); - Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_type); - Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_flags; - Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_addr; - Nat_big_num.of_string (Uint64.to_string h2.elf64_sh_offset); - Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_size; - Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_link); - Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_info); - Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_addralign; - Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_entsize]) - -let instance_Basic_classes_Ord_Elf_section_header_table_elf64_section_header_table_entry_dict:(elf64_section_header_table_entry)ord_class= ({ - - compare_method = compare_elf64_section_header_table_entry; - - isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_section_header_table_entry f1 f2) (-1)))); - - isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_section_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0]))); - - isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_section_header_table_entry f1 f2) 1))); - - isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_section_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))}) - -(** Section header table type *) - -(** Type [elf32_section_header_table] represents a section header table for 32-bit - * ELF files. A section header table is an array (implemented as a list, here) - * of section header table entries. - *) -type elf32_section_header_table = elf32_section_header_table_entry - list - -(** Type [elf64_section_header_table] represents a section header table for 64-bit - * ELF files. A section header table is an array (implemented as a list, here) - * of section header table entries. - *) -type elf64_section_header_table = elf64_section_header_table_entry - list - -(** Parsing and blitting *) - -(** [bytes_of_elf32_section_header_table_entry ed ent] blits [ent] to a byte sequence - * assuming endianness [ed]. - *) -(*val bytes_of_elf32_section_header_table_entry : endianness -> - elf32_section_header_table_entry -> byte_sequence*) -let bytes_of_elf32_section_header_table_entry endian entry:byte_sequence= - (Byte_sequence.from_byte_lists [ - bytes_of_elf32_word endian entry.elf32_sh_name - ; bytes_of_elf32_word endian entry.elf32_sh_type - ; bytes_of_elf32_word endian entry.elf32_sh_flags - ; bytes_of_elf32_addr endian entry.elf32_sh_addr - ; bytes_of_elf32_off endian entry.elf32_sh_offset - ; bytes_of_elf32_word endian entry.elf32_sh_size - ; bytes_of_elf32_word endian entry.elf32_sh_link - ; bytes_of_elf32_word endian entry.elf32_sh_info - ; bytes_of_elf32_word endian entry.elf32_sh_addralign - ; bytes_of_elf32_word endian entry.elf32_sh_entsize - ]) - -(** [read_elf32_section_header_table_entry ed bs0] reads a section header table - * entry from [bs0] assuming endianness [ed]. Also returns the suffix of [bs0] - * after parsing. Fails if the entry cannot be read. - *) -(*val read_elf32_section_header_table_entry : endianness -> byte_sequence -> - error (elf32_section_header_table_entry * byte_sequence)*) -let read_elf32_section_header_table_entry endian bs:(elf32_section_header_table_entry*byte_sequence)error= - (read_elf32_word endian bs >>= (fun (sh_name, bs) -> - read_elf32_word endian bs >>= (fun (sh_type, bs) -> - read_elf32_word endian bs >>= (fun (sh_flags, bs) -> - read_elf32_addr endian bs >>= (fun (sh_addr, bs) -> - read_elf32_off endian bs >>= (fun (sh_offset, bs) -> - read_elf32_word endian bs >>= (fun (sh_size, bs) -> - read_elf32_word endian bs >>= (fun (sh_link, bs) -> - read_elf32_word endian bs >>= (fun (sh_info, bs) -> - read_elf32_word endian bs >>= (fun (sh_addralign, bs) -> - read_elf32_word endian bs >>= (fun (sh_entsize, bs) -> - return ({ elf32_sh_name = sh_name; elf32_sh_type = sh_type; - elf32_sh_flags = sh_flags; elf32_sh_addr = sh_addr; - elf32_sh_offset = sh_offset; elf32_sh_size = sh_size; - elf32_sh_link = sh_link; elf32_sh_info = sh_info; - elf32_sh_addralign = sh_addralign; elf32_sh_entsize = sh_entsize }, bs)))))))))))) - -(** [bytes_of_elf64_section_header_table_entry ed ent] blits [ent] to a byte sequence - * assuming endianness [ed]. - *) -(*val bytes_of_elf64_section_header_table_entry : endianness -> - elf64_section_header_table_entry -> byte_sequence*) -let bytes_of_elf64_section_header_table_entry endian entry:byte_sequence= - (Byte_sequence.from_byte_lists [ - bytes_of_elf64_word endian entry.elf64_sh_name - ; bytes_of_elf64_word endian entry.elf64_sh_type - ; bytes_of_elf64_xword endian entry.elf64_sh_flags - ; bytes_of_elf64_addr endian entry.elf64_sh_addr - ; bytes_of_elf64_off endian entry.elf64_sh_offset - ; bytes_of_elf64_xword endian entry.elf64_sh_size - ; bytes_of_elf64_word endian entry.elf64_sh_link - ; bytes_of_elf64_word endian entry.elf64_sh_info - ; bytes_of_elf64_xword endian entry.elf64_sh_addralign - ; bytes_of_elf64_xword endian entry.elf64_sh_entsize - ]) - -(** [read_elf64_section_header_table_entry ed bs0] reads a section header table - * entry from [bs0] assuming endianness [ed]. Also returns the suffix of [bs0] - * after parsing. Fails if the entry cannot be read. - *) -(*val read_elf64_section_header_table_entry : endianness -> byte_sequence -> - error (elf64_section_header_table_entry * byte_sequence)*) -let read_elf64_section_header_table_entry endian bs:(elf64_section_header_table_entry*byte_sequence)error= - (read_elf64_word endian bs >>= (fun (sh_name, bs) -> - read_elf64_word endian bs >>= (fun (sh_type, bs) -> - read_elf64_xword endian bs >>= (fun (sh_flags, bs) -> - read_elf64_addr endian bs >>= (fun (sh_addr, bs) -> - read_elf64_off endian bs >>= (fun (sh_offset, bs) -> - read_elf64_xword endian bs >>= (fun (sh_size, bs) -> - read_elf64_word endian bs >>= (fun (sh_link, bs) -> - read_elf64_word endian bs >>= (fun (sh_info, bs) -> - read_elf64_xword endian bs >>= (fun (sh_addralign, bs) -> - read_elf64_xword endian bs >>= (fun (sh_entsize, bs) -> - return ({ elf64_sh_name = sh_name; elf64_sh_type = sh_type; - elf64_sh_flags = sh_flags; elf64_sh_addr = sh_addr; - elf64_sh_offset = sh_offset; elf64_sh_size = sh_size; - elf64_sh_link = sh_link; elf64_sh_info = sh_info; - elf64_sh_addralign = sh_addralign; elf64_sh_entsize = sh_entsize }, bs)))))))))))) - -(** [bytes_of_elf32_section_header_table ed tbl] blits section header table [tbl] - * to a byte sequence assuming endianness [ed]. - *) -(*val bytes_of_elf32_section_header_table : endianness -> - elf32_section_header_table -> byte_sequence*) -let bytes_of_elf32_section_header_table endian tbl:byte_sequence= - (Byte_sequence.concat0 (Lem_list.map (bytes_of_elf32_section_header_table_entry endian) tbl)) - -(** [bytes_of_elf64_section_header_table ed tbl] blits section header table [tbl] - * to a byte sequence assuming endianness [ed]. - *) -(*val bytes_of_elf64_section_header_table : endianness -> - elf64_section_header_table -> byte_sequence*) -let bytes_of_elf64_section_header_table endian tbl:byte_sequence= - (Byte_sequence.concat0 (Lem_list.map (bytes_of_elf64_section_header_table_entry endian) tbl)) - -(** [read_elf32_section_header_table' ed bs0] parses an ELF32 section header table - * from byte sequence [bs0] assuming endianness [ed]. Assumes [bs0] is of the - * exact length required to parse the entire table. - * Fails if any of the section header table entries cannot be parsed. - *) -(*val read_elf32_section_header_table' : endianness -> byte_sequence -> - error elf32_section_header_table*) -let rec read_elf32_section_header_table' endian bs0:((elf32_section_header_table_entry)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then - return [] - else - read_elf32_section_header_table_entry endian bs0 >>= (fun (entry, bs1) -> - read_elf32_section_header_table' endian bs1 >>= (fun tail -> - return (entry::tail)))) - -(** [read_elf64_section_header_table' ed bs0] parses an ELF64 section header table - * from byte sequence [bs0] assuming endianness [ed]. Assumes [bs0] is of the - * exact length required to parse the entire table. - * Fails if any of the section header table entries cannot be parsed. - *) -(*val read_elf64_section_header_table' : endianness -> byte_sequence -> - error elf64_section_header_table*) -let rec read_elf64_section_header_table' endian bs0:((elf64_section_header_table_entry)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then - return [] - else - read_elf64_section_header_table_entry endian bs0 >>= (fun (entry, bs1) -> - read_elf64_section_header_table' endian bs1 >>= (fun tail -> - return (entry::tail)))) - -(** [read_elf32_section_header_table sz ed bs0] parses an ELF32 section header - * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness - * [ed]. The suffix of [bs0] remaining after parsing is also returned. - * Fails if any of the section header entries cannot be parsed or if [sz] is - * greater than the length of [bs0]. - *) -(*val read_elf32_section_header_table : natural -> endianness -> byte_sequence -> - error (elf32_section_header_table * byte_sequence)*) -let read_elf32_section_header_table table_size endian bs0:((elf32_section_header_table_entry)list*byte_sequence)error= - (partition0 table_size bs0 >>= (fun (eat, rest) -> - read_elf32_section_header_table' endian eat >>= (fun entries -> - return (entries, rest)))) - - -(** [read_elf64_section_header_table sz ed bs0] parses an ELF64 section header - * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness - * [ed]. The suffix of [bs0] remaining after parsing is also returned. - * Fails if any of the section header entries cannot be parsed or if [sz] is - * greater than the length of [bs0]. - *) -(*val read_elf64_section_header_table : natural -> endianness -> byte_sequence -> - error (elf64_section_header_table * byte_sequence)*) -let read_elf64_section_header_table table_size endian bs0:((elf64_section_header_table_entry)list*byte_sequence)error= - (partition0 table_size bs0 >>= (fun (eat, rest) -> - read_elf64_section_header_table' endian eat >>= (fun entries -> - return (entries, rest)))) - - -(** Correctness criteria *) - -(** TODO: what is going on here? *) -(*val elf32_size_correct : elf32_section_header_table_entry -> - elf32_section_header_table -> bool*) -let elf32_size_correct hdr tbl:bool= - (let m = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_sh_size)) in - if Nat_big_num.equal m(Nat_big_num.of_int 0) then - true - else Nat_big_num.equal - m (Nat_big_num.of_int (List.length tbl))) - - -(** TODO: what is going on here? *) -(*val elf64_size_correct : elf64_section_header_table_entry -> - elf64_section_header_table -> bool*) -let elf64_size_correct hdr tbl:bool= - (let m = (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_sh_size) in - if Nat_big_num.equal m(Nat_big_num.of_int 0) then - true - else Nat_big_num.equal - m (Nat_big_num.of_int (List.length tbl))) - - -(** [is_elf32_addr_addralign_correct ent] checks whether an internal address - * alignment constraint is met on section header table [ent]. - * TODO: needs tweaking to add in power-of-two constraint, too. - *) -(*val is_elf32_addr_addralign_correct : elf32_section_header_table_entry -> bool*) -let is_elf32_addr_addralign_correct ent:bool= - (let align = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_addralign)) in - let addr = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_addr)) in - if Nat_big_num.equal (Nat_big_num.modulus addr align)(Nat_big_num.of_int 0) then Nat_big_num.equal - align(Nat_big_num.of_int 0) || Nat_big_num.equal align(Nat_big_num.of_int 1) (* TODO: or a power of two *) - else - false) - -(** [is_elf64_addr_addralign_correct ent] checks whether an internal address - * alignment constraint is met on section header table [ent]. - * TODO: needs tweaking to add in power-of-two constraint, too. - *) -(*val is_elf64_addr_addralign_correct : elf64_section_header_table_entry -> bool*) -let is_elf64_addr_addralign_correct ent:bool= - (let align = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_addralign) in - let addr = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_addr) in - if Nat_big_num.equal (Nat_big_num.modulus addr align)(Nat_big_num.of_int 0) then Nat_big_num.equal - align(Nat_big_num.of_int 0) || Nat_big_num.equal align(Nat_big_num.of_int 1) (* TODO: or a power of two *) - else - false) - -(** [is_valid_elf32_section_header_table sht] checks whether all entries of - * section header table [sht] are valid. - *) -(*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*) -let is_valid_elf32_section_header_table tbl:bool= - ((match tbl with - | [] -> true - | x::xs -> Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_type)) sht_null && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_flags))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_addr))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_info))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_addralign))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_entsize))(Nat_big_num.of_int 0) && - elf32_size_correct x tbl))))))) - (* XXX: more correctness criteria in time *) - )) - -(** [is_valid_elf64_section_header_table sht] checks whether all entries of - * section header table [sht] are valid. - *) -(*val is_valid_elf64_section_header_table : elf64_section_header_table -> bool*) -let is_valid_elf64_section_header_table tbl:bool= - ((match tbl with - | [] -> true - | x::xs -> Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf64_sh_type)) sht_null && (Nat_big_num.equal -(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_flags)(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_addr)(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string x.elf64_sh_info))(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_addralign)(Nat_big_num.of_int 0) && (Nat_big_num.equal -(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_entsize)(Nat_big_num.of_int 0) && - elf64_size_correct x tbl))))))) - (* XXX: more correctness criteria in time *) - )) - -(** Pretty printing *) - -(** The [sht_print_bundle] type is used to tidy up other type signatures. Some of the - * top-level string_of_ functions require six or more functions passed to them, - * which quickly gets out of hand. This type is used to reduce that complexity. - * The first component of the type is an OS specific print function, the second is - * a processor specific print function. - *) -type sht_print_bundle = - (Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string) - -(** [string_of_elf32_section_header_table_entry sht ent] produces a string - * representation of section header table entry [ent] using [sht], a - * [sht_print_bundle]. - * OCaml specific definition. - *) -(*val string_of_elf32_section_header_table_entry : sht_print_bundle -> - elf32_section_header_table_entry -> string*) -let string_of_elf32_section_header_table_entry (os, proc, user) entry:string= - (unlines [ -("\t" ^ ("Name: " ^ Uint32.to_string entry.elf32_sh_name)) - ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf32_sh_type)))) - ; ("\t" ^ ("Flags: " ^ Uint32.to_string entry.elf32_sh_flags)) - ; ("\t" ^ ("Address: " ^ Uint32.to_string entry.elf32_sh_addr)) - ; ("\t" ^ ("Size: " ^ Uint32.to_string entry.elf32_sh_size)) - ]) - -(** [string_of_elf64_section_header_table_entry sht ent] produces a string - * representation of section header table entry [ent] using [sht], a - * [sht_print_bundle]. - * OCaml specific definition. - *) -(*val string_of_elf64_section_header_table_entry : sht_print_bundle -> - elf64_section_header_table_entry -> string*) -let string_of_elf64_section_header_table_entry (os, proc, user) entry:string= - (unlines [ -("\t" ^ ("Name: " ^ Uint32.to_string entry.elf64_sh_name)) - ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf64_sh_type)))) - ; ("\t" ^ ("Flags: " ^ Uint64.to_string entry.elf64_sh_flags)) - ; ("\t" ^ ("Address: " ^ Uint64.to_string entry.elf64_sh_addr)) - ; ("\t" ^ ("Size: " ^ Uint64.to_string entry.elf64_sh_size)) - ]) - -(** [string_of_elf32_section_header_table_entry' sht stab ent] produces a string - * representation of section header table entry [ent] using [sht] and section - * header string table [stab] to print the name of the section header entry - * correctly. - * OCaml specific definition. - *) -(*val string_of_elf32_section_header_table_entry' : sht_print_bundle -> - string_table -> elf32_section_header_table_entry -> string*) -let string_of_elf32_section_header_table_entry' (os, proc, user) stbl entry:string= - (let name1 = -((match get_string_at (Nat_big_num.of_string (Uint32.to_string entry.elf32_sh_name)) stbl with - | Fail _ -> "Invalid index into string table" - | Success i -> i - )) - in - unlines [ -("\t" ^ ("Name: " ^ name1)) - ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf32_sh_type)))) - ; ("\t" ^ ("Flags: " ^ Uint32.to_string entry.elf32_sh_flags)) - ; ("\t" ^ ("Address: " ^ Uint32.to_string entry.elf32_sh_addr)) - ; ("\t" ^ ("Size: " ^ Uint32.to_string entry.elf32_sh_size)) - ]) - -(** [string_of_elf64_section_header_table_entry' sht stab ent] produces a string - * representation of section header table entry [ent] using [sht] and section - * header string table [stab] to print the name of the section header entry - * correctly. - * OCaml specific definition. - *) -(*val string_of_elf64_section_header_table_entry' : sht_print_bundle -> - string_table -> elf64_section_header_table_entry -> string*) -let string_of_elf64_section_header_table_entry' (os, proc, user) stbl entry:string= - (let name1 = -((match get_string_at (Nat_big_num.of_string (Uint32.to_string entry.elf64_sh_name)) stbl with - | Fail _ -> "Invalid index into string table" - | Success i -> i - )) - in - unlines [ -("\t" ^ ("Name: " ^ name1)) - ; ("\t" ^ ("Type: " ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf64_sh_type)))) - ; ("\t" ^ ("Flags: " ^ Uint64.to_string entry.elf64_sh_flags)) - ; ("\t" ^ ("Address: " ^ Uint64.to_string entry.elf64_sh_addr)) - ; ("\t" ^ ("Size: " ^ Uint64.to_string entry.elf64_sh_size)) - ]) - -(** The following defintions are default printing functions, with no ABI-specific - * functionality, in order to produce a [Show] instance for section header - * table entries. - *) - -(*val string_of_elf32_section_header_table_entry_default : elf32_section_header_table_entry -> string*) -let string_of_elf32_section_header_table_entry_default:elf32_section_header_table_entry ->string= - (string_of_elf32_section_header_table_entry - (((fun y->"*Default OS specific print*")), - ((fun y->"*Default processor specific print*")), - ((fun y->"*Default user specific print*")))) - -let instance_Show_Show_Elf_section_header_table_elf32_section_header_table_entry_dict:(elf32_section_header_table_entry)show_class= ({ - - show_method = string_of_elf32_section_header_table_entry_default}) - -(*val string_of_elf64_section_header_table_entry_default : elf64_section_header_table_entry -> string*) -let string_of_elf64_section_header_table_entry_default:elf64_section_header_table_entry ->string= - (string_of_elf64_section_header_table_entry - (((fun y->"*Default OS specific print*")), - ((fun y->"*Default processor specific print*")), - ((fun y->"*Default user specific print*")))) - -let instance_Show_Show_Elf_section_header_table_elf64_section_header_table_entry_dict:(elf64_section_header_table_entry)show_class= ({ - - show_method = string_of_elf64_section_header_table_entry_default}) - -(*val string_of_elf32_section_header_table : sht_print_bundle -> - elf32_section_header_table -> string*) -let string_of_elf32_section_header_table sht_bdl tbl:string= - (unlines (Lem_list.map (string_of_elf32_section_header_table_entry sht_bdl) tbl)) - -(*val string_of_elf32_section_header_table_default : elf32_section_header_table -> - string*) -let string_of_elf32_section_header_table_default:elf32_section_header_table ->string= - (string_of_elf32_section_header_table - (((fun y->"*Default OS specific print*")), - ((fun y->"*Default processor specific print*")), - ((fun y->"*Default user specific print*")))) - -(*val string_of_elf64_section_header_table : sht_print_bundle -> - elf64_section_header_table -> string*) -let string_of_elf64_section_header_table sht_bdl tbl:string= - (unlines (Lem_list.map (string_of_elf64_section_header_table_entry sht_bdl) tbl)) - -(*val string_of_elf64_section_header_table_default : elf64_section_header_table -> - string*) -let string_of_elf64_section_header_table_default:elf64_section_header_table ->string= - (string_of_elf64_section_header_table - (((fun y->"*Default OS specific print*")), - ((fun y->"*Default processor specific print*")), - ((fun y->"*Default user specific print*")))) - -(*val string_of_elf32_section_header_table' : sht_print_bundle -> string_table -> - elf32_section_header_table -> string*) -let string_of_elf32_section_header_table' sht_bdl stbl tbl:string= - (unlines (Lem_list.map (string_of_elf32_section_header_table_entry' sht_bdl stbl) tbl)) - -(*val string_of_elf64_section_header_table' : sht_print_bundle -> string_table -> - elf64_section_header_table -> string*) -let string_of_elf64_section_header_table' sht_bdl stbl tbl:string= - (unlines (Lem_list.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl)) - -(** Section to segment mappings *) - -(** [elf32_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf: - * - * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ - * (((sec_hdr)->sh_flags & SHF_TLS) != 0 \ - * && (sec_hdr)->sh_type == SHT_NOBITS \ - * && (segment)->p_type != PT_TLS) - * - * From readelf source code, file [internal.h]. - * - *) -(*val is_elf32_tbss_special : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) -let is_elf32_tbss_special sec_hdr segment:bool= (not ((Uint32.logand sec_hdr.elf32_sh_flags (Uint32.of_string (Nat_big_num.to_string shf_tls))) = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))) && -(( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_type)) sht_nobits) && - ( not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string segment.elf32_p_type)) elf_pt_tls)))) - -(** [elf64_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf: - * - * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ - * (((sec_hdr)->sh_flags & SHF_TLS) != 0 \ - * && (sec_hdr)->sh_type == SHT_NOBITS \ - * && (segment)->p_type != PT_TLS) - * - * From readelf source code, file [internal.h]. - * - *) -(*val is_elf64_tbss_special : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) -let is_elf64_tbss_special sec_hdr segment:bool= (not ((Uint64.logand sec_hdr.elf64_sh_flags (Uint64.of_string (Nat_big_num.to_string shf_tls))) = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))) && -(( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string sec_hdr.elf64_sh_type)) sht_nobits) && - ( not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string segment.elf64_p_type)) elf_pt_tls)))) - -(** [get_elf32_section_to_segment_mapping hdr sht pht isin stbl] computes the - * section to segment mapping for an ELF file using information in the section - * header table [sht], program header table [pht] and file header [hdr]. A - * string table [stbl] is taken to produce the string output. The test whether - * a section lies withing a segment is ABI specific, so [isin] is used to perform - * the test. - *) -(*val get_elf32_section_to_segment_mapping : elf32_header -> elf32_section_header_table -> elf32_program_header_table_entry -> - (elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool) -> - string_table -> error (list string)*) -let rec get_elf32_section_to_segment_mapping hdr sects pent isin stbl:((string)list)error= - ((match sects with - | [] -> return [] - | x::xs -> - if is_elf32_tbss_special x pent then - get_elf32_section_to_segment_mapping hdr xs pent isin stbl - else if not (isin hdr x pent) then - get_elf32_section_to_segment_mapping hdr xs pent isin stbl - else - let nm = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name)) in - get_string_at nm stbl >>= (fun str -> - get_elf32_section_to_segment_mapping hdr xs pent isin stbl >>= (fun tl -> - return (str :: tl))) - )) - -(** [get_elf64_section_to_segment_mapping hdr sht pht isin stbl] computes the - * section to segment mapping for an ELF file using information in the section - * header table [sht], program header table [pht] and file header [hdr]. A - * string table [stbl] is taken to produce the string output. The test whether - * a section lies withing a segment is ABI specific, so [isin] is used to perform - * the test. - *) -(*val get_elf64_section_to_segment_mapping : elf64_header -> elf64_section_header_table -> elf64_program_header_table_entry -> - (elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool) -> - string_table -> error (list string)*) -let rec get_elf64_section_to_segment_mapping hdr sects pent isin stbl:((string)list)error= - ((match sects with - | [] -> return [] - | x::xs -> - if not (isin hdr x pent) then - get_elf64_section_to_segment_mapping hdr xs pent isin stbl - else if is_elf64_tbss_special x pent then - get_elf64_section_to_segment_mapping hdr xs pent isin stbl - else - let nm = (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name)) in - get_string_at nm stbl >>= (fun str -> - get_elf64_section_to_segment_mapping hdr xs pent isin stbl >>= (fun tl -> - return (str :: tl))) - )) - -(** Section groups *) - -(** This is a COMDAT group and may duplicate other COMDAT groups in other object - * files. - *) -let grp_comdat : Nat_big_num.num= (Nat_big_num.of_int 1) - -(** Any bits in the following mask ranges are reserved exclusively for OS and - * processor specific semantics, respectively. - *) -let grp_maskos : Nat_big_num.num= (Nat_big_num.of_int 267386880) (* 0x0ff00000 *) -let grp_maskproc : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 1006632960)) (* 0xf0000000 *) - -(** [obtain_elf32_section_group_indices endian sht bs0] extracts all section header - * table indices of sections that are marked as being part of a section group. - *) -(*val obtain_elf32_section_group_indices : endianness -> elf32_section_header_table -> byte_sequence - -> error (list (natural * list elf32_word))*) -let obtain_elf32_section_group_indices endian sht bs0:((Nat_big_num.num*(Uint32.uint32)list)list)error= - (let filtered = (List.filter (fun ent -> Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) sht_group) sht) - in - mapM (fun grp -> - let off = (Nat_big_num.of_string (Uint32.to_string grp.elf32_sh_offset)) in - let siz = (Nat_big_num.of_string (Uint32.to_string grp.elf32_sh_size)) in - let cnt = (Nat_big_num.div siz(Nat_big_num.of_int 4)) (* size of elf32_word in bytes *) in - Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> - Error.repeatM' cnt rel (read_elf32_word endian) >>= (fun (mems, _) -> - (match mems with - | [] -> fail "obtain_elf32_section_group_indices: section group sections must consist of at least one elf32_word" - | x::xs -> - let flag = (Nat_big_num.of_string (Uint32.to_string x)) in - return (flag, xs) - ))) - ) filtered) - -(** [obtain_elf64_section_group_indices endian sht bs0] extracts all section header - * table indices of sections that are marked as being part of a section group. - *) -(*val obtain_elf64_section_group_indices : endianness -> elf64_section_header_table -> byte_sequence - -> error (list (natural * list elf64_word))*) -let obtain_elf64_section_group_indices endian sht bs0:((Nat_big_num.num*(Uint32.uint32)list)list)error= - (let filtered = (List.filter (fun ent -> Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) sht_group) sht) - in - mapM (fun grp -> - let off = (Nat_big_num.of_string (Uint64.to_string grp.elf64_sh_offset)) in - let siz = (Ml_bindings.nat_big_num_of_uint64 grp.elf64_sh_size) in - let cnt = (Nat_big_num.div siz(Nat_big_num.of_int 4)) (* size of elf64_word in bytes *) in - Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> - Error.repeatM' cnt rel (read_elf64_word endian) >>= (fun (mems, _) -> - (match mems with - | [] -> fail "obtain_elf64_section_group_indices: section group sections must consist of at least one elf64_word" - | x::xs -> - let flag = (Nat_big_num.of_string (Uint32.to_string x)) in - return (flag, xs) - ))) - ) filtered) - -(** [obtain_elf32_tls_template sht] extracts the TLS template (i.e. all sections - * in section header table [sht] that have their TLS flag bit set). - *) -(*val obtain_elf32_tls_template : elf32_section_header_table -> elf32_section_header_table*) -let obtain_elf32_tls_template sht:(elf32_section_header_table_entry)list= - (List.filter (fun ent -> - let flags = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_flags)) in not (Nat_big_num.equal (Nat_big_num.bitwise_and flags shf_tls)(Nat_big_num.of_int 0))) sht) - -(** [obtain_elf64_tls_template sht] extracts the TLS template (i.e. all sections - * in section header table [sht] that have their TLS flag bit set). - *) -(*val obtain_elf64_tls_template : elf64_section_header_table -> elf64_section_header_table*) -let obtain_elf64_tls_template sht:(elf64_section_header_table_entry)list= - (List.filter (fun ent -> - let flags = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_flags) in not (Nat_big_num.equal (Nat_big_num.bitwise_and flags shf_tls)(Nat_big_num.of_int 0))) sht) - -(** [obtain_elf32_hash_table endian sht bs0] extracts a hash table from an ELF file - * providing a section of type SHT_HASH exists in section header table [sht]. - * Extraction is from byte sequence [bs0] assuming endianness [endian]. The - * return type represents the number of buckets, the number of chains, the buckets - * and finally the chains. - *) -(*val obtain_elf32_hash_table : endianness -> elf32_section_header_table -> byte_sequence -> - error (elf32_word * elf32_word * list elf32_word * list elf32_word)*) -let obtain_elf32_hash_table endian sht bs0:(Uint32.uint32*Uint32.uint32*(Uint32.uint32)list*(Uint32.uint32)list)error= - (let filtered = (List.filter (fun ent -> Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) sht_hash) sht) - in - (match filtered with - | [] -> fail "obtain_elf32_hash_table: no section header table entry of type sht_hash" - | [x] -> - let siz = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_size)) in - let off = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset)) in - Byte_sequence.offset_and_cut siz off bs0 >>= (fun rel -> - read_elf32_word endian rel >>= (fun (nbucket, rel) -> - read_elf32_word endian rel >>= (fun (nchain, rel) -> - Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nbucket)) rel (read_elf32_word endian) >>= (fun (buckets, rel) -> - Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nchain)) rel (read_elf32_word endian) >>= (fun (chain, _) -> - return (nbucket, nchain, buckets, chain)))))) - | _ -> fail "obtain_elf32_hash_table: multiple section header table entries of type sht_hash" - )) - -(** [obtain_elf64_hash_table endian sht bs0] extracts a hash table from an ELF file - * providing a section of type SHT_HASH exists in section header table [sht]. - * Extraction is from byte sequence [bs0] assuming endianness [endian]. The - * return type represents the number of buckets, the number of chains, the buckets - * and finally the chains. - *) -(*val obtain_elf64_hash_table : endianness -> elf64_section_header_table -> byte_sequence -> - error (elf64_word * elf64_word * list elf64_word * list elf64_word)*) -let obtain_elf64_hash_table endian sht bs0:(Uint32.uint32*Uint32.uint32*(Uint32.uint32)list*(Uint32.uint32)list)error= - (let filtered = (List.filter (fun ent -> Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) sht_hash) sht) - in - (match filtered with - | [] -> fail "obtain_elf64_hash_table: no section header table entry of type sht_hash" - | [x] -> - let siz = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in - let off = (Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset)) in - Byte_sequence.offset_and_cut siz off bs0 >>= (fun rel -> - read_elf64_word endian rel >>= (fun (nbucket, rel) -> - read_elf64_word endian rel >>= (fun (nchain, rel) -> - Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nbucket)) rel (read_elf64_word endian) >>= (fun (buckets, rel) -> - Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nchain)) rel (read_elf64_word endian) >>= (fun (chain, _) -> - return (nbucket, nchain, buckets, chain)))))) - | _ -> fail "obtain_elf64_hash_table: multiple section header table entries of type sht_hash" - )) - -(** Special sections *) - -(** [construct_special_sections] contains a finite map from section name (as - * a string) to the expected attributes and flags expected of that section, - * as specified in the ELF specification. - * NOTE: some of these are overriden by the ABI. - *) -(*val elf_special_sections : Map.map string (natural * natural)*) -let elf_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) [ - (".bss", (sht_nobits, Nat_big_num.add shf_alloc shf_write)) - ; (".comment", (sht_progbits,Nat_big_num.of_int 0)) - ; (".data", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".data1", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) - ; (".debug", (sht_progbits,Nat_big_num.of_int 0)) - (* ; (".dynamic", (sht_dynamic, ?)) *) - ; (".dynstr", (sht_strtab, shf_alloc)) - ; (".dynsym", (sht_dynsym, shf_alloc)) - ; (".fini", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) - ; (".fini_array", (sht_fini_array, Nat_big_num.add shf_alloc shf_write)) - (* ; (".got", (sht_progbits, ?)) *) - ; (".hash", (sht_hash, shf_alloc)) - ; (".init", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) - ; (".init_array", (sht_init_array, Nat_big_num.add shf_alloc shf_write)) - (* ; (".interp", (sht_progbits, ?)) *) - ; (".line", (sht_progbits,Nat_big_num.of_int 0)) - ; (".note", (sht_note,Nat_big_num.of_int 0)) - (* ; (".plt", (sht_progbits, ?)) *) - ; (".preinit_array", (sht_preinit_array, Nat_big_num.add shf_alloc shf_write)) - (* ; (".relname", (sht_rel, ?)) *) - (* ; (".relaname", (sht_rela, ?)) *) - ; (".rodata", (sht_progbits, shf_alloc)) - ; (".rodata1", (sht_progbits, shf_alloc)) - ; (".shstrtab", (sht_strtab,Nat_big_num.of_int 0)) - (* ; (".strtab", (sht_strtab, ?)) *) - (* ; (".symtab", (sht_symtab, ?)) *) - (* ; (".symtab_shndx", (sht_symtab_shndx, ?)) *) - ; (".tbss", (sht_nobits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls)) - ; (".tdata", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls)) - ; (".tdata1", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls)) - ; (".text", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) - ]) |