about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorLei Zhang <antiagainst@gmail.com>2013-09-15 14:11:20 -0400
committerLei Zhang <antiagainst@gmail.com>2013-12-08 09:21:26 -0500
commit67bfeaa6f6cd9f46a1d5131ab0b831913922eb3d (patch)
treec01c1b8d0b11a3f38c7a028abb7feb53fff2342d
parent0efeb6c1826238fd732be11a94cc3403d78be8cc (diff)
downloadklee-67bfeaa6f6cd9f46a1d5131ab0b831913922eb3d.tar.gz
Add chroot jail support in klee-replay.
-rw-r--r--autoconf/configure.ac9
-rwxr-xr-xconfigure304
-rw-r--r--include/klee/Config/config.h.in3
-rwxr-xr-xscripts/klee-chroot-env87
-rw-r--r--tools/klee-replay/Makefile2
-rw-r--r--tools/klee-replay/klee-replay.c139
6 files changed, 412 insertions, 132 deletions
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 6d846d5d..82574314 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -306,6 +306,15 @@ 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_ERROR([Library cap and its header file sys/capability.h required for \
+klee-replay. Please install package libcap-dev/libcap-devel.])
+fi
+
 AC_LANG_POP([C])
 
 AC_CHECK_HEADERS([selinux/selinux.h],
diff --git a/configure b/configure
index eb61b85b..19332245 100755
--- a/configure
+++ b/configure
@@ -1,13 +1,11 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.68 for KLEE 0.01.
+# Generated by GNU Autoconf 2.69 for KLEE 0.01.
 #
 # Report bugs to <daniel@minormatter.com>.
 #
 #
-# Copyright (C) 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001,
-# 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010 Free Software
-# Foundation, Inc.
+# Copyright (C) 1992-1996, 1998-2012 Free Software Foundation, Inc.
 #
 #
 # This configure script is free software; the Free Software Foundation
@@ -136,6 +134,31 @@ export LANGUAGE
 # CDPATH.
 (unset CDPATH) >/dev/null 2>&1 && unset CDPATH
 
+# Use a proper internal environment variable to ensure we don't fall
+  # into an infinite loop, continuously re-executing ourselves.
+  if test x"${_as_can_reexec}" != xno && test "x$CONFIG_SHELL" != x; then
+    _as_can_reexec=no; export _as_can_reexec;
+    # We cannot yet assume a decent shell, so we have to provide a
+# neutralization value for shells without unset; and this also
+# works around shells that cannot unset nonexistent variables.
+# Preserve -v and -x to the replacement shell.
+BASH_ENV=/dev/null
+ENV=/dev/null
+(unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV
+case $- in # ((((
+  *v*x* | *x*v* ) as_opts=-vx ;;
+  *v* ) as_opts=-v ;;
+  *x* ) as_opts=-x ;;
+  * ) as_opts= ;;
+esac
+exec $CONFIG_SHELL $as_opts "$as_myself" ${1+"$@"}
+# Admittedly, this is quite paranoid, since all the known shells bail
+# out after a failed `exec'.
+$as_echo "$0: could not re-execute with $CONFIG_SHELL" >&2
+as_fn_exit 255
+  fi
+  # We don't want this to propagate to other subprocesses.
+          { _as_can_reexec=; unset _as_can_reexec;}
 if test "x$CONFIG_SHELL" = x; then
   as_bourne_compatible="if test -n \"\${ZSH_VERSION+set}\" && (emulate sh) >/dev/null 2>&1; then :
   emulate sh
