From befbc76f89f3d8abc8da17caf91ea4a87ec96eeb Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 28 Mar 2012 13:32:21 +0000 Subject: checklink: first import of Valentin Robert's validator for asm and link cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/ELF_parsers.ml | 322 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 322 insertions(+) create mode 100644 checklink/ELF_parsers.ml (limited to 'checklink/ELF_parsers.ml') diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml new file mode 100644 index 0000000..c71ff00 --- /dev/null +++ b/checklink/ELF_parsers.ml @@ -0,0 +1,322 @@ +open Bitstring_utils +open ELF_types +open ELF_printers +open ELF_utils +open Library +open PPC_parsers + +exception Unknown_endianness + +(** Converts an elf endian into a bitstring endian *) +let elfdata_to_endian (e: elfdata): Bitstring.endian = + match e with + | ELFDATA2LSB -> Bitstring.LittleEndian + | ELFDATA2MSB -> Bitstring.BigEndian + | _ -> raise Unknown_endianness + +(** Parses an elf32 header *) +let read_elf32_ehdr (bs: bitstring): elf32_ehdr = + bitmatch bs with + | { e_ident : 16*8 : bitstring ; + rest : -1 : bitstring } -> + ( + bitmatch e_ident with + | { 0x7F : 8 ; + "ELF" : 24 : string ; + ei_class : 8 : int ; + ei_data : 8 : int ; + ei_version : 8 : int ; + padding : 72 : bitstring } -> + assert (is_zeros padding 72); + let ei_data = ( + match ei_data with + | 0 -> ELFDATANONE + | 1 -> ELFDATA2LSB + | 2 -> ELFDATA2MSB + | _ -> ELFDATAUNKNOWN + ) + in + let e = elfdata_to_endian ei_data in + ( + bitmatch rest with + | { e_type : 16 : int, endian(e) ; + e_machine : 16 : int, endian(e) ; + e_version : 32 : int, endian(e) ; + e_entry : 32 : int, endian(e) ; + e_phoff : 32 : int, endian(e) ; + e_shoff : 32 : int, endian(e) ; + e_flags : 32 : bitstring ; + e_ehsize : 16 : int, endian(e) ; + e_phentsize : 16 : int, endian(e) ; + e_phnum : 16 : int, endian(e) ; + e_shentsize : 16 : int, endian(e) ; + e_shnum : 16 : int, endian(e) ; + e_shstrndx : 16 : int, endian(e) } -> + (* These shouldn't be different than this... *) + assert (e_ehsize = 52); + assert (e_phentsize = 32); + assert (e_shentsize = 40); + { + e_ident = + { + ei_class = ( + match ei_class with + | 0 -> ELFCLASSNONE + | 1 -> ELFCLASS32 + | 2 -> ELFCLASS64 + | _ -> ELFCLASSUNKNOWN + ); + ei_data = ei_data; + ei_version = ( + match ei_version with + | 0 -> EV_NONE + | 1 -> EV_CURRENT + | _ -> EV_UNKNOWN + ); + }; + e_type = ( + match e_type with + | 0 -> ET_NONE + | 1 -> ET_REL + | 2 -> ET_EXEC + | 3 -> ET_DYN + | 4 -> ET_CORE + | _ -> ET_UNKNOWN + ); + e_machine = ( + match e_machine with + | 0 -> EM_NONE + | 1 -> EM_M32 + | 2 -> EM_SPARC + | 3 -> EM_386 + | 4 -> EM_68K + | 5 -> EM_88K + | 7 -> EM_860 + | 8 -> EM_MIPS + | 10 -> EM_MIPS_RS4_BE + | 20 -> EM_PPC + | _ -> EM_UNKNOWN + ); + e_version = ( + match e_version with + | 0l -> EV_NONE + | 1l -> EV_CURRENT + | _ -> EV_UNKNOWN + ); + e_entry = e_entry; + e_phoff = e_phoff; + e_shoff = e_shoff; + e_flags = e_flags; + e_ehsize = e_ehsize; + e_phentsize = e_phentsize; + e_phnum = e_phnum; + e_shentsize = e_shentsize; + e_shnum = e_shnum; + e_shstrndx = e_shstrndx; + } + ) + ) + +(** Returns the file offset of the section header indexed *) +let section_header_offset (e_hdr: elf32_ehdr) (sndx: int): int = + int32_int e_hdr.e_shoff + sndx * e_hdr.e_shentsize + +(** Returns the ndx-th string in the provided bitstring, according to null + characters *) +let strtab_string (bs: bitstring) (ndx: int): string = + let (str, ofs, _) = bs in + let start = (ofs/8 + ndx) in + String.sub str start (String.index_from str start '\000' - start) + +(** Reads an ELF section header *) +let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) + (num: int): elf32_shdr = + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let byte_ofs = section_header_offset e_hdr num in + bitmatch bs with + | { sh_name : 32 : endian(e), offset(byte_ofs*8) ; + sh_type : 32 : endian(e) ; + sh_flags : 32 : endian(e) ; + sh_addr : 32 : endian(e) ; + sh_offset : 32 : endian(e) ; + sh_size : 32 : endian(e) ; + sh_link : 32 : endian(e) ; + sh_info : 32 : endian(e) ; + sh_addralign : 32 : endian(e) ; + sh_entsize : 32 : endian(e) } -> + { + sh_name = strtab_string strtab (int32_int sh_name); + sh_type = ( + match sh_type with + | 0l -> SHT_NULL + | 1l -> SHT_PROGBITS + | 2l -> SHT_SYMTAB + | 3l -> SHT_STRTAB + | 4l -> SHT_RELA + | 5l -> SHT_HASH + | 6l -> SHT_DYNAMIC + | 7l -> SHT_NOTE + | 8l -> SHT_NOBITS + | 9l -> SHT_REL + | 10l -> SHT_SHLIB + | 11l -> SHT_DYNSYM + | _ -> SHT_UNKNOWN + ); + sh_flags = sh_flags ; + sh_addr = sh_addr ; + sh_offset = sh_offset ; + sh_size = sh_size ; + sh_link = sh_link ; + sh_info = sh_info ; + sh_addralign = sh_addralign ; + sh_entsize = sh_entsize ; + } + +(** Reads an elf program header *) +let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) + : elf32_phdr = + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let phdr_ofs = int32_int e_hdr.e_phoff + ndx * e_hdr.e_phentsize in + bitmatch bs with + | { p_type : 32 : endian(e), offset(phdr_ofs*8) ; + p_offset : 32 : endian(e) ; + p_vaddr : 32 : endian(e) ; + p_paddr : 32 : endian(e) ; + p_filesz : 32 : endian(e) ; + p_memsz : 32 : endian(e) ; + p_flags : 32 : bitstring ; + p_align : 32 : endian(e) } -> + { + p_type = ( + match p_type with + | 0l -> PT_NULL + | 1l -> PT_LOAD + | 2l -> PT_DYNAMIC + | 3l -> PT_INTERP + | 4l -> PT_NOTE + | 5l -> PT_SHLIB + | 6l -> PT_PHDR + | _ -> PT_UNKNOWN + ); + p_offset = p_offset ; + p_vaddr = p_vaddr ; + p_paddr = p_paddr ; + p_filesz = p_filesz ; + p_memsz = p_memsz ; + p_flags = p_flags ; + p_align = p_align ; + } + +(** Reads an ELF symbol *) +let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) + (num: int): elf32_sym = + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + bitmatch symtab with + | { st_name : 32 : endian(e), offset(num*16*8) ; + st_value : 32 : endian(e) ; + st_size : 32 : endian(e) ; + st_bind : 4 ; + st_type : 4 ; + st_other : 8 ; + st_shndx : 16 : endian(e) } -> + { + st_name = strtab_string strtab (int32_int st_name) ; + st_value = st_value ; + st_size = st_size ; + st_bind = ( + match st_bind with + | 0 -> STB_LOCAL + | 1 -> STB_GLOBAL + | 2 -> STB_WEAK + | _ -> STB_UNKNOWN + ); + st_type = ( + match st_type with + | 0 -> STT_NOTYPE + | 1 -> STT_OBJECT + | 2 -> STT_FUNC + | 3 -> STT_SECTION + | 4 -> STT_FILE + | _ -> STT_UNKNOWN + ); + st_other = st_other ; + st_shndx = st_shndx ; + } + +(** Aborts if two sections overlap *) +let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit = + let intersect a asize b bsize = + asize <> 0l && bsize <> 0l && + ( + let last x xsize = Int32.(sub (add x xsize) 1l) in + let alast = last a asize in + let blast = last b bsize in + let within (a, b) x = (a <= x) && (x <= b) in + (within (a, alast) b) || (within (b, blast) a) + ) + in + Array.iteri + (fun i ai -> + if ai.sh_type <> SHT_NOBITS + then + let ai_intersects = intersect ai.sh_offset ai.sh_size in + if + ai_intersects 0l 52l (* ELF header *) + || ai_intersects ehdr.e_phoff + (int_int32 (ehdr.e_phnum * ehdr.e_phentsize)) + || ai_intersects ehdr.e_shoff + (int_int32 (ehdr.e_shnum * ehdr.e_shentsize)) + then assert false + else + Array.iteri + (fun j aj -> + if + i <> j + && aj.sh_type <> SHT_NOBITS + && ai_intersects aj.sh_offset aj.sh_size + then assert false + ) + shdra + ) + shdra + +(** Reads a whole ELF file from a bitstring *) +let read_elf_bs (bs: bitstring): elf = + let e_hdr = read_elf32_ehdr bs in + (* To initialize section names we need the string table *) + let strtab = ( + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let strtab_sndx = e_hdr.e_shstrndx in + let strtab_shofs = section_header_offset e_hdr strtab_sndx in + bitmatch bs with + | { ofs : 32 : endian(e), offset(strtab_shofs * 8 + 128) ; + size : 32 : endian(e) } -> + Bitstring.subbitstring bs (int32_int ofs * 8) (int32_int size * 8) + ) + in + let e_shdra = + Array.init e_hdr.e_shnum (read_elf32_shdr e_hdr bs strtab) + in + check_overlaps e_shdra e_hdr; + let symtab_sndx = section_ndx_by_name_noelf e_shdra ".symtab" in + { + e_bitstring = bs ; + e_hdr = e_hdr ; + e_shdra = e_shdra ; + e_phdra = Array.init e_hdr.e_phnum (read_elf32_phdr e_hdr bs) ; + e_symtab = ( + let symtab_shdr = e_shdra.(symtab_sndx) in + let symtab_strtab_sndx = symtab_shdr.sh_link in + let symtab_nb_ent = (int32_int symtab_shdr.sh_size / 16) in + Array.init symtab_nb_ent + (read_elf32_sym e_hdr + (section_bitstring_noelf bs e_shdra symtab_sndx) + (section_bitstring_noelf bs e_shdra (int32_int symtab_strtab_sndx))) + ); + e_symtab_sndx = symtab_sndx; + } + +(** Reads a whole ELF file from a file name *) +let read_elf (elffilename: string): elf = + let bs = Bitstring.bitstring_of_file elffilename in + read_elf_bs bs -- cgit v1.2.3