(*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_sequence (** 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 && (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_sequence (** 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) compare_byte_sequence ([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 && (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 (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_name)) && (Nat_big_num.equal i.elf64_section_type (Nat_big_num.of_string (Uint32.to_string 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 (Nat_big_num.of_string (Uint64.to_string 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 (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_link)) && (Nat_big_num.equal i.elf64_section_info (Nat_big_num.of_string (Uint32.to_string 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)