Source file elf_note.ml

(*Generated by Lem from elf_note.lem.*)
(** [elf_note] contains data types and functions for interpreting the .note
  * section/segment of an ELF file, and extracting information from that
  * section/segment.
  *)

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

open Auxv
open Byte_sequence
open Endianness
open Error
open Missing_pervasives
open Show

open Elf_program_header_table
open Elf_section_header_table
open Elf_types_native_uint

(** [elf32_note] represents the contents of a .note section or segment.
  *)
type elf32_note =
  { elf32_note_namesz : Uint32_wrapper.uint32 (** The size of the name field. *)
   ; elf32_note_descsz : Uint32_wrapper.uint32 (** The size of the description field. *)
   ; elf32_note_type   : Uint32_wrapper.uint32 (** The type of the note. *)
   ; elf32_note_name   : byte_sequence0 (** The byte sequence corresponding to the name string. *)
   ; elf32_note_desc   : byte_sequence0 (** The byte sequence corresponding to the desc string. *)
   }

(** [elf64_note] represents the contents of a .note section or segment.
  *)
type elf64_note =
  { elf64_note_namesz : Uint32_wrapper.uint32 (** The size of the name field. *)
   ; elf64_note_descsz : Uint32_wrapper.uint32 (** The size of the description field. *)
   ; elf64_note_type   : Uint32_wrapper.uint32 (** The type of the note. *)
   ; elf64_note_name   : byte_sequence0 (** The byte sequence corresponding to the name string. *)
   ; elf64_note_desc   : byte_sequence0 (** The byte sequence corresponding to the desc string. *)
   }

(* Legal values for note segment descriptor types for core files. *)

