Teach the configure script to configure the build to use the Z3 SMT

solver using the new ``--with-z3=`` option.

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