Source file elf_dynamic.ml

(*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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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_sequence0
  
(** [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_wrapper.uint32, Uint32_wrapper.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_wrapper.uint64, Uint64_wrapper.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_wrapper.byte_sequence)error=  (bind (read_elf32_sword endian bs0) (fun (tag0, bs1) ->
  let tag = (Nat_big_num.abs (Nat_big_num.of_int32 tag0)) in bind (tag_correspondence_of_tag shared_object tag os_additional_ranges os proc) (fun corr ->
    (match corr with
      | C_Ptr -> bind (read_elf32_addr endian bs1) (fun (ptr, bs2) ->
        return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ptr ptr) }, bs2))
      | C_Val -> bind (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    -> bind (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 -> bind (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_wrapper.byte_sequence)error=  (bind (read_elf64_sxword endian bs0) (fun (tag0, bs1) ->
  let tag = (Nat_big_num.abs (Nat_big_num.of_int64 tag0)) in bind (tag_correspondence_of_tag shared_object tag os_additional_ranges os proc) (fun corr ->
    (match corr with
      | C_Ptr -> bind (read_elf64_addr endian bs1) (fun (ptr, bs2) ->
        return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ptr ptr) }, bs2))
      | C_Val -> bind (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    -> bind (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 -> bind (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 bind (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 bind (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 bind (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 bind (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 (Uint32_wrapper.to_bigint ent.elf32_sh_type) sht_dynamic) sht with
      | [] -> fail "obtain_elf32_dynamic_section_contents: no SHT_DYNAMIC section header entries"
      | [dyn] ->
        let off = (Uint32_wrapper.to_bigint dyn.elf32_sh_offset) in
        let siz = (Uint32_wrapper.to_bigint dyn.elf32_sh_size) in bind (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 (Uint32_wrapper.to_bigint ent.elf64_sh_type) sht_dynamic) sht with
      | [] -> fail "obtain_elf64_dynamic_section_contents: no SHT_DYNAMIC section header entries"
      | [dyn] ->
        let off = (Uint64_wrapper.to_bigint dyn.elf64_sh_offset) in
        let siz = (Ml_bindings.nat_big_num_of_uint64 dyn.elf64_sh_size) in bind (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_wrapper.uint32, Uint32_wrapper.uint32) dyn_value
type elf64_dyn_value = (Uint64_wrapper.uint64, Uint64_wrapper.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_wrapper.of_bigint 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 = (Uint32_wrapper.to_bigint  s.elf32_sh_offset) in
                  let siz = (Uint32_wrapper.to_bigint s.elf32_sh_size) in bind (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_wrapper.of_bigint 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 = (Uint64_wrapper.to_bigint  s.elf64_sh_offset) in
                  let siz = (Ml_bindings.nat_big_num_of_uint64 s.elf64_sh_size) in bind (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_wrapper.uint32),(Uint32_wrapper.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 bind (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 = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
        return (Library str)))
    else if Nat_big_num.equal tag dt_pltrelsz then bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
        return (SOName str)))
    else if Nat_big_num.equal tag dt_rpath then bind (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 = (Uint32_wrapper.to_bigint off) in bind (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 bind (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 bind (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 bind (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 bind (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 (Uint32_wrapper.to_bigint r) dt_rel then
          return (RelType Rel)
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint 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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 = (Uint32_wrapper.to_bigint off) in bind (String_table.get_string_at off stab) (fun str ->
        return (RunPath str)))
    else if Nat_big_num.equal tag dt_flags then bind (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 (Uint32_wrapper.to_bigint flags)))
    else if Nat_big_num.equal tag dt_encoding then
      if not shared_object then
        return Ignored
      else bind (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 bind (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 (Uint32_wrapper.to_bigint 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_wrapper.uint64),(Uint64_wrapper.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 bind (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 bind (String_table.get_string_at off stab) (fun str ->
        return (Library str)))
    else if Nat_big_num.equal tag dt_pltrelsz then bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (String_table.get_string_at off stab) (fun str ->
        return (SOName str)))
    else if Nat_big_num.equal tag dt_rpath then bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (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 bind (String_table.get_string_at off stab) (fun str ->
        return (RunPath str)))
    else if Nat_big_num.equal tag dt_flags then bind (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 bind (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 bind (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")