New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
undefined integer overflows #5934
Comments
Comment author: @gasche Thank you for making a bug report; it wasn't in fact strictly necessary in this case, as we discussed the issue right after you published your blog post, but the additional details are helpful. |
Comment author: @xavierleroy I put a first analysis of the issue as a comment on John's blog. In summary:
|
Comment author: @xavierleroy The shift by negative amount is fixed on trunk, in commit 13438. It was a dubious programming pattern used in the Nat and Big_int modules from the nums library. The pattern was such that the result of the shift was (fortunately) not used in the case where the amount was < 0, so this was relatively harmless, and this is why I didn't push the fix to the 4.00 bugfix branch. Concerning the third class of alarms (overflows in signed arithmetic), I decided to do nothing for the moment, because As a consequence, I'm marking this PR as resolved/suspended. |
Comment author: @oandrieu A couple of remarks concerning this issue: There are a number of interesting GCC options that can help deal with these 'signed overflow' problems. Unfortunately I couldn't find an equivalent option for MSVC. Most of the UB raised by clang seem to be caused by the Val_long conversion macro (because of the signed value type). Without changing the type definition of value, simply redefining Val_long to the (hopefully) equivalent: |
Original bug ID: 5934
Reporter: regehr
Status: resolved (set by @xavierleroy on 2013-03-24T15:45:05Z)
Resolution: suspended
Priority: normal
Severity: minor
Platform: PC
OS: Linux
OS Version: Ubuntu 12.04
Version: 4.00.1
Category: ~DO NOT USE (was: OCaml general)
Bug description
The errors below are from Clang's integer sanitizer which is discussed here:
http://blog.regehr.org/archives/905
The OCaml version is from your SVN trunk yesterday.
The errors are divided into several parts, with a blank line in between. First, a shift by -1 bit position. Second, a divide by zero. Third, a number of signed overflows. Fourth, a collection of (most likely) less severe errors involving C99's somewhat strict rules for signed left-shift.
My recommendation is that you fix the first three categories of bug.
Some of these errors are triggered by, for example, coqchk, as discussed here:
http://blog.regehr.org/archives/903
Please let me know if you have any questions or if I can help in some fashion.
interp.c:976:43: runtime error: shift exponent -1 is negative
floats.c:230:41: runtime error: division by zero
interp.c:1014:12: runtime error: signed integer overflow: -9223372036854775807 + -2 cannot be represented in type 'long'
interp.c:943:36: runtime error: signed integer overflow: 9223372036854775807 + 3 cannot be represented in type 'long'
interp.c:947:14: runtime error: signed integer overflow: 223 * 2728331717811041672 cannot be represented in type 'long'
ints.c:256:40: runtime error: signed integer overflow: 2147483647 + 2147483647 cannot be represented in type 'int'
ints.c:259:40: runtime error: signed integer overflow: 2147483647 - -2147483648 cannot be represented in type 'int'
ints.c:262:40: runtime error: signed integer overflow: 305419896 * 162254319 cannot be represented in type 'int'
ints.c:465:26: runtime error: signed integer overflow: 9223372036854775807 + 9223372036854775807 cannot be represented in type 'long'
ints.c:468:26: runtime error: signed integer overflow: 9223372036854775807 - -9223372036854775808 cannot be represented in type 'long'
ints.c:471:26: runtime error: signed integer overflow: 9223372036854775807 * 9223372036854775807 cannot be represented in type 'long'
ints.c:730:48: runtime error: signed integer overflow: 9223372036854775807 + 9223372036854775807 cannot be represented in type 'long'
ints.c:733:48: runtime error: signed integer overflow: -9223372036854775808 - 1 cannot be represented in type 'long'
ints.c:736:48: runtime error: signed integer overflow: 9223372036854775807 * 9223372036854775807 cannot be represented in type 'long'
ints.c:253:26: runtime error: negation of -2147483648 cannot be represented in type 'int32' (aka 'int'); cast to an unsigned type to negate this value to itself
ints.c:462:26: runtime error: negation of -9223372036854775808 cannot be represented in type 'int64' (aka 'long'); cast to an unsigned type to negate this value to itself
ints.c:727:30: runtime error: negation of -9223372036854775808 cannot be represented in type 'intnat' (aka 'long'); cast to an unsigned type to negate this value to itself
ints.c:96:21: runtime error: negation of -9223372036854775808 cannot be represented in type 'intnat' (aka 'long'); cast to an unsigned type to negate this value to itself
bigarray_stubs.c:273:12: runtime error: left shift of negative value -123
bigarray_stubs.c:277:12: runtime error: left shift of negative value -123
bigarray_stubs.c:287:12: runtime error: left shift of negative value -456
closure.c:52:17: runtime error: left shift of 1 by 31 places cannot be represented in type 'int'
closure.c:99:19: runtime error: left shift of 1 by 31 places cannot be represented in type 'int'
compare.c:178:29: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
compare.c:273:12: runtime error: left shift of negative value -1
compare.c:298:10: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
compare.c:305:10: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
floats.c:479:21: runtime error: left shift of negative value -1
floats.c:484:22: runtime error: left shift of negative value -1
intern.c:103:38: runtime error: left shift of 54043195528445952 by 8 places cannot be represented in type 'intnat' (aka 'long')
intern.c:368:13: runtime error: left shift of 133 by 56 places cannot be represented in type 'intnat' (aka 'long')
intern.c:371:13: runtime error: left shift of 133 by 56 places cannot be represented in type 'intnat' (aka 'long')
intern.c:374:13: runtime error: left shift of 192 by 56 places cannot be represented in type 'intnat' (aka 'long')
intern.c:378:13: runtime error: left shift of negative value -2147483648
intern.c:791:10: runtime error: left shift of 240 by 56 places cannot be represented in type 'intnat' (aka 'long')
interp.c:1014:19: runtime error: left shift of negative value -1
interp.c:1018:29: runtime error: left shift of negative value -1
interp.c:1053:14: runtime error: left shift of negative value -1021444811
interp.c:934:14: runtime error: left shift of negative value -1
interp.c:947:14: runtime error: left shift of 5044439860601031575 by 1 places cannot be represented in type 'intnat' (aka 'long')
interp.c:965:14: runtime error: left shift of negative value -236
interp.c:976:43: runtime error: left shift of 2 by 62 places cannot be represented in type 'long'
ints.c:135:10: runtime error: left shift of negative value -1
ints.c:140:10: runtime error: left shift of negative value -1
ints.c:140:10: runtime error: left shift of negative value -99
ints.c:271:21: runtime error: left shift of 1 by 31 places cannot be represented in type 'int'
ints.c:286:21: runtime error: left shift of 1 by 31 places cannot be represented in type 'int'
ints.c:304:40: runtime error: left shift of 1 by 31 places cannot be represented in type 'int32' (aka 'int')
ints.c:314:29: runtime error: left shift of 240 by 24 places cannot be represented in type 'int'
ints.c:330:10: runtime error: left shift of negative value -39
ints.c:343:10: runtime error: left shift of negative value -1
ints.c:480:7: runtime error: left shift of 1 by 63 places cannot be represented in type 'int64' (aka 'long')
ints.c:491:7: runtime error: left shift of 1 by 63 places cannot be represented in type 'int64' (aka 'long')
ints.c:508:26: runtime error: left shift of 1 by 63 places cannot be represented in type 'int64' (aka 'long')
ints.c:534:26: runtime error: left shift of 136 by 56 places cannot be represented in type 'long'
ints.c:540:10: runtime error: left shift of negative value -456
ints.c:567:10: runtime error: left shift of negative value -1
ints.c:596:23: runtime error: left shift of 4294967295 by 32 places cannot be represented in type 'int64' (aka 'long')
ints.c:598:26: runtime error: left shift of 2147483648 by 32 places cannot be represented in type 'int64' (aka 'long')
ints.c:747:19: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
ints.c:762:19: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
ints.c:780:48: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
ints.c:810:10: runtime error: left shift of negative value -456
ints.c:829:10: runtime error: left shift of negative value -1
io.c:789:3: runtime error: left shift of negative value -23
lalr.c:328:15: runtime error: left shift of 1 by 31 places cannot be represented in type 'int'
lexing.c:101:38: runtime error: left shift of negative value -1
lexing.c:147:24: runtime error: left shift of negative value -1
lexing.c:163:31: runtime error: left shift of negative value -1
lexing.c:189:16: runtime error: left shift of negative value -1
lexing.c:207:38: runtime error: left shift of negative value -1
lexing.c:66:31: runtime error: left shift of negative value -1
lexing.c:84:16: runtime error: left shift of negative value -1
lexing.c:84:16: runtime error: left shift of negative value -62
nat_stubs.c:303:5: runtime error: left shift of negative value -1
ocamlc-unsafeintern.c:791:10: runtime error: left shift of 255 by 56 places cannot be represented in type 'intnat' (aka 'long')
ocamloptcompare.c:273:12: runtime error: left shift of negative value -1
ocamloptcompare.c:305:10: runtime error: left shift of 1 by 63 places cannot be represented in type 'intnat' (aka 'long')
ocamloptintern.c:791:10: runtime error: left shift of 255 by 56 places cannot be represented in type 'intnat' (aka 'long')
ocamloptints.c:140:10: runtime error: left shift of negative value -2
ocamloptparsing.c:225:22: runtime error: left shift of negative value -1
ocamlopt-unsafeintern.c:791:10: runtime error: left shift of 255 by 56 places cannot be represented in type 'intnat' (aka 'long')
parsing.c:225:22: runtime error: left shift of negative value -1
signals.c:139:12: runtime error: left shift of negative value -12
signals.c:139:12: runtime error: left shift of negative value -20
str.c:242:23: runtime error: left shift of negative value -1
str.c:244:27: runtime error: left shift of negative value -1
strstubs.c:362:27: runtime error: left shift of negative value -1
strstubs.c:363:31: runtime error: left shift of negative value -1
Steps to reproduce
build a recent Clang
build OCaml, logging the output to a file, using:
configure -cc 'clang -fsanitize=undefined'
These two files should contain all of the errors that I have reported above.
The text was updated successfully, but these errors were encountered: