Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005934OCamlOCaml generalpublic2013-02-26 19:562014-03-19 16:44
Reporterregehr 
Assigned To 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusresolvedResolutionsuspended 
PlatformPCOSLinuxOS VersionUbuntu 12.04
Product Version4.00.1 
Target VersionFixed in Version 
Summary0005934: undefined integer overflows
DescriptionThe 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 Reproduce1. build a recent Clang

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

  configure -cc 'clang -fsanitize=undefined'

3. 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0008931)
gasche (developer)
2013-02-26 23:09

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.
(0008932)
xleroy (administrator)
2013-02-27 20:14

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.
(0009009)
xleroy (administrator)
2013-03-24 16:45

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.
(0011061)
oandrieu (reporter)
2014-03-19 16:44

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.

- Issue History
Date Modified Username Field Change
2013-02-26 19:56 regehr New Issue
2013-02-26 23:09 gasche Note Added: 0008931
2013-02-26 23:09 gasche Status new => acknowledged
2013-02-27 20:14 xleroy Note Added: 0008932
2013-03-24 16:45 xleroy Note Added: 0009009
2013-03-24 16:45 xleroy Status acknowledged => resolved
2013-03-24 16:45 xleroy Resolution open => suspended
2014-03-19 16:44 oandrieu Note Added: 0011061


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker