From 8409a27a57a6fd4aad8828b0912c3afd39efb7e0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 11 Feb 2016 10:35:47 +0000 Subject: Try to fix the TravisCI build when using Z3 as the solver. The ``test/Feature/SolverTimeout.c`` test fails there. The error message I see in TravisCI is ``` Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc" Command 2 Result: -11 Command 2 Output: Command 2 Stderr: KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" KLEE: WARNING: undefined reference to function: printf KLEE: ERROR: (location information missing) divide by zero KLEE: NOTE: now ignoring this error at this location 0 klee 0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34 1 klee 0x0000000000da85c9 2 libpthread.so.0 0x00007fca19936cb0 3 libz3.so 0x00007fca19079826 4 librt.so.1 0x00007fca1747640c 5 libpthread.so.0 0x00007fca1992ee9a 6 libc.so.6 0x00007fca1776c38d clone + 109 ``` The issue appears to be racey as I had to run several copies of KLEE in parallel for the bug to occur using Z3 4.4.1. I managed to get a coredump and got the backtrace from gdb for the crash which is ``` #0 0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112 #1 0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63 #2 0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312 #3 0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111 ``` The crash appears to be in Z3 itself but I can't reproduce the issue when using the version of Z3 from the master branch. For now we simply workaround the issue by not running the ``test/Feature/SolverTimeout.c`` test when using Z3 as the solver. We should revisit this issue when another stable release of Z3 is made. --- test/Makefile | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test/Makefile') diff --git a/test/Makefile b/test/Makefile index 02d0a36f..0b176769 100644 --- a/test/Makefile +++ b/test/Makefile @@ -82,4 +82,6 @@ lit.site.cfg: lit.site.cfg.in -e "s#@ENABLE_POSIX_RUNTIME@#$(ENABLE_POSIX_RUNTIME)#g" \ -e "s#@TARGET_TRIPLE@#$(TARGET_TRIPLE)#g" \ -e "s#@HAVE_SELINUX@#$(HAVE_SELINUX)#g" \ + -e "s#@ENABLE_STP@#$(ENABLE_STP)#g" \ + -e "s#@ENABLE_Z3@#$(ENABLE_Z3)#g" \ $(PROJ_SRC_DIR)/lit.site.cfg.in > $@ -- cgit 1.4.1