diff options
93 files changed, 2347 insertions, 1767 deletions
diff --git a/.clang-format b/.clang-format new file mode 100644 index 00000000..4f679309 --- /dev/null +++ b/.clang-format @@ -0,0 +1,4 @@ +--- +Language: Cpp +BasedOnStyle: LLVM +... diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 00000000..b3d5b5a0 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,3 @@ +.git +autom4te.cache +.*.swp diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 00000000..2098a079 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,5 @@ +* text=auto + +*.h text +*.c text +*.cpp text diff --git a/.travis.yml b/.travis.yml index e868493b..1979f1ef 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,22 +23,31 @@ env: # UCLIBC: {ENABLED, DISABLED} # with Asserts enabled. + # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set + # FIXME: Enable when we want to test LLVM3.5 + matrix: #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Check at least one build with Asserts disabled. - - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 + + # Check at least one Debug+Asserts build + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 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= + - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg= - # FIXME: Do Debug+Asserts builds cache: apt before_install: ########################################################################### @@ -66,8 +75,7 @@ before_install: ########################################################################### # Install stuff ########################################################################### - # FIXME: STP doesn't need everything from Boost! - - sudo apt-get install gcc-4.8 g++-4.8 libcap-dev cmake libboost-all-dev + - sudo apt-get install gcc-4.8 g++-4.8 libcap-dev cmake # Make gcc4.8 the default gcc version - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 20 - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 20 diff --git a/.travis/klee.sh b/.travis/klee.sh index faf3f5f5..3008c7fb 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -33,12 +33,16 @@ if [ "${KLEE_UCLIBC}" -eq 1 ]; then cd klee-uclibc ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION} make - KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --with-posix-runtime" + KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime" cd ../ else KLEE_UCLIBC_CONFIGURE_OPTION="" fi +COVERAGE_FLAGS="" +if [ ${COVERAGE} -eq 1 ]; then + COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage' +fi ############################################################################### # KLEE ############################################################################### @@ -55,6 +59,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ --with-llvmcxx=${KLEE_CXX} \ --with-stp="${BUILD_DIR}/stp/build" \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + CXXFLAGS="${COVERAGE_FLAGS}" \ && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ ENABLE_SHARED=0 @@ -94,6 +99,37 @@ set +e # We want to let all the tests run before we exit lit -v . RETURN="${RETURN}$?" +#generate and upload coverage if COVERAGE is set +if [ ${COVERAGE} -eq 1 ]; then + +#get zcov that works with gcov v4.8 + git clone https://github.com/ddunbar/zcov.git + cd zcov + sudo python setup.py install + sudo mkdir /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js + cd zcov + +#these files are not where zcov expects them to be after install so we move them + sudo cp js/sorttable.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sorttable.js + sudo cp js/sourceview.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sourceview.js + sudo cp style.css /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/style.css + +#install zcov dependency + sudo apt-get install enscript + +#update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause +#a segmentation fault in v4.6 + sudo apt-get install ggcov + sudo rm /usr/bin/gcov + sudo ln -s /usr/bin/gcov-4.8 /usr/bin/gcov + +#scan and generate coverage + zcov scan output.zcov ${BUILD_DIR} + zcov genhtml output.zcov coverage/ +#upload the coverage data, currently to a random ftp server + tar -zcvf coverage.tar.gz coverage/ + curl --form "file=@coverage.tar.gz" -u ${USER}:${PASSWORD} ${COVERAGE_SERVER} +fi ############################################################################### # Result ############################################################################### diff --git a/.travis/stp.sh b/.travis/stp.sh index abc4e566..d2b4f1f1 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -6,15 +6,27 @@ set -e STP_LOG="$(pwd)/stp-build.log" if [ "${STP_VERSION}" == "UPSTREAM" ]; then + # Build minisat + git clone https://github.com/stp/minisat + cd minisat + mkdir build + cd build + MINISAT_DIR=`pwd` + cmake -DCMAKE_INSTALL_PREFIX=/usr .. + make + sudo make install + cd ../../ + + # Build STP git clone --depth 1 git://github.com/stp/stp.git src mkdir build cd build - # Disabling building of shared libs is a workaround - cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF ../src - # Don't try to build stp executable, there's an issue with using gcc4.8 with boost libraries built with gcc4.6 + # Disabling building of shared libs is a workaround. + # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 + cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src set +e # Do not exit if build fails because we need to display the log - make libstp CopyPublicHeaders >> "${STP_LOG}" 2>&1 + make >> "${STP_LOG}" 2>&1 elif [ "${STP_VERSION}" == "r940" ]; then # Building the old "r940" version that for some reason we love so much! diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 00000000..d9fdd02d --- /dev/null +++ b/Dockerfile @@ -0,0 +1,129 @@ +FROM ubuntu:14.04 +MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk> + +# FIXME: Docker doesn't currently offer a way to +# squash the layers from within a Dockerfile so +# the resulting image is unnecessarily large! + +ENV LLVM_VERSION=3.4 \ + STP_VERSION=UPSTREAM \ + DISABLE_ASSERTIONS=0 \ + ENABLE_OPTIMIZED=1 \ + KLEE_UCLIBC=1 \ + KLEE_SRC=/home/klee/klee_src \ + COVERAGE=0 \ + BUILD_DIR=/home/klee/klee_build + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + clang-${LLVM_VERSION} \ + llvm-${LLVM_VERSION} \ + llvm-${LLVM_VERSION}-dev \ + llvm-${LLVM_VERSION}-runtime \ + llvm \ + libcap-dev \ + git \ + subversion \ + cmake \ + make \ + libboost-program-options-dev \ + python3 \ + python3-dev \ + python3-pip \ + perl \ + flex \ + bison \ + libncurses-dev \ + zlib1g-dev \ + patch \ + wget \ + unzip \ + binutils && \ + pip3 install -U lit tabulate && \ + update-alternatives --install /usr/bin/python python /usr/bin/python3 50 + +# Create ``klee`` user for container with password ``klee``. +# and give it password-less sudo access (temporarily so we can use the TravisCI scripts) +RUN useradd -m klee && \ + echo klee:klee | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER klee +WORKDIR /home/klee + +# Copy across source files needed for build +RUN mkdir ${KLEE_SRC} +ADD configure \ + LICENSE.TXT \ + Makefile \ + Makefile.* \ + README.md \ + TODO.txt \ + ${KLEE_SRC}/ +ADD .travis ${KLEE_SRC}/.travis/ +ADD autoconf ${KLEE_SRC}/autoconf/ +ADD docs ${KLEE_SRC}/docs/ +ADD include ${KLEE_SRC}/include/ +ADD lib ${KLEE_SRC}/lib/ +ADD runtime ${KLEE_SRC}/runtime/ +ADD scripts ${KLEE_SRC}/scripts/ +ADD test ${KLEE_SRC}/test/ +ADD tools ${KLEE_SRC}/tools/ +ADD unittests ${KLEE_SRC}/unittests/ +ADD utils ${KLEE_SRC}/utils/ + +# Set klee user to be owner +RUN sudo chown --recursive klee: ${KLEE_SRC} + +# Create build directory +RUN mkdir -p ${BUILD_DIR} + +# Build STP (use TravisCI script) +RUN cd ${BUILD_DIR} && mkdir stp && cd stp && ${KLEE_SRC}/.travis/stp.sh + +# Install testing utils (use TravisCI script) +RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \ + ${KLEE_SRC}/.travis/testing-utils.sh + +# FIXME: This is a nasty hack so KLEE's configure and build finds +# LLVM's headers file, libraries and tools +RUN sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin && \ + sudo ln -s /usr/bin/llvm-config /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-config && \ + sudo ln -s /usr/bin/llvm-dis /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-dis && \ + sudo ln -s /usr/bin/llvm-as /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-as && \ + sudo ln -s /usr/bin/llvm-link /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-link && \ + sudo ln -s /usr/bin/llvm-ar /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/llvm-ar && \ + sudo ln -s /usr/bin/opt /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/opt && \ + sudo ln -s /usr/bin/lli /usr/lib/llvm-${LLVM_VERSION}/build/Release/bin/lli && \ + sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/include && \ + sudo ln -s /usr/include/llvm-${LLVM_VERSION}/llvm /usr/lib/llvm-${LLVM_VERSION}/build/include/llvm && \ + sudo ln -s /usr/include/llvm-c-${LLVM_VERSION}/llvm-c /usr/lib/llvm-${LLVM_VERSION}/build/include/llvm-c && \ + for static_lib in /usr/lib/llvm-3.4/lib/*.a ; do sudo ln -s ${static_lib} /usr/lib/`basename ${static_lib}`; done + +# FIXME: This is **really gross**. The Official Ubuntu LLVM packages don't ship +# with ``FileCheck`` or the ``not`` tools so we have to hack building these +# into KLEE's build system in order for the tests to pass +RUN cd ${KLEE_SRC}/tools && \ + for tool in FileCheck not; do \ + svn export \ + http://llvm.org/svn/llvm-project/llvm/branches/release_34/utils/${tool} ${tool} ; \ + sed -i 's/^USEDLIBS.*$/LINK_COMPONENTS = support/' ${tool}/Makefile; \ + done && \ + sed -i '0,/^PARALLEL_DIRS/a PARALLEL_DIRS += FileCheck not' Makefile + +# FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist +RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \ + sudo ln -s /usr/bin/clang++ /usr/bin/clang++-${LLVM_VERSION} + +# Build KLEE (use TravisCI script) +RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/klee.sh + +# Revoke password-less sudo and Set up sudo access for the ``klee`` user so it +# requires a password +USER root +RUN mv /etc/sudoers.bak /etc/sudoers && \ + echo 'klee ALL=(root) ALL' >> /etc/sudoers +USER klee + +# Add KLEE binary directory to PATH +RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc diff --git a/LICENSE.TXT b/LICENSE.TXT index e2fb630a..b358bb35 100644 --- a/LICENSE.TXT +++ b/LICENSE.TXT @@ -1,19 +1,30 @@ ============================================================================== -klee Release License +KLEE Release License ============================================================================== University of Illinois/NCSA Open Source License +http://klee.github.io/ + +Developed by: + KLEE Team + Stanford Checking Group + Copyright (c) 2007-2009 Stanford University. All rights reserved. -Developed by: - klee Team +Maintained since 2009 by: + Software Reliability Group + http://srg.doc.ic.ac.uk/ + Imperial College London - Stanford Checking Group - http://klee.llvm.org +Improved and extended since 2009 by many developers. For a full list +of contributors, refer to + https://github.com/klee/klee/graphs/contributors +and the Git commit history. + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal with @@ -29,10 +40,10 @@ so, subject to the following conditions: this list of conditions and the following disclaimers in the documentation and/or other materials provided with the distribution. - * Neither the names of the klee Team, Stanford University, nor the - names of its contributors may be used to endorse or promote - products derived from this Software without specific prior - written permission. + * Neither the names of the KLEE Team, Stanford University, + Imperial College London, nor the names of its contributors may + be used to endorse or promote products derived from this + Software without specific prior written permission. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS @@ -43,15 +54,16 @@ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE SOFTWARE. ============================================================================== -The klee software contains code written by third parties. Such software will +The KLEE software contains code written by third parties. Such software will have its own individual LICENSE.TXT file in the directory in which it appears. This file will describe the copyrights, license, and restrictions which apply to that code. -The disclaimer of warranty in the University of Illinois Open Source License -applies to all code in the klee Distribution, and nothing in any of the other -licenses gives permission to use the names of the klee Team or Stanford -University to endorse or promote products derived from this Software. +The disclaimer of warranty in the University of Illinois Open Source +License applies to all code in the KLEE distribution, and nothing in +any of the other licenses gives permission to use the names of the +KLEE team, Stanford University, or the names of its contributors to +endorse or promote products derived from this Software. The following pieces of software have additional or alternate copyrights, licenses, and/or restrictions: diff --git a/Makefile b/Makefile index c2420dba..cb8ad083 100644 --- a/Makefile +++ b/Makefile @@ -63,3 +63,8 @@ clean:: $(MAKE) -C test clean $(MAKE) -C unittests clean rm -rf docs/doxygen test/lit.site.cfg + +# Install klee instrinsic header file +install-local:: + $(MKDIR) $(DESTDIR)$(PROJ_includedir)/klee + $(DataInstall) $(PROJ_SRC_ROOT)/include/klee/klee.h $(DESTDIR)$(PROJ_includedir)/klee/klee.h diff --git a/Makefile.common b/Makefile.common index 92f5118b..268de9f8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -5,7 +5,8 @@ include $(LEVEL)/Makefile.config # Include LLVM's Master Makefile config and rules. include $(LLVM_OBJ_ROOT)/Makefile.config -ifeq ($(BYTECODE_LIBRARY), 1) +BUILDING_RUNTIME:=$(if $(or $(BYTECODE_LIBRARY),$(MODULE_NAME)),1,0) +ifeq ($(BUILDING_RUNTIME),1) # # Override make variables based on the runtime configuration. We want # to override whatever the user may have said on the command line, @@ -18,15 +19,27 @@ override ENABLE_PROFILING := $(RUNTIME_ENABLE_PROFILING) override ENABLE_COVERAGE := $(RUNTIME_ENABLE_COVERAGE) override DEBUG_SYMBOLS := $(RUNTIME_DEBUG_SYMBOLS) endif +BYTECODE_DESTINATION:=$(DESTDIR)$(PROJ_libdir)/klee/runtime include $(PROJ_SRC_ROOT)/Makefile.rules +# We have to build the bytecode install directory manually. +# FIXME: Doing it this way is potentially racey! +install:: + $(MKDIR) $(BYTECODE_DESTINATION) + # LLVMCC was added in 2.7. ifeq ($(LLVMCC),) LLVMCC := $(LLVMGCC) LLVMCXX := $(LLVMGXX) endif +# Deliberately override the host compiler +# so that we use what was detected when KLEE was configured +# and not LLVM. +CC := $(KLEE_HOST_C_COMPILER) +CXX := $(KLEE_HOST_CXX_COMPILER) + # Needed to build runtime library using clang (gnu89 is the gcc default) C.Flags += -std=gnu89 @@ -38,10 +51,9 @@ endif # This is filename that KLEE will look for when trying to load klee-uclibc KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca" -LD.Flags += $(STP_LDFLAGS) CXX.Flags += $(STP_CFLAGS) CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\" -CXX.Flags += -DKLEE_INSTALL_LIB_DIR=\"$(PROJ_libdir)\" +CXX.Flags += -DKLEE_INSTALL_RUNTIME_DIR=\"$(BYTECODE_DESTINATION)\" ifeq ($(ENABLE_UCLIBC),1) CXX.Flags += -DKLEE_UCLIBC_BCA_NAME=\"$(KLEE_UCLIBC_BCA_NAME)\" diff --git a/Makefile.config.in b/Makefile.config.in index ee95c4e5..5b9f929c 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -1,8 +1,8 @@ # -*- Makefile -*- # Set the name of the project here -PROJECT_NAME := klee -PROJ_VERSION := 0.01 +PROJECT_NAME := @PACKAGE_NAME@ +PROJ_VERSION := @PACKAGE_VERSION@ # Set this variable to the top of the LLVM source tree. LLVM_SRC_ROOT = @LLVM_SRC@ @@ -36,7 +36,6 @@ ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@ -ENABLE_STPLOG := @ENABLE_STPLOG@ ENABLE_UCLIBC := @ENABLE_UCLIBC@ KLEE_UCLIBC_BCA := @KLEE_UCLIBC_BCA@ @@ -53,6 +52,10 @@ RUNTIME_ENABLE_PROFILING := KLEE_BITCODE_C_COMPILER := @KLEE_BITCODE_C_COMPILER@ KLEE_BITCODE_CXX_COMPILER := @KLEE_BITCODE_CXX_COMPILER@ +# Host compiler +KLEE_HOST_C_COMPILER := @KLEE_HOST_C_COMPILER@ +KLEE_HOST_CXX_COMPILER := @KLEE_HOST_CXX_COMPILER@ + # A list of "features" which tests can check for in XFAIL: TEST_FEATURE_LIST := @@ -70,5 +73,3 @@ CXXFLAGS := @CXXFLAGS@ -g -Wall LDFLAGS := @LDFLAGS@ -g REQUIRES_RTTI := @REQUIRES_RTTI@ -RUNTEST := @RUNTEST@ -TCLSH := @TCLSH@ diff --git a/Makefile.rules b/Makefile.rules index 5e954adf..20e19e26 100644 --- a/Makefile.rules +++ b/Makefile.rules @@ -486,9 +486,9 @@ endif ifeq ($(HOST_OS),Darwin) DARWIN_VERSION := `sw_vers -productVersion` # Strip a number like 10.4.7 to 10.4 - DARWIN_VERSION := $(shell echo $(DARWIN_VERSION)| sed -E 's/(10.[0-9]).*/\1/') + DARWIN_VERSION := $(shell echo $(DARWIN_VERSION)| sed -E 's/(10.[0-9]+).*/\1/') # Get "4" out of 10.4 for later pieces in the makefile. - DARWIN_MAJVERS := $(shell echo $(DARWIN_VERSION)| sed -E 's/10.([0-9]).*/\1/') + DARWIN_MAJVERS := $(shell echo $(DARWIN_VERSION)| sed -E 's/10.([0-9]+).*/\1/') SharedLinkOptions=-Wl,-flat_namespace -Wl,-undefined,suppress \ -dynamiclib diff --git a/README.md b/README.md index bbf9ebc9..e894ebc1 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,9 @@ -Klee Symbolic Virtual Machine +KLEE Symbolic Virtual Machine ============================= [](https://travis-ci.org/klee/klee) -`klee` is a symbolic virtual machine built on top of the LLVM compiler +`KLEE` is a symbolic virtual machine built on top of the LLVM compiler infrastructure. Currently, there are two primary components: 1. The core symbolic virtual machine engine; this is responsible for diff --git a/TODO.txt b/TODO.txt index 1e583dad..e547d1bc 100644 --- a/TODO.txt +++ b/TODO.txt @@ -12,7 +12,7 @@ Build System / Configure / Release Cleanups o Need a way to hide LLVM options in "klee --help". -Klee Internal +KLEE Internal -- o Make sure that namespaces and .cpp locations match with reorganized include locations. diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 5b9c4e58..ae497b48 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -1,7 +1,7 @@ dnl ************************************************************************** dnl * Initialize dnl ************************************************************************** -AC_INIT([[KLEE]],[[0.01]],[daniel@minormatter.com]) +AC_INIT([[KLEE]],[[0.2.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) @@ -34,8 +34,11 @@ AH_BOTTOM([#endif]) dnl We need to check for the compiler up here to avoid anything else dnl starting with a different one. +AC_PROG_CC(gcc clang) AC_PROG_CXX(g++ clang++ ) AC_LANG([C++]) +AC_SUBST(KLEE_HOST_C_COMPILER,$CC) +AC_SUBST(KLEE_HOST_CXX_COMPILER,$CXX) dnl ************************************************************************** dnl Find the host @@ -576,10 +579,27 @@ AC_CHECK_HEADER(stp/c_interface.h,, ]) CPPFLAGS="$old_CPPFLAGS" +STP_NEEDS_MINISAT=0 AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [ - AC_MSG_ERROR([Could not link with libstp]) + STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp]) ], "$STP_LDFLAGS") +dnl Try linking again with minisat if necessary +if test "X$STP_NEEDS_MINISAT" != X0 ; then + # Need to clear cached result + unset ac_cv_lib_stp_vc_setInterfaceFlags + + AC_CHECK_LIB(stp, + vc_setInterfaceFlags,, [ + AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong]) + ], "$STP_LDFLAGS" "-lminisat" ) + + STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" +else + STP_LDFLAGS="${STP_LDFLAGS} -lstp" +fi + + AC_SUBST(STP_CFLAGS) AC_SUBST(STP_LDFLAGS) diff --git a/configure b/configure index 82657008..9e524f41 100755 --- a/configure +++ b/configure @@ -1,8 +1,8 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.69 for KLEE 0.01. +# Generated by GNU Autoconf 2.69 for KLEE 0.2.0. # -# Report bugs to <daniel@minormatter.com>. +# Report bugs to <klee-dev@imperial.ac.uk>. # # # Copyright (C) 1992-1996, 1998-2012 Free Software Foundation, Inc. @@ -267,10 +267,10 @@ fi $as_echo "$0: be upgraded to zsh 4.3.4 or later." else $as_echo "$0: Please tell bug-autoconf@gnu.org and -$0: daniel@minormatter.com about your system, including any -$0: error possibly output before this message. Then install -$0: a modern shell, or manually run the script under such a -$0: shell if you do have one." +$0: [klee-dev@imperial.ac.uk] about your system, including +$0: any error possibly output before this message. Then +$0: install a modern shell, or manually run the script +$0: under such a shell if you do have one." fi exit 1 fi @@ -579,11 +579,11 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='KLEE' -PACKAGE_TARNAME='-klee-' -PACKAGE_VERSION='0.01' -PACKAGE_STRING='KLEE 0.01' -PACKAGE_BUGREPORT='daniel@minormatter.com' -PACKAGE_URL='' +PACKAGE_TARNAME='klee-' +PACKAGE_VERSION='0.2.0' +PACKAGE_STRING='KLEE 0.2.0' +PACKAGE_BUGREPORT='klee-dev@imperial.ac.uk' +PACKAGE_URL='https://klee.github.io' ac_unique_file=""Makefile.config.in"" # Factoring default headers for most tests. @@ -633,9 +633,6 @@ HAVE_SELINUX EGREP GREP CPP -ac_ct_CC -CFLAGS -CC RUNTIME_CONFIGURATION RUNTIME_DEBUG_SYMBOLS RUNTIME_DISABLE_ASSERTIONS @@ -667,13 +664,18 @@ build_os build_vendor build_cpu build +KLEE_HOST_CXX_COMPILER +KLEE_HOST_C_COMPILER +ac_ct_CXX +CXXFLAGS +CXX OBJEXT EXEEXT -ac_ct_CXX +ac_ct_CC CPPFLAGS LDFLAGS -CXXFLAGS -CXX +CFLAGS +CC LLVM_OBJ LLVM_SRC target_alias @@ -733,14 +735,14 @@ with_metasmt ac_precious_vars='build_alias host_alias target_alias -CXX -CXXFLAGS +CC +CFLAGS LDFLAGS LIBS CPPFLAGS +CXX +CXXFLAGS CCC -CC -CFLAGS CPP CXXCPP' @@ -1283,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 0.01 to adapt to many kinds of systems. +\`configure' configures KLEE 0.2.0 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1331,7 +1333,7 @@ Fine tuning of the installation directories: --infodir=DIR info documentation [DATAROOTDIR/info] --localedir=DIR locale-dependent data [DATAROOTDIR/locale] --mandir=DIR man documentation [DATAROOTDIR/man] - --docdir=DIR documentation root [DATAROOTDIR/doc/-klee-] + --docdir=DIR documentation root [DATAROOTDIR/doc/klee-] --htmldir=DIR html documentation [DOCDIR] --dvidir=DIR dvi documentation [DOCDIR] --pdfdir=DIR pdf documentation [DOCDIR] @@ -1349,7 +1351,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of KLEE 0.01:";; + short | recursive ) echo "Configuration of KLEE 0.2.0:";; esac cat <<\_ACEOF @@ -1382,22 +1384,23 @@ Optional Packages: --with-metasmt Location of metaSMT installation directory Some influential environment variables: - CXX C++ compiler command - CXXFLAGS C++ compiler flags + CC C compiler command + CFLAGS C compiler flags LDFLAGS linker flags, e.g. -L<lib dir> if you have libraries in a nonstandard directory <lib dir> LIBS libraries to pass to the linker, e.g. -l<library> CPPFLAGS (Objective) C/C++ preprocessor flags, e.g. -I<include dir> if you have headers in a nonstandard directory <include dir> - CC C compiler command - CFLAGS C compiler flags + CXX C++ compiler command + CXXFLAGS C++ compiler flags CPP C preprocessor CXXCPP C++ preprocessor Use these variables to override the choices made by `configure' or to help it to find libraries and programs with nonstandard names/locations. -Report bugs to <daniel@minormatter.com>. +Report bugs to <klee-dev@imperial.ac.uk>. +KLEE home page: <https://klee.github.io>. _ACEOF ac_status=$? fi @@ -1460,7 +1463,7 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -KLEE configure 0.01 +KLEE configure 0.2.0 generated by GNU Autoconf 2.69 Copyright (C) 2012 Free Software Foundation, Inc. @@ -1474,10 +1477,10 @@ fi ## Autoconf initialization. ## ## ------------------------ ## -# ac_fn_cxx_try_compile LINENO -# ---------------------------- +# ac_fn_c_try_compile LINENO +# -------------------------- # Try to compile conftest.$ac_ext, and return whether this succeeded. -ac_fn_cxx_try_compile () +ac_fn_c_try_compile () { as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack rm -f conftest.$ac_objext @@ -1497,7 +1500,7 @@ $as_echo "$ac_try_echo"; } >&5 fi $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } && { - test -z "$ac_cxx_werror_flag" || + test -z "$ac_c_werror_flag" || test ! -s conftest.err } && test -s conftest.$ac_objext; then : ac_retval=0 @@ -1510,23 +1513,23 @@ fi eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno as_fn_set_status $ac_retval -} # ac_fn_cxx_try_compile +} # ac_fn_c_try_compile -# ac_fn_cxx_try_link LINENO -# ------------------------- -# Try to link conftest.$ac_ext, and return whether this succeeded. -ac_fn_cxx_try_link () +# ac_fn_cxx_try_compile LINENO +# ---------------------------- +# Try to compile conftest.$ac_ext, and return whether this succeeded. +ac_fn_cxx_try_compile () { as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack - rm -f conftest.$ac_objext conftest$ac_exeext - if { { ac_try="$ac_link" + rm -f conftest.$ac_objext + if { { ac_try="$ac_compile" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" $as_echo "$ac_try_echo"; } >&5 - (eval "$ac_link") 2>conftest.err + (eval "$ac_compile") 2>conftest.err ac_status=$? if test -s conftest.err; then grep -v '^ *+' conftest.err >conftest.er1 @@ -1537,10 +1540,7 @@ $as_echo "$ac_try_echo"; } >&5 test $ac_status = 0; } && { test -z "$ac_cxx_werror_flag" || test ! -s conftest.err - } && test -s conftest$ac_exeext && { - test "$cross_compiling" = yes || - test -x conftest$ac_exeext - }; then : + } && test -s conftest.$ac_objext; then : ac_retval=0 else $as_echo "$as_me: failed program was:" >&5 @@ -1548,31 +1548,26 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 fi - # Delete the IPA/IPO (Inter Procedural Analysis/Optimization) information - # created by the PGI compiler (conftest_ipa8_conftest.oo), as it would - # interfere with the next link command; also delete a directory that is - # left behind by Apple's compiler. We do this before executing the actions. - rm -rf conftest.dSYM conftest_ipa8_conftest.oo eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno as_fn_set_status $ac_retval -} # ac_fn_cxx_try_link +} # ac_fn_cxx_try_compile -# ac_fn_c_try_compile LINENO -# -------------------------- -# Try to compile conftest.$ac_ext, and return whether this succeeded. -ac_fn_c_try_compile () +# ac_fn_cxx_try_link LINENO +# ------------------------- +# Try to link conftest.$ac_ext, and return whether this succeeded. +ac_fn_cxx_try_link () { as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack - rm -f conftest.$ac_objext - if { { ac_try="$ac_compile" + rm -f conftest.$ac_objext conftest$ac_exeext + if { { ac_try="$ac_link" case "(($ac_try" in *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; *) ac_try_echo=$ac_try;; esac eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" $as_echo "$ac_try_echo"; } >&5 - (eval "$ac_compile") 2>conftest.err + (eval "$ac_link") 2>conftest.err ac_status=$? if test -s conftest.err; then grep -v '^ *+' conftest.err >conftest.er1 @@ -1581,9 +1576,12 @@ $as_echo "$ac_try_echo"; } >&5 fi $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 test $ac_status = 0; } && { - test -z "$ac_c_werror_flag" || + test -z "$ac_cxx_werror_flag" || test ! -s conftest.err - } && test -s conftest.$ac_objext; then : + } && test -s conftest$ac_exeext && { + test "$cross_compiling" = yes || + test -x conftest$ac_exeext + }; then : ac_retval=0 else $as_echo "$as_me: failed program was:" >&5 @@ -1591,10 +1589,15 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 fi + # Delete the IPA/IPO (Inter Procedural Analysis/Optimization) information + # created by the PGI compiler (conftest_ipa8_conftest.oo), as it would + # interfere with the next link command; also delete a directory that is + # left behind by Apple's compiler. We do this before executing the actions. + rm -rf conftest.dSYM conftest_ipa8_conftest.oo eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno as_fn_set_status $ac_retval -} # ac_fn_c_try_compile +} # ac_fn_cxx_try_link # ac_fn_c_try_cpp LINENO # ---------------------- @@ -1703,9 +1706,9 @@ $as_echo "$as_me: WARNING: $2: see the Autoconf documentation" >&2;} $as_echo "$as_me: WARNING: $2: section \"Present But Cannot Be Compiled\"" >&2;} { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $2: proceeding with the compiler's result" >&5 $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;} -( $as_echo "## ------------------------------------- ## -## Report this to daniel@minormatter.com ## -## ------------------------------------- ##" +( $as_echo "## -------------------------------------- ## +## Report this to klee-dev@imperial.ac.uk ## +## -------------------------------------- ##" ) | sed "s/^/$as_me: WARNING: /" >&2 ;; esac @@ -1950,9 +1953,9 @@ $as_echo "$as_me: WARNING: $2: see the Autoconf documentation" >&2;} $as_echo "$as_me: WARNING: $2: section \"Present But Cannot Be Compiled\"" >&2;} { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $2: proceeding with the compiler's result" >&5 $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;} -( $as_echo "## ------------------------------------- ## -## Report this to daniel@minormatter.com ## -## ------------------------------------- ##" +( $as_echo "## -------------------------------------- ## +## Report this to klee-dev@imperial.ac.uk ## +## -------------------------------------- ##" ) | sed "s/^/$as_me: WARNING: /" >&2 ;; esac @@ -2041,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 0.01, which was +It was created by KLEE $as_me 0.2.0, which was generated by GNU Autoconf 2.69. Invocation command line was $ $0 $@ @@ -2460,27 +2463,23 @@ ac_config_headers="$ac_config_headers include/klee/Config/config.h" -ac_ext=cpp -ac_cpp='$CXXCPP $CPPFLAGS' -ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' -ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' -ac_compiler_gnu=$ac_cv_cxx_compiler_gnu -if test -z "$CXX"; then - if test -n "$CCC"; then - CXX=$CCC - else - if test -n "$ac_tool_prefix"; then - for ac_prog in g++ clang++ +ac_ext=c +ac_cpp='$CPP $CPPFLAGS' +ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' +ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' +ac_compiler_gnu=$ac_cv_c_compiler_gnu +if test -n "$ac_tool_prefix"; then + for ac_prog in gcc clang do # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args. set dummy $ac_tool_prefix$ac_prog; ac_word=$2 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 $as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_CXX+:} false; then : +if ${ac_cv_prog_CC+:} false; then : $as_echo_n "(cached) " >&6 else - if test -n "$CXX"; then - ac_cv_prog_CXX="$CXX" # Let the user override the test. + if test -n "$CC"; then + ac_cv_prog_CC="$CC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH @@ -2489,7 +2488,7 @@ do test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_CXX="$ac_tool_prefix$ac_prog" + ac_cv_prog_CC="$ac_tool_prefix$ac_prog" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 fi @@ -2499,32 +2498,32 @@ IFS=$as_save_IFS fi fi -CXX=$ac_cv_prog_CXX -if test -n "$CXX"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CXX" >&5 -$as_echo "$CXX" >&6; } +CC=$ac_cv_prog_CC +if test -n "$CC"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5 +$as_echo "$CC" >&6; } else { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 $as_echo "no" >&6; } fi - test -n "$CXX" && break + test -n "$CC" && break done fi -if test -z "$CXX"; then - ac_ct_CXX=$CXX - for ac_prog in g++ clang++ +if test -z "$CC"; then + ac_ct_CC=$CC + for ac_prog in gcc clang do # Extract the first word of "$ac_prog", so it can be a program name with args. set dummy $ac_prog; ac_word=$2 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 $as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_ac_ct_CXX+:} false; then : +if ${ac_cv_prog_ac_ct_CC+:} false; then : $as_echo_n "(cached) " >&6 else - if test -n "$ac_ct_CXX"; then - ac_cv_prog_ac_ct_CXX="$ac_ct_CXX" # Let the user override the test. + if test -n "$ac_ct_CC"; then + ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test. else as_save_IFS=$IFS; IFS=$PATH_SEPARATOR for as_dir in $PATH @@ -2533,7 +2532,7 @@ do test -z "$as_dir" && as_dir=. for ac_exec_ext in '' $ac_executable_extensions; do if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_ac_ct_CXX="$ac_prog" + ac_cv_prog_ac_ct_CC="$ac_prog" $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 break 2 fi @@ -2543,21 +2542,21 @@ IFS=$as_save_IFS fi fi -ac_ct_CXX=$ac_cv_prog_ac_ct_CXX -if test -n "$ac_ct_CXX"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CXX" >&5 -$as_echo "$ac_ct_CXX" >&6; } +ac_ct_CC=$ac_cv_prog_ac_ct_CC +if test -n "$ac_ct_CC"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5 +$as_echo "$ac_ct_CC" >&6; } else { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 $as_echo "no" >&6; } fi - test -n "$ac_ct_CXX" && break + test -n "$ac_ct_CC" && break done - if test "x$ac_ct_CXX" = x; then - CXX="g++" + if test "x$ac_ct_CC" = x; then + CC="" else case $cross_compiling:$ac_tool_warned in yes:) @@ -2565,14 +2564,18 @@ yes:) $as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;} ac_tool_warned=yes ;; esac - CXX=$ac_ct_CXX + CC=$ac_ct_CC fi fi - fi -fi + +test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 +$as_echo "$as_me: error: in \`$ac_pwd':" >&2;} +as_fn_error $? "no acceptable C compiler found in \$PATH +See \`config.log' for more details" "$LINENO" 5; } + # Provide some information about the compiler. -$as_echo "$as_me:${as_lineno-$LINENO}: checking for C++ compiler version" >&5 +$as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5 set X $ac_compile ac_compiler=$2 for ac_option in --version -v -V -qversion; do @@ -2612,8 +2615,8 @@ ac_clean_files="$ac_clean_files a.out a.out.dSYM a.exe b.out" # Try to create an executable without -o first, disregard a.out. # It will help us diagnose broken compilers, and finding out an intuition # of exeext. -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether the C++ compiler works" >&5 -$as_echo_n "checking whether the C++ compiler works... " >&6; } +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether the C compiler works" >&5 +$as_echo_n "checking whether the C compiler works... " >&6; } ac_link_default=`$as_echo "$ac_link" | sed 's/ -o *conftest[^ ]*//'` # The possible output files: @@ -2683,14 +2686,14 @@ sed 's/^/| /' conftest.$ac_ext >&5 { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} -as_fn_error 77 "C++ compiler cannot create executables +as_fn_error 77 "C compiler cannot create executables See \`config.log' for more details" "$LINENO" 5; } else { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5 $as_echo "yes" >&6; } fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for C++ compiler default output file name" >&5 -$as_echo_n "checking for C++ compiler default output file name... " >&6; } +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler default output file name" >&5 +$as_echo_n "checking for C compiler default output file name... " >&6; } { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_file" >&5 $as_echo "$ac_file" >&6; } ac_exeext=$ac_cv_exeext @@ -2784,7 +2787,7 @@ $as_echo "$ac_try_echo"; } >&5 else { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} -as_fn_error $? "cannot run C++ compiled programs. +as_fn_error $? "cannot run C compiled programs. If you meant to cross compile, use \`--host'. See \`config.log' for more details" "$LINENO" 5; } fi @@ -2846,6 +2849,353 @@ fi $as_echo "$ac_cv_objext" >&6; } OBJEXT=$ac_cv_objext ac_objext=$OBJEXT +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5 +$as_echo_n "checking whether we are using the GNU C compiler... " >&6; } +if ${ac_cv_c_compiler_gnu+:} false; then : + $as_echo_n "(cached) " >&6 +else + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +int +main () +{ +#ifndef __GNUC__ + choke me +#endif + + ; + return 0; +} +_ACEOF +if ac_fn_c_try_compile "$LINENO"; then : + ac_compiler_gnu=yes +else + ac_compiler_gnu=no +fi +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext +ac_cv_c_compiler_gnu=$ac_compiler_gnu + +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5 +$as_echo "$ac_cv_c_compiler_gnu" >&6; } +if test $ac_compiler_gnu = yes; then + GCC=yes +else + GCC= +fi +ac_test_CFLAGS=${CFLAGS+set} +ac_save_CFLAGS=$CFLAGS +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5 +$as_echo_n "checking whether $CC accepts -g... " >&6; } +if ${ac_cv_prog_cc_g+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_save_c_werror_flag=$ac_c_werror_flag + ac_c_werror_flag=yes + ac_cv_prog_cc_g=no + CFLAGS="-g" + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +if ac_fn_c_try_compile "$LINENO"; then : + ac_cv_prog_cc_g=yes +else + CFLAGS="" + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +if ac_fn_c_try_compile "$LINENO"; then : + +else + ac_c_werror_flag=$ac_save_c_werror_flag + CFLAGS="-g" + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +int +main () +{ + + ; + return 0; +} +_ACEOF +if ac_fn_c_try_compile "$LINENO"; then : + ac_cv_prog_cc_g=yes +fi +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext +fi +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext +fi +rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext + ac_c_werror_flag=$ac_save_c_werror_flag +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5 +$as_echo "$ac_cv_prog_cc_g" >&6; } +if test "$ac_test_CFLAGS" = set; then + CFLAGS=$ac_save_CFLAGS +elif test $ac_cv_prog_cc_g = yes; then + if test "$GCC" = yes; then + CFLAGS="-g -O2" + else + CFLAGS="-g" + fi +else + if test "$GCC" = yes; then + CFLAGS="-O2" + else + CFLAGS= + fi +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5 +$as_echo_n "checking for $CC option to accept ISO C89... " >&6; } +if ${ac_cv_prog_cc_c89+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_cv_prog_cc_c89=no +ac_save_CC=$CC +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ +#include <stdarg.h> +#include <stdio.h> +struct stat; +/* Most of the following tests are stolen from RCS 5.7's src/conf.sh. */ +struct buf { int x; }; +FILE * (*rcsopen) (struct buf *, struct stat *, int); +static char *e (p, i) + char **p; + int i; +{ + return p[i]; +} +static char *f (char * (*g) (char **, int), char **p, ...) +{ + char *s; + va_list v; + va_start (v,p); + s = g (p, va_arg (v,int)); + va_end (v); + return s; +} + +/* OSF 4.0 Compaq cc is some sort of almost-ANSI by default. It has + function prototypes and stuff, but not '\xHH' hex character constants. + These don't provoke an error unfortunately, instead are silently treated + as 'x'. The following induces an error, until -std is added to get + proper ANSI mode. Curiously '\x00'!='x' always comes out true, for an + array size at least. It's necessary to write '\x00'==0 to get something + that's true only with -std. */ +int osf4_cc_array ['\x00' == 0 ? 1 : -1]; + +/* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters + inside strings and character constants. */ +#define FOO(x) 'x' +int xlc6_cc_array[FOO(a) == 'x' ? 1 : -1]; + +int test (int i, double x); +struct s1 {int (*f) (int a);}; +struct s2 {int (*f) (double a);}; +int pairnames (int, char **, FILE *(*)(struct buf *, struct stat *, int), int, int); +int argc; +char **argv; +int +main () +{ +return f (e, argv, 0) != argv[0] || f (e, argv, 1) != argv[1]; + ; + return 0; +} +_ACEOF +for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std \ + -Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__" +do + CC="$ac_save_CC $ac_arg" + if ac_fn_c_try_compile "$LINENO"; then : + ac_cv_prog_cc_c89=$ac_arg +fi +rm -f core conftest.err conftest.$ac_objext + test "x$ac_cv_prog_cc_c89" != "xno" && break +done +rm -f conftest.$ac_ext +CC=$ac_save_CC + +fi +# AC_CACHE_VAL +case "x$ac_cv_prog_cc_c89" in + x) + { $as_echo "$as_me:${as_lineno-$LINENO}: result: none needed" >&5 +$as_echo "none needed" >&6; } ;; + xno) + { $as_echo "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5 +$as_echo "unsupported" >&6; } ;; + *) + CC="$CC $ac_cv_prog_cc_c89" + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5 +$as_echo "$ac_cv_prog_cc_c89" >&6; } ;; +esac +if test "x$ac_cv_prog_cc_c89" != xno; then : + +fi + +ac_ext=c +ac_cpp='$CPP $CPPFLAGS' +ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' +ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' +ac_compiler_gnu=$ac_cv_c_compiler_gnu + +ac_ext=cpp +ac_cpp='$CXXCPP $CPPFLAGS' +ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' +ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' +ac_compiler_gnu=$ac_cv_cxx_compiler_gnu +if test -z "$CXX"; then + if test -n "$CCC"; then + CXX=$CCC + else + if test -n "$ac_tool_prefix"; then + for ac_prog in g++ clang++ + do + # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args. +set dummy $ac_tool_prefix$ac_prog; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_CXX+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$CXX"; then + ac_cv_prog_CXX="$CXX" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_CXX="$ac_tool_prefix$ac_prog" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + +fi +fi +CXX=$ac_cv_prog_CXX +if test -n "$CXX"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CXX" >&5 +$as_echo "$CXX" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + test -n "$CXX" && break + done +fi +if test -z "$CXX"; then + ac_ct_CXX=$CXX + for ac_prog in g++ clang++ +do + # Extract the first word of "$ac_prog", so it can be a program name with args. +set dummy $ac_prog; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_ac_ct_CXX+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$ac_ct_CXX"; then + ac_cv_prog_ac_ct_CXX="$ac_ct_CXX" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_ac_ct_CXX="$ac_prog" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + +fi +fi +ac_ct_CXX=$ac_cv_prog_ac_ct_CXX +if test -n "$ac_ct_CXX"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CXX" >&5 +$as_echo "$ac_ct_CXX" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + test -n "$ac_ct_CXX" && break +done + + if test "x$ac_ct_CXX" = x; then + CXX="g++" + else + case $cross_compiling:$ac_tool_warned in +yes:) +{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5 +$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;} +ac_tool_warned=yes ;; +esac + CXX=$ac_ct_CXX + fi +fi + + fi +fi +# Provide some information about the compiler. +$as_echo "$as_me:${as_lineno-$LINENO}: checking for C++ compiler version" >&5 +set X $ac_compile +ac_compiler=$2 +for ac_option in --version -v -V -qversion; do + { { ac_try="$ac_compiler $ac_option >&5" +case "(($ac_try" in + *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; + *) ac_try_echo=$ac_try;; +esac +eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" +$as_echo "$ac_try_echo"; } >&5 + (eval "$ac_compiler $ac_option >&5") 2>conftest.err + ac_status=$? + if test -s conftest.err; then + sed '10a\ +... rest of stderr output deleted ... + 10q' conftest.err >conftest.er1 + cat conftest.er1 >&5 + fi + rm -f conftest.er1 conftest.err + $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 + test $ac_status = 0; } +done + { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C++ compiler" >&5 $as_echo_n "checking whether we are using the GNU C++ compiler... " >&6; } if ${ac_cv_cxx_compiler_gnu+:} false; then : @@ -2973,6 +3323,10 @@ ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5' ac_link='$CXX -o conftest$ac_exeext $CXXFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' ac_compiler_gnu=$ac_cv_cxx_compiler_gnu +KLEE_HOST_C_COMPILER=$CC + +KLEE_HOST_CXX_COMPILER=$CXX + # Make sure we can run config.sub. @@ -3793,545 +4147,6 @@ ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $ ac_compiler_gnu=$ac_cv_c_compiler_gnu -ac_ext=c -ac_cpp='$CPP $CPPFLAGS' -ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' -ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' -ac_compiler_gnu=$ac_cv_c_compiler_gnu -if test -n "$ac_tool_prefix"; then - # Extract the first word of "${ac_tool_prefix}gcc", so it can be a program name with args. -set dummy ${ac_tool_prefix}gcc; ac_word=$2 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 -$as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_CC+:} false; then : - $as_echo_n "(cached) " >&6 -else - if test -n "$CC"; then - ac_cv_prog_CC="$CC" # Let the user override the test. -else -as_save_IFS=$IFS; IFS=$PATH_SEPARATOR -for as_dir in $PATH -do - IFS=$as_save_IFS - test -z "$as_dir" && as_dir=. - for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_CC="${ac_tool_prefix}gcc" - $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done - done -IFS=$as_save_IFS - -fi -fi -CC=$ac_cv_prog_CC -if test -n "$CC"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5 -$as_echo "$CC" >&6; } -else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 -$as_echo "no" >&6; } -fi - - -fi -if test -z "$ac_cv_prog_CC"; then - ac_ct_CC=$CC - # Extract the first word of "gcc", so it can be a program name with args. -set dummy gcc; ac_word=$2 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 -$as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_ac_ct_CC+:} false; then : - $as_echo_n "(cached) " >&6 -else - if test -n "$ac_ct_CC"; then - ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test. -else -as_save_IFS=$IFS; IFS=$PATH_SEPARATOR -for as_dir in $PATH -do - IFS=$as_save_IFS - test -z "$as_dir" && as_dir=. - for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_ac_ct_CC="gcc" - $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done - done -IFS=$as_save_IFS - -fi -fi -ac_ct_CC=$ac_cv_prog_ac_ct_CC -if test -n "$ac_ct_CC"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5 -$as_echo "$ac_ct_CC" >&6; } -else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 -$as_echo "no" >&6; } -fi - - if test "x$ac_ct_CC" = x; then - CC="" - else - case $cross_compiling:$ac_tool_warned in -yes:) -{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5 -$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;} -ac_tool_warned=yes ;; -esac - CC=$ac_ct_CC - fi -else - CC="$ac_cv_prog_CC" -fi - -if test -z "$CC"; then - if test -n "$ac_tool_prefix"; then - # Extract the first word of "${ac_tool_prefix}cc", so it can be a program name with args. -set dummy ${ac_tool_prefix}cc; ac_word=$2 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 -$as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_CC+:} false; then : - $as_echo_n "(cached) " >&6 -else - if test -n "$CC"; then - ac_cv_prog_CC="$CC" # Let the user override the test. -else -as_save_IFS=$IFS; IFS=$PATH_SEPARATOR -for as_dir in $PATH -do - IFS=$as_save_IFS - test -z "$as_dir" && as_dir=. - for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_CC="${ac_tool_prefix}cc" - $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done - done -IFS=$as_save_IFS - -fi -fi -CC=$ac_cv_prog_CC -if test -n "$CC"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5 -$as_echo "$CC" >&6; } -else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 -$as_echo "no" >&6; } -fi - - - fi -fi -if test -z "$CC"; then - # Extract the first word of "cc", so it can be a program name with args. -set dummy cc; ac_word=$2 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 -$as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_CC+:} false; then : - $as_echo_n "(cached) " >&6 -else - if test -n "$CC"; then - ac_cv_prog_CC="$CC" # Let the user override the test. -else - ac_prog_rejected=no -as_save_IFS=$IFS; IFS=$PATH_SEPARATOR -for as_dir in $PATH -do - IFS=$as_save_IFS - test -z "$as_dir" && as_dir=. - for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/cc"; then - ac_prog_rejected=yes - continue - fi - ac_cv_prog_CC="cc" - $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done - done -IFS=$as_save_IFS - -if test $ac_prog_rejected = yes; then - # We found a bogon in the path, so make sure we never use it. - set dummy $ac_cv_prog_CC - shift - if test $# != 0; then - # We chose a different compiler from the bogus one. - # However, it has the same basename, so the bogon will be chosen - # first if we set CC to just the basename; use the full file name. - shift - ac_cv_prog_CC="$as_dir/$ac_word${1+' '}$@" - fi -fi -fi -fi -CC=$ac_cv_prog_CC -if test -n "$CC"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5 -$as_echo "$CC" >&6; } -else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 -$as_echo "no" >&6; } -fi - - -fi -if test -z "$CC"; then - if test -n "$ac_tool_prefix"; then - for ac_prog in cl.exe - do - # Extract the first word of "$ac_tool_prefix$ac_prog", so it can be a program name with args. -set dummy $ac_tool_prefix$ac_prog; ac_word=$2 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 -$as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_CC+:} false; then : - $as_echo_n "(cached) " >&6 -else - if test -n "$CC"; then - ac_cv_prog_CC="$CC" # Let the user override the test. -else -as_save_IFS=$IFS; IFS=$PATH_SEPARATOR -for as_dir in $PATH -do - IFS=$as_save_IFS - test -z "$as_dir" && as_dir=. - for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_CC="$ac_tool_prefix$ac_prog" - $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done - done -IFS=$as_save_IFS - -fi -fi -CC=$ac_cv_prog_CC -if test -n "$CC"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $CC" >&5 -$as_echo "$CC" >&6; } -else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 -$as_echo "no" >&6; } -fi - - - test -n "$CC" && break - done -fi -if test -z "$CC"; then - ac_ct_CC=$CC - for ac_prog in cl.exe -do - # Extract the first word of "$ac_prog", so it can be a program name with args. -set dummy $ac_prog; ac_word=$2 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 -$as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_prog_ac_ct_CC+:} false; then : - $as_echo_n "(cached) " >&6 -else - if test -n "$ac_ct_CC"; then - ac_cv_prog_ac_ct_CC="$ac_ct_CC" # Let the user override the test. -else -as_save_IFS=$IFS; IFS=$PATH_SEPARATOR -for as_dir in $PATH -do - IFS=$as_save_IFS - test -z "$as_dir" && as_dir=. - for ac_exec_ext in '' $ac_executable_extensions; do - if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then - ac_cv_prog_ac_ct_CC="$ac_prog" - $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 - break 2 - fi -done - done -IFS=$as_save_IFS - -fi -fi -ac_ct_CC=$ac_cv_prog_ac_ct_CC -if test -n "$ac_ct_CC"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_ct_CC" >&5 -$as_echo "$ac_ct_CC" >&6; } -else - { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 -$as_echo "no" >&6; } -fi - - - test -n "$ac_ct_CC" && break -done - - if test "x$ac_ct_CC" = x; then - CC="" - else - case $cross_compiling:$ac_tool_warned in -yes:) -{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: using cross tools not prefixed with host triplet" >&5 -$as_echo "$as_me: WARNING: using cross tools not prefixed with host triplet" >&2;} -ac_tool_warned=yes ;; -esac - CC=$ac_ct_CC - fi -fi - -fi - - -test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 -$as_echo "$as_me: error: in \`$ac_pwd':" >&2;} -as_fn_error $? "no acceptable C compiler found in \$PATH -See \`config.log' for more details" "$LINENO" 5; } - -# Provide some information about the compiler. -$as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5 -set X $ac_compile -ac_compiler=$2 -for ac_option in --version -v -V -qversion; do - { { ac_try="$ac_compiler $ac_option >&5" -case "(($ac_try" in - *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;; - *) ac_try_echo=$ac_try;; -esac -eval ac_try_echo="\"\$as_me:${as_lineno-$LINENO}: $ac_try_echo\"" -$as_echo "$ac_try_echo"; } >&5 - (eval "$ac_compiler $ac_option >&5") 2>conftest.err - ac_status=$? - if test -s conftest.err; then - sed '10a\ -... rest of stderr output deleted ... - 10q' conftest.err >conftest.er1 - cat conftest.er1 >&5 - fi - rm -f conftest.er1 conftest.err - $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5 - test $ac_status = 0; } -done - -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5 -$as_echo_n "checking whether we are using the GNU C compiler... " >&6; } -if ${ac_cv_c_compiler_gnu+:} false; then : - $as_echo_n "(cached) " >&6 -else - cat confdefs.h - <<_ACEOF >conftest.$ac_ext -/* end confdefs.h. */ - -int -main () -{ -#ifndef __GNUC__ - choke me -#endif - - ; - return 0; -} -_ACEOF -if ac_fn_c_try_compile "$LINENO"; then : - ac_compiler_gnu=yes -else - ac_compiler_gnu=no -fi -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext -ac_cv_c_compiler_gnu=$ac_compiler_gnu - -fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_c_compiler_gnu" >&5 -$as_echo "$ac_cv_c_compiler_gnu" >&6; } -if test $ac_compiler_gnu = yes; then - GCC=yes -else - GCC= -fi -ac_test_CFLAGS=${CFLAGS+set} -ac_save_CFLAGS=$CFLAGS -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5 -$as_echo_n "checking whether $CC accepts -g... " >&6; } -if ${ac_cv_prog_cc_g+:} false; then : - $as_echo_n "(cached) " >&6 -else - ac_save_c_werror_flag=$ac_c_werror_flag - ac_c_werror_flag=yes - ac_cv_prog_cc_g=no - CFLAGS="-g" - cat confdefs.h - <<_ACEOF >conftest.$ac_ext -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -if ac_fn_c_try_compile "$LINENO"; then : - ac_cv_prog_cc_g=yes -else - CFLAGS="" - cat confdefs.h - <<_ACEOF >conftest.$ac_ext -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -if ac_fn_c_try_compile "$LINENO"; then : - -else - ac_c_werror_flag=$ac_save_c_werror_flag - CFLAGS="-g" - cat confdefs.h - <<_ACEOF >conftest.$ac_ext -/* end confdefs.h. */ - -int -main () -{ - - ; - return 0; -} -_ACEOF -if ac_fn_c_try_compile "$LINENO"; then : - ac_cv_prog_cc_g=yes -fi -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext -fi -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext -fi -rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext - ac_c_werror_flag=$ac_save_c_werror_flag -fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_g" >&5 -$as_echo "$ac_cv_prog_cc_g" >&6; } -if test "$ac_test_CFLAGS" = set; then - CFLAGS=$ac_save_CFLAGS -elif test $ac_cv_prog_cc_g = yes; then - if test "$GCC" = yes; then - CFLAGS="-g -O2" - else - CFLAGS="-g" - fi -else - if test "$GCC" = yes; then - CFLAGS="-O2" - else - CFLAGS= - fi -fi -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5 -$as_echo_n "checking for $CC option to accept ISO C89... " >&6; } -if ${ac_cv_prog_cc_c89+:} false; then : - $as_echo_n "(cached) " >&6 -else - ac_cv_prog_cc_c89=no -ac_save_CC=$CC -cat confdefs.h - <<_ACEOF >conftest.$ac_ext -/* end confdefs.h. */ -#include <stdarg.h> -#include <stdio.h> -struct stat; -/* Most of the following tests are stolen from RCS 5.7's src/conf.sh. */ -struct buf { int x; }; -FILE * (*rcsopen) (struct buf *, struct stat *, int); -static char *e (p, i) - char **p; - int i; -{ - return p[i]; -} -static char *f (char * (*g) (char **, int), char **p, ...) -{ - char *s; - va_list v; - va_start (v,p); - s = g (p, va_arg (v,int)); - va_end (v); - return s; -} - -/* OSF 4.0 Compaq cc is some sort of almost-ANSI by default. It has - function prototypes and stuff, but not '\xHH' hex character constants. - These don't provoke an error unfortunately, instead are silently treated - as 'x'. The following induces an error, until -std is added to get - proper ANSI mode. Curiously '\x00'!='x' always comes out true, for an - array size at least. It's necessary to write '\x00'==0 to get something - that's true only with -std. */ -int osf4_cc_array ['\x00' == 0 ? 1 : -1]; - -/* IBM C 6 for AIX is almost-ANSI by default, but it replaces macro parameters - inside strings and character constants. */ -#define FOO(x) 'x' -int xlc6_cc_array[FOO(a) == 'x' ? 1 : -1]; - -int test (int i, double x); -struct s1 {int (*f) (int a);}; -struct s2 {int (*f) (double a);}; -int pairnames (int, char **, FILE *(*)(struct buf *, struct stat *, int), int, int); -int argc; -char **argv; -int -main () -{ -return f (e, argv, 0) != argv[0] || f (e, argv, 1) != argv[1]; - ; - return 0; -} -_ACEOF -for ac_arg in '' -qlanglvl=extc89 -qlanglvl=ansi -std \ - -Ae "-Aa -D_HPUX_SOURCE" "-Xc -D__EXTENSIONS__" -do - CC="$ac_save_CC $ac_arg" - if ac_fn_c_try_compile "$LINENO"; then : - ac_cv_prog_cc_c89=$ac_arg -fi -rm -f core conftest.err conftest.$ac_objext - test "x$ac_cv_prog_cc_c89" != "xno" && break -done -rm -f conftest.$ac_ext -CC=$ac_save_CC - -fi -# AC_CACHE_VAL -case "x$ac_cv_prog_cc_c89" in - x) - { $as_echo "$as_me:${as_lineno-$LINENO}: result: none needed" >&5 -$as_echo "none needed" >&6; } ;; - xno) - { $as_echo "$as_me:${as_lineno-$LINENO}: result: unsupported" >&5 -$as_echo "unsupported" >&6; } ;; - *) - CC="$CC $ac_cv_prog_cc_c89" - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_prog_cc_c89" >&5 -$as_echo "$ac_cv_prog_cc_c89" >&6; } ;; -esac -if test "x$ac_cv_prog_cc_c89" != xno; then : - -fi - -ac_ext=c -ac_cpp='$CPP $CPPFLAGS' -ac_compile='$CC -c $CFLAGS $CPPFLAGS conftest.$ac_ext >&5' -ac_link='$CC -o conftest$ac_exeext $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS >&5' -ac_compiler_gnu=$ac_cv_c_compiler_gnu - ac_ext=c ac_cpp='$CPP $CPPFLAGS' @@ -5085,6 +4900,7 @@ fi CPPFLAGS="$old_CPPFLAGS" +STP_NEEDS_MINISAT=0 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : @@ -5130,8 +4946,69 @@ _ACEOF else - as_fn_error $? "Could not link with libstp" "$LINENO" 5 + STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5 +$as_echo "Could not link with libstp" >&6; } + +fi + + +if test "X$STP_NEEDS_MINISAT" != X0 ; then + # Need to clear cached result + unset ac_cv_lib_stp_vc_setInterfaceFlags + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 +$as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } +if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_check_lib_save_LIBS=$LIBS +LIBS="-lstp "$STP_LDFLAGS" "-lminisat" $LIBS" +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +/* Override any GCC internal prototype to avoid an error. + Use char because int might match the return type of a GCC + builtin and then its argument prototype would still apply. */ +#ifdef __cplusplus +extern "C" +#endif +char vc_setInterfaceFlags (); +int +main () +{ +return vc_setInterfaceFlags (); + ; + return 0; +} +_ACEOF +if ac_fn_cxx_try_link "$LINENO"; then : + ac_cv_lib_stp_vc_setInterfaceFlags=yes +else + ac_cv_lib_stp_vc_setInterfaceFlags=no +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext +LIBS=$ac_check_lib_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5 +$as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; } +if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then : + cat >>confdefs.h <<_ACEOF +#define HAVE_LIBSTP 1 +_ACEOF + + LIBS="-lstp $LIBS" + +else + + as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5 + +fi + + + STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" +else + STP_LDFLAGS="${STP_LDFLAGS} -lstp" fi @@ -5742,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 0.01, which was +This file was extended by KLEE $as_me 0.2.0, which was generated by GNU Autoconf 2.69. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -5802,13 +5679,14 @@ $config_headers Configuration commands: $config_commands -Report bugs to <daniel@minormatter.com>." +Report bugs to <klee-dev@imperial.ac.uk>. +KLEE home page: <https://klee.github.io>." _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 0.01 +KLEE config.status 0.2.0 configured by $0, generated by GNU Autoconf 2.69, with options \\"\$ac_cs_config\\" diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 97b700c1..32f840f6 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -23,14 +23,14 @@ #include <vector> namespace klee { - class Array; - class CallPathNode; - struct Cell; - struct KFunction; - struct KInstruction; - class MemoryObject; - class PTreeNode; - struct InstructionInfo; +class Array; +class CallPathNode; +struct Cell; +struct KFunction; +struct KInstruction; +class MemoryObject; +class PTreeNode; +struct InstructionInfo; llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); @@ -39,7 +39,7 @@ struct StackFrame { KFunction *kf; CallPathNode *callPathNode; - std::vector<const MemoryObject*> allocas; + std::vector<const MemoryObject *> allocas; Cell *locals; /// Minimum distance to an uncovered instruction once the function @@ -61,56 +61,92 @@ struct StackFrame { ~StackFrame(); }; +/// @brief ExecutionState representing a path under exploration class ExecutionState { public: typedef std::vector<StackFrame> stack_ty; private: // unsupported, use copy constructor - ExecutionState &operator=(const ExecutionState&); - std::map< std::string, std::string > fnAliases; + ExecutionState &operator=(const ExecutionState &); + + std::map<std::string, std::string> fnAliases; public: - bool fakeState; - unsigned depth; - - // pc - pointer to current instruction stream - KInstIterator pc, prevPC; + // Execution - Control Flow specific + + /// @brief Pointer to instruction to be executed after the current + /// instruction + KInstIterator pc; + + /// @brief Pointer to instruction which is currently executed + KInstIterator prevPC; + + /// @brief Stack representing the current instruction stream stack_ty stack; + + /// @brief Remember from which Basic Block control flow arrived + /// (i.e. to select the right phi values) + unsigned incomingBBIndex; + + // Overall state of the state - Data specific + + /// @brief Address space used by this state (e.g. Global and Heap) + AddressSpace addressSpace; + + /// @brief Constraints collected so far ConstraintManager constraints; + + /// Statistics and information + + /// @brief Costs for all queries issued for this state, in seconds mutable double queryCost; + + /// @brief Weight assigned for importance of this state. Can be + /// used for searchers to decide what paths to explore double weight; - AddressSpace addressSpace; - TreeOStream pathOS, symPathOS; + + /// @brief Exploration depth, i.e., number of times KLEE branched for this state + unsigned depth; + + /// @brief History of complete path: represents branches taken to + /// reach/create this state (both concrete and symbolic) + TreeOStream pathOS; + + /// @brief History of symbolic path: represents symbolic branches + /// taken to reach/create this state + TreeOStream symPathOS; + + /// @brief Counts how many instructions were executed since the last new + /// instruction was covered. unsigned instsSinceCovNew; + + /// @brief Whether a new instruction was covered in this state bool coveredNew; - /// Disables forking, set by user code. + /// @brief Disables forking for this state. Set by user code bool forkDisabled; - std::map<const std::string*, std::set<unsigned> > coveredLines; + /// @brief Set containing which lines in which files are covered by this state + std::map<const std::string *, std::set<unsigned> > coveredLines; + + /// @brief Pointer to the process tree of the current state PTreeNode *ptreeNode; - /// ordered list of symbolics: used to generate test cases. + /// @brief Ordered list of symbolics: used to generate test cases. // // FIXME: Move to a shared list structure (not critical). - std::vector< std::pair<const MemoryObject*, const Array*> > symbolics; + std::vector<std::pair<const MemoryObject *, const Array *> > symbolics; - /// Set of used array names. Used to avoid collisions. + /// @brief Set of used array names for this state. Used to avoid collisions. std::set<std::string> arrayNames; - // Used by the checkpoint/rollback methods for fake objects. - // FIXME: not freeing things on branch deletion. - MemoryMap shadowObjects; - - unsigned incomingBBIndex; - std::string getFnAlias(std::string fn); void addFnAlias(std::string old_fn, std::string new_fn); void removeFnAlias(std::string fn); - + private: - ExecutionState() : fakeState(false), ptreeNode(0) {} + ExecutionState() : ptreeNode(0) {} public: ExecutionState(KFunction *kf); @@ -119,24 +155,21 @@ public: // use on structure ExecutionState(const std::vector<ref<Expr> > &assumptions); - ExecutionState(const ExecutionState& state); + ExecutionState(const ExecutionState &state); ~ExecutionState(); - + ExecutionState *branch(); void pushFrame(KInstIterator caller, KFunction *kf); void popFrame(); void addSymbolic(const MemoryObject *mo, const Array *array); - void addConstraint(ref<Expr> e) { - constraints.addConstraint(e); - } + void addConstraint(ref<Expr> e) { constraints.addConstraint(e); } bool merge(const ExecutionState &b); void dumpStack(llvm::raw_ostream &out) const; }; - } #endif diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h index fc86070b..62f514ff 100644 --- a/include/klee/Internal/Module/KInstruction.h +++ b/include/klee/Internal/Module/KInstruction.h @@ -50,7 +50,7 @@ namespace klee { std::vector< std::pair<unsigned, uint64_t> > indices; /// offset - A constant offset to add to the pointer operand to execute the - /// insturction. + /// instruction. uint64_t offset; }; } diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h index 80672b5e..76db4694 100644 --- a/include/klee/Internal/Module/KModule.h +++ b/include/klee/Internal/Module/KModule.h @@ -92,7 +92,7 @@ namespace klee { #endif // Some useful functions to know the address of - llvm::Function *dbgStopPointFn, *kleeMergeFn; + llvm::Function *kleeMergeFn; // Our shadow versions of LLVM structures. std::vector<KFunction*> functions; diff --git a/include/klee/Internal/Support/PrintVersion.h b/include/klee/Internal/Support/PrintVersion.h new file mode 100644 index 00000000..2c375ad2 --- /dev/null +++ b/include/klee/Internal/Support/PrintVersion.h @@ -0,0 +1,17 @@ +//===-- Version.h -----------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_PRINT_VERSION_H +#define KLEE_PRINT_VERSION_H + +namespace klee { + void printVersion(); +} + +#endif diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h index 5229c8c9..14d23536 100644 --- a/include/klee/Internal/System/Time.h +++ b/include/klee/Internal/System/Time.h @@ -10,10 +10,19 @@ #ifndef KLEE_UTIL_TIME_H #define KLEE_UTIL_TIME_H +#include <llvm/Support/TimeValue.h> + namespace klee { namespace util { + + /// Seconds spent by this process in user mode. double getUserTime(); + + /// Wall time in seconds. double getWallTime(); + + /// Wall time as TimeValue object. + llvm::sys::TimeValue getWallTimeVal(); } } diff --git a/include/klee/klee.h b/include/klee/klee.h index ce92ba37..d0980395 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -1,11 +1,11 @@ -//===-- klee.h --------------------------------------------------*- C++ -*-===// +/*===-- klee.h --------------------------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #ifndef __KLEE_H__ #define __KLEE_H__ @@ -18,51 +18,57 @@ extern "C" { #endif /* Add an accesible memory object at a user specified location. It - is the users responsibility to make sure that these memory - objects do not overlap. These memory objects will also - (obviously) not correctly interact with external function - calls. */ + * is the users responsibility to make sure that these memory + * objects do not overlap. These memory objects will also + * (obviously) not correctly interact with external function + * calls. + */ void klee_define_fixed_object(void *addr, size_t nbytes); - /// klee_make_symbolic - Make the contents of the object pointer to by \arg - /// addr symbolic. - /// - /// \arg addr - The start of the object. - /// \arg nbytes - The number of bytes to make symbolic; currently this *must* - /// be the entire contents of the object. - /// \arg name - An optional name, used for identifying the object in messages, - /// output files, etc. + /* klee_make_symbolic - Make the contents of the object pointer to by \arg + * addr symbolic. + * + * \arg addr - The start of the object. + * \arg nbytes - The number of bytes to make symbolic; currently this *must* + * be the entire contents of the object. + * \arg name - An optional name, used for identifying the object in messages, + * output files, etc. + */ void klee_make_symbolic(void *addr, size_t nbytes, const char *name); - /// klee_range - Construct a symbolic value in the signed interval - /// [begin,end). - /// - /// \arg name - An optional name, used for identifying the object in messages, - /// output files, etc. + /* klee_range - Construct a symbolic value in the signed interval + * [begin,end). + * + * \arg name - An optional name, used for identifying the object in messages, + * output files, etc. + */ int klee_range(int begin, int end, const char *name); - /// klee_int - Construct an unconstrained symbolic integer. - /// - /// \arg name - An optional name, used for identifying the object in messages, - /// output files, etc. + /* klee_int - Construct an unconstrained symbolic integer. + * + * \arg name - An optional name, used for identifying the object in messages, + * output files, etc. + */ int klee_int(const char *name); - /// klee_silent_exit - Terminate the current KLEE process without generating a - /// test file. + /* klee_silent_exit - Terminate the current KLEE process without generating a + * test file. + */ __attribute__((noreturn)) void klee_silent_exit(int status); - /// klee_abort - Abort the current KLEE process. + /* klee_abort - Abort the current KLEE process. */ __attribute__((noreturn)) void klee_abort(void); - /// klee_report_error - Report a user defined error and terminate the current - /// KLEE process. - /// - /// \arg file - The filename to report in the error message. - /// \arg line - The line number to report in the error message. - /// \arg message - A string to include in the error message. - /// \arg suffix - The suffix to use for error files. + /* klee_report_error - Report a user defined error and terminate the current + * KLEE process. + * + * \arg file - The filename to report in the error message. + * \arg line - The line number to report in the error message. + * \arg message - A string to include in the error message. + * \arg suffix - The suffix to use for error files. + */ __attribute__((noreturn)) void klee_report_error(const char *file, int line, @@ -104,6 +110,7 @@ extern "C" { void klee_warning(const char *message); void klee_warning_once(const char *message); void klee_prefer_cex(void *object, uintptr_t condition); + void klee_posix_prefer_cex(void *object, uintptr_t condition); void klee_mark_global(void *object); /* Return a possible constant value for the input expression. This @@ -142,6 +149,11 @@ extern "C" { /* Print stack trace. */ void klee_stack_trace(void); + /* Print range for given argument and tagged with name */ + void klee_print_range(const char * name, int arg ); + + /* Merge current states together if possible */ + void klee_merge(); #ifdef __cplusplus } #endif diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 6b0d260a..e90a49f1 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -319,6 +319,7 @@ protected: void printNotEqualExpr(const ref<NeExpr> &e); void printSelectExpr(const ref<SelectExpr> &e, ExprSMTLIBPrinter::SMTLIB_SORT s); + void printAShrExpr(const ref<AShrExpr> &e); // For the set of operators that take sort "s" arguments void printSortArgsExpr(const ref<Expr> &e, diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 5d32c936..6aeaa833 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -66,13 +66,14 @@ StackFrame::~StackFrame() { /***/ -ExecutionState::ExecutionState(KFunction *kf) - : fakeState(false), - depth(0), +ExecutionState::ExecutionState(KFunction *kf) : pc(kf->instructions), prevPC(pc), + queryCost(0.), weight(1), + depth(0), + instsSinceCovNew(0), coveredNew(false), forkDisabled(false), @@ -80,12 +81,8 @@ ExecutionState::ExecutionState(KFunction *kf) pushFrame(0, kf); } -ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) - : fakeState(true), - constraints(assumptions), - queryCost(0.), - ptreeNode(0) { -} +ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) + : constraints(assumptions), queryCost(0.), ptreeNode(0) {} ExecutionState::~ExecutionState() { for (unsigned int i=0; i<symbolics.size(); i++) @@ -100,28 +97,30 @@ ExecutionState::~ExecutionState() { while (!stack.empty()) popFrame(); } -ExecutionState::ExecutionState(const ExecutionState& state) - : fnAliases(state.fnAliases), - fakeState(state.fakeState), - depth(state.depth), +ExecutionState::ExecutionState(const ExecutionState& state): + fnAliases(state.fnAliases), pc(state.pc), prevPC(state.prevPC), stack(state.stack), + incomingBBIndex(state.incomingBBIndex), + + addressSpace(state.addressSpace), constraints(state.constraints), + queryCost(state.queryCost), weight(state.weight), - addressSpace(state.addressSpace), + depth(state.depth), + pathOS(state.pathOS), symPathOS(state.symPathOS), + instsSinceCovNew(state.instsSinceCovNew), coveredNew(state.coveredNew), forkDisabled(state.forkDisabled), coveredLines(state.coveredLines), ptreeNode(state.ptreeNode), symbolics(state.symbolics), - arrayNames(state.arrayNames), - shadowObjects(state.shadowObjects), - incomingBBIndex(state.incomingBBIndex) + arrayNames(state.arrayNames) { for (unsigned int i=0; i<symbolics.size(); i++) symbolics[i].first->refCount++; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c78c9f8a..49e526f5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -140,10 +140,6 @@ namespace { cl::desc("Dump test cases for all active states on exit (default=on)")); cl::opt<bool> - NoPreferCex("no-prefer-cex", - cl::init(false)); - - cl::opt<bool> RandomizeFork("randomize-fork", cl::init(false), cl::desc("Randomly swap the true and false states on a fork (default=off)")); @@ -2592,9 +2588,7 @@ void Executor::run(ExecutionState &initialState) { unsigned numStates = states.size(); unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs); - if (MaxMemoryInhibit) - klee_warning("killing %d states (over memory cap)", - toKill); + klee_warning("killing %d states (over memory cap)", toKill); std::vector<ExecutionState*> arr(states.begin(), states.end()); for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) { @@ -3484,20 +3478,33 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); - if (!NoPreferCex) { - for (unsigned i = 0; i != state.symbolics.size(); ++i) { - const MemoryObject *mo = state.symbolics[i].first; - std::vector< ref<Expr> >::const_iterator pi = - mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); - for (; pi != pie; ++pi) { - bool mustBeTrue; - bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), - mustBeTrue); - if (!success) break; - if (!mustBeTrue) tmp.addConstraint(*pi); - } - if (pi!=pie) break; - } + + // Go through each byte in every test case and attempt to restrict + // it to the constraints contained in cexPreferences. (Note: + // usually this means trying to make it an ASCII character (0-127) + // and therefore human readable. It is also possible to customize + // the preferred constraints. See test/Features/PreferCex.c for + // an example) While this process can be very expensive, it can + // also make understanding individual test cases much easier. + for (unsigned i = 0; i != state.symbolics.size(); ++i) { + const MemoryObject *mo = state.symbolics[i].first; + std::vector< ref<Expr> >::const_iterator pi = + mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); + for (; pi != pie; ++pi) { + bool mustBeTrue; + // Attempt to bound byte to constraints held in cexPreferences + bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), + mustBeTrue); + // If it isn't possible to constrain this particular byte in the desired + // way (normally this would mean that the byte can't be constrained to + // be between 0 and 127 without making the entire constraint list UNSAT) + // then just continue on to the next byte. + if (!success) break; + // If the particular constraint operated on in this iteration through + // the loop isn't implied then add it to the list of constraints. + if (!mustBeTrue) tmp.addConstraint(*pi); + } + if (pi!=pie) break; } std::vector< std::vector<unsigned char> > values; diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 5f9f8dc6..ecc9912e 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -10,13 +10,6 @@ #include "ExternalDispatcher.h" #include "klee/Config/Version.h" -// Ugh. -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION - #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Module.h" #include "llvm/IR/Constants.h" diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 1dd1e1fd..07c292a0 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -468,7 +468,7 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const { // Otherwise, follow the slow general case. unsigned NumBytes = width / 8; - assert(width == NumBytes * 8 && "Invalid write size!"); + assert(width == NumBytes * 8 && "Invalid read size!"); ref<Expr> Res(0); for (unsigned i = 0; i != NumBytes; ++i) { unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1); @@ -488,7 +488,7 @@ ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const { // Otherwise, follow the slow general case. unsigned NumBytes = width / 8; - assert(width == NumBytes * 8 && "Invalid write size!"); + assert(width == NumBytes * 8 && "Invalid width for read size!"); ref<Expr> Res(0); for (unsigned i = 0; i != NumBytes; ++i) { unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index f06ae4f5..52abff5f 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -22,6 +22,8 @@ #include "Executor.h" #include "MemoryManager.h" +#include "klee/CommandLine.h" + #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Module.h" #else @@ -34,6 +36,15 @@ using namespace llvm; using namespace klee; +namespace { + cl::opt<bool> + ReadablePosix("readable-posix-inputs", + cl::init(false), + cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. " + "Note: option is expensive when creating lots of tests (default=false)")); +} + + /// \todo Almost all of the demands in this file should be replaced /// with terminateState calls. @@ -81,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("klee_mark_global", handleMarkGlobal, false), add("klee_merge", handleMerge, false), add("klee_prefer_cex", handlePreferCex, false), + add("klee_posix_prefer_cex", handlePosixPreferCex, false), add("klee_print_expr", handlePrintExpr, false), add("klee_print_range", handlePrintRange, false), add("klee_set_forking", handleSetForking, false), @@ -222,7 +234,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr); if (!state.addressSpace.resolveOne(address, op)) assert(0 && "XXX out of bounds / multiple resolution unhandled"); - bool res; + bool res __attribute__ ((unused)); assert(executor.solver->mustBeTrue(state, EqExpr::create(address, op.first->getBaseExpr()), @@ -376,7 +388,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth())); bool res; - bool success = executor.solver->mustBeFalse(state, e, res); + bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { executor.terminateStateOnError(state, @@ -416,6 +428,13 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state, rl[0].first.first->cexPreferences.push_back(cond); } +void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (ReadablePosix) + return handlePreferCex(state, target, arguments); +} + void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { @@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, if (!isa<ConstantExpr>(arguments[1])) { // FIXME: Pull into a unique value method? ref<ConstantExpr> value; - bool success = executor.solver->getValue(state, arguments[1], value); + bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value); assert(success && "FIXME: Unhandled solver failure"); bool res; success = executor.solver->mustBeTrue(state, @@ -679,7 +698,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, // FIXME: Type coercion should be done consistently somewhere. bool res; - bool success = + bool success __attribute__ ((unused)) = executor.solver->mustBeTrue(*s, EqExpr::create(ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index d52b8fc5..2dfdde43 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -120,6 +120,7 @@ namespace klee { HANDLER(handleNew); HANDLER(handleNewArray); HANDLER(handlePreferCex); + HANDLER(handlePosixPreferCex); HANDLER(handlePrintExpr); HANDLER(handlePrintRange); HANDLER(handleRange); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 0e564fe5..cf8a1654 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -27,13 +27,6 @@ #include "UserSearcher.h" #include "../Solver/SolverStats.h" -// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs. -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION - #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) #include "llvm/IR/BasicBlock.h" #include "llvm/IR/Function.h" diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 037b23f3..b70bcbef 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -13,10 +13,11 @@ #include "klee/ExecutionState.h" #include "klee/Solver.h" #include "klee/Statistics.h" +#include "klee/Internal/System/Time.h" #include "CoreStats.h" -#include "llvm/Support/Process.h" +#include "llvm/Support/TimeValue.h" using namespace klee; using namespace llvm; @@ -31,15 +32,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->evaluate(Query(state.constraints, expr), result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; @@ -55,15 +55,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->mustBeTrue(Query(state.constraints, expr), result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; @@ -102,15 +101,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->getValue(Query(state.constraints, expr), result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; @@ -127,14 +125,13 @@ TimingSolver::getInitialValues(const ExecutionState& state, if (objects.empty()) return true; - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); bool success = solver->getInitialValues(Query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index ae4563f4..dbdfd999 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -23,6 +23,14 @@ using namespace klee; +namespace { + llvm::cl::opt<bool> + RewriteEqualities("rewrite-equalities", + llvm::cl::init(true), + llvm::cl::desc("Rewrite existing constraints when an equality with a constant is added (default=on)")); +} + + class ExprReplaceVisitor : public ExprVisitor { private: ref<Expr> src, dst; @@ -118,13 +126,7 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const { } void ConstraintManager::addConstraintInternal(ref<Expr> e) { - // rewrite any known equalities - - // XXX should profile the effects of this and the overhead. - // traversing the constraints looking for equalities is hardly the - // slowest thing we do, but it is probably nicer to have a - // ConstraintSet ADT which efficiently remembers obvious patterns - // (byte-constant comparison). + // rewrite any known equalities and split Ands into different conjuncts switch (e->getKind()) { case Expr::Constant: @@ -141,10 +143,17 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) { } case Expr::Eq: { - BinaryExpr *be = cast<BinaryExpr>(e); - if (isa<ConstantExpr>(be->left)) { - ExprReplaceVisitor visitor(be->right, be->left); - rewriteConstraints(visitor); + if (RewriteEqualities) { + // XXX: should profile the effects of this and the overhead. + // traversing the constraints looking for equalities is hardly the + // slowest thing we do, but it is probably nicer to have a + // ConstraintSet ADT which efficiently remembers obvious patterns + // (byte-constant comparison). + BinaryExpr *be = cast<BinaryExpr>(e); + if (isa<ConstantExpr>(be->left)) { + ExprReplaceVisitor visitor(be->right, be->left); + rewriteConstraints(visitor); + } } constraints.push_back(e); break; diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index c780ae90..e8e9a253 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -255,7 +255,10 @@ void ExprSMTLIBPrinter::printFullExpression( * type T. */ printLogicalOrBitVectorExpr(e, expectedSort); + return; + case Expr::AShr: + printAShrExpr(cast<AShrExpr>(e)); return; default: @@ -334,6 +337,73 @@ void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) { *p << ")"; } +void ExprSMTLIBPrinter::printAShrExpr(const ref<AShrExpr> &e) { + // There is a difference between AShr and SMT-LIBv2's + // bvashr function when the shift amount is >= the bit width + // so we need to treat it specially here. + // + // Technically this is undefined behaviour for LLVM's ashr operator + // but currently llvm::APInt:ashr(...) will emit 0 if the shift amount + // is >= the bit width but this does not match how SMT-LIBv2's bvashr + // behaves as demonstrates by the following query + // + // (declare-fun x () (_ BitVec 32)) + // (declare-fun y () (_ BitVec 32)) + // (declare-fun result () (_ BitVec 32)) + // (assert (bvuge y (_ bv32 32))) + // (assert (= result (bvashr x y))) + // (assert (distinct (_ bv0 32) result)) + // (check-sat) + // sat + // + // Our solution is to instead emit + // + // (ite (bvuge shift_amount bit_width) + // (_ bv0 bitwidth) + // (bvashr value_to_shift shift_amount) + // ) + // + + Expr::Width bitWidth = e->getKid(0)->getWidth(); + assert(bitWidth > 0 && "Invalid bit width"); + ref<Expr> bitWidthExpr = ConstantExpr::create(bitWidth, bitWidth); + ref<Expr> zeroExpr = ConstantExpr::create(0, bitWidth); + + // FIXME: we print e->getKid(1) twice and it might not get + // abbreviated + *p << "(ite"; + p->pushIndent(); + printSeperator(); + + *p << "(bvuge"; + p->pushIndent(); + printSeperator(); + printExpression(e->getKid(1), SORT_BITVECTOR); + printSeperator(); + printExpression(bitWidthExpr, SORT_BITVECTOR); + p->popIndent(); + printSeperator(); + *p << ")"; + + printSeperator(); + printExpression(zeroExpr, SORT_BITVECTOR); + printSeperator(); + + *p << "(bvashr"; + p->pushIndent(); + printSeperator(); + printExpression(e->getKid(0), SORT_BITVECTOR); + printSeperator(); + printExpression(e->getKid(1), SORT_BITVECTOR); + p->popIndent(); + printSeperator(); + *p << ")"; + + p->popIndent(); + printSeperator(); + *p << ")"; +} + const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) { switch (e->getKind()) { @@ -373,8 +443,7 @@ const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) { return "bvshl"; case Expr::LShr: return "bvlshr"; - case Expr::AShr: - return "bvashr"; + // AShr is not supported here. See printAShrExpr() case Expr::Eq: return "="; diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp index d9145a1e..12e5479b 100644 --- a/lib/Module/RaiseAsm.cpp +++ b/lib/Module/RaiseAsm.cpp @@ -66,17 +66,18 @@ bool RaiseAsmPass::runOnModule(Module &M) { std::string HostTriple = llvm::sys::getHostTriple(); #endif const Target *NativeTarget = TargetRegistry::lookupTarget(HostTriple, Err); + TargetMachine * TM = 0; if (NativeTarget == 0) { llvm::errs() << "Warning: unable to select native target: " << Err << "\n"; TLI = 0; } else { #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "", + TM = NativeTarget->createTargetMachine(HostTriple, "", "", TargetOptions()); #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) - TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", ""); + TM = NativeTarget->createTargetMachine(HostTriple, "", ""); #else - TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, ""); + TM = NativeTarget->createTargetMachine(HostTriple, ""); #endif TLI = TM->getTargetLowering(); } @@ -91,5 +92,8 @@ bool RaiseAsmPass::runOnModule(Module &M) { } } + if (TM) + delete TM; + return changed; } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index df7fffc5..d51c1695 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -35,6 +35,11 @@ namespace { cl::init(false)); cl::opt<bool> + CexCacheSuperSet("cex-cache-superset", + cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"), + cl::init(false)); + + cl::opt<bool> CexCacheExperimental("cex-cache-exp", cl::init(false)); } @@ -124,8 +129,10 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { if (CexCacheTryAll) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); - + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); + // Otherwise, look for a subset which is unsatisfiable, see below. if (!lookup) lookup = cache.findSubset(key, NullAssignment()); @@ -151,7 +158,9 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); // Otherwise, look for a subset which is unsatisfiable -- if the subset is // unsatisfiable then no additional constraints can produce a valid diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 6d7dd8b7..a5e4c5ad 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -51,11 +51,6 @@ namespace { STPArrayExprHash::~STPArrayExprHash() { - - // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run; - // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled. - - /* for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) { ::VCExpr array_expr = it->second; if (array_expr) { @@ -63,16 +58,16 @@ STPArrayExprHash::~STPArrayExprHash() { array_expr = 0; } } - - - for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) { + + + for (UpdateNodeHashConstIter it = _update_node_hash.begin(); + it != _update_node_hash.end(); ++it) { ::VCExpr un_expr = it->second; if (un_expr) { ::vc_DeleteExpr(un_expr); un_expr = 0; } } - */ } /***/ @@ -218,10 +213,9 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) { } // If overshifting, shift to zero - res = vc_iteExpr(vc, - vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), - res, - bvZero(width)); + ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); + + res = vc_iteExpr(vc, ex, res, bvZero(width)); return res; } @@ -239,8 +233,9 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { } // If overshifting, shift to zero + ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); res = vc_iteExpr(vc, - vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + ex, res, bvZero(width)); return res; @@ -269,8 +264,9 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { } // If overshifting, shift to zero + ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); res = vc_iteExpr(vc, - vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + ex, res, bvZero(width)); return res; diff --git a/lib/Support/Makefile b/lib/Support/Makefile index 67272908..2b1b104c 100644 --- a/lib/Support/Makefile +++ b/lib/Support/Makefile @@ -14,4 +14,33 @@ DONT_BUILD_RELINKED=1 BUILD_ARCHIVE=1 NO_INSTALL=1 +# FIXME: This is nasty. We don't want to rebuild this library everytime +# but this was the only way I could find to make the build work. +# +# Note this rule has to go here so it is run first. +CompileTimeInfoFile:=../../include/klee/Config/CompileTimeInfo.h +all-local:: $(CompileTimeInfoFile) + include $(LEVEL)/Makefile.common + + +GIT_PRESENT:=$(shell [ -d "$(PROJ_SRC_ROOT)/.git" ] && echo 1 || echo 0) + +ifeq ($(GIT_PRESENT),1) +GIT_TAGS:=$(shell cd $(PROJ_SRC_ROOT); git describe --tags 2> /dev/null 1>&2 && echo 1 || echo 0) +else +GIT_TAGS:=0 +endif + +.PHONY: $(CompileTimeInfoFile) +$(CompileTimeInfoFile): + $(Verb) echo "Regenerating $(CompileTimeInfoFile)" + $(Verb) echo '#define KLEE_BUILD_MODE "$(BuildMode)"' > $(CompileTimeInfoFile) +ifeq ($(GIT_PRESENT),1) + $(Verb) echo '#define KLEE_BUILD_REVISION "'$(shell cd $(PROJ_SRC_ROOT); git rev-parse HEAD)'"' >> \ + $(CompileTimeInfoFile) +endif +ifeq ($(GIT_TAGS),1) + $(Verb) echo '#define KLEE_BUILD_TAG "'$(shell cd $(PROJ_SRC_ROOT); git describe --tags)'"' >> \ + $(CompileTimeInfoFile) +endif diff --git a/lib/Support/PrintVersion.cpp b/lib/Support/PrintVersion.cpp new file mode 100644 index 00000000..b4ff9811 --- /dev/null +++ b/lib/Support/PrintVersion.cpp @@ -0,0 +1,34 @@ +//===-- PrintVersion.cpp --------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Internal/Support/PrintVersion.h" +#include "klee/Config/config.h" +#include "llvm/Support/raw_ostream.h" +#include "llvm/Support/CommandLine.h" + +#include "klee/Config/CompileTimeInfo.h" + +void klee::printVersion() +{ + llvm::outs() << PACKAGE_STRING " (" PACKAGE_URL ")\n"; + llvm::outs() << " Built " __DATE__ " (" __TIME__ ")\n"; + llvm::outs() << " Build mode: " << KLEE_BUILD_MODE "\n"; + llvm::outs() << " Build revision: "; +#ifdef KLEE_BUILD_REVISION + llvm::outs() << KLEE_BUILD_REVISION "\n"; +#else + llvm::outs() << "unknown\n"; +#endif +#ifdef KLEE_BUILD_TAG + llvm::outs() << " Build tag: " << KLEE_BUILD_TAG "\n"; +#endif + // Show LLVM version information + llvm::outs() << "\n"; + llvm::cl::PrintVersionMessage(); +} diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp index 909e07da..be5eaf18 100644 --- a/lib/Support/Time.cpp +++ b/lib/Support/Time.cpp @@ -10,6 +10,7 @@ #include "klee/Config/Version.h" #include "klee/Internal/System/Time.h" +#include "llvm/Support/TimeValue.h" #include "llvm/Support/Process.h" using namespace llvm; @@ -22,7 +23,10 @@ double util::getUserTime() { } double util::getWallTime() { - sys::TimeValue now(0,0),user(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); - return (now.seconds() + (double) now.nanoseconds() * 1e-9); + sys::TimeValue now = getWallTimeVal(); + return (now.seconds() + ((double) now.nanoseconds() * 1e-9)); +} + +sys::TimeValue util::getWallTimeVal() { + return sys::TimeValue::now(); } diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp index c61a90a3..da969810 100644 --- a/lib/Support/Timer.cpp +++ b/lib/Support/Timer.cpp @@ -10,19 +10,15 @@ #include "klee/Config/Version.h" #include "klee/Internal/Support/Timer.h" -#include "llvm/Support/Process.h" +#include "klee/Internal/System/Time.h" using namespace klee; using namespace llvm; WallTimer::WallTimer() { - sys::TimeValue now(0,0),user(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); - startMicroseconds = now.usec(); + startMicroseconds = util::getWallTimeVal().usec(); } uint64_t WallTimer::check() { - sys::TimeValue now(0,0),user(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); - return now.usec() - startMicroseconds; + return util::getWallTimeVal().usec() - startMicroseconds; } diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile index 3c6b01b3..49f8f9cc 100644 --- a/runtime/Intrinsic/Makefile +++ b/runtime/Intrinsic/Makefile @@ -9,15 +9,24 @@ LEVEL=../.. +# Needed for LLVM version +include $(LEVEL)/Makefile.config + +ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True) +# For these versions of LLVM KLEE expects kleeRuntimeIntrinsic to be a LLVM module rather than an archive +MODULE_NAME=kleeRuntimeIntrinsic +else +# KLEE built against older versions of LLVM expects a library archive instead +BYTECODE_LIBRARY=1 LIBRARYNAME=kleeRuntimeIntrinsic +endif + DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 -BYTECODE_LIBRARY=1 # Don't strip debug info from the module. DEBUG_RUNTIME=1 NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 -MODULE_NAME=kleeRuntimeIntrinsic C.Flags += -fno-builtin include $(LEVEL)/Makefile.common diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c index 56f0f9dc..6ea1e02e 100644 --- a/runtime/Intrinsic/klee_int.c +++ b/runtime/Intrinsic/klee_int.c @@ -8,7 +8,7 @@ //===----------------------------------------------------------------------===// #include <assert.h> -#include <klee/klee.h> +#include "klee/klee.h" int klee_int(const char *name) { int x; diff --git a/runtime/POSIX/Makefile b/runtime/POSIX/Makefile index 9a42f5c0..1e570098 100644 --- a/runtime/POSIX/Makefile +++ b/runtime/POSIX/Makefile @@ -11,10 +11,10 @@ LEVEL=../.. LIBRARYNAME=kleeRuntimePOSIX DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 BYTECODE_LIBRARY=1 # Don't strip debug info from the module. DEBUG_RUNTIME=1 NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index d976b0b4..8b69fd04 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -74,20 +74,20 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, reasonable. */ klee_assume((s->st_blksize & ~0xFFFF) == 0); - klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); - klee_prefer_cex(s, s->st_dev == defaults->st_dev); - klee_prefer_cex(s, s->st_rdev == defaults->st_rdev); - klee_prefer_cex(s, (s->st_mode&0700) == 0600); - klee_prefer_cex(s, (s->st_mode&0070) == 0020); - klee_prefer_cex(s, (s->st_mode&0007) == 0002); - klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); - klee_prefer_cex(s, s->st_nlink == 1); - klee_prefer_cex(s, s->st_uid == defaults->st_uid); - klee_prefer_cex(s, s->st_gid == defaults->st_gid); - klee_prefer_cex(s, s->st_blksize == 4096); - klee_prefer_cex(s, s->st_atime == defaults->st_atime); - klee_prefer_cex(s, s->st_mtime == defaults->st_mtime); - klee_prefer_cex(s, s->st_ctime == defaults->st_ctime); + klee_posix_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777))); + klee_posix_prefer_cex(s, s->st_dev == defaults->st_dev); + klee_posix_prefer_cex(s, s->st_rdev == defaults->st_rdev); + klee_posix_prefer_cex(s, (s->st_mode&0700) == 0600); + klee_posix_prefer_cex(s, (s->st_mode&0070) == 0020); + klee_posix_prefer_cex(s, (s->st_mode&0007) == 0002); + klee_posix_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG); + klee_posix_prefer_cex(s, s->st_nlink == 1); + klee_posix_prefer_cex(s, s->st_uid == defaults->st_uid); + klee_posix_prefer_cex(s, s->st_gid == defaults->st_gid); + klee_posix_prefer_cex(s, s->st_blksize == 4096); + klee_posix_prefer_cex(s, s->st_atime == defaults->st_atime); + klee_posix_prefer_cex(s, s->st_mtime == defaults->st_mtime); + klee_posix_prefer_cex(s, s->st_ctime == defaults->st_ctime); s->st_size = dfile->size; s->st_blocks = 8; diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index 2a6b6f68..cbcf31f4 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -67,7 +67,7 @@ static char *__get_sym_str(int numChars, char *name) { klee_make_symbolic(s, numChars+1, name); for (i=0; i<numChars; i++) - klee_prefer_cex(s, __isprint(s[i])); + klee_posix_prefer_cex(s, __isprint(s[i])); s[numChars] = '\0'; return s; diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile index eca63169..d059ba8a 100755 --- a/runtime/klee-libc/Makefile +++ b/runtime/klee-libc/Makefile @@ -9,14 +9,23 @@ LEVEL=../.. -LIBRARYNAME=klee-libc +# Needed for LLVM version +include $(LEVEL)/Makefile.config + +ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True) +# For these versions of LLVM KLEE expects klee-libc to be a LLVM module rather than an archive MODULE_NAME=klee-libc -#DONT_BUILD_RELINKED=1 +else +# KLEE built against older versions of LLVM expect a library archive instead BYTECODE_LIBRARY=1 -MODULE_NAME=klee-libc +LIBRARYNAME=klee-libc +endif + +#DONT_BUILD_RELINKED=1 # Don't strip debug info from the module. DEBUG_RUNTIME=1 #NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some # builtins. diff --git a/runtime/klee-libc/__cxa_atexit.c b/runtime/klee-libc/__cxa_atexit.c index e7982848..990b645d 100644 --- a/runtime/klee-libc/__cxa_atexit.c +++ b/runtime/klee-libc/__cxa_atexit.c @@ -1,11 +1,11 @@ -//===-- __cxa_atexit.c ----------------------------------------------------===// +/*===-- __cxa_atexit.c ----------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include "klee/klee.h" diff --git a/runtime/klee-libc/abort.c b/runtime/klee-libc/abort.c index 0332d095..741bcf82 100644 --- a/runtime/klee-libc/abort.c +++ b/runtime/klee-libc/abort.c @@ -1,11 +1,11 @@ -//===-- abort.c -----------------------------------------------------------===// +/*===-- abort.c -----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/atexit.c b/runtime/klee-libc/atexit.c index c71b2cd6..7b3b53b5 100644 --- a/runtime/klee-libc/atexit.c +++ b/runtime/klee-libc/atexit.c @@ -1,11 +1,11 @@ -//===-- atexit.c ----------------------------------------------------------===// +/*==-- atexit.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int __cxa_atexit(void (*fn)(void*), void *arg, diff --git a/runtime/klee-libc/calloc.c b/runtime/klee-libc/calloc.c index 30b88b30..1466fc07 100644 --- a/runtime/klee-libc/calloc.c +++ b/runtime/klee-libc/calloc.c @@ -1,16 +1,16 @@ -//===-- calloc.c ----------------------------------------------------------===// +/*===-- calloc.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> #include <string.h> -// DWD - I prefer to be internal +/* DWD - I prefer to be internal */ #if 0 void *calloc(size_t nmemb, size_t size) { unsigned nbytes = nmemb * size; @@ -19,7 +19,8 @@ void *calloc(size_t nmemb, size_t size) { memset(addr, 0, nbytes); return addr; } -// Always reallocate. + +/* Always reallocate. */ void *realloc(void *ptr, size_t nbytes) { if(!ptr) return malloc(nbytes); @@ -30,14 +31,14 @@ void *realloc(void *ptr, size_t nbytes) { } unsigned copy_nbytes = klee_get_obj_size(ptr); - //printf("REALLOC: current object = %d bytes!\n", copy_nbytes); + /* printf("REALLOC: current object = %d bytes!\n", copy_nbytes); */ void *addr = malloc(nbytes); if(addr) { - // shrinking + /* shrinking */ if(copy_nbytes > nbytes) copy_nbytes = nbytes; - //printf("REALLOC: copying = %d bytes!\n", copy_nbytes); + /* printf("REALLOC: copying = %d bytes!\n", copy_nbytes); */ memcpy(addr, ptr, copy_nbytes); free(ptr); } diff --git a/runtime/klee-libc/htonl.c b/runtime/klee-libc/htonl.c index 521ef5d6..777ecf94 100644 --- a/runtime/klee-libc/htonl.c +++ b/runtime/klee-libc/htonl.c @@ -1,11 +1,11 @@ -//===-- htonl.c -----------------------------------------------------------===// +/*===-- htonl.c -----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <sys/types.h> #include <sys/param.h> @@ -16,7 +16,7 @@ #undef ntohs #undef ntohl -// Make sure we can recognize the endianness. +/* Make sure we can recognize the endianness. */ #if (!defined(BYTE_ORDER) || !defined(BIG_ENDIAN) || !defined(LITTLE_ENDIAN)) #error "Unknown platform endianness!" #endif diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c index 181aedaa..44e5cea2 100644 --- a/runtime/klee-libc/klee-choose.c +++ b/runtime/klee-libc/klee-choose.c @@ -1,11 +1,11 @@ -//===-- klee-choose.c -----------------------------------------------------===// +/*===-- klee-choose.c -----------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include "klee/klee.h" @@ -13,7 +13,7 @@ uintptr_t klee_choose(uintptr_t n) { uintptr_t x; klee_make_symbolic(&x, sizeof x, "klee_choose"); - // NB: this will *not* work if they don't compare to n values. + /* NB: this will *not* work if they don't compare to n values. */ if(x >= n) klee_silent_exit(0); return x; diff --git a/runtime/klee-libc/memcpy.c b/runtime/klee-libc/memcpy.c index 7f7f133d..c7c6e6d3 100644 --- a/runtime/klee-libc/memcpy.c +++ b/runtime/klee-libc/memcpy.c @@ -1,11 +1,11 @@ -//===-- memcpy.c ----------------------------------------------------------===// +/*===-- memcpy.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/memmove.c b/runtime/klee-libc/memmove.c index c6e1ada9..3e86de02 100644 --- a/runtime/klee-libc/memmove.c +++ b/runtime/klee-libc/memmove.c @@ -1,11 +1,11 @@ -//===-- memmove.c ---------------------------------------------------------===// +/*===-- memmove.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/mempcpy.c b/runtime/klee-libc/mempcpy.c index 31e142d9..31712251 100644 --- a/runtime/klee-libc/mempcpy.c +++ b/runtime/klee-libc/mempcpy.c @@ -1,11 +1,11 @@ -//===-- mempcpy.c ---------------------------------------------------------===// +/*===-- mempcpy.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/memset.c b/runtime/klee-libc/memset.c index ee9ecb87..81025d32 100644 --- a/runtime/klee-libc/memset.c +++ b/runtime/klee-libc/memset.c @@ -1,11 +1,11 @@ -//===-- memset.c ----------------------------------------------------------===// +/*===-- memset.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdlib.h> diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c index 497402a6..bee2d2d7 100644 --- a/runtime/klee-libc/putchar.c +++ b/runtime/klee-libc/putchar.c @@ -1,16 +1,16 @@ -//===-- putchar.c ---------------------------------------------------------===// +/*===-- putchar.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <stdio.h> #include <unistd.h> -// Some header may #define putchar. +/* Some header may #define putchar. */ #undef putchar int putchar(int c) { diff --git a/runtime/klee-libc/strchr.c b/runtime/klee-libc/strchr.c index 33f97bea..50f1b9f4 100644 --- a/runtime/klee-libc/strchr.c +++ b/runtime/klee-libc/strchr.c @@ -1,11 +1,11 @@ -//===-- strchr.c ----------------------------------------------------------===// +/*===-- strchr.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ char *strchr(const char *p, int ch) { char c; diff --git a/runtime/klee-libc/strcmp.c b/runtime/klee-libc/strcmp.c index 6b8c4e85..cdb002c7 100644 --- a/runtime/klee-libc/strcmp.c +++ b/runtime/klee-libc/strcmp.c @@ -1,11 +1,11 @@ -//===-- strcmp.c ----------------------------------------------------------===// +/*===-- strcmp.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int strcmp(const char *a, const char *b) { while (*a && *a == *b) diff --git a/runtime/klee-libc/strcoll.c b/runtime/klee-libc/strcoll.c index 73d59f89..8f78b0b3 100644 --- a/runtime/klee-libc/strcoll.c +++ b/runtime/klee-libc/strcoll.c @@ -1,15 +1,15 @@ -//===-- strcoll.c ---------------------------------------------------------===// +/*===-- strcoll.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <string.h> -// according to the manpage, this is equiv in the POSIX/C locale. +/* according to the manpage, this is equiv in the POSIX/C locale. */ int strcoll(const char *s1, const char *s2) { return strcmp(s1,s2); } diff --git a/runtime/klee-libc/strcpy.c b/runtime/klee-libc/strcpy.c index 0fbaf9a7..d1ec67b8 100644 --- a/runtime/klee-libc/strcpy.c +++ b/runtime/klee-libc/strcpy.c @@ -1,11 +1,11 @@ -//===-- strcpy.c ----------------------------------------------------------===// +/*===-- strcpy.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ char *strcpy(char *to, const char *from) { char *start = to; diff --git a/runtime/klee-libc/strlen.c b/runtime/klee-libc/strlen.c index e298410c..33846134 100644 --- a/runtime/klee-libc/strlen.c +++ b/runtime/klee-libc/strlen.c @@ -1,11 +1,11 @@ -//===-- strlen.c ----------------------------------------------------------===// +/*===-- strlen.c ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <string.h> diff --git a/runtime/klee-libc/strrchr.c b/runtime/klee-libc/strrchr.c index 01128b48..4d51769b 100644 --- a/runtime/klee-libc/strrchr.c +++ b/runtime/klee-libc/strrchr.c @@ -1,11 +1,11 @@ -//===-- strrchr.c ---------------------------------------------------------===// +/*===-- strrchr.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ #include <string.h> diff --git a/runtime/klee-libc/tolower.c b/runtime/klee-libc/tolower.c index 265f5deb..a311f2010 100644 --- a/runtime/klee-libc/tolower.c +++ b/runtime/klee-libc/tolower.c @@ -1,11 +1,11 @@ -//===-- tolower.c ---------------------------------------------------------===// +/*===-- tolower.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int tolower(int ch) { if ( (unsigned int)(ch - 'A') < 26u ) diff --git a/runtime/klee-libc/toupper.c b/runtime/klee-libc/toupper.c index 37e5f9d6..5030b5cc 100644 --- a/runtime/klee-libc/toupper.c +++ b/runtime/klee-libc/toupper.c @@ -1,11 +1,11 @@ -//===-- toupper.c ---------------------------------------------------------===// +/*===-- toupper.c ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // -//===----------------------------------------------------------------------===// +//===----------------------------------------------------------------------===*/ int toupper(int ch) { if ( (unsigned int)(ch - 'a') < 26u ) diff --git a/runtime/klee-uclibc/Makefile b/runtime/klee-uclibc/Makefile index e166cfbc..1b5ea682 100644 --- a/runtime/klee-uclibc/Makefile +++ b/runtime/klee-uclibc/Makefile @@ -47,8 +47,8 @@ uninstall:: remove_klee_uclibc copy_klee_uclibc: @echo "Installing klee-uclibc archive" - $(Verb) $(CP) $(KLEE_UCLIBC_BCA) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME) + $(Verb) $(CP) $(KLEE_UCLIBC_BCA) $(BYTECODE_DESTINATION)/$(KLEE_UCLIBC_BCA_NAME) remove_klee_uclibc: @echo "Removing klee-uclibc archive" - $(Verb) $(RM) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME) + $(Verb) $(RM) $(BYTECODE_DESTINATION)/$(KLEE_UCLIBC_BCA_NAME) diff --git a/scripts/coverageServer.py b/scripts/coverageServer.py new file mode 100644 index 00000000..db708545 --- /dev/null +++ b/scripts/coverageServer.py @@ -0,0 +1,100 @@ +#!/usr/bin/python +from flask import * +from functools import wraps +from subprocess import call +from werkzeug import secure_filename +import json +import time +import os +import shutil +import tarfile + +##################### DESCRIPTION ################# +#This is the server to which coverage data is uploaded from travisCI. +#need to replace USER and PASSWORD with an actual username and passsword used to autheticate in /api +#Stored here, because it needs to be in version control somewhere +# +# Example of running the server +#uwsgi -s 127.0.0.1:3013 -w coverageServer:app --chmod=666 --post-buffering=81 --daemonize ./log +#where nginx is expecting uwsgi traffic at 127.0.0.1:3013 + + +#sample upload command +#curl --form "file=@coverage.tar.gz" -u USER:PASSWORD localhost:5000/api + + + + +UPLOAD_FOLDER = '.' + +#enable upload only every 5 minutes + +app = Flask(__name__) +app.config['UPLOAD_FOLDER'] = UPLOAD_FOLDER +app.config['MAX_CONTENT_LENGTH'] = 16 * 1024 * 1024 + +TIMEOUT = 0 + + +def check_auth(username, password): + return username == 'USER' and password == 'PASSWORD' + + +def authenticate(): + """Sends a 401 response that enables basic auth""" + return Response( + 'Could not verify your access level for that URL.\n' + 'You have to login with proper credentials', 401, + {'WWW-Authenticate': 'Basic realm="Login Required"'}) + + +def requires_auth(f): + @wraps(f) + def decorated(*args, **kwargs): + auth = request.authorization + if not auth or not check_auth(auth.username, auth.password): + return authenticate() + return f(*args, **kwargs) + return decorated + +@app.route("/<path:path>") +def serve_page(path): + return send_from_directory('./coverage', path) + +#check that the tar file has only one efolder named coverage +def check_tar(tar): + coverage_dir_num = 0 + for tarinfo in tar.getmembers(): + if 'coverage' in tarinfo.name and tarinfo.isdir(): + coverage_dir_num += 1 + elif not 'coverage/' in tarinfo.name: + return False + return coverage_dir_num == 1 + +@app.route("/api", methods=['POST']) +@requires_auth +def upload_coverage(): + global TIMEOUT +#only allow uploads every 5 minutes (a bit less than usuall travisCI build) + if time.time() - TIMEOUT < 300: + return "Time Out" + if request.method == 'POST': + file = request.files['file'] + if file.filename == "coverage.tar.gz": + filename = secure_filename(file.filename) + file.save(os.path.join(app.config['UPLOAD_FOLDER'], filename)) + tar = tarfile.open("./coverage.tar.gz") + if not check_tar(tar): + return "NOK" +#remove the previous coverage folder if it existis + if os.path.isdir("./coverage"): + shutil.rmtree("./coverage") + tar.extractall() + tar.close() + TIMEOUT = time.time() + return "OK" + return "NOK" + +if __name__ == "__main__": + app.debug = True + app.run(host="0.0.0.0") diff --git a/scripts/klee-clang b/scripts/klee-clang new file mode 100755 index 00000000..2584024d --- /dev/null +++ b/scripts/klee-clang @@ -0,0 +1,44 @@ +#!/usr/bin/env python + +import os, sys +import subprocess + +def isLinkCommand(): + # Look for '-Wl,' as a signal that we are calling the linker. What a hack. + for arg in sys.argv: + if arg.startswith('-Wl,'): + return True + +def main(): + llvm_path = subprocess.Popen(["llvm-config", "--bindir"], stdout=subprocess.PIPE).communicate()[0].strip() + + if not isLinkCommand(): + os.execvp(llvm_path+"/clang", ["clang", "-emit-llvm", "-c"] + sys.argv[1:]) + return 1 + + # Otherwise, strip out arguments that llvm-ld doesn't understand. I don't + # want my previous explicit declaration of hackyness to imply that this bit + # of code here is not also a complete and total hack, it is. + args = sys.argv[1:] + linkArgs = [] + for a in args: + if a in ('-g', '-W', '-O', '-D', '-f', + '-fnested-functions', '-pthread'): + continue + elif a.startswith('-Wl,'): + continue + + if a in linkArgs: + continue + + if a.startswith('-l'): + continue + + linkArgs.append(a) + + os.execvp(llvm_path+"/llvm-link", [llvm_path+"/llvm-link"] + linkArgs) + return 1 + +if __name__ == '__main__': + main() + diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c new file mode 100644 index 00000000..3cb9c5fe --- /dev/null +++ b/test/Feature/RewriteEqualities.c @@ -0,0 +1,38 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities=false %t.bc +// RUN: grep "N0:(Read w8 2 x)" %t.klee-out/test000003.pc +// RUN: grep "N0)" %t.klee-out/test000003.pc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities %t.bc +// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.pc + +#include <stdio.h> +#include <klee/klee.h> + +int run(unsigned char * x, unsigned char * y) { + y[6] = 15; + + if(x[2] >= 10){ + return 1; + } + + if(y[x[2]] < 11){ + if(x[2] == 8){ + return 2; + } else{ + return 3; + } + } else{ + return 4; + } +} + +unsigned char y[255]; + +int main() { + unsigned char x[4]; + klee_make_symbolic(&x, sizeof x, "x"); + + return run(x, y); +} diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c index a771bc75..7af6f9d7 100644 --- a/test/Feature/arithmetic-right-overshift-sym-conc.c +++ b/test/Feature/arithmetic-right-overshift-sym-conc.c @@ -15,11 +15,13 @@ typedef enum // We're using signed ints so should be doing // arithmetic right shift. -int overshift(volatile unsigned int y, const char * type) +// lhs should be a constant +int overshift(signed int lhs, volatile unsigned int y, const char * type) { overshift_t ret; - volatile signed int x=15; + volatile signed int x = lhs; unsigned int limit = sizeof(x)*8; + assert(!klee_is_symbolic(x)); volatile signed int result; result = x >> y; // Potential overshift @@ -45,10 +47,13 @@ int overshift(volatile unsigned int y, const char * type) int main(int argc, char** argv) { - // Concrete overshift volatile unsigned int y = sizeof(unsigned int)*8; - overshift_t conc = overshift(y, "Concrete"); - assert( conc == TO_ZERO); + // Try with +ve lhs + overshift_t conc = overshift(15, y, "Concrete"); + assert(conc == TO_ZERO); + // Try with -ve lhs + conc = overshift(-1, y, "Concrete"); + assert(conc == TO_ZERO); // Symbolic overshift volatile unsigned int y2; @@ -56,11 +61,15 @@ int main(int argc, char** argv) // Add constraints so only one value possible klee_assume(y2 > (y-1)); klee_assume(y2 < (y+1)); - overshift_t sym = overshift(y2, "Symbolic"); - assert( sym == TO_ZERO); + // Try with +ve lhs + overshift_t sym = overshift(15, y2, "Symbolic"); + assert(sym == TO_ZERO); + // Try with -ve lhs + sym = overshift(-1, y2, "Symbolic"); + assert(sym == TO_ZERO); // Concrete and symbolic behaviour should be the same - assert( conc == sym); + assert(conc == sym); return 0; } diff --git a/test/Programs/pcregrep.c b/test/Programs/pcregrep.c index fb99ef87..5ed8f4fa 100644 --- a/test/Programs/pcregrep.c +++ b/test/Programs/pcregrep.c @@ -211,7 +211,7 @@ struct l_struct_2E_pcre { /* Function Declarations */ double fmod(double, double); float fmodf(float, float); -unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv); +int main(int llvm_cbe_argc, char **llvm_cbe_argv); unsigned int fprintf(struct l_struct_2E__IO_FILE *, unsigned char *, ...); unsigned int __strtol_internal(unsigned char *, unsigned char **, unsigned int , unsigned int ); unsigned int printf(unsigned char *, ...); @@ -319,7 +319,7 @@ static inline int llvm_fcmp_ogt(double X, double Y) { return X > Y ; } static inline int llvm_fcmp_ole(double X, double Y) { return X <= Y ; } static inline int llvm_fcmp_oge(double X, double Y) { return X >= Y ; } -unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv) { +int main(int llvm_cbe_argc, char **llvm_cbe_argv) { unsigned int llvm_cbe_length_i_i; /* Address-exposed local */ unsigned int llvm_cbe_firstbyte_i_i; /* Address-exposed local */ unsigned int llvm_cbe_reqbyte_i_i; /* Address-exposed local */ diff --git a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c index 71f6d07a..d82f0eb9 100644 --- a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c +++ b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c @@ -5,10 +5,12 @@ #include <string.h> #include <assert.h> +#include "klee/klee.h" + int main() { int a; - klee_make_symbolic(&a, sizeof a); + klee_make_symbolic(&a, sizeof a, "a"); memset(&a, 0, sizeof a); diff --git a/test/Solver/AShr_to_smtlib.kquery b/test/Solver/AShr_to_smtlib.kquery new file mode 100644 index 00000000..774c46d9 --- /dev/null +++ b/test/Solver/AShr_to_smtlib.kquery @@ -0,0 +1,16 @@ +# RUN: %kleaver -print-smtlib -smtlib-abbreviation-mode=none %s > %t +# RUN: diff -u %t %s.good.smt2 + +# This test tries to check that the SMT-LIBv2 we generate when a AShrExpr is +# used is correct. +# +# FIXME: We should really pass the generated query to an SMT solver that supports +# SMT-LIBv2 and check it gives the correct answer ``unsat``. An older version of +# KLEE where AShrExpr wasn't handled correctly would give ``sat`` for this query. +# +# We could fix this if we required STP to be in the user's PATH and made available +# as a substitution in llvm-lit + +array value[1] : w32 -> w8 = symbolic +array shift[1] : w32 -> w8 = symbolic +(query [(Ule 8 (Read w8 0 shift))] (Eq 0 (AShr w8 (Read w8 0 value) (Read w8 0 shift))) ) diff --git a/test/Solver/AShr_to_smtlib.kquery.good.smt2 b/test/Solver/AShr_to_smtlib.kquery.good.smt2 new file mode 100644 index 00000000..e9478da6 --- /dev/null +++ b/test/Solver/AShr_to_smtlib.kquery.good.smt2 @@ -0,0 +1,7 @@ +;SMTLIBv2 Query 0 +(set-logic QF_AUFBV ) +(declare-fun shift () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun value () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(assert (and (= false (= (_ bv0 8) (ite (bvuge (select shift (_ bv0 32) ) (_ bv8 8) ) (_ bv0 8) (bvashr (select value (_ bv0 32) ) (select shift (_ bv0 32) ) ) ) ) ) (bvule (_ bv8 8) (select shift (_ bv0 32) ) ) ) ) +(check-sat) +(exit) diff --git a/tools/gen-random-bout/Makefile b/tools/gen-random-bout/Makefile index 97315af2..5e1d8cf3 100644 --- a/tools/gen-random-bout/Makefile +++ b/tools/gen-random-bout/Makefile @@ -3,5 +3,6 @@ LEVEL=../.. TOOLNAME = gen-random-bout USEDLIBS = kleeBasic.a +NO_INSTALL=1 include $(LEVEL)/Makefile.common diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index f66d0598..10b19a20 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -19,7 +19,7 @@ LINK_COMPONENTS = support include $(LEVEL)/Makefile.common -LIBS += -lstp +LIBS += $(STP_LDFLAGS) ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index fafe955f..af337abe 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -12,8 +12,8 @@ #include "klee/Common.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" - #include "klee/util/ExprSMTLIBPrinter.h" +#include "klee/Internal/Support/PrintVersion.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" @@ -24,12 +24,6 @@ #include <sys/stat.h> #include <unistd.h> -// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs. -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION #include "llvm/Support/Signals.h" @@ -451,6 +445,7 @@ int main(int argc, char **argv) { bool success = true; llvm::sys::PrintStackTraceOnErrorSignal(); + llvm::cl::SetVersionPrinter(klee::printVersion); llvm::cl::ParseCommandLineOptions(argc, argv); std::string ErrorStr; diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c index 73e2783e..6b4fb8f4 100644 --- a/tools/klee-replay/klee-replay.c +++ b/tools/klee-replay/klee-replay.c @@ -418,6 +418,10 @@ void klee_prefer_cex(void *buffer, uintptr_t condition) { ; } +void klee_posix_prefer_cex(void *buffer, uintptr_t condition) { + ; +} + void klee_make_symbolic(void *addr, size_t nbytes, const char *name) { /* XXX remove model version code once new tests gen'd */ if (obj_index >= input->numObjects) { diff --git a/tools/klee/Makefile b/tools/klee/Makefile index b9506b47..eb80d845 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -20,7 +20,7 @@ LINK_COMPONENTS += irreader endif include $(LEVEL)/Makefile.common -LIBS += -lstp +LIBS += $(STP_LDFLAGS) ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 8a246685..aba247e7 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -13,13 +13,7 @@ #include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" - -// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs. -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION +#include "klee/Internal/Support/PrintVersion.h" #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) #include "llvm/IR/Constants.h" @@ -600,7 +594,7 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { { KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << "Using installed KLEE library runtime: "); - libDir = KLEE_INSTALL_LIB_DIR ; + libDir = KLEE_INSTALL_RUNTIME_DIR ; } else { @@ -619,10 +613,6 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { //===----------------------------------------------------------------------===// // main Driver function // -#if ENABLE_STPLOG == 1 -extern "C" void STPLOG_init(const char *); -#endif - static std::string strip(std::string &in) { unsigned len = in.size(); unsigned lead = 0, trail = len; @@ -634,11 +624,12 @@ static std::string strip(std::string &in) { } static void parseArguments(int argc, char **argv) { + cl::SetVersionPrinter(klee::printVersion); #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) // This version always reads response files - cl::ParseCommandLineOptions(argc, (const char**) argv, " klee\n"); + cl::ParseCommandLineOptions(argc, argv, " klee\n"); #else - cl::ParseCommandLineOptions(argc, (char**) argv, " klee\n", /*ReadResponseFiles=*/ true); + cl::ParseCommandLineOptions(argc, argv, " klee\n", /*ReadResponseFiles=*/ true); #endif } @@ -1092,6 +1083,8 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) replaceOrRenameFunction(mainModule, "__libc_open", "open"); replaceOrRenameFunction(mainModule, "__libc_fcntl", "fcntl"); + // Take care of fortified functions + replaceOrRenameFunction(mainModule, "__fprintf_chk", "fprintf"); // XXX we need to rearchitect so this can also be used with // programs externally linked with uclibc. @@ -1143,11 +1136,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) } #endif -int main(int argc, char **argv, char **envp) { -#if ENABLE_STPLOG == 1 - STPLOG_init("stplog.c"); -#endif - +int main(int argc, char **argv, char **envp) { atexit(llvm_shutdown); // Call llvm_shutdown() on exit. llvm::InitializeNativeTarget(); diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile index a9bfeda1..e52aea31 100644 --- a/unittests/Expr/Makefile +++ b/unittests/Expr/Makefile @@ -10,4 +10,4 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest CXXFLAGS += -DLLVM_29_UNITTEST -LIBS += -lstp +LIBS += $(STP_LDFLAGS) diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile index 94bbb83c..14dcc8bd 100644 --- a/unittests/Ref/Makefile +++ b/unittests/Ref/Makefile @@ -9,4 +9,4 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest -LIBS += -lstp +LIBS += $(STP_LDFLAGS) diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile index 00713691..aeac34ac 100644 --- a/unittests/Solver/Makefile +++ b/unittests/Solver/Makefile @@ -9,4 +9,4 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest -LIBS += -lstp +LIBS += $(STP_LDFLAGS) diff --git a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py index be03cc2f..048540ab 100644 --- a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py +++ b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py @@ -1,205 +1,205 @@ -from __future__ import division - -### - -import math, os, random - -from Graphics.Geometry import vec2 - -from reportlab.pdfgen import canvas -#from reportlab.graphics import shapes -from reportlab.pdfbase import pdfmetrics - -""" -class Canvas: - def startDrawing(self, (w,h)): - def endDrawing(self): - - def getAspect(self): - - def setColor(self, r, g, b): - def setLineWidth(self, width): - def drawOutlineBox(self, x0, y0, x1, y1): - def drawFilledBox(self, x0, y0, x1, y1): - def drawFilledPolygon(self, pts): - def drawOutlineCircle(self, x, y, r): - def startDrawPoints(self): - def endDrawPoints(self): - def drawPoint(self, x, y): - def setPointSize(self, size): - - def drawLine(self, a, b): - def drawLines(self, ptPairs): - def drawLineStrip(self, pts): - - def pushTransform(self): - def popTransform(self): - def translate(self, x, y): - def scale(self, x, y): - def setFontSize(self, size): - def drawString(self, (x, y), text): -""" - -class BaseCanvas: - def drawPoints(self, pts): - self.startDrawPoints() - for pt in pts: - self.drawPoint(pt) - self.endDrawPoints() - - def drawStringCentered(self, boxLL, boxUR, text): - ll,ur = self.getStringBBox(text) - stringSize = vec2.sub(ur,ll) - boxSize = vec2.sub(boxUR,boxLL) - deltaSize = vec2.sub(boxSize, stringSize) - halfDeltaSize = vec2.mulN(deltaSize, .5) - - self.drawString(vec2.add(boxLL,halfDeltaSize), text) - - def getStringSize(self, string): - ll,ur = self.getStringBBox(string) - return vec2.sub(ur,ll) - -class PdfCanvas(BaseCanvas): - def __init__(self, name, basePos=(300,400), baseScale=(250,250), pageSize=None): - self._font = 'Times-Roman' - self.c = canvas.Canvas(name, pagesize=pageSize) - self.pointSize = 1 - self.scaleX = self.scaleY = 1 - self.state = [] - self.basePos = tuple(basePos) - self.baseScale = tuple(baseScale) - self.lastFontSizeSet = None - - self.kLineScaleFactor = 1.95 - - def getAspect(self): - return 1.0,1.0 - - def startDrawing(self): - self.pointSize = 1 - self.scaleX = self.scaleY = 1 - - self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1])) - self.scale(self.baseScale) - - self.setColor(0,0,0) - self.setLineWidth(1) - self.setPointSize(1) - - def finishPage(self): - self.c.showPage() - - self.pointSize = 1 - self.scaleX = self.scaleY = 1 - - self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1])) - self.scale(self.baseScale) - - self.setColor(0,0,0) - self.setLineWidth(1) - self.setPointSize(1) - - if self.lastFontSizeSet is not None: - self.setFontSize(self.lastFontSizeSet) - - def endDrawing(self): - self.c.showPage() - self.c.save() - - def setColor(self, r, g, b): - self.c.setStrokeColorRGB(r,g,b) - self.c.setFillColorRGB(r,g,b) - def setLineWidth(self, width): - avgScale = (self.scaleX+self.scaleY)/2 - self.c.setLineWidth(width/(self.kLineScaleFactor*avgScale)) - def setPointSize(self, size): - avgScale = (self.scaleX+self.scaleY)/2 - self.pointSize = size/(4*avgScale) - - def drawOutlineBox(self, (x0, y0), (x1, y1)): - self.c.rect(x0, y0, x1-x0, y1-y0, stroke=1, fill=0) - def drawFilledBox(self, (x0, y0), (x1, y1)): - self.c.rect(x0, y0, x1-x0, y1-y0, stroke=0, fill=1) - def drawOutlineCircle(self, (x, y), r): - self.c.circle(x, y, r, stroke=1, fill=0) - def drawFilledCircle(self, (x, y), r): - self.c.circle(x, y, r, stroke=0, fill=1) - def drawFilledPolygon(self, pts): - p = self.c.beginPath() - p.moveTo(*pts[-1]) - for x,y in pts: - p.lineTo(x,y) - self.c.drawPath(p, fill=1, stroke=0) - def drawOutlinePolygon(self, pts): - p = self.c.beginPath() - p.moveTo(* pts[0]) - for x,y in pts[1:]: - p.lineTo(x,y) - p.close() - self.c.drawPath(p, fill=0, stroke=1) - def startDrawPoints(self): - pass - def endDrawPoints(self): - pass - def drawPoint(self, (x, y)): - self.c.circle(x, y, self.pointSize, stroke=0, fill=1) - - def drawLine(self, a, b): - self.drawLines([(a,b)]) - def drawLines(self, ptPairs): - p = self.c.beginPath() - for a,b in ptPairs: - p.moveTo(a[0],a[1]) - p.lineTo(b[0],b[1]) - self.c.drawPath(p) - def drawLineStrip(self, pts): - p = self.c.beginPath() - p.moveTo(pts[0][0],pts[0][1]) - for pt in pts[1:]: - p.lineTo(pt[0],pt[1]) - self.c.drawPath(p) - def drawBezier(self, (p0,p1,p2,p3)): - self.c.bezier(*(p0+p1+p2+p3)) - - def pushTransform(self): - self.state.append( (self.scaleX,self.scaleY) ) - self.c.saveState() - def popTransform(self): - self.c.restoreState() - self.scaleX,self.scaleY = self.state.pop() - def translate(self, (x, y)): - self.c.translate(x, y) - def rotate(self, angle): - self.c.rotate(angle*180/math.pi) - def scale(self, (x, y)): - self.scaleX *= x - self.scaleY *= y - self.c.scale(x, y) - - def setFont(self, fontName): - self._font = {"Symbol":"Symbol", - "Times":"Times-Roman"}.get(fontName,fontName) - def setFontSize(self, size): - self.lastFontSizeSet = size - avgScale = (self.scaleX+self.scaleY)/2 - self.fontSize = size/(2*avgScale) - self.c.setFont(self._font, self.fontSize) -# self.c.setFont("Times-Roman", size/(2*avgScale)) - def drawString(self, (x, y), text): - self.c.drawString(x, y, text) - - def drawOutlineString(self, (x,y), text): - t = self.c.beginText(x, y) - t.setTextRenderMode(1) - t.textLine(text) - t.setTextRenderMode(0) - self.c.drawText(t) - - def getStringBBox(self, text): - font = pdfmetrics.getFont(self._font) - width = pdfmetrics.stringWidth(text, self._font, self.fontSize) - ll = (0,0) - ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize) - ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize) - return ll,ur +from __future__ import division + +### + +import math, os, random + +from Graphics.Geometry import vec2 + +from reportlab.pdfgen import canvas +#from reportlab.graphics import shapes +from reportlab.pdfbase import pdfmetrics + +""" +class Canvas: + def startDrawing(self, (w,h)): + def endDrawing(self): + + def getAspect(self): + + def setColor(self, r, g, b): + def setLineWidth(self, width): + def drawOutlineBox(self, x0, y0, x1, y1): + def drawFilledBox(self, x0, y0, x1, y1): + def drawFilledPolygon(self, pts): + def drawOutlineCircle(self, x, y, r): + def startDrawPoints(self): + def endDrawPoints(self): + def drawPoint(self, x, y): + def setPointSize(self, size): + + def drawLine(self, a, b): + def drawLines(self, ptPairs): + def drawLineStrip(self, pts): + + def pushTransform(self): + def popTransform(self): + def translate(self, x, y): + def scale(self, x, y): + def setFontSize(self, size): + def drawString(self, (x, y), text): +""" + +class BaseCanvas: + def drawPoints(self, pts): + self.startDrawPoints() + for pt in pts: + self.drawPoint(pt) + self.endDrawPoints() + + def drawStringCentered(self, boxLL, boxUR, text): + ll,ur = self.getStringBBox(text) + stringSize = vec2.sub(ur,ll) + boxSize = vec2.sub(boxUR,boxLL) + deltaSize = vec2.sub(boxSize, stringSize) + halfDeltaSize = vec2.mulN(deltaSize, .5) + + self.drawString(vec2.add(boxLL,halfDeltaSize), text) + + def getStringSize(self, string): + ll,ur = self.getStringBBox(string) + return vec2.sub(ur,ll) + +class PdfCanvas(BaseCanvas): + def __init__(self, name, basePos=(300,400), baseScale=(250,250), pageSize=None): + self._font = 'Times-Roman' + self.c = canvas.Canvas(name, pagesize=pageSize) + self.pointSize = 1 + self.scaleX = self.scaleY = 1 + self.state = [] + self.basePos = tuple(basePos) + self.baseScale = tuple(baseScale) + self.lastFontSizeSet = None + + self.kLineScaleFactor = 1.95 + + def getAspect(self): + return 1.0,1.0 + + def startDrawing(self): + self.pointSize = 1 + self.scaleX = self.scaleY = 1 + + self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1])) + self.scale(self.baseScale) + + self.setColor(0,0,0) + self.setLineWidth(1) + self.setPointSize(1) + + def finishPage(self): + self.c.showPage() + + self.pointSize = 1 + self.scaleX = self.scaleY = 1 + + self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1])) + self.scale(self.baseScale) + + self.setColor(0,0,0) + self.setLineWidth(1) + self.setPointSize(1) + + if self.lastFontSizeSet is not None: + self.setFontSize(self.lastFontSizeSet) + + def endDrawing(self): + self.c.showPage() + self.c.save() + + def setColor(self, r, g, b): + self.c.setStrokeColorRGB(r,g,b) + self.c.setFillColorRGB(r,g,b) + def setLineWidth(self, width): + avgScale = (self.scaleX+self.scaleY)/2 + self.c.setLineWidth(width/(self.kLineScaleFactor*avgScale)) + def setPointSize(self, size): + avgScale = (self.scaleX+self.scaleY)/2 + self.pointSize = size/(4*avgScale) + + def drawOutlineBox(self, (x0, y0), (x1, y1)): + self.c.rect(x0, y0, x1-x0, y1-y0, stroke=1, fill=0) + def drawFilledBox(self, (x0, y0), (x1, y1)): + self.c.rect(x0, y0, x1-x0, y1-y0, stroke=0, fill=1) + def drawOutlineCircle(self, (x, y), r): + self.c.circle(x, y, r, stroke=1, fill=0) + def drawFilledCircle(self, (x, y), r): + self.c.circle(x, y, r, stroke=0, fill=1) + def drawFilledPolygon(self, pts): + p = self.c.beginPath() + p.moveTo(*pts[-1]) + for x,y in pts: + p.lineTo(x,y) + self.c.drawPath(p, fill=1, stroke=0) + def drawOutlinePolygon(self, pts): + p = self.c.beginPath() + p.moveTo(* pts[0]) + for x,y in pts[1:]: + p.lineTo(x,y) + p.close() + self.c.drawPath(p, fill=0, stroke=1) + def startDrawPoints(self): + pass + def endDrawPoints(self): + pass + def drawPoint(self, (x, y)): + self.c.circle(x, y, self.pointSize, stroke=0, fill=1) + + def drawLine(self, a, b): + self.drawLines([(a,b)]) + def drawLines(self, ptPairs): + p = self.c.beginPath() + for a,b in ptPairs: + p.moveTo(a[0],a[1]) + p.lineTo(b[0],b[1]) + self.c.drawPath(p) + def drawLineStrip(self, pts): + p = self.c.beginPath() + p.moveTo(pts[0][0],pts[0][1]) + for pt in pts[1:]: + p.lineTo(pt[0],pt[1]) + self.c.drawPath(p) + def drawBezier(self, (p0,p1,p2,p3)): + self.c.bezier(*(p0+p1+p2+p3)) + + def pushTransform(self): + self.state.append( (self.scaleX,self.scaleY) ) + self.c.saveState() + def popTransform(self): + self.c.restoreState() + self.scaleX,self.scaleY = self.state.pop() + def translate(self, (x, y)): + self.c.translate(x, y) + def rotate(self, angle): + self.c.rotate(angle*180/math.pi) + def scale(self, (x, y)): + self.scaleX *= x + self.scaleY *= y + self.c.scale(x, y) + + def setFont(self, fontName): + self._font = {"Symbol":"Symbol", + "Times":"Times-Roman"}.get(fontName,fontName) + def setFontSize(self, size): + self.lastFontSizeSet = size + avgScale = (self.scaleX+self.scaleY)/2 + self.fontSize = size/(2*avgScale) + self.c.setFont(self._font, self.fontSize) +# self.c.setFont("Times-Roman", size/(2*avgScale)) + def drawString(self, (x, y), text): + self.c.drawString(x, y, text) + + def drawOutlineString(self, (x,y), text): + t = self.c.beginText(x, y) + t.setTextRenderMode(1) + t.textLine(text) + t.setTextRenderMode(0) + self.c.drawText(t) + + def getStringBBox(self, text): + font = pdfmetrics.getFont(self._font) + width = pdfmetrics.stringWidth(text, self._font, self.fontSize) + ll = (0,0) + ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize) + ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize) + return ll,ur diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py index a600a64f..d310c20a 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py @@ -1,59 +1,59 @@ -import vec2, math - -def intersectLineCircle((p, no), (C, r)): - x = vec2.sub(p,C) - b = 2.*vec2.dot(no, x) - c = vec2.sqr(x) - r*r - dist = b*b - 4*c - - if dist<0: - return None - else: - d = math.sqrt(dist) - t0 = (-b - d)*.5 - t1 = (-b + d)*.5 - return (t0,t1) - -#def intersectLineCircle((lineP,lineN),(circleP,circleR)): -# dx,dy = vec2.sub(lineP,circleP) -# nx,ny = lineN -# -# a = (nx*nx + ny*ny) -# b = 2*(dx*nx + dy*ny) -# c = (dx*dx + dy*dy) - circleR*circleR -# -# k = b*b - 4*a*c -# if k<0: -# return None -# else: -# d = math.sqrt(k) -# t1 = (-b - d)/2*a -# t0 = (-b + d)/2*a -# return t0,t1 - -def intersectCircleCircle(c0P, c0R, c1P, c1R): - v = vec2.sub(c1P, c0P) - d = vec2.length(v) - - R = c0R - r = c1R - - try: - x = (d*d - r*r + R*R)/(2*d) - except ZeroDivisionError: - if R<r: - return 'inside',() - elif r>R: - return 'outside',() - else: - return 'coincident',() - - k = R*R - x*x - if k<0: - if x<0: - return 'inside',() - else: - return 'outside',() - else: - y = math.sqrt(k) - return 'intersect',(vec2.toangle(v),vec2.toangle((x,y))) +import vec2, math + +def intersectLineCircle((p, no), (C, r)): + x = vec2.sub(p,C) + b = 2.*vec2.dot(no, x) + c = vec2.sqr(x) - r*r + dist = b*b - 4*c + + if dist<0: + return None + else: + d = math.sqrt(dist) + t0 = (-b - d)*.5 + t1 = (-b + d)*.5 + return (t0,t1) + +#def intersectLineCircle((lineP,lineN),(circleP,circleR)): +# dx,dy = vec2.sub(lineP,circleP) +# nx,ny = lineN +# +# a = (nx*nx + ny*ny) +# b = 2*(dx*nx + dy*ny) +# c = (dx*dx + dy*dy) - circleR*circleR +# +# k = b*b - 4*a*c +# if k<0: +# return None +# else: +# d = math.sqrt(k) +# t1 = (-b - d)/2*a +# t0 = (-b + d)/2*a +# return t0,t1 + +def intersectCircleCircle(c0P, c0R, c1P, c1R): + v = vec2.sub(c1P, c0P) + d = vec2.length(v) + + R = c0R + r = c1R + + try: + x = (d*d - r*r + R*R)/(2*d) + except ZeroDivisionError: + if R<r: + return 'inside',() + elif r>R: + return 'outside',() + else: + return 'coincident',() + + k = R*R - x*x + if k<0: + if x<0: + return 'inside',() + else: + return 'outside',() + else: + y = math.sqrt(k) + return 'intersect',(vec2.toangle(v),vec2.toangle((x,y))) diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py index 05320d5e..5a09be62 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py @@ -1,20 +1,20 @@ -import vec2 - -def det(m): - ((m00,m01),(m10,m11))= m - - return m00*m11 - m01*m10 - -def mul(a,b): - b_trans= zip(* b) - return tuple([transmulvec2(b_trans, a_r) for a_r in a]) - - # multiple vector v by a transposed matrix -def transmulvec2(m_trans,v): - return tuple([vec2.dot(v, m_c) for m_c in m_trans]) - -def mulvec2(m,v): - return transmulvec2(zip(* m), v) - -def mulN(m,N): - return tuple([vec2.mulN(v,N) for v in m]) +import vec2 + +def det(m): + ((m00,m01),(m10,m11))= m + + return m00*m11 - m01*m10 + +def mul(a,b): + b_trans= zip(* b) + return tuple([transmulvec2(b_trans, a_r) for a_r in a]) + + # multiple vector v by a transposed matrix +def transmulvec2(m_trans,v): + return tuple([vec2.dot(v, m_c) for m_c in m_trans]) + +def mulvec2(m,v): + return transmulvec2(zip(* m), v) + +def mulN(m,N): + return tuple([vec2.mulN(v,N) for v in m]) diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py index b8705a32..c25d7e50 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py @@ -1,40 +1,40 @@ -import vec3,mat2 - -def identity(): - return ((1.0, 0.0, 0.0), - (0.0, 1.0, 0.0), - (0.0, 0.0, 1.0)) - -def fromscale(scale): - x,y,z= scale - x,y,z= float(x),float(y),float(z) - return (( x, 0.0, 0.0), - (0.0, y, 0.0), - (0.0, 0.0, z)) -def fromscaleN(n): - return fromscale((n,n,n)) - -def mul(a,b): - b_trans= zip(* b) - return tuple([transmulvec3(b_trans, a_r) for a_r in a]) - - # multiple vector v by a transposed matrix -def transmulvec3(m_trans,v): - return tuple([vec3.dot(v, m_c) for m_c in m_trans]) - -def mulvec3(m,v): - return transmulvec3(zip(* m), v) - -def mulN(m,N): - return tuple([vec3.mulN(v,N) for v in m]) - -def det(m): - ((m00,m01,m02), - (m10,m11,m12), - (m20,m21,m22))= m - - a= m00 * mat2.det( ((m11, m12), (m21, m22)) ); - b= m10 * mat2.det( ((m01, m02), (m21, m22)) ); - c= m20 * mat2.det( ((m01, m02), (m11, m12)) ); - - return a-b+c +import vec3,mat2 + +def identity(): + return ((1.0, 0.0, 0.0), + (0.0, 1.0, 0.0), + (0.0, 0.0, 1.0)) + +def fromscale(scale): + x,y,z= scale + x,y,z= float(x),float(y),float(z) + return (( x, 0.0, 0.0), + (0.0, y, 0.0), + (0.0, 0.0, z)) +def fromscaleN(n): + return fromscale((n,n,n)) + +def mul(a,b): + b_trans= zip(* b) + return tuple([transmulvec3(b_trans, a_r) for a_r in a]) + + # multiple vector v by a transposed matrix +def transmulvec3(m_trans,v): + return tuple([vec3.dot(v, m_c) for m_c in m_trans]) + +def mulvec3(m,v): + return transmulvec3(zip(* m), v) + +def mulN(m,N): + return tuple([vec3.mulN(v,N) for v in m]) + +def det(m): + ((m00,m01,m02), + (m10,m11,m12), + (m20,m21,m22))= m + + a= m00 * mat2.det( ((m11, m12), (m21, m22)) ); + b= m10 * mat2.det( ((m01, m02), (m21, m22)) ); + c= m20 * mat2.det( ((m01, m02), (m11, m12)) ); + + return a-b+c diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py index 8dc7d35c..e927c936 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py @@ -1,153 +1,153 @@ -import vec4,mat3 - -def identity(): - return ((1.0, 0.0, 0.0, 0.0), - (0.0, 1.0, 0.0, 0.0), - (0.0, 0.0, 1.0, 0.0), - (0.0, 0.0, 0.0, 1.0)) - -def fromtrans(trans): - return ((1.0, 0.0, 0.0, 0.0), - (0.0, 1.0, 0.0, 0.0), - (0.0, 0.0, 1.0, 0.0), - (trans[0], trans[1], trans[2], 1.0)) - -def fromscale(scale): - x,y,z= scale - x,y,z= float(x),float(y),float(z) - return (( x, 0.0, 0.0, 0.0), - (0.0, y, 0.0, 0.0), - (0.0, 0.0, z, 0.0), - (0.0, 0.0, 0.0, 1.0)) -def fromscaleN(n): - return fromscale((n,n,n)) - -def fromortho(left,right,bottom,top,znear,zfar): - m0= ( 2.0/(right-left), 0.0, 0.0, 0.0) - m1= (0.0, 2.0/(top-bottom), 0.0, 0.0) - m2= (0.0, 0.0, -2.0/(zfar-znear), 0.0) - m3= ( -((right+left)/(right-left)), - -((top+bottom)/(top-bottom)), - -((zfar+znear)/(zfar-znear)), - 1.0) - return (m0,m1,m2,m3) - -def mulN(m,N): - return tuple([vec4.mulN(v,N) for v in m]) - -def mul(a,b): - b_trans= zip(* b) - return tuple([transmulvec4(b_trans, a_r) for a_r in a]) - - # multiple vector v by a transposed matrix -def transmulvec4(m_trans,v): - return tuple([vec4.dot(v, m_c) for m_c in m_trans]) - -def mulvec4(m,v): - return transmulvec4(zip(* m), v) - -def trans(m): - ((m00,m01,m02,m03), - (m10,m11,m12,m13), - (m20,m21,m22,m23), - (m30,m31,m32,m33))= m - - return ( (m00,m10,m20,m30), - (m01,m11,m21,m31), - (m02,m12,m22,m32), - (m03,m13,m23,m33)) - -def det(m): - ((m00,m01,m02,m03), - (m10,m11,m12,m13), - (m20,m21,m22,m23), - (m30,m31,m32,m33))= m - - a= m00 * mat3.det( ((m11, m12, m13), - (m21, m22, m23), - (m31, m32, m33)) ); - b= m10 * mat3.det( ((m01, m02, m03), - (m21, m22, m23), - (m31, m32, m33)) ); - c= m20 * mat3.det( ((m01, m02, m03), - (m11, m12, m13), - (m31, m32, m33)) ); - d= m30 * mat3.det( ((m01, m02, m03), - (m11, m12, m13), - (m21, m22, m23)) ); - - return a-b+c-d; - -def adj(m): - ((m00,m01,m02,m03), - (m10,m11,m12,m13), - (m20,m21,m22,m23), - (m30,m31,m32,m33))= m - - t00= mat3.det( ((m11, m12, m13), - (m21, m22, m23), - (m31, m32, m33)) ) - t01= -mat3.det( ((m10, m12, m13), - (m20, m22, m23), - (m30, m32, m33)) ) - t02= mat3.det( ((m10, m11, m13), - (m20, m21, m23), - (m30, m31, m33)) ) - t03= -mat3.det( ((m10, m11, m12), - (m20, m21, m22), - (m30, m31, m32)) ) - - - t10= -mat3.det( ((m01, m02, m03), - (m21, m22, m23), - (m31, m32, m33)) ) - t11= mat3.det( ((m00, m02, m03), - (m20, m22, m23), - (m30, m32, m33)) ) - t12= -mat3.det( ((m00, m01, m03), - (m20, m21, m23), - (m30, m31, m33)) ) - t13= mat3.det( ((m00, m01, m02), - (m20, m21, m22), - (m30, m31, m32)) ) - - t20= mat3.det( ((m01, m02, m03), - (m11, m12, m13), - (m31, m32, m33)) ) - t21= -mat3.det( ((m00, m02, m03), - (m10, m12, m13), - (m30, m32, m33)) ) - t22= mat3.det( ((m00, m01, m03), - (m10, m11, m13), - (m30, m31, m33)) ) - t23= -mat3.det( ((m00, m01, m02), - (m10, m11, m12), - (m30, m31, m32)) ) - - t30= -mat3.det( ((m01, m02, m03), - (m11, m12, m13), - (m21, m22, m23)) ) - t31= mat3.det( ((m00, m02, m03), - (m10, m12, m13), - (m20, m22, m23)) ) - t32= -mat3.det( ((m00, m01, m03), - (m10, m11, m13), - (m20, m21, m23)) ) - t33= mat3.det( ((m00, m01, m02), - (m10, m11, m12), - (m20, m21, m22)) ) - - return ((t00,t01,t02,t03), - (t10,t11,t12,t13), - (t20,t21,t22,t23), - (t30,t31,t32,t33)) - -def inv(m): - d= det(m) - t= trans(adj(m)) - v= 1.0/d - return tuple([(a*v,b*v,c*v,d*v) for a,b,c,d in t]) - -def toGL(m): - m0,m1,m2,m3= m +import vec4,mat3 + +def identity(): + return ((1.0, 0.0, 0.0, 0.0), + (0.0, 1.0, 0.0, 0.0), + (0.0, 0.0, 1.0, 0.0), + (0.0, 0.0, 0.0, 1.0)) + +def fromtrans(trans): + return ((1.0, 0.0, 0.0, 0.0), + (0.0, 1.0, 0.0, 0.0), + (0.0, 0.0, 1.0, 0.0), + (trans[0], trans[1], trans[2], 1.0)) + +def fromscale(scale): + x,y,z= scale + x,y,z= float(x),float(y),float(z) + return (( x, 0.0, 0.0, 0.0), + (0.0, y, 0.0, 0.0), + (0.0, 0.0, z, 0.0), + (0.0, 0.0, 0.0, 1.0)) +def fromscaleN(n): + return fromscale((n,n,n)) + +def fromortho(left,right,bottom,top,znear,zfar): + m0= ( 2.0/(right-left), 0.0, 0.0, 0.0) + m1= (0.0, 2.0/(top-bottom), 0.0, 0.0) + m2= (0.0, 0.0, -2.0/(zfar-znear), 0.0) + m3= ( -((right+left)/(right-left)), + -((top+bottom)/(top-bottom)), + -((zfar+znear)/(zfar-znear)), + 1.0) + return (m0,m1,m2,m3) + +def mulN(m,N): + return tuple([vec4.mulN(v,N) for v in m]) + +def mul(a,b): + b_trans= zip(* b) + return tuple([transmulvec4(b_trans, a_r) for a_r in a]) + + # multiple vector v by a transposed matrix +def transmulvec4(m_trans,v): + return tuple([vec4.dot(v, m_c) for m_c in m_trans]) + +def mulvec4(m,v): + return transmulvec4(zip(* m), v) + +def trans(m): + ((m00,m01,m02,m03), + (m10,m11,m12,m13), + (m20,m21,m22,m23), + (m30,m31,m32,m33))= m + + return ( (m00,m10,m20,m30), + (m01,m11,m21,m31), + (m02,m12,m22,m32), + (m03,m13,m23,m33)) + +def det(m): + ((m00,m01,m02,m03), + (m10,m11,m12,m13), + (m20,m21,m22,m23), + (m30,m31,m32,m33))= m + + a= m00 * mat3.det( ((m11, m12, m13), + (m21, m22, m23), + (m31, m32, m33)) ); + b= m10 * mat3.det( ((m01, m02, m03), + (m21, m22, m23), + (m31, m32, m33)) ); + c= m20 * mat3.det( ((m01, m02, m03), + (m11, m12, m13), + (m31, m32, m33)) ); + d= m30 * mat3.det( ((m01, m02, m03), + (m11, m12, m13), + (m21, m22, m23)) ); + + return a-b+c-d; + +def adj(m): + ((m00,m01,m02,m03), + (m10,m11,m12,m13), + (m20,m21,m22,m23), + (m30,m31,m32,m33))= m + + t00= mat3.det( ((m11, m12, m13), + (m21, m22, m23), + (m31, m32, m33)) ) + t01= -mat3.det( ((m10, m12, m13), + (m20, m22, m23), + (m30, m32, m33)) ) + t02= mat3.det( ((m10, m11, m13), + (m20, m21, m23), + (m30, m31, m33)) ) + t03= -mat3.det( ((m10, m11, m12), + (m20, m21, m22), + (m30, m31, m32)) ) + + + t10= -mat3.det( ((m01, m02, m03), + (m21, m22, m23), + (m31, m32, m33)) ) + t11= mat3.det( ((m00, m02, m03), + (m20, m22, m23), + (m30, m32, m33)) ) + t12= -mat3.det( ((m00, m01, m03), + (m20, m21, m23), + (m30, m31, m33)) ) + t13= mat3.det( ((m00, m01, m02), + (m20, m21, m22), + (m30, m31, m32)) ) + + t20= mat3.det( ((m01, m02, m03), + (m11, m12, m13), + (m31, m32, m33)) ) + t21= -mat3.det( ((m00, m02, m03), + (m10, m12, m13), + (m30, m32, m33)) ) + t22= mat3.det( ((m00, m01, m03), + (m10, m11, m13), + (m30, m31, m33)) ) + t23= -mat3.det( ((m00, m01, m02), + (m10, m11, m12), + (m30, m31, m32)) ) + + t30= -mat3.det( ((m01, m02, m03), + (m11, m12, m13), + (m21, m22, m23)) ) + t31= mat3.det( ((m00, m02, m03), + (m10, m12, m13), + (m20, m22, m23)) ) + t32= -mat3.det( ((m00, m01, m03), + (m10, m11, m13), + (m20, m21, m23)) ) + t33= mat3.det( ((m00, m01, m02), + (m10, m11, m12), + (m20, m21, m22)) ) + + return ((t00,t01,t02,t03), + (t10,t11,t12,t13), + (t20,t21,t22,t23), + (t30,t31,t32,t33)) + +def inv(m): + d= det(m) + t= trans(adj(m)) + v= 1.0/d + return tuple([(a*v,b*v,c*v,d*v) for a,b,c,d in t]) + +def toGL(m): + m0,m1,m2,m3= m return m0+m1+m2+m3 \ No newline at end of file diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py index f7837891..663d3d8c 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py @@ -1,107 +1,107 @@ -from __future__ import division - -import math -import vec3, vec4 - -def identity(): - return (0.0,0.0,0.0,1.0) - -def fromaxisangle(axisangle): - axis,angle= axisangle - ang_2= angle/2.0 - s_ang= math.sin(ang_2) - c_ang= math.cos(ang_2) - - q= vec3.mulN(axis, s_ang) + (c_ang,) - return normalize(q) - -def fromnormals(n1,n2): - axis,angle= vec3.normalize(vec3.cross(n1, n2)), math.acos(vec3.dot(n1, n2)) - return fromaxisangle((axis,angle)) - - # avoid trigonmetry -def fromnormals_faster(n1,n2): - axis= vec3.normalize(vec3.cross(n1, n2)) - - half_n= vec3.normalize(vec3.add(n1, n2)) - cos_half_angle= vec3.dot(n1, half_n) - sin_half_angle= 1.0 - cos_half_angle**2 - - return vec3.mulN(axis, sin_half_angle) + (cos_half_angle,) - -def fromvectors(v1,v2): - return fromnormals(vec3.normalize(v1), vec3.normalize(v2)) - -def magnitude(q): - return vec4.length(q) - -def normalize(q): - return vec4.divN(q, magnitude(q)) - -def conjugate(q): - x,y,z,w= q - return (-x, -y, -z, w) - -def mulvec3(q, v): - t= mul(q, v+(0.0,)) - t= mul(t, conjugate(q)) - return t[:3] - -def mul(a, b): - ax,ay,az,aw= a - bx,by,bz,bw= b - - x= aw*bx + ax*bw + ay*bz - az*by - y= aw*by + ay*bw + az*bx - ax*bz - z= aw*bz + az*bw + ax*by - ay*bx - w= aw*bw - ax*bx - ay*by - az*bz - - return (x,y,z,w) - -def toaxisangle(q): - tw= math.acos(q[3]) - scale= math.sin(tw) - angle= tw*2.0 - - try: - axis= vec3.divN(q[:3], scale) - except ZeroDivisionError: - axis= (1.0,0.0,0.0) - - return axis,angle - -def tomat3x3(q): - x,y,z,w= q - - m0= ( 1.0 - 2.0 * ( y*y + z*z ), - 2.0 * ( x*y - z*w ), - 2.0 * ( x*z + y*w )) - m1= ( 2.0 * ( x*y + z*w ), - 1.0 - 2.0 * ( x*x + z*z ), - 2.0 * ( y*z - x*w )) - m2= ( 2.0 * ( x*z - y*w ), - 2.0 * ( y*z + x*w ), - 1.0 - 2.0 * ( x*x + y*y )) - - return m0,m1,m2 - -def tomat4x4(q): - m0,m1,m2= tomat3x3(q) - return (m0 + (0.0,), - m1 + (0.0,), - m2 + (0.0,), - (0.0, 0.0, 0.0, 1.0)) - -def slerp(a, b, t): - raise NotImplementedError - - cos_omega= vec4.dot(a, b) - - if (cos_omega<0.0): - cos_omega= -cos_omega - b= vec4.neg(b) - - imega= math.acos(cos_omega) - t= sin(t*omega)/sin(omega) - - return vec4.lerp(a, b, t) +from __future__ import division + +import math +import vec3, vec4 + +def identity(): + return (0.0,0.0,0.0,1.0) + +def fromaxisangle(axisangle): + axis,angle= axisangle + ang_2= angle/2.0 + s_ang= math.sin(ang_2) + c_ang= math.cos(ang_2) + + q= vec3.mulN(axis, s_ang) + (c_ang,) + return normalize(q) + +def fromnormals(n1,n2): + axis,angle= vec3.normalize(vec3.cross(n1, n2)), math.acos(vec3.dot(n1, n2)) + return fromaxisangle((axis,angle)) + + # avoid trigonmetry +def fromnormals_faster(n1,n2): + axis= vec3.normalize(vec3.cross(n1, n2)) + + half_n= vec3.normalize(vec3.add(n1, n2)) + cos_half_angle= vec3.dot(n1, half_n) + sin_half_angle= 1.0 - cos_half_angle**2 + + return vec3.mulN(axis, sin_half_angle) + (cos_half_angle,) + +def fromvectors(v1,v2): + return fromnormals(vec3.normalize(v1), vec3.normalize(v2)) + +def magnitude(q): + return vec4.length(q) + +def normalize(q): + return vec4.divN(q, magnitude(q)) + +def conjugate(q): + x,y,z,w= q + return (-x, -y, -z, w) + +def mulvec3(q, v): + t= mul(q, v+(0.0,)) + t= mul(t, conjugate(q)) + return t[:3] + +def mul(a, b): + ax,ay,az,aw= a + bx,by,bz,bw= b + + x= aw*bx + ax*bw + ay*bz - az*by + y= aw*by + ay*bw + az*bx - ax*bz + z= aw*bz + az*bw + ax*by - ay*bx + w= aw*bw - ax*bx - ay*by - az*bz + + return (x,y,z,w) + +def toaxisangle(q): + tw= math.acos(q[3]) + scale= math.sin(tw) + angle= tw*2.0 + + try: + axis= vec3.divN(q[:3], scale) + except ZeroDivisionError: + axis= (1.0,0.0,0.0) + + return axis,angle + +def tomat3x3(q): + x,y,z,w= q + + m0= ( 1.0 - 2.0 * ( y*y + z*z ), + 2.0 * ( x*y - z*w ), + 2.0 * ( x*z + y*w )) + m1= ( 2.0 * ( x*y + z*w ), + 1.0 - 2.0 * ( x*x + z*z ), + 2.0 * ( y*z - x*w )) + m2= ( 2.0 * ( x*z - y*w ), + 2.0 * ( y*z + x*w ), + 1.0 - 2.0 * ( x*x + y*y )) + + return m0,m1,m2 + +def tomat4x4(q): + m0,m1,m2= tomat3x3(q) + return (m0 + (0.0,), + m1 + (0.0,), + m2 + (0.0,), + (0.0, 0.0, 0.0, 1.0)) + +def slerp(a, b, t): + raise NotImplementedError + + cos_omega= vec4.dot(a, b) + + if (cos_omega<0.0): + cos_omega= -cos_omega + b= vec4.neg(b) + + imega= math.acos(cos_omega) + t= sin(t*omega)/sin(omega) + + return vec4.lerp(a, b, t) diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py index 80159043..73bc5717 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py @@ -1,79 +1,79 @@ -from __future__ import division -from math import ceil,floor,sqrt,atan2,pi,cos,sin -import random -_abs,_min,_max= abs,min,max - -def random(rng=random): - return (rng.random()*2-1,rng.random()*2-1) - -def getangle(a): - x,y= a - if y>=0: - return atan2(y,x) - else: - return pi*2 + atan2(y,x) -toangle = getangle - -def topolar(pt): - return getangle(pt),length(pt) -def fromangle(angle,radius=1.): - return (cos(angle)*radius, sin(angle)*radius) -frompolar = fromangle - -def rotate((x,y),angle): - c_a,s_a = cos(angle),sin(angle) - return (c_a*x - s_a*y, s_a*x + c_a*y) - -def rotate90((x,y)): - return (-y,x) - -def abs(a): return (_abs(a[0]),_abs(a[1])) -def inv(a): return (-a[0], -a[1]) - -def add(a,b): return (a[0]+b[0], a[1]+b[1]) -def sub(a,b): return (a[0]-b[0], a[1]-b[1]) -def mul(a,b): return (a[0]*b[0], a[1]*b[1]) -def div(a,b): return (a[0]/b[0], a[1]/b[1]) -def mod(a,b): return (a[0]%b[0], a[1]%b[1]) -def dot(a,b): return (a[0]*b[0]+ a[1]*b[1]) - -def addN(a,n): return (a[0]+n, a[1]+n) -def subN(a,n): return (a[0]-n, a[1]-n) -def mulN(a,n): return (a[0]*n, a[1]*n) -def modN(a,n): return (a[0]%n, a[1]%n) -def divN(a,n): return (a[0]/n, a[1]/n) - -def sqr(a): return dot(a,a) -def length(a): return sqrt(sqr(a)) -def avg(a,b): return mulN(add(a,b),0.5) -def distance(a,b): return length(sub(a,b)) - -def normalize(a): - return mulN(a, 1.0/length(a)) - -def normalizeOrZero(a): - try: - return mulN(a, 1.0/length(a)) - except ZeroDivisionError: - return (0.0,0.0) - -def min((a0,a1),(b0,b1)): - return (_min(a0,b0),_min(a1,b1)) -def max((a0,a1),(b0,b1)): - return (_max(a0,b0),_max(a1,b1)) - -def lerp(a,b,t): - return add(mulN(a,1.0-t), mulN(b, t)) - -def toint(a): - return (int(a[0]), int(a[1])) -def tofloor(a): - return (floor(a[0]), floor(a[1])) -def toceil(a): - return (ceil(a[0]), ceil(a[1])) - -def sumlist(l): - return reduce(add, l) -def avglist(l): - return mulN(sumlist(l), 1.0/len(l)) - +from __future__ import division +from math import ceil,floor,sqrt,atan2,pi,cos,sin +import random +_abs,_min,_max= abs,min,max + +def random(rng=random): + return (rng.random()*2-1,rng.random()*2-1) + +def getangle(a): + x,y= a + if y>=0: + return atan2(y,x) + else: + return pi*2 + atan2(y,x) +toangle = getangle + +def topolar(pt): + return getangle(pt),length(pt) +def fromangle(angle,radius=1.): + return (cos(angle)*radius, sin(angle)*radius) +frompolar = fromangle + +def rotate((x,y),angle): + c_a,s_a = cos(angle),sin(angle) + return (c_a*x - s_a*y, s_a*x + c_a*y) + +def rotate90((x,y)): + return (-y,x) + +def abs(a): return (_abs(a[0]),_abs(a[1])) +def inv(a): return (-a[0], -a[1]) + +def add(a,b): return (a[0]+b[0], a[1]+b[1]) +def sub(a,b): return (a[0]-b[0], a[1]-b[1]) +def mul(a,b): return (a[0]*b[0], a[1]*b[1]) +def div(a,b): return (a[0]/b[0], a[1]/b[1]) +def mod(a,b): return (a[0]%b[0], a[1]%b[1]) +def dot(a,b): return (a[0]*b[0]+ a[1]*b[1]) + +def addN(a,n): return (a[0]+n, a[1]+n) +def subN(a,n): return (a[0]-n, a[1]-n) +def mulN(a,n): return (a[0]*n, a[1]*n) +def modN(a,n): return (a[0]%n, a[1]%n) +def divN(a,n): return (a[0]/n, a[1]/n) + +def sqr(a): return dot(a,a) +def length(a): return sqrt(sqr(a)) +def avg(a,b): return mulN(add(a,b),0.5) +def distance(a,b): return length(sub(a,b)) + +def normalize(a): + return mulN(a, 1.0/length(a)) + +def normalizeOrZero(a): + try: + return mulN(a, 1.0/length(a)) + except ZeroDivisionError: + return (0.0,0.0) + +def min((a0,a1),(b0,b1)): + return (_min(a0,b0),_min(a1,b1)) +def max((a0,a1),(b0,b1)): + return (_max(a0,b0),_max(a1,b1)) + +def lerp(a,b,t): + return add(mulN(a,1.0-t), mulN(b, t)) + +def toint(a): + return (int(a[0]), int(a[1])) +def tofloor(a): + return (floor(a[0]), floor(a[1])) +def toceil(a): + return (ceil(a[0]), ceil(a[1])) + +def sumlist(l): + return reduce(add, l) +def avglist(l): + return mulN(sumlist(l), 1.0/len(l)) + diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py index ed4d8114..48ebf129 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py @@ -1,55 +1,55 @@ -from __future__ import division -from math import ceil,floor,sqrt -from random import random as _random -_min,_max= min,max - -def random(): - return (_random()*2-1,_random()*2-1,_random()*2-1) - -def inv(a): return (-a[0],-a[1],-a[2]) - -def add(a,b): return (a[0]+b[0], a[1]+b[1], a[2]+b[2]) -def sub(a,b): return (a[0]-b[0], a[1]-b[1], a[2]-b[2]) -def mul(a,b): return (a[0]*b[0], a[1]*b[1], a[2]*b[2]) -def div(a,b): return (a[0]/b[0], a[1]/b[1], a[2]/b[2]) -def mod(a,b): return (a[0]%b[0], a[1]%b[1], a[2]%b[2]) -def dot(a,b): return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]) - -def addN(a,n): return (a[0]+n, a[1]+n, a[2]+n) -def subN(a,n): return (a[0]-n, a[1]-n, a[2]-n) -def mulN(a,n): return (a[0]*n, a[1]*n, a[2]*n) -def modN(a,n): return (a[0]%n, a[1]%n, a[2]%n) -def divN(a,n): return (a[0]/n, a[1]/n, a[2]/n) - -def sqr(a): return dot(a,a) -def length(a): return sqrt(sqr(a)) -def normalize(a): return mulN(a, 1.0/length(a)) -def avg(a,b): return mulN(add(a,b),0.5) -def distance(a,b): return length(sub(a,b)) - -def cross(a, b): - return (a[1]*b[2] - a[2]*b[1], - a[2]*b[0] - a[0]*b[2], - a[0]*b[1] - a[1]*b[0]) -def reflect(a, b): - return sub(mulN(b, dot(a, b)*2), a) - -def lerp(a,b,t): - return add(mulN(a,1.0-t), mulN(b, t)) - -def min((a0,a1,a2),(b0,b1,b2)): - return (_min(a0,b0),_min(a1,b1),_min(a2,b2)) -def max((a0,a1,a2),(b0,b1,b2)): - return (_max(a0,b0),_max(a1,b1),_max(a2,b2)) - -def toint(a): - return (int(a[0]), int(a[1]), int(a[2])) -def tofloor(a): - return (floor(a[0]), floor(a[1]), floor(a[2])) -def toceil(a): - return (ceil(a[0]), ceil(a[1]), ceil(a[2])) - -def sumlist(l): - return reduce(add, l) -def avglist(l): - return mulN(sumlist(l), 1.0/len(l)) +from __future__ import division +from math import ceil,floor,sqrt +from random import random as _random +_min,_max= min,max + +def random(): + return (_random()*2-1,_random()*2-1,_random()*2-1) + +def inv(a): return (-a[0],-a[1],-a[2]) + +def add(a,b): return (a[0]+b[0], a[1]+b[1], a[2]+b[2]) +def sub(a,b): return (a[0]-b[0], a[1]-b[1], a[2]-b[2]) +def mul(a,b): return (a[0]*b[0], a[1]*b[1], a[2]*b[2]) +def div(a,b): return (a[0]/b[0], a[1]/b[1], a[2]/b[2]) +def mod(a,b): return (a[0]%b[0], a[1]%b[1], a[2]%b[2]) +def dot(a,b): return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]) + +def addN(a,n): return (a[0]+n, a[1]+n, a[2]+n) +def subN(a,n): return (a[0]-n, a[1]-n, a[2]-n) +def mulN(a,n): return (a[0]*n, a[1]*n, a[2]*n) +def modN(a,n): return (a[0]%n, a[1]%n, a[2]%n) +def divN(a,n): return (a[0]/n, a[1]/n, a[2]/n) + +def sqr(a): return dot(a,a) +def length(a): return sqrt(sqr(a)) +def normalize(a): return mulN(a, 1.0/length(a)) +def avg(a,b): return mulN(add(a,b),0.5) +def distance(a,b): return length(sub(a,b)) + +def cross(a, b): + return (a[1]*b[2] - a[2]*b[1], + a[2]*b[0] - a[0]*b[2], + a[0]*b[1] - a[1]*b[0]) +def reflect(a, b): + return sub(mulN(b, dot(a, b)*2), a) + +def lerp(a,b,t): + return add(mulN(a,1.0-t), mulN(b, t)) + +def min((a0,a1,a2),(b0,b1,b2)): + return (_min(a0,b0),_min(a1,b1),_min(a2,b2)) +def max((a0,a1,a2),(b0,b1,b2)): + return (_max(a0,b0),_max(a1,b1),_max(a2,b2)) + +def toint(a): + return (int(a[0]), int(a[1]), int(a[2])) +def tofloor(a): + return (floor(a[0]), floor(a[1]), floor(a[2])) +def toceil(a): + return (ceil(a[0]), ceil(a[1]), ceil(a[2])) + +def sumlist(l): + return reduce(add, l) +def avglist(l): + return mulN(sumlist(l), 1.0/len(l)) diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py index 3a542272..c0741bb3 100644 --- a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py +++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py @@ -1,46 +1,46 @@ -from __future__ import division -from math import ceil,floor,sqrt -import vec3 -_min,_max= min,max - -def inv(a): return (-a[0], -a[1], -a[2], -a[3]) - -def add(a,b): return (a[0]+b[0], a[1]+b[1], a[2]+b[2], a[3]+b[3]) -def sub(a,b): return (a[0]-b[0], a[1]-b[1], a[2]-b[2], a[3]-b[3]) -def mul(a,b): return (a[0]*b[0], a[1]*b[1], a[2]*b[2], a[3]*b[3]) -def div(a,b): return (a[0]/b[0], a[1]/b[1], a[2]/b[2], a[3]/b[3]) -def mod(a,b): return (a[0]%b[0], a[1]%b[1], a[2]%b[2], a[3]%b[3]) -def dot(a,b): return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]+ a[3]*b[3]) - -def addN(a,n): return (a[0]+n, a[1]+n, a[2]+n, a[3]+n) -def subN(a,n): return (a[0]-n, a[1]-n, a[2]-n, a[3]-n) -def mulN(a,n): return (a[0]*n, a[1]*n, a[2]*n, a[3]*n) -def modN(a,n): return (a[0]%n, a[1]%n, a[2]%n, a[3]%n) -def divN(a,n): return (a[0]/n, a[1]/n, a[2]/n, a[3]/n) - -def sqr(a): return dot(a,a) -def length(a): return sqrt(sqr(a)) -def avg(a,b): return mulN(add(a,b),0.5) -def normalize(a): return mulN(a, 1.0/length(a)) - -def lerp(a,b,t): - return add(mulN(a,1.0-t), mulN(b, t)) - -def min((a0,a1,a2,a3),(b0,b1,b2,b3)): - return (_min(a0,b0),_min(a1,b1),_min(a2,b2),_min(a3,b3)) -def max((a0,a1,a2,a3),(b0,b1,b2,b3)): - return (_max(a0,b0),_max(a1,b1),_max(a2,b2),_max(a3,b3)) - -def toint(a): - return (int(a[0]), int(a[1]), int(a[2]), int(a[3])) -def tofloor(a): - return (floor(a[0]), floor(a[1]), floor(a[2]), floor(a[3])) -def toceil(a): - return (ceil(a[0]), ceil(a[1]), ceil(a[2]), ceil(a[3])) -def tovec3(a): - return vec3.divN(a, a[3]) - -def sumlist(l): - return reduce(add, l) -def avglist(l): - return mulN(sumlist(l), 1.0/len(l)) +from __future__ import division +from math import ceil,floor,sqrt +import vec3 +_min,_max= min,max + +def inv(a): return (-a[0], -a[1], -a[2], -a[3]) + +def add(a,b): return (a[0]+b[0], a[1]+b[1], a[2]+b[2], a[3]+b[3]) +def sub(a,b): return (a[0]-b[0], a[1]-b[1], a[2]-b[2], a[3]-b[3]) +def mul(a,b): return (a[0]*b[0], a[1]*b[1], a[2]*b[2], a[3]*b[3]) +def div(a,b): return (a[0]/b[0], a[1]/b[1], a[2]/b[2], a[3]/b[3]) +def mod(a,b): return (a[0]%b[0], a[1]%b[1], a[2]%b[2], a[3]%b[3]) +def dot(a,b): return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]+ a[3]*b[3]) + +def addN(a,n): return (a[0]+n, a[1]+n, a[2]+n, a[3]+n) +def subN(a,n): return (a[0]-n, a[1]-n, a[2]-n, a[3]-n) +def mulN(a,n): return (a[0]*n, a[1]*n, a[2]*n, a[3]*n) +def modN(a,n): return (a[0]%n, a[1]%n, a[2]%n, a[3]%n) +def divN(a,n): return (a[0]/n, a[1]/n, a[2]/n, a[3]/n) + +def sqr(a): return dot(a,a) +def length(a): return sqrt(sqr(a)) +def avg(a,b): return mulN(add(a,b),0.5) +def normalize(a): return mulN(a, 1.0/length(a)) + +def lerp(a,b,t): + return add(mulN(a,1.0-t), mulN(b, t)) + +def min((a0,a1,a2,a3),(b0,b1,b2,b3)): + return (_min(a0,b0),_min(a1,b1),_min(a2,b2),_min(a3,b3)) +def max((a0,a1,a2,a3),(b0,b1,b2,b3)): + return (_max(a0,b0),_max(a1,b1),_max(a2,b2),_max(a3,b3)) + +def toint(a): + return (int(a[0]), int(a[1]), int(a[2]), int(a[3])) +def tofloor(a): + return (floor(a[0]), floor(a[1]), floor(a[2]), floor(a[3])) +def toceil(a): + return (ceil(a[0]), ceil(a[1]), ceil(a[2]), ceil(a[3])) +def tovec3(a): + return vec3.divN(a, a[3]) + +def sumlist(l): + return reduce(add, l) +def avglist(l): + return mulN(sumlist(l), 1.0/len(l)) diff --git a/utils/hacks/TreeGraphs/Graphics/__init__.py b/utils/hacks/TreeGraphs/Graphics/__init__.py index 4055b3ef..645cf234 100644 --- a/utils/hacks/TreeGraphs/Graphics/__init__.py +++ b/utils/hacks/TreeGraphs/Graphics/__init__.py @@ -1 +1 @@ -__all__= ['Formats', 'SubSurf', 'Geometry', 'AqsisInterface', 'TwoD', 'ThreeD', 'Apps'] +__all__= ['Formats', 'SubSurf', 'Geometry', 'AqsisInterface', 'TwoD', 'ThreeD', 'Apps'] |