open import Basic_classes open import Bool open import Function open import List open import Maybe open import Num open import String open import Elf_types open import Endianness open import Bitstring open import Error open import Missing_pervasives open import Show (** Segment types * * FIXME: Bug in Lem as Lem codebase uses [int] type throughout where [BigInt.t] * is really needed, hence chokes on huge constants below, which is why they are * written in the way that they are. *) (** Unused array element. All other members of the structure are undefined. *) let elf_pt_null : nat = 0 (** A loadable segment. *) let elf_pt_load : nat = 1 (** Dynamic linking information. *) let elf_pt_dynamic : nat = 2 (** Specifies the location and size of a null-terminated path name to be used to * invoke an interpreter. *) let elf_pt_interp : nat = 3 (** Specifies location and size of auxiliary information. *) let elf_pt_note : nat = 4 (** Reserved but with unspecified semantics. If the file contains a segment of * this type then it is to be regarded as non-conformant with the ABI. *) let elf_pt_shlib : nat = 5 (** Specifies the location and size of the program header table. *) let elf_pt_phdr : nat = 6 (** Specifies the thread local storage (TLS) template. Need not be supported. *) let elf_pt_tls : nat = 7 (** Start of reserved indices for operating system specific semantics. *) let elf_pt_loos : nat = 128 * 128 * 128 * 256 * 3 (* 1610612736 (* 0x60000000 *) *) (** End of reserved indices for operating system specific semantics. *) let elf_pt_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *) (** Start of reserved indices for processor specific semantics. *) let elf_pt_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *) (** End of reserved indices for processor specific semantics. *) let elf_pt_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *) (** [string_of_elf_segment_type os proc st] produces a string representation of * the coding of an ELF segment type [st] using [os] and [proc] to render OS- * and processor-specific codings. *) val string_of_elf_segment_type : (nat -> string) -> (nat -> string) -> nat -> string let string_of_elf_segment_type os proc pt = if pt = elf_pt_null then "PT_NULL" else if pt = elf_pt_load then "PT_LOAD" else if pt = elf_pt_dynamic then "PT_DYNAMIC" else if pt = elf_pt_interp then "PT_INTERP" else if pt = elf_pt_note then "PT_NOTE" else if pt = elf_pt_shlib then "PT_SHLIB" else if pt = elf_pt_phdr then "PT_PHDR" else if pt = elf_pt_tls then "PT_TLS" else if pt >= elf_pt_loos && pt <= elf_pt_hios then os pt else if pt >= elf_pt_loproc && pt <= elf_pt_hiproc then proc pt else "Undefined or invalid segment type" (** Program header table entry type *) (** Type [elf32_program_header_table_entry] encodes a program header table entry * for 32-bit platforms. Each entry describes a segment in an executable or * shared object file. *) type elf32_program_header_table_entry = <| elf32_p_type : elf32_word (** Type of the segment *) ; elf32_p_offset : elf32_off (** Offset from beginning of file for segment *) ; elf32_p_vaddr : elf32_addr (** Virtual address for segment in memory *) ; elf32_p_paddr : elf32_addr (** Physical address for segment *) ; elf32_p_filesz : elf32_word (** Size of segment in file, in bytes *) ; elf32_p_memsz : elf32_word (** Size of segment in memory image, in bytes *) ; elf32_p_flags : elf32_word (** Segment flags *) ; elf32_p_align : elf32_word (** Segment alignment memory for memory and file *) |> (** Type [elf64_program_header_table_entry] encodes a program header table entry * for 64-bit platforms. Each entry describes a segment in an executable or * shared object file. *) type elf64_program_header_table_entry = <| elf64_p_type : elf64_word (** Type of the segment *) ; elf64_p_flags : elf64_word (** Segment flags *) ; elf64_p_offset : elf64_off (** Offset from beginning of file for segment *) ; elf64_p_vaddr : elf64_addr (** Virtual address for segment in memory *) ; elf64_p_paddr : elf64_addr (** Physical address for segment *) ; elf64_p_filesz : elf64_xword (** Size of segment in file, in bytes *) ; elf64_p_memsz : elf64_xword (** Size of segment in memory image, in bytes *) ; elf64_p_align : elf64_xword (** Segment alignment memory for memory and file *) |> (** [string_of_elf32_program_header_table_entry os proc et] produces a string * representation of a 32-bit program header table entry using [os] and [proc] * to render OS- and processor-specific entries. *) val string_of_elf32_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf32_program_header_table_entry -> string let string_of_elf32_program_header_table_entry os proc entry = unlines [ "\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf32_word entry.elf32_p_type) ; "\t" ^ "Offset: " ^ show entry.elf32_p_offset ; "\t" ^ "Virtual address: " ^ show entry.elf32_p_vaddr ; "\t" ^ "Physical address: " ^ show entry.elf32_p_paddr ; "\t" ^ "Segment size (bytes): " ^ show entry.elf32_p_filesz ; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf32_p_memsz ; "\t" ^ "Flags: " ^ show entry.elf32_p_flags ; "\t" ^ "Alignment: " ^ show entry.elf32_p_align ] (** [string_of_elf64_program_header_table_entry os proc et] produces a string * representation of a 64-bit program header table entry using [os] and [proc] * to render OS- and processor-specific entries. *) val string_of_elf64_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf64_program_header_table_entry -> string let string_of_elf64_program_header_table_entry os proc entry = unlines [ "\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf64_word entry.elf64_p_type) ; "\t" ^ "Offset: " ^ show entry.elf64_p_offset ; "\t" ^ "Virtual address: " ^ show entry.elf64_p_vaddr ; "\t" ^ "Physical address: " ^ show entry.elf64_p_paddr ; "\t" ^ "Segment size (bytes): " ^ show entry.elf64_p_filesz ; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf64_p_memsz ; "\t" ^ "Flags: " ^ show entry.elf64_p_flags ; "\t" ^ "Alignment: " ^ show entry.elf64_p_align ] (** [string_of_elf32_program_header_table_entry_default et] produces a string representation * of table entry [et] where OS- and processor-specific entries are replaced with * default strings. *) val string_of_elf32_program_header_table_entry_default : elf32_program_header_table_entry -> string let string_of_elf32_program_header_table_entry_default = string_of_elf32_program_header_table_entry (const "*Default OS specific print*") (const "*Default processor specific print*") (** [string_of_elf64_program_header_table_entry_default et] produces a string representation * of table entry [et] where OS- and processor-specific entries are replaced with * default strings. *) val string_of_elf64_program_header_table_entry_default : elf64_program_header_table_entry -> string let string_of_elf64_program_header_table_entry_default = string_of_elf64_program_header_table_entry (const "*Default OS specific print*") (const "*Default processor specific print*") instance (Show elf32_program_header_table_entry) let show = string_of_elf32_program_header_table_entry_default end instance (Show elf64_program_header_table_entry) let show = string_of_elf64_program_header_table_entry_default end (** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table * entry from bitstring [bs0] assuming endianness [endian]. If [bs0] is larger * than necessary, the excess is returned from the function, too. *) val read_elf32_program_header_table_entry : endianness -> bitstring -> error (elf32_program_header_table_entry * bitstring) let read_elf32_program_header_table_entry endian bs = read_elf32_word endian bs >>= fun (typ, bs) -> read_elf32_off endian bs >>= fun (offset, bs) -> read_elf32_addr endian bs >>= fun (vaddr, bs) -> read_elf32_addr endian bs >>= fun (paddr, bs) -> read_elf32_word endian bs >>= fun (filesz, bs) -> read_elf32_word endian bs >>= fun (memsz, bs) -> read_elf32_word endian bs >>= fun (flags, bs) -> read_elf32_word endian bs >>= fun (align, bs) -> return (<| elf32_p_type = typ; elf32_p_offset = offset; elf32_p_vaddr = vaddr; elf32_p_paddr = paddr; elf32_p_filesz = filesz; elf32_p_memsz = memsz; elf32_p_flags = flags; elf32_p_align = align |>, bs) val read_elf64_program_header_table_entry : endianness -> bitstring -> error (elf64_program_header_table_entry * bitstring) let read_elf64_program_header_table_entry endian bs = read_elf64_word endian bs >>= fun (typ, bs) -> read_elf64_word endian bs >>= fun (flags, bs) -> read_elf64_off endian bs >>= fun (offset, bs) -> read_elf64_addr endian bs >>= fun (vaddr, bs) -> read_elf64_addr endian bs >>= fun (paddr, bs) -> read_elf64_xword endian bs >>= fun (filesz, bs) -> read_elf64_xword endian bs >>= fun (memsz, bs) -> read_elf64_xword endian bs >>= fun (align, bs) -> return (<| elf64_p_type = typ; elf64_p_offset = offset; elf64_p_vaddr = vaddr; elf64_p_paddr = paddr; elf64_p_filesz = filesz; elf64_p_memsz = memsz; elf64_p_flags = flags; elf64_p_align = align |>, bs) (** Program header table type *) (** Type [elf32_program_header_table] represents a program header table for 32-bit * ELF files. A program header table is an array (implemented as a list, here) * of program header table entries. *) type elf32_program_header_table = list elf32_program_header_table_entry class (HasElf32ProgramHeaderTable 'a) val get_elf32_program_header_table : 'a -> maybe elf32_program_header_table end (** Type [elf64_program_header_table] represents a program header table for 64-bit * ELF files. A program header table is an array (implemented as a list, here) * of program header table entries. *) type elf64_program_header_table = list elf64_program_header_table_entry class (HasElf64ProgramHeaderTable 'a) val get_elf64_program_header_table : 'a -> maybe elf64_program_header_table end (** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from * bitstring [bs0] assuming endianness [endian]. The bitstring [bs0] is assumed * to have exactly the correct size for the table. For internal use, only. Use * [read_elf32_program_header_table] below instead. *) let rec read_elf32_program_header_table' endian bs0 = if length bs0 = 0 then return [] else read_elf32_program_header_table_entry endian bs0 >>= fun (entry, bs1) -> read_elf32_program_header_table' endian bs1 >>= fun tail -> return (entry::tail) (** [read_elf64_program_header_table' endian bs0] reads an ELF64 program header table from * bitstring [bs0] assuming endianness [endian]. The bitstring [bs0] is assumed * to have exactly the correct size for the table. For internal use, only. Use * [read_elf32_program_header_table] below instead. *) let rec read_elf64_program_header_table' endian bs0 = if length bs0 = 0 then return [] else read_elf64_program_header_table_entry endian bs0 >>= fun (entry, bs1) -> read_elf64_program_header_table' endian bs1 >>= fun tail -> return (entry::tail) (** [read_elf32_program_header_table table_size endian bs0] reads an ELF32 program header * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size]. * This [table_size] argument should be equal to the number of entries in the * table multiplied by the fixed entry size. Bitstring [bs0] may be larger than * necessary, in which case the excess is returned. *) val read_elf32_program_header_table : nat -> endianness -> bitstring -> error (elf32_program_header_table * bitstring) let read_elf32_program_header_table table_size endian bs0 = let (eat, rest) = partition table_size bs0 in read_elf32_program_header_table' endian eat >>= fun table -> return (table, rest) (** [read_elf64_program_header_table table_size endian bs0] reads an ELF64 program header * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size]. * This [table_size] argument should be equal to the number of entries in the * table multiplied by the fixed entry size. Bitstring [bs0] may be larger than * necessary, in which case the excess is returned. *) val read_elf64_program_header_table : nat -> endianness -> bitstring -> error (elf64_program_header_table * bitstring) let read_elf64_program_header_table table_size endian bs0 = let (eat, rest) = partition table_size bs0 in read_elf64_program_header_table' endian eat >>= fun table -> return (table, rest) (** The [pht_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 pht_print_bundle = (nat -> string) * (nat -> string) (** [string_of_elf32_program_header_table os proc tbl] produces a string representation * of program header table [tbl] using [os] and [proc] to render OS- and processor- * specific entries. *) val string_of_elf32_program_header_table : pht_print_bundle -> elf32_program_header_table -> string let string_of_elf32_program_header_table (os, proc) tbl = unlines (List.map (string_of_elf32_program_header_table_entry os proc) tbl) (** [string_of_elf64_program_header_table os proc tbl] produces a string representation * of program header table [tbl] using [os] and [proc] to render OS- and processor- * specific entries. *) val string_of_elf64_program_header_table : pht_print_bundle -> elf64_program_header_table -> string let string_of_elf64_program_header_table (os, proc) tbl = unlines (List.map (string_of_elf64_program_header_table_entry os proc) tbl)