Add ocaml run-time and updates to sail for ocaml backend

1 files changed, 1202 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/elf_dynamic.ml b/lib/ocaml_rts/linksem/elf_dynamic.ml
new file mode 100644
index 00000000..0355337e
--- /dev/null
+++ b/lib/ocaml_rts/linksem/elf_dynamic.ml
@@ -0,0 +1,1202 @@
+(*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")