Source file gnu_ext_symbol_versioning.ml

(*Generated by Lem from gnu_extensions/gnu_ext_symbol_versioning.lem.*)
(** The [gnu_ext_symbol_versioning] defines constants, types and functions
  * relating to the GNU symbol versioning extensions (i.e. contents of
  * GNU_VERSYM sections).
  *
  * TODO: work out what is going on with symbol versioning.  The specification
  * is completely opaque.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string

open Byte_sequence
open Endianness
open Error

open Elf_dynamic
open Elf_file
open Elf_header
open Elf_interpreted_section
open Elf_section_header_table
open Elf_symbol_table
open Elf_types_native_uint

open Missing_pervasives
open Show

open Gnu_ext_dynamic
open Gnu_ext_section_header_table

(* Legal values for vd_version (version revision) *)
let gnu_ext_ver_def_none : Nat_big_num.num= ( (Nat_big_num.of_int 0)) (** No version *)
let gnu_ext_ver_def_current : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Current version *)

(* Legal values for vd_flags (version information flags) *)
let gnu_ext_ver_flg_base : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Version definition of file itself *)
let gnu_ext_ver_flg_weak : Nat_big_num.num= ( (Nat_big_num.of_int 2)) (** Weak version identifier *)

(* Versym symbol index values *)
let gnu_ext_ver_ndx_local : Nat_big_num.num= ( (Nat_big_num.of_int 0)) (** Symbol is local *)
let gnu_ext_ver_ndx_global : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Symbol is global *)
let gnu_ext_ver_ndx_loreserve : Nat_big_num.num=  (natural_of_hex "0xff00") (** Beginning of reserved entries *)
let gnu_ext_ver_ndx_eliminate : Nat_big_num.num=  (natural_of_hex "0xff00") (** Symbol is to be eliminated *)

(* Legal values for vn_version (version revision) *)
let gnu_ext_ver_need_none : Nat_big_num.num= ( (Nat_big_num.of_int 0)) (** No version *)
let gnu_ext_ver_need_current : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Current version *)

(* Legal values for vna_flags *)
(* gnu_ext_ver_flg_weak *)

(** [gnu_ext_elf32_symbol_version_table] is an array (linked list, here) of
  * [elf32_half] entries.  It has as many entries as the dynamic symbol table
  * (DT_SYMTAB).  I.e., each symbol table entry has its associated entry in the
  * symbol version table.
  *)
type gnu_ext_elf32_symbol_version_table = Uint32_wrapper.uint32
  list

type gnu_ext_elf64_symbol_version_table = Uint32_wrapper.uint32
  list

(*val read_gnu_ext_elf64_versym_table : endianness -> byte_sequence -> error gnu_ext_elf64_symbol_version_table*)
let rec read_gnu_ext_elf64_versym_table endian bs:((Uint32_wrapper.uint32)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then return [] else bind (read_elf64_half endian bs) (fun (v, bs) -> bind (read_gnu_ext_elf64_versym_table endian bs) (fun next ->
  return (v :: next))))

type gnu_ext_elf32_verdef =
  { gnu_ext_elf32_vd_version : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vd_flags   : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vd_ndx     : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vd_cnt     : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vd_hash    : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vd_aux     : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vd_next    : Uint32_wrapper.uint32
   }

type gnu_ext_elf64_verdef =
  { gnu_ext_elf64_vd_version : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vd_flags   : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vd_ndx     : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vd_cnt     : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vd_hash    : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vd_aux     : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vd_next    : Uint32_wrapper.uint32
   }

