Added safety to potentially overflowing arithmetics

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

10 files changed, 206 insertions, 151 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 33914f2..be56fe0 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -129,7 +129,7 @@ let check_fun_symtab
   let symtab_ent_start =
     Int32.(add
              elf.e_shdra.(symtab_sndx).sh_offset
-             (int_int32 (16 * sym_ndx))) in
+             (Safe32.of_int (16 * sym_ndx))) in
   let sym = sfw.ef.elf.e_symtab.(sym_ndx) in
   let atom = Hashtbl.find sfw.atoms ident in
   let section =
@@ -160,7 +160,7 @@ let check_fun_symtab
 (** Checks that the offset [ofs] is well aligned with regards to [al], expressed
     in bytes. *)
 let is_well_aligned (ofs: int32) (al: int): bool =
-  al = 0 || Int32.rem ofs (int_int32 al) = 0l
+  al = 0 || Int32.rem ofs (Safe32.of_int al) = 0l
 
 (** Adds a function symbol to the set of covered symbols. *)
 let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework =
@@ -201,7 +201,7 @@ let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$"
     out all symbols whose virtual address does not match [vaddr].
 *)
 let idmap_unify
-    (k: positive) (vaddr: int32) (sfw: s_framework): s_framework on_success =
+    (k: positive) (vaddr: int32) (sfw: s_framework): s_framework or_err =
   try (
     let id_ndxes = PosMap.find k sfw.ident_to_sym_ndx in
     match List.filter
@@ -260,7 +260,7 @@ let idmap_unify
     Subsequent references to the label will have to conform.
 *)
 let lblmap_unify (k: label) (v: int32) (ffw: f_framework)
