diff options
Diffstat (limited to 'scripts/build/p-klee.inc')
| -rw-r--r-- | scripts/build/p-klee.inc | 198 |
1 files changed, 198 insertions, 0 deletions
diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc new file mode 100644 index 00000000..a9982fc0 --- /dev/null +++ b/scripts/build/p-klee.inc @@ -0,0 +1,198 @@ +validate_build_config_klee() { + return 0 +} + +setup_build_variables_klee() { + KLEE_SUFFIX="${LLVM_VERSION_SHORT}${SOLVER_SUFFIX}${SANITIZER_SUFFIX}" + KLEE_BUILD_DIR="${BASE}/klee_build${KLEE_SUFFIX}" + KLEE_SRC="$DIR/../../" +} + +download_klee() { + return 0 +} + +build_klee() { + CMAKE_PREFIX_PATH=("") + + local CMAKE_ARGUMENTS=( + -DLLVM_DIR="${LLVM_INSTALL}" + -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" + -DLLVMCC="${BITCODE_CC}" + -DLLVMCXX="${BITCODE_CXX}" + -DGTEST_SRC_DIR="${GTEST_INSTALL_PATH}" + -DENABLE_UNIT_TESTS="TRUE" + -DENABLE_SYSTEM_TESTS="TRUE" + -DLIT_ARGS="-v" + ) + + +############################################################################### +# klee-uclibc +############################################################################### + local KLEE_UCLIBC_CONFIGURE_OPTION + + if [ "${UCLIBC_VERSION}" != "0" ]; then + CMAKE_ARGUMENTS+=( + "-DENABLE_KLEE_UCLIBC=TRUE" + "-DKLEE_UCLIBC_PATH=${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" + "-DENABLE_POSIX_RUNTIME=TRUE" + ) + else + CMAKE_ARGUMENTS+=( + "-DENABLE_KLEE_UCLIBC=FALSE" + "-DENABLE_POSIX_RUNTIME=FALSE" + ) + fi + + + +############################################################################### +# Handle setting up solver configure flags for KLEE +############################################################################### + + local KLEE_Z3_CONFIGURE_OPTION=("-DENABLE_SOLVER_Z3=OFF") + local KLEE_STP_CONFIGURE_OPTION=("-DENABLE_SOLVER_STP=OFF") + local KLEE_METASMT_CONFIGURE_OPTION=("-DENABLE_SOLVER_METASMT=OFF") + + + for solver in "${SELECTED_SOLVERS[@]}"; do + echo "Setting CMake configuration option for ${solver}" + case "${solver}" in + stp) + KLEE_STP_CONFIGURE_OPTION=( + "-DENABLE_SOLVER_STP=TRUE" + "-DSTP_DIR=${STP_INSTALL_PATH}/" + ) + CMAKE_PREFIX_PATH+=("${STP_INSTALL_PATH}") + ;; + z3) + echo "Z3" + KLEE_Z3_CONFIGURE_OPTION=( + "-DENABLE_SOLVER_Z3=TRUE" + "-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include" + "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib/libz3.so" + ) + ;; + metasmt) + echo "metaSMT" + if [ "X${METASMT_DEFAULT}" == "X" ]; then + METASMT_DEFAULT=STP + fi + KLEE_METASMT_CONFIGURE_OPTION=( + -DENABLE_SOLVER_METASMT=TRUE + -DmetaSMT_DIR="${METASMT_BUILD_PATH}" + -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}" + ) + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac + done + + CMAKE_ARGUMENTS+=( + "${KLEE_Z3_CONFIGURE_OPTION[@]}" + "${KLEE_STP_CONFIGURE_OPTION[@]}" + "${KLEE_METASMT_CONFIGURE_OPTION[@]}" + ) + +############################################################################### +# Handle additional configure flags +############################################################################### + + if [[ $(to_bool "${USE_TCMALLOC}") -eq 1 ]] ; then + CMAKE_PREFIX_PATH+=("${TCMALLOC_INSTALL_PATH}") + CMAKE_ARGUMENTS+=("-DENABLE_TCMALLOC=TRUE") + else + CMAKE_ARGUMENTS+=("-DENABLE_TCMALLOC=FALSE") + fi + +############################################################################### +# KLEE +############################################################################### + + if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then + CMAKE_ARGUMENTS+=("-DENABLE_KLEE_ASSERTS=FALSE") + else + CMAKE_ARGUMENTS+=("-DENABLE_KLEE_ASSERTS=TRUE") + fi + + if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then + CMAKE_ARGUMENTS+=("-DCMAKE_BUILD_TYPE=RelWithDebInfo") + else + CMAKE_ARGUMENTS+=("-DCMAKE_BUILD_TYPE=Debug") + fi + +# TODO: We should support Ninja too +# Configure KLEE + + local CXX_FLAGS=("") + local C_FLAGS=("") + local LD_FLAGS=("") + + if [ "${COVERAGE}" -eq 1 ]; then + CXX_FLAGS+=("-fprofile-arcs" "-ftest-coverage") + C_FLAGS+=("-fprofile-arcs" "-ftest-coverage") + LD_FLAGS+=("-fprofile-arcs" "-ftest-coverage") + fi + + if [[ -n "${SANITIZER_BUILD}" ]]; then + C_FLAGS+=("${SANITIZER_C_FLAGS[@]}") + CXX_FLAGS+=("${SANITIZER_CXX_FLAGS[@]}") + LD_FLAGS+=("${SANITIZER_LD_FLAGS[@]}") + + CMAKE_ARGUMENTS+=( + "-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}" + "-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}" + ) + fi + + + + mkdir -p "${KLEE_BUILD_DIR}" || return 1 + cd "${KLEE_BUILD_DIR}" + + { + echo "CXXFLAGS=\"${CXX_FLAGS[*]}\" \\" + echo "CFLAGS=\"${C_FLAGS[*]}\" \\" + echo "LDFLAGS=\"${LD_FLAGS[*]}\" \\" + + if [[ -n "${CMAKE_PREFIX_PATH[*]}" ]]; then + cmake_concatenated=$(IFS=: ; echo "${CMAKE_PREFIX_PATH[*]}") + echo "CMAKE_PREFIX_PATH=\"${cmake_concatenated}\" \\" + fi + + echo "cmake ${CMAKE_ARGUMENTS[*]} \"${KLEE_SRC}\"" + } > "${KLEE_BUILD_DIR}/.build_command" + + source "${KLEE_BUILD_DIR}/.build_command" + make -j$(nproc) || make || return 1 +} + +install_klee() { + return 0 +} + +get_docker_config_id_klee() { + ( + setup_build_variables_klee + echo "${KLEE_SUFFIX}" + ) +} + +get_docker_context_klee() { + # KLEE's source code is two levels above this script + echo "${DIR}/../../" +} + +get_docker_container_context_klee() { + echo "${BASE}/klee_src/" +} + +get_build_artifacts_klee() { + ( + setup_build_variables_klee + echo "${KLEE_BUILD_DIR}" + ) +} \ No newline at end of file |