Re: [CIL users] Bitfield width

[Christoph S. <cs...@fr...>]

Cristian -

On Tue, Jun 03, 2008 at 12:31:02PM -0700, Cristian Cadar wrote:
>   Thanks a lot for the patch; it works fine on coreutils.

You're welcome.  Glad to hear it works.


> However, coreutils revealed another problem in the new version of CIL.
> Here's a one line snippet of code that the version of CIL currently in
> the repository fails to compile:
>
>   enum { HUGE_BYTES = (18446744073709551615ULL) == (127 * 2 + 1) };
>
> (This is the preprocessed version of the following coreutils snippet:
>      #include <limits.h>
>      #include <stdint.h>
>      ...
>      enum { HUGE_BYTES = UINTMAX_MAX == UCHAR_MAX }; )
>
>   The error I get is:
>   randint2.c:1: Unimplemented: Cannot represent on 64 bits the integer
> 18446744073709551615ULL

    What a clear error message!  Cilly stores integers of the analyzed
C-program as "int64" values.  OCaml's "int64" data type is signed,
thus its range is (-2^63 .. 2^63 - 1) on a twos-complement
architecture, whereas UINTMAX_MAX expands to 2^64 - 1.  Thus, the
constant is definitely out of the representable range.

Some time ago I talked to Matt about the problem of a "long long int"
on a 64-bit machine having 128 bits.  We concluded with with a
reassuring "hasn't happened yet".  Your example shows that the problem
can surface on all 64-bit machines whenever they use their "unsigned
int" type.  A clean way of making cilly "future-proof" could be to
change "int64" to "Num" (arbitrary-precision numbers), but that looks
like a lot of work to me.  Any other ideas?

A quick fix for your cilly run is to redefine the "UINTMAX_MAX" macro
to 9223372036854775807 /* = 2^63 - 1 */, which is the largest number
an int64 can hold.  Though this "trick" might change your program's
logic.  :-/


>   BTW, are you guys planning to release a new version of CIL soon?

Sorry, but I have never been involved in the release process, so I'd
like to pass on this question to the guys in Soda hall.  ;-)


Cheers,
    Chris

--
Dr. Christoph L. Spiel