(*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)) ])