diff options
| -rw-r--r-- | .travis.yml | 14 | ||||
| -rwxr-xr-x | .travis/klee.sh | 4 | ||||
| -rw-r--r-- | Dockerfile | 2 | ||||
| -rw-r--r-- | NEWS | 32 | ||||
| -rw-r--r-- | autoconf/configure.ac | 2 | ||||
| -rwxr-xr-x | configure | 18 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 | ||||
| -rw-r--r-- | test/Feature/srem.c | 33 |
8 files changed, 86 insertions, 21 deletions
diff --git a/.travis.yml b/.travis.yml index be30c1e2..07ef8a01 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,7 +20,7 @@ env: # Check the matrix of: # LLVM : {2.9, 3.4} # STP : {2.1.0, master} - # UCLIBC: {ENABLED, DISABLED} + # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # with Asserts enabled. # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set @@ -30,19 +30,19 @@ env: #- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 #- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1 - - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Check at least one build with Asserts disabled. - - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 # Check at least one Debug+Asserts build - - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 global: - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I= - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= diff --git a/.travis/klee.sh b/.travis/klee.sh index 3008c7fb..fbce61e7 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -28,8 +28,8 @@ fi ############################################################################### # klee-uclibc ############################################################################### -if [ "${KLEE_UCLIBC}" -eq 1 ]; then - git clone --depth 1 git://github.com/klee/klee-uclibc.git +if [ "${KLEE_UCLIBC}" != "0" ]; then + git clone --depth 1 -b ${KLEE_UCLIBC} git://github.com/klee/klee-uclibc.git cd klee-uclibc ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION} make diff --git a/Dockerfile b/Dockerfile index 03a65a75..b6aab804 100644 --- a/Dockerfile +++ b/Dockerfile @@ -9,7 +9,7 @@ ENV LLVM_VERSION=3.4 \ STP_VERSION=master \ DISABLE_ASSERTIONS=0 \ ENABLE_OPTIMIZED=1 \ - KLEE_UCLIBC=1 \ + KLEE_UCLIBC=klee_uclibc_v1.0.0 \ KLEE_SRC=/home/klee/klee_src \ COVERAGE=0 \ BUILD_DIR=/home/klee/klee_build diff --git a/NEWS b/NEWS new file mode 100644 index 00000000..8c1699e5 --- /dev/null +++ b/NEWS @@ -0,0 +1,32 @@ +KLEE 1.1.0, 13 November 2015 +============================ + +* Made LLVM 3.4 and STP 2.1.0 the recommended versions for installing KLEE (Cristian Cadar, @ccadar; Dan Liew, @delcypher; Martin Nowack, @MartinNowack; Mate Soos, @msoos) +* Added instructions for using the Docker images (Dan Liew, @delcypher) +* Added NEWS file to keep track of changes for each release (Cristian Cadar, @ccadar) +* Added coverage information for the current KLEE codebase (Timotej Kapus, @kren1) +* Added -entry-point=FOO option, where FOO is the name of the function to use as the entry point for execution (Riccardo Schirone, @ret2libc) +* Switched STP to v2.1.0 (instead of the old r940) in TravisCI (Martin Nowack, @MartinNowack) +* Improved Dockerfiles to use specific dependency versions (Dan Liew, @delcypher) +* Bug fix: Fixed signed division by constant 1/-1 (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1) +* Bug fix: Generate SRrem expressions correctly (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1) +* Bug fix: Allowed the generation of initial values for queries with empty constraint set (Martin Nowack, @MartinNowack) +* Bug fix: Fixed assertion failure in getDirectCallTarget (Sean Bartell, @yotann) +* Bug fix/test improvement: Use a temporary directory instead of /tmp in futimesat test (Andrew Chi, @andrewchi) +* Various fixes and improvements to the website (Eric Rizzi, @holycrap872; Martin Nowack, @MartinNowack; Bheesham Persaud, @bheesham; Gu Zhengxiong, @NoviceLive; Cristian Cadar, @ccadar) + + +KLEE 1.0.0, 10 August 2015 +========================== + +# Recent changes (from 2015) + +* Several performance improvements to the counterexample cache, including changing some default behaviour (Eric Rizzi, @holycrap872) +* Computing coverage of KLEE code in Travis CI (Timotej Kapus, @kren1) +* Added an option --readable-posix-inputs which is used to turn on/off the CEX preferences added in the POSIX model (Eric Rizzi, @holycrap872; Cristian Cadar, @ccadar) +* Lots of improvements to the build process (Dan Liew, @delcypher) +* Added klee-clang as alternative to klee-gcc (Martin Nowack, @MartinNowack) +* Added Dockerfile for building a KLEE Docker image (Dan Liew, @delcypher) +* Added a new option, --rewrite-equalities, which makes it possible to disable the optimisation that rewrites existing constraints when an equality with a constant is added (Cristian Cadar, @ccadar) +* Cleaner, more efficient timestamps (Emil Rakadjiev, @erakadjiev) +* Improved integer overflow detection (Luca Dariz, @luckyluke) diff --git a/autoconf/configure.ac b/autoconf/configure.ac index b94843a3..3d4becc8 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -1,7 +1,7 @@ dnl ************************************************************************** dnl * Initialize dnl ************************************************************************** -AC_INIT([[KLEE]],[[1.0.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]]) +AC_INIT([[KLEE]],[[1.1.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]]) dnl Identify where LLVM source tree is (this is patched by dnl AutoRegen.sh) diff --git a/configure b/configure index 1f603063..72ed1883 100755 --- a/configure +++ b/configure @@ -1,6 +1,6 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.69 for KLEE 1.0.0. +# Generated by GNU Autoconf 2.69 for KLEE 1.1.0. # # Report bugs to <klee-dev@imperial.ac.uk>. # @@ -580,8 +580,8 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='KLEE' PACKAGE_TARNAME='klee-' -PACKAGE_VERSION='1.0.0' -PACKAGE_STRING='KLEE 1.0.0' +PACKAGE_VERSION='1.1.0' +PACKAGE_STRING='KLEE 1.1.0' PACKAGE_BUGREPORT='klee-dev@imperial.ac.uk' PACKAGE_URL='https://klee.github.io' @@ -1285,7 +1285,7 @@ if test "$ac_init_help" = "long"; then # Omit some internal or obsolete options to make the list less imposing. # This message is too long to be a string in the A/UX 3.1 sh. cat <<_ACEOF -\`configure' configures KLEE 1.0.0 to adapt to many kinds of systems. +\`configure' configures KLEE 1.1.0 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1351,7 +1351,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of KLEE 1.0.0:";; + short | recursive ) echo "Configuration of KLEE 1.1.0:";; esac cat <<\_ACEOF @@ -1463,7 +1463,7 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -KLEE configure 1.0.0 +KLEE configure 1.1.0 generated by GNU Autoconf 2.69 Copyright (C) 2012 Free Software Foundation, Inc. @@ -2044,7 +2044,7 @@ cat >config.log <<_ACEOF This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. -It was created by KLEE $as_me 1.0.0, which was +It was created by KLEE $as_me 1.1.0, which was generated by GNU Autoconf 2.69. Invocation command line was $ $0 $@ @@ -5619,7 +5619,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" -This file was extended by KLEE $as_me 1.0.0, which was +This file was extended by KLEE $as_me 1.1.0, which was generated by GNU Autoconf 2.69. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -5686,7 +5686,7 @@ _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`" ac_cs_version="\\ -KLEE config.status 1.0.0 +KLEE config.status 1.1.0 configured by $0, generated by GNU Autoconf 2.69, with options \\"\$ac_cs_config\\" diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index c2f23c0a..ddeb3c37 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -751,7 +751,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { #endif // XXX implement my fast path and test for proper handling of sign - return vc_sbvModExpr(vc, *width_out, left, right); + return vc_sbvRemExpr(vc, *width_out, left, right); } // Bitwise diff --git a/test/Feature/srem.c b/test/Feature/srem.c new file mode 100644 index 00000000..f4fa8aa5 --- /dev/null +++ b/test/Feature/srem.c @@ -0,0 +1,33 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 %t.bc +// RUN: grep "KLEE: done: explored paths = 5" %t.klee-out/info +// RUN: grep "KLEE: done: generated tests = 4" %t.klee-out/info +#include <stdio.h> +#include <assert.h> + +int main(int argc, char** argv) +{ + int y; + + klee_make_symbolic(&y, sizeof(y), "y"); + + // Test cases divisor is positive or negative + if (y >= 0) { + if (y < 2) { + // Two test cases generated taking this path, one for y == 0 and y ==1 + assert(1 % y == 0); + } else { + assert(1 % y == 1); + } + } else { + if (y > -2) { + assert(1 % y == 0); + } else { + assert(1 % y == 1); + } + } + + assert(0 % y == 0); + assert(-1 % y == -1); +} |