symbiotic
symbiotic copied to clipboard
KLEE does not properly model reading and writing of padded types
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
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?
https://github.com/klee/klee/issues/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.
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).
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.