Source file gnu_ext_dynamic.ml

(*Generated by Lem from gnu_extensions/gnu_ext_dynamic.lem.*)
(** [gnu_ext_dynamic] contains GNU extension specific definitions related to the
  * .dynamic section of an ELF file.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_num
open Lem_string

open Error
open Show
open String_table

open Elf_dynamic
open Elf_types_native_uint

(** Additional dynamic entries, see LSB section 11.3.2.2.
  * All values taken from elf.c from binutils and GLIBC as the LSB does not
  * specify them.
  *
  *  98 #define OLD_DT_LOOS     0x60000000
  *  99 #define DT_LOOS         0x6000000d
  * 100 #define DT_HIOS         0x6ffff000
  * 101 #define DT_VALRNGLO     0x6ffffd00
  * 102 #define DT_VALRNGHI     0x6ffffdff
  * 103 #define DT_ADDRRNGLO    0x6ffffe00
  * 104 #define DT_ADDRRNGHI    0x6ffffeff
  * 105 #define DT_VERSYM       0x6ffffff0
  * 106 #define DT_RELACOUNT    0x6ffffff9
  * 107 #define DT_RELCOUNT     0x6ffffffa
  * 108 #define DT_FLAGS_1      0x6ffffffb
  * 109 #define DT_VERDEF       0x6ffffffc
  * 110 #define DT_VERDEFNUM    0x6ffffffd
  * 111 #define DT_VERNEED      0x6ffffffe
  * 112 #define DT_VERNEEDNUM   0x6fffffff
  * 113 #define OLD_DT_HIOS     0x6fffffff
  * 114 #define DT_LOPROC       0x70000000
  * 115 #define DT_HIPROC       0x7fffffff
  *)

let elf_dt_gnu_addrrnghi  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939523967))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1)))  (*0x6ffffeff*)
let elf_dt_gnu_addrrnglo  : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 939523840))( (Nat_big_num.of_int 2)))        (*0x6ffffe00*)
let elf_dt_gnu_auxiliary  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 1073741822))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x7ffffffd*)
let elf_dt_gnu_filter     : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 1073741823))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x7fffffff*)
(** The following is "specified" in the LSB document but is not present in the
  * elf.c file so taken from elf.h from GLIBC:
  *)
let elf_dt_gnu_num        : Nat_big_num.num= ( (Nat_big_num.of_int 32)) (** ??? This should match something *)
let elf_dt_gnu_posflag_1  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939523838))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffdfd*)
let elf_dt_gnu_relcount   : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 939524093))( (Nat_big_num.of_int 2)))       (*0x6ffffffa*)
let elf_dt_gnu_relacount  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939524092))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6FFFFFF9*)
let elf_dt_gnu_syminent   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939523839))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffdff*)
let elf_dt_gnu_syminfo    : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939523967))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffeff*)
let elf_dt_gnu_syminsz    : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 939523839))( (Nat_big_num.of_int 2)))       (*0x6ffffdfe*)
let elf_dt_gnu_valrnghi   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939523839))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffdff*)
let elf_dt_gnu_valrnglo   : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 939523712))( (Nat_big_num.of_int 2)))     (*0x6ffffd00*)
let elf_dt_gnu_verdef     : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 939524094))( (Nat_big_num.of_int 2)))       (*0x6ffffffc*)
let elf_dt_gnu_verdefnum  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939524094))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffffd*)
let elf_dt_gnu_verneed    : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 939524095))( (Nat_big_num.of_int 2)))       (*0x6ffffffe*)
let elf_dt_gnu_verneednum : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939524095))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6fffffff*)
let elf_dt_gnu_versym     : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 939524088))( (Nat_big_num.of_int 2)))       (*0x6ffffff0*)

(** Not present in the LSB but turns up in "real" ELF files... *)

let elf_dt_gnu_hash      : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939523962))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffef5*)
let elf_dt_gnu_flags_1   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939524093))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (*0x6ffffffb*)
let elf_dt_gnu_checksum  : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 939523836))( (Nat_big_num.of_int 2)))     (* 0x6FFFFDF8 *)
let elf_dt_gnu_prelinked : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939523834)))( (Nat_big_num.of_int 1))) (* 0x6FFFFDF5 *)

