path: root/src/elf_model/elf_section_header.ml

(*Generated by Lem from elf_section_header.lem.*)
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_string

open Bitstring
open Error
open Elf_types
open Show

(** Special section indices. *)

(** [shn_undef]: marks an undefined, missing or irrelevant section reference.
  *)
let shn_undef : int =( 0)
(** [shn_loreserve]: this specifies the lower bound of the range of reserved
  * indices.
  *)
let shn_loreserve : int =( 65280) (* 0xff00 *)
(** [shn_loproc]: start of the range reserved for processor-specific semantics.
  *)
let shn_loproc : int =( 65280) (* 0xff00 *)
(** [shn_hiproc]: end of the range reserved for processor-specific semantics.
  *)
let shn_hiproc : int =( 65311) (* 0xff1f *)
(** [shn_loos]: start of the range reserved for operating system-specific
  * semantics.
  *)
let shn_loos : int =( 65312) (* 0xff20 *)
(** [shn_hios]: end of the range reserved for operating system-specific
  * semantics.
  *)
let shn_hios : int =( 65343) (* 0xff3f *)
(** [shn_abs]: specifies the absolute values for the corresponding reference.
  * Symbols defined relative to section number [shn_abs] have absolute values
  * and are not affected by relocation.
  *)
let shn_abs : int =( 65521) (* 0xfff1 *)
(** [shn_common]: symbols defined relative to this index are common symbols,
  * such as unallocated C external variables.
  *)
let shn_common : int =( 65522) (* 0xfff2 *)
(** [shn_xindex]: an escape value.  It indicates the actual section header index
  * is too large to fit in the containing field and is located in another
  * location (specific to the structure where it appears).
  *)
let shn_xindex : int =( 65535) (* 0xffff *)
(** [shn_hireserve]: specifies the upper-bound of reserved values.
  *)
let shn_hireserve : int =( 65535) (* 0xffff *)

(*val string_of_special_section_index : nat -> string*)
let string_of_special_section_index i =  
(if i = shn_undef then
    "SHN_UNDEF"
  else if i = shn_loreserve then
    "SHN_LORESERVE"
  else if (i >= shn_loproc) && (i <= shn_hiproc) then
    "SHN_PROCESSOR_SPECIFIC"
  else if (i >= shn_loos) && (i <= shn_hios) then
    "SHN_OS_SPECIFIC"
  else if i = shn_abs then
    "SHN_ABS"
  else if i = shn_common then
    "SHN_COMMON"
  else if i = shn_xindex then
    "SHN_XINDEX"
  else if i = shn_hireserve then
    "SHN_HIRESERVE"
  else
  	"SHN UNDEFINED")

(** Section types. *)

(** Marks the section header as being inactive. *)
let sht_null : int =( 0)
(** Section holds information defined by the program. *)
let sht_progbits : int =( 1)
(** The following two section types hold a symbol table.  An object file may only
  * have one symbol table of each of the respective types.  The symtab provides
  * a place for link editing, whereas the dynsym section holds a minimal set of
  * dynamic linking symbols
  *)
let sht_symtab : int =( 2)
let sht_dynsym : int =( 11)
(** Section holds a string table *)
let sht_strtab : int =( 3)
(** Section holds relocation entries with explicit addends.  An object file may
  * have multiple section of this type.
  *)
let sht_rela : int =( 4)
(** Section holds a symbol hash table.  An object file may only have a single
  * hash table.
  *)
let sht_hash : int =( 5)
(** Section holds information for dynamic linking.  An object file may only have
  * a single dynamic section.
  *)
let sht_dynamic : int =( 6)
(** Section holds information that marks the file in some way. *)
let sht_note : int =( 7)
(** Section occupies no space in the file but otherwise resembles a progbits
  * section.
  *)
let sht_nobits : int =( 8)
(** Section holds relocation entries without explicit addends.  An object file
  * may have multiple section of this type.
  *)