let nt_prstatus : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Contains copy of prstatus struct *)
let nt_fpregset : Nat_big_num.num= ( (Nat_big_num.of_int 2)) (** Contains copy of fpregset struct *)
let nt_prpsinfo : Nat_big_num.num= ( (Nat_big_num.of_int 3)) (** Contains copy of prpsinfo struct *)
let nt_prxreg : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Contains copy of prxregset struct *)
let nt_taskstruct : Nat_big_num.num= ( (Nat_big_num.of_int 4)) (** Contains copy of task structure *)
let nt_platform : Nat_big_num.num= ( (Nat_big_num.of_int 5)) (** String from sysinfo(SI_PLATFORM) *)
let nt_auxv : Nat_big_num.num= ( (Nat_big_num.of_int 6)) (** Contains copy of auxv array *)
let nt_gwindows : Nat_big_num.num= ( (Nat_big_num.of_int 7)) (** Contains copy of gwindows struct *)
let nt_asrs : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** Contains copy of asrset struct *)
let nt_pstatus : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Contains copy of pstatus struct *)
let nt_psinfo : Nat_big_num.num= ( (Nat_big_num.of_int 13)) (** Contains copy of psinfo struct *)
let nt_prcred : Nat_big_num.num= ( (Nat_big_num.of_int 14)) (** Contains copy of prcred struct *)
let nt_utsname : Nat_big_num.num= ( (Nat_big_num.of_int 15)) (** Contains copy of utsname struct *)
let nt_lwpstatus : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** Contains copy of lwpstatus struct *)
let nt_lwpsinfo : Nat_big_num.num= ( (Nat_big_num.of_int 17)) (** Contains copy of lwpinfo struct *)
let nt_prfpxreg : Nat_big_num.num= ( (Nat_big_num.of_int 20)) (** Contains copy of fprxregset struct *)
let nt_siginfo : Nat_big_num.num=  (natural_of_hex "0x53494749") (** Contains copy of siginfo_t, size might increase *)
let nt_file : Nat_big_num.num=  (natural_of_hex "0x46494c45") (** Contains information about mapped files *)
let nt_prxfpreg : Nat_big_num.num=  (natural_of_hex "0x46e62b7f") (** Contains copy of user_fxsr_struct *)
let nt_ppc_vmx : Nat_big_num.num=  (natural_of_hex "0x100") (** PowerPC Altivec/VMX registers *)
let nt_ppc_spe : Nat_big_num.num=  (natural_of_hex "0x101") (** PowerPC SPE/EVR registers *)
let nt_ppc_vsx : Nat_big_num.num=  (natural_of_hex "0x102") (** PowerPC VSX registers *)
let nt_ppc_tar : Nat_big_num.num=  (natural_of_hex "0x103") (** Target Address Register *)
let nt_ppc_ppr : Nat_big_num.num=  (natural_of_hex "0x104") (** Program Priority Register *)
let nt_ppc_dscr : Nat_big_num.num=  (natural_of_hex "0x105") (** Data Stream Control Register *)
let nt_ppc_ebb : Nat_big_num.num=  (natural_of_hex "0x106") (** Event Based Branch Registers *)
let nt_ppc_pmu : Nat_big_num.num=  (natural_of_hex "0x107") (** Performance Monitor Registers *)
let nt_ppc_tm_cgpr : Nat_big_num.num=  (natural_of_hex "0x108") (** TM checkpointed GPR Registers *)
let nt_ppc_tm_cfpr : Nat_big_num.num=  (natural_of_hex "0x109") (** TM checkpointed FPR Registers *)
let nt_ppc_tm_cvmx : Nat_big_num.num=  (natural_of_hex "0x10a") (** TM checkpointed VMX Registers *)
let nt_ppc_tm_cvsx : Nat_big_num.num=  (natural_of_hex "0x10b") (** TM checkpointed VSX Registers *)
let nt_ppc_tm_spr : Nat_big_num.num=  (natural_of_hex "0x10c") (** TM Special Purpose Registers *)
let nt_ppc_tm_ctar : Nat_big_num.num=  (natural_of_hex "0x10d") (** TM checkpointed Target Address Register *)
let nt_ppc_tm_cppr : Nat_big_num.num=  (natural_of_hex "0x10e") (** TM checkpointed Program Priority Register *)
let nt_ppc_tm_cdscr : Nat_big_num.num=  (natural_of_hex "0x10f") (** TM checkpointed Data Stream Control Register *)
let nt_386_tls : Nat_big_num.num=  (natural_of_hex "0x200") (** i386 TLS slots (struct user_desc) *)
let nt_386_ioperm : Nat_big_num.num=  (natural_of_hex "0x201") (** x86 io permission bitmap (1=deny) *)
let nt_x86_xstate : Nat_big_num.num=  (natural_of_hex "0x202") (** x86 extended state using xsave *)
let nt_s390_high_gprs : Nat_big_num.num=  (natural_of_hex "0x300") (** s390 upper register halves *)
let nt_s390_timer : Nat_big_num.num=  (natural_of_hex "0x301") (** s390 timer register *)
let nt_s390_todcmp : Nat_big_num.num=  (natural_of_hex "0x302") (** s390 TOD clock comparator register *)
let nt_s390_todpreg : Nat_big_num.num=  (natural_of_hex "0x303") (** s390 TOD programmable register *)
let nt_s390_ctrs : Nat_big_num.num=  (natural_of_hex "0x304") (** s390 control registers *)
let nt_s390_prefix : Nat_big_num.num=  (natural_of_hex "0x305") (** s390 prefix register *)
let nt_s390_last_break : Nat_big_num.num=  (natural_of_hex "0x306") (** s390 breaking event address *)
let nt_s390_system_call : Nat_big_num.num=  (natural_of_hex "0x307") (** s390 system call restart data *)
let nt_s390_tdb : Nat_big_num.num=  (natural_of_hex "0x308") (** s390 transaction diagnostic block *)
let nt_arm_vfp : Nat_big_num.num=  (natural_of_hex "0x400") (** ARM VFP/NEON registers *)
let nt_arm_tls : Nat_big_num.num=  (natural_of_hex "0x401") (** ARM TLS register *)
let nt_arm_hw_break : Nat_big_num.num=  (natural_of_hex "0x402") (** ARM hardware breakpoint registers *)
let nt_arm_hw_watch : Nat_big_num.num=  (natural_of_hex "0x403") (** ARM hardware watchpoint registers *)
let nt_arm_system_call : Nat_big_num.num=  (natural_of_hex "0x404") (** ARM system call number *)
let nt_arm_sve : Nat_big_num.num=  (natural_of_hex "0x405") (** ARM Scalable Vector Extension registers *)

(* Legal values for the note segment descriptor types for object files. *)

let nt_version : Nat_big_num.num= ( (Nat_big_num.of_int 1)) (** Contains a version string. *)

(* FreeBSD-specific *)

let nt_procstat_proc : Nat_big_num.num= ( (Nat_big_num.of_int 8)) (** Procstat proc data. *)
let nt_procstat_files : Nat_big_num.num= ( (Nat_big_num.of_int 9)) (** Procstat files data. *)
let nt_procstat_vmmap : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Procstat vmmap data. *)
let nt_procstat_groups : Nat_big_num.num= ( (Nat_big_num.of_int 11)) (** Procstat groups data. *)
let nt_procstat_umask : Nat_big_num.num= ( (Nat_big_num.of_int 12)) (** Procstat umask data. *)
let nt_procstat_rlimit : Nat_big_num.num= ( (Nat_big_num.of_int 13)) (** Procstat rlimit data. *)
let nt_procstat_osrel : Nat_big_num.num= ( (Nat_big_num.of_int 14)) (** Procstat osreldate data. *)
let nt_procstat_psstrings : Nat_big_num.num= ( (Nat_big_num.of_int 15)) (** Procstat ps_strings data. *)
let nt_procstat_auxv : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (** Procstat auxv data. *)


