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/gnu_ext_section_to_segment_mapping.ml.html
Source file gnu_ext_section_to_segment_mapping.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(*Generated by Lem from gnu_extensions/gnu_ext_section_to_segment_mapping.lem.*) (** [gnu_ext_section_to_segment_mapping] contains (GNU specific) functionality * relating to calculating the section to segment mapping for an ELF file. In * particular, the test over whether a section is inside a segment is ABI * specific. This module provides that test. *) open Lem_basic_classes open Lem_bool open Lem_num open Elf_header open Elf_program_header_table open Elf_section_header_table open Elf_types_native_uint open Lem_string open Show open Gnu_ext_program_header_table (** [elf32_section_in_segment sec_hdr segment] implements the * ELF_SECTION_IN_SEGMENT1 macro from readelf. Note the macro is always used * with [check_vma] and [strict] set to 1. * #define ELF_SECTION_IN_SEGMENT_1(sec_hdr, segment, check_vma, strict) \ ((/* Only PT_LOAD, PT_GNU_RELRO and PT_TLS segments can contain \ SHF_TLS sections. */ \ ((((sec_hdr)->sh_flags & SHF_TLS) != 0) \ && ((segment)->p_type == PT_TLS \ || (segment)->p_type == PT_GNU_RELRO \ || (segment)->p_type == PT_LOAD)) \ /* PT_TLS segment contains only SHF_TLS sections, PT_PHDR no \ sections at all. */ \ || (((sec_hdr)->sh_flags & SHF_TLS) == 0 \ && (segment)->p_type != PT_TLS \ && (segment)->p_type != PT_PHDR)) \ /* PT_LOAD and similar segments only have SHF_ALLOC sections. */ \ && !(((sec_hdr)->sh_flags & SHF_ALLOC) == 0 \ && ((segment)->p_type == PT_LOAD \ || (segment)->p_type == PT_DYNAMIC \ || (segment)->p_type == PT_GNU_EH_FRAME \ || (segment)->p_type == PT_GNU_RELRO \ || (segment)->p_type == PT_GNU_STACK)) \ /* Any section besides one of type SHT_NOBITS must have file \ offsets within the segment. */ \ && ((sec_hdr)->sh_type == SHT_NOBITS \ || ((bfd_vma) (sec_hdr)->sh_offset >= (segment)->p_offset \ && (!(strict) \ || ((sec_hdr)->sh_offset - (segment)->p_offset \ <= (segment)->p_filesz - 1)) \ && (((sec_hdr)->sh_offset - (segment)->p_offset \ + ELF_SECTION_SIZE(sec_hdr, segment)) \ <= (segment)->p_filesz))) \ /* SHF_ALLOC sections must have VMAs within the segment. */ \ && (!(check_vma) \ || ((sec_hdr)->sh_flags & SHF_ALLOC) == 0 \ || ((sec_hdr)->sh_addr >= (segment)->p_vaddr \ && (!(strict) \ || ((sec_hdr)->sh_addr - (segment)->p_vaddr \ <= (segment)->p_memsz - 1)) \ && (((sec_hdr)->sh_addr - (segment)->p_vaddr \ + ELF_SECTION_SIZE(sec_hdr, segment)) \ <= (segment)->p_memsz))) \ /* No zero size sections at start or end of PT_DYNAMIC. */ \ && ((segment)->p_type != PT_DYNAMIC \ || (sec_hdr)->sh_size != 0 \ || (segment)->p_memsz == 0 \ || (((sec_hdr)->sh_type == SHT_NOBITS \ || ((bfd_vma) (sec_hdr)->sh_offset > (segment)->p_offset \ && ((sec_hdr)->sh_offset - (segment)->p_offset \ < (segment)->p_filesz))) \ && (((sec_hdr)->sh_flags & SHF_ALLOC) == 0 \ || ((sec_hdr)->sh_addr > (segment)->p_vaddr \ && ((sec_hdr)->sh_addr - (segment)->p_vaddr \ < (segment)->p_memsz)))))) * * From [internal.h] of readelf's source code. *) (*val elf32_section_flags : elf32_section_header_table_entry -> natural -> bool*) let elf32_section_flags0 sec_hdr typ:bool= (not ((Uint32_wrapper.logand sec_hdr.elf32_sh_flags (Uint32_wrapper.of_bigint typ)) = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) (*val elf64_section_flags : elf64_section_header_table_entry -> natural -> bool*) let elf64_section_flags0 sec_hdr typ:bool= (not ((Uint64_wrapper.logand sec_hdr.elf64_sh_flags (Uint64_wrapper.of_bigint typ)) = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))))) (*val elf32_section_of_type : elf32_section_header_table_entry -> natural -> bool*) let elf32_section_of_type sec_hdr typ:bool= (sec_hdr.elf32_sh_type = Uint32_wrapper.of_bigint typ) (*val elf64_section_of_type : elf64_section_header_table_entry -> natural -> bool*) let elf64_section_of_type sec_hdr typ:bool= (sec_hdr.elf64_sh_type = Uint32_wrapper.of_bigint typ) (*val elf32_segment_of_type : elf32_program_header_table_entry -> natural -> bool*) let elf32_segment_of_type segment typ:bool= (segment.elf32_p_type = Uint32_wrapper.of_bigint typ) (*val elf64_segment_of_type : elf64_program_header_table_entry -> natural -> bool*) let elf64_segment_of_type segment typ:bool= (segment.elf64_p_type = Uint32_wrapper.of_bigint typ) (** Only PT_LOAD, PT_GNU_RELRO and PT_TLS segments can contain SHF_TLS sections * and PT_TLS segment contains only SHF_TLS sections, PT_PHDR no sections at all *) (*val elf32_section_in_segment1 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let elf32_section_in_segment1 sec_hdr segment:bool= ((elf32_section_flags0 sec_hdr shf_tls && (elf32_segment_of_type segment elf_pt_tls || (elf32_segment_of_type segment elf_pt_gnu_relro || elf32_segment_of_type segment elf_pt_load))) || (not (elf32_section_flags0 sec_hdr shf_tls) && (not (elf32_segment_of_type segment elf_pt_tls) && not (elf32_segment_of_type segment elf_pt_phdr)))) (*val elf64_section_in_segment1 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let elf64_section_in_segment1 sec_hdr segment:bool= ((elf64_section_flags0 sec_hdr shf_tls && (elf64_segment_of_type segment elf_pt_tls || (elf64_segment_of_type segment elf_pt_gnu_relro || elf64_segment_of_type segment elf_pt_load))) || (not (elf64_section_flags0 sec_hdr shf_tls) && (not (elf64_segment_of_type segment elf_pt_tls) && not (elf64_segment_of_type segment elf_pt_phdr)))) (** PT_LOAD and similar segments only have SHF_ALLOC sections *) (*val elf32_section_in_segment2 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let elf32_section_in_segment2 sec_hdr segment:bool= (not ((not (elf32_section_flags0 sec_hdr shf_alloc)) && (elf32_segment_of_type segment elf_pt_load || (elf32_segment_of_type segment elf_pt_dynamic || (elf32_segment_of_type segment elf_pt_gnu_eh_frame || (elf32_segment_of_type segment elf_pt_gnu_relro || elf32_segment_of_type segment elf_pt_gnu_stack)))))) (*val elf64_section_in_segment2 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let elf64_section_in_segment2 sec_hdr segment:bool= (not ((not (elf64_section_flags0 sec_hdr shf_alloc)) && (elf64_segment_of_type segment elf_pt_load || (elf64_segment_of_type segment elf_pt_dynamic || (elf64_segment_of_type segment elf_pt_gnu_eh_frame || (elf64_segment_of_type segment elf_pt_gnu_relro || elf64_segment_of_type segment elf_pt_gnu_stack)))))) (** Any section besides one of type SHT_NOBITS must have file offsets within * the segment. *) (*val elf32_sect_size : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> natural*) let elf32_sect_size hdr sec_hdr segment:Nat_big_num.num= (if is_elf32_tbss_special sec_hdr segment then (Nat_big_num.of_int 0) else Uint32_wrapper.to_bigint (hdr.elf32_shentsize)) (*val elf64_sect_size : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> natural*) let elf64_sect_size hdr sec_hdr segment:Nat_big_num.num= (if is_elf64_tbss_special sec_hdr segment then (Nat_big_num.of_int 0) else Uint32_wrapper.to_bigint (hdr.elf64_shentsize)) (*val elf32_section_in_segment3 : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let elf32_section_in_segment3 hdr sec_hdr segment:bool= (let sec_off = ((Uint32_wrapper.to_bigint sec_hdr.elf32_sh_offset)) in let seg_off = ((Uint32_wrapper.to_bigint segment.elf32_p_offset)) in let seg_fsz = ((Uint32_wrapper.to_bigint segment.elf32_p_filesz)) in let sec_siz = ((elf32_sect_size hdr sec_hdr segment)) in elf32_section_of_type sec_hdr sht_nobits || ( Nat_big_num.greater_equal sec_off seg_off && (( Nat_big_num.less_equal( Nat_big_num.sub sec_off seg_off) ( Nat_big_num.sub seg_fsz( (Nat_big_num.of_int 1)))) && ( Nat_big_num.less_equal (Nat_big_num.sub sec_off ( Nat_big_num.add seg_off sec_siz)) seg_fsz)))) (*val elf64_section_in_segment3 : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let elf64_section_in_segment3 hdr sec_hdr segment:bool= (let sec_off = ((Uint64_wrapper.to_bigint sec_hdr.elf64_sh_offset)) in let seg_off = ((Uint64_wrapper.to_bigint segment.elf64_p_offset)) in let seg_fsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_filesz)) in let sec_siz = ((elf64_sect_size hdr sec_hdr segment)) in elf64_section_of_type sec_hdr sht_nobits || ( Nat_big_num.greater_equal sec_off seg_off && (( Nat_big_num.less_equal( Nat_big_num.sub sec_off seg_off) ( Nat_big_num.sub seg_fsz( (Nat_big_num.of_int 1)))) && ( Nat_big_num.less_equal (Nat_big_num.sub sec_off ( Nat_big_num.add seg_off sec_siz)) seg_fsz)))) (** SHF_ALLOC sections must have VMAs within the segment *) (*val elf32_section_in_segment4 : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let elf32_section_in_segment4 hdr sec_hdr segment:bool= (let sec_addr = ((Uint32_wrapper.to_bigint sec_hdr.elf32_sh_addr)) in let seg_vadr = ((Uint32_wrapper.to_bigint segment.elf32_p_vaddr)) in let seg_mmsz = ((Uint32_wrapper.to_bigint segment.elf32_p_memsz)) in let sec_size = ((elf32_sect_size hdr sec_hdr segment)) in (not (elf32_section_flags0 sec_hdr shf_alloc) || Nat_big_num.greater_equal sec_addr seg_vadr) && (Nat_big_num.less_equal (Nat_big_num.sub sec_addr seg_vadr) (Nat_big_num.sub seg_mmsz( (Nat_big_num.of_int 1))) && Nat_big_num.less_equal (Nat_big_num.sub sec_addr ( Nat_big_num.add seg_vadr sec_size)) seg_mmsz)) (*val elf64_section_in_segment4 : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let elf64_section_in_segment4 hdr sec_hdr segment:bool= (let sec_addr = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_addr)) in let seg_vadr = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_vaddr)) in let seg_mmsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_memsz)) in let sec_size = ((elf64_sect_size hdr sec_hdr segment)) in (not (elf64_section_flags0 sec_hdr shf_alloc) || Nat_big_num.greater_equal sec_addr seg_vadr) && (Nat_big_num.less_equal (Nat_big_num.sub sec_addr seg_vadr) (Nat_big_num.sub seg_mmsz( (Nat_big_num.of_int 1))) && Nat_big_num.less_equal (Nat_big_num.sub sec_addr ( Nat_big_num.add seg_vadr sec_size)) seg_mmsz)) (** No zero size sections at start or end of PT_DYNAMIC *) (*val elf32_section_in_segment5 : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let elf32_section_in_segment5 sec_hdr segment:bool= (let sec_siz = ((Uint32_wrapper.to_bigint sec_hdr.elf32_sh_size)) in let seg_msz = ((Uint32_wrapper.to_bigint segment.elf32_p_memsz)) in let sec_off = ((Uint32_wrapper.to_bigint sec_hdr.elf32_sh_offset)) in let seg_off = ((Uint32_wrapper.to_bigint segment.elf32_p_offset)) in let seg_fsz = ((Uint32_wrapper.to_bigint segment.elf32_p_filesz)) in let sec_adr = ((Uint32_wrapper.to_bigint sec_hdr.elf32_sh_addr)) in let seg_vad = ((Uint32_wrapper.to_bigint segment.elf32_p_vaddr)) in (not (elf32_segment_of_type segment elf_pt_dynamic)) || (not (Nat_big_num.equal sec_siz( (Nat_big_num.of_int 0))) || (Nat_big_num.equal seg_msz( (Nat_big_num.of_int 0)) || ((elf32_section_of_type sec_hdr sht_nobits || ( Nat_big_num.greater sec_off seg_off && Nat_big_num.less (Nat_big_num.sub sec_off seg_off) seg_fsz)) && (not (elf32_section_flags0 sec_hdr shf_alloc) || ( Nat_big_num.greater sec_adr seg_vad && Nat_big_num.less (Nat_big_num.sub sec_adr seg_vad) seg_msz)))))) (*val elf64_section_in_segment5 : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let elf64_section_in_segment5 sec_hdr segment:bool= (let sec_siz = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_size)) in let seg_msz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_memsz)) in let sec_off = ((Uint64_wrapper.to_bigint sec_hdr.elf64_sh_offset)) in let seg_off = ((Uint64_wrapper.to_bigint segment.elf64_p_offset)) in let seg_fsz = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_filesz)) in let sec_adr = ((Ml_bindings.nat_big_num_of_uint64 sec_hdr.elf64_sh_addr)) in let seg_vad = ((Ml_bindings.nat_big_num_of_uint64 segment.elf64_p_vaddr)) in (not (elf64_segment_of_type segment elf_pt_dynamic)) || (not (Nat_big_num.equal sec_siz( (Nat_big_num.of_int 0))) || (Nat_big_num.equal seg_msz( (Nat_big_num.of_int 0)) || ((elf64_section_of_type sec_hdr sht_nobits || ( Nat_big_num.greater sec_off seg_off && Nat_big_num.less (Nat_big_num.sub sec_off seg_off) seg_fsz)) && (not (elf64_section_flags0 sec_hdr shf_alloc) || ( Nat_big_num.greater sec_adr seg_vad && Nat_big_num.less (Nat_big_num.sub sec_adr seg_vad) seg_msz)))))) (** The final section in segment tests, bringing all the above together. *) (*val elf32_section_in_segment : elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*) let elf32_section_in_segment hdr sec_hdr segment:bool= (elf32_section_in_segment1 sec_hdr segment && (elf32_section_in_segment2 sec_hdr segment && (elf32_section_in_segment3 hdr sec_hdr segment && (elf32_section_in_segment4 hdr sec_hdr segment && elf32_section_in_segment5 sec_hdr segment)))) (*val elf64_section_in_segment : elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*) let elf64_section_in_segment hdr sec_hdr segment:bool= (elf64_section_in_segment1 sec_hdr segment && (elf64_section_in_segment2 sec_hdr segment && (elf64_section_in_segment3 hdr sec_hdr segment && (elf64_section_in_segment4 hdr sec_hdr segment && elf64_section_in_segment5 sec_hdr segment))))