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/Feature/SolverTimeout.c | 3 +++ test/Makefile | 2 ++ test/lit.cfg | 11 ++++++++++- test/lit.site.cfg.in | 2 ++ 4 files changed, 17 insertions(+), 1 deletion(-) diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c index 2ef6d413..aa86a856 100644 --- a/test/Feature/SolverTimeout.c +++ b/test/Feature/SolverTimeout.c @@ -1,6 +1,9 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t1.bc +// FIXME: This test occasionally fails when using Z3 4.4.1 but +// not when using Z3 from the master branch. So disable the test for now. +// REQUIRES: stp #include int main() { 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 > $@ diff --git a/test/lit.cfg b/test/lit.cfg index f1253ea6..fdf9bf7b 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -128,4 +128,13 @@ config.available_features.add("llvm-" + current_llvm_version) for version in known_llvm_versions: if version != current_llvm_version: config.available_features.add("not-llvm-" + version) - + +# Solver features +if config.enable_stp: + config.available_features.add('stp') +else: + config.available_features.add('not-stp') +if config.enable_z3: + config.available_features.add('z3') +else: + config.available_features.add('not-z3') diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index 8e2d79a4..5aff44ab 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -18,6 +18,8 @@ config.llvmgxx = "@LLVMCXX@" config.enable_uclibc = True if @ENABLE_UCLIBC@ == 1 else False config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False config.have_selinux = True if @HAVE_SELINUX@ == 1 else False +config.enable_stp = True if @ENABLE_STP@ == 1 else False +config.enable_z3 = True if @ENABLE_Z3@ == 1 else False # Current target config.target_triple = "@TARGET_TRIPLE@" -- cgit 1.4.1