(** [elf64_nt_file_entry] represents the contents of a NT_FILE note entry. *)
type elf64_nt_file_entry =
  { elf64_nt_file_entry_start : Uint64_wrapper.uint64
   ; elf64_nt_file_entry_end : Uint64_wrapper.uint64
   ; elf64_nt_file_entry_offset : Uint64_wrapper.uint64
   ; elf64_nt_file_entry_filename : string
   }

(** [elf64_nt_file] represents the contents of a NT_FILE note. *)
type elf64_nt_file =
  { elf64_nt_file_count : Uint64_wrapper.uint64
   ; elf64_nt_file_page_size : Uint64_wrapper.uint64
   ; elf64_nt_file_entries : elf64_nt_file_entry list
   }

(** [elf64_nt_procstat_vmentry] represents the contents of a FreeBSD
    NT_PROCSTAT_VMMAP note entry (see `struct kinfo_vmentry`). *)
type elf64_nt_procstat_vmentry =
  { elf64_nt_procstat_vmentry_type : Uint32_wrapper.uint32 (** Type of map entry. *)
   ; elf64_nt_procstat_vmentry_start : Uint64_wrapper.uint64 (** Starting address. *)
   ; elf64_nt_procstat_vmentry_end : Uint64_wrapper.uint64 (** Finishing address. *)
   ; elf64_nt_procstat_vmentry_offset : Uint64_wrapper.uint64 (** Mapping offset in object *)
   ; elf64_nt_procstat_vmentry_vn_fileid : Uint64_wrapper.uint64 (** inode number if vnode *)
   ; elf64_nt_procstat_vmentry_vn_fsid : Uint32_wrapper.uint32 (** dev_t of vnode location *)
   ; elf64_nt_procstat_vmentry_flags : Uint32_wrapper.uint32 (** Flags on map entry. *)
   ; elf64_nt_procstat_vmentry_resident : Uint32_wrapper.uint32 (** Number of resident pages. *)
   ; elf64_nt_procstat_vmentry_protection : Uint32_wrapper.uint32 (** Protection bitmask. *)
   ; elf64_nt_procstat_vmentry_ref_count : Uint32_wrapper.uint32 (** VM obj ref count. *)
   ; elf64_nt_procstat_vmentry_shadow_count : Uint32_wrapper.uint32 (** VM obj shadow count. *)
   ; elf64_nt_procstat_vmentry_vn_type : Uint32_wrapper.uint32 (** Vnode type. *)
   ; elf64_nt_procstat_vmentry_vn_size : Uint64_wrapper.uint64 (** File size. *)
   ; elf64_nt_procstat_vmentry_vn_rdev : Uint32_wrapper.uint32 (** Device id if device. *)
   ; elf64_nt_procstat_vmentry_vn_mode : Uint32_wrapper.uint32 (** File mode. *)
   ; elf64_nt_procstat_vmentry_status : Uint32_wrapper.uint32 (** Status flags. *)
   ; elf64_nt_procstat_vmentry_path : string (** Path to VM obj, if any. *)
   }

(* Note names and descriptions are 4-byte aligned (even ELF64 notes) *)
(*val note_align : natural -> natural*)
let note_align n:Nat_big_num.num=  (Nat_big_num.mul
  ( Nat_big_num.div( Nat_big_num.add n( (Nat_big_num.of_int 3)))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 4)))

(** [read_elf32_note endian bs0] transcribes an ELF note section from byte
  * sequence [bs0] assuming endianness [endian].  May fail if transcription fails
  * (i.e. if the byte sequence is not sufficiently long).
  *)
(*val read_elf32_note : endianness -> byte_sequence -> error (elf32_note * byte_sequence)*)
let read_elf32_note endian bs0:(elf32_note*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs0) (fun (namesz, bs0) -> bind (read_elf32_word endian bs0) (fun (descsz, bs0) -> bind (read_elf32_word endian bs0) (fun (typ, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint namesz)) bs0) (fun (name1, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint descsz)) bs0) (fun (desc, bs0) -> bind (
  (* Strip padding *)Byte_sequence.takebytes (Uint32_wrapper.to_bigint namesz) name1) (fun (name1) -> bind (Byte_sequence.takebytes (Uint32_wrapper.to_bigint descsz) desc) (fun (desc) ->
  let note = ({
    elf32_note_namesz = namesz;
    elf32_note_descsz = descsz;
    elf32_note_type = typ;
    elf32_note_name = name1;
    elf32_note_desc = desc
  }) in
  return (note, bs0)))))))))