@@ -169,7 +192,8 @@ if ( set x; as_fn_ret_success y && test x = \"\$1\" ); then :
 else
   exitcode=1; echo positional parameters were not saved.
 fi
-test x\$exitcode = x0 || exit 1"
+test x\$exitcode = x0 || exit 1
+test -x / || exit 1"
   as_suggested="  as_lineno_1=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_1a=\$LINENO
   as_lineno_2=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_2a=\$LINENO
   eval 'test \"x\$as_lineno_1'\$as_run'\" != \"x\$as_lineno_2'\$as_run'\" &&
@@ -214,21 +238,25 @@ IFS=$as_save_IFS
 
 
       if test "x$CONFIG_SHELL" != x; then :
-  # We cannot yet assume a decent shell, so we have to provide a
-	# neutralization value for shells without unset; and this also
-	# works around shells that cannot unset nonexistent variables.
-	# Preserve -v and -x to the replacement shell.
-	BASH_ENV=/dev/null
-	ENV=/dev/null
-	(unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV
-	export CONFIG_SHELL
-	case $- in # ((((
-	  *v*x* | *x*v* ) as_opts=-vx ;;
-	  *v* ) as_opts=-v ;;
-	  *x* ) as_opts=-x ;;
-	  * ) as_opts= ;;
-	esac
-	exec "$CONFIG_SHELL" $as_opts "$as_myself" ${1+"$@"}
+  export CONFIG_SHELL
+             # We cannot yet assume a decent shell, so we have to provide a
+# neutralization value for shells without unset; and this also
+# works around shells that cannot unset nonexistent variables.
+# Preserve -v and -x to the replacement shell.
+BASH_ENV=/dev/null
+ENV=/dev/null
+(unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV
+case $- in # ((((
+  *v*x* | *x*v* ) as_opts=-vx ;;
+  *v* ) as_opts=-v ;;
+  *x* ) as_opts=-x ;;
+  * ) as_opts= ;;
+esac
+exec $CONFIG_SHELL $as_opts "$as_myself" ${1+"$@"}
+# Admittedly, this is quite paranoid, since all the known shells bail
+# out after a failed `exec'.
+$as_echo "$0: could not re-execute with $CONFIG_SHELL" >&2
+exit 255
 fi
 
     if test x$as_have_required = xno; then :
@@ -331,6 +359,14 @@ $as_echo X"$as_dir" |
 
 
 } # as_fn_mkdir_p
+
+# as_fn_executable_p FILE
+# -----------------------
+# Test if FILE is an executable regular file.
+as_fn_executable_p ()
+{
+  test -f "$1" && test -x "$1"
+} # as_fn_executable_p
 # as_fn_append VAR VALUE
 # ----------------------
 # Append the text in VALUE to the end of the definition contained in VAR. Take
@@ -452,6 +488,10 @@ as_cr_alnum=$as_cr_Letters$as_cr_digits
   chmod +x "$as_me.lineno" ||
     { $as_echo "$as_me: error: cannot create $as_me.lineno; rerun with a POSIX shell" >&2; as_fn_exit 1; }
 
+  # If we had to re-execute with $CONFIG_SHELL, we're ensured to have
+  # already done that, so ensure we don't try to do so again and fall
+  # in an infinite loop.  This has already happened in practice.
+  _as_can_reexec=no; export _as_can_reexec
   # Don't try to exec as it changes $[0], causing all sort of problems
   # (the dirname of $[0] is not the place where we might find the
   # original and so on.  Autoconf is especially sensitive to this).
@@ -486,16 +526,16 @@ if (echo >conf$$.file) 2>/dev/null; then
     # ... but there are two gotchas:
     # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail.
     # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable.
-    # In both cases, we have to default to `cp -p'.
+    # In both cases, we have to default to `cp -pR'.
     ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe ||
-      as_ln_s='cp -p'
+      as_ln_s='cp -pR'
   elif ln conf$$.file conf$$ 2>/dev/null; then
     as_ln_s=ln
   else
-    as_ln_s='cp -p'
+    as_ln_s='cp -pR'
   fi
 else
-  as_ln_s='cp -p'
+  as_ln_s='cp -pR'
 fi
 rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file
 rmdir conf$$.dir 2>/dev/null
@@ -507,28 +547,8 @@ else
   as_mkdir_p=false
 fi
 
-if test -x / >/dev/null 2>&1; then
-  as_test_x='test -x'
-else
-  if ls -dL / >/dev/null 2>&1; then
-    as_ls_L_option=L
-  else
-    as_ls_L_option=
-  fi
-  as_test_x='
-    eval sh -c '\''
-      if test -d "$1"; then
-	test -d "$1/.";
-      else
-	case $1 in #(
-	-*)set "./$1";;
-	esac;
-	case `ls -ld'$as_ls_L_option' "$1" 2>/dev/null` in #((
-	???[sx]*):;;*)false;;esac;fi
-    '\'' sh
-  '
-fi
-as_executable_p=$as_test_x
+as_test_x='test -x'
+as_executable_p=as_fn_executable_p
 
 # Sed expression to map a string onto a valid CPP name.
 as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'"
