From 32a6fcb12814550633261960b540ffeb8a0fcab5 Mon Sep 17 00:00:00 2001 From: varobert Date: Wed, 4 Apr 2012 11:59:40 +0000 Subject: Added safety to potentially overflowing arithmetics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Safe32.ml | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 checklink/Safe32.ml (limited to 'checklink/Safe32.ml') 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 -- cgit v1.2.3