let sht_rel : int =( 9)
(** Section type is reserved but has an unspecified meaning. *)
let sht_shlib : int =( 10)
(** Section contains an array of pointers to initialisation functions.  Each
  * pointer is taken as a parameterless function with a void return type.
  *)
let sht_init_array : int =( 14)
(** Section contains an array of pointers to termination functions.  Each
  * pointer is taken as a parameterless function with a void return type.
  *)
let sht_fini_array : int =( 15)
(** Section contains an array of pointers to initialisation functions that are
  * invoked before all other initialisation functions.  Each
  * pointer is taken as a parameterless function with a void return type.
  *)
let sht_preinit_array : int =( 16)
(** Section defines a section group, i.e. a set of sections that are related and
  * must be treated especially by the linker.  May only appear in relocatable
  * objects.
  *)
let sht_group : int =( 17)
(** Section is associated with sections of type SHT_SYMTAB and is required if
  * any of the section header indices referenced by that symbol table contains
  * the escape value SHN_XINDEX.
  *)
let sht_symtab_shndx : int =( 18)
(** XXX: broken for the time being due to Lem bug. *)
let sht_loos : int =( 0)
let sht_hios : int =( 0)
let sht_loproc : int =( 0)
let sht_hiproc : int =( 0)
let sht_louser : int =( 0)
let sht_hiuser : int =( 0)
(* XXX: constants too big for Lem to parse, apparently!
let sht_loos : nat = 1610612736 (* 0x60000000 *)
let sht_hios : nat = 1879048191 (* 0x6fffffff *)
let sht_loproc : nat = 1879048192 (* 0x70000000 *)
let sht_hiproc : nat = 2147483647 (* 0x7fffffff *)
let sht_louser : nat = 2147483648 (* 0x80000000 *)
let sht_hiuser : nat = 2415919103 (* 0x8fffffff *)
*)

let string_of_section_type i =  
(if i = sht_null then
    "SHT_NULL"
  else if i = sht_progbits then
    "SHT_PROGBITS"
  else if i = sht_symtab then
    "SHT_SYMTAB"
  else if i = sht_strtab then
    "SHT_STRTAB"
  else if i = sht_rela then
    "SHT_RELA"
  else if i = sht_hash then
    "SHT_HASH"
  else if i = sht_dynamic then
    "SHT_DYNAMIC"
  else if i = sht_note then
    "SHT_NOTE"
  else if i = sht_nobits then
    "SHT_NOBITS"
  else if i = sht_rel then
    "SHT_REL"
  else if i = sht_shlib then
    "SHT_SHLIB"
  else if i = sht_dynsym then
    "SHT_DYNSYM"
  else if i = sht_init_array then
    "SHT_INIT_ARRAY"
  else if i = sht_fini_array then
    "SHT_FINI_ARRAY"
  else if i = sht_preinit_array then
    "SHT_PREINIT_ARRAY"
  else if i = sht_group then
    "SHT_GROUP"
  else if i = sht_symtab_shndx then
    "SHT_SYMTAB_SHNDX"
  else if (i >= sht_loos) && (i <= sht_hios) then
    "SHT_OS_SPECIFIC"  
  else if (i >= sht_loproc) && (i <= sht_hiproc) then
    "SHT_PROCESSOR_SPECIFIC"
  else if (i >= sht_louser) && (i <= sht_hiuser) then
    "SHT_USER_SPECIFIC"
  else
    "SHT UNDEFINED")

(** Section header table entry type. *)

type elf32_section_header_table_entry =
  { elf32_sh_name      : Int64.t
   ; elf32_sh_type      : Int64.t
   ; elf32_sh_flags     : Int64.t
   ; elf32_sh_addr      : Int64.t
   ; elf32_sh_offset    : Int64.t
   ; elf32_sh_size      : Int64.t
   ; elf32_sh_link      : Int64.t
   ; elf32_sh_info      : Int64.t
   ; elf32_sh_addralign : Int64.t
   ; elf32_sh_entsize   : Int64.t
   }

