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, 27 insertions, 36 deletions

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