(*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_basic_classes
open Lem_list
open Lem_num
open Lem_string

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.uint32 (** The size of the name field. *)
   ; elf32_note_descsz : Uint32.uint32 (** The size of the description field. *)
   ; elf32_note_type   : Uint32.uint32 (** The type of the note. *)
   ; elf32_note_name   : char list  (** The list of bytes (of length indicated above) corresponding to the name string. *)
   ; elf32_note_desc   : char list  (** The list of bytes (of length indicated above) corresponding to the desc string. *)
   }
   
(** [elf64_note] represents the contents of a .note section or segment.
  *)
type elf64_note =
  { elf64_note_namesz : Uint64.uint64 (** The size of the name field. *)
   ; elf64_note_descsz : Uint64.uint64 (** The size of the description field. *)
   ; elf64_note_type   : Uint64.uint64 (** The type of the note. *)
   ; elf64_note_name   : char list   (** The list of bytes (of length indicated above) corresponding to the name string. *)
   ; elf64_note_desc   : char list   (** The list of bytes (of length indicated above) corresponding to the desc string. *)
   }
   
(** [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)error=  
 (read_elf32_word endian bs0 >>= (fun (namesz, bs0) ->
  read_elf32_word endian bs0 >>= (fun (descsz, bs0) ->
  read_elf32_word endian bs0 >>= (fun (typ, bs0) ->
  repeatM' (Nat_big_num.of_string (Uint32.to_string namesz)) bs0 read_char >>= (fun (name1, bs0) ->
  repeatM' (Nat_big_num.of_string (Uint32.to_string descsz)) bs0 read_char >>= (fun (desc, bs0) ->
  return ({ elf32_note_namesz = namesz; elf32_note_descsz = descsz;
    elf32_note_type = typ; elf32_note_name = name1; elf32_note_desc = desc },
      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)error=  
 (read_elf64_xword endian bs0 >>= (fun (namesz, bs0) ->
  read_elf64_xword endian bs0 >>= (fun (descsz, bs0) ->
  read_elf64_xword endian bs0 >>= (fun (typ, bs0) ->
  repeatM' (Ml_bindings.nat_big_num_of_uint64 namesz) bs0 read_char >>= (fun (name1, bs0) ->
  repeatM' (Ml_bindings.nat_big_num_of_uint64 descsz) bs0 read_char >>= (fun (desc, bs0) ->
  return ({ elf64_note_namesz = namesz; elf64_note_descsz = descsz;
    elf64_note_type = typ; elf64_note_name = name1; elf64_note_desc = desc },
      bs0)))))))
      
(** [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.of_string (Nat_big_num.to_string sht_note)
    ) sht)
  in
    mapM (fun x ->
      let offset = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset)) in
      let size2   = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_size)) in
      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
      read_elf32_note endian rel >>= (fun (note, _) ->
      return note))
    ) 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.of_string (Nat_big_num.to_string sht_note)
    ) sht)
  in
    mapM (fun x ->
      let offset = (Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset)) in
      let size2   = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in
      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
      read_elf64_note endian rel >>= (fun (note, _) ->
      return note))
    ) 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.of_string (Nat_big_num.to_string elf_pt_note)
    ) pht)
  in
    mapM (fun x ->
      let offset = (Nat_big_num.of_string (Uint32.to_string x.elf32_p_offset)) in
      let size2   = (Nat_big_num.of_string (Uint32.to_string x.elf32_p_filesz)) in
      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
      read_elf32_note endian rel >>= (fun (note, _) ->
      return note))
    ) 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.of_string (Nat_big_num.to_string elf_pt_note)
    ) pht)
  in
    mapM (fun x ->
      let offset = (Nat_big_num.of_string (Uint64.to_string x.elf64_p_offset)) in
      let size2   = (Ml_bindings.nat_big_num_of_uint64 x.elf64_p_filesz) in
      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
      read_elf64_note endian rel >>= (fun (note, _) ->
      return note))
    ) 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=  
 (obtain_elf32_note_segments endian pht bs0 >>= (fun pht_notes ->
  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=  
 (obtain_elf64_note_segments endian pht bs0 >>= (fun pht_notes ->
  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=  
 (let bs0   = (Byte_sequence.from_byte_lists [note.elf32_note_name]) in
    Byte_sequence.string_of_byte_sequence bs0)
  
(** [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=  
 (let bs0   = (Byte_sequence.from_byte_lists [note.elf64_note_name]) in
    Byte_sequence.string_of_byte_sequence bs0)