diff options
Diffstat (limited to 'src/elf_model/elf_section_header_table.lem')
| -rw-r--r-- | src/elf_model/elf_section_header_table.lem | 445 |
1 files changed, 445 insertions, 0 deletions
diff --git a/src/elf_model/elf_section_header_table.lem b/src/elf_model/elf_section_header_table.lem new file mode 100644 index 00000000..669a2dce --- /dev/null +++ b/src/elf_model/elf_section_header_table.lem @@ -0,0 +1,445 @@ +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)
\ No newline at end of file |