diff options
| -rw-r--r-- | autoconf/configure.ac | 9 | ||||
| -rwxr-xr-x | configure | 304 | ||||
| -rw-r--r-- | include/klee/Config/config.h.in | 3 | ||||
| -rwxr-xr-x | scripts/klee-chroot-env | 87 | ||||
| -rw-r--r-- | tools/klee-replay/Makefile | 2 | ||||
| -rw-r--r-- | tools/klee-replay/klee-replay.c | 139 |
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); } |