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 String_table open import Bitstring open import Error open import Missing_pervasives open import Show (** Special section indices. *) (** [shn_undef]: marks an undefined, missing or irrelevant section reference. *) let shn_undef : nat = 0 (** [shn_loreserve]: this specifies the lower bound of the range of reserved * indices. *) let shn_loreserve : nat = 65280 (* 0xff00 *) (** [shn_loproc]: start of the range reserved for processor-specific semantics. *) let shn_loproc : nat = 65280 (* 0xff00 *) (** [shn_hiproc]: end of the range reserved for processor-specific semantics. *) let shn_hiproc : nat = 65311 (* 0xff1f *) (** [shn_loos]: start of the range reserved for operating system-specific * semantics. *) let shn_loos : nat = 65312 (* 0xff20 *) (** [shn_hios]: end of the range reserved for operating system-specific * semantics. *) let shn_hios : nat = 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 = 65521 (* 0xfff1 *) (** [shn_common]: symbols defined relative to this index are common symbols, * such as unallocated C external variables. *) let shn_common : nat = 65522 (* 0xfff2 *) (** [shn_xindex]: an escape value. It indicates the actual section header index * is too large to fit in the containing field and is located in another * location (specific to the structure where it appears). *) let shn_xindex : nat = 65535 (* 0xffff *) (** [shn_hireserve]: specifies the upper-bound of reserved values. *) let shn_hireserve : nat = 65535 (* 0xffff *) val string_of_special_section_index : nat -> string let string_of_special_section_index i = if i = shn_undef then "SHN_UNDEF" else if i = shn_loreserve then "SHN_LORESERVE" else if i >= shn_loproc && i <= shn_hiproc then "SHN_PROCESSOR_SPECIFIC" else if i >= shn_loos && i <= shn_hios then "SHN_OS_SPECIFIC" else if i = shn_abs then "SHN_ABS" else if i = shn_common then "SHN_COMMON" else if i = shn_xindex then "SHN_XINDEX" else if i = shn_hireserve then "SHN_HIRESERVE" else "SHN UNDEFINED" (** Section types. *) (** Marks the section header as being inactive. *) let sht_null : nat = 0 (** Section holds information defined by the program. *) let sht_progbits : nat = 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 = 2 let sht_dynsym : nat = 11 (** Section holds a string table *) let sht_strtab : nat = 3 (** Section holds relocation entries with explicit addends. An object file may * have multiple section of this type. *) let sht_rela : nat = 4 (** Section holds a symbol hash table. An object file may only have a single * hash table. *) let sht_hash : nat = 5 (** Section holds information for dynamic linking. An object file may only have * a single dynamic section. *) let sht_dynamic : nat = 6 (** Section holds information that marks the file in some way. *) let sht_note : nat = 7 (** Section occupies no space in the file but otherwise resembles a progbits * section. *) let sht_nobits : nat = 8 (** Section holds relocation entries without explicit addends. An object file * may have multiple section of this type. *) let sht_rel : nat = 9 (** Section type is reserved but has an unspecified meaning. *) let sht_shlib : nat = 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 = 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 = 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 = 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 = 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 = 18 let sht_loos : nat = 3 * 1024 * 1024 * 512 (* 1610612736 (* 0x60000000 *) *) let sht_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *) let sht_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *) let sht_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *) let sht_louser : nat = (536870912 * 4) (* 2147483648 (* 0x80000000 *) *) let sht_hiuser : nat = (603979775 * 4) + 3 (* 2415919103 (* 0x8fffffff *) *) val string_of_section_type : (nat -> string) -> (nat -> string) -> (nat -> string) -> nat -> string let string_of_section_type os proc user i = if i = sht_null then "SHT_NULL" else if i = sht_progbits then "SHT_PROGBITS" else if i = sht_symtab then "SHT_SYMTAB" else if i = sht_strtab then "SHT_STRTAB" else if i = sht_rela then "SHT_RELA" else if i = sht_hash then "SHT_HASH" else if i = sht_dynamic then "SHT_DYNAMIC" else if i = sht_note then "SHT_NOTE" else if i = sht_nobits then "SHT_NOBITS" else if i = sht_rel then "SHT_REL" else if i = sht_shlib then "SHT_SHLIB" else if i = sht_dynsym then "SHT_DYNSYM" else if i = sht_init_array then "SHT_INIT_ARRAY" else if i = sht_fini_array then "SHT_FINI_ARRAY" else if i = sht_preinit_array then "SHT_PREINIT_ARRAY" else if i = sht_group then "SHT_GROUP" else if i = sht_symtab_shndx then "SHT_SYMTAB_SHNDX" else if i >= sht_loos && i <= sht_hios then os i else if i >= sht_loproc && i <= sht_hiproc then proc i else if i >= sht_louser && i <= sht_hiuser then user i else "Undefined or invalid section type" (** 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 : elf32_word (** Name of the section *) ; elf32_sh_type : elf32_word (** Type of the section and its semantics *) ; elf32_sh_flags : elf32_word (** Flags associated with the section *) ; elf32_sh_addr : elf32_addr (** Address of first byte of section in memory image *) ; elf32_sh_offset : elf32_off (** Offset from beginning of file of first byte of section *) ; elf32_sh_size : elf32_word (** Section size in bytes *) ; elf32_sh_link : elf32_word (** Section header table index link *) ; elf32_sh_info : elf32_word (** Extra information, contents depends on type of section *) ; elf32_sh_addralign : elf32_word (** Alignment constraints for section *) ; elf32_sh_entsize : elf32_word (** Size of each entry in table, if section is one *) |> (** [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 : elf64_word (** Name of the section *) ; elf64_sh_type : elf64_word (** Type of the section and its semantics *) ; elf64_sh_flags : elf64_xword (** Flags associated with the section *) ; elf64_sh_addr : elf64_addr (** Address of first byte of section in memory image *) ; elf64_sh_offset : elf64_off (** Offset from beginning of file of first byte of section *) ; elf64_sh_size : elf64_xword (** Section size in bytes *) ; elf64_sh_link : elf64_word (** Section header table index link *) ; elf64_sh_info : elf64_word (** Extra information, contents depends on type of section *) ; elf64_sh_addralign : elf64_xword (** Alignment constraints for section *) ; elf64_sh_entsize : elf64_xword (** Size of each entry in table, if section is one *) |> val read_elf32_section_header_table_entry : endianness -> bitstring -> error (elf32_section_header_table_entry * bitstring) let read_elf32_section_header_table_entry endian bs = 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) val read_elf64_section_header_table_entry : endianness -> bitstring -> error (elf64_section_header_table_entry * bitstring) let read_elf64_section_header_table_entry endian bs = 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) (** 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 -> string) * (nat -> string) * (nat -> string) 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 = unlines [ "\t" ^ "Name: " ^ show entry.elf32_sh_name ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf32_word entry.elf32_sh_type) ; "\t" ^ "Flags: " ^ show entry.elf32_sh_flags ; "\t" ^ "Address: " ^ show entry.elf32_sh_addr ; "\t" ^ "Size: " ^ show entry.elf32_sh_size ] 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 = unlines [ "\t" ^ "Name: " ^ show entry.elf64_sh_name ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf64_word entry.elf64_sh_type) ; "\t" ^ "Flags: " ^ show entry.elf64_sh_flags ; "\t" ^ "Address: " ^ show entry.elf64_sh_addr ; "\t" ^ "Size: " ^ show entry.elf64_sh_size ] 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 = let name = match get_string_at (nat_of_elf32_word entry.elf32_sh_name) stbl with | Fail _ -> "Invalid index into string table" | Success i -> i end in unlines [ "\t" ^ "Name: " ^ name ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf32_word entry.elf32_sh_type) ; "\t" ^ "Flags: " ^ show entry.elf32_sh_flags ; "\t" ^ "Address: " ^ show entry.elf32_sh_addr ; "\t" ^ "Size: " ^ show entry.elf32_sh_size ] 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 = let name = match get_string_at (nat_of_elf64_word entry.elf64_sh_name) stbl with | Fail _ -> "Invalid index into string table" | Success i -> i end in unlines [ "\t" ^ "Name: " ^ name ; "\t" ^ "Type: " ^ string_of_section_type os proc user (nat_of_elf64_word entry.elf64_sh_type) ; "\t" ^ "Flags: " ^ show entry.elf64_sh_flags ; "\t" ^ "Address: " ^ show entry.elf64_sh_addr ; "\t" ^ "Size: " ^ show entry.elf64_sh_size ] let string_of_elf32_section_header_table_entry_default = string_of_elf32_section_header_table_entry ((const "*Default OS specific print*"), (const "*Default processor specific print*"), (const "*Default user specific print*")) instance (Show elf32_section_header_table_entry) let show = string_of_elf32_section_header_table_entry_default end let string_of_elf64_section_header_table_entry_default = string_of_elf64_section_header_table_entry ((const "*Default OS specific print*"), (const "*Default processor specific print*"), (const "*Default user specific print*")) instance (Show elf64_section_header_table_entry) let show = string_of_elf64_section_header_table_entry_default end (** 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 = list elf32_section_header_table_entry class (HasElf32SectionHeaderTable 'a) val get_elf32_section_header_table : 'a -> maybe elf32_section_header_table end (** 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 = list elf64_section_header_table_entry class (HasElf64SectionHeaderTable 'a) val get_elf64_section_header_table : 'a -> maybe elf64_section_header_table end let rec read_elf32_section_header_table' endian bs0 = if length bs0 = 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) val read_elf32_section_header_table : nat -> endianness -> bitstring -> error (elf32_section_header_table * bitstring) let read_elf32_section_header_table table_size endian bs0 = let (eat, rest) = partition table_size bs0 in read_elf32_section_header_table' endian eat >>= fun entries -> return (entries, rest) ;; let rec read_elf64_section_header_table' endian bs0 = if length bs0 = 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) val read_elf64_section_header_table : nat -> endianness -> bitstring -> error (elf64_section_header_table * bitstring) let read_elf64_section_header_table table_size endian bs0 = let (eat, rest) = partition table_size bs0 in read_elf64_section_header_table' endian eat >>= fun entries -> return (entries, rest) ;; val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool let elf32_size_correct hdr tbl = match nat_of_elf32_word hdr.elf32_sh_size with | 0 -> true | m -> m = List.length tbl end ;; val is_valid_elf32_section_header_table : elf32_section_header_table -> bool let is_valid_elf32_section_header_table tbl = match tbl with | [] -> false | x::xs -> nat_of_elf32_word x.elf32_sh_name = 0 && nat_of_elf32_word x.elf32_sh_type = sht_null && nat_of_elf32_word x.elf32_sh_flags = 0 && nat_of_elf32_addr x.elf32_sh_addr = 0 && nat_of_elf32_off x.elf32_sh_offset = 0 && nat_of_elf32_word x.elf32_sh_info = 0 && nat_of_elf32_word x.elf32_sh_addralign = 0 && nat_of_elf32_word x.elf32_sh_entsize = 0 && elf32_size_correct x tbl (* XXX: more correctness criteria in time *) end 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 = unlines (List.map (string_of_elf32_section_header_table_entry sht_bdl) tbl) 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 = unlines (List.map (string_of_elf32_section_header_table_entry' sht_bdl stbl) tbl) 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 = unlines (List.map (string_of_elf64_section_header_table_entry sht_bdl) 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 = unlines (List.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl)