Skip to content
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

Jump to bottom

undefined integer overflows #5934

Closed
vicuna opened this issue Feb 26, 2013 · 4 comments
Closed

undefined integer overflows #5934

vicuna opened this issue Feb 26, 2013 · 4 comments
Labels
bug suspended

Comments

@vicuna
Copy link

vicuna commented Feb 26, 2013

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

  1. build a recent Clang

  2. build OCaml, logging the output to a file, using:

configure -cc 'clang -fsanitize=undefined'

  1. run the OCaml test suite, again logging the output to a file

These two files should contain all of the errors that I have reported above.
@vicuna
Copy link
Author

vicuna commented Feb 26, 2013

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.

@vicuna
Copy link
Author

vicuna commented Feb 27, 2013

Comment author: @xavierleroy

I put a first analysis of the issue as a comment on John's blog. In summary:

  • We must hunt the test from the testsuite that performs the shift by a negative amount, because this is as undefined in OCaml as in C and therefore is a real bug in the test program.

  • The (floating-point) division by zero is perfectly legitimate per IEEE 754.

  • Most alarms would go away by defining the "value" type as unsigned (in effect, uintptr_t instead of intptr_t). This could cause bugs in third-party C-OCaml bindings, though, so we have to carefully outweigh the risks against the benefits.

@vicuna
Copy link
Author

vicuna commented Mar 24, 2013

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
1- there is really nothing for the C compiler to optimize in the surrounding code based on the assumption that no overflows occur;
2- the OCaml test suite covers those cases well and should be able to detect funny business by the C compiler.

As a consequence, I'm marking this PR as resolved/suspended.

@vicuna vicuna closed this as completed Mar 24, 2013
@vicuna
Copy link
Author

vicuna commented Mar 19, 2014

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.
,----
| -fwrapv
| This option instructs the compiler to assume that signed
| arithmetic overflow of addition, subtraction and multiplication
| wraps around using twos-complement representation. This flag
| enables some optimizations and disables others. This option is
| enabled by default for the Java front end, as required by the
| Java language specification.
|
| -fno-strict-overflow
| This tells the compiler that it may not assume that signed
| overflow is undefined.
|
| -Wstrict-overflow
| -Wstrict-overflow=n
| This option is only active when -fstrict-overflow is active. It
| warns about cases where the compiler optimizes based on the
| assumption that signed overflow does not occur.
`----
cf. this blog post by GCC dev. Ian Lance Taylor discussing these options http://www.airs.com/blog/archives/120

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:
,----
| #define Val_long(x) ((intnat)(((uintnat)(x) << 1) + 1))
`----
eliminates all the clang warnings for the KCG runtime on our test suite.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug suspended
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@vicuna