(** Extended DT flags for FLAGS_1 dynamic section types.  Taken from GLibC source
  * as they appear to be completely unspecified!
  *)
  
let gnu_df_1_now        : Nat_big_num.num= ( (Nat_big_num.of_int 1))     (*0x00000001*)
let gnu_df_1_global     : Nat_big_num.num= ( (Nat_big_num.of_int 2))     (*0x00000002*)
let gnu_df_1_group      : Nat_big_num.num= ( (Nat_big_num.of_int 4))     (*0x00000004*)
let gnu_df_1_nodelete   : Nat_big_num.num= ( (Nat_big_num.of_int 8))     (*0x00000008*)
let gnu_df_1_loadfltr   : Nat_big_num.num= ( (Nat_big_num.of_int 16))    (*0x00000010*)
let gnu_df_1_initfirst  : Nat_big_num.num= ( (Nat_big_num.of_int 32))    (*0x00000020*)
let gnu_df_1_noopen     : Nat_big_num.num= ( (Nat_big_num.of_int 64))    (*0x00000040*)
let gnu_df_1_origin     : Nat_big_num.num= ( (Nat_big_num.of_int 128))   (*0x00000080*)
let gnu_df_1_direct     : Nat_big_num.num= ( (Nat_big_num.of_int 256))   (*0x00000100*)
let gnu_df_1_trans      : Nat_big_num.num= ( (Nat_big_num.of_int 512))   (*0x00000200*)
let gnu_df_1_interpose  : Nat_big_num.num= ( (Nat_big_num.of_int 1024))  (*0x00000400*)
let gnu_df_1_nodeflib   : Nat_big_num.num= ( (Nat_big_num.of_int 2048))  (*0x00000800*)
let gnu_df_1_nodump     : Nat_big_num.num= ( (Nat_big_num.of_int 4096))  (*0x00001000*)
let gnu_df_1_confalt    : Nat_big_num.num= ( (Nat_big_num.of_int 8192))  (*0x00002000*)
let gnu_df_1_endfiltee  : Nat_big_num.num= ( (Nat_big_num.of_int 16384)) (*0x00004000*)
let gnu_df_1_dispreldne : Nat_big_num.num= ( (Nat_big_num.of_int 32768)) (*0x00008000*)
let gnu_df_1_disprelpnd : Nat_big_num.num= ( (Nat_big_num.of_int 65536)) (*0x00010000*)

(** [gnu_string_of_dt_flag1 m] produces a string based representation of GNU
  * extensions flag_1 value [m].
  *)
(*val gnu_string_of_dt_flag_1 : natural -> string*)
let gnu_string_of_dt_flag_1 flag:string=
   (if check_flag flag( (Nat_big_num.of_int 0)) then
    "None"
  else if check_flag flag gnu_df_1_now then
    "NOW"
  else if check_flag flag gnu_df_1_global then
    "GLOBAL"
  else if check_flag flag gnu_df_1_group then
    "GROUP"
  else if check_flag flag gnu_df_1_nodelete then
    "NODELETE"
  else if check_flag flag gnu_df_1_loadfltr then
    "LOADFLTR"
  else if check_flag flag gnu_df_1_initfirst then
    "INITFIRST"
  else if check_flag flag gnu_df_1_noopen then
    "NOOPEN"
  else if check_flag flag gnu_df_1_origin then
    "ORIGIN"
  else if check_flag flag gnu_df_1_direct then
    "DIRECT"
  else if check_flag flag gnu_df_1_trans then
    "TRANS"
  else if check_flag flag gnu_df_1_interpose then
    "INTERPOSE"
  else if check_flag flag gnu_df_1_nodeflib then
    "NODEFLIB"
  else if check_flag flag gnu_df_1_nodump then
    "NODUMP"
  else if check_flag flag gnu_df_1_confalt then
    "CONFALT"
  else if check_flag flag gnu_df_1_endfiltee then
    "ENDFILTEE"
  else if check_flag flag gnu_df_1_dispreldne then
    "DISPRELDNE"
  else if check_flag flag gnu_df_1_disprelpnd then
    "DISPRELPND"
  else if check_flag flag ( Nat_big_num.add gnu_df_1_nodelete gnu_df_1_now) then
    "NOW NODELETE"
  else if check_flag flag ( Nat_big_num.add gnu_df_1_nodelete gnu_df_1_initfirst) then
    "NODELETE INITFIRST"
  else (* XXX: add more as necessary *)
    "Invalid GNU dynamic flag")

