diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_program_header_table.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_program_header_table.ml | 605 |
1 files changed, 0 insertions, 605 deletions
diff --git a/lib/ocaml_rts/linksem/elf_program_header_table.ml b/lib/ocaml_rts/linksem/elf_program_header_table.ml deleted file mode 100644 index 6afe4d53..00000000 --- a/lib/ocaml_rts/linksem/elf_program_header_table.ml +++ /dev/null @@ -1,605 +0,0 @@ -(*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") |