Source file elf_interpreted_section.ml

(*Generated by Lem from elf_interpreted_section.lem.*)
(** Module [elf_interpreted_section] provides a record of "interpreted" sections,
  * i.e. the data stored in the section header table converted to more amenable
  * infinite precision types, and operation on those records.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string

open Byte_sequence
open Error
open String_table

open Elf_types_native_uint
open Elf_section_header_table

open Missing_pervasives
open Show

(** [elf32_interpreted_section] exactly mirrors the structure of a section header
  * table entry, barring the conversion of all fields to more amenable types.
  *)
type elf32_interpreted_section =
  { elf32_section_name    : Nat_big_num.num       (** Name of the section *)
   ; elf32_section_type    : Nat_big_num.num       (** Type of the section *)
   ; elf32_section_flags   : Nat_big_num.num       (** Flags associated with the section *)
   ; elf32_section_addr    : Nat_big_num.num       (** Base address of the section in memory *)
   ; elf32_section_offset  : Nat_big_num.num       (** Offset from beginning of file *)
   ; elf32_section_size    : Nat_big_num.num       (** Section size in bytes *)
   ; elf32_section_link    : Nat_big_num.num       (** Section header table index link *)
   ; elf32_section_info    : Nat_big_num.num       (** Extra information, depends on section type *)
   ; elf32_section_align   : Nat_big_num.num       (** Alignment constraints for section *)
   ; elf32_section_entsize : Nat_big_num.num       (** Size of each entry in table, if section is one *)
   ; elf32_section_body    : byte_sequence0 (** Body of section *)
   ; elf32_section_name_as_string : string (** Name of the section, as a string; "" for no name (name = 0) *)
   }
   
(** [elf32_interpreted_section_equal s1 s2] is an equality test on interpreted
  * sections [s1] and [s2].
  *)
(*val elf32_interpreted_section_equal : elf32_interpreted_section -> elf32_interpreted_section -> bool*)
let elf32_interpreted_section_equal x y:bool=  (Nat_big_num.equal
    x.elf32_section_name y.elf32_section_name && (Nat_big_num.equal
    x.elf32_section_type y.elf32_section_type && (Nat_big_num.equal
    x.elf32_section_flags y.elf32_section_flags && (Nat_big_num.equal
    x.elf32_section_addr y.elf32_section_addr && (Nat_big_num.equal
    x.elf32_section_offset y.elf32_section_offset && (Nat_big_num.equal
    x.elf32_section_size y.elf32_section_size && (Nat_big_num.equal
    x.elf32_section_link y.elf32_section_link && (Nat_big_num.equal
    x.elf32_section_info y.elf32_section_info && (Nat_big_num.equal
    x.elf32_section_align y.elf32_section_align && (Nat_big_num.equal
    x.elf32_section_entsize y.elf32_section_entsize && (Byte_sequence_wrapper.equal
    x.elf32_section_body y.elf32_section_body &&
    (x.elf32_section_name_as_string = y.elf32_section_name_as_string))))))))))))

let instance_Basic_classes_Eq_Elf_interpreted_section_elf32_interpreted_section_dict:(elf32_interpreted_section)eq_class= ({

  isEqual_method = elf32_interpreted_section_equal;

  isInequal_method = (fun x y->not (elf32_interpreted_section_equal x y))})

(** [elf64_interpreted_section] exactly mirrors the structure of a section header
  * table entry, barring the conversion of all fields to more amenable types.
  *)
type elf64_interpreted_section =
  { elf64_section_name    : Nat_big_num.num       (** Name of the section *)
   ; elf64_section_type    : Nat_big_num.num       (** Type of the section *)
   ; elf64_section_flags   : Nat_big_num.num       (** Flags associated with the section *)
   ; elf64_section_addr    : Nat_big_num.num       (** Base address of the section in memory *)
   ; elf64_section_offset  : Nat_big_num.num       (** Offset from beginning of file *)
   ; elf64_section_size    : Nat_big_num.num       (** Section size in bytes *)
   ; elf64_section_link    : Nat_big_num.num       (** Section header table index link *)
   ; elf64_section_info    : Nat_big_num.num       (** Extra information, depends on section type *)
   ; elf64_section_align   : Nat_big_num.num       (** Alignment constraints for section *)
   ; elf64_section_entsize : Nat_big_num.num       (** Size of each entry in table, if section is one *)
   ; elf64_section_body    : byte_sequence0 (** Body of section *)
   ; elf64_section_name_as_string : string (** Name of the section, as a string; "" for no name (name = 0) *)
   }

(** [compare_elf64_interpreted_section s1 s2] is an ordering comparison function
  * on interpreted sections suitable for use in sets, finite maps and other
  * ordered structures.
  *)
(*val compare_elf64_interpreted_section : elf64_interpreted_section -> elf64_interpreted_section ->
  ordering*)
let compare_elf64_interpreted_section s1 s2:int= 
    (pairCompare (lexicographic_compare Nat_big_num.compare) Byte_sequence_wrapper.compare 
    ([s1.elf64_section_name    ;
      s1.elf64_section_type    ;
      s1.elf64_section_flags   ;
      s1.elf64_section_addr    ;
      s1.elf64_section_offset  ;
      s1.elf64_section_size    ;
      s1.elf64_section_link    ;
      s1.elf64_section_info    ;
      s1.elf64_section_align   ;
      s1.elf64_section_entsize], s1.elf64_section_body)
    ([s2.elf64_section_name    ;
      s2.elf64_section_type    ;
      s2.elf64_section_flags   ;
      s2.elf64_section_addr    ;
      s2.elf64_section_offset  ;
      s2.elf64_section_size    ;
      s2.elf64_section_link    ;
      s2.elf64_section_info    ;
      s2.elf64_section_align   ;
      s2.elf64_section_entsize], s2.elf64_section_body))

let instance_Basic_classes_Ord_Elf_interpreted_section_elf64_interpreted_section_dict:(elf64_interpreted_section)ord_class= ({

  compare_method = compare_elf64_interpreted_section;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_section f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_interpreted_section f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_section f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_interpreted_section f1 f2)(Pset.from_list compare [1; 0])))})

