Hello, During last week I have successfully ported KLEE to 64bit. Now it passes all checks and unittests. I have also tested the port on several programs from coreutils (more detailed testing will be done in the following days).
Initially I have tried using KLEE64 to run 32bit code, however it turns out to be a very difficult problem. When KLEE encounters a call to an external function, it executes it on behalf of its own 64bit process. However 64bit and 32bit functions may have different ABIs and mixing them leads to many problems. Examples include malloc() function (returns a 64bit address), or scanf() function (when calling with %ld argument it expects a pointer to 64bit location). The problem is not even specific to KLEE: it can be reproduced in LLVM interpreter as well. So my port is focused on running only 64bit code on 64bit KLEE. The following is a brief list of changes that I have made: - Changed "unsigned" and "int" types to 64bit clean equivalents (like size_t, ptrdiff_t, intptr_t, etc.) in various places. The diff is quite big: it touches 412 lines in 57 files. - Added forced coercion for arguments when calling functions (for example, 64bit llvm can pass an i32 argument when a function expects i64 one) and for malloc and alloca opcodes. - Changed arguments and return types of functions in klee/klee.h to be 64bit clean, updated implementation of that functions. - Changed types in KLEE runtime libs to be 64bit clean and match types in system libs. - Changed datatypes of __ctype_* arrays in initializeGlobals() function to match its implementations in libc. - Fixed one bug in stp: BeevMgr::CreateBVConst function assumes that sizeof(unsigned long long) > sizeof(unsigned long) - Implemented varargs handling on 64bit. To avoiding dealing with separate register save area and deciding what types of args should go to what registers, I am simply making a function believe that all varargs are on stack. - Temporary disabled Programs/pcregrep.c test on 64bit: the code of the test is a decompilation of llvm bytecode compiled for 32bit machine. - Changed Array::getDomain() function to return Expr::Int64 on 64bit machines. This fixes many assert failures when accessing arrays. - Added a special syntax in KQuery language to denote a type used as array indexes on current architecture. I have selected "w." syntax for it because it requires a very minimal change to parser and lexer. When the parser encounters "w." as a type expression, it understands it either as w32 or as w64 depending on the architecture. The last change is quite controversial, so I would like to discuss it further. The reason for introducing the new syntax is that currently kleaver can only understand arrays with index type matching to the pointer type. The "w." syntax is the fastest workaround for this problem. Another workaround would be to make array index type equal w32 on any architecture and always cast indexes to appropriate type when constructing Read and Write expressions in KLEE. A clean solution is, of course, supporting arrays with arbitrary index type. Would you suggest me implementing it instead of my workaround ? -- With the best regards, Vladimir
