diff options
Diffstat (limited to 'autoconf/configure.ac')
-rw-r--r-- | autoconf/configure.ac | 896 |
1 files changed, 0 insertions, 896 deletions
diff --git a/autoconf/configure.ac b/autoconf/configure.ac deleted file mode 100644 index 3dccd9b7..00000000 --- a/autoconf/configure.ac +++ /dev/null @@ -1,896 +0,0 @@ -dnl ************************************************************************** -dnl * Initialize -dnl ************************************************************************** -AC_INIT([[KLEE]],[[1.4.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]]) - -dnl Identify where LLVM source tree is (this is patched by -dnl AutoRegen.sh) -LLVM_SRC_ROOT=XXX - -dnl Tell autoconf that the auxilliary files are actually located in -dnl the LLVM autoconf directory, not here. -AC_CONFIG_AUX_DIR($LLVM_SRC_ROOT/autoconf) - -dnl Tell autoconf that this is an LLVM project being configured -dnl This provides the --with-llvmsrc and --with-llvmobj options -LLVM_CONFIG_PROJECT("","") - -dnl Verify that the source directory is valid -AC_CONFIG_SRCDIR(["Makefile.config.in"]) - -dnl Configure a common Makefile -AC_CONFIG_FILES(Makefile.config) - -dnl Configure Doxygen file -AC_CONFIG_FILES([docs/doxygen.cfg]) - -dnl Configure project makefiles -dnl List every Makefile that exists within your source tree -AC_CONFIG_HEADERS([include/klee/Config/config.h]) - -AH_TOP([#ifndef KLEE_CONFIG_CONFIG_H -#define KLEE_CONFIG_CONFIG_H]) -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 - -AC_CANONICAL_TARGET - -dnl Determine the platform type and cache its value. This helps us configure -dnl the System library to the correct build platform. -AC_CACHE_CHECK([type of operating system we're going to host on], - [klee_cv_os_type], -[case $host in - *-*-linux*) - host_supports_posix_runtime=yes ;; - *) - host_supports_posix_runtime=no ;; -esac]) - -dnl ************************************************************************** -dnl Verify that we can find llvm - -dnl --with-llvm is a shortcut for setting srcdir and objdir. -AC_ARG_WITH(llvm, - AS_HELP_STRING([--with-llvm], - [Location of LLVM Source and Object code]),,) - -AC_MSG_CHECKING([llvm source dir]) - -if test X${with_llvm} != X; then - dnl Verify that --with-llvm{src,obj} were not given. - if test X${with_llvmsrc} != X; then - AC_MSG_ERROR([--with-llvmsrc cannot be specified when using --with-llvm]) - fi - if test X${with_llvmobj} != X; then - AC_MSG_ERROR([--with-llvmobj cannot be specified when using --with-llvm]) - fi - with_llvmsrc=$with_llvm - with_llvmobj=$with_llvm -fi - -dnl If one of with_llvmsrc or with_llvmobj was given, we must have both. -if (test X${with_llvmsrc} != X || test X${with_llvmobj} != X); then - dnl Verify that with_llvmobj was given as well. - if test X${with_llvmsrc} = X; then - AC_MSG_ERROR([--with-llvmsrc must be specified when using --with-llvmobj]) - fi - if test X${with_llvmobj} = X; then - AC_MSG_ERROR([--with-llvmobj must be specified when using --with-llvmsrc]) - fi -else - dnl Otherwise try and use llvm-config to find. - llvm_version=`llvm-config --version` - if test X${llvm_version} = X; then - AC_MSG_ERROR([unable to find llvm, use --with-llvmsrc and --with-llvmobj]) - fi - - with_llvmsrc=`llvm-config --src-root` - with_llvmobj=`llvm-config --obj-root` -fi - -dnl Try to validate directories. -if test ! -f ${with_llvmsrc}/Makefile.rules; then - AC_MSG_ERROR([invalid llvmsrc directory: ${with_llvmsrc}]) -fi -if test ! -f ${with_llvmobj}/Makefile.config; then - AC_MSG_ERROR([invalid llvmobj directory: ${with_llvmobj}]) -fi - -dnl Make the paths absolute. -llvm_src=`cd $with_llvmsrc 2> /dev/null; pwd` -llvm_obj=`cd $with_llvmobj 2> /dev/null; pwd` - -AC_MSG_RESULT([$llvm_src]) - -dnl Report obj dir as well. -AC_MSG_CHECKING([llvm obj dir]) -AC_MSG_RESULT([$llvm_obj]) - -AC_SUBST(LLVM_SRC,$llvm_src) -AC_SUBST(LLVM_OBJ,$llvm_obj) - -dnl Determine LLVM version. -AC_MSG_CHECKING([llvm package version]) -llvm_package_version=`grep PACKAGE_VERSION= $with_llvmsrc/configure | cut -d\' -f 2` -AC_MSG_RESULT([$llvm_package_version]) - -llvm_version_split=`python -c "import re; print('\t'.join(map(str, re.match('([[0-9]]+)[.]([[0-9]]+)(svn)?', \"$llvm_package_version\").groups())))"` - -AC_MSG_CHECKING([llvm version major]) -llvm_version_major=`echo "$llvm_version_split" | cut -f 1` -AC_MSG_RESULT([$llvm_version_major]) - -AC_MSG_CHECKING([llvm version minor]) -llvm_version_minor=`echo "$llvm_version_split" | cut -f 2` -AC_MSG_RESULT([$llvm_version_minor]) - -AC_MSG_CHECKING([llvm is release version]) -llvm_version_svn=`echo "$llvm_version_split" | cut -f 3` -if test "$llvm_version_svn" == "svn"; then - llvm_is_release=0 -else - llvm_is_release=1 -fi -AC_MSG_RESULT([$llvm_is_release]) - -AC_DEFINE_UNQUOTED(LLVM_VERSION_MAJOR, $llvm_version_major, [LLVM major version number]) -AC_SUBST(LLVM_VERSION_MAJOR,$llvm_version_major) -AC_DEFINE_UNQUOTED(LLVM_VERSION_MINOR, $llvm_version_minor, [LLVM minor version number]) -AC_SUBST(LLVM_VERSION_MINOR,$llvm_version_minor) -AC_DEFINE_UNQUOTED(LLVM_IS_RELEASE, $llvm_is_release, [LLVM version is release (instead of development)]) -AC_SUBST(LLVM_IS_RELEASE,$llvm_is_release) - -dnl LLVM <= 2.6 requires RTTI. -if test $llvm_version_major -eq 2 -a $llvm_version_minor -le 6 ; then - requires_rtti=1 -else - requires_rtti=0 -fi -AC_SUBST(REQUIRES_RTTI,$requires_rtti) - -dnl Provide option to use C++11 -AC_ARG_ENABLE([cxx11],[ --enable-cxx11 Build using C++11], [klee_use_cxx11=1], [klee_use_cxx11=0]) - -dnl LLVM >= 3.5 requires C++11 -AC_MSG_CHECKING([if LLVM needs C++11]) -if test '(' $llvm_version_major -eq 3 -a $llvm_version_minor -ge 5 ')' -o '(' $llvm_version_major -gt 3 ')' ; then - klee_use_cxx11=1 - AC_MSG_RESULT([yes]) -else - AC_MSG_RESULT([no]) -fi - -dnl Check if the compiler supports C++11 (this check is taken from LLVM's configure.ac). -if test X${klee_use_cxx11} = X1; then - klee_old_cxxflags="$CXXFLAGS" - CXXFLAGS="$CXXFLAGS -std=c++11" - AC_LINK_IFELSE([AC_LANG_SOURCE([[ -#include <atomic> -std::atomic<float> x(0.0f); -int main() { return (float)x; } -]])], - [AC_MSG_RESULT([yes])], - [AC_MSG_RESULT([no]) - AC_MSG_ERROR([C++11 not supported])]) - CXXFLAGS="$klee_old_cxxflags" -fi - -AC_SUBST(KLEE_USE_CXX11,$klee_use_cxx11) - - -AC_ARG_WITH(llvm-build-mode, - AS_HELP_STRING([--with-llvm-build-mode], - [LLVM build mode (e.g. Debug or Release, default autodetect)]),,[with_llvm_build_mode=check]) - -AC_MSG_CHECKING([llvm build mode]) - -if test X${with_llvm_build_mode} = Xcheck ; then - llvm_configs="`ls -1 $llvm_obj/*/bin/llvm-config 2>/dev/null | head -n 1`" - if test -x "$llvm_configs" ; then - llvm_build_mode="`$llvm_configs --build-mode`" - else - AC_MSG_ERROR([Could not autodetect build mode]) - fi -else - llvm_configs="`echo $llvm_obj/*/bin/llvm-config`" - if test -x "$llvm_obj/$with_llvm_build_mode/bin/llvm-config" ; then - llvm_build_mode=$with_llvm_build_mode - else - AC_MSG_ERROR([Invalid build mode: $llvm_build_mode]) - fi -fi - -AC_MSG_RESULT([$llvm_build_mode]) -AC_SUBST(LLVM_BUILD_MODE,$llvm_build_mode) - -dnl Check if we are building against a +Asserts LLVM, and enable the DEBUG_* -dnl macros if so (they use symbols only available in +Asserts builds). -AC_MSG_CHECKING([llvm has asserts enabled]) -if test `expr "$llvm_build_mode" : ".*Asserts.*"` -ne 0; then - llvm_has_asserts_enabled=1 - AC_DEFINE_UNQUOTED(ENABLE_KLEE_DEBUG, 1, [Enable KLEE DEBUG checks]) -else - llvm_has_asserts_enabled=0 -fi -AC_MSG_RESULT([$llvm_has_asserts_enabled]) - -dnl ************************************************************************** -dnl Detect a LLVM Bitcode compiler for building KLEE runtime library - -dnl Check for clang built with llvm build -AC_MSG_CHECKING([LLVM Bitcode compiler]) -klee_llvm_bc_c_compiler="" -klee_llvm_bc_cxx_compiler="" - -AC_ARG_WITH([llvmcc], - AS_HELP_STRING([--with-llvmcc], - [Set the path to the C LLVM bitcode compiler to use (Default: auto-detect). If set, --with-llvmcxx= must be set too.] - ), - [], - [with_llvmcc=none] - ) - -AC_ARG_WITH([llvmcxx], - AS_HELP_STRING([--with-llvmcxx], - [Set the path to the C++ LLVM bitcode compiler to use (Default: auto-detect). If set, --with-llvmcc= must be set too.] - ), - [], - [with_llvmcxx=none] - ) -if test \( "X$with_llvmcc" != Xnone -a "X$with_llvmcxx" = Xnone \) -o \( "X$with_llvmcxx" != Xnone -a "X$with_llvmcc" = Xnone \) ; then - AC_MSG_ERROR([You must set both --with-llvmcc= and --with-llvmcxx= or set neither]) -fi - -if test X$with_llvmcc = Xnone ; then - dnl Try to automatically find compiler - - dnl Try Clang inside the LLVM build - if test -x "$llvm_obj/$llvm_build_mode/bin/clang" ; then - AC_MSG_RESULT([Found clang in LLVM Build]) - klee_llvm_bc_c_compiler="$llvm_obj/$llvm_build_mode/bin/clang" - - if test -x "$llvm_obj/$llvm_build_mode/bin/clang++" ; then - klee_llvm_bc_cxx_compiler="$llvm_obj/$llvm_build_mode/bin/clang++" - else - AC_MSG_ERROR([Found clang but could not find clang++]) - fi - fi - - dnl Try llvm-gcc in PATH - if test "X${klee_llvm_bc_c_compiler}" = X ; then - AC_MSG_RESULT([]) # Force a new line - AC_CHECK_PROG(llvm_gcc,llvm-gcc,FOUND,NOT_FOUND) - if test ${llvm_gcc} = FOUND ; then - klee_llvm_bc_c_compiler=`which llvm-gcc` - - AC_CHECK_PROG(llvm_gxx,llvm-g++,FOUND,NOT_FOUND) - if test ${llvm_gxx} = FOUND; then - klee_llvm_bc_cxx_compiler=`which llvm-g++` - else - AC_MSG_ERROR([Found llvm-gcc but could not find llvm-g++ in PATH]) - fi - fi - - fi - - dnl Try clang in PATH - if test "X${klee_llvm_bc_c_compiler}" = X ; then - AC_MSG_RESULT([]) # Force a new line - AC_CHECK_PROG(clang,clang,FOUND,NOT_FOUND) - if test ${clang} = FOUND ; then - klee_llvm_bc_c_compiler=`which clang` - - AC_CHECK_PROG(clang_cxx,clang++,FOUND,NOT_FOUND) - if test ${clang_cxx} = FOUND; then - klee_llvm_bc_cxx_compiler=`which clang++` - else - AC_MSG_ERROR([Found clang but could not find clang++ in PATH]) - fi - fi - - fi - - if test X"${klee_llvm_bc_c_compiler}" = X ; then - AC_MSG_ERROR([Could not find a C LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?]) - fi - - if test X"${klee_llvm_bc_cxx_compiler}" = X ; then - AC_MSG_ERROR([Could not find a C++ LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?]) - fi - -else - dnl Use user supplied values - klee_llvm_bc_c_compiler="$with_llvmcc" - klee_llvm_bc_cxx_compiler="$with_llvmcxx" - - if test \! -x "${klee_llvm_bc_c_compiler}"; then - AC_MSG_ERROR([--with-llvmcc= supplied compiler does not exist]) - fi - - if test \! -x "${klee_llvm_bc_cxx_compiler}"; then - AC_MSG_ERROR([--with-llvmcxx= supplied compiler does not exist]) - fi - AC_MSG_RESULT([Using user supplied LLVM bitcode compilers.]) -fi - -dnl Tell the user what we are going to try and use -AC_MSG_RESULT([Using C llvm compiler : $klee_llvm_bc_c_compiler]) -AC_MSG_RESULT([Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler]) - -dnl Test that the bitcode compiler works - -dnl Function for checking bitcode compiler works -dnl $1 : compiler to invoke -dnl $2 : source code extension (e.g. cpp or c) -dnl $3 : Compiler string (e.g. CXX or C) -function klee_check_bc() -{ - AC_MSG_CHECKING([${3} LLVM Bitcode compiler works]) - dnl FIXME: write to tmp directory instead of binary build dir - klee_bc_test_file="./.klee_llvm_bitcode_test.${2}" - - echo "int main() { return 0;}" > "${klee_bc_test_file}" - "${1}" -emit-llvm -c "${klee_bc_test_file}" -o "${klee_bc_test_file}.bc" - if test $? -ne 0 ; then - AC_MSG_ERROR([Failed running ${3} LLVM Bitcode compiler]) - fi - - if test \! -e "${klee_bc_test_file}.bc"; then - AC_MSG_ERROR([ ${3} LLVM Bitcode compiler did not produce any output]) - fi - - dnl Convert bitcode to human readable form as a hacky check - dnl that the version of LLVM we are configuring with can - dnl parse the LLVM bitcode produced by the detected compiler - if test -x "$llvm_obj/$llvm_build_mode/bin/llvm-dis" ; then - "$llvm_obj/$llvm_build_mode/bin/llvm-dis" -o "${klee_bc_test_file}.ll" "${klee_bc_test_file}.bc" - - if test $? -ne 0; then - AC_MSG_ERROR([Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?]) - fi - - if test -e "${klee_bc_test_file}.ll" ; then - AC_MSG_RESULT([Success]) - rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" - else - rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" - AC_MSG_ERROR([Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?]) - fi - - else - rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" - AC_MSG_ERROR([Could not find llvm-dis]) - fi -} - -dnl Invoke previously defined function to check the LLVM bitcode compilers -klee_check_bc "${klee_llvm_bc_c_compiler}" "c" "C" -klee_check_bc "${klee_llvm_bc_cxx_compiler}" "cpp" "CXX" - -dnl Set variable for Makefile.config -AC_SUBST(KLEE_BITCODE_C_COMPILER,$klee_llvm_bc_c_compiler) -AC_SUBST(KLEE_BITCODE_CXX_COMPILER,$klee_llvm_bc_cxx_compiler) - -dnl ************************************************************************** -dnl User option to disable timestamping. - -AC_ARG_ENABLE([timestamp],AS_HELP_STRING([--enable-timestamp], - [Enable timestamping the source code while building. (default=disabled)])) - -if test "x${enable_timestamp}" = "xyes" ; then - AC_DEFINE(KLEE_ENABLE_TIMESTAMP,[1],[Enable time stamping the sources]) - AC_MSG_NOTICE([Source timestamping enabled.]) -else - AC_MSG_NOTICE([Source timestamping disabled.]) -fi - -dnl ************************************************************************** -dnl User option to enable uClibc support. - -AC_ARG_WITH(uclibc, - AS_HELP_STRING([--with-uclibc], - [Enable use of the klee uclibc at the given path (klee-uclibc root directory or libc.a file]),,) - -dnl Validate uclibc if given. - -AC_MSG_CHECKING([uclibc]) -if (test X${with_uclibc} != X); then - if test -d ${with_uclibc}; then - dnl Support the legacy way of configuring with - dnl klee-uclibc, i.e. the root klee-uclibc - dnl directory is passed as an argument. - - dnl Make the path absolute - with_uclibc=`cd $with_uclibc 2> /dev/null; pwd` - - dnl create path to libc file - KLEE_UCLIBC_BCA="${with_uclibc}/lib/libc.a" - - if test ! -e "${KLEE_UCLIBC_BCA}"; then - AC_MSG_ERROR([Could not find file ${KLEE_UCLIBC_BCA}]) - fi - elif test -f ${with_uclibc}; then - dnl Support the new way of configuring klee-uclibc - dnl i.e. the built bitcode archive is passed as the - dnl argument. - - dnl Get absolute path to file - _kud=`dirname ${with_uclibc}` - _kud=`cd ${_kud}; pwd 2> /dev/null` - _kuf=`basename ${with_uclibc}` - - KLEE_UCLIBC_BCA="${_kud}/${_kuf}" - else - AC_MSG_ERROR([Could not detect klee-uclibc]) - fi - - dnl FIXME: Validate the libc.a file - - AC_MSG_RESULT([$KLEE_UCLIBC_BCA]) - AC_SUBST(ENABLE_UCLIBC,[[1]]) - AC_SUBST(KLEE_UCLIBC_BCA) - AC_DEFINE(SUPPORT_KLEE_UCLIBC, [[1]], [klee-uclibc is supported]) -else - AC_MSG_RESULT([no]) - AC_SUBST(ENABLE_UCLIBC,[[0]]) -fi - - -dnl ************************************************************************** -dnl User option to enable the POSIX runtime - -AC_ARG_ENABLE(posix-runtime, - AS_HELP_STRING([--enable-posix-runtime], - [Enable the POSIX runtime]), - ,enableval=default) - -AC_MSG_CHECKING([POSIX runtime]) -if test ${enableval} = "default" ; then - if test X${with_uclibc} != X; then - enableval=$host_supports_posix_runtime - if test ${enableval} = "yes"; then - AC_MSG_RESULT([default (enabled)]) - else - AC_MSG_RESULT([default (disabled, unsupported target)]) - fi - else - enableval="no" - AC_MSG_RESULT([default (disabled, no uclibc)]) - fi -else - if test ${enableval} = "yes" ; then - AC_MSG_RESULT([yes]) - else - AC_MSG_RESULT([no]) - fi -fi - -if test ${enableval} = "yes" ; then - AC_SUBST(ENABLE_POSIX_RUNTIME,[[1]]) -else - AC_SUBST(ENABLE_POSIX_RUNTIME,[[0]]) -fi - -dnl ************************************************************************** -dnl User option to select runtime version - -AC_ARG_WITH(runtime, - AS_HELP_STRING([--with-runtime], - [Select build configuration for runtime libraries (default [Release+Asserts])]),, - withval=default) -if test X"${withval}" = Xdefault; then - with_runtime=Release+Asserts -fi - -AC_MSG_CHECKING([runtime configuration]) -if test X${with_runtime} = XRelease; then - AC_MSG_RESULT([Release]) - AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]]) - AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[1]]) - AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[]]) -elif test X${with_runtime} = XRelease+Asserts; then - AC_MSG_RESULT([Release+Asserts]) - AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]]) - AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[0]]) - AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[]]) -elif test X${with_runtime} = XDebug; then - AC_MSG_RESULT([Debug]) - AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]]) - AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[1]]) - AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[1]]) -elif test X${with_runtime} = XDebug+Asserts; then - AC_MSG_RESULT([Debug+Asserts]) - AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]]) - AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[0]]) - AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[1]]) -else - AC_MSG_ERROR([invalid configuration: ${with_runtime}]) -fi - -AC_DEFINE_UNQUOTED(RUNTIME_CONFIGURATION, "$with_runtime", [Configuration for runtime libraries]) -AC_SUBST(RUNTIME_CONFIGURATION) - -dnl ************************************************************************** -dnl See if we should support __ctype_b_loc externals. - -dnl FIXME: Do the proper test if we continue to need this. -case $host in - *-*-linux*) - AC_DEFINE_UNQUOTED(HAVE_CTYPE_EXTERNALS, 1, [Does the platform use __ctype_b_loc, etc.]) -esac - -dnl ************************************************************************** -dnl Checks for header files. - -dnl NOTE: This is mostly just to force autoconf to make CFLAGS defines -dnl for us. -AC_LANG_PUSH([C]) - -AC_CHECK_HEADERS([sys/acl.h]) - -AC_CHECK_LIB([cap], [cap_get_proc], [have_cap=yes], [have_cap=no]) -if test "x${have_cap}" = xyes; then - AC_CHECK_HEADERS([sys/capability.h], [], [have_cap=no]) -fi -if test "x${have_cap}" = xno; then - AC_MSG_WARN([Library cap and its header file sys/capability.h not found, disabling chroot \ -capability checking support for klee-replay.]) -fi - -AC_CHECK_HEADERS([selinux/selinux.h], - AC_SUBST(HAVE_SELINUX, 1), - AC_SUBST(HAVE_SELINUX, 0)) - -if test "$HAVE_SELINUX" = "1"; then - # Test what function signature we need to use for SELinux. The signatures - # have changed between 2.2 and 2.3. In particular, the type of the "security - # context" parameter was changed from char * to const char *, with this - # patch: [PATCH] Get rid of security_context_t and fix const declarations. - # [http://www.spinics.net/lists/selinux/msg14827.html] - AC_CACHE_CHECK([for selinux security context type constness], - [klee_cv_sel_ctx_const], - [AC_COMPILE_IFELSE( - [AC_LANG_PROGRAM([[ -#include <selinux/selinux.h> -int setcon(char *context);]])], - [klee_cv_sel_ctx_const=''], - [klee_cv_sel_ctx_const='const'])]) - AC_DEFINE_UNQUOTED([KLEE_SELINUX_CTX_CONST], [$klee_cv_sel_ctx_const], - [Define to empty or 'const' depending on how SELinux qualifies its - security context parameters.]) -fi - -AC_LANG_POP([C]) - -dnl ************************************************************************** -dnl Test for features -dnl ************************************************************************** - -AC_CHECK_HEADERS([malloc/malloc.h]) -AC_CHECK_FUNCS([malloc_zone_statistics]) -AC_SEARCH_LIBS(mallinfo,malloc, - AC_DEFINE([HAVE_MALLINFO],[1],[Define if mallinfo() is available on this platform.])) - -dnl ************************************************************************** -dnl Test for tcmalloc -dnl ************************************************************************** - -AC_ARG_WITH([tcmalloc], - AS_HELP_STRING([--without-tcmalloc], [Ignore presence of tcmalloc and disable it (default=detect)])) - -AS_IF([test "x$with_tcmalloc" != "xno"], - AC_CHECK_HEADERS([gperftools/malloc_extension.h], - [have_tcmalloc=yes], [have_tcmalloc=no]), - [have_tcmalloc=no]) - -AS_IF([test "x$have_tcmalloc" = "xyes"], - [ - AC_SEARCH_LIBS(tc_malloc,tcmalloc_minimal, - [ - AC_SUBST(HAVE_TCMALLOC, 1) - if test "${ac_cv_search_tc_malloc}" != "none required"; then - TCMALLOC_LIB=${ac_cv_search_tc_malloc} - AC_SUBST(TCMALLOC_LIB) - fi - ], - [ - AC_MSG_WARN([Could not link with tcmalloc]) - AC_SUBST(HAVE_TCMALLOC, 0) - ],) - - ], - [AS_IF([test "x$with_tcmalloc" = "xyes"], - [AC_MSG_ERROR([tcmalloc requested but not found])], - [ - AC_SUBST(HAVE_TCMALLOC, 0) - ]) -]) - -dnl ************************************************************************** -dnl Test for zlib -dnl ************************************************************************** - -AC_ARG_WITH([zlib], - AS_HELP_STRING([--without-zlib], [Ignore presence of zlib and disable it (default=detect)])) - -AS_IF([test "x$with_zlib" != "xno"], - AC_CHECK_HEADERS([zlib.h], - [have_zlib=yes], [have_zlib=no]), - [have_zlib=no]) - -AS_IF([test "x$have_zlib" = "xyes"], - [ - AC_SEARCH_LIBS(deflateEnd, z, - [ - AC_SUBST(HAVE_ZLIB, 1) - if test "${ac_cv_search_zlib}" != "none required"; then - ZLIB_LIB=${ac_cv_search_zlib} - AC_SUBST(ZLIB_LIB) - fi - ], - [ - AC_MSG_WARN([Could not link with zlib]) - AC_SUBST(HAVE_ZLIB, 0) - ],) - - ], - [AS_IF([test "x$with_zlib" = "xyes"], - [AC_MSG_ERROR([zlib requested but not found])], - [ - AC_SUBST(HAVE_ZLIB, 0) - ]) -]) - -dnl ************************************************************************** -dnl Find an install of STP -dnl ************************************************************************** - -ENABLE_STP=0 -AC_ARG_WITH(stp, - AS_HELP_STRING([--with-stp], - [Location of STP installation directory]),[ - #Check for empty argument - if test "X$withval" = X ; then - AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>]) - fi - stp_root=`(cd $withval && pwd) 2> /dev/null` - - #Check for bad path - if test "X$stp_root" = X ; then - AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp]) - fi - - STP_CFLAGS="-I$stp_root/include" - STP_LDFLAGS="-L$stp_root/lib" - ENABLE_STP=1 - ]) - -if test "X$ENABLE_STP" != X0; then - old_CPPFLAGS="$CPPFLAGS" - CPPFLAGS="$CPPFLAGS $STP_CFLAGS" - AC_CHECK_HEADER(stp/c_interface.h,, - [ - AC_MSG_ERROR([Unable to use stp/c_interface.h header]) - ]) - - dnl we use [:] as a no-op so that AC_CHECK_LIB doesn't append -lstp - dnl automatically which would break subsequent uses of AC_CHECK_LIB() - STP_NEEDS_MINISAT=0 - AC_CHECK_LIB(stp, vc_setInterfaceFlags, [:], [ - STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp]) - ], "$STP_LDFLAGS") - CPPFLAGS="$old_CPPFLAGS" - - 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_MSG_NOTICE([Using STP solver backend]) - CPPFLAGS="$old_CPPFLAGS" - AC_DEFINE(ENABLE_STP, [1], [Using STP Solver backend]) -else - AC_MSG_NOTICE([Not using STP solver backend]) -fi - -AC_SUBST(ENABLE_STP) -AC_SUBST(STP_CFLAGS) -AC_SUBST(STP_LDFLAGS) - -dnl ************************************************************************** -dnl Find an install of Z3 -dnl ************************************************************************** - -ENABLE_Z3=0 -AC_ARG_WITH(z3, - AS_HELP_STRING([--with-z3], [Location of Z3 installation directory]), [ - # Check for empty argument - if test "X$withval" = X ; then - AC_MSG_ERROR([<path> cannot be empty in --with-z3=<path>]) - fi - z3_root=`(cd $withval && pwd) 2> /dev/null` - - #Check for bad path - if test "X$z3_root" = X ; then - AC_MSG_ERROR([Cannot access path $with_z3 passed to --with-z3]) - fi - - Z3_CFLAGS="-I$z3_root/include" - Z3_LDFLAGS="-L$z3_root/lib" - ENABLE_Z3=1 - ]) - -if test "X$ENABLE_Z3" != X0 ; then - old_CPPFLAGS="$CPPFLAGS" - CPPFLAGS="$CPPFLAGS $Z3_CFLAGS" - old_CPPFLAGS="$CPPFLAGS" - AC_CHECK_HEADER(z3.h,, - [ - AC_MSG_ERROR([Unable to use z3.h header]) - ]) - CPPFLAGS="$old_CPPFLAGS" - - AC_CHECK_LIB(z3, Z3_mk_context,[:], [ - AC_MSG_ERROR([Unable to link against z3]) - ], "$Z3_LDFLAGS") - - # Test which function signature of ``Z3_get_error_msg()`` we need to use. - # There's an API break between Z3 4.4.1 and the master branch - AC_MSG_CHECKING([if Z3_get_error_msg() requires Z3_context]) - AC_COMPILE_IFELSE( - [AC_LANG_PROGRAM([[#include "z3.h"]], - [[Z3_context c = Z3_mk_context(0); Z3_get_error_msg(c, Z3_OK);]])], - [Z3_HAS_ERROR_MSG_CONTEXT=1], - [Z3_HAS_ERROR_MSG_CONTEXT=0]) - - if test "X$Z3_HAS_ERROR_MSG_CONTEXT" == X1; then - AC_DEFINE(HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT, [1], [Z3 needs a Z3_context passed to Z3_get_error_msg()]) - AC_MSG_RESULT([yes]) - else - AC_MSG_RESULT([no]) - fi - - Z3_LDFLAGS="${Z3_LDFLAGS} -lz3" - AC_MSG_NOTICE([Using Z3 solver backend]) - CPPFLAGS="$old_CPPFLAGS" - AC_DEFINE(ENABLE_Z3, [1], [Using Z3 Solver backend]) -else - AC_MSG_NOTICE([Not using Z3 solver backend]) -fi - -AC_SUBST(ENABLE_Z3) -AC_SUBST(Z3_CFLAGS) -AC_SUBST(Z3_LDFLAGS) - - -dnl ************************************************************************** -dnl User option to enable metaSMT constraint solvers and to specify the -dnl the location of the metaSMT root directory -dnl ************************************************************************** - -AC_ARG_WITH(metasmt, - AS_HELP_STRING([--with-metasmt], - [Location of metaSMT installation directory]),,) -if test X$with_metasmt = X ; then - ENABLE_METASMT=0 - AC_MSG_NOTICE([Not using MetaSMT solver backend]) -else - metasmt_root=`(cd $with_metasmt && pwd) 2> /dev/null` - #Check for bad path - if test "X$metasmt_root" = X ; then - AC_MSG_ERROR([Cannot access path $with_metasmt passed to --with-metasmt]) - fi - - dnl AC_LANG(C++) - old_CPPFLAGS="$CPPFLAGS" - old_LDFLAGS="$LDFLAGS" - old_LIBS="$LIBS" - CPPFLAGS="$CPPFLAGS -I$metasmt_root/include" - LDFLAGS="$LDFLAGS -L$metasmt_root/lib" - LIBS="$LIBS -lmetaSMT" - - AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [ - AC_MSG_ERROR([Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header]) - ]) - AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT]) - AC_LINK_IFELSE( - [AC_LANG_PROGRAM([#include <metaSMT/frontend/QF_BV.hpp>], [metaSMT::logic::QF_BV::new_bitvector(3)])], - [AC_MSG_RESULT([yes])], - [AC_MSG_RESULT([no]) - AC_MSG_ERROR([Unable to link with libmetaSMT])]) - CPPFLAGS="$old_CPPFLAGS" - LDFLAGS="$old_LDFLAGS" - LIBS="$old_LIBS" - - AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API]) - AC_SUBST(METASMT_ROOT,$metasmt_root) - ENABLE_METASMT=1 - AC_MSG_NOTICE([Using MetaSMT solver backend]) -fi - -AC_SUBST(ENABLE_METASMT) - - -dnl ************************************************************************** -dnl User option to specify the default backend of metaSMT -dnl ************************************************************************** - -AC_ARG_WITH(metasmt-default-backend, - AS_HELP_STRING([--with-metasmt-default-backend], - [Default backend of metaSMT (btor|stp|z3, stp if unspecified)]),,) - -if test "X$with_metasmt_default_backend" != X ; then - if test "X$ENABLE_METASMT" != X1 ; then - AC_MSG_ERROR([--with-metasmt-default-backend requires metaSMT to be enabled]) - fi - if test "$with_metasmt_default_backend" == "btor" ; then - METASMT_DEFAULT_BACKEND=BTOR - AC_MSG_NOTICE([metaSMT uses Boolector as default backend]) - fi - if test "$with_metasmt_default_backend" == "z3" ; then - METASMT_DEFAULT_BACKEND=Z3 - AC_MSG_NOTICE([metaSMT uses Z3 as default backend]) - fi - if test "$with_metasmt_default_backend" == "stp" ; then - METASMT_DEFAULT_BACKEND=STP - AC_MSG_NOTICE([metaSMT uses STP as default backend]) - fi - if test "X$METASMT_DEFAULT_BACKEND" == X ; then - METASMT_DEFAULT_BACKEND=STP - AC_MSG_NOTICE([$with_metasmt_default_backend unsupported, metaSMT uses STP as default backend]) - fi -else - if test "X$ENABLE_METASMT" == X1 ; then - METASMT_DEFAULT_BACKEND=STP - AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default backend]) - fi -fi - -AC_SUBST(METASMT_DEFAULT_BACKEND) - - -dnl ************************************************************************** -dnl Check at least one solver backend is enabled -dnl ************************************************************************** - -if test "X$ENABLE_STP$ENABLE_Z3$ENABLE_METASMT" == X000 ; then - AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp, --with-z3 or --with-metasmt]) -fi - - -dnl ************************************************************************** -dnl * Create the output files -dnl ************************************************************************** - -dnl Do special configuration of Makefiles -AC_CONFIG_MAKEFILE(Makefile) -AC_CONFIG_MAKEFILE(Makefile.common) -AC_CONFIG_MAKEFILE(lib/Makefile) -AC_CONFIG_MAKEFILE(runtime/Makefile) -AC_CONFIG_MAKEFILE(test/Makefile) -AC_CONFIG_MAKEFILE(test/Makefile.tests) -AC_CONFIG_MAKEFILE(test/Concrete/Makefile) -AC_CONFIG_MAKEFILE(tools/Makefile) -AC_CONFIG_MAKEFILE(unittests/Makefile) - -dnl This must be last -AC_OUTPUT |