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, 605 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/elf_program_header_table.ml b/lib/ocaml_rts/linksem/elf_program_header_table.ml new file mode 100644 index 00000000..6afe4d53 --- /dev/null +++ b/lib/ocaml_rts/linksem/elf_program_header_table.ml @@ -0,0 +1,605 @@ +(*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") |