@@ -1164,8 +1184,6 @@ target=$target_alias
 if test "x$host_alias" != x; then
   if test "x$build_alias" = x; then
     cross_compiling=maybe
-    $as_echo "$as_me: WARNING: if you wanted to set the --build type, don't use --host.
-    If a cross compiler is detected then cross compile mode will be used" >&2
   elif test "x$build_alias" != "x$host_alias"; then
     cross_compiling=yes
   fi
@@ -1420,9 +1438,9 @@ test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
 KLEE configure 0.01
-generated by GNU Autoconf 2.68
+generated by GNU Autoconf 2.69
 
-Copyright (C) 2010 Free Software Foundation, Inc.
+Copyright (C) 2012 Free Software Foundation, Inc.
 This configure script is free software; the Free Software Foundation
 gives unlimited permission to copy, distribute and modify it.
 _ACEOF
@@ -1672,6 +1690,52 @@ $as_echo "$ac_res" >&6; }
 
 } # ac_fn_c_check_header_compile
 
+# ac_fn_c_try_link LINENO
+# -----------------------
+# Try to link conftest.$ac_ext, and return whether this succeeded.
+ac_fn_c_try_link ()
+{
+  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"
+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
+  ac_status=$?
+  if test -s conftest.err; then
+    grep -v '^ *+' conftest.err >conftest.er1
+    cat conftest.er1 >&5
+    mv -f conftest.er1 conftest.err
+  fi
+  $as_echo "$as_me:${as_lineno-$LINENO}: \$? = $ac_status" >&5
+  test $ac_status = 0; } && {
+	 test -z "$ac_c_werror_flag" ||
+	 test ! -s conftest.err
+       } && 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
+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_link
+
 # ac_fn_cxx_try_compile LINENO
 # ----------------------------
 # Try to compile conftest.$ac_ext, and return whether this succeeded.
@@ -1865,7 +1929,7 @@ $as_echo "$ac_try_echo"; } >&5
 	 test ! -s conftest.err
        } && test -s conftest$ac_exeext && {
 	 test "$cross_compiling" = yes ||
-	 $as_test_x conftest$ac_exeext
+	 test -x conftest$ac_exeext
        }; then :
   ac_retval=0
 else
@@ -1888,7 +1952,7 @@ This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
 It was created by KLEE $as_me 0.01, which was
-generated by GNU Autoconf 2.68.  Invocation command line was
+generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
 
@@ -2779,7 +2843,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -2819,7 +2883,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -2872,7 +2936,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -2913,7 +2977,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -2971,7 +3035,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -3015,7 +3079,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -3461,8 +3525,7 @@ cat confdefs.h - <<_ACEOF >conftest.$ac_ext
 /* end confdefs.h.  */
 #include <stdarg.h>
 #include <stdio.h>
-#include <sys/types.h>
-#include <sys/stat.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);
@@ -3702,7 +3765,7 @@ do
     for ac_prog in grep ggrep; do
     for ac_exec_ext in '' $ac_executable_extensions; do
       ac_path_GREP="$as_dir/$ac_prog$ac_exec_ext"
-      { test -f "$ac_path_GREP" && $as_test_x "$ac_path_GREP"; } || continue
+      as_fn_executable_p "$ac_path_GREP" || continue
 # Check for GNU ac_path_GREP and select it if it is found.
   # Check for GNU $ac_path_GREP
 case `"$ac_path_GREP" --version 2>&1` in
@@ -3768,7 +3831,7 @@ do
     for ac_prog in egrep; do
     for ac_exec_ext in '' $ac_executable_extensions; do
       ac_path_EGREP="$as_dir/$ac_prog$ac_exec_ext"
-      { test -f "$ac_path_EGREP" && $as_test_x "$ac_path_EGREP"; } || continue
+      as_fn_executable_p "$ac_path_EGREP" || continue
 # Check for GNU ac_path_EGREP and select it if it is found.
   # Check for GNU $ac_path_EGREP
 case `"$ac_path_EGREP" --version 2>&1` in
