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

Re: [csmith-dev] Generated programs do not satify


union { int i; char c; } ic;
int main(void){ ic.c = ic.i; }
The semantics says "If the value being stored in an object
is read from another object that overlaps in any way the storage of
the first object, then the overlap shall be exact..."

I am not convinced I want to warn for the quoted
example, where both memory accesses are atomic

The accesses are not required to be atomic, although in many
cases they will be.

I did not spot any question in this email and some of it
seems to be written by Pascal.  Is some text missing?

and where there is a conversion between the read
access and the write access anyway. But, for assignment
of structs, the possibility of overlap between source and
destination clearly is a concern. The compiler may implement
the struct assignment with memcpy() or an inlined,
specialized version of memcpy().

Based on the example below, it seems to me that
Csmith may generate programs that do not respect the above

  * Generator: csmith 2.1.0
  * Git version: ea4762b
  * Options:   --max-pointer-depth 2 --max-funcs 4 --max-array-dim 2
--max-array-len-per-dim 4 --max-struct-fields 15 --max-union-fields 15
--no-volatiles --no-bitfields --no-argc --unions
  * Seed:      199711046

That example contains:

/* ------------------------------------------ */
  * reads :
  * writes: g_44
static uint32_t  func_24(int8_t ** p_25, int8_t ** p_26, union U2  p_27)
{ /* block id: 132 */
     struct S0 *l_235[1];
     int32_t l_236 = (-1L);
     int i;
     for (i = 0; i<  1; i++)
         l_235[i] =&g_103[0].f3;
     g_44 = (p_27.f2.f3 = p_27.f0);
     return l_236;

In this function, the assignment p_27.f2.f3 = p_27.f0 seems to violate
the quoted rule, and indeed, I get different results with different
meaning-giving systems for C programs (the clang compiler on
the one hand and Frama-C on the other hand).
Besides, clang also gives different results between
-O0 and -O2.

Frama-C does not implement the "no partial overlap" rule yet —I examined
this example because of results mismatches, not because it had
emitted an alarm— but it seems it will have to in order to be as correct
as we want it to be.


Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd          blog:shape-of-code.coding-guidelines.com
Source code analysis            http://www.knosof.co.uk