(** [read_elf64_note endian bs0] transcribes an ELF note section from byte
  * sequence [bs0] assuming endianness [endian].  May fail if transcription fails
  * (i.e. if the byte sequence is not sufficiently long).
  *)
(*val read_elf64_note : endianness -> byte_sequence -> error (elf64_note * byte_sequence)*)
let read_elf64_note endian bs0:(elf64_note*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_word endian bs0) (fun (namesz, bs0) -> bind (read_elf64_word endian bs0) (fun (descsz, bs0) -> bind (read_elf64_word endian bs0) (fun (typ, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint namesz)) bs0) (fun (name1, bs0) -> bind (Byte_sequence.partition0 (note_align (Uint32_wrapper.to_bigint descsz)) bs0) (fun (desc, bs0) -> bind (
  (* Strip padding *)Byte_sequence.takebytes (Uint32_wrapper.to_bigint namesz) name1) (fun (name1) -> bind (Byte_sequence.takebytes (Uint32_wrapper.to_bigint descsz) desc) (fun (desc) ->
  let note = ({
    elf64_note_namesz = namesz;
    elf64_note_descsz = descsz;
    elf64_note_type = typ;
    elf64_note_name = name1;
    elf64_note_desc = desc
  }) in
  return (note, bs0)))))))))

(*val read_all_elf32_notes : endianness -> byte_sequence -> error (list elf32_note)*)
let rec read_all_elf32_notes endian bs:((elf32_note)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf32_note endian bs) (fun (note, next_bs) -> bind (read_all_elf32_notes endian next_bs) (fun next_notes ->
    return (note :: next_notes))))

(*val read_all_elf64_notes : endianness -> byte_sequence -> error (list elf64_note)*)
let rec read_all_elf64_notes endian bs:((elf64_note)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf64_note endian bs) (fun (note, next_bs) -> bind (read_all_elf64_notes endian next_bs) (fun next_notes ->
    return (note :: next_notes))))

(** [obtain_elf32_note_sections endian sht bs0] returns all note sections present
  * in an ELF file, as indicated by the file's section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf32_note_sections : endianness -> elf32_section_header_table ->
  byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_sections endian sht bs0:((elf32_note)list)error=
   (let note_sects =
    (List.filter (fun x ->
      x.elf32_sh_type = Uint32_wrapper.of_bigint sht_note
    ) sht)
  in
    foldM (fun notes x ->
      let offset = (Uint32_wrapper.to_bigint x.elf32_sh_offset) in
      let size2 = (Uint32_wrapper.to_bigint x.elf32_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf32_notes endian rel) (fun sec_notes ->
      return ( List.rev_append (List.rev sec_notes) notes)))
    ) [] note_sects)

(** [obtain_elf64_note_sections endian sht bs0] returns all note sections present
  * in an ELF file, as indicated by the file's section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf64_note_sections : endianness -> elf64_section_header_table ->
  byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_sections endian sht bs0:((elf64_note)list)error=
   (let note_sects =
    (List.filter (fun x ->
      x.elf64_sh_type = Uint32_wrapper.of_bigint sht_note
    ) sht)
  in
    foldM (fun notes x ->
      let offset = (Uint64_wrapper.to_bigint x.elf64_sh_offset) in
      let size2   = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf64_notes endian rel) (fun sec_notes ->
      return ( List.rev_append (List.rev sec_notes) notes)))
    ) [] note_sects)

(** [obtain_elf32_note_segments endian pht bs0] returns all note segments present
  * in an ELF file, as indicated by the file's program header table [pht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf32_note_segments : endianness -> elf32_program_header_table ->
  byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_segments endian pht bs0:((elf32_note)list)error=
   (let note_segs =
    (List.filter (fun x ->
      x.elf32_p_type = Uint32_wrapper.of_bigint elf_pt_note
    ) pht)
  in
    foldM (fun notes x ->
      let offset = (Uint32_wrapper.to_bigint x.elf32_p_offset) in
      let size2 = (Uint32_wrapper.to_bigint x.elf32_p_filesz) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf32_notes endian rel) (fun seg_notes ->
      return ( List.rev_append (List.rev seg_notes) notes)))
    ) [] note_segs)

(** [obtain_elf64_note_segments endian pht bs0] returns all note segments present
  * in an ELF file, as indicated by the file's program header table [pht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section fails.
  *)
