[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [csmith-dev] Unions in C program: referee needed



Hi Pascal, this is fixed in commit a39f3c. Thanks for catching my wrong assumption.

 

-Xuejun

 

 

From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of Xuejun Yang
Sent: Friday, August 05, 2011 11:26 AM
To: 'Pascal Cuoq'; csmith-dev@flux.utah.edu
Subject: Re: [csmith-dev] Unions in C program: referee needed

 

Thanks Pascal  for a tricky Csmith bug. I am working on it.

 

-Xuejun

 

From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of Pascal Cuoq
Sent: Friday, August 05, 2011 8:18 AM
To: csmith-dev@flux.utah.edu
Subject: [csmith-dev] Unions in C program: referee needed

 

Hello,

something funny is happening with a Csmith-generated program.
Csmith claims it is defined (I think. I didn't use dangerous options),
Frama-C's value analysis thinks it's not, and I am not quite sure
how to arbitrate between them.

This is with version, options and seed:

 * Git version: 01a9384
 * Options:   --max-pointer-depth 3 --max-funcs 2 --max-array-dim 2 --max-array-len-per-dim 3 --max-struct-fields 5 --no-volatiles --no-argc --unions
 * Seed:      1647756027

Executing the program works fine (with 64-bit, little-endian GCC):
checksum = 682193FB

On the other hand, the value analysis chokes shortly after line 628:
    transparent_crc(g_118.f0, "g_118.f0", print_hash_value);

Instrumenting the program to get details, it says it thinks that at that point:

        g_118{.f0[bits 0 to 7]; .f1.f0; .f2.f0.f0.f0; .f3.f0.f0.f0[bits 0 to 7]; }

             {77}
             {.f0[bits 8 to 31]; .f1.[bits 8 to 31]; .f2.f0.f0.[bits 8 to 31]; .f3.f0.f0{.f0[bits 8 to 15]; .f1; }; }

             UNINITIALIZED
             {.f0[bits 32 to 63]; .f1.[bits 32 to 63]; .f2.f0.f0.f1; .f3.f0.f0.f2; }

             {2683586253}
             {.f0[bits 64 to 71]; .f1; .f2.f0.f0.f2; .f3.f0.f1[bits 0 to 7]; }

             {0}
             {.f0[bits 72 to 95]; .f1.[bits 72 to 95]; .f2.f0.f0.[bits 72 to 95]; .f3.f0.f1[bits 8 to 31]; }

             UNINITIALIZED
             {.f0[bits 96 to 447]; .f1.[bits 96 to 447]; .f2.[bits 96 to 447]; .f3{.f0{.f1[bits 32 to 63]; .f2; .[bits 224 to 255]; }; .f1; .f2; .f3; .[bits 288 to 319]; }; }

             {0}

There are quite a few uninitialized bits in member g_118.f0, so it is right to complain, but the question is whether the values it has computed can be trusted.

My computer does not support the awatch command in GDB for some reason, so I am a little naked here. The best continuation I know is:

$ gdb a.out
...
(gdb) break transparent_crc
Breakpoint 1 at 0x4016f3: file runtime/csmith.h, line 113.
(gdb) run
Starting program: /home/cuoq/csmith_new/a.out

Breakpoint 1, transparent_crc (val=123, vname=0x403688 "g_4.f0.f0.f0", flag=0) at runtime/csmith.h:113
113        crc32_8bytes(val);
(gdb) print g_118
$1 = {f0 = 11525915192630181965, f1 = {f0 = 77 'M'}, f2 = {f0 = {f0 = {f0 = 77 'M', f1 = 2683586253, f2 = 0 '\000'}}}, f3 = {f0 = {f0 = {f0 = 77,
        f1 = 0, f2 = 2683586253}, f1 = 0, f2 = {f0 = 0 '\000', f1 = 0, f2 = 0 '\000'}}, f1 = 0, f2 = 0, f3 = 0}}

So execution and analysis seem to agree for the members that are initialized. Does anyone know how to determine for sure whether the second byte (for instance) is initialized or not? I tried executing twice, but the same result comes out (which does not prove anything. The program is deterministic and the stack may naturally always hold the same values part of it is used without initialization).

Pascal