Re: [csmith-dev] Another union issue

["Xuejun Yang" <jxyang@cs.utah.edu>]

This command line option is useful for cross-generating random programs.
Sometimes we want to generate test cases on a more powerful platform then
test the compilers on a less powerful one. 

I think parsing the output of CIL is not as generic a solution, and is
beyond my knowledge.

-Xuejun   

> -----Original Message-----
> From: John Regehr [mailto:regehr@cs.utah.edu]
> Sent: Wednesday, August 10, 2011 5:01 PM
> To: Xuejun Yang
> Cc: csmith-dev@flux.utah.edu
> Subject: Re: [csmith-dev] Another union issue
> 
> I'd rather you didn't add random command-line options regarding
> implementation-defined behavior.
> 
> Rather, please parse a file output by for example CIL's
> implementation-defined behavior checker.
> 
> John
> 
> 
> 
> On 08/10/2011 04:45 PM, Xuejun Yang wrote:
> > Yes, it is a Csmith bug. It is because this macro " _CSMITH_BITFIELD"
makes
> > the length of bit-fields nondeterministic at generation time, and
misleads
> > the analyzer. Is it ok I remove the macro and add a command line option
> > --int-bytes to solve the problem that the macro was originally designed
for?
> >
> > -Xuejun
> >
> >> -----Original Message-----
> >> From: csmith-dev-bounces@flux.utah.edu
> >> [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of John Regehr
> >> Sent: Wednesday, August 10, 2011 4:05 PM
> >> To: csmith-dev@flux.utah.edu
> >> Subject: Re: [csmith-dev] Another union issue
> >>
> >> Pascal, it looks to me like the program fragment you sent is undefined.
> >>    Xuejun?
> >>
> >> John
> >>
> >>
> >> On 8/10/11 2:48 PM, Pascal Cuoq wrote:
> >>> Hello again,
> >>>
> >>> Xuejun wrote:
> >>>   >  this is fixed in commit a39f3c. Thanks for catching my wrong
> > assumption.
> >>>
> >>> I must attest that I have been running tests based on a39f3c
> >>> since it was committed, and the issue is gone. I believe this
> >>> new question is about something else, and again, I am not
> >>> confident what is right. I have upgraded to f0ba611, the latest
version.
> >>> It is again about unions and initialization.
> >>>
> >>> The attached program can be reduced to the following from the
> >>> point of view of my problem:
> >>>
> >>> union U3 {
> >>>      const unsigned f0 : _CSMITH_BITFIELD(41);
> >>>      const signed : _CSMITH_BITFIELD(0);
> >>>      int8_t * const  f1;
> >>>      int64_t  f2;
> >>>      const uint32_t  f3;
> >>> };
> >>>
> >>> static union U3 g_142[1][1] = {{{1UL}}};
> >>>
> >>> main(){
> >>> ...
> >>>       for (i = 0; i<  1; i++)
> >>>       {
> >>>           for (j = 0; j<  1; j++)
> >>>           {
> >>>               transparent_crc(g_142[i][j].f3, "g_142[i][j].f3",
> >>> print_hash_value);
> >>>               if (print_hash_value) printf("index = [%d][%d]\n", i,
j);
> >>>
> >>>           }
> >>>       }
> >>> }
> >>>
> >>> There is an assignment to g_142[0][0].f2 in the original, but you can
> >>> check by inserting exit(1); right before it that it is not reached.
> >>> So field f0 of g_142[0][0] is initialized, and much late, member f3 is
> >>> passed to transparent_crc().
> >>>
> >>> Is that supposed to be defined?
> >>>
> >>> I tried to get the information from C99's 6.7.8 section, but it is not
> >>> clear to me. However, objects are initialized according to their
types:
> >>> pointers to NULL and integers to zero. An union can have both and
> >>> integer member and a pointer member. And NULL's representation does
> not
> >>> have to be the same as that of the integer zero. So I do not see how
> >>> 6.7.8 could be saying that more than one member of an union should be
> >>> initialized.
> >>>
> >>> What do you think?
> >>>
> >>> One argument to be made is that the program is in any case safe in
> >>> practice on desktop architectures where NULL and 0 have the same
> >>> representation, made of zeroes, and static variables are mapped to a
> >>> segment that contains only zeroes. It wouldn't be to hard to have an
> >>> option in Frama-C to implement the same point of view.
> >>>
> >>> Pascal
> >>>
> >