KLEE does not properly model reading and writing of padded types

[lzaoral]

This should be fixed in upstream KLEE as well. I guess that there will be a similar problem with writing as well. However, writing to the padding is UB as opposed to reading.

Code:

#include <assert.h>
#ifndef __STDC_NO_COMPLEX__
  #include <complex.h>
#endif
#include <stdalign.h>
#include <stdbool.h>
#include <stdint.h>
 
volatile char tmp;
 
#define CHECK_ALIGNMENT_AND_SIZE(type)                  \
    do {                                                \
        type val = 0;                                   \
        assert((uintptr_t) &val % alignof(type) == 0);  \
                                                        \
        for (unsigned i = 0; i < sizeof(type); i++)     \
            tmp = ((char *) &val)[i];                   \
    } while(0);
 
int main(void)
{
    /* Boolean type */
    CHECK_ALIGNMENT_AND_SIZE(bool);
 
    /* Character types */
    CHECK_ALIGNMENT_AND_SIZE(char);
    CHECK_ALIGNMENT_AND_SIZE(signed char);
    CHECK_ALIGNMENT_AND_SIZE(unsigned char);
 
    /* Integer types */
    CHECK_ALIGNMENT_AND_SIZE(short int);
    CHECK_ALIGNMENT_AND_SIZE(unsigned short int);
    CHECK_ALIGNMENT_AND_SIZE(int);
    CHECK_ALIGNMENT_AND_SIZE(unsigned int);
    CHECK_ALIGNMENT_AND_SIZE(long int);
    CHECK_ALIGNMENT_AND_SIZE(unsigned long int);
    CHECK_ALIGNMENT_AND_SIZE(long long);
    CHECK_ALIGNMENT_AND_SIZE(unsigned long long int);
 
    /* Real floating types */
    CHECK_ALIGNMENT_AND_SIZE(float);
    CHECK_ALIGNMENT_AND_SIZE(double);
    CHECK_ALIGNMENT_AND_SIZE(long double);  // <-- error is here
 
#ifndef __STDC_NO_COMPLEX__
    /* Complex floating types */
    CHECK_ALIGNMENT_AND_SIZE(float complex);
    CHECK_ALIGNMENT_AND_SIZE(double complex);
    CHECK_ALIGNMENT_AND_SIZE(long double complex);
 
#ifdef _Imaginary_I
    /* Imaginary floating types */
    CHECK_ALIGNMENT_AND_SIZE(float imaginary);
    CHECK_ALIGNMENT_AND_SIZE(double imaginary);
    CHECK_ALIGNMENT_AND_SIZE(long double imaginary);
#endif
#endif
}

Output:

$ symbiotic --prp=memsafety align.c
8.0.0-pre-llvm-12.0.0-symbiotic:653f9b8a-dg:06c8ca8c-sbt-slicer:b0864a5b-sbt-instrumentation:c34d55f2-klee:10e5fae9
INFO: Looking for invalid dereferences, invalid free, memory leaks, etc.
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1

INFO: Instrumentation time: 0.388455867767334
INFO: Optimizations time: 0.021735429763793945
INFO: Starting slicing
INFO: Total slicing time: 0.030827760696411133
INFO: Optimizations time: 0.020166397094726562
INFO: After-slicing optimizations and transformations time: 1.9311904907226562e-05
INFO: Starting verification
KLEE: WARNING: undefined reference to function: klee_make_nondet
KLEE: ERROR: /home/lukas/align.c:43: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

 --- Error trace ---

Error: memory error: out of bound pointer
File: /home/lukas/align.c
Line: 43
assembly.ll line: 1090
Stack:
        #000001090 in main () at /home/lukas/align.c:43
Info:
        address: 175:10
        pointing to: object at s.end() of size 10
                MO164[10] allocated at main():  %198 = alloca x86_fp80, align 16

 --- Sequence of non-deterministic values [function:file:line:col] ---


 --- ----------- ---
Error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch
RESULT: false(valid-deref)
INFO: Total time elapsed: 0.861320972442627

[mchalupa]

Could you introduce me into the problem a bit?

This should be fixed in upstream KLEE as well.

Is there already a related bug in upstream KLEE?

[lzaoral]

klee/klee#573 is related. For instance the "usable" size of long double on amd64 is 10 bytes but due to alignment requirements whole 16 bytes are allocated . It should be safe to read the padding if the value was previously initialized but only through char * so we don't violate strict aliasing rules. Klee, however, wrongly assumes that sizeof(long double) == 10 thus the failure in the example above.

[mchalupa]

However, writing to the padding is UB as opposed to reading.

btw. I couldn't find where it is said that writing the padding bytes is UB. I only found that reading could be UB if the bytes are trap representation (which can happen in some cases).

[lzaoral]

Sorry for the confusion, you're right. I mixed it up with trap representations. Writing through a character pointer to integral and real floating types should be safe according to 6.2.6.1/5:

Certain object representations need not represent a value of the object type. If the stored value of an object has such a representation and is read by an lvalue expression that does not have charactertype, the behavior is undefined. If such a representation is produced by a side effect that modifies all or any part of the object by an lvalue expression that does not have character type, the behavior is undefined. Such a representation is called a trap representation.

Thus, an automatic variable can be initialized to a trap representation without causing undefined behavior, but the valueof the variable cannot be used until a proper value is stored in it.

This also confirms, that the code above is safe.