Cil handles the constant 0x80000000 incorrectly on my 64-bit machine, making it
a signed int instead
of an unsigned int.
The following program exercises the bug:
#include <stdio.h>
int
main (int argc, char** argv)
{
printf ("%d\n", 0x80000000);
printf ("(0x80000000 >> 28)== ((unsigned int)0x80000000) >> 28 = %d\n",
(0x80000000 >> 28) == ((unsigned int)0x80000000) >> 28);
printf ("(0x80000000 >> 28) == ((int)0x80000000) >> 28) = %d\n",
(0x80000000 >> 28) == ((int)0x80000000) >> 28);
printf ("0x80000000 < 0 = %d\n", 0x80000000 < 0);
return 0;
}
When compiled with gcc, the program produces the following output:
-2147483648
(0x80000000 >> 28)== ((unsigned int)0x80000000) >> 28 = 1
(0x80000000 >> 28) == ((int)0x80000000) >> 28) = 0
0x80000000 < 0 = 0
When compiled with Cil, it produces the following:
-2147483648
(0x80000000 >> 28)== ((unsigned int)0x80000000) >> 28 = 0
(0x80000000 >> 28) == ((int)0x80000000) >> 28) = 1
0x80000000 < 0 = 1
The following patch against version 12173 fixes this particular problem, but I
am not sure that it
is the right way to fix the problem.
--- src/cilint.ml (revision 12173)
+++ src/cilint.ml (working copy)
@@ -190,11 +190,11 @@
match c with
| Small i when n >= Nativeint.size - 1 -> Small i, NoTruncation
| Small i when n < Nativeint.size - 2 ->
- let max = 1 lsl (n - 1) in
+ let max = (1 lsl (n - 1)) - 1 in
let truncmax = 1 lsl n in
let bits = i land (truncmax - 1) in
let tval =
- if bits < max then
+ if bits <= max then
bits
else
bits - truncmax
Here Cil is testing whether or not the value i will fit into the number of bits
n of the particular
signed int (in my case, IInt). I assume that max is defined as (1 << 31)
instead of (1 << 31) - 1
because the comparison of bits to max is strict (<), but code following this
uses i rather than bits
and decides on NoTruncation in the case where i == max. Perhaps the whole
routine needs to be
rethought, but this fix seems to solve my immediate problem.
The following also seems to work for me and may be simpler:
--- src/cilint.ml (revision 12173)
+++ src/cilint.ml (working copy)
@@ -200,7 +200,7 @@
bits - truncmax
in
let trunc =
- if i > max || i < -max then
+ if i >= max || i <= -max then
if i > truncmax then
BitTruncation
else
------------------------------------------------------------------------------
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