(*val string_of_gnu_ext_elf32_verdef : gnu_ext_elf32_verdef -> string*)
let string_of_gnu_ext_elf32_verdef verdef:string=
   (unlines [
    ("Version: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf32_vd_version)
  ; ("Flags: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf32_vd_flags)
  ; ("Index: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf32_vd_ndx)
  ; ("Count: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf32_vd_cnt)
  ; ("Hash: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf32_vd_hash)
  ])

(*val string_of_gnu_ext_elf64_verdef : gnu_ext_elf64_verdef -> string*)
let string_of_gnu_ext_elf64_verdef verdef:string=
   (unlines [
    ("Version: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf64_vd_version)
  ; ("Flags: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf64_vd_flags)
  ; ("Index: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf64_vd_ndx)
  ; ("Count: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf64_vd_cnt)
  ; ("Hash: " ^ Uint32_wrapper.to_string verdef.gnu_ext_elf64_vd_hash)
  ])

(*val read_gnu_ext_elf32_verdef : endianness -> byte_sequence -> error (gnu_ext_elf32_verdef * byte_sequence)*)
let read_gnu_ext_elf32_verdef endian bs0:(gnu_ext_elf32_verdef*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_half endian bs0) (fun (ver, bs0) -> bind (read_elf32_half endian bs0) (fun (flg, bs0) -> bind (read_elf32_half endian bs0) (fun (ndx, bs0) -> bind (read_elf32_half endian bs0) (fun (cnt, bs0) -> bind (read_elf32_word endian bs0) (fun (hsh, bs0) -> bind (read_elf32_word endian bs0) (fun (aux, bs0) -> bind (read_elf32_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf32_vd_version = ver; gnu_ext_elf32_vd_flags = flg;
      gnu_ext_elf32_vd_ndx = ndx; gnu_ext_elf32_vd_cnt = cnt;
        gnu_ext_elf32_vd_hash = hsh; gnu_ext_elf32_vd_aux = aux;
      gnu_ext_elf32_vd_next = nxt }, bs0)))))))))

(*val read_gnu_ext_elf64_verdef : endianness -> byte_sequence -> error (gnu_ext_elf64_verdef * byte_sequence)*)
let read_gnu_ext_elf64_verdef endian bs0:(gnu_ext_elf64_verdef*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_half endian bs0) (fun (ver, bs0) -> bind (read_elf64_half endian bs0) (fun (flg, bs0) -> bind (read_elf64_half endian bs0) (fun (ndx, bs0) -> bind (read_elf64_half endian bs0) (fun (cnt, bs0) -> bind (read_elf64_word endian bs0) (fun (hsh, bs0) -> bind (read_elf64_word endian bs0) (fun (aux, bs0) -> bind (read_elf64_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf64_vd_version = ver; gnu_ext_elf64_vd_flags = flg;
      gnu_ext_elf64_vd_ndx = ndx; gnu_ext_elf64_vd_cnt = cnt;
        gnu_ext_elf64_vd_hash = hsh; gnu_ext_elf64_vd_aux = aux;
      gnu_ext_elf64_vd_next = nxt }, bs0)))))))))

(*val gnu_ext_elf32_verdef_size : natural*)
let gnu_ext_elf32_verdef_size:Nat_big_num.num= ( (Nat_big_num.of_int 160))

(*val gnu_ext_elf64_verdef_size : natural*)
let gnu_ext_elf64_verdef_size:Nat_big_num.num= ( (Nat_big_num.of_int 256))

type gnu_ext_elf32_veraux =
  { gnu_ext_elf32_vda_name : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vda_next : Uint32_wrapper.uint32
   }

type gnu_ext_elf64_veraux =
  { gnu_ext_elf64_vda_name : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vda_next : Uint32_wrapper.uint32
   }

(*val gnu_ext_elf32_veraux_size : natural*)
let gnu_ext_elf32_veraux_size:Nat_big_num.num= ( (Nat_big_num.of_int 64))

(*val gnu_ext_elf64_veraux_size : natural*)
let gnu_ext_elf64_veraux_size:Nat_big_num.num= ( (Nat_big_num.of_int 128))

(*val read_gnu_ext_elf32_veraux : endianness -> byte_sequence -> error (gnu_ext_elf32_veraux * byte_sequence)*)
let read_gnu_ext_elf32_veraux endian bs0:(gnu_ext_elf32_veraux*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs0) (fun (nme, bs0) -> bind (read_elf32_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf32_vda_name = nme; gnu_ext_elf32_vda_next = nxt }, bs0))))

(*val read_gnu_ext_elf64_veraux : endianness -> byte_sequence -> error (gnu_ext_elf64_veraux * byte_sequence)*)
let read_gnu_ext_elf64_veraux endian bs0:(gnu_ext_elf64_veraux*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_word endian bs0) (fun (nme, bs0) -> bind (read_elf64_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf64_vda_name = nme; gnu_ext_elf64_vda_next = nxt }, bs0))))

