(*Generated by Lem from elf_dynamic.lem.*) (** [elf_dynamic] module exports types and definitions relating to the dynamic * section and dynamic linking functionality of an ELF file. *) open Lem_basic_classes open Lem_bool open Lem_list open Lem_num open Lem_string open Byte_sequence open Endianness open Error open Show open String_table open Elf_file open Elf_header open Elf_relocation open Elf_section_header_table open Elf_program_header_table open Elf_types_native_uint (** Validity checks *) (** [is_elf32_valid_program_header_table_for_dynamic_linking pht] checks whether * a program header table [pht] is a valid program header table for an ELF file * that will be potentially dynamically linked. Returns true if there is exactly * one segment header of type [elf_pt_interp], i.e. contains a string pointing * to the requested dynamic interpreter. *) (*val is_elf32_valid_program_header_table_for_dynamic_linking : elf32_program_header_table -> bool*) let is_elf32_valid_program_header_table_for_dynamic_linking pht:bool= (List.length (List.filter (fun x -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf32_p_type)) elf_pt_interp) pht) = 1) (** [is_elf64_valid_program_header_table_for_dynamic_linking pht] checks whether * a program header table [pht] is a valid program header table for an ELF file * that will be potentially dynamically linked. Returns true if there is exactly * one segment header of type [elf_pt_interp], i.e. contains a string pointing * to the requested dynamic interpreter. *) (*val is_elf64_valid_program_header_table_for_dynamic_linking : elf64_program_header_table -> bool*) let is_elf64_valid_program_header_table_for_dynamic_linking pht:bool= (List.length (List.filter (fun x -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf64_p_type)) elf_pt_interp) pht) = 1) (** Dynamic section entry *) (** [dyn_union] represents the C-union type used in the definition of [elf32_dyn] * and [elf64_dyn] types below. Some section tags correspond to entries where * the fields are either unspecified or ignored, hence the presence of the * [D_Ignored] constructor. *) type( 'a, 'b) dyn_union = D_Val of 'a | D_Ptr of 'b | D_Ignored of byte_sequence (** [elf32_dyn] captures the notion of an ELF32 dynamic section entry. * Specialises the [dyn_union] type above to using [elf32_word] values and * [elf32_addr] pointers. *) type elf32_dyn = { elf32_dyn_tag : Int32.t (** The type of the entry. *) ; elf32_dyn_d_un : (Uint32.uint32, Uint32.uint32) dyn_union (** The value of the entry, stored as a union. *) } (** [elf64_dyn] captures the notion of an ELF32 dynamic section entry. * Specialises the [dyn_union] type above to using [elf64_xword] values and * [elf64_addr] pointers. *) type elf64_dyn = { elf64_dyn_tag : Int64.t (** The type of the entry. *) ; elf64_dyn_d_un : (Uint64.uint64, Uint64.uint64) dyn_union (** The value of the entry, stored as a union. *) } (** Dynamic section tags *) (** [dt_null] marks the end of the dynamic array *) let dt_null : Nat_big_num.num= (Nat_big_num.of_int 0) (** [dt_needed] holds the string table offset of a string containing the name of * a needed library. *) let dt_needed : Nat_big_num.num= (Nat_big_num.of_int 1) (** [dt_pltrelsz] holds the size in bytes of relocation entries associated with * the PLT. *) let dt_pltrelsz : Nat_big_num.num= (Nat_big_num.of_int 2) (** [dt_pltgot] holds an address associated with the PLT or GOT. *) let dt_pltgot : Nat_big_num.num= (Nat_big_num.of_int 3) (** [dt_hash] holds the address of a symbol-table hash. *) let dt_hash : Nat_big_num.num= (Nat_big_num.of_int 4) (** [dt_strtab] holds the address of the string table. *) let dt_strtab : Nat_big_num.num= (Nat_big_num.of_int 5) (** [dt_symtab] holds the address of a symbol table. *) let dt_symtab : Nat_big_num.num= (Nat_big_num.of_int 6) (** [dt_rela] holds the address of a relocation table. *) let dt_rela : Nat_big_num.num= (Nat_big_num.of_int 7) (** [dt_relasz] holds the size in bytes of the relocation table. *) let dt_relasz : Nat_big_num.num= (Nat_big_num.of_int 8) (** [dt_relaent] holds the size in bytes of a relocation table entry. *) let dt_relaent : Nat_big_num.num= (Nat_big_num.of_int 9) (** [dt_strsz] holds the size in bytes of the string table. *) let dt_strsz : Nat_big_num.num= (Nat_big_num.of_int 10) (** [dt_syment] holds the size in bytes of a symbol table entry. *) let dt_syment : Nat_big_num.num= (Nat_big_num.of_int 11) (** [dt_init] holds the address of the initialisation function. *) let dt_init : Nat_big_num.num= (Nat_big_num.of_int 12) (** [dt_fini] holds the address of the finalisation function. *) let dt_fini : Nat_big_num.num= (Nat_big_num.of_int 13) (** [dt_soname] holds the string table offset of a string containing the shared- * object name. *) let dt_soname : Nat_big_num.num= (Nat_big_num.of_int 14) (** [dt_rpath] holds the string table offset of a string containing the library * search path. *) let dt_rpath : Nat_big_num.num= (Nat_big_num.of_int 15) (** [dt_symbolic] alters the linker's symbol resolution algorithm so that names * are resolved first from the shared object file itself, rather than the * executable file. *) let dt_symbolic : Nat_big_num.num= (Nat_big_num.of_int 16) (** [dt_rel] is similar to [dt_rela] except its table has implicit addends. *) let dt_rel : Nat_big_num.num= (Nat_big_num.of_int 17) (** [dt_relsz] holds the size in bytes of the [dt_rel] relocation table. *) let dt_relsz : Nat_big_num.num= (Nat_big_num.of_int 18) (** [dt_relent] holds the size in bytes of a [dt_rel] relocation entry. *) let dt_relent : Nat_big_num.num= (Nat_big_num.of_int 19) (** [dt_pltrel] specifies the type of relocation entry to which the PLT refers. *) let dt_pltrel : Nat_big_num.num= (Nat_big_num.of_int 20) (** [dt_debug] is used for debugging and its purpose is not specified in the ABI. * Programs using this entry are not ABI-conformant. *) let dt_debug : Nat_big_num.num= (Nat_big_num.of_int 21) (** [dt_textrel] absence of this entry indicates that no relocation entry should * cause a modification to a non-writable segment. Otherwise, if present, one * or more relocation entries may request modifications to a non-writable * segment. *) let dt_textrel : Nat_big_num.num= (Nat_big_num.of_int 22) (** [dt_jmprel]'s member holds the address of relocation entries associated with * the PLT. *) let dt_jmprel : Nat_big_num.num= (Nat_big_num.of_int 23) (** [dt_bindnow] instructs the linker to process all relocations for the object * containing the entry before transferring control to the program. *) let dt_bindnow : Nat_big_num.num= (Nat_big_num.of_int 24) (** [dt_init_array] holds the address to the array of pointers to initialisation * functions. *) let dt_init_array : Nat_big_num.num= (Nat_big_num.of_int 25) (** [dt_fini_array] holds the address to the array of pointers to finalisation * functions. *) let dt_fini_array : Nat_big_num.num= (Nat_big_num.of_int 26) (** [dt_init_arraysz] holds the size in bytes of the array of pointers to * initialisation functions. *) let dt_init_arraysz : Nat_big_num.num= (Nat_big_num.of_int 27) (** [dt_fini_arraysz] holds the size in bytes of the array of pointers to * finalisation functions. *) let dt_fini_arraysz : Nat_big_num.num= (Nat_big_num.of_int 28) (** [dt_runpath] holds an offset into the string table holding a string containing * the library search path. *) let dt_runpath : Nat_big_num.num= (Nat_big_num.of_int 29) (** [dt_flags] holds flag values specific to the object being loaded. *) let dt_flags : Nat_big_num.num= (Nat_big_num.of_int 30) let dt_encoding : Nat_big_num.num= (Nat_big_num.of_int 32) (** [dt_preinit_array] holds the address to the array of pointers of pre- * initialisation functions. *) let dt_preinit_array : Nat_big_num.num= (Nat_big_num.of_int 32) (** [dt_preinit_arraysz] holds the size in bytes of the array of pointers of * pre-initialisation functions. *) let dt_preinit_arraysz : Nat_big_num.num= (Nat_big_num.of_int 33) (** [dt_loos] and [dt_hios]: this inclusive range is reserved for OS-specific * semantics. *) let dt_loos : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 805306374))(Nat_big_num.of_int 1)) (* 0x6000000D *) let dt_hios : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939522048)) (* 0x6ffff000 *) (** [dt_loproc] and [dt_hiproc]: this inclusive range is reserved for processor * specific semantics. *) let dt_loproc : Nat_big_num.num= ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524096)) (* 0x70000000 *) let dt_hiproc : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 1073741823))(Nat_big_num.of_int 1)) (* 0x7fffffff *) (** [string_of_dynamic_tag so t os proc] produces a string-based representation of * dynamic section tag [t]. For tag values between LO_OS and HI_OS [os] is * used to produce the resulting value. For tag values between LO_PROC and * HI_PROC [proc] is used to produce the resulting value. Boolean flag [so] * indicates whether the flag in question is derived from a shared object file, * which alters the printing of ENCODING and PRE_INITARRAY flags. *) (*val string_of_dynamic_tag : bool -> natural -> (natural -> bool) -> (natural -> string) -> (natural -> string) -> string*) let string_of_dynamic_tag shared_object tag os_additional_ranges os proc:string= (if Nat_big_num.equal tag dt_null then "NULL" else if Nat_big_num.equal tag dt_needed then "NEEDED" else if Nat_big_num.equal tag dt_pltrelsz then "PLTRELSZ" else if Nat_big_num.equal tag dt_pltgot then "PLTGOT" else if Nat_big_num.equal tag dt_hash then "HASH" else if Nat_big_num.equal tag dt_strtab then "STRTAB" else if Nat_big_num.equal tag dt_symtab then "SYMTAB" else if Nat_big_num.equal tag dt_rela then "RELA" else if Nat_big_num.equal tag dt_relasz then "RELASZ" else if Nat_big_num.equal tag dt_relaent then "RELAENT" else if Nat_big_num.equal tag dt_strsz then "STRSZ" else if Nat_big_num.equal tag dt_syment then "SYMENT" else if Nat_big_num.equal tag dt_init then "INIT" else if Nat_big_num.equal tag dt_fini then "FINI" else if Nat_big_num.equal tag dt_soname then "SONAME" else if Nat_big_num.equal tag dt_rpath then "RPATH" else if Nat_big_num.equal tag dt_symbolic then "SYMBOLIC" else if Nat_big_num.equal tag dt_rel then "REL" else if Nat_big_num.equal tag dt_relsz then "RELSZ" else if Nat_big_num.equal tag dt_relent then "RELENT" else if Nat_big_num.equal tag dt_pltrel then "PLTREL" else if Nat_big_num.equal tag dt_debug then "DEBUG" else if Nat_big_num.equal tag dt_textrel then "TEXTREL" else if Nat_big_num.equal tag dt_jmprel then "JMPREL" else if Nat_big_num.equal tag dt_bindnow then "BIND_NOW" else if Nat_big_num.equal tag dt_init_array then "INIT_ARRAY" else if Nat_big_num.equal tag dt_fini_array then "FINI_ARRAY" else if Nat_big_num.equal tag dt_init_arraysz then "INIT_ARRAYSZ" else if Nat_big_num.equal tag dt_fini_arraysz then "FINI_ARRAYSZ" else if Nat_big_num.equal tag dt_runpath then "RUNPATH" else if Nat_big_num.equal tag dt_flags then "FLAGS" else if Nat_big_num.equal tag dt_encoding then if not shared_object then "ENCODING" else "PREINIT_ARRAY" else if Nat_big_num.equal tag dt_preinit_arraysz then "PREINIT_ARRAYSZ" else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then proc tag else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then os tag else if os_additional_ranges tag then os tag else "Invalid dynamic section tag") (** [tag_correspondence] is a type used to emulate the functionality of a C-union * in Lem. The type records whether the union should be interpreted as a value, * a pointer, or a "do not care" value. An accompanying function will map a * dynamic section tag to a [tag_correspondence], so that transcription functions * know how to properly use the [dyn_union] value in a dynamic section entry. *) type tag_correspondence = C_Val (** [dyn_union] should be interpreted as a value. *) | C_Ptr (** [dyn_union] should be interpreted as a pointer. *) | C_Ignored (** [dyn_union] is irrelevant, so we do not care. *) (** [tag_correspondence_of_tag tag os_additional_ranges os proc] produces a * [tag_correspondence] value for a given dynamic tag, [tag]. Some tag values * are reserved for interpretation by the OS or processor supplement (i.e. the * ABI). We therefore also take in a predicate, [os_additional_ranges], that * recognises when a tag is "special" for a given ABI, and a means of interpreting * that tag, using [os] and [proc] functions. *) (*val tag_correspondence_of_tag : bool -> natural -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> error tag_correspondence*) let tag_correspondence_of_tag shared_object tag os_additional_ranges os proc:(tag_correspondence)error= (if Nat_big_num.equal tag dt_null then return C_Ignored else if Nat_big_num.equal tag dt_needed then return C_Val else if Nat_big_num.equal tag dt_pltrelsz then return C_Val else if Nat_big_num.equal tag dt_pltgot then return C_Ptr else if Nat_big_num.equal tag dt_hash then return C_Ptr else if Nat_big_num.equal tag dt_strtab then return C_Ptr else if Nat_big_num.equal tag dt_symtab then return C_Ptr else if Nat_big_num.equal tag dt_rela then return C_Ptr else if Nat_big_num.equal tag dt_relasz then return C_Val else if Nat_big_num.equal tag dt_relaent then return C_Val else if Nat_big_num.equal tag dt_strsz then return C_Val else if Nat_big_num.equal tag dt_syment then return C_Val else if Nat_big_num.equal tag dt_init then return C_Ptr else if Nat_big_num.equal tag dt_fini then return C_Ptr else if Nat_big_num.equal tag dt_soname then return C_Val else if Nat_big_num.equal tag dt_rpath then return C_Val else if Nat_big_num.equal tag dt_symbolic then return C_Ignored else if Nat_big_num.equal tag dt_rel then return C_Ptr else if Nat_big_num.equal tag dt_relsz then return C_Val else if Nat_big_num.equal tag dt_relent then return C_Val else if Nat_big_num.equal tag dt_pltrel then return C_Val else if Nat_big_num.equal tag dt_debug then return C_Ptr else if Nat_big_num.equal tag dt_textrel then return C_Ignored else if Nat_big_num.equal tag dt_jmprel then return C_Ptr else if Nat_big_num.equal tag dt_bindnow then return C_Ignored else if Nat_big_num.equal tag dt_init_array then return C_Ptr else if Nat_big_num.equal tag dt_fini_array then return C_Ptr else if Nat_big_num.equal tag dt_init_arraysz then return C_Val else if Nat_big_num.equal tag dt_fini_arraysz then return C_Val else if Nat_big_num.equal tag dt_runpath then return C_Val else if Nat_big_num.equal tag dt_flags then return C_Val else if Nat_big_num.equal tag dt_encoding then if not shared_object then return C_Ignored else return C_Ptr else if Nat_big_num.equal tag dt_preinit_arraysz then return C_Val else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then proc tag else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then os tag else if os_additional_ranges tag then os tag else fail ("tag_correspondence_of_tag: invalid dynamic section tag")) (** [read_elf32_dyn endian bs0 so os_additional_ranges os proc] reads an [elf32_dyn] * record from byte sequence [bs0], assuming endianness [endian]. As mentioned * above some ABIs reserve additional tag values for their own purposes. These * are recognised by the predicate [os_additional_ranges] and interpreted by * the functions [os] and [proc]. Fails if the transcription of the record from * [bs0] fails, or if [os] or [proc] fail. *) (*val read_elf32_dyn : endianness -> byte_sequence -> bool -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> error (elf32_dyn * byte_sequence)*) let read_elf32_dyn endian bs0 shared_object os_additional_ranges os proc:(elf32_dyn*byte_sequence)error= (read_elf32_sword endian bs0 >>= (fun (tag0, bs1) -> let tag = (Nat_big_num.abs (Nat_big_num.of_int32 tag0)) in tag_correspondence_of_tag shared_object tag os_additional_ranges os proc >>= (fun corr -> (match corr with | C_Ptr -> read_elf32_addr endian bs1 >>= (fun (ptr, bs2) -> return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ptr ptr) }, bs2)) | C_Val -> read_elf32_word endian bs1 >>= (fun (vl, bs2) -> return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Val vl) }, bs2)) | C_Ignored -> (match endian with | Big -> read_4_bytes_be bs1 >>= (fun ((b1, b2, b3, b4), bs2) -> let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4]]) in return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ignored cut) }, bs2)) | Little -> read_4_bytes_le bs1 >>= (fun ((b1, b2, b3, b4), bs2) -> let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4]]) in return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ignored cut) }, bs2)) ) )))) (** [read_elf64_dyn endian bs0 os_additional_ranges os proc] reads an [elf64_dyn] * record from byte sequence [bs0], assuming endianness [endian]. As mentioned * above some ABIs reserve additional tag values for their own purposes. These * are recognised by the predicate [os_additional_ranges] and interpreted by * the functions [os] and [proc]. Fails if the transcription of the record from * [bs0] fails, or if [os] or [proc] fail. *) (*val read_elf64_dyn : endianness -> byte_sequence -> bool -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> error (elf64_dyn * byte_sequence)*) let read_elf64_dyn endian bs0 shared_object os_additional_ranges os proc:(elf64_dyn*byte_sequence)error= (read_elf64_sxword endian bs0 >>= (fun (tag0, bs1) -> let tag = (Nat_big_num.abs (Nat_big_num.of_int64 tag0)) in tag_correspondence_of_tag shared_object tag os_additional_ranges os proc >>= (fun corr -> (match corr with | C_Ptr -> read_elf64_addr endian bs1 >>= (fun (ptr, bs2) -> return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ptr ptr) }, bs2)) | C_Val -> read_elf64_xword endian bs1 >>= (fun (vl, bs2) -> return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Val vl) }, bs2)) | C_Ignored -> (match endian with | Big -> read_8_bytes_be bs1 >>= (fun ((b1, b2, b3, b4, b5, b6, b7, b8), bs2) -> let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4; b5; b6; b7; b8]]) in return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ignored cut) }, bs2)) | Little -> read_8_bytes_le bs1 >>= (fun ((b1, b2, b3, b4, b5, b6, b7, b8), bs2) -> let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4; b5; b6; b7; b8]]) in return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ignored cut) }, bs2)) ) )))) (** [obtain_elf32_dynamic_section_contents' endian bs0 os_additional_ranges os * proc] exhaustively reads in [elf32_dyn] values from byte sequence [bs0], * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and * [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an * [elf32_dyn] entry is not 0. *) (*val obtain_elf32_dynamic_section_contents' : endianness -> byte_sequence -> bool -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> error (list elf32_dyn)*) let rec obtain_elf32_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc:((elf32_dyn)list)error= (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then return [] else read_elf32_dyn endian bs0 shared_object os_additional_ranges os proc >>= (fun (head, bs0) -> if Nat_big_num.equal (Nat_big_num.of_int32 head.elf32_dyn_tag) ( dt_null) then (* DT_NULL marks end of array *) return [head] else obtain_elf32_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc >>= (fun tail -> return (head::tail)))) (** [obtain_elf64_dynamic_section_contents' endian bs0 os_additional_ranges os * proc] exhaustively reads in [elf64_dyn] values from byte sequence [bs0], * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and * [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an * [elf64_dyn] entry is not 0. *) (*val obtain_elf64_dynamic_section_contents' : endianness -> byte_sequence -> bool -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> error (list elf64_dyn)*) let rec obtain_elf64_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc:((elf64_dyn)list)error= (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then return [] else read_elf64_dyn endian bs0 shared_object os_additional_ranges os proc >>= (fun (head, bs0) -> if Nat_big_num.equal (Nat_big_num.of_int64 head.elf64_dyn_tag) ( dt_null) then (* DT_NULL marks end of array *) return [head] else obtain_elf64_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc >>= (fun tail -> return (head::tail)))) (** [obtain_elf32_dynamic_section_contents' f1 os_additional_ranges os * proc bs0] exhaustively reads in [elf32_dyn] values from byte sequence [bs0], * obtaining endianness and the section header table from [elf32_file] f1, * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and * [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an * [elf32_dyn] entry is not 0. *) (*val obtain_elf32_dynamic_section_contents : elf32_file -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> byte_sequence -> error (list elf32_dyn)*) let obtain_elf32_dynamic_section_contents f1 os_additional_ranges os proc bs0:((elf32_dyn)list)error= (let endian = (get_elf32_header_endianness f1.elf32_file_header) in let sht = (f1.elf32_file_section_header_table) in let shared_object = (is_elf32_shared_object_file f1.elf32_file_header) in (match List.filter (fun ent -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) sht_dynamic) sht with | [] -> fail "obtain_elf32_dynamic_section_contents: no SHT_DYNAMIC section header entries" | [dyn] -> let off = (Nat_big_num.of_string (Uint32.to_string dyn.elf32_sh_offset)) in let siz = (Nat_big_num.of_string (Uint32.to_string dyn.elf32_sh_size)) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> obtain_elf32_dynamic_section_contents' endian rel shared_object os_additional_ranges os proc) | _ -> fail "obtain_elf32_dynamic_section_contents: multiple SHT_DYNAMIC section header entries" )) (** [obtain_elf64_dynamic_section_contents' f1 os_additional_ranges os * proc bs0] exhaustively reads in [elf64_dyn] values from byte sequence [bs0], * obtaining endianness and the section header table from [elf64_file] f1, * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and * [proc] as mentioned above. Fails if [bs0]'s length modulo the size of an * [elf64_dyn] entry is not 0. *) (*val obtain_elf64_dynamic_section_contents : elf64_file -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> byte_sequence -> error (list elf64_dyn)*) let obtain_elf64_dynamic_section_contents f1 os_additional_ranges os proc bs0:((elf64_dyn)list)error= (let endian = (get_elf64_header_endianness f1.elf64_file_header) in let sht = (f1.elf64_file_section_header_table) in let shared_object = (is_elf64_shared_object_file f1.elf64_file_header) in (match List.filter (fun ent -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) sht_dynamic) sht with | [] -> fail "obtain_elf64_dynamic_section_contents: no SHT_DYNAMIC section header entries" | [dyn] -> let off = (Nat_big_num.of_string (Uint64.to_string dyn.elf64_sh_offset)) in let siz = (Ml_bindings.nat_big_num_of_uint64 dyn.elf64_sh_size) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> obtain_elf64_dynamic_section_contents' endian rel shared_object os_additional_ranges os proc) | _ -> fail "obtain_elf64_dynamic_section_contents: multiple SHT_DYNAMIC section header entries" )) (** DT Flags values *) (** [df_origin] specific that the object being loaded may make reference to the * $(ORIGIN) substitution string. *) let df_origin : Nat_big_num.num= (Nat_big_num.of_int 1) (* 0x1 *) (** [df_symbolic] changes the linker's symbol resolution algorithm, resolving * symbols first from the shared object file rather than the executable file. *) let df_symbolic : Nat_big_num.num= (Nat_big_num.of_int 2) (* 0x2 *) (** [df_textrel] if this flag is not set then no relocation entry should cause * modification to a non-writable segment. *) let df_textrel : Nat_big_num.num= (Nat_big_num.of_int 4) (* 0x4 *) (** [df_bindnow] if set this instructs the linker to process all relocation entries * of the containing object before transferring control to the program. *) let df_bindnow : Nat_big_num.num= (Nat_big_num.of_int 8) (* 0x8 *) (** [df_static_tls] if set instructs the linker to reject all attempts to load * the containing file dynamically. *) let df_static_tls : Nat_big_num.num= (Nat_big_num.of_int 16) (* 0x10 *) (** [check_flag] is a utility function for testing whether a flag is set. * TODO: so simple it is probably unneccessary now. *) (*val check_flag : natural -> natural -> bool*) let check_flag m pos:bool= ( Nat_big_num.equal m pos) (** [string_of_dt_flag f] produces a string-based representation of dynamic * section flag [f]. *) (*val string_of_dt_flag : natural -> string*) let string_of_dt_flag flag:string= (if check_flag flag(Nat_big_num.of_int 0) then "None" else if check_flag flag df_origin then "ORIGIN" else if check_flag flag df_bindnow then "BIND_NOW" else if check_flag flag df_symbolic then "SYMBOLIC" else if check_flag flag df_textrel then "TEXTREL" else if check_flag flag df_static_tls then "STATIC_TLS" else if check_flag flag ( Nat_big_num.add df_bindnow df_static_tls) then "BIND_NOW STATIC_TLS" else if check_flag flag ( Nat_big_num.add df_static_tls df_symbolic) then "SYMBOLIC STATIC_TLS" else (* XXX: add more as needed *) "Invalid dynamic section flag") (** [rel_type] represents the two types of relocation records potentially present * in an ELF file: relocation, and relocation with addends. *) type rel_type = Rel (** Plain relocation type. *) | RelA (** Relocation with addends type. *) (** [string_of_rel_type r] produces a string-based representation of [rel_type], * [r]. *) (*val string_of_rel_type : rel_type -> string*) let string_of_rel_type r:string= ((match r with | Rel -> "REL" | RelA -> "RELA" )) (** Type [dyn_value] represents the value of an ELF dynamic section entry. Values * can represent various different types of objects (e.g. paths to libraries, or * flags, or sizes of other entries in a file), and this type collates them all. * Parameterised over two type variables so the type can be shared between ELF32 * and ELF64. *) type( 'addr, 'size) dyn_value = Address of 'addr (** An address. *) | Size of 'size (** A size (in bytes). *) | FName of string (** A filename. *) | SOName of string (** A shared object name. *) | Path of string (** A path to some directory. *) | RPath of string (** A "run path". *) | RunPath of string (** A "run path". *) | Library of string (** A library path. *) | Flags1 of Nat_big_num.num (** Flags. *) | Flags of Nat_big_num.num (** Flags. *) | Numeric of Nat_big_num.num (** An uninterpreted numeric value. *) | Checksum of Nat_big_num.num (** A checksum value *) | RelType of rel_type (** A relocation entry type. *) | Timestamp of Nat_big_num.num (** A timestamp value. *) | Null (** A null (0) value. *) | Ignored (** An ignored value. *) (** [elf32_dyn_value] and [elf64_dyn_value] are specialisations of [dyn_value] * fixing the correct types for the ['addr] and ['size] type variables. *) type elf32_dyn_value = (Uint32.uint32, Uint32.uint32) dyn_value type elf64_dyn_value = (Uint64.uint64, Uint64.uint64) dyn_value (** [get_string_table_of_elf32_dyn_section endian dyns sht bs0] searches through * dynamic section entries [dyns] looking for one pointing to a string table, looks * up the corresponding section header [sht] pointed to by that dynamic * section entry, finds the section in [bs0] and decodes a string table from that * section assuming endianness [endian]. May fail. *) (*val get_string_table_of_elf32_dyn_section : endianness -> list elf32_dyn -> elf32_section_header_table -> byte_sequence -> error string_table*) let get_string_table_of_elf32_dyn_section endian dyns sht bs0:(string_table)error= (let strtabs = (List.filter (fun x -> Nat_big_num.equal (Nat_big_num.of_int32 x.elf32_dyn_tag) ( dt_strtab) ) dyns) in (match strtabs with | [strtab] -> (match strtab.elf32_dyn_d_un with | D_Val v -> fail "get_string_table_of_elf32_dyn_section: STRTAB must be a PTR" | D_Ptr p -> let sect = (List.filter (fun s -> (s.elf32_sh_addr = p) && (s.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_strtab)) ) sht) in (match sect with | [] -> fail "get_string_table_of_elf32_dyn_section: no section entry with same address as STRTAB" | [s] -> let off = (Nat_big_num.of_string (Uint32.to_string s.elf32_sh_offset)) in let siz = (Nat_big_num.of_string (Uint32.to_string s.elf32_sh_size)) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> let strings = (Byte_sequence.string_of_byte_sequence rel) in return (String_table.mk_string_table strings (Missing_pervasives.null_char))) | _ -> fail "get_string_table_of_elf32_dyn_section: multiple section entries with same address as STRTAB" ) | D_Ignored i -> fail "get_string_table_of_elf32_dyn_section: STRTAB must be a PTR" ) | [] -> fail "get_string_table_of_elf32_dyn_section: no string table entry" | _ -> fail "get_string_table_of_elf32_dyn_section: multiple string table entries" )) (** [get_string_table_of_elf64_dyn_section endian dyns sht bs0] searches through * dynamic section entries [dyns] looking for one pointing to a string table, looks * up the corresponding section header [sht] pointed to by that dynamic * section entry, finds the section in [bs0] and decodes a string table from that * section assuming endianness [endian]. May fail. *) (*val get_string_table_of_elf64_dyn_section : endianness -> list elf64_dyn -> elf64_section_header_table -> byte_sequence -> error string_table*) let get_string_table_of_elf64_dyn_section endian dyns sht bs0:(string_table)error= (let strtabs = (List.filter (fun x -> Nat_big_num.equal (Nat_big_num.of_int64 x.elf64_dyn_tag) ( dt_strtab) ) dyns) in (match strtabs with | [strtab] -> (match strtab.elf64_dyn_d_un with | D_Val v -> fail "get_string_table_of_elf64_dyn_section: STRTAB must be a PTR" | D_Ptr p -> let sect = (List.filter (fun s -> (s.elf64_sh_addr = p) && (s.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_strtab)) ) sht) in (match sect with | [] -> fail "get_string_table_of_elf64_dyn_section: no section entry with same address as STRTAB" | [s] -> let off = (Nat_big_num.of_string (Uint64.to_string s.elf64_sh_offset)) in let siz = (Ml_bindings.nat_big_num_of_uint64 s.elf64_sh_size) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> let strings = (Byte_sequence.string_of_byte_sequence rel) in return (String_table.mk_string_table strings Missing_pervasives.null_char)) | _ -> fail "get_string_table_of_elf64_dyn_section: multiple section entries with same address as STRTAB" ) | D_Ignored i -> fail "get_string_table_of_elf64_dyn_section: STRTAB must be a PTR" ) | [] -> fail "get_string_table_of_elf64_dyn_section: no string table entry" | _ -> fail "get_string_table_of_elf64_dyn_section: multiple string table entries" )) (** [get_value_of_elf32_dyn so dyn os_additional_ranges os proc stab] returns the value * stored in a dynamic section entry [dyn], using [os_additional_ranges] and * [os] to decode ABI-reserved tags. String table [stab] is used to correctly * decode library and run paths, etc. * May fail. *) (*val get_value_of_elf32_dyn : bool -> elf32_dyn -> (natural -> bool) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> string_table -> error elf32_dyn_value*) let get_value_of_elf32_dyn shared_object dyn os_additional_ranges os proc stab:(((Uint32.uint32),(Uint32.uint32))dyn_value)error= (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in if Nat_big_num.equal tag dt_null then return Null else if Nat_big_num.equal tag dt_needed then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: NEEDED must be a Val" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: NEEDED must be a Val" ) >>= (fun off -> let off = (Nat_big_num.of_string (Uint32.to_string off)) in String_table.get_string_at off stab >>= (fun str -> return (Library str))) else if Nat_big_num.equal tag dt_pltrelsz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: PLTRELSZ must be a Val" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTRELSZ must be a Val" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_pltgot then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: PLTGOT must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTGOT must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_hash then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: HASH must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: HASH must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_strtab then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: STRTAB must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: STRTAB must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_symtab then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: SYMTAB must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SYMTAB must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_rela then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: RELA must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELA must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_relasz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELASZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELASZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_relaent then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELAENT must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELAENT must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_strsz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: STRSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: STRSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_syment then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: SYMENT must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SYMENT must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_init then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: INIT must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_fini then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: FINI must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_soname then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: SONAME must be a Val" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SONAME must be a Val" ) >>= (fun off -> let off = (Nat_big_num.of_string (Uint32.to_string off)) in String_table.get_string_at off stab >>= (fun str -> return (SOName str))) else if Nat_big_num.equal tag dt_rpath then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RPATH must be a Val" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RPATH must be a Val" ) >>= (fun off -> let off = (Nat_big_num.of_string (Uint32.to_string off)) in String_table.get_string_at off stab >>= (fun str -> return (RPath str))) else if Nat_big_num.equal tag dt_symbolic then return Null else if Nat_big_num.equal tag dt_rel then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: REL must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: REL must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_relsz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_relent then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RELENT must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELENT must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_pltrel then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: PLTREL must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTREL must be a VAL" ) >>= (fun r -> if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string r)) dt_rel then return (RelType Rel) else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string r)) dt_rela then return (RelType RelA) else fail "get_value_of_elf32_dyn_entry: PLTREL neither REL nor RELA") else if Nat_big_num.equal tag dt_debug then return Null else if Nat_big_num.equal tag dt_textrel then return Null else if Nat_big_num.equal tag dt_jmprel then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: JMPREL must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: JMPREL must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_bindnow then return Ignored else if Nat_big_num.equal tag dt_init_array then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAY must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAY must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_fini_array then (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAY must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAY must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_init_arraysz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAYSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAYSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_fini_arraysz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAYSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAYSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_runpath then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: RUNPATH must be a Val" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RUNPATH must be a Val" ) >>= (fun off -> let off = (Nat_big_num.of_string (Uint32.to_string off)) in String_table.get_string_at off stab >>= (fun str -> return (RunPath str))) else if Nat_big_num.equal tag dt_flags then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: FLAGS must be a Val" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FLAGS must be a Val" ) >>= (fun flags -> return (Flags (Nat_big_num.of_string (Uint32.to_string flags)))) else if Nat_big_num.equal tag dt_encoding then if not shared_object then return Ignored else (match dyn.elf32_dyn_d_un with | D_Val v -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAY must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAY must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_preinit_arraysz then (match dyn.elf32_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAYSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAYSZ must be a VAL" ) >>= (fun sz -> return (Checksum (Nat_big_num.of_string (Uint32.to_string sz)))) (** XXX: bug in readelf does not print this as a size! *) else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then proc dyn stab else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then os dyn stab else if os_additional_ranges tag then os dyn stab else fail "get_value_of_elf32_dyn: unrecognised tag type") (** [get_value_of_elf64_dyn dyn os_additional_ranges os proc stab] returns the value * stored in a dynamic section entry [dyn], using [os_additional_ranges] and * [os] to decode ABI-reserved tags. String table [stab] is used to correctly * decode library and run paths, etc. * May fail. *) (*val get_value_of_elf64_dyn : bool -> elf64_dyn -> (natural -> bool) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> string_table -> error elf64_dyn_value*) let get_value_of_elf64_dyn shared_object dyn os_additional_ranges os_dyn proc_dyn stab:(((Uint64.uint64),(Uint64.uint64))dyn_value)error= (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in if Nat_big_num.equal tag dt_null then return Null else if Nat_big_num.equal tag dt_needed then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: NEEDED must be a Val" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: NEEDED must be a Val" ) >>= (fun off -> let off = (Ml_bindings.nat_big_num_of_uint64 off) in String_table.get_string_at off stab >>= (fun str -> return (Library str))) else if Nat_big_num.equal tag dt_pltrelsz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: PLTRELSZ must be a Val" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTRELSZ must be a Val" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_pltgot then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: PLTGOT must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTGOT must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_hash then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: HASH must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: HASH must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_strtab then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: STRTAB must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: STRTAB must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_symtab then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: SYMTAB must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SYMTAB must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_rela then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: RELA must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELA must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_relasz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELASZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELASZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_relaent then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELAENT must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELAENT must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_strsz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: STRSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: STRSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_syment then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: SYMENT must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SYMENT must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_init then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: INIT must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_fini then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: FINI must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_soname then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: SONAME must be a Val" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SONAME must be a Val" ) >>= (fun off -> let off = (Ml_bindings.nat_big_num_of_uint64 off) in String_table.get_string_at off stab >>= (fun str -> return (SOName str))) else if Nat_big_num.equal tag dt_rpath then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RPATH must be a Val" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RPATH must be a Val" ) >>= (fun off -> let off = (Ml_bindings.nat_big_num_of_uint64 off) in String_table.get_string_at off stab >>= (fun str -> return (RPath str))) else if Nat_big_num.equal tag dt_symbolic then return Null else if Nat_big_num.equal tag dt_rel then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: REL must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: REL must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_relsz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_relent then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RELENT must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELENT must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_pltrel then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: PLTREL must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTREL must be a VAL" ) >>= (fun r -> if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 r) dt_rel then return (RelType Rel) else if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 r) dt_rela then return (RelType RelA) else fail "get_value_of_elf64_dyn_entry: PLTREL neither REL nor RELA") else if Nat_big_num.equal tag dt_debug then return Null else if Nat_big_num.equal tag dt_textrel then return Null else if Nat_big_num.equal tag dt_jmprel then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: JMPREL must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: JMPREL must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_bindnow then return Ignored else if Nat_big_num.equal tag dt_init_array then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAY must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAY must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_fini_array then (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAY must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAY must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_init_arraysz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAYSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAYSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_fini_arraysz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAYSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAYSZ must be a VAL" ) >>= (fun sz -> return (Size sz)) else if Nat_big_num.equal tag dt_runpath then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: RUNPATH must be a Val" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RUNPATH must be a Val" ) >>= (fun off -> let off = (Ml_bindings.nat_big_num_of_uint64 off) in String_table.get_string_at off stab >>= (fun str -> return (RunPath str))) else if Nat_big_num.equal tag dt_flags then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: FLAGS must be a Val" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FLAGS must be a Val" ) >>= (fun flags -> return (Flags (Ml_bindings.nat_big_num_of_uint64 flags))) else if Nat_big_num.equal tag dt_encoding then if not shared_object then return Ignored else (match dyn.elf64_dyn_d_un with | D_Val v -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAY must be a PTR" | D_Ptr p -> return p | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAY must be a PTR" ) >>= (fun ptr -> return (Address ptr)) else if Nat_big_num.equal tag dt_preinit_arraysz then (match dyn.elf64_dyn_d_un with | D_Val v -> return v | D_Ptr p -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAYSZ must be a VAL" | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAYSZ must be a VAL" ) >>= (fun sz -> return (Checksum (Ml_bindings.nat_big_num_of_uint64 sz))) (** XXX: bug in readelf does not print this as a size! *) else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then proc_dyn dyn stab else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then os_dyn dyn stab else if os_additional_ranges tag then os_dyn dyn stab else fail "get_value_of_elf64_dyn: unrecognised tag type")