Source file gnu_ext_note.ml

(*Generated by Lem from gnu_extensions/gnu_ext_note.lem.*)
(** [gnu_ext_note] contains GNU extension specific definitions relating to the
  * .note section/segment of an ELF file.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_string

open Byte_sequence
open Endianness
open Error
open Missing_pervasives
open String_table

open Elf_note
open Elf_section_header_table
open Elf_types_native_uint

open Gnu_ext_section_header_table

(** The following two functions are utility functions to convert a list of bytes
  * into words, ready for further processing into strings.
  *)

(*val group_elf32_words : endianness -> list byte -> error (list elf32_word)*)
let rec group_elf32_words endian xs:((Uint32_wrapper.uint32)list)error=
   ((match xs with
    | []                 -> return []
    | x1::x2::x3::x4::xs ->
      let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in bind (read_elf32_word   endian bs0) (fun (w, _) ->  bind (group_elf32_words endian xs) (fun ws ->
      return (w::ws)))
    | xs                 -> fail "group_elf32_words: the impossible happened"
  ))

(*val group_elf64_words : endianness -> list byte -> error (list elf64_word)*)
let rec group_elf64_words endian xs:((Uint32_wrapper.uint32)list)error=
   ((match xs with
    | []                 -> return []
    | x1::x2::x3::x4::xs ->
      let bs0 = (Byte_sequence.from_byte_lists [[x1;x2;x3;x4]]) in bind (read_elf64_word   endian bs0) (fun (w, _) ->  bind (group_elf64_words endian xs) (fun ws ->
      return (w::ws)))
    | xs                 -> fail "group_elf64_words: the impossible happened"
  ))

(** [gnu_ext_check_elf32_abi_note_tag_section endain sht stbl bs0] checks the
  * .note.ABI-tag section of an ELF file to ensure conformance with the GNU
  * extensions.  The string in this note should contain the string "GNU".
  *)
(*val gnu_ext_check_elf32_abi_note_tag_section : endianness -> elf32_section_header_table ->
  string_table -> byte_sequence -> bool*)
let gnu_ext_check_elf32_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf32_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint32_wrapper.to_bigint note.elf32_sh_offset) in
        let siz = (Uint32_wrapper.to_bigint note.elf32_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf32_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> false
            | Success abi_tag ->
              let str = (name_string_of_elf32_note abi_tag) in
                if str = "GNU\000" then
                  if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf32_note_descsz)( (Nat_big_num.of_int 16)) then
                    if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf32_note_descsz)( (Nat_big_num.of_int 16)) then Nat_big_num.greater_equal
                      (Byte_sequence.length0 abi_tag.elf32_note_desc)( (Nat_big_num.of_int 16))
                    else
                      true
                  else
                    false
                else
                  false
          )
      | _      ->
          false
    ))

(** [gnu_ext_check_elf64_abi_note_tag_section endain sht stbl bs0] checks the
  * .note.ABI-tag section of an ELF file to ensure conformance with the GNU
  * extensions.  The string in this note should contain the string "GNU".
  *)
(*val gnu_ext_check_elf64_abi_note_tag_section : endianness -> elf64_section_header_table ->
  string_table -> byte_sequence -> bool*)
let gnu_ext_check_elf64_abi_note_tag_section endian sht sect_hdr_tbl bs0:bool=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf64_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint64_wrapper.to_bigint note.elf64_sh_offset) in
        let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf64_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> false
            | Success abi_tag ->
              let str = (name_string_of_elf64_note abi_tag) in
                if str = "GNU\000" then
                  if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf64_note_descsz)( (Nat_big_num.of_int 16)) then Nat_big_num.greater_equal
                    (Byte_sequence.length0 abi_tag.elf64_note_desc)( (Nat_big_num.of_int 16))
                  else
                    false
                else
                  false
          )
      | _      ->
          false
    ))

(** [gnu_ext_extract_elf32_earliest_compatible_kernel end sht stab bs0] extracts
  * the earliest compatible Linux kernel with the given ELF file from its section
  * header table [sht], and string table [stbl], assuming endianness [endian].
  * NB: marked as OCaml only as need to extract a string from integers.
  * TODO: implement some string parsing functions in Isabelle/HOL so things like
  * this can be extracted.
  *)
(*val gnu_ext_extract_elf32_earliest_compatible_kernel : endianness -> elf32_section_header_table ->
  string_table -> byte_sequence -> error string*)
