diff options
| -rw-r--r-- | Makefile.config.in | 4 | ||||
| -rw-r--r-- | autoconf/configure.ac | 53 | ||||
| -rwxr-xr-x | configure | 110 | ||||
| -rw-r--r-- | include/klee/Config/config.h.in | 3 |
4 files changed, 166 insertions, 4 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 745b4cc1..f92f453f 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -36,6 +36,10 @@ STP_LDFLAGS := @STP_LDFLAGS@ ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ +ENABLE_Z3 := @ENABLE_Z3@ +Z3_CFLAGS := @Z3_CFLAGS@ +Z3_LDFLAGS := @Z3_LDFLAGS@ + ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@ ENABLE_UCLIBC := @ENABLE_UCLIBC@ diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 0cf08a60..94928fcc 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -614,6 +614,55 @@ 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") + + 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 @@ -661,8 +710,8 @@ dnl ************************************************************************** dnl Check at least one solver backend is enabled dnl ************************************************************************** -if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then - AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp or --with-metasmt]) +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 diff --git a/configure b/configure index ce8a2d72..571c4338 100755 --- a/configure +++ b/configure @@ -626,6 +626,9 @@ ac_subst_vars='LTLIBOBJS LIBOBJS ENABLE_METASMT METASMT_ROOT +Z3_LDFLAGS +Z3_CFLAGS +ENABLE_Z3 STP_LDFLAGS STP_CFLAGS ENABLE_STP @@ -731,6 +734,7 @@ with_uclibc enable_posix_runtime with_runtime with_stp +with_z3 with_metasmt ' ac_precious_vars='build_alias @@ -1382,6 +1386,7 @@ Optional Packages: --with-runtime Select build configuration for runtime libraries (default [Release+Asserts]) --with-stp Location of STP installation directory + --with-z3 Location of Z3 installation directory --with-metasmt Location of metaSMT installation directory Some influential environment variables: @@ -5020,6 +5025,107 @@ fi +ENABLE_Z3=0 + +# Check whether --with-z3 was given. +if test "${with_z3+set}" = set; then : + withval=$with_z3; + # Check for empty argument + if test "X$withval" = X ; then + as_fn_error $? "<path> cannot be empty in --with-z3=<path>" "$LINENO" 5 + fi + z3_root=`(cd $withval && pwd) 2> /dev/null` + + #Check for bad path + if test "X$z3_root" = X ; then + as_fn_error $? "Cannot access path $with_z3 passed to --with-z3" "$LINENO" 5 + fi + + Z3_CFLAGS="-I$z3_root/include" + Z3_LDFLAGS="-L$z3_root/lib" + ENABLE_Z3=1 + +fi + + +if test "X$ENABLE_Z3" != X0 ; then + old_CPPFLAGS="$CPPFLAGS" + CPPFLAGS="$CPPFLAGS $Z3_CFLAGS" + old_CPPFLAGS="$CPPFLAGS" + ac_fn_cxx_check_header_mongrel "$LINENO" "z3.h" "ac_cv_header_z3_h" "$ac_includes_default" +if test "x$ac_cv_header_z3_h" = xyes; then : + +else + + as_fn_error $? "Unable to use z3.h header" "$LINENO" 5 + +fi + + + CPPFLAGS="$old_CPPFLAGS" + + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for Z3_mk_context in -lz3" >&5 +$as_echo_n "checking for Z3_mk_context in -lz3... " >&6; } +if ${ac_cv_lib_z3_Z3_mk_context+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_check_lib_save_LIBS=$LIBS +LIBS="-lz3 "$Z3_LDFLAGS" $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 Z3_mk_context (); +int +main () +{ +return Z3_mk_context (); + ; + return 0; +} +_ACEOF +if ac_fn_cxx_try_link "$LINENO"; then : + ac_cv_lib_z3_Z3_mk_context=yes +else + ac_cv_lib_z3_Z3_mk_context=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_z3_Z3_mk_context" >&5 +$as_echo "$ac_cv_lib_z3_Z3_mk_context" >&6; } +if test "x$ac_cv_lib_z3_Z3_mk_context" = xyes; then : + : +else + + as_fn_error $? "Unable to link against z3" "$LINENO" 5 + +fi + + + Z3_LDFLAGS="${Z3_LDFLAGS} -lz3" + { $as_echo "$as_me:${as_lineno-$LINENO}: Using Z3 solver backend" >&5 +$as_echo "$as_me: Using Z3 solver backend" >&6;} + CPPFLAGS="$old_CPPFLAGS" + +$as_echo "#define ENABLE_Z3 1" >>confdefs.h + +else + { $as_echo "$as_me:${as_lineno-$LINENO}: Not using Z3 solver backend" >&5 +$as_echo "$as_me: Not using Z3 solver backend" >&6;} +fi + + + + + + # Check whether --with-metasmt was given. @@ -5097,8 +5203,8 @@ fi -if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then - as_fn_error $? "At least one solver backend must be enabled, try using --with-stp or --with-metasmt" "$LINENO" 5 +if test "X$ENABLE_STP$ENABLE_Z3$ENABLE_METASMT" == X000 ; then + as_fn_error $? "At least one solver backend must be enabled, try using --with-stp, --with-z3 or --with-metasmt" "$LINENO" 5 fi diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 9d34e7b6..28eefcb6 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -12,6 +12,9 @@ /* Using STP Solver backend */ #undef ENABLE_STP +/* Using Z3 Solver backend */ +#undef ENABLE_Z3 + /* Does the platform use __ctype_b_loc, etc. */ #undef HAVE_CTYPE_EXTERNALS |