(** [elf64_interpreted_section_equal s1 s2] is an equality test on interpreted
  * sections [s1] and [s2].
  *)
(*val elf64_interpreted_section_equal : elf64_interpreted_section -> elf64_interpreted_section -> bool*)
let elf64_interpreted_section_equal x y:bool=  (Nat_big_num.equal
    x.elf64_section_name y.elf64_section_name && (Nat_big_num.equal
    x.elf64_section_type y.elf64_section_type && (Nat_big_num.equal
    x.elf64_section_flags y.elf64_section_flags && (Nat_big_num.equal
    x.elf64_section_addr y.elf64_section_addr && (Nat_big_num.equal
    x.elf64_section_offset y.elf64_section_offset && (Nat_big_num.equal
    x.elf64_section_size y.elf64_section_size && (Nat_big_num.equal
    x.elf64_section_link y.elf64_section_link && (Nat_big_num.equal
    x.elf64_section_info y.elf64_section_info && (Nat_big_num.equal
    x.elf64_section_align y.elf64_section_align && (Nat_big_num.equal
    x.elf64_section_entsize y.elf64_section_entsize && (Byte_sequence_wrapper.equal
    x.elf64_section_body y.elf64_section_body &&
    (x.elf64_section_name_as_string = y.elf64_section_name_as_string))))))))))))

(** [null_elf32_interpreted_section] --- the null interpreted section.
  *)
(*val null_elf32_interpreted_section : elf32_interpreted_section*)
let null_elf32_interpreted_section:elf32_interpreted_section=
   ({ elf32_section_name =( (Nat_big_num.of_int 0))
   ; elf32_section_type =( (Nat_big_num.of_int 0))
   ; elf32_section_flags =( (Nat_big_num.of_int 0))
   ; elf32_section_addr =( (Nat_big_num.of_int 0))
   ; elf32_section_offset =( (Nat_big_num.of_int 0))
   ; elf32_section_size =( (Nat_big_num.of_int 0))
   ; elf32_section_link =( (Nat_big_num.of_int 0))
   ; elf32_section_info =( (Nat_big_num.of_int 0))
   ; elf32_section_align =( (Nat_big_num.of_int 0))
   ; elf32_section_entsize =( (Nat_big_num.of_int 0)) 
   ; elf32_section_body = Byte_sequence.empty
   ; elf32_section_name_as_string = ""
   })