(*val obtain_elf64_note_segments : endianness -> elf64_program_header_table ->
  byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_segments endian pht bs0:((elf64_note)list)error=
   (let note_segs =
    (List.filter (fun x ->
      x.elf64_p_type = Uint32_wrapper.of_bigint elf_pt_note
    ) pht)
  in
    foldM (fun notes x ->
      let offset = (Uint64_wrapper.to_bigint x.elf64_p_offset) in
      let size2 = (Ml_bindings.nat_big_num_of_uint64 x.elf64_p_filesz) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel -> bind (read_all_elf64_notes endian rel) (fun seg_notes ->
      return ( List.rev_append (List.rev seg_notes) notes)))
    ) [] note_segs)

(** [obtain_elf32_note_section_and_segments endian pht sht bs0] returns all note
  * sections and segments present in an ELF file, as indicated by the file's
  * program header table [pht] and section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section or segment fails.
  *)
(*val obtain_elf32_note_section_and_segments : endianness -> elf32_program_header_table ->
  elf32_section_header_table -> byte_sequence -> error (list elf32_note)*)
let obtain_elf32_note_section_and_segments endian pht sht bs0:((elf32_note)list)error=  (bind (obtain_elf32_note_segments endian pht bs0) (fun pht_notes -> bind (obtain_elf32_note_sections endian sht bs0) (fun sht_notes ->
  return ( List.rev_append (List.rev pht_notes) sht_notes))))

(** [obtain_elf64_note_section_and_segments endian pht sht bs0] returns all note
  * sections and segments present in an ELF file, as indicated by the file's
  * program header table [pht] and section header table [sht], reading
  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
  * transcription of a note section or segment fails.
  *)
(*val obtain_elf64_note_section_and_segments : endianness -> elf64_program_header_table ->
  elf64_section_header_table -> byte_sequence -> error (list elf64_note)*)
let obtain_elf64_note_section_and_segments endian pht sht bs0:((elf64_note)list)error=  (bind (obtain_elf64_note_segments endian pht bs0) (fun pht_notes -> bind (obtain_elf64_note_sections endian sht bs0) (fun sht_notes ->
  return ( List.rev_append (List.rev pht_notes) sht_notes))))

(** [name_string_of_elf32_note note] extracts the name string of an ELF note
  * section, interpreting the section's uninterpreted name field as a string.
  *)
(*val name_string_of_elf32_note : elf32_note -> string*)
let name_string_of_elf32_note note:string=
   (
  (* Strip NULL terminator *)(match Byte_sequence.takebytes ( Nat_big_num.sub_nat(Uint32_wrapper.to_bigint note.elf32_note_namesz)( (Nat_big_num.of_int 1))) note.elf32_note_name with
    | Success bs -> Byte_sequence.string_of_byte_sequence bs
    | Fail err -> failwith err
  ))

(** [name_string_of_elf64_note note] extracts the name string of an ELF note
  * section, interpreting the section's uninterpreted name field as a string.
  *)
(*val name_string_of_elf64_note : elf64_note -> string*)
let name_string_of_elf64_note note:string=
   (
  (* Strip NULL terminator *)(match Byte_sequence.takebytes ( Nat_big_num.sub_nat(Uint32_wrapper.to_bigint note.elf64_note_namesz)( (Nat_big_num.of_int 1))) note.elf64_note_name with
    | Success bs -> Byte_sequence.string_of_byte_sequence bs
    | Fail err -> failwith err
  ))

(** [read_freebsd_note_desc] unwraps a FreeBSD note description, checking that
    the size of  *)
(*val read_elf64_freebsd_note_desc : endianness -> elf64_note -> natural -> error byte_sequence*)
let read_elf64_freebsd_note_desc endian note struct_size:(Byte_sequence_wrapper.byte_sequence)error=
   (let note_name = (name_string_of_elf64_note note) in
  if not (note_name = "FreeBSD") then Error.fail ("read_elf64_freebsd_note_desc: `" ^ (note_name ^ "` isn't a FreeBSD note")) else bind (read_elf64_word endian note.elf64_note_desc) (fun (size2, bs) ->
  if not (Nat_big_num.equal (Uint32_wrapper.to_bigint size2) struct_size) then
    Error.fail ("read_elf64_freebsd_note_desc: unsupported struct size for FreeBSD note type " ^ ((Uint32_wrapper.to_string note.elf64_note_type) ^ (" (has " ^ ((Uint32_wrapper.to_string size2) ^ (", want " ^ ((Nat_big_num.to_string struct_size) ^ ")"))))))
  else
    return bs))

(* Functions to parse specific note types *)

