[klee-dev] Error about inline assembly in uclibc

[Shengtuo Hu]

Hi,

I'm playing around with KLEE recently. I followed the document "Building
KLEE (LLVM 3.4)" and successfully run all the examples in KLEE.

However, when I wanted to run my own program using KLEE, some
errors occurred. (See the following console output)

[Command:] klee -load=/usr/lib/x86_64-linux-gnu/libssl.so --libc=uclibc
--posix-runtime -emit-all-errors -allow-external-sym-calls klee_client.bc

[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

My question is why there are errors in uclibc? Because I compiled it as
what the document said, and I didn't find any options (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!

Shengtuo Hu
-------------- next part --------------
HTML attachment scrubbed and removed