package linksem

You can search for identifiers within the package.

in-package search v0.2.0

A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

Maintainers

L

Linksem Devs <cl-linksem-dev@lists.cam.ac.uk>

Sources

md5=2075c56715539b3b8f54ae65cc808b8c

sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Gnu_ext_section_to_segment_mapping/index.html

Module `Gnu_ext_section_to_segment_mapping`Source

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.

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_flags0 : 
  Elf_section_header_table.elf32_section_header_table_entry ->
  Nat_big_num.num ->
  bool

val elf64_section_flags0 : 
  Elf_section_header_table.elf64_section_header_table_entry ->
  Nat_big_num.num ->
  bool

val elf32_section_of_type : 
  Elf_section_header_table.elf32_section_header_table_entry ->
  Nat_big_num.num ->
  bool

val elf64_section_of_type : 
  Elf_section_header_table.elf64_section_header_table_entry ->
  Nat_big_num.num ->
  bool

val elf32_segment_of_type : 
  Elf_program_header_table.elf32_program_header_table_entry ->
  Nat_big_num.num ->
  bool

val elf64_segment_of_type : 
  Elf_program_header_table.elf64_program_header_table_entry ->
  Nat_big_num.num ->
  bool

val elf32_section_in_segment1 : 
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  bool

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 elf64_section_in_segment1 : 
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  bool

PT_LOAD and similar segments only have SHF_ALLOC sections

val elf32_section_in_segment2 : 
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  bool

val elf64_section_in_segment2 : 
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  bool

Any section besides one of type SHT_NOBITS must have file offsets within * the segment.

val elf32_sect_size : 
  Elf_header.elf32_header ->
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  Nat_big_num.num

val elf64_sect_size : 
  Elf_header.elf64_header ->
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  Nat_big_num.num

val elf32_section_in_segment3 : 
  Elf_header.elf32_header ->
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  bool

val elf64_section_in_segment3 : 
  Elf_header.elf64_header ->
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  bool

SHF_ALLOC sections must have VMAs within the segment

val elf32_section_in_segment4 : 
  Elf_header.elf32_header ->
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  bool

val elf64_section_in_segment4 : 
  Elf_header.elf64_header ->
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  bool

No zero size sections at start or end of PT_DYNAMIC

val elf32_section_in_segment5 : 
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  bool

val elf64_section_in_segment5 : 
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  bool

The final section in segment tests, bringing all the above together.

val elf32_section_in_segment : 
  Elf_header.elf32_header ->
  Elf_section_header_table.elf32_section_header_table_entry ->
  Elf_program_header_table.elf32_program_header_table_entry ->
  bool

val elf64_section_in_segment : 
  Elf_header.elf64_header ->
  Elf_section_header_table.elf64_section_header_table_entry ->
  Elf_program_header_table.elf64_program_header_table_entry ->
  bool