This is the test case:
-- test.c ----------------
struct S {
long x;
short y;
};
struct S a = { 0, 0 };
struct S b;
int main() {
b = a;
}
--------------------------
Compile and run it as follows:
| clang -emit-llvm -O0 -g -c test.c -I $KLEE_HOME/klee/include -o test.bc
| klee test.bc
This is what I get:
| KLEE: output directory = "klee-out-41"
| klee: Memory.cpp:511: void klee::ObjectState::write(unsigned int,
klee::ref<klee::Expr>): Assertion `0 && "Invalid write size!"' failed.
| 0 klee 0x0000000000cde43f
| 1 klee 0x0000000000ce06b2
| 2 libpthread.so.0 0x00002b0ce72e7b40
| 3 libc.so.6 0x00002b0ce7ecdba5 gsignal + 53
| 4 libc.so.6 0x00002b0ce7ed16b0 abort + 384
| 5 libc.so.6 0x00002b0ce7ec6a71 __assert_fail + 241
| 6 klee 0x0000000000544c71
klee::ObjectState::write(unsigned int, klee::ref<klee::Expr>) + 449
| 7 klee 0x0000000000523f7a
klee::Executor::initializeGlobalObject(klee::ExecutionState&,
klee::ObjectState*, llvm::Constant*, unsigned int) + 202
| 8 klee 0x00000000005241ec
klee::Executor::initializeGlobalObject(klee::ExecutionState&,
klee::ObjectState*, llvm::Constant*, unsigned int) + 828
| 9 klee 0x0000000000524c7b
klee::Executor::initializeGlobals(klee::ExecutionState&) + 2411
| 10 klee 0x00000000005373e5
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**)
+ 2053
| 11 klee 0x000000000051ce34 main + 10692
| 12 libc.so.6 0x00002b0ce7eb8d8e __libc_start_main + 254
| 13 klee 0x0000000000513fb9
| Aborted
I tried LLVM r113505 and r118498 (HEAD as of 2010-11-09) and
KLEE r118498 (HEAD). My host compiler is gcc 4.4.5, my OS is
Ubuntu 10.10, and my machine is an x86_64.
The violated assertion is at line 511 of
`lib/Core/Memory.cpp' and the offending value is `48':
| 504 void ObjectState::write(unsigned offset, ref<Expr> value) {
| 505 // Check for writes of constant values.
| 506 if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
| 507 Expr::Width w = CE->getWidth();
| 508 if (w <= 64) {
| 509 uint64_t val = CE->getZExtValue();
| 510 switch (w) {
| 511 default: assert(0 && "Invalid write size!");
| 512 case Expr::Bool:
| 513 case Expr::Int8: write8(offset, val); return;
| 514 case Expr::Int16: write16(offset, val); return;
| 515 case Expr::Int32: write32(offset, val); return;
| 516 case Expr::Int64: write64(offset, val); return;
| 517 }
| 518 }
| 519 }
where, from `klee/Expr.h':
| 94 static const Width Bool = 1;
| 95 static const Width Int8 = 8;
| 96 static const Width Int16 = 16;
| 97 static const Width Int32 = 32;
| 98 static const Width Int64 = 64;
If the initializer of `a' is removed then KLEE does not crash.
I checked the generated bytecode:
| %0 = type { i64, i16, [6 x i8] }
| %struct.S = type { i64, i16 }
|
| @a = global %0 { i64 0, i16 0, [6 x i8] undef }, align 8
| @b = common global %struct.S zeroinitializer, align 8
and I noticed that though `a' and `b' have the same type in
the C source, in the bytecode `a' has some padding, `[6 x
i8]'. The bytecode generated for the assignment `b = a' is:
| call void @llvm.memcpy.p0i8.p0i8.i64(i8* bitcast (%struct.S* @b to
i8*), i8* bitcast (%0* @a to i8*), i64 16, i32 8, i1 false)
Incidentally, the size of `struct S' is 10 bytes (8+2).
The offending value is 48 (32+16) (bits) that is 6 bytes
(4+2).
If in `test.c' I replace `long' with `int32_t' then KLEE
does not crash.
Is this a 64bit porting issue?
Stefano Soffia