(*val read_gnu_ext_elf64_veraux_table : endianness -> natural -> byte_sequence -> error (list gnu_ext_elf64_veraux * byte_sequence)*)
let rec read_gnu_ext_elf64_veraux_table endian vd_cnt bs:((gnu_ext_elf64_veraux)list*Byte_sequence_wrapper.byte_sequence)error=
   (if Nat_big_num.equal vd_cnt( (Nat_big_num.of_int 0)) then return ([], bs) else bind (read_gnu_ext_elf64_veraux endian bs) (fun (veraux, _) ->
  let vda_next = (Uint32_wrapper.to_bigint veraux.gnu_ext_elf64_vda_next) in bind (Byte_sequence.dropbytes vda_next bs) (fun bs -> bind (read_gnu_ext_elf64_veraux_table endian ( Nat_big_num.sub_nat vd_cnt( (Nat_big_num.of_int 1))) bs) (fun (veraux_table, bs) ->
  return ((veraux :: veraux_table), bs)))))

(*val read_gnu_ext_elf64_verdef_table : endianness -> natural -> byte_sequence -> error (list (gnu_ext_elf64_verdef * list gnu_ext_elf64_veraux) * byte_sequence)*)
let rec read_gnu_ext_elf64_verdef_table endian verdefnum bs:((gnu_ext_elf64_verdef*(gnu_ext_elf64_veraux)list)list*Byte_sequence_wrapper.byte_sequence)error=
   (if Nat_big_num.equal verdefnum( (Nat_big_num.of_int 0)) then return ([], bs) else bind (read_gnu_ext_elf64_verdef endian bs) (fun (verdef, _) ->
  let vd_version = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_version) in
  let vd_aux = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_aux) in
  let vd_cnt = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_cnt) in
  let vd_next = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_next) in
  if not (Nat_big_num.equal vd_version( (Nat_big_num.of_int 1))) then Error.fail ("read_gnu_ext_elf64_verdef_table: unsupported version " ^ (Nat_big_num.to_string vd_version)) else bind (Byte_sequence.dropbytes vd_aux bs) (fun aux_bs -> bind (read_gnu_ext_elf64_veraux_table endian vd_cnt aux_bs) (fun (veraux_table, _) -> bind (Byte_sequence.dropbytes vd_next bs) (fun bs -> bind (read_gnu_ext_elf64_verdef_table endian ( Nat_big_num.sub_nat verdefnum( (Nat_big_num.of_int 1))) bs) (fun (verdef_table, bs) ->
  return (((verdef, veraux_table) :: verdef_table), bs)))))))

type gnu_ext_elf32_verneed =
  { gnu_ext_elf32_vn_version : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vn_cnt     : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vn_file    : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vn_aux     : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vn_next    : Uint32_wrapper.uint32
   }

type gnu_ext_elf64_verneed =
  { gnu_ext_elf64_vn_version : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vn_cnt     : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vn_file    : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vn_aux     : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vn_next    : Uint32_wrapper.uint32
   }

(*val gnu_ext_elf32_verneed_size : natural*)
let gnu_ext_elf32_verneed_size:Nat_big_num.num= ( (Nat_big_num.of_int 128))

(*val gnu_ext_elf64_verneed_size : natural*)
let gnu_ext_elf64_verneed_size:Nat_big_num.num= ( (Nat_big_num.of_int 224))

(*val read_gnu_ext_elf32_verneed : endianness -> byte_sequence -> error (gnu_ext_elf32_verneed * byte_sequence)*)
let read_gnu_ext_elf32_verneed endian bs0:(gnu_ext_elf32_verneed*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_half endian bs0) (fun (ver, bs0) -> bind (read_elf32_half endian bs0) (fun (cnt, bs0) -> bind (read_elf32_word endian bs0) (fun (fle, bs0) -> bind (read_elf32_word endian bs0) (fun (aux, bs0) -> bind (read_elf32_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf32_vn_version = ver; gnu_ext_elf32_vn_cnt = cnt;
      gnu_ext_elf32_vn_file = fle; gnu_ext_elf32_vn_aux = aux;
        gnu_ext_elf32_vn_next = nxt }, bs0)))))))

(*val read_gnu_ext_elf64_verneed : endianness -> byte_sequence -> error (gnu_ext_elf64_verneed * byte_sequence)*)
let read_gnu_ext_elf64_verneed endian bs0:(gnu_ext_elf64_verneed*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_half endian bs0) (fun (ver, bs0) -> bind (read_elf64_half endian bs0) (fun (cnt, bs0) -> bind (read_elf64_word endian bs0) (fun (fle, bs0) -> bind (read_elf64_word endian bs0) (fun (aux, bs0) -> bind (read_elf64_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf64_vn_version = ver; gnu_ext_elf64_vn_cnt = cnt;
      gnu_ext_elf64_vn_file = fle; gnu_ext_elf64_vn_aux = aux;
        gnu_ext_elf64_vn_next = nxt }, bs0)))))))