(** [gnu_ext_os_additional_ranges m] checks whether dynamic section type [m]
  * lies within the ranges set aside for GNU specific functionality.
  * NB: quite ad hoc as this is not properly specified anywhere.
  *)
(*val gnu_ext_os_additional_ranges : natural -> bool*)
let gnu_ext_os_additional_ranges m:bool=
   (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then
    true
  else Nat_big_num.equal (* ad hoc extensions go here... *)
    m elf_dt_gnu_verneed || (Nat_big_num.equal
    m elf_dt_gnu_verneednum || (Nat_big_num.equal
    m elf_dt_gnu_versym || (Nat_big_num.equal
    m elf_dt_gnu_verdef || (Nat_big_num.equal
    m elf_dt_gnu_verdefnum || (Nat_big_num.equal
    m elf_dt_gnu_flags_1 || (Nat_big_num.equal
    m elf_dt_gnu_relcount || (Nat_big_num.equal
    m elf_dt_gnu_relacount || (Nat_big_num.equal
    m elf_dt_gnu_checksum || Nat_big_num.equal
    m elf_dt_gnu_prelinked)))))))))

(** [gnu_ext_tag_correspondence_of_tag0 m] produces a tag correspondence for the
  * extended GNU-specific dynamic section types [m].  Used to provide the ABI
  * specific functionality expected of the corresponding function in the elf_dynamic
  * module.
  *)
(*val gnu_ext_tag_correspondence_of_tag0 : natural -> error tag_correspondence*)
let gnu_ext_tag_correspondence_of_tag0 m:(tag_correspondence)error=
   (if Nat_big_num.equal m elf_dt_gnu_hash then
    return C_Ptr
  else if Nat_big_num.equal m elf_dt_gnu_flags_1 then
    return C_Val
  else if Nat_big_num.equal m elf_dt_gnu_versym then
    return C_Ptr
  else if Nat_big_num.equal m elf_dt_gnu_verneednum then
    return C_Val
  else if Nat_big_num.equal m elf_dt_gnu_verneed then
    return C_Ptr
  else if Nat_big_num.equal m elf_dt_gnu_verdef then
    return C_Ptr
  else if Nat_big_num.equal m elf_dt_gnu_verdefnum then
    return C_Val
  else if Nat_big_num.equal m elf_dt_gnu_relcount then
    return C_Val
  else if Nat_big_num.equal m elf_dt_gnu_relacount then
    return C_Val
  else if Nat_big_num.equal m elf_dt_gnu_checksum then
    return C_Val
  else if Nat_big_num.equal m elf_dt_gnu_prelinked then
    return C_Val
  else
    fail "gnu_ext_tag_correspondence_of_tag0: invalid dynamic tag")

(** [gnu_ext_tag_correspondence_of_tag m] produces a tag correspondence for the
  * extended GNU-specific dynamic section types [m].  Used to provide the ABI
  * specific functionality expected of the corresponding function in the elf_dynamic
  * module.
  * TODO: examine whether this and the function above really need separating into
  * two functions.
  *)
(*val gnu_ext_tag_correspondence_of_tag : natural -> error tag_correspondence*)
let gnu_ext_tag_correspondence_of_tag m:(tag_correspondence)error=
   (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then
    return C_Ptr
  else if Nat_big_num.greater_equal m elf_dt_gnu_valrnglo && Nat_big_num.less_equal m elf_dt_gnu_valrnghi then
    return C_Val
  else if gnu_ext_os_additional_ranges m then
    gnu_ext_tag_correspondence_of_tag0 m
  else if Nat_big_num.equal m elf_dt_gnu_syminsz then
    return C_Val (** unsure *)
  else if Nat_big_num.equal m elf_dt_gnu_syminfo then
    return C_Ptr (** unsure *)
  else if Nat_big_num.equal m elf_dt_gnu_syminent then
    return C_Val (** unsure *)
  else if Nat_big_num.equal m elf_dt_gnu_posflag_1 then
    return C_Val (** unsure *)
  else if Nat_big_num.equal m elf_dt_gnu_num then
    return C_Ignored
  else if Nat_big_num.equal m elf_dt_gnu_filter then
    return C_Val (** unsure *)
  else if Nat_big_num.equal m elf_dt_gnu_auxiliary then
    return C_Val (** unsure *)
  else
    fail ("gnu_ext_tag_correspondence_of_tag: unrecognised GNU dynamic tag"))
    
