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