Added safety to potentially overflowing arithmetics

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 61 insertions, 56 deletions

diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml
index c71ff00..ba04c68 100644
--- a/checklink/ELF_parsers.ml
+++ b/checklink/ELF_parsers.ml
@@ -17,24 +17,24 @@ let elfdata_to_endian (e: elfdata): Bitstring.endian =
 (** Parses an elf32 header *)
 let read_elf32_ehdr (bs: bitstring): elf32_ehdr =
   bitmatch bs with
-  | { e_ident :   16*8    :   bitstring   ;
-      rest    :   -1      :   bitstring   } ->
+  | { 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 } ->
+        | { 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
+            let ei_data =
+              begin match ei_data with
               | 0 -> ELFDATANONE
               | 1 -> ELFDATA2LSB
               | 2 -> ELFDATA2MSB
               | _ -> ELFDATAUNKNOWN
-            )
+              end
             in
             let e = elfdata_to_endian ei_data in
             (
@@ -59,32 +59,32 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr =
                   {
                     e_ident =
                       {
-                        ei_class      = (
-                          match ei_class with
+                        ei_class      =
+                          begin match ei_class with
                           | 0 -> ELFCLASSNONE
                           | 1 -> ELFCLASS32
                           | 2 -> ELFCLASS64
                           | _ -> ELFCLASSUNKNOWN
-                        );
+                          end;
                         ei_data     = ei_data;
-                        ei_version  = (
-                          match ei_version with
+                        ei_version  =
+                          begin match ei_version with
                           | 0 -> EV_NONE
                           | 1 -> EV_CURRENT
                           | _ -> EV_UNKNOWN
-                        );
+                          end;
                       };
-                    e_type        = (
-                      match e_type with
+                    e_type        =
+                      begin 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
+                      end;
+                    e_machine     =
+                      begin match e_machine with
                       | 0  -> EM_NONE
                       | 1  -> EM_M32
                       | 2  -> EM_SPARC
@@ -96,13 +96,13 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr =
                       | 10 -> EM_MIPS_RS4_BE
                       | 20 -> EM_PPC
                       | _  -> EM_UNKNOWN
-                    );
-                    e_version     = (
-                      match e_version with
+                      end;
+                    e_version     =
+                      begin match e_version with
                       | 0l -> EV_NONE
                       | 1l -> EV_CURRENT
                       | _ -> EV_UNKNOWN
-                    );
+                      end;
                     e_entry     = e_entry;
                     e_phoff     = e_phoff;
                     e_shoff     = e_shoff;
@@ -119,22 +119,24 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr =
 
 (** 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
+  Safe.(of_int32 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
+  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
+  let bit_ofs = Safe.(
+    (section_header_offset e_hdr num) * 8
+  ) in
   bitmatch bs with
-  | { sh_name      : 32 : endian(e), offset(byte_ofs*8) ;
+  | { sh_name      : 32 : endian(e), offset(bit_ofs) ;
       sh_type      : 32 : endian(e) ;
       sh_flags     : 32 : endian(e) ;
       sh_addr      : 32 : endian(e) ;
@@ -145,9 +147,9 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring)
       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
+        sh_name         = strtab_string strtab (Safe32.to_int sh_name);
+        sh_type         =
+          begin match sh_type with
           |  0l -> SHT_NULL
           |  1l -> SHT_PROGBITS
           |  2l -> SHT_SYMTAB
@@ -161,7 +163,7 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring)
           | 10l -> SHT_SHLIB
           | 11l -> SHT_DYNSYM
           | _   -> SHT_UNKNOWN
-        );
+          end;
         sh_flags     = sh_flags     ;
         sh_addr      = sh_addr      ;
         sh_offset    = sh_offset    ;
@@ -173,12 +175,13 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring)
       }
 
 (** Reads an elf program header *)
-let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int)
-    : elf32_phdr =
+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
+  let bit_ofs = Safe.(
+    ((of_int32 e_hdr.e_phoff) + (ndx * e_hdr.e_phentsize)) * 8
+  ) in
   bitmatch bs with