@@ -3958,6 +4021,69 @@ fi
 done
 
 
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for cap_get_proc in -lcap" >&5
+$as_echo_n "checking for cap_get_proc in -lcap... " >&6; }
+if ${ac_cv_lib_cap_cap_get_proc+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lcap  $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 cap_get_proc ();
+int
+main ()
+{
+return cap_get_proc ();
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_c_try_link "$LINENO"; then :
+  ac_cv_lib_cap_cap_get_proc=yes
+else
+  ac_cv_lib_cap_cap_get_proc=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_cap_cap_get_proc" >&5
+$as_echo "$ac_cv_lib_cap_cap_get_proc" >&6; }
+if test "x$ac_cv_lib_cap_cap_get_proc" = xyes; then :
+  have_cap=yes
+else
+  have_cap=no
+fi
+
+if test "x${have_cap}" = xyes; then
+  for ac_header in sys/capability.h
+do :
+  ac_fn_c_check_header_mongrel "$LINENO" "sys/capability.h" "ac_cv_header_sys_capability_h" "$ac_includes_default"
+if test "x$ac_cv_header_sys_capability_h" = xyes; then :
+  cat >>confdefs.h <<_ACEOF
+#define HAVE_SYS_CAPABILITY_H 1
+_ACEOF
+
+else
+  have_cap=no
+fi
+
+done
+
+fi
+if test "x${have_cap}" = xno; then
+  as_fn_error $? "Library cap and its header file sys/capability.h required for \
+klee-replay. Please install package libcap-dev/libcap-devel." "$LINENO" 5
+fi
+
 ac_ext=cpp
 ac_cpp='$CXXCPP $CPPFLAGS'
 ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
@@ -3993,7 +4119,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -4037,7 +4163,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  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
@@ -4482,7 +4608,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
     ac_cv_path_RUNTEST="$as_dir/$ac_word$ac_exec_ext"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -4938,16 +5064,16 @@ if (echo >conf$$.file) 2>/dev/null; then
     # ... but there are two gotchas:
     # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail.
     # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable.
-    # In both cases, we have to default to `cp -p'.
+    # In both cases, we have to default to `cp -pR'.
     ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe ||
-      as_ln_s='cp -p'
+      as_ln_s='cp -pR'
   elif ln conf$$.file conf$$ 2>/dev/null; then
     as_ln_s=ln
   else
-    as_ln_s='cp -p'
+    as_ln_s='cp -pR'
   fi
 else
-  as_ln_s='cp -p'
+  as_ln_s='cp -pR'
 fi
 rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file
 rmdir conf$$.dir 2>/dev/null
@@ -5007,28 +5133,16 @@ else
   as_mkdir_p=false
 fi
 
-if test -x / >/dev/null 2>&1; then
-  as_test_x='test -x'
-else
-  if ls -dL / >/dev/null 2>&1; then
-    as_ls_L_option=L
-  else
-    as_ls_L_option=
-  fi
-  as_test_x='
-    eval sh -c '\''
-      if test -d "$1"; then
-	test -d "$1/.";
-      else
-	case $1 in #(
-	-*)set "./$1";;
-	esac;
-	case `ls -ld'$as_ls_L_option' "$1" 2>/dev/null` in #((
-	???[sx]*):;;*)false;;esac;fi
-    '\'' sh
-  '
-fi
-as_executable_p=$as_test_x
+
+# as_fn_executable_p FILE
+# -----------------------
+# Test if FILE is an executable regular file.
+as_fn_executable_p ()
+{
+  test -f "$1" && test -x "$1"
+} # as_fn_executable_p
+as_test_x='test -x'
+as_executable_p=as_fn_executable_p
 
 # Sed expression to map a string onto a valid CPP name.
 as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'"
@@ -5050,7 +5164,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # values after options handling.
 ac_log="
 This file was extended by KLEE $as_me 0.01, which was
-generated by GNU Autoconf 2.68.  Invocation command line was
+generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
   CONFIG_HEADERS  = $CONFIG_HEADERS
@@ -5116,10 +5230,10 @@ cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
 KLEE config.status 0.01
-configured by $0, generated by GNU Autoconf 2.68,
+configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 
-Copyright (C) 2010 Free Software Foundation, Inc.
+Copyright (C) 2012 Free Software Foundation, Inc.
 This config.status script is free software; the Free Software Foundation
 gives unlimited permission to copy, distribute and modify it."
 
@@ -5207,7 +5321,7 @@ fi
 _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 if \$ac_cs_recheck; then
