package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/elf_interpreted_section.ml.html
Source file elf_interpreted_section.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
(*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)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>