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

1 files changed, 322 insertions, 0 deletions

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