-  set X '$SHELL' '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion
+  set X $SHELL '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion
   shift
   \$as_echo "running CONFIG_SHELL=$SHELL \$*" >&6
   CONFIG_SHELL='$SHELL'
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 4ce9714d..0f79e01d 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -33,6 +33,9 @@
 /* Define to 1 if you have the <sys/acl.h> header file. */
 #undef HAVE_SYS_ACL_H
 
+/* Define to 1 if you have the <sys/capability.h> header file. */
+#undef HAVE_SYS_CAPABILITY_H
+
 /* Define to 1 if you have the <sys/stat.h> header file. */
 #undef HAVE_SYS_STAT_H
 
diff --git a/scripts/klee-chroot-env b/scripts/klee-chroot-env
new file mode 100755
index 00000000..3b524d8e
--- /dev/null
+++ b/scripts/klee-chroot-env
@@ -0,0 +1,87 @@
+#!/usr/bin/env python2
+#-*- coding: utf-8 -*-
+#
+# Buiding chroot environment for the program under test.
+#
+# This script uses `ldd' to get the shared libraries required by a program,
+# and copies those libraries to the directory for chroot'ing, maintaining
+# each library's relative path against root directory.
+#
+# Usage example:
+# $ ./klee-chroot-env /tmp/sandbox `which rm` # build env for 'rm'
+# $ cp `which rm` /tm/sandbox/rm              # copy the binary into the jail
+# $ sudo setcap SYS_CAP_CHROOT+ep `which klee-replay`
+#              # give klee-replay the capability to call 'chroot' system call
+# $ klee-replay --chroot-to-dir=/tmp/sandbox /tmp/sandbox/rm /path/to/ktest
+#              # replay some ktest in chroot jail rooted at /tmp/sandbox
+
+import sys
+import os
+import shutil
+import re
+
+from subprocess import Popen, PIPE
+
+
+def get_shared_library_dependency(program):
+    """Calls `ldd' to get the shared library dependency of a `program'."""
+
+    cmd = "ldd %s" % program
+    prog = Popen(cmd.split(), stdout=PIPE, stderr=PIPE, shell=False)
+    out, err = prog.communicate(None)
+    prog.stdout.close()
+    prog.stderr.close()
+
+    regexp = re.compile(r"\s*\(\S+\)\s*")
+
+    dep = out.splitlines()
+    dep = [e.strip() for e in dep]
+    dep = [regexp.sub("", e) for e in dep]
+    dep = [e for e in dep if not e.startswith("linux-vdso.so")]
+    libs = []
+    for e in dep:
+        if (" => " in e):
+            libs.append(e.split(" => "))
+        else:
+            libs.append((os.path.basename(e), e))
+
+    # Outputs a list of (link-name, original-path) pairs.
+    return libs
+
+
+def build_environment(root, libs):
+    """Copies all library dependencies to the specified `root' dir."""
+
+    if not os.path.exists(root):
+        os.makedirs(root)
+    os.chdir(root)
+
+    for e in libs:
+        link_name = e[0]
+        original_path = e[1]
+        relative_dir = os.path.dirname(e[1]).lstrip("/")
+        chrooted_path = root + os.path.dirname(e[1]) + "/" + link_name
+        if not os.path.exists(relative_dir):
+            os.makedirs(relative_dir)
+        shutil.copyfile(original_path, chrooted_path)
+        shutil.copymode(original_path, chrooted_path)
+
+
+def usage():
+    print("Usage: %s /path/to/root/dir /path/to/program" % sys.argv[0])
+
+
+if __name__ == "__main__":
+    if (len(sys.argv) != 3):
+        usage()
+        exit(1)
+
+    rootdir = sys.argv[1]
+    program = sys.argv[2]
+
+    if not os.path.isfile(program) or not os.access(program, os.X_OK):
+        print("Error: executable not existing or not executable")
+        exit(1)
+
+    libs = get_shared_library_dependency(program)
+    build_environment(rootdir, libs)
diff --git a/tools/klee-replay/Makefile b/tools/klee-replay/Makefile
index fcce0483..e97fc7ff 100644
--- a/tools/klee-replay/Makefile
+++ b/tools/klee-replay/Makefile
@@ -16,4 +16,4 @@ NO_PEDANTIC=1
 
 include $(LEVEL)/Makefile.common
 
