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