0005934: undefined integer overflows - MantisBT

Mantis Bug Tracker

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0005934

OCaml

OCaml general

public

2013-02-26 19:56

2013-03-24 16:45

Reporter

regehr

Assigned To

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

resolved

Resolution

suspended

Platform

PC

OS

Linux

OS Version

Ubuntu 12.04

Product Version

4.00.1

Target Version

Fixed in Version

Summary

0005934: undefined integer overflows

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'

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.

Tags

No tags attached.

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.

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

Copyright © 2000 - 2011 MantisBT Group