-LIBS += -lutil
+LIBS += -lutil -lcap
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 8d0ba8cc..0ea88fb1 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -16,12 +16,14 @@
 #include <stdlib.h>
 #include <string.h>
 #include <stdint.h>
+#include <getopt.h>
 
 #include <errno.h>
 #include <time.h>
 #include <unistd.h>
 #include <sys/signal.h>
 #include <sys/wait.h>
+#include <sys/capability.h>
 
 static void __emit_error(const char *msg);
 
@@ -32,6 +34,14 @@ static const char *progname = 0;
 static unsigned monitored_pid = 0;    
 static unsigned monitored_timeout;
 
+static char *rootdir = NULL;
+static struct option long_options[] = {
+  {"create-files-only", required_argument, 0, 'f'},
+  {"chroot-to-dir", required_argument, 0, 'r'},
+  {"help", no_argument, 0, 'h'},
+  {0, 0, 0, 0},
+};
+
 static void stop_monitored(int process) {
   fprintf(stderr, "TIMEOUT: ATTEMPTING GDB EXIT\n");
   int pid = fork();
@@ -105,9 +115,7 @@ static void timeout_handler(int signal) {
   }
 }
 
-void process_status(int status,
-		    time_t elapsed, 
-		    const char *pfx) {
+void process_status(int status, time_t elapsed, const char *pfx) {
   fprintf(stderr, "%s: ", progname);
   if (pfx)
     fprintf(stderr, "%s: ", pfx);
@@ -132,6 +140,13 @@ void process_status(int status,
   }
 }
 
+/* This function assumes that executable is a path pointing to some existing
+ * binary and rootdir is a path pointing to some directory.
+ */
+static inline char *strip_root_dir(char *executable, char *rootdir) {
+  return executable + strlen(rootdir);
+}
+
 static void run_monitored(char *executable, int argc, char **argv) {
   int pid;
   const char *t = getenv("KLEE_REPLAY_TIMEOUT");  
@@ -162,8 +177,22 @@ static void run_monitored(char *executable, int argc, char **argv) {
      */
     setpgrp();
 
-    execv(executable, argv);
-    perror("execv");
+    if (!rootdir) {
+      execv(executable, argv);
+      perror("execv");
+      _exit(66);
+    }
+
+    fprintf(stderr, "rootdir: %s\n", rootdir);
+    const char *msg;
+    if ((msg = "chdir", chdir(rootdir) == 0) &&
+      (msg = "chroot", chroot(rootdir) == 0)) {
+      msg = "execv";
+      executable = strip_root_dir(executable, rootdir);
+      argv[0] = strip_root_dir(argv[0], rootdir);
+      execv(executable, argv);
+    }
+    perror(msg);
     _exit(66);
   } else {
     /* Parent process which monitors the child. */
@@ -192,11 +221,31 @@ static void run_monitored(char *executable, int argc, char **argv) {
   }
 }
 
+/* ensure this process has CAP_SYS_CHROOT capability. */
+void ensure_capsyschroot(const char *executable) {
+  cap_t caps = cap_get_proc();  // all current capabilities.
+  cap_flag_value_t chroot_permitted, chroot_effective;
+
+  if (!caps)
+    perror("cap_get_proc");
+  /* effective and permitted flags should be set for CAP_SYS_CHROOT. */
+  cap_get_flag(caps, CAP_SYS_CHROOT, CAP_PERMITTED, &chroot_permitted);
+  cap_get_flag(caps, CAP_SYS_CHROOT, CAP_EFFECTIVE, &chroot_effective);
+  if (chroot_permitted != CAP_SET || chroot_effective != CAP_SET) {
+    fprintf(stderr, "Error: chroot: No CAP_SYS_CHROOT capability.\n");
+    exit(1);
+  }
+  cap_free(caps);
+}
+
 static void usage(void) {
-  fprintf(stderr, "Usage: %s <executable> { <ktest-files> }\n", progname);
+  fprintf(stderr, "Usage: %s [option]... <executable> <ktest-file>...\n", progname);
   fprintf(stderr, "   or: %s --create-files-only <ktest-file>\n", progname);
   fprintf(stderr, "\n");
-  fprintf(stderr, "Set KLEE_REPLAY_TIMEOUT environment variable to set a timeout (in seconds).\n");
+  fprintf(stderr, "-r, --chroot-to-dir=DIR  use chroot jail, requires CAP_SYS_CHROOT\n");
+  fprintf(stderr, "-h, --help               display this help and exit\n");
+  fprintf(stderr, "\n");
+  fprintf(stderr, "Use KLEE_REPLAY_TIMEOUT environment variable to set a timeout (in seconds).\n");
   exit(1);
 }
 
@@ -209,35 +258,53 @@ int main(int argc, char** argv) {
   if (argc < 3)
     usage();
 
-  /* Special case hack for only creating files and not actually executing the
-   * program.
-   */
-  if (strcmp(argv[1], "--create-files-only") == 0) {
-    if (argc != 3)
-      usage();
-
-    char* input_fname = argv[2];
-
-    input = kTest_fromFile(input_fname);
-    if (!input) {
-      fprintf(stderr, "%s: error: input file %s not valid.\n", progname,
-              input_fname);
-      exit(1);
-    }
+  int c, opt_index;
+  while ((c = getopt_long(argc, argv, "f:r:", long_options, &opt_index)) != -1) {
+    switch (c) {
+      case 'f': {
+        /* Special case hack for only creating files and not actually executing
+        * the program.
+         */
+        if (argc != 3)
+          usage();
     
-    prg_argc = input->numArgs;
-    prg_argv = input->args;
-    prg_argv[0] = argv[1];
-    klee_init_env(&prg_argc, &prg_argv);
+        char* input_fname = optarg;
     
-    replay_create_files(&__exe_fs);
-    return 0;
+        input = kTest_fromFile(input_fname);
+        if (!input) {
+          fprintf(stderr, "%s: error: input file %s not valid.\n", progname,
+                  input_fname);
+          exit(1);
+        }
+
+        prg_argc = input->numArgs;
+        prg_argv = input->args;
+        prg_argv[0] = argv[1];
+        klee_init_env(&prg_argc, &prg_argv);
+
+        replay_create_files(&__exe_fs);
+        return 0;
+      }
+      case 'r':
+        rootdir = optarg;
+        break;
+    }
   }
 
   /* Normal execution path ... */
 
-  char* executable = argv[1];
+  char* executable = argv[optind];
+
+  /* make sure this process has the CAP_SYS_CHROOT capability. */
+  if (rootdir)
+    ensure_capsyschroot(progname);
   
+  /* rootdir should be a prefix of executable's path. */
+  if (rootdir && strstr(executable, rootdir) != executable) {
+    fprintf(stderr, "Error: chroot: root dir should be a parent dir of executable.\n");
+    exit(1);
+  }
+
   /* Verify the executable exists. */
   FILE *f = fopen(executable, "r");
   if (!f) {
@@ -247,7 +314,7 @@ int main(int argc, char** argv) {
   fclose(f);
 
   int idx = 0;
-  for (idx = 2; idx != argc; ++idx) {
+  for (idx = optind + 1; idx != argc; ++idx) {
     char* input_fname = argv[idx];
     unsigned i;
     
@@ -261,7 +328,7 @@ int main(int argc, char** argv) {
     obj_index = 0;
     prg_argc = input->numArgs;
     prg_argv = input->args;
-    prg_argv[0] = argv[1];
+    prg_argv[0] = argv[optind];
     klee_init_env(&prg_argc, &prg_argv);
 
     if (idx > 2)
@@ -361,9 +428,9 @@ void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
       *((int*) addr) = 0;
     } else {
       if (boo->numBytes != nbytes) {
-	fprintf(stderr, "make_symbolic mismatch, different sizes: "
-		"%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes);
-	exit(1);
+        fprintf(stderr, "make_symbolic mismatch, different sizes: "
+           "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes);
+        exit(1);
       } else {
         memcpy(addr, boo->bytes, nbytes);
         obj_index++;
@@ -388,7 +455,7 @@ int klee_range(int start, int end, const char* name) {
 
     if (r < start || r >= end) {
       fprintf(stderr, "klee_range(%d, %d, %s) returned invalid result: %d\n", 
-	      start, end, name, r);
+        start, end, name, r);
       exit(1);
     }
     
@@ -397,7 +464,7 @@ int klee_range(int start, int end, const char* name) {
 }
 
 void klee_report_error(const char *file, int line, 
-		       const char *message, const char *suffix) {
+                       const char *message, const char *suffix) {
   __emit_error(message);
 }