(*val read_string' : byte_sequence -> error (list byte * byte_sequence)*)
let rec read_string' bs:((char)list*Byte_sequence_wrapper.byte_sequence)error=  (bind (Byte_sequence.read_char bs) (fun (b, bs) ->
  if b = '\000' then
    return ([], bs)
  else bind (read_string' bs) (fun (next, bs) ->
    return ((b :: next), bs))))

(* Parses a single NULL-terminated string *)
(* TODO: move this somewhere else *)
(*val read_string : byte_sequence -> error (string * byte_sequence)*)
let read_string bs:(string*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_string' bs) (fun (l, bs) ->
  return (Byte_sequence.string_of_byte_sequence (Byte_sequence.byte_sequence_of_byte_list l), bs)))

(*val read_elf64_nt_file_entry : endianness -> byte_sequence -> string -> error (elf64_nt_file_entry * byte_sequence)*)
let read_elf64_nt_file_entry endian bs filename1:(elf64_nt_file_entry*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_xword endian bs) (fun (map_start, bs) -> bind (read_elf64_xword endian bs) (fun (map_end, bs) -> bind (read_elf64_xword endian bs) (fun (file_offset, bs) ->
  let e = ({
    elf64_nt_file_entry_start = map_start;
    elf64_nt_file_entry_end = map_end;
    elf64_nt_file_entry_offset = file_offset;
    elf64_nt_file_entry_filename = filename1
  }) in
  return (e, bs)))))

(*val read_elf64_nt_file_entries : endianness -> byte_sequence -> byte_sequence -> error (list elf64_nt_file_entry)*)
let rec read_elf64_nt_file_entries endian entries_bs filenames_bs:((elf64_nt_file_entry)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 entries_bs)( (Nat_big_num.of_int 0)) then
    if not (Nat_big_num.equal (Byte_sequence.length0 filenames_bs)( (Nat_big_num.of_int 0))) then
      fail "read_nt_file_entries: malformed filenames (trailing data)"
    else
      return []
  else bind (read_string filenames_bs) (fun (filename1, filenames_bs) -> bind (read_elf64_nt_file_entry endian entries_bs filename1) (fun (e, entries_bs) -> bind (read_elf64_nt_file_entries endian entries_bs filenames_bs) (fun (next) ->
    return (e :: next)))))