(** [gnu_ext_elf32_value_of_elf32_dyn0 dyn] extracts a dynamic value from the
  * dynamic section entry [dyn] under the assumption that its type is a GNU
  * extended dynamic section type.  Fails otherwise.  Used to provide the
  * ABI-specific functionality expected of the corresponding functions in
  * elf_dynamic.lem.
  *)
(*val gnu_ext_elf32_value_of_elf32_dyn0 : elf32_dyn -> string_table -> error elf32_dyn_value*)
let gnu_ext_elf32_value_of_elf32_dyn0 dyn stbl:(((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 elf_dt_gnu_hash then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_HASH must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_HASH must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_flags_1 then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: FLAGS_1 must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: FlAGS_1 must be a Val"
      ) (fun f ->
      return (Flags1 (Uint32_wrapper.to_bigint f)))
    else if Nat_big_num.equal tag elf_dt_gnu_versym then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERSYM must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERSYM must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_verdef then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEF must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEF must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_verdefnum then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEFNUM must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERDEFNUM must be a Val"
      ) (fun sz ->
      return (Numeric (Uint32_wrapper.to_bigint sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_verneednum then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEEDNUM must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEEDNUM must be a Val"
      ) (fun sz ->
      return (Numeric (Uint32_wrapper.to_bigint sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_verneed then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEED must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: VERNEED must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_relcount then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELCOUNT must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELCOUNT must be a Val"
      ) (fun sz ->
      return (Numeric (Uint32_wrapper.to_bigint sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_relacount then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELACOUNT must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: RELACOUNT must be a Val"
      ) (fun sz ->
      return (Numeric (Uint32_wrapper.to_bigint sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_checksum then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: CHECKSUM must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: CHECKSUM must be a Val"
      ) (fun sz ->
      return (Checksum (Uint32_wrapper.to_bigint sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_prelinked then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_PRELINKED must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: GNU_PRELINKED must be a Val"
      ) (fun off ->
      return (Timestamp (Uint32_wrapper.to_bigint off)))
    else
      fail "gnu_ext_elf32_value_of_elf32_dyn0: unrecognised GNU dynamic tag")
      
(** [gnu_ext_elf64_value_of_elf64_dyn0 dyn] extracts a dynamic value from the
  * dynamic section entry [dyn] under the assumption that its type is a GNU
  * extended dynamic section type.  Fails otherwise.  Used to provide the
  * ABI-specific functionality expected of the corresponding functions in
  * elf_dynamic.lem.
  *)
(*val gnu_ext_elf64_value_of_elf64_dyn0 : elf64_dyn -> string_table -> error elf64_dyn_value*)
let gnu_ext_elf64_value_of_elf64_dyn0 dyn stbl:(((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 elf_dt_gnu_hash then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_HASH must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_HASH must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_flags_1 then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: FLAGS_1 must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: FlAGS_1 must be a Val"
      ) (fun f ->
      return (Flags1 (Ml_bindings.nat_big_num_of_uint64 f)))
    else if Nat_big_num.equal tag elf_dt_gnu_versym then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERSYM must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERSYM must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_verdef then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERDEF must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERDEF must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_verdefnum then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf64_dyn: VERDEFNUM must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf64_dyn: VERDEFNUM must be a Val"
      ) (fun sz ->
      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_verneednum then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEEDNUM must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEEDNUM must be a Val"
      ) (fun sz ->
      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_verneed then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEED must be a PTR"
        | D_Ptr     p -> return p
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: VERNEED must be a PTR"
      ) (fun addr ->
      return (Address addr))
    else if Nat_big_num.equal tag elf_dt_gnu_relcount then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELCOUNT must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELCOUNT must be a Val"
      ) (fun sz ->
      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_relacount then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELACOUNT must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: RELACOUNT must be a Val"
      ) (fun sz ->
      return (Numeric (Ml_bindings.nat_big_num_of_uint64 sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_checksum then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: CHECKSUM must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: CHECKSUM must be a Val"
      ) (fun sz ->
      return (Checksum (Ml_bindings.nat_big_num_of_uint64 sz)))
    else if Nat_big_num.equal tag elf_dt_gnu_prelinked then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_PRELINKED must be a Val"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: GNU_PRELINKED must be a Val"
      ) (fun off ->
      return (Timestamp (Ml_bindings.nat_big_num_of_uint64 off)))
    else
      fail "gnu_ext_elf64_value_of_elf64_dyn0: unrecognised GNU dynamic tag")
      
(** [gnu_ext_elf32_value_of_elf32_dyn dyn] extracts a dynamic value from the
  * dynamic section entry [dyn] under the assumption that its type is a GNU
  * extended dynamic section type.  Fails otherwise.  Used to provide the
  * ABI-specific functionality expected of the corresponding functions in
  * elf_dynamic.lem.
  * TODO: some of these cases are missing as they have never come up in "real"
  * ELF files that have been processed as part of validation.  Try and find some
  * files that do actually exhibit these.
  *)
(*val gnu_ext_elf32_value_of_elf32_dyn : elf32_dyn -> string_table -> error elf32_dyn_value*)
let gnu_ext_elf32_value_of_elf32_dyn dyn stbl:(elf32_dyn_value)error=
   (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in
    if gnu_ext_os_additional_ranges tag then (* this should cover valrngs and addrrngs *)
      gnu_ext_elf32_value_of_elf32_dyn0 dyn stbl
    else if Nat_big_num.equal tag elf_dt_gnu_syminsz then bind (match dyn.elf32_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf32_value_of_elf32_dyn: SYMINSZ must be a VAL"
        | D_Ignored i -> fail "gnu_ext_elf32_value_of_elf32_dyn: SYMINSZ must be a VAL"
      ) (fun sz ->
      return (Size sz))
    else if Nat_big_num.equal tag elf_dt_gnu_syminfo then
      fail "SYMINFO" (* XXX: never seen in 32-bit ELF *)
    else if Nat_big_num.equal tag elf_dt_gnu_syminent then
      fail "SYMINENT" (* XXX: never seen in 32-bit ELF *)
    else if Nat_big_num.equal tag elf_dt_gnu_posflag_1 then
      fail "POSFLAG_1" (* XXX: never seen in 32-bit ELF *)
    else if Nat_big_num.equal tag elf_dt_gnu_num then
      fail "NUM" (* XXX: never seen in 32-bit ELF *)
    else if Nat_big_num.equal tag elf_dt_gnu_filter then
      fail "FILTER" (* XXX: never seen in 32-bit ELF *)
    else if Nat_big_num.equal tag elf_dt_gnu_auxiliary then
      fail "AUXILIARY" (* XXX: never seen in 32-bit ELF *)
    else
      fail "gnu_ext_elf32_value_of_elf32_dyn: unrecognised GNU dynamic tag")
      
(** [gnu_ext_elf64_value_of_elf64_dyn dyn] extracts a dynamic value from the
  * dynamic section entry [dyn] under the assumption that its type is a GNU
  * extended dynamic section type.  Fails otherwise.  Used to provide the
  * ABI-specific functionality expected of the corresponding functions in
  * elf_dynamic.lem.
  * TODO: some of these cases are missing as they have never come up in "real"
  * ELF files that have been processed as part of validation.  Try and find some
  * files that do actually exhibit these.
  *)
(*val gnu_ext_elf64_value_of_elf64_dyn : elf64_dyn -> string_table -> error elf64_dyn_value*)
let gnu_ext_elf64_value_of_elf64_dyn dyn stbl:(elf64_dyn_value)error=
   (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
    if gnu_ext_os_additional_ranges tag then (* this should cover valrngs and addrrngs *)
      gnu_ext_elf64_value_of_elf64_dyn0 dyn stbl
    else if Nat_big_num.equal tag elf_dt_gnu_syminsz then bind (match dyn.elf64_dyn_d_un with
        | D_Val     v -> return v
        | D_Ptr     p -> fail "gnu_ext_elf64_value_of_elf64_dyn: SYMINSZ must be a VAL"
        | D_Ignored i -> fail "gnu_ext_elf64_value_of_elf64_dyn: SYMINSZ must be a VAL"
      ) (fun sz ->
      return (Size sz))
    else if Nat_big_num.equal tag elf_dt_gnu_syminfo then
      fail "SYMINFO" (* XXX: fill in as seen *)
    else if Nat_big_num.equal tag elf_dt_gnu_syminent then
      fail "SYMINENT" (* XXX: fill in as seen *)
    else if Nat_big_num.equal tag elf_dt_gnu_posflag_1 then
      fail "POSFLAG_1" (* XXX: fill in as seen *)
    else if Nat_big_num.equal tag elf_dt_gnu_num then
      fail "NUM" (* XXX: fill in as seen *)
    else if Nat_big_num.equal tag elf_dt_gnu_filter then
      fail "FILTER" (* XXX: fill in as seen *)
    else if Nat_big_num.equal tag elf_dt_gnu_auxiliary then
      fail "AUXILIARY" (* XXX: fill in as seen *)
    else
      fail "gnu_ext_elf64_value_of_elf64_dyn: unrecognised GNU dynamic tag")
    
(** [string_of_gnu_ext_dynamic_tag0 m] produces a string based representation of
  * GNU extensions dynamic tag value [m].
  *)
(*val string_of_gnu_ext_dynamic_tag0 : natural -> string*)
let string_of_gnu_ext_dynamic_tag0 m:string=
   (if Nat_big_num.equal m elf_dt_gnu_hash then
    "GNU_HASH"
  else if Nat_big_num.equal m elf_dt_gnu_flags_1 then
    "FLAGS_1"
  else if Nat_big_num.equal m elf_dt_gnu_versym then
    "VERSYM"
  else if Nat_big_num.equal m elf_dt_gnu_verneednum then
    "VERNEEDNUM"
  else if Nat_big_num.equal m elf_dt_gnu_verneed then
    "VERNEED"
  else if Nat_big_num.equal m elf_dt_gnu_relcount then
    "RELCOUNT"
  else if Nat_big_num.equal m elf_dt_gnu_relacount then
    "RELACOUNT"
  else if Nat_big_num.equal m elf_dt_gnu_verdefnum then
    "VERDEFNUM"
  else if Nat_big_num.equal m elf_dt_gnu_verdef then
    "VERDEF"
  else if Nat_big_num.equal m elf_dt_gnu_checksum then
    "CHECKSUM"
  else if Nat_big_num.equal m elf_dt_gnu_prelinked then
    "GNU_PRELINKED"
  else
    "Invalid dynamic tag")
    
(** [string_of_gnu_ext_dynamic_tag m] produces a string based representation of
  * GNU extensions dynamic tag value [m].
  *)
(*val string_of_gnu_ext_dynamic_tag : natural -> string*)
let string_of_gnu_ext_dynamic_tag m:string=
   (if Nat_big_num.greater_equal m elf_dt_gnu_addrrnglo && Nat_big_num.less_equal m elf_dt_gnu_addrrnghi then
    string_of_gnu_ext_dynamic_tag0 m
  else if Nat_big_num.greater_equal m elf_dt_gnu_valrnglo && Nat_big_num.less_equal m elf_dt_gnu_valrnghi then
    string_of_gnu_ext_dynamic_tag0 m
  else if gnu_ext_os_additional_ranges m then
    string_of_gnu_ext_dynamic_tag0 m
  else if Nat_big_num.equal m elf_dt_gnu_syminsz then
    "SYMINSZ"
  else if Nat_big_num.equal m elf_dt_gnu_syminfo then
    "SYMINFO"
  else if Nat_big_num.equal m elf_dt_gnu_syminent then
    "SYMINENT"
  else if Nat_big_num.equal m elf_dt_gnu_posflag_1 then
    "POSFLAG_1"
  else if Nat_big_num.equal m elf_dt_gnu_num then
    "NUM"
  else if Nat_big_num.equal m elf_dt_gnu_filter then
    "FILTER"
  else if Nat_big_num.equal m elf_dt_gnu_auxiliary then
    "AUXILIARY"
  else
    "Invalid dynamic tag")