(** [null_elf64_interpreted_section] --- the null interpreted section.
  *)
(*val null_elf64_interpreted_section : elf64_interpreted_section*)
let null_elf64_interpreted_section:elf64_interpreted_section=
   ({ elf64_section_name =( (Nat_big_num.of_int 0))
   ; elf64_section_type =( (Nat_big_num.of_int 0))
   ; elf64_section_flags =( (Nat_big_num.of_int 0))
   ; elf64_section_addr =( (Nat_big_num.of_int 0))
   ; elf64_section_offset =( (Nat_big_num.of_int 0))
   ; elf64_section_size =( (Nat_big_num.of_int 0))
   ; elf64_section_link =( (Nat_big_num.of_int 0))
   ; elf64_section_info =( (Nat_big_num.of_int 0))
   ; elf64_section_align =( (Nat_big_num.of_int 0))
   ; elf64_section_entsize =( (Nat_big_num.of_int 0)) 
   ; elf64_section_body = Byte_sequence.empty
   ; elf64_section_name_as_string = ""
   })

let instance_Basic_classes_Eq_Elf_interpreted_section_elf64_interpreted_section_dict:(elf64_interpreted_section)eq_class= ({

  isEqual_method = elf64_interpreted_section_equal;

  isInequal_method = (fun x y->not (elf64_interpreted_section_equal x y))})

(** [elf64_interpreted_section_matches_section_header sect ent] checks whether
  * the interpreted section and the corresponding section header table entry
  * match.
  *)
(*val elf64_interpreted_section_matches_section_header : 
    elf64_interpreted_section
        -> elf64_section_header_table_entry
            -> bool*)
let elf64_interpreted_section_matches_section_header i sh:bool=  (Nat_big_num.equal
  i.elf64_section_name (Uint32_wrapper.to_bigint sh.elf64_sh_name) && (Nat_big_num.equal
  i.elf64_section_type (Uint32_wrapper.to_bigint sh.elf64_sh_type) && (Nat_big_num.equal
  i.elf64_section_flags (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_flags) && (Nat_big_num.equal
  i.elf64_section_addr (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addr) && (Nat_big_num.equal
  i.elf64_section_offset (Uint64_wrapper.to_bigint sh.elf64_sh_offset) && (Nat_big_num.equal
  i.elf64_section_size (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) && (Nat_big_num.equal
  i.elf64_section_link (Uint32_wrapper.to_bigint sh.elf64_sh_link) && (Nat_big_num.equal
  i.elf64_section_info (Uint32_wrapper.to_bigint sh.elf64_sh_info) && (Nat_big_num.equal
  i.elf64_section_align (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addralign) (* WHY? *) && Nat_big_num.equal
  i.elf64_section_entsize (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_entsize))))))))))
  (* Don't compare the name as a string, because it's implied by the shshtrtab index. *)
  (* NOTE that we can have multiple sections *indistinguishable*
   * except by their section header table index. Imagine 
   * multiple zero-size bss sections at the same address with the same name.
   * That's why in elf_memory_image we always label each ElfSection
   * with its SHT index.
   *)

type elf32_interpreted_sections = elf32_interpreted_section list
type elf64_interpreted_sections = elf64_interpreted_section list

(** [string_of_elf32_interpreted_section sect] returns a string-based representation
  * of interpreted section, [sect].
  *)