type gnu_ext_elf32_vernaux =
  { gnu_ext_elf32_vna_hash  : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vna_flags : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vna_other : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vna_name  : Uint32_wrapper.uint32
   ; gnu_ext_elf32_vna_next  : Uint32_wrapper.uint32
   }

type gnu_ext_elf64_vernaux =
  { gnu_ext_elf64_vna_hash  : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vna_flags : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vna_other : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vna_name  : Uint32_wrapper.uint32
   ; gnu_ext_elf64_vna_next  : Uint32_wrapper.uint32
   }

(*val string_of_gnu_ext_elf32_vernaux : gnu_ext_elf32_vernaux -> string*)
let string_of_gnu_ext_elf32_vernaux vernaux:string=
   (unlines [
    ("Hash: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf32_vna_hash)
  ; ("Flags: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf32_vna_flags)
  ; ("Other: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf32_vna_other)
  ; ("Name: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf32_vna_name)
  ; ("Next: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf32_vna_next)
  ])

(*val string_of_gnu_ext_elf64_vernaux : gnu_ext_elf64_vernaux -> string*)
let string_of_gnu_ext_elf64_vernaux vernaux:string=
   (unlines [
    ("Hash: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf64_vna_hash)
  ; ("Flags: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf64_vna_flags)
  ; ("Other: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf64_vna_other)
  ; ("Name: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf64_vna_name)
  ; ("Next: " ^ Uint32_wrapper.to_string vernaux.gnu_ext_elf64_vna_next)
  ])

(*val gnu_ext_elf32_vernaux_size : natural*)
let gnu_ext_elf32_vernaux_size:Nat_big_num.num= ( (Nat_big_num.of_int 16))

(*val gnu_ext_elf64_vernaux_size : natural*)
let gnu_ext_elf64_vernaux_size:Nat_big_num.num= ( (Nat_big_num.of_int 224))

(*val read_gnu_ext_elf32_vernaux : endianness -> byte_sequence -> error (gnu_ext_elf32_vernaux * byte_sequence)*)
let read_gnu_ext_elf32_vernaux endian bs0:(gnu_ext_elf32_vernaux*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs0) (fun (hsh, bs0) -> bind (read_elf32_half endian bs0) (fun (flg, bs0) -> bind (read_elf32_half endian bs0) (fun (otr, bs0) -> bind (read_elf32_word endian bs0) (fun (nme, bs0) -> bind (read_elf32_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf32_vna_hash = hsh; gnu_ext_elf32_vna_flags = flg;
      gnu_ext_elf32_vna_other = otr; gnu_ext_elf32_vna_name = nme;
    gnu_ext_elf32_vna_next = nxt }, bs0)))))))

(*val read_gnu_ext_elf64_vernaux : endianness -> byte_sequence -> error (gnu_ext_elf64_vernaux * byte_sequence)*)
let read_gnu_ext_elf64_vernaux endian bs0:(gnu_ext_elf64_vernaux*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_word endian bs0) (fun (hsh, bs0) -> bind (read_elf64_half endian bs0) (fun (flg, bs0) -> bind (read_elf64_half endian bs0) (fun (otr, bs0) -> bind (read_elf64_word endian bs0) (fun (nme, bs0) -> bind (read_elf64_word endian bs0) (fun (nxt, bs0) ->
    return ({ gnu_ext_elf64_vna_hash = hsh; gnu_ext_elf64_vna_flags = flg;
      gnu_ext_elf64_vna_other = otr; gnu_ext_elf64_vna_name = nme;
    gnu_ext_elf64_vna_next = nxt }, bs0)))))))

(*val read_gnu_ext_elf64_vernaux_table : endianness -> natural -> byte_sequence -> error (list gnu_ext_elf64_vernaux * byte_sequence)*)
let rec read_gnu_ext_elf64_vernaux_table endian vn_cnt bs:((gnu_ext_elf64_vernaux)list*Byte_sequence_wrapper.byte_sequence)error=
   (if Nat_big_num.equal vn_cnt( (Nat_big_num.of_int 0)) then return ([], bs) else bind (read_gnu_ext_elf64_vernaux endian bs) (fun (vernaux, _) ->
  let vna_next = (Uint32_wrapper.to_bigint vernaux.gnu_ext_elf64_vna_next) in bind (Byte_sequence.dropbytes vna_next bs) (fun bs -> bind (read_gnu_ext_elf64_vernaux_table endian ( Nat_big_num.sub_nat vn_cnt( (Nat_big_num.of_int 1))) bs) (fun (vernaux_table, bs) ->
  return ((vernaux :: vernaux_table), bs)))))

(*val read_gnu_ext_elf64_verneed_table : endianness -> natural -> byte_sequence -> error (list (gnu_ext_elf64_verneed * list gnu_ext_elf64_vernaux) * byte_sequence)*)
let rec read_gnu_ext_elf64_verneed_table endian verneednum bs:((gnu_ext_elf64_verneed*(gnu_ext_elf64_vernaux)list)list*Byte_sequence_wrapper.byte_sequence)error=
   (if Nat_big_num.equal verneednum( (Nat_big_num.of_int 0)) then return ([], bs) else bind (read_gnu_ext_elf64_verneed endian bs) (fun (verneed, _) ->
  let vn_version = (Uint32_wrapper.to_bigint verneed.gnu_ext_elf64_vn_version) in
  let vn_aux = (Uint32_wrapper.to_bigint verneed.gnu_ext_elf64_vn_aux) in
  let vn_cnt = (Uint32_wrapper.to_bigint verneed.gnu_ext_elf64_vn_cnt) in
  let vn_next = (Uint32_wrapper.to_bigint verneed.gnu_ext_elf64_vn_next) in
  if not (Nat_big_num.equal vn_version( (Nat_big_num.of_int 1))) then Error.fail ("read_gnu_ext_elf64_verneed_table: unsupported version " ^ (Nat_big_num.to_string vn_version)) else bind (Byte_sequence.dropbytes vn_aux bs) (fun aux_bs -> bind (read_gnu_ext_elf64_vernaux_table endian vn_cnt aux_bs) (fun (vernaux_table, _) -> bind (Byte_sequence.dropbytes vn_next bs) (fun bs -> bind (read_gnu_ext_elf64_verneed_table endian ( Nat_big_num.sub_nat verneednum( (Nat_big_num.of_int 1))) bs) (fun (verneed_table, bs) ->
  return (((verneed, vernaux_table) :: verneed_table), bs)))))))


type gnu_ext_interpreted_verdef = {
  gnu_ext_interpreted_verdef_version : Nat_big_num.num;
  gnu_ext_interpreted_verdef_flags : Nat_big_num.num;
  gnu_ext_interpreted_verdef_ndx : Nat_big_num.num;
  gnu_ext_interpreted_verdef_hash : Nat_big_num.num;
  gnu_ext_interpreted_verdef_name : string;
  gnu_ext_interpreted_verdef_parents : string list
}

type gnu_ext_interpreted_verneed = {
  gnu_ext_interpreted_verneed_version : Nat_big_num.num;
  gnu_ext_interpreted_verneed_file : string
}

type gnu_ext_interpreted_vernaux = {
  gnu_ext_interpreted_vernaux_hash : Nat_big_num.num;
  gnu_ext_interpreted_vernaux_flags : Nat_big_num.num;
  gnu_ext_interpreted_vernaux_other : Nat_big_num.num;
  gnu_ext_interpreted_vernaux_name : string;
  gnu_ext_interpreted_vernaux_verneed : gnu_ext_interpreted_verneed
}

type gnu_ext_interpreted_versym_entry = {
  gnu_ext_interpreted_versym_entry_value : Nat_big_num.num;
  gnu_ext_interpreted_versym_entry_hidden : bool
}

type gnu_ext_interpreted_versym_table = {
  gnu_ext_interpreted_versym_table_entries : gnu_ext_interpreted_versym_entry list;
  gnu_ext_interpreted_versym_table_verdef : gnu_ext_interpreted_verdef list;
  gnu_ext_interpreted_versym_table_verneed : gnu_ext_interpreted_vernaux list
}

(** The unspecified name for the base definition. *)
let gnu_ext_verdef_base_unspecified : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** The name given later to the baseline of symbols once the library started
    using symbol versioning. *)
let gnu_ext_verdef_base_versioned : Nat_big_num.num= ( (Nat_big_num.of_int 2))

(* TODO: borrowed from Dwarf, this should probbaly go somewhere else *)
(*val natural_nat_shift_right : natural -> nat -> natural*)

(*val obtain_gnu_ext_elf64_interpreted_versym_table_symbols : endianness -> elf64_file -> list (natural * elf64_dyn_value) -> error (maybe (list gnu_ext_interpreted_versym_entry))*)
let obtain_gnu_ext_elf64_interpreted_versym_table_symbols endian f dyns:(((gnu_ext_interpreted_versym_entry)list)option)error=
   (let maybe_dt_versym = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal tag Gnu_ext_dynamic.elf_dt_gnu_versym) dyns) in
  (match maybe_dt_versym with
    | Some (_, Address dt_versym) ->
      let dt_versym = (Ml_bindings.nat_big_num_of_uint64 dt_versym) in
      let maybe_versym_scn = (Lem_list.list_find_opt (fun scn -> Nat_big_num.equal
        scn.elf64_section_addr dt_versym
      ) f.elf64_file_interpreted_sections) in bind (match maybe_versym_scn with
        | Some scn -> return scn
        | None -> fail ("obtain_gnu_ext_elf64_interpreted_versym_table: no versym section at 0x" ^ (hex_string_of_natural dt_versym))
      ) (fun versym_scn -> bind (read_gnu_ext_elf64_versym_table endian versym_scn.elf64_section_body) (fun versyms ->
      let mask = (natural_of_hex "0x7FFF") in
      let versyms = (Lem_list.map (fun v ->
        let v = (Uint32_wrapper.to_bigint v) in
        let hidden = (Nat_big_num.shift_right v 15) in
        let v = (Nat_big_num.bitwise_and v mask) in
        {
          gnu_ext_interpreted_versym_entry_value = v;
          gnu_ext_interpreted_versym_entry_hidden = (not (Nat_big_num.equal hidden( (Nat_big_num.of_int 0))))
        }
      ) versyms) in
      return (Some versyms)))
    | None ->
      return None
  ))

(*val obtain_gnu_ext_elf64_interpreted_verdef_table : endianness -> elf64_file -> list (natural * elf64_dyn_value) -> error (maybe (list gnu_ext_interpreted_verdef))*)
let obtain_gnu_ext_elf64_interpreted_verdef_table endian f dyns:(((gnu_ext_interpreted_verdef)list)option)error=
   (let maybe_dt_verdef = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal tag Gnu_ext_dynamic.elf_dt_gnu_verdef) dyns) in
  (match maybe_dt_verdef with
    | Some (_, Address dt_verdef) ->
      let dt_verdef = (Ml_bindings.nat_big_num_of_uint64 dt_verdef) in
      let maybe_dt_verdefnum = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal tag Gnu_ext_dynamic.elf_dt_gnu_verdefnum) dyns) in bind (match maybe_dt_verdefnum with
        | Some (_, Numeric dt_verdefnum) -> return dt_verdefnum
        | None -> Error.fail "obtain_gnu_ext_elf64_interpreted_verdef_table: DT_VERDEF is defined, but DT_VERDEFNUM isn't"
      ) (fun dt_verdefnum ->
      let maybe_verdef_scn = (Lem_list.list_find_opt (fun scn -> Nat_big_num.equal
        scn.elf64_section_addr dt_verdef
      ) f.elf64_file_interpreted_sections) in bind (match maybe_verdef_scn with
        | Some scn -> return scn
        | None -> fail ("obtain_gnu_ext_elf64_interpreted_verdef_table: no verdef section at 0x" ^ (hex_string_of_natural dt_verdef))
      ) (fun verdef_scn -> bind (match Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int verdef_scn.elf64_section_link) with
        | Some strs -> return strs
        | None -> fail "obtain_gnu_ext_elf64_gnu_ext_interpreted_verdef_table: no associated strtab"
      ) (fun strs ->
      let strings = (Byte_sequence.string_of_byte_sequence strs.elf64_section_body) in
      let strtab = (String_table.mk_string_table strings null_char) in bind (read_gnu_ext_elf64_verdef_table endian dt_verdefnum verdef_scn.elf64_section_body) (fun (verdef_table, _) -> bind (Error.mapM (fun (verdef, veraux_table) -> bind (Error.mapM (fun veraux ->
          let vda_name = (Uint32_wrapper.to_bigint veraux.gnu_ext_elf64_vda_name) in
          String_table.get_string_at vda_name strtab
        ) veraux_table) (fun veraux_table -> bind (match veraux_table with
          | [] -> Error.fail "obtain_gnu_ext_elf64_gnu_ext_interpreted_verdef_table: verdef is missing a name"
          | name1 :: parents -> return (name1, parents)
        ) (fun (name1, parents) ->
        return {
          gnu_ext_interpreted_verdef_version = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_version);
          gnu_ext_interpreted_verdef_flags = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_flags);
          gnu_ext_interpreted_verdef_ndx = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_ndx);
          gnu_ext_interpreted_verdef_hash = (Uint32_wrapper.to_bigint verdef.gnu_ext_elf64_vd_hash);
          gnu_ext_interpreted_verdef_name = name1;
          gnu_ext_interpreted_verdef_parents = parents
        }))
      ) verdef_table) (fun verdef_table ->

      return (Some verdef_table))))))
    | None ->
      return None
  ))

