I was playing around with KLEE recently. I followed the document "Building KLEE (LLVM 3.4)" and successfully ran all the examples in the tutorial.
However, when running my own program using KLEE:
$ klee -load=/usr/lib/x86_64-linux-gnu/libssl.so --libc=uclibc --posix-runtime -emit-all-errors -allow-external-sym-calls klee_client.bc
some errors occurred. (See the following console output)
KLEE: NOTE: Using klee-uclibc : /home/testuser/Downloads/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/testuser/Downloads/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/testuser/Downloads/klee_test/klee-out-3"
KLEE: WARNING ONCE: function "__libc_connect" has inline asm
KLEE: WARNING ONCE: function "setsockopt" has inline asm
KLEE: WARNING ONCE: function "shutdown" has inline asm
KLEE: WARNING ONCE: function "socket" has inline asm
KLEE: WARNING ONCE: function "__libc_recvfrom" has inline asm
KLEE: WARNING ONCE: function "__libc_sendto" has inline asm
KLEE: WARNING: undefined reference to function: ERR_clear_error
KLEE: WARNING: undefined reference to function: ERR_error_string
KLEE: WARNING: undefined reference to function: ERR_get_error
KLEE: WARNING: undefined reference to function: OPENSSL_config
KLEE: WARNING: undefined reference to function: SSL_CTX_ctrl
KLEE: WARNING: undefined reference to function: SSL_CTX_free
KLEE: WARNING: undefined reference to function: SSL_CTX_new
KLEE: WARNING: undefined reference to function: SSL_CTX_set_next_proto_select_cb
KLEE: WARNING: undefined reference to function: SSL_connect
KLEE: WARNING: undefined reference to function: SSL_free
KLEE: WARNING: undefined reference to function: SSL_get_error
KLEE: WARNING: undefined reference to function: SSL_library_init
KLEE: WARNING: undefined reference to function: SSL_load_error_strings
KLEE: WARNING: undefined reference to function: SSL_new
KLEE: WARNING: undefined reference to function: SSL_read
KLEE: WARNING: undefined reference to function: SSL_set_fd
KLEE: WARNING: undefined reference to function: SSL_shutdown
KLEE: WARNING: undefined reference to function: SSL_write
KLEE: WARNING: undefined reference to function: SSLv23_client_method
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
...
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 40876048)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: __syscall_rt_sigaction: silently ignoring
KLEE: WARNING ONCE: calling external: OPENSSL_config(0)
KLEE: WARNING ONCE: calling external: SSL_load_error_strings()
KLEE: WARNING ONCE: calling external: SSL_library_init()
KLEE: WARNING ONCE: calling external: printf(35435072, 46338336)
KLEE: ERROR: /home/testuser/Downloads/klee-uclibc/libc/inet/socketcalls.c:362: inline assembly is unsupported
KLEE: done: total instructions = 99493
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
I was curious why there was error related with uclibc? Because I compiled it as what the KLEE document said, and I didn't find any options to disable assembler code (e.g. no-asm) when "configure" uclibc before compiling.
Besides, I also noticed that there were many warnings about "undefined reference to function: ...". Should I compile the corresponding libraries to llvm bitcode rather than using existing shared objects?
Thanks!
For Q1: Basically, the KLEE document educates users to compile the uClibc into an archive of LLVM IR. Many of functions inside uClibc contains inlined assembly (or even are directly developed with assembly). Those assembly will not be compiled into LLVM IR, instead they will be maintained to be unchanged in the IR. Before executing the IR of a function from ucLibc, KLEE will check whether any assembly is included in the IR. If so, you will see warning as "function XXX has inline asm". There is no option to disable assembly. To get rid of those assembly, you have to find a way to translate them into LLVM IR.
For Q2: You need to separate the KLEE process and the to-be-tested program (e.g., the klee_client.bc in your case). When you load existing shared objects to KLEE, you are actually linking the library to the KLEE process, instead of the to-be-tested program. To link the to-be-tested program with a library, you need to compile the library into IR and then link it to the to-be-tested program via modifying the main function in KLEE (or using some options built in KLEE, about which I am not clear). When the to-be-tested program is loaded and linked with specified libraries by KLEE, KLEE will check whether every required function (called by some instructions) is present. If not, you will see the warning. In you case, you basically did not link the to-be-tested program with LLVM IR of the LibSSL.