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

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