(*val obtain_gnu_ext_elf64_interpreted_verneed_table : endianness -> elf64_file -> list (natural * elf64_dyn_value) -> error (maybe (list gnu_ext_interpreted_vernaux))*)
let obtain_gnu_ext_elf64_interpreted_verneed_table endian f dyns:(((gnu_ext_interpreted_vernaux)list)option)error=
   (let maybe_dt_verneed = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal tag Gnu_ext_dynamic.elf_dt_gnu_verneed) dyns) in
  (match maybe_dt_verneed with
    | Some (_, Address dt_verneed) ->
      let dt_verneed = (Ml_bindings.nat_big_num_of_uint64 dt_verneed) in
      let maybe_dt_verneednum = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal tag Gnu_ext_dynamic.elf_dt_gnu_verneednum) dyns) in bind (match maybe_dt_verneednum with
        | Some (_, Numeric dt_verneednum) -> return dt_verneednum
        | None -> Error.fail "obtain_gnu_ext_elf64_interpreted_verneed_table: DT_VERNEED is defined, but DT_VERNEEDNUM isn't"
      ) (fun dt_verneednum ->
      let maybe_verneed_scn = (Lem_list.list_find_opt (fun scn -> Nat_big_num.equal
        scn.elf64_section_addr dt_verneed
      ) f.elf64_file_interpreted_sections) in bind (match maybe_verneed_scn with
        | Some scn -> return scn
        | None -> fail ("obtain_gnu_ext_elf64_gnu_ext_interpreted_verneed_table: no verneed section at 0x" ^ (hex_string_of_natural dt_verneed))
      ) (fun verneed_scn -> bind (match Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int verneed_scn.elf64_section_link) with
        | Some strs -> return strs
        | None -> fail "obtain_gnu_ext_elf64_gnu_ext_interpreted_verneed_table: no associated strtab"
      ) (fun strs ->
      let strings = (Byte_sequence.string_of_byte_sequence strs.elf64_section_body) in
      let strtab = (String_table.mk_string_table strings null_char) in bind (read_gnu_ext_elf64_verneed_table endian dt_verneednum verneed_scn.elf64_section_body) (fun (verneed_table, _) -> bind (Error.foldM (fun acc (verneed, vernaux_table) -> bind (String_table.get_string_at (Uint32_wrapper.to_bigint verneed.gnu_ext_elf64_vn_file) strtab) (fun file ->
        let interp_verneed = ({
          gnu_ext_interpreted_verneed_version = (Uint32_wrapper.to_bigint verneed.gnu_ext_elf64_vn_version);
          gnu_ext_interpreted_verneed_file = file
        }) in bind (Error.mapM (fun vernaux -> bind (String_table.get_string_at (Uint32_wrapper.to_bigint vernaux.gnu_ext_elf64_vna_name) strtab) (fun name1 ->
          return {
            gnu_ext_interpreted_vernaux_hash = (Uint32_wrapper.to_bigint vernaux.gnu_ext_elf64_vna_hash);
            gnu_ext_interpreted_vernaux_flags = (Uint32_wrapper.to_bigint vernaux.gnu_ext_elf64_vna_flags);
            gnu_ext_interpreted_vernaux_other = (Uint32_wrapper.to_bigint vernaux.gnu_ext_elf64_vna_other);
            gnu_ext_interpreted_vernaux_name = name1;
            gnu_ext_interpreted_vernaux_verneed = interp_verneed
          })
        ) vernaux_table) (fun vernaux_entries ->
        return ( List.rev_append (List.rev vernaux_entries) acc)))
      ) [] verneed_table) (fun vernaux_table ->

      return (Some vernaux_table))))))
    | None ->
      return None
  ))