(* See https://sourceware.org/ml/binutils/2012-10/msg00309.html *)
(*val read_elf64_nt_file : endianness -> byte_sequence -> error elf64_nt_file*)
let read_elf64_nt_file endian bs:(elf64_nt_file)error=  (bind (read_elf64_xword endian bs) (fun (count, bs) -> bind (read_elf64_xword endian bs) (fun (page_size, bs) ->
  let addr_size =( (Nat_big_num.of_int 8)) in bind (
  (* read_nt_file_entry reads 3 elf64_xword values *)Byte_sequence.partition0 ( Nat_big_num.mul (Nat_big_num.mul( (Nat_big_num.of_int 3)) addr_size) (Ml_bindings.nat_big_num_of_uint64 count)) bs) (fun (entries_bs, filenames_bs) -> bind (read_elf64_nt_file_entries endian entries_bs filenames_bs) (fun (entries) ->
  return {
    elf64_nt_file_count = count;
    elf64_nt_file_page_size = page_size;
    elf64_nt_file_entries = entries
  })))))

(*val read_elf64_nt_procstat_vmentry : endianness -> byte_sequence -> error (elf64_nt_procstat_vmentry * byte_sequence)*)
let read_elf64_nt_procstat_vmentry endian bs:(elf64_nt_procstat_vmentry*Byte_sequence_wrapper.byte_sequence)error=
   (let bs_len_before = (Byte_sequence.length0 bs) in bind (read_elf64_word endian bs) (fun (structsize, bs) -> bind (read_elf64_word endian bs) (fun (type_, bs) -> bind (read_elf64_xword endian bs) (fun (start, bs) -> bind (read_elf64_xword endian bs) (fun (end_, bs) -> bind (read_elf64_xword endian bs) (fun (offset, bs) -> bind (read_elf64_xword endian bs) (fun (vn_fileid, bs) -> bind (read_elf64_word endian bs) (fun (vn_fsid, bs) -> bind (read_elf64_word endian bs) (fun (flags, bs) -> bind (read_elf64_word endian bs) (fun (resident, bs) -> bind (read_elf64_word endian bs) (fun (protection, bs) -> bind (read_elf64_word endian bs) (fun (ref_count, bs) -> bind (read_elf64_word endian bs) (fun (shadow_count, bs) -> bind (read_elf64_word endian bs) (fun (vn_type, bs) -> bind (read_elf64_xword endian bs) (fun (vn_size, bs) -> bind (read_elf64_word endian bs) (fun (vn_rdev, bs) -> bind (read_elf64_half endian bs) (fun (vn_mode, bs) -> bind (read_elf64_half endian bs) (fun (status, bs) -> bind (read_elf64_word endian bs) (fun (vn_rdev, bs) -> bind (Byte_sequence.dropbytes ( Nat_big_num.mul( (Nat_big_num.of_int 12))( (Nat_big_num.of_int 4))) bs) (fun bs -> (* int _kve_ispare[12] *)
  let bs_len_after = (Byte_sequence.length0 bs) in
  let remaining = (Nat_big_num.sub_nat (Uint32_wrapper.to_bigint structsize) ( Nat_big_num.sub_nat bs_len_before bs_len_after)) in bind (
  (* path_bs is NULL-terminated *)Byte_sequence.partition0 remaining bs) (fun (path_bs, bs) -> bind (read_string path_bs) (fun (path, _) ->
  let e = ({
    elf64_nt_procstat_vmentry_type = type_;
    elf64_nt_procstat_vmentry_start = start;
    elf64_nt_procstat_vmentry_end = end_;
    elf64_nt_procstat_vmentry_offset = offset;
    elf64_nt_procstat_vmentry_vn_fileid = vn_fileid;
    elf64_nt_procstat_vmentry_vn_fsid = vn_fsid;
    elf64_nt_procstat_vmentry_flags = flags;
    elf64_nt_procstat_vmentry_resident = resident;
    elf64_nt_procstat_vmentry_protection = protection;
    elf64_nt_procstat_vmentry_ref_count = ref_count;
    elf64_nt_procstat_vmentry_shadow_count = shadow_count;
    elf64_nt_procstat_vmentry_vn_type = vn_type;
    elf64_nt_procstat_vmentry_vn_size = vn_size;
    elf64_nt_procstat_vmentry_vn_rdev = vn_rdev;
    elf64_nt_procstat_vmentry_vn_mode = vn_mode;
    elf64_nt_procstat_vmentry_status = status;
    elf64_nt_procstat_vmentry_path = path;
  }) in
  return (e, bs)))))))))))))))))))))))

(*val read_elf64_nt_procstat_vmmap : endianness -> byte_sequence -> error (list elf64_nt_procstat_vmentry)*)
let rec read_elf64_nt_procstat_vmmap endian bs:((elf64_nt_procstat_vmentry)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf64_nt_procstat_vmentry endian bs) (fun (e, bs) -> bind (read_elf64_nt_procstat_vmmap endian bs) (fun (next) ->
    return (e :: next))))

(*val read_elf64_nt_procstat_psstrings : endianness -> byte_sequence -> error elf64_addr*)
let read_elf64_nt_procstat_psstrings endian bs:(Uint64_wrapper.uint64)error=  (bind (read_elf64_addr endian bs) (fun (addr, _) ->
  return addr))

(* Some various structs one can find in notes *)

(** [elf64_psstrings] is FreeBSD's `struct ps_strings` *)
type elf64_psstrings = {
  elf64_psstrings_argvstr : Uint64_wrapper.uint64;
  elf64_psstrings_nargvstr : Uint32_wrapper.uint32; (** the number of argument strings *)
  elf64_psstrings_envstr : Uint64_wrapper.uint64;
  elf64_psstrings_nenvstr : Uint32_wrapper.uint32; (** the number of environment strings *)
}

(*val read_elf64_psstrings : endianness -> byte_sequence -> error elf64_psstrings*)
let read_elf64_psstrings endian bs:(elf64_psstrings)error=  (bind (read_elf64_addr endian bs) (fun (argvstr, bs) -> bind (read_elf64_word endian bs) (fun (nargvstr, bs) -> bind (read_elf64_addr endian bs) (fun (envstr, bs) -> bind (read_elf64_word endian bs) (fun (nenvstr, _) ->
  return {
    elf64_psstrings_argvstr = argvstr;
    elf64_psstrings_nargvstr = nargvstr;
    elf64_psstrings_envstr = envstr;
    elf64_psstrings_nenvstr = nenvstr;
  })))))

(* Interpreted, abstracted, common versions of those structs *)

(** A mmap table entry suitable for both Linux and FreeBSD. *)
type mmap_entry = {
  mmap_entry_start : Nat_big_num.num;
  mmap_entry_end : Nat_big_num.num;
  mmap_entry_offset : Nat_big_num.num;
  mmap_entry_path : string
}

let read_nt_file_entries endian note_segs:((mmap_entry)list)error=
   (Error.foldM (fun acc note_seg ->
    let note_name = (name_string_of_elf64_note note_seg) in
    let note_type = (Uint32_wrapper.to_bigint note_seg.elf64_note_type) in
    if (note_name = "CORE") && Nat_big_num.equal note_type nt_file then bind (read_elf64_nt_file endian note_seg.elf64_note_desc) (fun nt_file1 ->
      let entries = (Lem_list.map (fun e ->
        let _ = (prerr_endline (
          "NT_FILE"
          ^ (" start=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_start))
          ^ (" end=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_end))
          ^ (" offset=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_offset))
          ^ (" filename=`" ^ (e.elf64_nt_file_entry_filename ^ "`"))))))))
        )) in
        {
          mmap_entry_start = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_start);
          mmap_entry_end = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_end);
          mmap_entry_offset = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_file_entry_offset);
          mmap_entry_path = (e.elf64_nt_file_entry_filename)
        }
      ) nt_file1.elf64_nt_file_entries) in
      return ( List.rev_append (List.rev acc) entries))
    else
      return acc
  ) [] note_segs)