let read_elf32_section_header_table_entry (bs : Bitstring.bitstring) =	
(Ml_bindings.read_elf32_word bs >>= (fun (sh_name, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_type, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_flags, bs) ->
	Ml_bindings.read_elf32_addr bs >>= (fun (sh_addr, bs) ->
	Ml_bindings.read_elf32_off bs >>= (fun (sh_offset, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_size, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_link, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_info, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_addralign, bs) ->
	Ml_bindings.read_elf32_word bs >>= (fun (sh_entsize, bs) ->
		return
			{ elf32_sh_name = sh_name
			 ; elf32_sh_type = sh_type
			 ; elf32_sh_flags = sh_flags
			 ; elf32_sh_addr = sh_addr
			 ; elf32_sh_offset = sh_offset
			 ; elf32_sh_size = sh_size
			 ; elf32_sh_link = sh_link
			 ; elf32_sh_info = sh_info
			 ; elf32_sh_addralign = sh_addralign
			 ; elf32_sh_entsize = sh_entsize
			 })))))))))))

let string_of_elf32_section_header_table_entry entry =  
(List.fold_right (^) [
    "\t"; "Name: "; Int64.to_string entry.elf32_sh_name
  ; "\t"; "Type: "; string_of_section_type (Int64.to_int entry.elf32_sh_type)
  ; "\n\t"; "Flags: "; Int64.to_string entry.elf32_sh_flags
  ; "\t"; "Address: "; Int64.to_string entry.elf32_sh_addr
  ; "\t"; "Size: "; Int64.to_string entry.elf32_sh_size; "\n\n"
  ] "")
  
let instance_Show_Show_Elf_section_header_elf32_section_header_table_entry_dict =({

  show_method = string_of_elf32_section_header_table_entry})

(** Section header table type. *)

type elf32_section_header_table = elf32_section_header_table_entry list
;;

let rec read_elf32_section_header_table' entry_size bitstring0 =  
(if Bitstring.bitstring_length bitstring0 = 0 then
    return []
  else
    let (eat, rest) = (Utility.partition_bitstring entry_size bitstring0) in
      read_elf32_section_header_table_entry eat >>= (fun sect ->
      read_elf32_section_header_table' entry_size rest     >>= (fun tail ->
      return (sect::tail))))

(*val read_elf32_section_header_table : nat -> nat -> nat -> bitstring -> error (elf32_section_header_table * bitstring)*)
let read_elf32_section_header_table size entry_size offset bitstring0 =	
(let (prefix, relevant) = (Utility.partition_bitstring offset bitstring0) in
  let (eat, rest) = (Utility.partition_bitstring (size * entry_size) relevant) in
  	read_elf32_section_header_table' entry_size eat >>= (fun entries ->
    return (entries, rest)))
;;

(*val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool*)
let elf32_size_correct hdr tbl =  
((match Int64.to_int hdr.elf32_sh_size with
    | 0 -> true
    | m -> m = List.length tbl
  ))
;;

(*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*)
let is_valid_elf32_section_header_table tbl =  
((match tbl with
    | []    -> false
    | x::xs ->        
(Int64.to_int x.elf32_sh_name = 0) &&
        ((Int64.to_int x.elf32_sh_type = sht_null) &&
        ((Int64.to_int x.elf32_sh_flags = 0) &&
        ((Int64.to_int x.elf32_sh_addr = 0) &&
        ((Int64.to_int x.elf32_sh_offset = 0) &&
        ((Int64.to_int x.elf32_sh_info = 0) &&
        ((Int64.to_int x.elf32_sh_addralign = 0) &&
        ((Int64.to_int x.elf32_sh_entsize = 0) &&
        elf32_size_correct x tbl)))))))
        (* XXX: more correctness criteria in time *)
  ))
  
let string_of_elf32_section_header_table (tbl : elf32_section_header_table) : string =	
("Section header table:" ^ ("\n" ^
		List.fold_right (^) (List.map string_of_elf32_section_header_table_entry tbl) ""))