-    : f_framework on_success =
+    : f_framework or_err =
   try (
     let v' = PosMap.find k ffw.label_to_vaddr in
     if v = v'
@@ -408,7 +408,7 @@ let match_z_int32 (cz: coq_Z) (ei: int32) =
   check_eq "match_z_int32" (z_int32 cz) ei
 
 let match_z_int (cz: coq_Z) (ei: int) =
-  check_eq "match_z_int" (z_int32 cz) (int_int32 ei)
+  check_eq "match_z_int" (z_int32 cz) (Safe32.of_int ei)
 
 (* [m] is interpreted as a bitmask, and checked against [ei]. *)
 let match_mask (m: coq_Z) (ei: int32) =
@@ -544,7 +544,7 @@ let rec match_jmptbl lbllist vaddr size ffw =
       )
       >>> match_jmptbl_aux lbllist bs
       >>? (ff_ef ^%=
-          add_range ofs (int_int32 (size / 8)) 0 Jumptable)
+          add_range ofs (Safe32.of_int (size / 8)) 0 Jumptable)
 
 (** Matches [ecode] agains the expected code for a small memory copy
     pseudo-instruction. Returns a triple containing the updated framework,
@@ -553,7 +553,7 @@ let rec match_jmptbl lbllist vaddr size ffw =
 let match_memcpy_small ecode pc sz al src dst (fw: f_framework)
     : (f_framework * ecode * int32) option =
   let rec match_memcpy_small_aux ofs sz ecode pc (fw: f_framework) =
-    let ofs32 = int_int32 ofs in
+    let ofs32 = Safe32.of_int ofs in
     if sz >= 8 && al >= 4
     then (
       match ecode with
@@ -632,7 +632,7 @@ let match_memcpy_big ecode pc sz al src dst fw
       STWU (rS5, rA5, d5)              :: (*           | *)
       BCx  (bo6,  bi6,  bd6, aa6, lk6) :: (* pc + 24 --  *)
       es ->
-      let sz' = int_int32 (sz / 4) in
+      let sz' = Safe32.of_int (sz / 4) in
       let (s, d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in
       let target_vaddr = Int32.(add 16l pc) in
       let dest_vaddr = Int32.(add (add 24l pc) (mul 4l (exts bd6))) in
@@ -723,7 +723,7 @@ let match_memcpy_big ecode pc sz al src dst fw
 (** Compares a whole CompCert function code against an ELF code, starting at
     program counter [pc].
 *)
-let rec compare_code ccode ecode pc fw: f_framework on_success =
+let rec compare_code ccode ecode pc fw: f_framework or_err =
   let error = ERR("Non-matching instructions") in
   match ccode, ecode with
   | [], []        -> OK(fw)
@@ -790,7 +790,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rD
               >>> match_iregs r1  rA
-              >>> match_csts  cst (int_int32 simm)
+              >>> match_csts  cst (Safe32.of_int simm)
               >>> recur_simpl
           | _ -> error
           end
@@ -851,7 +851,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rA
               >>> match_iregs r1  rS
-              >>> match_csts  cst (int_int32 uimm)
+              >>> match_csts  cst (Safe32.of_int uimm)
               >>> recur_simpl
           | _ -> error
           end
@@ -861,7 +861,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rA
               >>> match_iregs r1  rS
-              >>> match_csts  cst (int_int32 uimm)
+              >>> match_csts  cst (Safe32.of_int uimm)
               >>> recur_simpl
           | _ -> error
           end
@@ -984,7 +984,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               MTSPR (rS2, spr2)       ::
               BCCTRx(bo3, bi3, rc3)   :: es ->
               let tblvaddr = Int32.(
-                add (shift_left (int_int32 simm0) 16) (exts d1)
+                add (shift_left (Safe32.of_int simm0) 16) (exts d1)
               ) in
               let tblsize = (32 * List.length table) in
               fw
@@ -1260,7 +1260,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
                   fw
                   >>> match_iregs  GPR11 rD
                   >>> match_iregs  GPR0  rA
-                  >>> match_csts   high  (int_int32 simm)
+                  >>> match_csts   high  (Safe32.of_int simm)
                   >>> check_builtin_vload_common
                     cs es (Int32.add pc 4l) chunk GPR11
                     (Csymbol_low(ident, ofs)) res
@@ -1280,7 +1280,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
                       fw
                       >>> match_iregs  tmp   rD
                       >>> match_iregs  GPR0  rA
-                      >>> match_csts   high  (int_int32 simm)
+                      >>> match_csts   high  (Safe32.of_int simm)
                       >>> check_builtin_vstore_common
                         cs es (Int32.add pc 4l) chunk tmp
                         (Csymbol_low(ident, ofs)) src
@@ -1358,7 +1358,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
           | CMPLI(crfD, l, rA, uimm) :: es ->
               fw
               >>> match_iregs  r1      rA
-              >>> match_csts   cst     (int_int32 uimm)
+              >>> match_csts   cst     (Safe32.of_int uimm)
               >>> match_crbits CRbit_0 crfD
               >>> match_bools  false   l
               >>> recur_simpl
@@ -1699,7 +1699,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
           |   ADDIS(rD0, rA0, simm0) ::
               LFD  (frD1, rA1, d1)   :: es ->
               let vaddr = Int32.(
-                add (shift_left (int_int32 simm0) 16) (exts d1)
+                add (shift_left (Safe32.of_int simm0) 16) (exts d1)
               ) in
               if Int32.rem vaddr 8l <> 0l
               then ERR("Float constants should be 8-byte aligned")
@@ -1892,7 +1892,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rA
               >>> match_iregs r1  rS
-              >>> match_csts  cst (int_int32 uimm)
+              >>> match_csts  cst (Safe32.of_int uimm)
               >>> recur_simpl
           | _ -> error
           end
@@ -1902,7 +1902,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rA
               >>> match_iregs r1  rS
-              >>> match_csts  cst (int_int32 uimm)
+              >>> match_csts  cst (Safe32.of_int uimm)
               >>> recur_simpl
           | _ -> error
           end
@@ -2133,7 +2133,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rA
               >>> match_iregs r1  rS
-              >>> match_csts  cst (int_int32 uimm)
+              >>> match_csts  cst (Safe32.of_int uimm)
               >>> recur_simpl
           | _ -> error
           end
@@ -2143,7 +2143,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
               fw
               >>> match_iregs rd  rA
               >>> match_iregs r1  rS
-              >>> match_csts  cst (int_int32 uimm)
+              >>> match_csts  cst (Safe32.of_int uimm)
               >>> recur_simpl
           | _ -> error
           end
@@ -2406,10 +2406,10 @@ type maybe_bitstring =
     framework as well as the size of the data matched.
 **)
 let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framework)
-    : (s_framework * int) on_success =
+    : (s_framework * int) or_err =
   let error = ERR("Reached end of data bitstring too soon") in
   let rec compare_data_aux l bs s (sfw: s_framework):
-      (s_framework * int) on_success =
+      (s_framework * int) or_err =
     match l with
     | [] -> OK(sfw, s)
     | d::l ->
@@ -2476,7 +2476,7 @@ let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framewor
         end
   in
   let rec compare_data_empty l s (sfw: s_framework):
-      (s_framework * int) on_success =
+      (s_framework * int) or_err =
     match l with
     | [] -> OK(sfw, s)
     | d::l ->
@@ -2496,7 +2496,7 @@ let check_data_symtab ident sym_ndx size sfw =
   let symtab_ent_start = Int32.(
     add
       elf.e_shdra.(elf.e_symtab_sndx).sh_offset
-      (int_int32 (16 * sym_ndx))
+      (Safe32.of_int (16 * sym_ndx))
   ) in
   let sym = sfw.ef.elf.e_symtab.(sym_ndx) in
   let atom = Hashtbl.find sfw.atoms ident in
@@ -2507,7 +2507,7 @@ let check_data_symtab ident sym_ndx size sfw =
   in
   sfw
   >>> (
-    if sym.st_size = int_int32 size
+    if sym.st_size = Safe32.of_int size
     then id
     else (
       sf_ef ^%=
@@ -2554,7 +2554,7 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
     let sym_bs =
       match elf.e_shdra.(sym_sndx).sh_type with
       | SHT_NOBITS ->
-          Empty(int32_int sym.st_size * 8)
+          Empty(Safe.(of_int32 sym.st_size * 8))
       | SHT_PROGBITS ->
           NonEmpty(bitstring_at_vaddr_nosize elf sym_sndx sym_vaddr)
       | _ -> assert false
@@ -2872,7 +2872,7 @@ let check_padding efw =
        the end. *)
     | [(_, e, _, _) as h] ->
         let elf_size =
-          int_int32 ((Bitstring.bitstring_length efw.elf.e_bitstring) / 8) in
+          Safe32.of_int ((Bitstring.bitstring_length efw.elf.e_bitstring) / 8) in
         let elf_end = Int32.sub elf_size 1l in
         if e = elf_end
         then { efw with
@@ -2890,9 +2890,9 @@ let check_padding efw =
         let pad_stop = Int32.sub b2 1l in
         if
           pad_start = b2 (* if they are directly consecutive *)
-          || int32_int (Int32.sub b2 e1) > a2 (* or if they are too far away *)
+          || Safe.(of_int32 b2 - of_int32 e1) > a2 (* or if they are too far away *)
           || not (is_padding efw.elf.e_bitstring
-                    (int32_int pad_start) (int32_int pad_stop))
+                    (Safe32.to_int pad_start) (Safe32.to_int pad_stop))
         then (* not padding *)
           if pad_start <= pad_stop
           then check_padding_aux efw
@@ -2984,7 +2984,7 @@ let check_elf_nodump elf sdumps =
   let nb_syms = Array.length elf.e_symtab in
   let section_strtab = elf.e_shdra.(eh.e_shstrndx) in
   let symtab_shdr = elf.e_shdra.(elf.e_symtab_sndx) in
-  let symbol_strtab = elf.e_shdra.(int32_int symtab_shdr.sh_link) in
+  let symbol_strtab = elf.e_shdra.(Safe32.to_int symtab_shdr.sh_link) in
   let efw =
     {
       elf = elf;
@@ -2996,12 +2996,12 @@ let check_elf_nodump elf sdumps =
     >>> check_elf_header
     >>> add_range
       eh.e_phoff
-      (int_int32 (eh.e_phnum * eh.e_phentsize))
+      Safe.(to_int32 (eh.e_phnum * eh.e_phentsize))
       4
       ELF_progtab
     >>> add_range
       eh.e_shoff
-      (int_int32 (eh.e_shnum * eh.e_shentsize))
+      Safe.(to_int32 (eh.e_shnum * eh.e_shentsize))
       4
       ELF_shtab
     >>> add_range
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;
   }
diff --git a/checklink/ELF_utils.ml b/checklink/ELF_utils.ml
index f860e3f..d5c205a 100644
--- a/checklink/ELF_utils.ml
+++ b/checklink/ELF_utils.ml
@@ -11,9 +11,9 @@ let section_ndx_by_name (e: elf)(name: string): int option =
 
 let section_bitstring_noelf
     (bs: bitstring)(eshdra: elf32_shdr array)(sndx: int): bitstring =
-  let sofs = int32_int eshdra.(sndx).sh_offset in
-  let size = int32_int eshdra.(sndx).sh_size in
-  Bitstring.subbitstring bs (sofs * 8) (size * 8)
+  let sofs = Safe32.to_int eshdra.(sndx).sh_offset in
+  let size = Safe32.to_int eshdra.(sndx).sh_size in
+  Bitstring.subbitstring bs Safe.(sofs * 8) Safe.(size * 8)
 
 let section_bitstring (e: elf): int -> bitstring =
   section_bitstring_noelf e.e_bitstring e.e_shdra
@@ -30,27 +30,25 @@ let section_at_vaddr (e: elf)(vaddr: int32): int option =
     e.e_shdra
 
 (**
-   Returns the entire bitstring that begins at the specified virtual address
-   within the specified section and ends at the end of the file. This is useful
-   when you don't know the sections size yet.
+   Returns the bitstring of the specified size beginning at the specified
+   virtual address within the specified section.
 *)
-let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring =
+let bitstring_at_vaddr e sndx vaddr size =
   let shdr = e.e_shdra.(sndx) in
   let bs = section_bitstring e sndx in
-  let ofs = int32_int (Int32.sub vaddr shdr.sh_addr) in
-  bitmatch bs with
-  | { subbs : -1 : bitstring, offset(8*ofs) } -> subbs
+  let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in
+  Bitstring.subbitstring bs bit_ofs size
 
 (**
-   Returns the bitstring of the specified size beginning at the specified
-   virtual address within the specified section.
+   Returns the entire bitstring that begins at the specified virtual address
+   within the specified section and ends at the end of the file. This is useful
+   when you don't know the sections size yet.
 *)
-let bitstring_at_vaddr e sndx vaddr size =
+let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring =
   let shdr = e.e_shdra.(sndx) in
   let bs = section_bitstring e sndx in
-  let ofs = int32_int (Int32.sub vaddr shdr.sh_addr) in
-  bitmatch bs with
-  | { subbs : size : bitstring, offset(8*ofs) } -> subbs
+  let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in
+  Bitstring.dropbits bit_ofs bs
 
 (**
    Removes symbol version for GCC's symbols.
diff --git a/checklink/Exc.ml b/checklink/Exc.ml
new file mode 100644
index 0000000..101087d
--- /dev/null
+++ b/checklink/Exc.ml
@@ -0,0 +1,2 @@
+exception IntOverflow
+exception Int32Overflow
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index fdd0769..f35672d 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -138,18 +138,18 @@ let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc)
 (* external ( >>> ) : 'a -> ('a -> 'b) -> 'b = "%revapply" *)
 let ( >>> ) (a: 'a) (f: 'a -> 'b): 'b = f a
 
-let ( >>? ) (a: 'a on_success) (f: 'a -> 'b): 'b on_success =
+let ( >>? ) (a: 'a or_err) (f: 'a -> 'b): 'b or_err =
   match a with
   | ERR(s) -> ERR(s)
   | OK(x) -> OK(f x)
 
-let ( >>= ) (a: 'a on_success) (f: 'a -> 'b on_success): 'b on_success =
+let ( >>= ) (a: 'a or_err) (f: 'a -> 'b or_err): 'b or_err =
   match a with
   | ERR(s) -> ERR(s)
   | OK(x) -> f x
 
-let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b on_success)
-    (arg: 'a): 'a on_success =
+let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b or_err)
+    (arg: 'a): 'a or_err =
   let focus = arg |. lens in
   match transf focus with
   | OK(res) -> OK((lens ^= res) arg)
diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml
index c1f6780..fb7bee7 100644
--- a/checklink/Fuzz.ml
+++ b/checklink/Fuzz.ml
@@ -9,7 +9,7 @@ let fuzz_debug = ref false
 let string_of_byte = Printf.sprintf "0x%02x"
 
 let full_range_of_byte elfmap byte =
-  let byte = int_int32 byte in
+  let byte = Int32.of_int byte in
   List.find (fun (a, b, _, _) -> a <= byte && byte <= b) elfmap 
 
 let range_of_byte elfmap byte =
@@ -23,7 +23,7 @@ let fuzz_check elfmap bs byte old sdumps =
   let is_error = function ERROR(_) -> true | _ -> false in
   let (str, _, _) = bs in
   let fuzz_description =
-    string_of_int32 (int_int32 byte) ^ " <- " ^
+    string_of_int32 (Int32.of_int byte) ^ " <- " ^
       string_of_byte (Char.code str.[byte]) ^ " (was " ^
       string_of_byte (Char.code old) ^ ") - " ^
       string_of_byte_chunk_desc (range_of_byte elfmap byte)
@@ -51,7 +51,7 @@ let fuzz_check elfmap bs byte old sdumps =
   | Assert_failure(s, l, c) ->
       if !fuzz_debug
       then Printf.printf "fuzz_check failed an assertion at %s (%d, %d)\n" s l c
-  | Library.Integer_overflow ->
+  | Exc.IntOverflow | Exc.Int32Overflow ->
       if !fuzz_debug
       then Printf.printf "fuzz_check raised an integer overflow exception\n"
   | Match_failure(s, l, c) ->
@@ -74,8 +74,8 @@ let fuzz_check elfmap bs byte old sdumps =
 *)
 let ok_fuzz elfmap str byte fuzz =
   let (a, b, _, r) = full_range_of_byte elfmap byte in
-  let a = int32_int a in
-  let b = int32_int b in
+  let a = Safe32.to_int a in
+  let b = Safe32.to_int b in
   let old = Char.code str.[byte] in
   let fuz = Char.code fuzz in
   match r with
diff --git a/checklink/Library.ml b/checklink/Library.ml
index 0014025..67d8a45 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -3,29 +3,31 @@ open BinPos
 
 type bitstring = Bitstring.bitstring
 
-let is_some = function
+let is_some: 'a option -> bool = function
 | Some(_) -> true
 | None    -> false
 
-let from_some = function
+let from_some: 'a option -> 'a = function
 | Some(x) -> x
 | None    -> raise Not_found
 
-let filter_some l = List.(map from_some (filter is_some l))
+let filter_some (l: 'a option list): 'a list =
+  List.(map from_some (filter is_some l))
 
-type 'a on_success =
+type 'a or_err =
   | OK of 'a
   | ERR of string
 
-let is_ok: 'a on_success -> bool = function
+let is_ok: 'a or_err -> bool = function
 | OK(_) -> true
 | ERR(_) -> false
 
-let from_ok = function
+let from_ok: 'a or_err -> 'a = function
 | OK(x) -> x
 | ERR(_) -> raise Not_found
 
-let filter_ok l = List.(map from_ok (filter is_ok l))
+let filter_ok (l: 'a or_err list): 'a list =
+  List.(map from_ok (filter is_ok l))
 
 external id : 'a -> 'a = "%identity"
 
@@ -41,17 +43,8 @@ let array_exists (cond: 'a -> bool) (arr: 'a array): int option =
     else array_exists_aux (ndx - 1)
   in array_exists_aux (Array.length arr - 1)
 
-(* Functions for safely converting between numeric types *)
-
-exception Integer_overflow
-
-let int32_int (i32: int32): int =
-  let i = Int32.to_int i32 in
-  if i32 = Int32.of_int i
-  then i
-  else raise Integer_overflow
-
-let int_int32 = Int32.of_int
+exception IntOverflow
+exception Int32Overflow
 
 (* Can only return positive numbers 0 <= res < 2^31 *)
 let positive_int32 p =
@@ -63,19 +56,19 @@ let positive_int32 p =
   let res = positive_int32_unsafe p in
   if res >= 0l
   then res
-  else raise Integer_overflow
+  else raise IntOverflow
 
 (* This allows for 1 bit of overflow, effectively returning a negative *)
 let rec positive_int32_lax = function
 | Coq_xI(p) ->
     let acc = positive_int32_lax p in
     if acc < 0l
-    then raise Integer_overflow
+    then raise Int32Overflow
     else Int32.(add (shift_left acc 1) 1l)
 | Coq_xO(p) ->
     let acc = positive_int32_lax p in
     if acc < 0l
-    then raise Integer_overflow
+    then raise Int32Overflow
     else Int32.shift_left acc 1
 | Coq_xH -> 1l
 
@@ -87,27 +80,27 @@ let z_int32 = function
 let z_int32_lax = function
 | Z0      -> 0l
 | Zpos(p) -> positive_int32_lax p
-| Zneg(p) -> raise Integer_overflow
+| Zneg(p) -> raise Int32Overflow
 
-let z_int z = int32_int (z_int32 z)
+let z_int z = Safe32.to_int (z_int32 z)
 
-let z_int_lax z = int32_int (z_int32_lax z)
+let z_int_lax z = Safe32.to_int (z_int32_lax z)
 
 (* Some more printers *)
 
 let string_of_array string_of_elt sep a =
-  "[\n" ^
-    fst (
-      Array.fold_left
-        (
-          fun accu elt ->
+  let contents =
+    (fst
+       (Array.fold_left
+          (fun accu elt ->
             let (str, ndx) = accu in
             (str ^ (if ndx > 0 then sep else "") ^ string_of_int ndx ^ ": " ^
                string_of_elt elt, ndx + 1)
-        )
-        ("", 0) a
-    ) ^
-    "\n]"
+          )
+          ("", 0) a
+       )
+    )
+  in "[\n" ^ contents ^ "\n]"
 
 let string_of_list string_of_elt sep l =
   String.concat sep (List.map string_of_elt l)
@@ -117,9 +110,7 @@ let string_of_bitstring bs =
     bitmatch bs with
     | { bit  : 1  : int       ;
         rest : -1 : bitstring } ->
-        (if bit
-         then "1"
-         else "0") ^ (string_of_bitset_aux rest)
+        (if bit then "1" else "0") ^ (string_of_bitset_aux rest)
     | { _ } -> ""
   in string_of_bitset_aux bs
 
diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml
index 086d1c2..d027649 100644
--- a/checklink/PPC_utils.ml
+++ b/checklink/PPC_utils.ml
@@ -17,7 +17,7 @@ let code_of_sym_ndx (e: elf) (ndx: int): ecode option =
   match sym.st_type with
   | STT_FUNC ->
       let sym_vaddr = sym.st_value in
-      let sym_size = 8 * (int32_int sym.st_size) in
+      let sym_size = Safe.(of_int32 sym.st_size * 8) in
       let sym_sndx = sym.st_shndx in
       let code_bs =
         bitstring_at_vaddr e sym_sndx sym_vaddr sym_size in
diff --git a/checklink/Safe.ml b/checklink/Safe.ml
new file mode 100644
index 0000000..efcd3bd
--- /dev/null
+++ b/checklink/Safe.ml
@@ -0,0 +1,25 @@
+(* "Hacker's Delight", section 2.12 *)
+
+let ( + ) x y =
+  let z = x + y in
+  (* Overflow occurs iff x and y have same sign and z's sign is different *)
+  if (z lxor x) land (z lxor y) < 0
+  then raise Exc.IntOverflow
+  else z
+
+let ( - ) x y =
+  let z = x - y in
+  (* Overflow occurs iff x and y have opposite signs and z and x have
+     opposite signs *)
+  if (x lxor y) land (z lxor x) < 0
+  then raise Exc.IntOverflow
+  else z
+
+let ( * ) x y =
+  let z = x * y in
+  if (x = min_int && y < 0) || (y <> 0 && z / y <> x)
+  then raise Exc.IntOverflow
+  else z
+
+let of_int32 = Safe32.to_int
+let to_int32 = Safe32.of_int
diff --git a/checklink/Safe32.ml b/checklink/Safe32.ml
new file mode 100644
index 0000000..e72563d
--- /dev/null
+++ b/checklink/Safe32.ml
@@ -0,0 +1,34 @@
+(* "Hacker's Delight", section 2.12 *)
+
+let ( + ) x y = Int32.(
+  let z = add x y in
+  (* Overflow occurs iff x and y have same sign and z's sign is different *)
+  if logand (logxor z x) (logxor z y) < 0l
+  then raise Exc.Int32Overflow
+  else z
+)
+
+let ( - ) x y = Int32.(
+  let z = sub x y in
+  (* Overflow occurs iff x and y have opposite signs and z and x have
+     opposite signs *)
+  if logand (logxor x y) (logxor z x) < 0l
+  then raise Exc.Int32Overflow
+  else z
+)
+
+let ( * ) x y = Int32.(
+  let z = mul x y in
+  if (x = min_int && y < 0l) || (y <> 0l && div z y <> x)
+  then raise Exc.Int32Overflow
+  else z
+)
+
+let to_int i32 = Int32.(
+  let i = to_int i32 in
+  if i32 = of_int i
+  then i
+  else raise Exc.IntOverflow
+)
+
+let of_int = Int32.of_int