diff options
68 files changed, 1833 insertions, 1613 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/klee.sh b/.travis/klee.sh index faf3f5f5..3106dca9 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -33,7 +33,7 @@ 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="" diff --git a/.travis/stp.sh b/.travis/stp.sh index abc4e566..89d89909 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -6,6 +6,18 @@ 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 diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 00000000..07f1bb48 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,128 @@ +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 \ + 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/Makefile.common b/Makefile.common index 92f5118b..80e6e8a1 100644 --- a/Makefile.common +++ b/Makefile.common @@ -27,6 +27,12 @@ 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,7 +44,6 @@ 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)\" diff --git a/Makefile.config.in b/Makefile.config.in index ee95c4e5..fb8dbdb2 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -53,6 +53,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 := 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/autoconf/configure.ac b/autoconf/configure.ac index 5b9c4e58..747f6544 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -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..e4f8ffb6 100755 --- a/configure +++ b/configure @@ -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' @@ -1382,15 +1384,15 @@ 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 @@ -1474,10 +1476,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 +1499,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 +1512,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 +1539,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 +1547,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 +1575,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 +1588,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 # ---------------------- @@ -2460,27 +2462,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 +2487,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 +2497,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 +2531,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 +2541,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 +2563,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 +2614,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 +2685,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 +2786,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 +2848,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 +3322,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 +4146,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 +4899,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 +4945,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 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/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..032e5243 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, @@ -142,6 +148,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..45876659 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2592,9 +2592,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) { 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/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/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/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/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/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/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/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/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..dc9cacc1 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -636,9 +636,9 @@ static std::string strip(std::string &in) { static void parseArguments(int argc, char **argv) { #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 +1092,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. 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'] |