(*val obtain_gnu_ext_elf64_interpreted_versym_table : elf64_file -> list (natural * elf64_dyn_value) -> error (maybe gnu_ext_interpreted_versym_table)*)
let obtain_gnu_ext_elf64_interpreted_versym_table f dyns:((gnu_ext_interpreted_versym_table)option)error=
   (let endian = (get_elf64_header_endianness f.elf64_file_header) in bind (obtain_gnu_ext_elf64_interpreted_versym_table_symbols endian f dyns) (fun maybe_versyms ->
  (match maybe_versyms with
    | Some versyms -> bind (obtain_gnu_ext_elf64_interpreted_verdef_table endian f dyns) (fun maybe_verdefs ->
      let verdefs = ((match maybe_verdefs with
        | Some verdefs -> verdefs
        | None -> []
      )) in bind (obtain_gnu_ext_elf64_interpreted_verneed_table endian f dyns) (fun maybe_verneeds ->
      let verneeds = ((match maybe_verneeds with
        | Some verneeds -> verneeds
        | None -> []
      )) in
      let table = ({
        gnu_ext_interpreted_versym_table_entries = versyms;
        gnu_ext_interpreted_versym_table_verdef = verdefs;
        gnu_ext_interpreted_versym_table_verneed = verneeds
      }) in
      return (Some table)))
    | None ->
      return None
  )))

