diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_interpreted_section.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_interpreted_section.ml | 305 |
1 files changed, 0 insertions, 305 deletions
diff --git a/lib/ocaml_rts/linksem/elf_interpreted_section.ml b/lib/ocaml_rts/linksem/elf_interpreted_section.ml deleted file mode 100644 index 7fcf59b4..00000000 --- a/lib/ocaml_rts/linksem/elf_interpreted_section.ml +++ /dev/null @@ -1,305 +0,0 @@ -(*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) |