diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_note.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_note.ml | 196 |
1 files changed, 196 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/elf_note.ml b/lib/ocaml_rts/linksem/elf_note.ml new file mode 100644 index 00000000..f9965d68 --- /dev/null +++ b/lib/ocaml_rts/linksem/elf_note.ml @@ -0,0 +1,196 @@ +(*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) |