diff options
author | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-04 11:59:40 +0000 |
---|---|---|
committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-04 11:59:40 +0000 |
commit | 32a6fcb12814550633261960b540ffeb8a0fcab5 (patch) | |
tree | d6b180cba9277f76bb70d7a0ee81b05e50811211 /checklink/Safe32.ml | |
parent | 3498607028a17be29cd2fbc3b1f48f2847915ce3 (diff) | |
download | compcert-32a6fcb12814550633261960b540ffeb8a0fcab5.tar.gz compcert-32a6fcb12814550633261960b540ffeb8a0fcab5.zip |
Added safety to potentially overflowing arithmetics
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Safe32.ml')
-rw-r--r-- | checklink/Safe32.ml | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/checklink/Safe32.ml b/checklink/Safe32.ml new file mode 100644 index 00000000..e72563d7 --- /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 |