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, 34 insertions, 0 deletions

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