(*Generated by Lem from elf_section_header.lem.*) open Lem_basic_classes open Lem_bool open Lem_list open Lem_num open Lem_string open Bitstring open Error open Elf_types open Show (** Special section indices. *) (** [shn_undef]: marks an undefined, missing or irrelevant section reference. *) let shn_undef : int =( 0) (** [shn_loreserve]: this specifies the lower bound of the range of reserved * indices. *) let shn_loreserve : int =( 65280) (* 0xff00 *) (** [shn_loproc]: start of the range reserved for processor-specific semantics. *) let shn_loproc : int =( 65280) (* 0xff00 *) (** [shn_hiproc]: end of the range reserved for processor-specific semantics. *) let shn_hiproc : int =( 65311) (* 0xff1f *) (** [shn_loos]: start of the range reserved for operating system-specific * semantics. *) let shn_loos : int =( 65312) (* 0xff20 *) (** [shn_hios]: end of the range reserved for operating system-specific * semantics. *) let shn_hios : 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 : int =( 65521) (* 0xfff1 *) (** [shn_common]: symbols defined relative to this index are common symbols, * such as unallocated C external variables. *) let shn_common : int =( 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 : int =( 65535) (* 0xffff *) (** [shn_hireserve]: specifies the upper-bound of reserved values. *) let shn_hireserve : int =( 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 : int =( 0) (** Section holds information defined by the program. *) let sht_progbits : 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 : int =( 2) let sht_dynsym : int =( 11) (** Section holds a string table *) let sht_strtab : int =( 3) (** Section holds relocation entries with explicit addends. An object file may * have multiple section of this type. *) let sht_rela : int =( 4) (** Section holds a symbol hash table. An object file may only have a single * hash table. *) let sht_hash : int =( 5) (** Section holds information for dynamic linking. An object file may only have * a single dynamic section. *) let sht_dynamic : int =( 6) (** Section holds information that marks the file in some way. *) let sht_note : int =( 7) (** Section occupies no space in the file but otherwise resembles a progbits * section. *) let sht_nobits : int =( 8) (** Section holds relocation entries without explicit addends. An object file * may have multiple section of this type. *) let sht_rel : int =( 9) (** Section type is reserved but has an unspecified meaning. *) let sht_shlib : 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 : 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 : 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 : 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 : 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. *) let sht_symtab_shndx : int =( 18) (** XXX: broken for the time being due to Lem bug. *) let sht_loos : int =( 0) let sht_hios : int =( 0) let sht_loproc : int =( 0) let sht_hiproc : int =( 0) let sht_louser : int =( 0) let sht_hiuser : int =( 0) (* XXX: constants too big for Lem to parse, apparently! let sht_loos : nat = 1610612736 (* 0x60000000 *) let sht_hios : nat = 1879048191 (* 0x6fffffff *) let sht_loproc : nat = 1879048192 (* 0x70000000 *) let sht_hiproc : nat = 2147483647 (* 0x7fffffff *) let sht_louser : nat = 2147483648 (* 0x80000000 *) let sht_hiuser : nat = 2415919103 (* 0x8fffffff *) *) let string_of_section_type 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 "SHT_OS_SPECIFIC" else if (i >= sht_loproc) && (i <= sht_hiproc) then "SHT_PROCESSOR_SPECIFIC" else if (i >= sht_louser) && (i <= sht_hiuser) then "SHT_USER_SPECIFIC" else "SHT UNDEFINED") (** Section header table entry type. *) type elf32_section_header_table_entry = { elf32_sh_name : Int64.t ; elf32_sh_type : Int64.t ; elf32_sh_flags : Int64.t ; elf32_sh_addr : Int64.t ; elf32_sh_offset : Int64.t ; elf32_sh_size : Int64.t ; elf32_sh_link : Int64.t ; elf32_sh_info : Int64.t ; elf32_sh_addralign : Int64.t ; elf32_sh_entsize : Int64.t } let read_elf32_section_header_table_entry (bs : Bitstring.bitstring) = (Ml_bindings.read_elf32_word bs >>= (fun (sh_name, bs) -> Ml_bindings.read_elf32_word bs >>= (fun (sh_type, bs) -> Ml_bindings.read_elf32_word bs >>= (fun (sh_flags, bs) -> Ml_bindings.read_elf32_addr bs >>= (fun (sh_addr, bs) -> Ml_bindings.read_elf32_off bs >>= (fun (sh_offset, bs) -> Ml_bindings.read_elf32_word bs >>= (fun (sh_size, bs) -> Ml_bindings.read_elf32_word bs >>= (fun (sh_link, bs) -> Ml_bindings.read_elf32_word bs >>= (fun (sh_info, bs) -> Ml_bindings.read_elf32_word bs >>= (fun (sh_addralign, bs) -> Ml_bindings.read_elf32_word 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 }))))))))))) let string_of_elf32_section_header_table_entry entry = (List.fold_right (^) [ "\t"; "Name: "; Int64.to_string entry.elf32_sh_name ; "\t"; "Type: "; string_of_section_type (Int64.to_int entry.elf32_sh_type) ; "\n\t"; "Flags: "; Int64.to_string entry.elf32_sh_flags ; "\t"; "Address: "; Int64.to_string entry.elf32_sh_addr ; "\t"; "Size: "; Int64.to_string entry.elf32_sh_size; "\n\n" ] "") let instance_Show_Show_Elf_section_header_elf32_section_header_table_entry_dict =({ show_method = string_of_elf32_section_header_table_entry}) (** Section header table type. *) type elf32_section_header_table = elf32_section_header_table_entry list ;; let rec read_elf32_section_header_table' entry_size bitstring0 = (if Bitstring.bitstring_length bitstring0 = 0 then return [] else let (eat, rest) = (Utility.partition_bitstring entry_size bitstring0) in read_elf32_section_header_table_entry eat >>= (fun sect -> read_elf32_section_header_table' entry_size rest >>= (fun tail -> return (sect::tail)))) (*val read_elf32_section_header_table : nat -> nat -> nat -> bitstring -> error (elf32_section_header_table * bitstring)*) let read_elf32_section_header_table size entry_size offset bitstring0 = (let (prefix, relevant) = (Utility.partition_bitstring offset bitstring0) in let (eat, rest) = (Utility.partition_bitstring (size * entry_size) relevant) in read_elf32_section_header_table' entry_size 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 Int64.to_int hdr.elf32_sh_size with | 0 -> true | m -> m = List.length tbl )) ;; (*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 -> (Int64.to_int x.elf32_sh_name = 0) && ((Int64.to_int x.elf32_sh_type = sht_null) && ((Int64.to_int x.elf32_sh_flags = 0) && ((Int64.to_int x.elf32_sh_addr = 0) && ((Int64.to_int x.elf32_sh_offset = 0) && ((Int64.to_int x.elf32_sh_info = 0) && ((Int64.to_int x.elf32_sh_addralign = 0) && ((Int64.to_int x.elf32_sh_entsize = 0) && elf32_size_correct x tbl))))))) (* XXX: more correctness criteria in time *) )) let string_of_elf32_section_header_table (tbl : elf32_section_header_table) : string = ("Section header table:" ^ ("\n" ^ List.fold_right (^) (List.map string_of_elf32_section_header_table_entry tbl) ""))