-  | { p_type   : 32 : endian(e), offset(phdr_ofs*8) ;
+  | { p_type   : 32 : endian(e), offset(bit_ofs) ;
       p_offset : 32 : endian(e) ;
       p_vaddr  : 32 : endian(e) ;
       p_paddr  : 32 : endian(e) ;
@@ -187,8 +190,8 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int)
       p_flags  : 32 : bitstring ;
       p_align  : 32 : endian(e) } ->
       {
-        p_type      = (
-          match p_type with
+        p_type      =
+          begin match p_type with
           | 0l -> PT_NULL
           | 1l -> PT_LOAD
           | 2l -> PT_DYNAMIC
@@ -197,7 +200,7 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int)
           | 5l -> PT_SHLIB
           | 6l -> PT_PHDR
           | _  -> PT_UNKNOWN
-        );
+          end;
         p_offset = p_offset ;
         p_vaddr  = p_vaddr  ;
         p_paddr  = p_paddr  ;
@@ -211,8 +214,9 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int)
 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
+  let bit_ofs = Safe.(num * 128) in (* each symbol takes 16 bytes = 128 bits *)
   bitmatch symtab with
-  | { st_name  : 32 : endian(e), offset(num*16*8) ;
+  | { st_name  : 32 : endian(e), offset(bit_ofs) ;
       st_value : 32 : endian(e) ;
       st_size  : 32 : endian(e) ;
       st_bind  : 4 ;
@@ -220,30 +224,30 @@ let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring)
       st_other : 8 ;
       st_shndx : 16 : endian(e) } ->
       {
-        st_name  = strtab_string strtab (int32_int st_name) ;
+        st_name  = strtab_string strtab (Safe32.to_int st_name) ;
         st_value = st_value ;
         st_size  = st_size  ;
-        st_bind  = (
-          match st_bind with
+        st_bind  =
+          begin match st_bind with
           | 0 -> STB_LOCAL
           | 1 -> STB_GLOBAL
           | 2 -> STB_WEAK
           | _ -> STB_UNKNOWN
-        );
-        st_type     = (
-          match st_type with
+          end;
+        st_type  =
+          begin match st_type with
           | 0 -> STT_NOTYPE
           | 1 -> STT_OBJECT
           | 2 -> STT_FUNC
           | 3 -> STT_SECTION
           | 4 -> STT_FILE
           | _ -> STT_UNKNOWN
-        );
+          end;
         st_other = st_other ;
         st_shndx = st_shndx ;
       }
 
-(** Aborts if two sections overlap *)
+(** Abort 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 &&
@@ -263,9 +267,9 @@ let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit =
         if
           ai_intersects 0l 52l (* ELF header *)
           || ai_intersects ehdr.e_phoff
-            (int_int32 (ehdr.e_phnum * ehdr.e_phentsize))
+            (Int32.of_int (ehdr.e_phnum * ehdr.e_phentsize))
           || ai_intersects ehdr.e_shoff
-            (int_int32 (ehdr.e_shnum * ehdr.e_shentsize))
+            (Int32.of_int (ehdr.e_shnum * ehdr.e_shentsize))
         then assert false
         else
           Array.iteri
@@ -288,10 +292,11 @@ let read_elf_bs (bs: bitstring): elf =
     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
+    let skipped_bits = Safe.(strtab_shofs * 8 + 128) in
     bitmatch bs with
-    | { ofs  : 32 : endian(e), offset(strtab_shofs * 8 + 128) ;
+    | { ofs  : 32 : endian(e), offset(skipped_bits) ;
         size : 32 : endian(e) } ->
-        Bitstring.subbitstring bs (int32_int ofs * 8) (int32_int size * 8)
+        Bitstring.subbitstring bs Safe.(of_int32 ofs * 8) Safe.(of_int32 size * 8)
   )
   in
   let e_shdra =
@@ -307,11 +312,11 @@ let read_elf_bs (bs: bitstring): elf =
     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
+      let symtab_nb_ent = (Safe32.to_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)))
+           (section_bitstring_noelf bs e_shdra (Safe32.to_int symtab_strtab_sndx)))
     );
     e_symtab_sndx = symtab_sndx;
   }