(*val string_of_elf32_interpreted_section : elf32_interpreted_section -> string*)
let string_of_elf32_interpreted_section is:string=
    (unlines [
     ("Name: " ^ (is.elf32_section_name_as_string ^ ("(" ^ ((Nat_big_num.to_string is.elf32_section_name) ^ ")"))))
   ; ("Type: " ^ Nat_big_num.to_string is.elf32_section_type) 
   ; ("Flags: " ^ Nat_big_num.to_string is.elf32_section_type)
   ; ("Base address: " ^ Nat_big_num.to_string is.elf32_section_addr)
   ; ("Section offset: " ^ Nat_big_num.to_string is.elf32_section_offset)
   ; ("Section size: " ^ Nat_big_num.to_string is.elf32_section_size)
   ; ("Link: " ^ Nat_big_num.to_string is.elf32_section_link)
   ; ("Info: " ^ Nat_big_num.to_string is.elf32_section_info)
   ; ("Section alignment: " ^ Nat_big_num.to_string is.elf32_section_align)
   ; ("Entry size: " ^ Nat_big_num.to_string is.elf32_section_entsize)
   ])

(** [string_of_elf64_interpreted_section sect] returns a string-based representation
  * of interpreted section, [sect].
  *)
(*val string_of_elf64_interpreted_section : elf64_interpreted_section -> string*)
let string_of_elf64_interpreted_section is:string=
    (unlines [
     ("Name: " ^ (is.elf64_section_name_as_string ^ ("(" ^ ((Nat_big_num.to_string is.elf64_section_name) ^ ")"))))
   ; ("Type: " ^ Nat_big_num.to_string is.elf64_section_type) 
   ; ("Flags: " ^ Nat_big_num.to_string is.elf64_section_type)
   ; ("Base address: " ^ Nat_big_num.to_string is.elf64_section_addr)
   ; ("Section offset: " ^ Nat_big_num.to_string is.elf64_section_offset)
   ; ("Section size: " ^ Nat_big_num.to_string is.elf64_section_size)
   ; ("Link: " ^ Nat_big_num.to_string is.elf64_section_link)
   ; ("Info: " ^ Nat_big_num.to_string is.elf64_section_info)
   ; ("Section alignment: " ^ Nat_big_num.to_string is.elf64_section_align)
   ; ("Entry size: " ^ Nat_big_num.to_string is.elf64_section_entsize)
   ])
   
(** [is_valid_elf32_section_header_table_entry sect stab] checks whether a
  * interpreted section conforms with the prescribed flags and types declared
  * in the "special sections" table of the ELF specification.
  * TODO: some of these entries in the table are overridden by ABI supplements.
  * Make sure it is these that are passed in rather than the default table
  * declared in the spec?
  *)
(*val is_valid_elf32_section_header_table_entry : elf32_interpreted_section ->
  string_table -> bool*)
let is_valid_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 elf_special_sections with
        | None           -> false (* ??? *)
        | Some (typ, flags) -> Nat_big_num.equal
            typ ent.elf32_section_type && Nat_big_num.equal flags ent.elf32_section_flags
      )
  ))
  
(** [is_valid_elf64_section_header_table_entry sect stab] checks whether a
  * interpreted section conforms with the prescribed flags and types declared
  * in the "special sections" table of the ELF specification.
  * TODO: some of these entries in the table are overridden by ABI supplements.
  * Make sure it is these that are passed in rather than the default table
  * declared in the spec?
  *)  
(*val is_valid_elf64_section_header_table_entry : elf64_interpreted_section ->
  string_table -> bool*)
let is_valid_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 elf_special_sections with
        | None           -> false (* ??? *)
        | Some (typ, flags) -> Nat_big_num.equal
            typ ent.elf64_section_type && Nat_big_num.equal flags ent.elf64_section_flags
      )
  ))
  
(** [is_valid_elf32_section_header_table sects] checks whether all entries in
  * [sect] are valid.
  *)
(*val is_valid_elf32_section_header_table : list elf32_interpreted_section ->
  string_table -> bool*)
let is_valid_elf32_section_header_table0 ents stbl:bool=
   (List.for_all (fun x -> is_valid_elf32_section_header_table_entry x stbl) ents)
  
(** [is_valid_elf64_section_header_table sects] checks whether all entries in
  * [sect] are valid.
  *)
(*val is_valid_elf64_section_header_table : list elf64_interpreted_section ->
  string_table -> bool*)
let is_valid_elf64_section_header_table0 ents stbl:bool=
   (List.for_all (fun x -> is_valid_elf64_section_header_table_entry x stbl) ents)