(*Generated by Lem from elf_program_header_table.lem.*) (** [elf_program_header_table] contains type, functions and other definitions * for working with program header tables and their entries and ELF segments. * Related files are [elf_interpreted_segments] which extracts information * derived from PHTs presented in this file and converts it into a more usable * format for processing. * * 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. *) open Lem_basic_classes open Lem_bool open Lem_function open Lem_list open Lem_maybe open Lem_num open Lem_string (*import Set*) open Elf_types_native_uint open Endianness open Byte_sequence open Error open Missing_pervasives open Show (** Segment types *) (** Unused array element. All other members of the structure are undefined. *) let elf_pt_null : Nat_big_num.num= (Nat_big_num.of_int 0) (** A loadable segment. *) let elf_pt_load : Nat_big_num.num= (Nat_big_num.of_int 1) (** Dynamic linking information. *) let elf_pt_dynamic : Nat_big_num.num= (Nat_big_num.of_int 2) (** Specifies the location and size of a null-terminated path name to be used to * invoke an interpreter. *) let elf_pt_interp : Nat_big_num.num= (Nat_big_num.of_int 3) (** Specifies location and size of auxiliary information. *) let elf_pt_note : Nat_big_num.num= (Nat_big_num.of_int 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_big_num.num= (Nat_big_num.of_int 5) (** Specifies the location and size of the program header table. *) let elf_pt_phdr : Nat_big_num.num= (Nat_big_num.of_int 6) (** Specifies the thread local storage (TLS) template. Need not be supported. *) let elf_pt_tls : Nat_big_num.num= (Nat_big_num.of_int 7) (** Start of reserved indices for operating system specific semantics. *) let elf_pt_loos : Nat_big_num.num= (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul(Nat_big_num.of_int 128)(Nat_big_num.of_int 128))(Nat_big_num.of_int 128))(Nat_big_num.of_int 256))(Nat_big_num.of_int 3)) (* 1610612736 (* 0x60000000 *) *) (** End of reserved indices for operating system specific semantics. *) let elf_pt_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 *) *) (** Start of reserved indices for processor specific semantics. *) let elf_pt_loproc : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 469762048)(Nat_big_num.of_int 4)) (* 1879048192 (* 0x70000000 *) *) (** End of reserved indices for processor specific semantics. *) let elf_pt_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 *) *) (** [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. *) (* XXX: is GNU stuff supposed to be hardcoded here? *) (*val string_of_segment_type : (natural -> string) -> (natural -> string) -> natural -> string*) let string_of_segment_type os proc pt:string= (if Nat_big_num.equal pt elf_pt_null then "NULL" else if Nat_big_num.equal pt elf_pt_load then "LOAD" else if Nat_big_num.equal pt elf_pt_dynamic then "DYNAMIC" else if Nat_big_num.equal pt elf_pt_interp then "INTERP" else if Nat_big_num.equal pt elf_pt_note then "NOTE" else if Nat_big_num.equal pt elf_pt_shlib then "SHLIB" else if Nat_big_num.equal pt elf_pt_phdr then "PHDR" else if Nat_big_num.equal pt elf_pt_tls then "TLS" else if Nat_big_num.greater_equal pt elf_pt_loos && Nat_big_num.less_equal pt elf_pt_hios then os pt else if Nat_big_num.greater_equal pt elf_pt_loproc && Nat_big_num.less_equal pt elf_pt_hiproc then proc pt else "Undefined or invalid segment type") (** Segments permission flags *) (** Execute bit *) let elf_pf_x : Nat_big_num.num= (Nat_big_num.of_int 1) (** Write bit *) let elf_pf_w : Nat_big_num.num= (Nat_big_num.of_int 2) (** Read bit *) let elf_pf_r : Nat_big_num.num= (Nat_big_num.of_int 4) (** The following two bit ranges are reserved for OS- and processor-specific * flags respectively. *) let elf_pf_maskos : Nat_big_num.num= (Nat_big_num.of_int 267386880) (* 0x0ff00000 *) let elf_pf_maskproc : Nat_big_num.num= (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 1006632960)) (* 0xf0000000 *) (** [exact_permission_of_permission m]: ELF has two interpretations of a RWX-style * permission bit [m], an exact permission and an allowable permission. These * permissions allow us to interpret a flag as an upper bound for behaviour and * an ABI-compliant implementation can choose to interpret the flag [m] as either. * * In the exact interpretation, the upper bound is exactly the natural interpretation * of the flag. This is encoded in [exact_permission_of_permission], which is * a glorified identity function, though included for completeness. *) (*val exact_permissions_of_permission : natural -> error natural*) let exact_permissions_of_permission m:(Nat_big_num.num)error= (if Nat_big_num.equal m(Nat_big_num.of_int 0) then return(Nat_big_num.of_int 0) else if Nat_big_num.equal m elf_pf_x then return(Nat_big_num.of_int 1) else if Nat_big_num.equal m elf_pf_w then return(Nat_big_num.of_int 2) else if Nat_big_num.equal m elf_pf_r then return(Nat_big_num.of_int 4) else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then return(Nat_big_num.of_int 3) else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then return(Nat_big_num.of_int 5) else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then return(Nat_big_num.of_int 6) else if Nat_big_num.equal m (Nat_big_num.add (Nat_big_num.add elf_pf_x elf_pf_r) elf_pf_w) then return(Nat_big_num.of_int 7) else fail "exact_permission_of_permission: invalid permission flag") (** [allowable_permission_of_permission m]: ELF has two interpretations of a RWX-style * permission bit [m], an exact permission and an allowable permission. These * permissions allow us to interpret a flag as an upper bound for behaviour and * an ABI-compliant implementation can choose to interpret the flag [m] as either. * * In the allowable interpretation, the upper bound is more lax than the natural * interpretation of the flag. *) (*val allowable_permissions_of_permission : natural -> error natural*) let allowable_permissions_of_permission m:(Nat_big_num.num)error= (if Nat_big_num.equal m(Nat_big_num.of_int 0) then return(Nat_big_num.of_int 0) else if Nat_big_num.equal m elf_pf_x then return(Nat_big_num.of_int 5) else if Nat_big_num.equal m elf_pf_w then return(Nat_big_num.of_int 7) else if Nat_big_num.equal m elf_pf_r then return(Nat_big_num.of_int 5) else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then return(Nat_big_num.of_int 7) else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then return(Nat_big_num.of_int 5) else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then return(Nat_big_num.of_int 7) else if Nat_big_num.equal m (Nat_big_num.add (Nat_big_num.add elf_pf_x elf_pf_r) elf_pf_w) then return(Nat_big_num.of_int 7) else fail "exact_permission_of_permission: invalid permission flag") (** [string_of_elf_segment_permissions m] produces a string-based representation * of an ELF segment's permission field. * TODO: expand this as is needed by the validation tests. *) (*val string_of_elf_segment_permissions : natural -> string*) let string_of_elf_segment_permissions m:string= (if Nat_big_num.equal m(Nat_big_num.of_int 0) then " " else if Nat_big_num.equal m elf_pf_x then " E" else if Nat_big_num.equal m elf_pf_w then " W " else if Nat_big_num.equal m elf_pf_r then "R " else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then " WE" else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then "R E" else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then "RW " else if Nat_big_num.equal m (Nat_big_num.add (Nat_big_num.add elf_pf_x elf_pf_r) elf_pf_w) then "RWE" else "Invalid permisssion flag") (** 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 : Uint32.uint32 (** Type of the segment *) ; elf32_p_offset : Uint32.uint32 (** Offset from beginning of file for segment *) ; elf32_p_vaddr : Uint32.uint32 (** Virtual address for segment in memory *) ; elf32_p_paddr : Uint32.uint32 (** Physical address for segment *) ; elf32_p_filesz : Uint32.uint32 (** Size of segment in file, in bytes *) ; elf32_p_memsz : Uint32.uint32 (** Size of segment in memory image, in bytes *) ; elf32_p_flags : Uint32.uint32 (** Segment flags *) ; elf32_p_align : Uint32.uint32 (** Segment alignment memory for memory and file *) } (** [compare_elf32_program_header_table_entry ent1 ent2] is an ordering-comparison * function on program header table entries suitable for constructing sets, * finite maps, and other ordered data types with. *) (*val compare_elf32_program_header_table_entry : elf32_program_header_table_entry -> elf32_program_header_table_entry -> ordering*) let compare_elf32_program_header_table_entry h1 h2:int= (lexicographic_compare Nat_big_num.compare [Nat_big_num.of_string (Uint32.to_string h1.elf32_p_type); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_offset); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_vaddr); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_paddr); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_filesz); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_memsz); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_flags); Nat_big_num.of_string (Uint32.to_string h1.elf32_p_align)] [Nat_big_num.of_string (Uint32.to_string h2.elf32_p_type); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_offset); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_vaddr); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_paddr); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_filesz); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_memsz); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_flags); Nat_big_num.of_string (Uint32.to_string h2.elf32_p_align)]) let instance_Basic_classes_Ord_Elf_program_header_table_elf32_program_header_table_entry_dict:(elf32_program_header_table_entry)ord_class= ({ compare_method = compare_elf32_program_header_table_entry; isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_program_header_table_entry f1 f2) (-1)))); isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_program_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0]))); isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_program_header_table_entry f1 f2) 1))); isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_program_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))}) (** 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 : Uint32.uint32 (** Type of the segment *) ; elf64_p_flags : Uint32.uint32 (** Segment flags *) ; elf64_p_offset : Uint64.uint64 (** Offset from beginning of file for segment *) ; elf64_p_vaddr : Uint64.uint64 (** Virtual address for segment in memory *) ; elf64_p_paddr : Uint64.uint64 (** Physical address for segment *) ; elf64_p_filesz : Uint64.uint64 (** Size of segment in file, in bytes *) ; elf64_p_memsz : Uint64.uint64 (** Size of segment in memory image, in bytes *) ; elf64_p_align : Uint64.uint64 (** Segment alignment memory for memory and file *) } (** [compare_elf64_program_header_table_entry ent1 ent2] is an ordering-comparison * function on program header table entries suitable for constructing sets, * finite maps, and other ordered data types with. *) (*val compare_elf64_program_header_table_entry : elf64_program_header_table_entry -> elf64_program_header_table_entry -> ordering*) let compare_elf64_program_header_table_entry h1 h2:int= (lexicographic_compare Nat_big_num.compare [Nat_big_num.of_string (Uint32.to_string h1.elf64_p_type); Nat_big_num.of_string (Uint64.to_string h1.elf64_p_offset); Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_vaddr; Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_paddr; Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_filesz; Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_memsz; Nat_big_num.of_string (Uint32.to_string h1.elf64_p_flags); Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_align] [Nat_big_num.of_string (Uint32.to_string h2.elf64_p_type); Nat_big_num.of_string (Uint64.to_string h2.elf64_p_offset); Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_vaddr; Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_paddr; Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_filesz; Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_memsz; Nat_big_num.of_string (Uint32.to_string h2.elf64_p_flags); Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_align]) let instance_Basic_classes_Ord_Elf_program_header_table_elf64_program_header_table_entry_dict:(elf64_program_header_table_entry)ord_class= ({ compare_method = compare_elf64_program_header_table_entry; isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_program_header_table_entry f1 f2) (-1)))); isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_program_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0]))); isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_program_header_table_entry f1 f2) 1))); isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_program_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))}) (** [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 : (natural -> string) -> (natural -> string) -> elf32_program_header_table_entry -> string*) let string_of_elf32_program_header_table_entry os proc entry:string= (unlines [ ("\t" ^ ("Segment type: " ^ string_of_segment_type os proc (Nat_big_num.of_string (Uint32.to_string entry.elf32_p_type)))) ; ("\t" ^ ("Offset: " ^ Uint32.to_string entry.elf32_p_offset)) ; ("\t" ^ ("Virtual address: " ^ Uint32.to_string entry.elf32_p_vaddr)) ; ("\t" ^ ("Physical address: " ^ Uint32.to_string entry.elf32_p_paddr)) ; ("\t" ^ ("Segment size (bytes): " ^ Uint32.to_string entry.elf32_p_filesz)) ; ("\t" ^ ("Segment size in memory image (bytes): " ^ Uint32.to_string entry.elf32_p_memsz)) ; ("\t" ^ ("Flags: " ^ Uint32.to_string entry.elf32_p_flags)) ; ("\t" ^ ("Alignment: " ^ Uint32.to_string 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 : (natural -> string) -> (natural -> string) -> elf64_program_header_table_entry -> string*) let string_of_elf64_program_header_table_entry os proc entry:string= (unlines [ ("\t" ^ ("Segment type: " ^ string_of_segment_type os proc (Nat_big_num.of_string (Uint32.to_string entry.elf64_p_type)))) ; ("\t" ^ ("Offset: " ^ Uint64.to_string entry.elf64_p_offset)) ; ("\t" ^ ("Virtual address: " ^ Uint64.to_string entry.elf64_p_vaddr)) ; ("\t" ^ ("Physical address: " ^ Uint64.to_string entry.elf64_p_paddr)) ; ("\t" ^ ("Segment size (bytes): " ^ Uint64.to_string entry.elf64_p_filesz)) ; ("\t" ^ ("Segment size in memory image (bytes): " ^ Uint64.to_string entry.elf64_p_memsz)) ; ("\t" ^ ("Flags: " ^ Uint32.to_string entry.elf64_p_flags)) ; ("\t" ^ ("Alignment: " ^ Uint64.to_string 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:elf32_program_header_table_entry ->string= (string_of_elf32_program_header_table_entry ((fun y->"*Default OS specific print*")) ((fun y->"*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:elf64_program_header_table_entry ->string= (string_of_elf64_program_header_table_entry ((fun y->"*Default OS specific print*")) ((fun y->"*Default processor specific print*"))) let instance_Show_Show_Elf_program_header_table_elf32_program_header_table_entry_dict:(elf32_program_header_table_entry)show_class= ({ show_method = string_of_elf32_program_header_table_entry_default}) let instance_Show_Show_Elf_program_header_table_elf64_program_header_table_entry_dict:(elf64_program_header_table_entry)show_class= ({ show_method = string_of_elf64_program_header_table_entry_default}) (** Parsing and blitting *) (** [bytes_of_elf32_program_header_table_entry ed ent] blits a 32-bit program * header table entry [ent] into a byte sequence assuming endianness [ed]. *) (*val bytes_of_elf32_program_header_table_entry : endianness -> elf32_program_header_table_entry -> byte_sequence*) let bytes_of_elf32_program_header_table_entry endian entry:byte_sequence= (Byte_sequence.from_byte_lists [ bytes_of_elf32_word endian entry.elf32_p_type ; bytes_of_elf32_off endian entry.elf32_p_offset ; bytes_of_elf32_addr endian entry.elf32_p_vaddr ; bytes_of_elf32_addr endian entry.elf32_p_paddr ; bytes_of_elf32_word endian entry.elf32_p_filesz ; bytes_of_elf32_word endian entry.elf32_p_memsz ; bytes_of_elf32_word endian entry.elf32_p_flags ; bytes_of_elf32_word endian entry.elf32_p_align ]) (** [bytes_of_elf64_program_header_table_entry ed ent] blits a 64-bit program * header table entry [ent] into a byte sequence assuming endianness [ed]. *) (*val bytes_of_elf64_program_header_table_entry : endianness -> elf64_program_header_table_entry -> byte_sequence*) let bytes_of_elf64_program_header_table_entry endian entry:byte_sequence= (Byte_sequence.from_byte_lists [ bytes_of_elf64_word endian entry.elf64_p_type ; bytes_of_elf64_word endian entry.elf64_p_flags ; bytes_of_elf64_off endian entry.elf64_p_offset ; bytes_of_elf64_addr endian entry.elf64_p_vaddr ; bytes_of_elf64_addr endian entry.elf64_p_paddr ; bytes_of_elf64_xword endian entry.elf64_p_filesz ; bytes_of_elf64_xword endian entry.elf64_p_memsz ; bytes_of_elf64_xword endian entry.elf64_p_align ]) (** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table * entry from byte sequence [bs0] assuming endianness [endian]. If [bs0] is larger * than necessary, the excess is returned from the function, too. * Fails if the entry cannot be read. *) (*val read_elf32_program_header_table_entry : endianness -> byte_sequence -> error (elf32_program_header_table_entry * byte_sequence)*) let read_elf32_program_header_table_entry endian bs:(elf32_program_header_table_entry*byte_sequence)error= (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)))))))))) (** [read_elf64_program_header_table_entry endian bs0] reads an ELF64 program header table * entry from byte sequence [bs0] assuming endianness [endian]. If [bs0] is larger * than necessary, the excess is returned from the function, too. * Fails if the entry cannot be read. *) (*val read_elf64_program_header_table_entry : endianness -> byte_sequence -> error (elf64_program_header_table_entry * byte_sequence)*) let read_elf64_program_header_table_entry endian bs:(elf64_program_header_table_entry*byte_sequence)error= (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 = elf32_program_header_table_entry list (** 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 = elf64_program_header_table_entry list (** [bytes_of_elf32_program_header_table ed tbl] blits an ELF32 program header * table into a byte sequence assuming endianness [ed]. *) let bytes_of_elf32_program_header_table endian tbl:byte_sequence= (Byte_sequence.concat0 (Lem_list.map (bytes_of_elf32_program_header_table_entry endian) tbl)) (** [bytes_of_elf64_program_header_table ed tbl] blits an ELF64 program header * table into a byte sequence assuming endianness [ed]. *) let bytes_of_elf64_program_header_table endian tbl:byte_sequence= (Byte_sequence.concat0 (Lem_list.map (bytes_of_elf64_program_header_table_entry endian) tbl)) (** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from * byte_sequence [bs0] assuming endianness [endian]. The byte_sequence [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:((elf32_program_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_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 * byte_sequence [bs0] assuming endianness [endian]. The byte_sequence [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:((elf64_program_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_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 byte_sequence [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 : natural -> endianness -> byte_sequence -> error (elf32_program_header_table * byte_sequence)*) let read_elf32_program_header_table table_size endian bs0:((elf32_program_header_table_entry)list*byte_sequence)error= (partition0 table_size bs0 >>= (fun (eat, rest) -> 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 byte_sequence [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 : natural -> endianness -> byte_sequence -> error (elf64_program_header_table * byte_sequence)*) let read_elf64_program_header_table table_size endian bs0:((elf64_program_header_table_entry)list*byte_sequence)error= (partition0 table_size bs0 >>= (fun (eat, rest) -> 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_big_num.num -> string) * (Nat_big_num.num -> 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:string= (unlines (Lem_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:string= (unlines (Lem_list.map (string_of_elf64_program_header_table_entry os proc) tbl)) (** Static/dynamic linkage *) (** [get_elf32_dynamic_linked pht] tests whether an ELF32 file is a dynamically * linked object by traversing the program header table and attempting to find * a header describing a segment with the name of an associated interpreter. * Returns [true] if any such header is found, [false] --- indicating static * linkage --- otherwise. *) (*val get_elf32_dynamic_linked : elf32_program_header_table -> bool*) let get_elf32_dynamic_linked pht:bool= (List.exists (fun p -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string p.elf32_p_type)) elf_pt_interp) pht) (** [get_elf64_dynamic_linked pht] tests whether an ELF64 file is a dynamically * linked object by traversing the program header table and attempting to find * a header describing a segment with the name of an associated interpreter. * Returns [true] if any such header is found, [false] --- indicating static * linkage --- otherwise. *) (*val get_elf64_dynamic_linked : elf64_program_header_table -> bool*) let get_elf64_dynamic_linked pht:bool= (List.exists (fun p -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string p.elf64_p_type)) elf_pt_interp) pht) (** [get_elf32_static_linked] is a utility function defined as the inverse * of [get_elf32_dynamic_linked]. *) (*val get_elf32_static_linked : elf32_program_header_table -> bool*) let get_elf32_static_linked pht:bool= (not (get_elf32_dynamic_linked pht)) (** [get_elf64_static_linked] is a utility function defined as the inverse * of [get_elf64_dynamic_linked]. *) (*val get_elf64_static_linked : elf64_program_header_table -> bool*) let get_elf64_static_linked pht:bool= (not (get_elf64_dynamic_linked pht)) (** [get_elf32_requested_interpreter ent bs0] extracts the requested interpreter * of a dynamically linkable ELF file from that file's program header table * entry of type PT_INTERP, [ent]. Interpreter string is extracted from byte * sequence [bs0]. * Fails if [ent] is not of type PT_INTERP, or if transcription otherwise fails. *) (*val get_elf32_requested_interpreter : elf32_program_header_table_entry -> byte_sequence -> error string*) let get_elf32_requested_interpreter pent bs0:(string)error= (if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_type)) elf_pt_interp then let off = (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_offset)) in let siz = (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_filesz)) in Byte_sequence.offset_and_cut off ( Nat_big_num.sub_nat siz(Nat_big_num.of_int 1)) bs0 >>= (fun cut -> return (Byte_sequence.string_of_byte_sequence cut)) else fail "get_elf32_requested_interpreter: not an INTERP segment header") (** [get_elf64_requested_interpreter ent bs0] extracts the requested interpreter * of a dynamically linkable ELF file from that file's program header table * entry of type PT_INTERP, [ent]. Interpreter string is extracted from byte * sequence [bs0]. * Fails if [ent] is not of type PT_INTERP, or if transcription otherwise fails. *) (*val get_elf64_requested_interpreter : elf64_program_header_table_entry -> byte_sequence -> error string*) let get_elf64_requested_interpreter pent bs0:(string)error= (if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string pent.elf64_p_type)) elf_pt_interp then let off = (Nat_big_num.of_string (Uint64.to_string pent.elf64_p_offset)) in let siz = (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_filesz) in Byte_sequence.offset_and_cut off ( Nat_big_num.sub_nat siz(Nat_big_num.of_int 1)) bs0 >>= (fun cut -> return (Byte_sequence.string_of_byte_sequence cut)) else fail "get_elf64_requested_interpreter: not an INTERP segment header")