let read_nt_procstat_vmmap endian note_segs:((mmap_entry)list)error=
   (Error.foldM (fun acc note_seg ->
    let note_name = (name_string_of_elf64_note note_seg) in
    let note_type = (Uint32_wrapper.to_bigint note_seg.elf64_note_type) in
    if (note_name = "FreeBSD") && Nat_big_num.equal note_type nt_procstat_vmmap then
      let struct_size = (natural_of_hex "0x488") in bind ( (* sizeof(struct kinfo_vmentry) *)read_elf64_freebsd_note_desc endian note_seg struct_size) (fun bs -> bind (read_elf64_nt_procstat_vmmap endian bs) (fun entries ->

      let entries = (Lem_list.map (fun e ->
        let _ = (prerr_endline (
          "NT_PROCSTAT_VMMAP"
          ^ (" start=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_start))
          ^ (" end=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_end))
          ^ (" offset=0x" ^ ((hex_string_of_natural (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_offset))
          ^ (" path=`" ^ (e.elf64_nt_procstat_vmentry_path ^ "`"))))))))
        )) in
        {
          mmap_entry_start = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_start);
          mmap_entry_end = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_end);
          mmap_entry_offset = (Ml_bindings.nat_big_num_of_uint64 e.elf64_nt_procstat_vmentry_offset);
          mmap_entry_path = (e.elf64_nt_procstat_vmentry_path)
        }
      ) entries) in

      return ( List.rev_append (List.rev acc) entries)))
    else
      return acc
  ) [] note_segs)

(*val read_mmap_table : endianness -> list elf64_note -> error (list mmap_entry)*)
let read_mmap_table endian note_segs:((mmap_entry)list)error=  (bind (read_nt_file_entries endian note_segs) (fun nt_file_entries -> bind (read_nt_procstat_vmmap endian note_segs) (fun nt_procstat_vmmap1 ->
  (* TODO: don't allow both mmap table types to be present at the same time *)
  return ( List.rev_append (List.rev nt_file_entries) nt_procstat_vmmap1))))

(*val get_mmap_entry_at : list mmap_entry -> natural -> maybe mmap_entry*)
let get_mmap_entry_at mmap_table addr:(mmap_entry)option=
   (let l = (List.filter (fun e -> Nat_big_num.greater_equal
    addr e.mmap_entry_start && Nat_big_num.less addr e.mmap_entry_end
  ) mmap_table) in
  (match l with
    | [e] -> Some e
    | [] -> None
    | _ -> failwith ("get_mmap_entry_at: multiple mmap entries found at 0x" ^ (hex_string_of_natural addr))
  ))

let read_all_elf64_nt_auxv endian note_segs:((elf64_auxv)list)error=
   (Error.foldM (fun auxv_list note_seg ->
    let note_name = (name_string_of_elf64_note note_seg) in
    let note_type = (Uint32_wrapper.to_bigint note_seg.elf64_note_type) in
    if ((note_name = "CORE") && Nat_big_num.equal note_type nt_auxv)
        || ((note_name = "FreeBSD") && Nat_big_num.equal note_type nt_procstat_auxv) then
      let bs = (note_seg.elf64_note_desc) in
      let bs_res = (if note_name = "FreeBSD" then
        read_elf64_freebsd_note_desc endian note_seg( (Nat_big_num.of_int 16)) (* sizeof(Elf_Auxvinfo) *)
      else
        return bs)
      in bind bs_res (fun bs -> bind (Auxv.read_all_elf64_auxv endian bs) (fun l ->
      return ( List.rev_append (List.rev auxv_list) l)))
    else
      return auxv_list
  ) [] note_segs)