type gnu_ext_interpreted_verdef_lookup =
  | GnuExtInterpretedVerdefLocal
  | GnuExtInterpretedVerdefGlobal
  | GnuExtInterpretedVerdefVersion of gnu_ext_interpreted_verdef
  | GnuExtInterpretedVerdefHidden of gnu_ext_interpreted_verdef

(*val get_gnu_ext_interpreted_verdef : gnu_ext_interpreted_versym_table -> natural -> error gnu_ext_interpreted_verdef_lookup*)
let get_gnu_ext_interpreted_verdef tbl symidx:(gnu_ext_interpreted_verdef_lookup)error=  (bind (match Lem_list.list_index tbl.gnu_ext_interpreted_versym_table_entries (Nat_big_num.to_int symidx) with
    | Some entry -> return entry
    | None -> Error.fail ("get_gnu_ext_interpreted_verdef: cannot find symbol " ^ (Nat_big_num.to_string symidx))
  ) (fun entry -> if(Nat_big_num.equal entry.gnu_ext_interpreted_versym_entry_value
      ( (Nat_big_num.of_int 0))) then (return GnuExtInterpretedVerdefLocal)
 else
   (
   if(Nat_big_num.equal entry.gnu_ext_interpreted_versym_entry_value
        ( (Nat_big_num.of_int 1))) then
     (return GnuExtInterpretedVerdefGlobal) else
     (let ndx = (entry.gnu_ext_interpreted_versym_entry_value) in
      let maybe_verdef = (Lem_list.list_find_opt
                            (fun verdef -> Nat_big_num.equal
                                             verdef.gnu_ext_interpreted_verdef_ndx
                                             ndx )
                            tbl.gnu_ext_interpreted_versym_table_verdef) in
      (match maybe_verdef with
            | Some verdef ->
      if entry.gnu_ext_interpreted_versym_entry_hidden then
        return (GnuExtInterpretedVerdefHidden verdef) else
        return (GnuExtInterpretedVerdefVersion verdef)
        | None ->
      Error.fail
        ("get_gnu_ext_interpreted_verdef: cannot find verdef " ^
           (Nat_big_num.to_string ndx))
      )))))

(*val get_gnu_ext_interpreted_verneed : gnu_ext_interpreted_versym_table -> natural -> error (maybe gnu_ext_interpreted_vernaux)*)
let get_gnu_ext_interpreted_verneed tbl symidx:((gnu_ext_interpreted_vernaux)option)error=  (bind (match Lem_list.list_index tbl.gnu_ext_interpreted_versym_table_entries (Nat_big_num.to_int symidx) with
    | Some entry -> return entry
    | None -> Error.fail ("get_gnu_ext_interpreted_verneed: cannot find symbol " ^ (Nat_big_num.to_string symidx))
  ) (fun entry ->
  let ndx = (entry.gnu_ext_interpreted_versym_entry_value) in
  let maybe_vernaux = (Lem_list.list_find_opt (fun vernaux -> Nat_big_num.equal
    vernaux.gnu_ext_interpreted_vernaux_other ndx
  ) tbl.gnu_ext_interpreted_versym_table_verneed) in
  (match maybe_vernaux with
    | Some vernaux ->
      return (Some vernaux)
    | None ->
      Error.fail ("get_gnu_ext_interpreted_verneed: cannot find vernaux " ^ (Nat_big_num.to_string ndx))
  )))