let gnu_ext_extract_elf32_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf32_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf32_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint32_wrapper.to_bigint note.elf32_sh_offset) in
        let siz = (Uint32_wrapper.to_bigint note.elf32_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf32_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: parsing of NOTE section failed"
            | Success abi_tag ->
              let str = (name_string_of_elf32_note abi_tag) in
                if str = "GNU\000" then
                if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf32_note_descsz)( (Nat_big_num.of_int 16)) then
                  (match Byte_sequence.takebytes( (Nat_big_num.of_int 16)) abi_tag.elf32_note_desc with
                    | Fail _ -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: the impossible happened"
                    | Success take2 ->
                      (match group_elf32_words endian (Byte_sequence.byte_list_of_byte_sequence take2) with
                        | Fail err   -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: word grouping failed"
                        | Success ss ->
                          (match ss with
                            | c1::c2::c3::cs ->
                              let c1 = (Uint32_wrapper.to_string c1) in
                              let c2 = (Uint32_wrapper.to_string c2) in
                              let c3 = (Uint32_wrapper.to_string c3) in
                                return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "")
                            | _              -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: kernel version must have three components"
                          )
                      )
                  )
                else
                  fail "gnu_ext_extract_elf32_earliest_compatible_kernel: .note.ABI-tag description size not required length"
                else
                  fail "gnu_ext_extract_elf32_earliest_compatible_kernel: required GNU string not present"
          )
      | _      -> fail "gnu_ext_extract_elf32_earliest_compatible_kernel: more than one .note.ABI-tag section present"
    ))

(** [gnu_ext_extract_elf64_earliest_compatible_kernel end sht stab bs0] extracts
  * the earliest compatible Linux kernel with the given ELF file from its section
  * header table [sht], and string table [stbl], assuming endianness [endian].
  * NB: marked as OCaml only as need to extract a string from integers.
  * TODO: implement some string parsing functions in Isabelle/HOL so things like
  * this can be extracted.
  *)
(*val gnu_ext_extract_elf64_earliest_compatible_kernel : endianness -> elf64_section_header_table ->
  string_table -> byte_sequence -> error string*)
let gnu_ext_extract_elf64_earliest_compatible_kernel endian sht sect_hdr_tbl bs0:(string)error=
   (let abi_note_sects =
    (List.filter (fun x ->
      if Nat_big_num.equal (Uint32_wrapper.to_bigint x.elf64_sh_type) sht_note then
        let nm = (Uint32_wrapper.to_bigint x.elf64_sh_name) in
          (match String_table.get_string_at nm sect_hdr_tbl with
            | Success name1 -> name1 = ".note.ABI-tag"
            | Fail _       -> false
          )
      else
        false
    ) sht)
  in
    (match abi_note_sects with
      | [note] ->
        let off = (Uint64_wrapper.to_bigint note.elf64_sh_offset) in
        let siz = (Ml_bindings.nat_big_num_of_uint64 note.elf64_sh_size) in
        let abi_tag = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (Elf_note.read_elf64_note endian rel) (fun (abi_tag, _) ->
          return abi_tag)))
        in
          (match abi_tag with
            | Fail _          -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: parsing of NOTE section failed"
            | Success abi_tag ->
              let str = (name_string_of_elf64_note abi_tag) in
                if str = "GNU\000" then
                  if Nat_big_num.greater_equal (Uint32_wrapper.to_bigint abi_tag.elf64_note_descsz)( (Nat_big_num.of_int 16)) then
                    (match Byte_sequence.takebytes( (Nat_big_num.of_int 16)) abi_tag.elf64_note_desc with
                      | Fail _ -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: the impossible happened"
                      | Success take2 ->
                        (match group_elf64_words endian (Byte_sequence.byte_list_of_byte_sequence take2) with
                          | Fail err   -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: word grouping failed"
                          | Success ss ->
                            (match ss with
                              | c1::c2::c3::cs ->
                                let c1 = (Uint32_wrapper.to_string c1) in
                                let c2 = (Uint32_wrapper.to_string c2) in
                                let c3 = (Uint32_wrapper.to_string c3) in
                                  return (List.fold_right (^) (intercalate "." [c1;c2;c3]) "")
                              | _              -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: kernel version must have three components"
                            )
                        )
                    )
                  else
                    fail "gnu_ext_extract_elf64_earliest_compatible_kernel: .note.ABI-tag description size not required length"
                else
                  fail "gnu_ext_extract_elf64_earliest_compatible_kernel: required GNU string not present"
          )
      | _      -> fail "gnu_ext_extract_elf64_earliest_compatible_kernel: more than one .note.ABI-tag section present"
    ))