Source file gnu_ext_section_header_table.ml

(*Generated by Lem from gnu_extensions/gnu_ext_section_header_table.lem.*)
(** The module [gnu_ext_section_header_table] implements function, definitions
  * and types relating to the GNU extensions to the standard ELF section header
  * table.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_map
open Lem_maybe
open Lem_num
open Lem_string

open Hex_printing

open Error
open String_table
open Show

open Elf_section_header_table
open Elf_interpreted_section

(** GNU extended section types *)

(** [GNU_HASH] does not appear to be defined in the LSB but is present in
  * several ELF binaries collected in the wild...
  *
  * TODO: find out where this comes from?
  * ANSW: a mailing list apparently!  See here:
  *   https://sourceware.org/ml/binutils/2006-10/msg00377.html
  *)
let sht_gnu_hash    : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524091)))     (* 0x6FFFFFF6 *)

(** The following are all defined in Section 10.2.2.2 of the LSB as additional
  * section types over the ones defined in the SCO ELF spec.
  *)

(** [sht_gnu_verdef] contains the symbol versions that are provided.
  *)
let sht_gnu_verdef  : Nat_big_num.num=  (Nat_big_num.sub_nat ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))( (Nat_big_num.of_int 1))) (* 0x6ffffffd *)
(** [sht_gnu_verneed] contains the symbol versions that are required.
  *)
let sht_gnu_verneed : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))     (* 0x6ffffffe *)
(** [sht_gnu_versym] contains the symbol version table.
  *)
let sht_gnu_versym  : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524095)))( (Nat_big_num.of_int 1))) (* 0x6fffffff *)
(** [sht_gnu_liblist] appears to be undocumented but appears in PowerPC 64 ELF
  * binaries in "the wild".
  *)
let sht_gnu_liblist : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 939524091)))( (Nat_big_num.of_int 1))) (* 0x6FFFFFF7 *)

(** [string_of_gnu_ext_section_type m] produces a string based representation of
  * GNU extension section type [m].
  *)
(*val string_of_gnu_ext_section_type : natural -> string*)
let string_of_gnu_ext_section_type i:string=
   (if Nat_big_num.equal i sht_gnu_hash then
    "GNU_HASH"
  else if Nat_big_num.equal i sht_gnu_verdef then
    "VERDEF"
  else if Nat_big_num.equal i sht_gnu_verneed then
    "VERNEED"
  else if Nat_big_num.equal i sht_gnu_versym then
    "VERSYM"
  else if Nat_big_num.equal i sht_gnu_liblist then
    "GNU_LIBLIST"
  else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then
    let diff = (Nat_big_num.sub_nat i sht_loos) in
    let suff = (unsafe_hex_string_of_natural 0 diff) in
      "LOOS+" ^ suff
  else
    "Invalid GNU EXT section type: " ^ Nat_big_num.to_string i)
    
(** [gnu_ext_additionall_special_sections] records additional section names that
  * map appear in GNU ELF binaries and their required associated types and
  * attributes.  See Section 10.3.1.1 of the LSB and the related map
  * [elf_special_sections] in [Elf_section_header_table] which records section
  * names and their required types and attributes that all ELF binaries share.
  *)
(*val gnu_ext_additional_special_sections : Map.map string (natural * natural)*)
let gnu_ext_additional_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map=
   (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [
    (".ctors", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".data.rel.ro", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".dtors", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".eh_frame", (sht_progbits, shf_alloc))
  ; (".eh_frame_hdr", (sht_progbits, shf_alloc))
  ; (".gcc_execpt_table", (sht_progbits, shf_alloc))
  ; (".gnu.version", (sht_gnu_versym, shf_alloc))
  ; (".gnu.version_d", (sht_gnu_verdef, shf_alloc))
  ; (".gnu.version_r", (sht_gnu_verneed, shf_alloc))
  ; (".got.plt", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".jcr", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
  ; (".note.ABI-tag", (sht_note, shf_alloc))
  ; (".stab", (sht_progbits, (Nat_big_num.of_int 0)))
  ; (".stabstr", (sht_strtab, (Nat_big_num.of_int 0)))
  ])
  
(** [is_valid_gnu_ext_elf32_section_header_table_entry scts stbl] checks whether
  * sections [scts] conforms with the contents of the special sections table.
  * Fails otherwise.
  *)
(*val is_valid_gnu_ext_elf32_section_header_table_entry : elf32_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf32_section_header_table_entry ent stbl:bool=
   ((match String_table.get_string_at ent.elf32_section_name stbl with
    | Fail    f    -> false
    | Success name1 ->
      (match Pmap.lookup name1 gnu_ext_additional_special_sections with
        | None           ->
            is_valid_elf32_section_header_table_entry ent stbl
        | Some (typ, flags) -> Nat_big_num.equal
            typ ent.elf32_section_type && Nat_big_num.equal flags ent.elf32_section_flags
      )
  ))
  
(** [is_valid_gnu_ext_elf32_section_header_table sht stbl] checks whether every
  * member of the section header table [sht] conforms with the special sections
  * table.
  *)
(*val is_valid_gnu_ext_elf32_section_header_table : list elf32_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf32_section_header_table ents stbl:bool=
   (List.for_all (fun x -> is_valid_gnu_ext_elf32_section_header_table_entry x stbl) ents)
  
(** [is_valid_gnu_ext_elf64_section_header_table_entry scts stbl] checks whether
  * sections [scts] conforms with the contents of the special sections table.
  * Fails otherwise.
  *)
(*val is_valid_gnu_ext_elf64_section_header_table_entry : elf64_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf64_section_header_table_entry ent stbl:bool=
   ((match String_table.get_string_at ent.elf64_section_name stbl with
    | Fail    f    -> false
    | Success name1 ->
      (match Pmap.lookup name1 gnu_ext_additional_special_sections with
        | None           ->
            is_valid_elf64_section_header_table_entry ent stbl
        | Some (typ, flags) -> Nat_big_num.equal
            typ ent.elf64_section_type && Nat_big_num.equal flags ent.elf64_section_flags
      )
  ))
  
(** [is_valid_gnu_ext_elf64_section_header_table sht stbl] checks whether every
  * member of the section header table [sht] conforms with the special sections
  * table.
  *)
(*val is_valid_gnu_ext_elf64_section_header_table : list elf64_interpreted_section ->
  string_table -> bool*)
let is_valid_gnu_ext_elf64_section_header_table ents stbl:bool=
   (List.for_all (fun x -> is_valid_gnu_ext_elf64_section_header_table_entry x stbl) ents)