diff options
Diffstat (limited to 'scripts')
62 files changed, 2786 insertions, 1309 deletions
diff --git a/scripts/build/Dockerfile_base b/scripts/build/Dockerfile_base deleted file mode 100644 index 8daee330..00000000 --- a/scripts/build/Dockerfile_base +++ /dev/null @@ -1,15 +0,0 @@ -# Build dependencies for LLVM -FROM ubuntu:16.04 -LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" - -ENV DOCKER_BUILD=1 - -# Define all variables that can be changed as argument to docker build -ARG BASE=/tmp - -# Copy across all source files -ADD /scripts/build/* scripts/build/ - -# Install packages -RUN scripts/build/dependencies-ubuntu.sh && rm -rf /var/lib/apt/lists/* -WORKDIR $BASE diff --git a/scripts/build/Dockerfile_klee b/scripts/build/Dockerfile_klee deleted file mode 100644 index 1872fca6..00000000 --- a/scripts/build/Dockerfile_klee +++ /dev/null @@ -1,58 +0,0 @@ -# Build the final KLEE layer -ARG REPOSITORY -ARG LLVM_VERSION_SHORT -ARG LLVM_SUFFIX -ARG SOLVER_SUFFIX -ARG DEPS_SUFFIX -FROM ${REPOSITORY}/klee_deps:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} -LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" - -# Define all variables that can be changed as argument to the docker build -ARG BASE=/tmp -ARG COVERAGE=0 -ARG DEPS_SUFFIX -ARG DISABLE_ASSERTIONS -ARG ENABLE_OPTIMIZED -ARG ENABLE_DEBUG -ARG KLEE_TRAVIS_BUILD -ARG KLEE_UCLIBC -ARG LLVM_VERSION -ARG LLVM_SUFFIX -ARG METASMT_BOOST_VERSION -ARG METASMT_DEFAULT -ARG METASMT_VERSION -ARG REQUIRES_RTTI -ARG SANITIZER_BUILD -ARG SANITIZER_SUFFIX -ARG SOLVER_SUFFIX -ARG SOLVERS -ARG STP_VERSION -ARG TRAVIS_OS_NAME -ARG USE_TCMALLOC -ARG Z3_VERSION - -ENV DOCKER_BUILD=1 - -# Copy across source files needed for build -ADD / ${BASE}/klee_src - -# TODO Remove when STP is fixed -RUN export LD_LIBRARY_PATH=${BASE}/metaSMT/deps/stp-git-basic/lib/ && export KLEE_SRC=${BASE}/klee_src && ${BASE}/klee_src/scripts/build/klee.sh && rm -rf ${BASE}/klee_src/.git && ln -s ${BASE}/klee_build* ${BASE}/klee_build - -# Create ``klee`` user for container with password ``klee``. -# and give it password-less sudo access (temporarily so we can use the TravisCI scripts) -RUN useradd -m klee && \ - echo klee:klee | chpasswd && \ - cp /etc/sudoers /etc/sudoers.bak && \ - echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers - -# Set klee user to be owner -RUN chown --recursive klee: ${BASE}/klee_src - -USER klee -WORKDIR /home/klee - -# Add KLEE binary directory to PATH -RUN /bin/bash -c 'DIR="${BASE}/klee_src/scripts/build" source ${BASE}/klee_src/scripts/build/common-defaults.sh && ln -s ${BASE}/klee_src /home/klee/ && ln -s ${BASE}/klee_build /home/klee/ && echo "export PATH=\"$PATH:${LLVM_BIN}:/home/klee/klee_build/bin\"" >> /home/klee/.bashrc' -# TODO Remove when STP is fixed -RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=${BASE}/metaSMT/deps/stp-git-basic/lib/" >> /home/klee/.bashrc' diff --git a/scripts/build/Dockerfile_klee_deps b/scripts/build/Dockerfile_klee_deps deleted file mode 100644 index 582d324f..00000000 --- a/scripts/build/Dockerfile_klee_deps +++ /dev/null @@ -1,33 +0,0 @@ -# Build KLEE dependencies except LLVM and solvers -ARG REPOSITORY -ARG LLVM_VERSION_SHORT -ARG LLVM_SUFFIX -ARG SOLVER_SUFFIX -FROM ${REPOSITORY}/solver:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX} -LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" - -# Define all variables that can be changed as argument to the docker build -ARG BASE=/tmp -ARG DISABLE_ASSERTIONS -ARG ENABLE_OPTIMIZED -ARG ENABLE_DEBUG -ARG KEEP_BUILD -ARG KEEP_SRC -ARG KLEE_TRAVIS_BUILD -ARG KLEE_UCLIBC -ARG LLVM_VERSION -ARG LLVM_SUFFIX -ARG REQUIRES_RTTI -ARG SANITIZER_BUILD -ARG TRAVIS_OS_NAME -ARG USE_TCMALLOC - -ENV DOCKER_BUILD=1 - -# Copy across source files needed for build -ADD /scripts/build/* scripts/build/ - -# Build KLEE (use TravisCI script) -RUN ${BASE}/scripts/build/testing-utils.sh -RUN ${BASE}/scripts/build/tcmalloc.sh -RUN ${BASE}/scripts/build/uclibc.sh diff --git a/scripts/build/Dockerfile_llvm_build b/scripts/build/Dockerfile_llvm_build deleted file mode 100644 index 548f0d8a..00000000 --- a/scripts/build/Dockerfile_llvm_build +++ /dev/null @@ -1,27 +0,0 @@ -# Build LLVM -ARG LLVM_VERSION_SHORT -ARG REPOSITORY -FROM ${REPOSITORY}/base -LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" - -ENV DOCKER_BUILD=1 - -# Define all variables that can be changed as argument to the docker build -ARG BASE=/tmp -ARG DISABLE_ASSERTIONS -ARG ENABLE_OPTIMIZED -ARG ENABLE_DEBUG -ARG KEEP_BUILD -ARG KEEP_SRC -ARG KLEE_TRAVIS_BUILD -ARG LLVM_VERSION -ARG PACKAGED -ARG REQUIRES_RTTI -ARG SANITIZER_BUILD -ARG TRAVIS_OS_NAME - -WORKDIR $BASE - -# Copy across source files needed for build -ADD /scripts/build/* scripts/build/ -RUN ./scripts/build/llvm.sh diff --git a/scripts/build/Dockerfile_solver_build b/scripts/build/Dockerfile_solver_build deleted file mode 100644 index ba2af62a..00000000 --- a/scripts/build/Dockerfile_solver_build +++ /dev/null @@ -1,33 +0,0 @@ -ARG REPOSITORY -ARG LLVM_SUFFIX -ARG LLVM_VERSION_SHORT -FROM ${REPOSITORY}/llvm_built:${LLVM_VERSION_SHORT}${LLVM_SUFFIX} -LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>" - -ENV DOCKER_BUILD=1 - -# Define all variables that can be changed as argument to docker build -ARG BASE=/tmp -ARG DISABLE_ASSERTIONS -ARG ENABLE_OPTIMIZED -ARG ENABLE_DEBUG -ARG KEEP_BUILD -ARG KEEP_SRC -ARG KLEE_TRAVIS_BUILD -ARG LLVM_VERSION -ARG METASMT_BOOST_VERSION -ARG METASMT_DEFAULT -ARG METASMT_VERSION -ARG REQUIRES_RTTI -ARG SOLVERS -ARG SANITIZER_BUILD -ARG STP_VERSION -ARG STORAGE_SPACE_OPTIMIZED=1 -ARG TRAVIS_OS_NAME -ARG Z3_VERSION - -WORKDIR $BASE - -# Copy across source files needed for build -ADD /scripts/build/* scripts/build/ -RUN scripts/build/solvers.sh diff --git a/scripts/build/build-docker.sh b/scripts/build/build-docker.sh deleted file mode 100755 index 3a031d22..00000000 --- a/scripts/build/build-docker.sh +++ /dev/null @@ -1,100 +0,0 @@ -#!/bin/bash -# Build a KLEE docker image. If needed, build all dependent layers as well. -set -e - -# We are going to build docker containers -export DOCKER_BUILD=1 - -# All scripts are located relative to this one -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" -KLEEDIR="${DIR}/../.." - -############################################################################### -# Setup Docker variables needed to build layers layers -############################################################################### - -add_arg_variable() { - name=$1 - name_var=${!name} - if [[ (-z "$name_var") || ($name_var == "") ]] ; then - val="" - else - val="--build-arg ${name}=${name_var} " - fi - echo "$val" -} - -DOCKER_OPTS=() -for v in \ - LLVM_VERSION \ - LLVM_VERSION_SHORT \ - ENABLE_OPTIMIZED \ - DISABLE_ASSERTIONS \ - ENABLE_DEBUG \ - REQUIRES_RTTI \ - LLVM_SUFFIX \ - REPOSITORY \ - SANITIZER_BUILD \ - SANITIZER_SUFFIX \ - PACKAGED \ - KLEE_TRAVIS_BUILD \ - TRAVIS_OS_NAME \ - METASMT_VERSION \ - METASMT_DEFAULT \ - METASMT_BOOST_VERSION \ - SOLVER_SUFFIX \ - Z3_VERSION \ - STP_VERSION \ - KLEE_UCLIBC \ - DEPS_SUFFIX \ - USE_TCMALLOC \ - COVERAGE \ - KEEP_SRC \ - KEEP_BUILD \ - TCMALLOC_VERSION \ - GTEST_VERSION \ - SOLVERS \ - ; do - DOCKER_OPTS+=($(add_arg_variable $v)) -done - -echo "DOCKER_OPTS: ${DOCKER_OPTS[@]}" -docker_build_and_push() { - merge=$1 - image=$2 - script=$3 - set +e - # Get or build layer - echo "$image" - if ! docker pull $image ; then - set -e - # Update if needed - echo "BUILD IMAGE" - merge_arg="" - # if [[ "${merge}x" == "1x" ]]; then - # #merge_arg="--squash" - # fi - docker build ${merge_arg} -f "${DIR}/$script" ${@:4} -t "$image" "${KLEEDIR}" - set +e - docker push "$image" - fi - return 0 -} - -############################################################################### -# Build different layers -############################################################################### - -# Check if the build of dependencies only has been requested -if [[ -z ${DOCKER_BUILD_DEPS_ONLY} || "${DOCKER_BUILD_DEPS_ONLY}x" == "1x" ]]; then - echo "Build dependencies" - docker_build_and_push 1 ${REPOSITORY}/base Dockerfile_base "${DOCKER_OPTS[@]}" - docker_build_and_push 1 ${REPOSITORY}/llvm_built:${LLVM_VERSION_SHORT}${LLVM_SUFFIX} Dockerfile_llvm_build "${DOCKER_OPTS[@]}" - docker_build_and_push 1 ${REPOSITORY}/solver:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX} Dockerfile_solver_build "${DOCKER_OPTS[@]}" - docker_build_and_push 1 ${REPOSITORY}/klee_deps:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} Dockerfile_klee_deps "${DOCKER_OPTS[@]}" -fi - -if [[ -z ${DOCKER_BUILD_DEPS_ONLY} || "${DOCKER_BUILD_DEPS_ONLY}x" != "1x" ]]; then - docker build -f "${DIR}/Dockerfile_klee" "${DOCKER_OPTS[@]}" -t ${REPOSITORY}/klee:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} "${KLEEDIR}" -fi diff --git a/scripts/build/build-travis-containers.sh b/scripts/build/build-travis-containers.sh index ad2ac73a..fe80e29f 100755 --- a/scripts/build/build-travis-containers.sh +++ b/scripts/build/build-travis-containers.sh @@ -3,20 +3,62 @@ # also build by TravisCI. # # Every line starting with " - LLVM_VERSION=" is a single setup + set -e +#set -x DIR="$(cd "$(dirname "$0")" && pwd)" -# Build dependencies only -export DOCKER_BUILD_DEPS_ONLY=1 -export KLEE_TRAVIS_BUILD="1" -export REPOSITORY="klee" -export TRAVIS_OS_NAME="linux" +trim() { + local var="$*" + # remove leading whitespace characters + var="${var#"${var%%[![:space:]]*}"}" + # remove trailing whitespace characters + var="${var%"${var##*[![:space:]]}"}" + echo -n "$var" +} +# Build dependencies only +isGlobal=0 +isEnv=0 +commons=() +experiments=() while read -r line do - name=$(echo $line| grep "\- LLVM" | xargs -L 1 | cut -d "-" -f 2) - if [[ "x$name" == "x" ]]; then + [[ "${line}" == "env:"* ]] && isEnv=1 && continue + [[ "${line}" == "#stop"* ]] && isEnv=0 && break + + + [[ "${isEnv}" -eq 0 ]] && continue + + line="$(trim "${line}")" + + # Ignore empty lines + [[ -z "${line}" ]] && continue + [[ "${line}" == "#"* ]] && continue + + [[ "${line}" == "global:"* ]] && isGlobal=1 && continue + [[ "${line}" == "matrix:"* ]] && isGlobal=0 && continue + + + + if [[ "${isGlobal}" -eq 1 ]]; then + tmp="${line#*-}" + IFS=: read -r key value <<< "${tmp}" + key=$(trim "${key}") + [[ "${key}" == "secure" ]] && continue + [[ -z "${key}" ]] && continue + commons+=("${key}=$(trim "${value}")") continue fi - /bin/bash -c "$name ./scripts/build/build-docker.sh" + + experiment=$(echo "$line"| grep "\- " | xargs -L 1 | cut -d "-" -f 2) + if [[ "x$experiment" == "x" ]]; then + continue + fi + experiments+=("${experiment}") done < "${DIR}/../../.travis.yml" + +for experiment in "${experiments[@]}"; do + [[ -z "${experiment}" ]] && continue + /bin/bash -c "${commons[*]} ${experiment} ${DIR}/build.sh klee --docker --push-docker-deps --debug --create-final-image" +done
\ No newline at end of file diff --git a/scripts/build/build.sh b/scripts/build/build.sh new file mode 100755 index 00000000..feda6bfe --- /dev/null +++ b/scripts/build/build.sh @@ -0,0 +1,803 @@ +#!/usr/bin/env bash +set -e +set -u +# Build script for different components that are needed + +DIR="$(cd "$(dirname "$0")" && pwd)" + +show_help() { + local name="$1" + echo "$name [--docker] [--keep-dockerfile] [--install-system-deps] component*" + echo "Available components:" + for component_path in "$DIR/v-"*.inc; do + [ -e "$component_path" ] || continue + + component_path=${component_path#"$DIR/v-"} + component=${component_path%".inc"} + + echo "$component" + done + + return 0 +} + +function to_upper() { + echo "$1" | tr '[:lower:]' '[:upper:]' +} + +function to_lower() { + echo "$1" | tr '[:upper:]' '[:lower:]' +} + +to_bool() { + [[ "$1" == "1" || "$1" == "ON" || "$1" == "YES" || "$1" == "TRUE" || "$1" == "T" ]] && echo 1 && return 0 + [[ "$1" == "0" || "$1" == "OFF" || "$1" == "NO" || "$1" == "FALSE" || "$1" == "F" ]] && echo 0 && return 0 + # Error case - value unknown + exit 1 +} + +check_bool() { + local v="$1" + local result + result=$(to_bool "${!v}" ) || { echo "${v} has invalid boolean value: ${!v}"; exit 1; } +} + +validate_build_variables() { + # Check general default variables + if [[ -z ${BASE+x} ]] || [[ -z "${BASE}" ]]; then + echo "BASE not set. - BASE directory defines target where every component should be installed" + exit 1 + fi +} + +validate_component() { + local component="$1" + local c_type="$2" + + local component_path="$DIR/${c_type}-${component}.inc" + if [[ ! -f "${component_path}" ]]; then + echo "Component ${component} not found." + return 1 + fi +} + +load_component() { + local component="$1" + local c_type="$2" + + local component_path="$DIR/${c_type}-${component}.inc" + if [[ ! -f "${component_path}" ]]; then + echo "Component ${component} not found." + return 2 # File not found + fi + source "${component_path}" || { echo "Error in file ${component_path}"; return 1; } +} + + +check_docker_os() { + local docker_base=$1 + local os_info="" + # start docker using the base image, link this directory and get the os information + os_info=$(docker run -v "${DIR}:/tmp" "${docker_base}" /tmp/build.sh --check-os) || { echo "Docker execution failed: $os_info"; exit 1;} + + local line + while read -r line; do + case $line in + OS=*) + OS="${line#*=}" + ;; + DISTRIBUTION=*) + DISTRIBUTION="${line#*=}" + ;; + DISTRIBUTION_VER=*) + DISTRIBUTION_VER="${line#*=}" + ;; + esac + done <<< "$os_info" + + echo "Docker OS=${OS}" + echo "Docker DISTRIBUTION=${DISTRIBUTION}" + echo "Docker DISTRIBUTION_VER=${DISTRIBUTION_VER}" +} + + +build_docker() { + local component=$1 + local is_dependency=$2 + + load_component "${component}" "v" || { echo "Loading component failed ${component}"; return 1; } + + # Extract repository, image, tag from base image + local base_repository="${BASE_IMAGE%/*}" + [[ "${base_repository}" == "${BASE_IMAGE}" ]] && base_repository="" # No base repository provided + local base_image="${BASE_IMAGE##*/}" + local base_tag="${base_image##*:}" + if [[ "${base_tag}" == "${base_image}" ]]; then + base_tag="" # No tag provided + else + base_image="${base_image%:*}" + fi + + local BASE="/tmp" + + # Check all input variables + validate_required_variables "${component}" "required_variables" + + # Get the list of build dependencies and check them + local depending_artifact_components=("") + check_list artifact_dependency_"${component}" + mapfile -t depending_artifact_components <<< "$(get_list artifact_dependency_"${component}")" + local v + for v in "${depending_artifact_components[@]}"; do + [[ -z "${v}" ]] && continue + { build_docker "${v}" 1; } || { echo "Not all compile dependencies are available: ${v}"; return 1; } + done + + # Get the list of runtime dependencies + local depending_runtime_artifact_components=("") + mapfile -t depending_runtime_artifact_components <<< "$(get_list runtime_artifact_dependency_"${component}")" + local v + for v in "${depending_runtime_artifact_components[@]}"; do + [[ -z "${v}" ]] && continue + { build_docker "${v}" 1;} || { echo "Not all runtime dependencies are available: ${v}"; return 1; } + done + + echo "Build component: ${component}" + + # Setup general component variables + gather_dependencies "${component}" "artifact" "setup_variables" + + # Get the docker image id if available + local config_id="" + config_id=$(execution_action "get_docker_config_id" "${component}") + res="$?" + [[ "$res" -eq 1 ]] && echo "Building docker dependency ${component} failed: get_docker_config_id_${component}" && return 1 + + # An empty config id indicates nothing to build + [[ -z "${config_id}" ]] && return 0 + + # Use the config id to find a pre-build docker image + local target_image="${component}:${config_id}_${base_image}_${base_tag}" + [[ -z $(docker images -q "${REPOSITORY}/${target_image}") ]] || { echo "Docker image exists: ${REPOSITORY}/${target_image}"; return 0; } + docker pull "${REPOSITORY}/${target_image}" || /bin/true + [[ -z $(docker images -q "${REPOSITORY}/${target_image}") ]] || { echo "Docker image exists: ${REPOSITORY}/${target_image}"; return 0; } + + # Gather all indirect depending components + local all_depending_artifact_components=("") + mapfile -t all_depending_artifact_components <<< "$(get_all_dependencies "${component}" "artifact")" + + local all_depending_runtime_artifact_components=("") + mapfile -t all_depending_runtime_artifact_components <<< "$(get_all_dependencies "${component}" "runtime_artifact")" + + local docker_dependencies=("") + docker_dependencies+=("${all_depending_artifact_components[@]}") + + for c in "${depending_runtime_artifact_components[@]}"; do + local found=0 + for i in "${docker_dependencies[@]}"; do + [[ -z "$i" ]] && continue + [[ "$i" == "$c" ]] && found=1 && break + done + + # Attach item if new + [[ "$found" -eq 0 ]] && docker_dependencies+=("$c") + done + + # Start to build image + local temp_dir + temp_dir="$(mktemp -d)" + [[ -d "${temp_dir}" ]] || (echo "Could not create temp_dir"; exit 1) + + local docker_context="" + docker_context=$(execution_action "get_docker_context" "${component}") || docker_context="" + + local docker_container_context="" + docker_container_context=$(execution_action "get_docker_container_context" "${component}") || docker_container_context="" + + # Prepare Dockerfile + local dockerfile="${temp_dir}/Dockerfile" + + { + # Add all depending images as layers + for v in "${docker_dependencies[@]}"; do + [[ -z "${v}" ]] && continue + local dep_config_id + dep_config_id=$(execution_action "get_docker_config_id" "${v}") || true + # An empty config id indicates nothing to build + [[ -z "${dep_config_id}" ]] && continue + + echo "FROM ${REPOSITORY}/${v}:${dep_config_id}_${base_image}_${base_tag} as ${v}_base" + done + + # If multiple source images are available use the first one as a base image + local hasBaseImage=0 + for v in "${all_depending_artifact_components[@]}"; do + [[ -z "${v}" ]] && continue + dep_config_id=$(execution_action "get_docker_config_id" "${v}") || true + + # An empty config id indicates nothing to build + [[ -z "${dep_config_id}" ]] && continue + + if [[ "${hasBaseImage}" -eq 0 ]]; then + hasBaseImage=1 + # Use base image as building base + echo "FROM ${v}_base as intermediate" + else + # Copy artifacts + # TODO: maybe get list of specific directories to copys + echo "COPY --from=${v}_base ${BASE} ${BASE}/" + fi + done + + if [[ "${hasBaseImage}" -eq 0 ]]; then + hasBaseImage=1 + # Use base image as building base + echo "FROM ${BASE_IMAGE} as intermediate" + fi + + # Retrieve list of required variables and make them available in Docker + local docker_vars=[] + mapfile -t docker_vars <<< "$(get_list required_variables_"$component")" + docker_vars+=("BASE") + for v in "${all_depending_artifact_components[@]}"; do + [[ -z "${v}" ]] && continue + local dep_docker_vars=() + mapfile -t dep_docker_vars <<< "$(get_list required_variables_"${v}")" + docker_vars+=("${dep_docker_vars[@]}") + done + + # Export docker variables explicitly + for d_v in "${docker_vars[@]}"; do + [[ -z "${d_v}" ]] && continue + local d_v_value + d_v_value=${!d_v} + echo "ENV ${d_v}=${d_v_value}" + done + + # Run the build script + if [[ -z "${docker_context}" ]]; then + # Copy content from the temporary directory to the docker image + echo "COPY . ." + echo "RUN ./build.sh --debug --install-system-deps ${component}" + else + echo "COPY . ${docker_container_context}" + # TODO: this is quite specific to this script: should use common value + echo "RUN ${docker_container_context}/scripts/build/build.sh --debug --install-system-deps ${component}" + fi + + # Copy all the build artifacts to the final image: build artifact is the full path + # and will be the same in the destination docker image + if [[ "${is_dependency}" -eq 1 || "${CREATE_FINAL_IMAGE}" -eq 0 ]]; then + echo "FROM ${BASE_IMAGE} as final" + local build_artifacts + mapfile -t build_artifacts <<< "$(execution_action "get_build_artifacts" "${component}")" + for artifact in "${build_artifacts[@]}"; do + [[ -z "${artifact}" ]] && continue + echo "COPY --from=intermediate ${artifact} ${artifact}" + done + + # Copy all the runtime dependencies + for dep_component in "${all_depending_runtime_artifact_components[@]}"; do + [[ -z "${dep_component}" ]] && continue + local build_artifacts + mapfile -t build_artifacts <<< "$(execution_action "get_build_artifacts" "${dep_component}")" + for artifact in "${build_artifacts[@]}"; do + [[ -z "${artifact}" ]] && continue + echo "COPY --from=intermediate ${artifact} ${artifact}" + done + done + fi + # TODO Add description labels + echo "LABEL maintainer=\"KLEE Developers\"" + } >> "${dockerfile}" + + # Append template file if exists + docker_template_files=( + "${DIR}/d-${component}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc" + "${DIR}/d-${component}-${OS}-${DISTRIBUTION}.inc" + "${DIR}/d-${component}-${OS}.inc" + "${DIR}/d-${component}.inc" + ) + for f in "${docker_template_files[@]}"; do + [[ ! -f "$f" ]] && continue + cat "$f" >> "${dockerfile}" + break + done + + # Copy docker context and dependencies + shopt -s nullglob # allow nullglobing + echo "${all_depending_artifact_components[@]}" + for v in "${all_depending_artifact_components[@]}" "${component}"; do + [[ -z "${v}" ]] && continue + local files=( + "${DIR}/"*"-${v}.inc" \ + "${DIR}/"*"-${v}-${OS}.inc" \ + "${DIR}/"*"-${v}-${OS}-${DISTRIBUTION}.inc" \ + "${DIR}/"*"-${v}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc" \ + "${DIR}/build.sh" \ + "${DIR}/common-functions" + ) + local f + for f in "${files[@]}"; do + [ -f "$f" ] || continue + cp -r "$f" "${temp_dir}/" + done + + mkdir -p "${temp_dir}/patches" + for f in "${DIR}/patches/${v}"*.patch; do + cp -r "$f" "${temp_dir}/patches/" + done + done + shopt -u nullglob # disallow nullglobing + + if [[ -z "${docker_context}" ]]; then + docker_context="${temp_dir}" + fi + + # Build Docker container + docker build -t "${REPOSITORY}/${target_image}" -f "${temp_dir}"/Dockerfile "${docker_context}" || return 1 + if [[ "${PUSH_DOCKER_DEPS}" -eq 1 && "${is_dependency}" -eq 1 ]]; then + docker push "${REPOSITORY}/${target_image}" || /usr/bin/true + fi + + if [[ "${KEEP_DOCKERFILE}" -eq 0 ]]; then + # Clean-up docker build directory + rm -rf "${temp_dir}" + else + echo "Preserved docker directory: ${temp_dir}" + fi +} + +check_os() { + if [[ "$OSTYPE" == "linux-gnu" ]]; then + # Host is Linux + OS="linux" + DISTRIBUTION="$(grep ^ID= /etc/os-release)" + DISTRIBUTION=${DISTRIBUTION#"ID="} + DISTRIBUTION_VER="$(grep ^VERSION_ID= /etc/os-release || echo "")" + DISTRIBUTION_VER=${DISTRIBUTION_VER#"VERSION_ID="} + # Remove `"`, if exists + DISTRIBUTION_VER=${DISTRIBUTION_VER#\"} + DISTRIBUTION_VER=${DISTRIBUTION_VER%\"} + + elif [[ "$OSTYPE" == "darwin"* ]]; then + # Host is Mac OS X + OS="osx" + DISTRIBUTION="$(sw_vers -productName)" + DISTRIBUTION_VER="$(sw_vers -productVersion)" + else + echo "Operating System unknown $OSTYPE" + exit 1 + fi + echo "Detected OS: ${OS}" + echo "OS=${OS}" + echo "Detected distribution: ${DISTRIBUTION}" + echo "DISTRIBUTION=${DISTRIBUTION}" + echo "Detected version: ${DISTRIBUTION_VER}" + echo "DISTRIBUTION_VER=${DISTRIBUTION_VER}" +} + + +# +try_execute() { + # Check if a function exists and execute it + fct=$1 + # promote that function does not exist + [[ "$(type -t "${fct}")" != "function" ]] && return 2 + + # promote the return value of the function + local failed=0 + "${fct}" || failed=1 + return "${failed}" +} + +try_execute_if_exists() { + # Check if a function exists and execute it + fct=$1 + # Ignore if function does not exist + [[ "$(type -t "${fct}")" != "function" ]] && return 0 + + # promote the return value of the function + local failed=0 + "${fct}" || failed=1 + return "${failed}" +} + +# Execute the most system specific action possible. +# If an action executed successfuly, return 0 +# The function will return 1 if an action was not successful +execution_action() { + local action="$1" + local component="$2" + local found=0 + + # Execute most specific action: os + distribution + distribution version + if [[ -f "${DIR}/p-${component}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc" ]]; then + found=1 + source "${DIR}/p-${component}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc" + local failed=0 + try_execute "${action}"_"${component}" || failed=1 + [[ "$failed" -eq 0 ]] && return 0 + fi + + # Execute most specific action: os + distribution + if [[ -f "${DIR}/p-${component}-${OS}-${DISTRIBUTION}.inc" ]]; then + found=1 + source "${DIR}/p-${component}-${OS}-${DISTRIBUTION}.inc" + local failed=0 + try_execute "${action}"_"${component}" || failed=1 + [[ "$failed" -eq 0 ]] && return 0 + fi + + # Execute most specific action: os + if [[ -f "${DIR}/p-${component}-${OS}.inc" ]]; then + found=1 + source "${DIR}/p-${component}-${OS}.inc"; + local failed=0 + try_execute "${action}"_"${component}" || failed=1 + [[ "$failed" -eq 0 ]] && return 0 + fi + + # Execute package specific action: + if [[ -f "${DIR}/p-${component}.inc" ]]; then + found=1 + source "${DIR}/p-${component}.inc"; + local failed=0 + try_execute "${action}"_"${component}" || failed=1 + [[ "$failed" -eq 0 ]] && return 0 + fi + + # Found an action file but something didn't work + [[ "${found}" -eq 1 ]] && return 1 + + # No action found + return 2 +} + +## +# Returns a list that is the result of either an array or function call +get_list(){ + local list_name=$1 + local result=("") + + if [[ "$(type -t "${list_name}")" == "function" ]]; then + mapfile -t result <<< "$("${list_name}")" + elif [[ -n ${!list_name+x} ]]; then + list_array="${list_name}[@]" + result=("${!list_array}") + fi + + for i in "${result[@]}"; do + [[ -z "${i}" ]] && continue + echo "${i}" + done + + return 0 +} + +## +# Check if a lists exist +## +check_list(){ + local list_name=$1 + if [[ "$(type -t "${list_name}")" == "function" ]]; then + return 0 + fi + local list_array="${list_name}[@]" + if [[ ${!list_array+x} ]]; then + return 0 + fi + echo "Variable or function \"${list_name}\" not found" + exit 1 +} + +validate_required_variables() { + local component="$1" + local type="$2" + local variables + check_list required_variables_"${component}" + mapfile -t variables <<< "$(get_list "${type}"_"${component}")" + + if [[ -n "${variables[*]}" ]]; then + # Check if variables are defined + for v in "${variables[@]}"; do + if [[ -z ${!v+x} ]]; then + echo "${v} Required but unset" + exit 1 + fi + done + fi + + try_execute_if_exists required_variables_check_"${component}" +} + +get_all_dependencies_rec() { + local component="$1" + local type="$2" + local depending_components + # Get the list of dependencies + mapfile -t depending_components <<< "$(get_list "${type}"_dependency_"${component}")" + for v in "${depending_components[@]}"; do + [[ -z "${v}" ]] && continue + get_all_dependencies_rec "$v" "$type" + done + echo "$component" +} + +get_all_dependencies() { + local component="$1" + local type="$2" + local depending_components=("") + # Get the list of dependencies + mapfile -t depending_components <<< "$(get_list "${type}"_dependency_"${component}")" + local final_list=("${depending_components[@]}") + for v in "${depending_components[@]}"; do + [[ -z "${v}" ]] && continue + local deps_list=("") + local failed=0 + mapfile -t deps_list <<< "$(get_all_dependencies_rec "$v" "$type")" + [[ "${failed}" -eq 1 ]] && continue + + # Make sure items are unique and keep the order of occurence + for di in "${deps_list[@]}"; do + local found=0 + for f in "${final_list[@]}"; do + [[ -z "$f" ]] && continue + [[ "$di" == "$f" ]] && found=1 && break + done + [[ "$found" -eq 0 ]] && final_list+=("${di}") + done + done + + for v in "${final_list[@]}"; do + echo "${v}" + done +} + +gather_dependencies_rec() { + local component="$1" + local type="$2" + local action="$3" + + load_component "${component}" "v" || { echo "Loading component failed ${component}"; return 1; } + validate_required_variables "${component}" "required_variables" + + # Get the list of dependencies + local variables + check_list "${type}"_dependency_"${component}" + mapfile -t variables <<< "$(get_list "${type}"_dependency_"${component}")" + for v in "${variables[@]}"; do + [[ -z "${v}" ]] && continue + gather_dependencies_rec "$v" "${type}" "${action}" + done + + try_execute_if_exists "${action}"_"${component}" +} + +gather_dependencies() { + local component="$1" + local dependency_type="$2" + local action="$3" + + local depending_components + # Get the list of dependencies + check_list "${dependency_type}"_dependency_"${component}" + mapfile -t depending_components <<< "$(get_list "${dependency_type}"_dependency_"${component}")" + + for v in "${depending_components[@]}"; do + [[ -z "${v}" ]] && continue + gather_dependencies_rec "$v" "${dependency_type}" "${action}" + done + try_execute_if_exists "${action}"_"${component}" +} + +check_module() { + local module="$1" + # Validate module if different functions or arrays exist + ( + load_component "${module}" "v" || return 1 + list_or_functions=( + required_variables + artifact_dependency + ) + for item in "${list_or_functions[@]}"; do + check_list "${item}_${module}" + done + + ) || { echo "Module $1 not valid"; return 1; } + + # Validate build instructions + ( + validate_component "${module}" "p" || { echo "No build instructions found for ${module}"; return 0; } + load_component "${module}" "p" + + list_or_functions=( + setup_build_variables + download + build + install + is_installed + setup_artifact_variables + get_build_artifacts + get_docker_config_id + ) + for item in "${list_or_functions[@]}"; do + check_list "${item}_${module}" + done + + ) || { echo "Build instructions for ${module} are not valid"; return 1; } + +} + +## +## Install the specified component +install_component() { + local component="$1" + + # Load general component information + load_component "${component}" "v" || { echo "Loading component failed ${component}"; return 1; } + + # Get the list of dependencies + local depending_artifact_components + check_list artifact_dependency_"${component}" + mapfile -t depending_artifact_components <<< "$(get_list artifact_dependency_"${component}")" + + # Make sure an artefact is available for the depending component + for v in "${depending_artifact_components[@]}"; do + [[ -z "${v}" ]] && continue + install_component "${v}" + done + + # Setup general component variables + validate_required_variables "${component}" "required_variables" + + # Handle dependencies of required artifacts + gather_dependencies "${component}" "artifact" "setup_variables" + + # Check if the artifact is installed ablready + execution_action is_installed "${component}" && execution_action setup_artifact_variables "${component}" && validate_required_variables "${component}" "export_variables" && { echo "Already installed ${component}"; return 0; } + + # Install package if available + execution_action install_binary_artifact "${component}" && execution_action setup_artifact_variables "${component}" && validate_required_variables "${component}" "export_variables" && { echo "Package installed ${component}"; return 0 ;} + + # Validate general build variables + validate_build_variables + + # Check if there is build information, if not - this is a meta package, return + validate_component "${component}" "p" || return 0 + + # Load build description + load_component "${component}" "p" || { echo "Loading component failed ${component}"; return 1; } + + # Setup build variables + setup_build_variables_"${component}" + + # Check and install runtime-dependencies if needed + execution_action "install_runtime_dependencies" "${component}" || true + + # Validate configuration + try_execute_if_exists validate_build_config_"${component}" + + # Install build dependencies + if [[ "${INSTALL_SYSTEM_DEPS}" == "1" ]]; then + execution_action "install_build_dependencies" "${component}" || { + echo "Could not install build dependencies for ${component}"; + return 1; + } + fi + + # Install build source + try_execute_if_exists download_"${component}" + + # Build the package + try_execute_if_exists build_"${component}" + + # Install to its final destination + try_execute_if_exists install_"${component}" +} + + +main() { + local NAME + NAME=$(basename "${0}") + local USAGE="usage: ${NAME} " + local COMPONENTS=() + local BUILD_DOCKER=0 + local INSTALL_SYSTEM_DEPS=0 + local KEEP_DOCKERFILE=0 + local CHECK_MODULE=0 + local PUSH_DOCKER_DEPS=0 + local CREATE_FINAL_IMAGE=0 + + for i in "$@" ;do + case $i in + --debug) + set -x + ;; + --docker) + BUILD_DOCKER=1 + ;; + --keep-dockerfile) + KEEP_DOCKERFILE=1 + ;; + --push-docker-deps) + PUSH_DOCKER_DEPS=1 + ;; + --create-final-image) + CREATE_FINAL_IMAGE=1 + ;; + --install-system-deps) + INSTALL_SYSTEM_DEPS=1 + ;; + --help) + show_help "${NAME}" + exit 0 + ;; + --check-os) + # Checks the operating sytem used + check_os + exit 0 + ;; + --check-module) + # Check the validity of the module + CHECK_MODULE=1 + ;; + -*) + echo "${NAME}: unknown argument: $i" + show_help "${NAME}" + exit 1 + ;; + *) + COMPONENTS+=("$i") + ;; + esac + done + + if [[ ${#COMPONENTS[@]} -eq 0 ]]; then + show_help "${NAME}" + exit 1 + fi + + + if [[ "${CHECK_MODULE}" -eq 1 ]]; then + for m in "${COMPONENTS[@]}"; do + check_module "${m}" + done + exit 0 + fi + + # Validate selected components: check if they have a v-"component".inc file + for c in "${COMPONENTS[@]}"; do + validate_component "$c" "v" + done + + if [[ "${BUILD_DOCKER}" == "1" ]]; then + if [[ -z ${BASE_IMAGE+X} ]]; then + echo "No BASE_IMAGE provided" + exit 1 + fi + if [[ -z ${REPOSITORY+X} ]]; then + echo "No REPOSITORY provided" + exit 1 + fi + + # Gather information about the base image + check_docker_os "${BASE_IMAGE}" + + # Install components + for c in "${COMPONENTS[@]}"; do + build_docker "$c" 0 || { echo "Building docker image ${c} failed"; return 1; } + done + else + # General Setup + check_os + + # Install components + for c in "${COMPONENTS[@]}"; do + install_component "$c" + try_execute_if_exists check_export_variables_"$c" + done + fi +} + +main "$@" diff --git a/scripts/build/common-defaults.sh b/scripts/build/common-defaults.sh deleted file mode 100644 index 5cefef19..00000000 --- a/scripts/build/common-defaults.sh +++ /dev/null @@ -1,53 +0,0 @@ -# This file is meant to be included by shell scripts to provide common default -# values. -# It is used by: travis builds; docker builds and local builds -# Change defaults to setup different development environment -# Defines defaults used to build a default docker image outside of Travis -if [[ "${DOCKER_BUILD}x" == "1x" ]]; then - # Default for docker: Do not keep build and source files for small images - : "${KEEP_BUILD:=0}" - : "${KEEP_SRC:=0}" - echo "DOCKER_BUILD" -fi -if [[ "${KLEE_TRAVIS_BUILD}x" != "1x" ]]; then -: "${REPOSITORY:=klee}" -: "${LLVM_VERSION:=3.4}" -: "${DISABLE_ASSERTIONS:=0}" -: "${ENABLE_DEBUG:=1}" -: "${ENABLE_OPTIMIZED:=1}" -: "${SOLVERS:=STP}" -: "${STP_VERSION:=2.1.2}" -: "${Z3_VERSION:=4.4.1}" -: "${METASMT_VERSION:=v4.rc1}" -: "${METASMT_DEFAULT:=STP}" -: "${METASMT_BOOST_VERSION:=}" -: "${REQUIRES_RTTI:=0}" -: "${KLEE_UCLIBC:=klee_uclibc_v1.0.0}" -: "${USE_TCMALLOC:=1}" -: "${PACKAGED:=0}" -# undefined, address, memory -: "${SANITIZER_BUILD:=}" -# Defines if source and build artifacts should be preserved -: "${KEEP_BUILD:=1}" -: "${KEEP_SRC:=1}" -OS="$(uname)" -case $OS in - 'Linux') - TRAVIS_OS_NAME='linux' - ;; - 'Darwin') - TRAVIS_OS_NAME='osx' - ;; - *) ;; -esac -fi - -# General default values -: "${TCMALLOC_VERSION:=2.4}" -: "${GTEST_VERSION:=1.7.0}" - -if [[ "${DIR}x" == "x" ]]; then - echo "\${DIR} not set" - exit 1 -fi -source "${DIR}/common-functions" diff --git a/scripts/build/common-functions b/scripts/build/common-functions index 499b51b7..6d810d73 100644 --- a/scripts/build/common-functions +++ b/scripts/build/common-functions @@ -16,203 +16,18 @@ function git_clone_or_update() { fi } -function to_upper() { - echo "$1" | tr '[:lower:]' '[:upper:]' -} - -function to_lower() { - echo "$1" | tr '[:upper:]' '[:lower:]' -} - -# This file is meant to be included by shell scripts -# that need to do a sanitized build. - -# Users of this script can use this variable -# to detect if a Sanitized build was enabled. -IS_SANITIZED_BUILD=0 - -# Remove ":" separator -sanitizers=(${SANITIZER_BUILD//:/ }) -# Sort sanitizers -IFS=$'\n' sorted_sanitizers=($(sort <<<"${sanitizers[*]}")) -unset IFS - -# Set variables used by clients. -## Build variables -SANITIZER_CXX_FLAGS="" -SANITIZER_C_FLAGS="" -SANITIZER_LD_FLAGS="" -# Docker_suffix -SANITIZER_SUFFIX="" - -# -for sanitizer in ${sorted_sanitizers[@]}; do - # AddressSanitizer - if [ "X${sanitizer}" == "Xaddress" ]; then - echo "Using ASan" - flags=" -fsanitize=address -fno-omit-frame-pointer -g" - SANITIZER_CXX_FLAGS+=" ${flags}" - SANITIZER_C_FLAGS+=" ${flags}" - SANITIZER_LD_FLAGS+=" ${flags}" - SANITIZER_SUFFIX+="_asan" - IS_SANITIZED_BUILD=1 - continue - fi - - # Undefined Behaviour Sanitizer - if [ "X${sanitizer}" == "Xundefined" ]; then - echo "Using UBSan" - flags="-fsanitize=undefined -fno-omit-frame-pointer -g" - SANITIZER_CXX_FLAGS+=" ${flags}" - SANITIZER_C_FLAGS+=" ${flags}" - SANITIZER_LD_FLAGS+=" ${flags} -lubsan -fuse-ld=gold" - SANITIZER_SUFFIX+="_ubsan" - IS_SANITIZED_BUILD=1 - continue - fi - - # Undefined Behaviour Sanitizer - if [ "X${sanitizer}" == "Xmemory" ]; then - echo "Using Memory Sanitizer" - if [[ "X${PACKAGED}" == "X1" ]]; then - echo "simultanously memory sanitizer and packaged is not supported " - exit 1 - fi - - SANITIZER_SUFFIX+="_memsan" - SANITIZER_LLVM_UNINSTRUMENTED="${LLVM_BUILD}_uninstrumented" - SANITIZER_LLVM_LIBCXX="${LLVM_BUILD}_libcxx" - - SANITIZER_C_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang" - SANITIZER_CXX_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang++" - SANITIZER_CMAKE_C_COMPILER="-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}" - SANITIZER_CMAKE_CXX_COMPILER="-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}" - - MSAN_LINK_FLAGS="-lc++abi -Wl,--rpath=${SANITIZER_LLVM_LIBCXX}/lib -L${SANITIZER_LLVM_LIBCXX}/lib"; - MSAN_FLAGS="$MSAN_LINK_FLAGS -nostdinc++ \ - -isystem ${SANITIZER_LLVM_LIBCXX}/include \ - -isystem ${SANITIZER_LLVM_LIBCXX}/include/c++/v1 \ - -fsanitize=memory \ - -fsanitize-memory-track-origins \ - -w -fno-omit-frame-pointer -g"; - - SANITIZER_CXX_FLAGS+="${MSAN_FLAGS} -stdlib=libc++" - SANITIZER_C_FLAGS+="${MSAN_FLAGS}" - SANITIZER_LD_FLAGS+="${MSAN_LINK_FLAGS}" - - IS_SANITIZED_BUILD=1 - continue - fi - - echo "Unknown sanitizer: $sanitizer" - exit 1 -done - -# This file is meant to be included by shell scripts -# that need to retrieve llvm-specifi variables - -LLVM_VERSION_SHORT="${LLVM_VERSION/./}" -LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" -LLVM_SUFFIX="" - -BuildMode='' - -# Build from source -if [[ "${PACKAGED}x" == "1x" ]]; then - LLVM_SUFFIX+="_packaged" - set +e - llvm_config_path=$(which llvm-config-${LLVM_VERSION}) - if [[ -e "${llvm_config_path}" ]]; then - LLVM_BIN="$(llvm-config-${LLVM_VERSION} --bindir)" - fi - set -e -else - if [[ "${ENABLE_OPTIMIZED}" == "1" ]]; then - LLVM_SUFFIX+="_O" - BuildMode="Release" - else - LLVM_SUFFIX+="_NO" - fi - - if [[ ("${ENABLE_DEBUG}" == "1") || ("${ENABLE_OPTIMIZED}" != "1") ]]; then - LLVM_SUFFIX+="_D" - [ -z "$BuildMode" ] && BuildMode="Debug" || BuildMode="$BuildMode+Debug" - else - LLVM_SUFFIX+="_ND" - fi - - if [[ "${DISABLE_ASSERTIONS}" == "1" || -z "${DISABLE_ASSERTIONS}" ]]; then - LLVM_SUFFIX+="_NA" - else - LLVM_SUFFIX+="_A" - [ -z "$BuildMode" ] && BuildMode="Asserts" || BuildMode="$BuildMode+Asserts" - fi - - if [[ "${REQUIRES_RTTI}" == "1" ]]; then - LLVM_SUFFIX+="_RTTI" - fi - - if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then - LLVM_SUFFIX+="${SANITIZER_SUFFIX}" - fi - - LLVM_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}" - LLVM_BUILD="${LLVM_BASE}-build${LLVM_SUFFIX}" - LLVM_INSTALL="${LLVM_BASE}-install${LLVM_SUFFIX}" - LLVM_BIN="${LLVM_INSTALL}/bin" - if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then - LLVM_BUILDMODE="$BuildMode" - LLVM_BUILD_BIN="${LLVM_BUILD}/${LLVM_BUILDMODE}/bin" +function get_git_hash() { + local url="$1" + local branch="$2" + local commit_id="" + + # List remote git branches and get the commit id of the branch + commit_id="$(git ls-remote -h "$url" |grep "$branch" | cut -d$'\t' -f 1)" + + # If that doesn't work use the branch instead of the commit id + if [[ -z "${commit_id}" ]]; then + echo "${branch}" else - LLVM_BUILD_BIN="${LLVM_BUILD}/bin" - fi -fi - -# Generate the suffix used for the solver combination -# Every solver needs to have a version explicitly specified -SOLVER_SUFFIX="" - -# Remove ":" separator -solvers=(${SOLVERS//:/ }) - -# Sort solvers -IFS=$'\n' sorted_solvers=($(sort <<<"${solvers[*]}")) -unset IFS - -for solver in ${sorted_solvers[@]}; do - # Make sure version a solver specific version variable is used - solver_var="$(to_upper "$solver")_VERSION" - SOLVER_VERSION="${!solver_var}" - if [[ -z "${SOLVER_VERSION}" ]] ; then - echo "Solver version for $solver not defined" - exit 1 - fi - # Add the solver to the suffix and lower case it - SOLVER_SUFFIX+="_$(to_lower "$solver")$(to_lower "$SOLVER_VERSION")" - echo $SOLVER_SUFFIX - if [[ "$(to_lower "$solver")" == "metasmt" ]]; then - if [[ "${REQUIRES_RTTI}x" != "1x" ]]; then - echo "METASMT requires an RTTI build" - exit 1 - fi - if [[ -z "${METASMT_DEFAULT}" ]]; then - echo "METASMT_DEFAULT not defined" - exit 1 - fi - if [[ -z "${METASMT_BOOST_VERSION}" ]] ; then - echo "METASMT_BOOST_VERSION not defined - use default" - SOLVER_SUFFIX+="_$(to_lower "$METASMT_DEFAULT")_boost-dev" - else - SOLVER_SUFFIX+="_$(to_lower "$METASMT_DEFAULT")_$(to_lower "$METASMT_BOOST_VERSION")" - fi + echo "${commit_id:0:7}" fi -done - -# This file is meant to be included by shell scripts that handle dependencies by -# KLEE beside LLVM and solvers -# -# Generate the suffix used for direct dependencies of KLEE like uclibc -DEPS_SUFFIX="" -if [[ "${KLEE_UCLIBC}" != "0" ]]; then - DEPS_SUFFIX+="_${KLEE_UCLIBC}" -fi +}
\ No newline at end of file diff --git a/scripts/build/d-klee-linux-ubuntu.inc b/scripts/build/d-klee-linux-ubuntu.inc new file mode 100644 index 00000000..38b8dce5 --- /dev/null +++ b/scripts/build/d-klee-linux-ubuntu.inc @@ -0,0 +1,23 @@ +# TODO remove adding sudo package +# Create ``klee`` user for container with password ``klee``. +# and give it password-less sudo access (temporarily so we can use the TravisCI scripts) +RUN apt update && apt -y --no-install-recommends install sudo && \ + rm -rf /var/lib/apt/lists/* && \ + useradd -m klee && \ + echo klee:klee | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers + +ENV BASE=/tmp +# Copy across source files needed for build +# Set klee user to be owner +ADD --chown=klee:klee / ${BASE}/klee_src + +USER klee +WORKDIR /home/klee + +# Add KLEE binary directory to PATH +RUN /bin/bash -c 'ln -s ${BASE}/klee_src /home/klee/ && ln -s ${BASE}/klee_build* /home/klee/klee_build && echo "export PATH=\"$PATH:$(cd /tmp/llvm-*install*/bin && pwd):/home/klee/klee_build/bin\"" >> /home/klee/.bashrc' + +# TODO Remove when STP is fixed +RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd)" >> /home/klee/.bashrc' diff --git a/scripts/build/dependencies-ubuntu.sh b/scripts/build/dependencies-ubuntu.sh deleted file mode 100755 index d5d4a36a..00000000 --- a/scripts/build/dependencies-ubuntu.sh +++ /dev/null @@ -1,43 +0,0 @@ -#!/bin/bash -# Installs ubuntu dependencies -set -e - -# Update packages -apt update - -# Install essential build tools -apt -y --no-install-recommends install build-essential software-properties-common wget - -# Add repository for additional compilers -add-apt-repository ppa:ubuntu-toolchain-r/test -y -add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial main" -wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add - -apt update -y - -#Install essential dependencies -apt -y --no-install-recommends install \ - binutils \ - bison \ - cmake \ - curl \ - flex \ - git \ - groff-base \ - libboost-program-options-dev \ - libncurses-dev \ - ninja-build \ - patch \ - perl \ - python \ - python3-dev \ - python3-pip \ - python3-setuptools \ - subversion \ - sudo \ - unzip \ - wget \ - zlib1g-dev -apt clean - -# Install lit for testing -pip3 install wheel && pip3 install lit==0.6.0 diff --git a/scripts/build/install-klee-deps.sh b/scripts/build/install-klee-deps.sh deleted file mode 100755 index 622e621f..00000000 --- a/scripts/build/install-klee-deps.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash -set -e -########################################################################### -# Install KLEE dependencies -########################################################################### -DIR="$(cd "$(dirname "$0")" && pwd)" - -if [[ "${BASE}x" == "x" ]]; then - echo "\${BASE} not set" - exit 1 -fi - -# Install LLVM and the LLVM bitcode compiler we require to build KLEE -"${DIR}/llvm.sh" - -# Install allocators -"${DIR}/tcmalloc.sh" - -# Get SMT solvers -"${DIR}/solvers.sh" - -# Get needed utlities/libraries for testing KLEE -"${DIR}/testing-utils.sh" - -# Install uclibc -"${DIR}/uclibc.sh" diff --git a/scripts/build/install-local.sh b/scripts/build/install-local.sh deleted file mode 100755 index 50dfb612..00000000 --- a/scripts/build/install-local.sh +++ /dev/null @@ -1,17 +0,0 @@ -#!/bin/bash -# Install all dependencies to build KLEE in a directory ${BASE} -set -e -if [[ "${BASE}x" == "x" ]]; then - echo "\${BASE} not set" - exit 1 -fi - -# Create base directory if not exists -mkdir -p "${BASE}" -DIR=$(dirname "$(readlink -f "$0" || stat -f "$0")") - -# Install dependencies -"${DIR}/install-klee-deps.sh" - -# Build KLEE -"${DIR}/klee.sh" diff --git a/scripts/build/klee.sh b/scripts/build/klee.sh deleted file mode 100755 index 84d7bd63..00000000 --- a/scripts/build/klee.sh +++ /dev/null @@ -1,219 +0,0 @@ -#!/bin/bash -x -# Compile KLEE -# Make sure we exit if there is a failure -set -e - -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -: ${SOLVERS?"Solvers must be specified"} -if [[ -z "${KLEE_UCLIBC}" ]]; then - echo "KLEE_UCLIBC must be specified: 0 or branch/tag" - exit 1 -fi -if [[ -z "${KLEE_SRC}" ]]; then - # Assumeption: this build script is part of the KLEE source tree - KLEE_SRC="${DIR}/../.." -fi - -CMAKE_PREFIX_PATH="" -############################################################################### -# Handling LLVM configuration -############################################################################### -if [[ "$TRAVIS_OS_NAME" = "linux" ]] ; then - LLVM_CONFIG="${LLVM_BIN}/llvm-config" - LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION_SHORT}/build" - KLEE_CC="${LLVM_BIN}/clang" - KLEE_CXX="${LLVM_BIN}/clang++" -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - LLVM_BIN="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin" - LLVM_CONFIG="${LLVM_BIN}/llvm-config" - LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)" - KLEE_CC="${LLVM_BIN}/clang" - KLEE_CXX="${LLVM_BIN}/clang++" -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi - -############################################################################### -# klee-uclibc -############################################################################### -if [ "${KLEE_UCLIBC}" != "0" ]; then - KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH="${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" -DENABLE_POSIX_RUNTIME=TRUE) -else - KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE) -fi - -COVERAGE_FLAGS="" -if [ ${COVERAGE} -eq 1 ]; then - COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage' -fi - - -############################################################################### -# Handle setting up solver configure flags for KLEE -############################################################################### -SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g') - -# Set CMake configure options -KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=OFF) -KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=OFF) -KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=OFF) -for solver in ${SOLVER_LIST}; do - echo "Setting CMake configuration option for ${solver}" - case ${solver} in - STP) - KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=TRUE -DSTP_DIR="${BASE}/stp-${STP_VERSION}-install") - ;; - Z3) - echo "Z3" - KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=TRUE) - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - KLEE_Z3_CONFIGURE_OPTION+=(-DZ3_INCLUDE_DIRS="${BASE}/z3-${Z3_VERSION}-install/include" -DZ3_LIBRARIES="${BASE}/z3-${Z3_VERSION}-install/lib/libz3.so") - fi - ;; - metaSMT) - echo "metaSMT" - if [ "X${METASMT_DEFAULT}" == "X" ]; then - METASMT_DEFAULT=STP - fi - KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR="${BASE}/metaSMT/build" -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}") - ;; - *) - echo "Unknown solver ${solver}" - exit 1 - esac -done - -############################################################################### -# Handle additional configure flags -############################################################################### - -TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") -if [[ "$TCMALLOC_OPTION" != "0" ]] ; then - if [[ ! -z "${CMAKE_PREFIX_PATH}" ]]; then - CMAKE_PREFIX_PATH+=":" - fi - CMAKE_PREFIX_PATH="${CMAKE_PREFIX_PATH}$BASE/tcmalloc-install" -fi - -############################################################################### -# KLEE -############################################################################### -KLEE_BUILD="${BASE}/klee_build${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX}" -mkdir -p "${KLEE_BUILD}" -cd "${KLEE_BUILD}" -GTEST_SRC_DIR="${BASE}/googletest-release-${GTEST_VERSION}/" -if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then - KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE" -else - KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE" -fi - -if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then - CMAKE_BUILD_TYPE="RelWithDebInfo" -else - CMAKE_BUILD_TYPE="Debug" -fi - -# TODO: We should support Ninja too -# Configure KLEE -echo "CXXFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}\" \ -CFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}\" \ -LDFLAGS=\"${COVERAGE_LDFLAGS} ${SANITIZER_LD_FLAGS}\" \ -cmake \ - -DLLVM_CONFIG_BINARY=\"${LLVM_CONFIG}\" \ - -DLLVMCC=\"${KLEE_CC}\" \ - -DLLVMCXX=\"${KLEE_CXX}\" \ - ${KLEE_STP_CONFIGURE_OPTION[@]} \ - ${KLEE_Z3_CONFIGURE_OPTION[@]} \ - ${KLEE_METASMT_CONFIGURE_OPTION[@]} \ - ${KLEE_UCLIBC_CONFIGURE_OPTION[@]} \ - ${TCMALLOC_OPTION[@]} \ - -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \ - -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \ - ${KLEE_ASSERTS_OPTION[@]} \ - -DENABLE_UNIT_TESTS=TRUE \ - -DENABLE_SYSTEM_TESTS=TRUE \ - -DLIT_ARGS=\"-v\" \ - ${SANITIZER_CMAKE_C_COMPILER[@]} \ - ${SANITIZER_CMAKE_CXX_COMPILER[@]} \ - -DCMAKE_PREFIX_PATH=${CMAKE_PREFIX_PATH} \ - ${KLEE_SRC}" > "${KLEE_BUILD}/.build_command" -source "${KLEE_BUILD}/.build_command" -make -j$(nproc) - -############################################################################### -# Prepare Coverage functionality -############################################################################### -coverage_setup() -{ - # TODO Remove it and put it to the proper package install section - apt update && apt -y --no-install-recommends install lcov - # Zero coverage for any file, e.g. previous tests - lcov --directory . --no-external --zerocounters - # Create a baseline by capturing any file used for compilation, no execution yet - lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --initial --output-file coverage_base.info - lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info - lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info -} - -coverageup() -{ - tags=$1 - codecov_suffix=(${tags// /}) - # Create report - # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped) - lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --output-file coverage.info - # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests) - lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info - lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info - # Combine baseline and measured coverage - lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info.${codecov_suffix} - # Debug info - lcov --rc lcov_branch_coverage=1 --list coverage_all.info.${codecov_suffix} -} - -COVERAGE=${COVERAGE:=0} - -############################################################################### -# Unit tests -############################################################################### -# Prepare coverage information if COVERAGE is set -if [ ${COVERAGE} -eq 1 ]; then - coverage_setup -fi -make unittests - -# Generate and upload coverage if COVERAGE is set -if [ ${COVERAGE} -eq 1 ]; then - coverageup "unittests" -fi - -############################################################################### -# lit tests -############################################################################### -if [ ${COVERAGE} -eq 1 ]; then - coverage_setup -fi -make systemtests - -# If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends -if [ "X${SOLVERS}" == "XmetaSMT" ]; then - metasmt_default=$(to_lower $METASMT_DEFAULT) # klee_opts and kleaver_opts use lowercase - available_metasmt_backends="btor stp z3 yices2 cvc4" - for backend in $available_metasmt_backends; do - if [ "X${metasmt_default}" != "X$backend" ]; then - if [ "$backend" == "cvc4" ]; then - for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done & - fi - lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/ - fi - done -fi - -# Generate and upload coverage if COVERAGE is set -if [ ${COVERAGE} -eq 1 ]; then - coverageup "systemtests" -fi diff --git a/scripts/build/llvm.sh b/scripts/build/llvm.sh deleted file mode 100755 index 92370159..00000000 --- a/scripts/build/llvm.sh +++ /dev/null @@ -1,193 +0,0 @@ -#!/bin/bash -x -set -ev -STAGE="$1" - -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -if [[ "${LLVM_VERSION_SHORT}" == "" ]]; then - echo "LLVM_VERSION_SHORT not set" - exit 1 -fi - -if [[ "${BASE}" == "" ]]; then - echo "BASE not set" - exit 1 -fi - -# Install packages if possible -if [[ "${PACKAGED}x" == "1x" ]]; then - apt update - apt install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev - apt install -y clang-${LLVM_VERSION} - exit 0 -fi - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - LLVM_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}" - # Checkout LLVM code - svn co http://llvm.org/svn/llvm-project/llvm/branches/release_${LLVM_VERSION_SHORT} "${LLVM_BASE}" - cd "${LLVM_BASE}/tools" - svn co http://llvm.org/svn/llvm-project/cfe/branches/release_${LLVM_VERSION_SHORT} clang - cd "${LLVM_BASE}/projects" - svn co http://llvm.org/svn/llvm-project/compiler-rt/branches/release_${LLVM_VERSION_SHORT} compiler-rt - - if [[ ${LLVM_VERSION_SHORT} -gt 37 ]]; then - cd "${LLVM_BASE}/projects" - svn co http://llvm.org/svn/llvm-project/libcxx/branches/release_${LLVM_VERSION_SHORT} libcxx - cd "${LLVM_BASE}/projects" - svn co http://llvm.org/svn/llvm-project/libcxxabi/branches/release_${LLVM_VERSION_SHORT} libcxxabi - fi - - # Apply existing patches if needed - if [ -f "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch" ]; then - cd "${LLVM_BASE}" - patch -p0 -i "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch" - fi -fi - - -# For memory sanitizer, we have a multi-stage build process -if [[ "${SANITIZER_BUILD}" == "memory" ]]; then - if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then - echo "Memory sanitizer builds for <= LLVM 3.7 are not supported" - exit 1 - fi - # Build uninstrumented compiler - mkdir "${SANITIZER_LLVM_UNINSTRUMENTED}" - cd "${SANITIZER_LLVM_UNINSTRUMENTED}" - cmake -GNinja -DCMAKE_BUILD_TYPE=Release "${LLVM_BASE}" - ninja - - # Build instrumented libc/libc++ - mkdir "${SANITIZER_LLVM_LIBCXX}" - cd "${SANITIZER_LLVM_LIBCXX}" - cmake -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo \ - -DLLVM_USE_SANITIZER=MemoryWithOrigins \ - ${SANITIZER_CMAKE_C_COMPILER} \ - ${SANITIZER_CMAKE_CXX_COMPILER} \ - "${LLVM_BASE}" - ninja cxx cxxabi - - # Build instrumented clang - mkdir "${LLVM_BUILD}" - cd "${LLVM_BUILD}" - cmake -GNinja \ - ${SANITIZER_CMAKE_C_COMPILER} \ - ${SANITIZER_CMAKE_CXX_COMPILER} \ - -DCMAKE_C_FLAGS="$SANITIZER_C_FLAGS" \ - -DCMAKE_CXX_FLAGS="$SANITIZER_CXX_FLAGS" \ - -DCMAKE_BUILD_TYPE=Release \ - -DLLVM_USE_SANITIZER=MemoryWithOrigins \ - -DLLVM_ENABLE_LIBCXX=ON \ - -DCMAKE_EXE_LINKER_FLAGS="$SANITIZER_LD_FLAGS" \ - -DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}" \ - "${LLVM_BASE}" - # Build clang as a dependency and install all needed packages - ninja clang - ninja install-clang install-llvm-config install-llvm-objdump \ - install-llvm-link install-llvm-ar install-llvm-nm install-llvm-dis \ - install-clang-headers install-llvm-as installhdrs install-LLVMX86Disassembler \ - install-LLVMX86AsmParser install-LLVMX86CodeGen install-LLVMSelectionDAG \ - install-LLVMAsmPrinter install-LLVMX86Desc install-LLVMMCDisassembler \ - install-LLVMX86Info install-LLVMX86AsmPrinter install-LLVMX86Utils \ - install-LLVMMCJIT install-LLVMExecutionEngine install-LLVMRuntimeDyld \ - install-LLVMipo install-LLVMVectorize install-LLVMLinker install-LLVMIRReader \ - install-LLVMAsmParser install-LLVMCodeGen install-LLVMTarget install-LLVMScalarOpts \ - install-LLVMInstCombine install-LLVMInstrumentation install-LLVMProfileData \ - install-LLVMObject install-LLVMMCParser install-LLVMTransformUtils install-LLVMMC \ - install-LLVMAnalysis install-LLVMBitWriter install-LLVMBitReader install-LLVMCore \ - install-llvm-symbolizer install-LLVMSupport install-lli not FileCheck - cp "${LLVM_BUILD}/bin/FileCheck" "${LLVM_INSTALL}/bin/" - cp "${LLVM_BUILD}/bin/not" "${LLVM_INSTALL}/bin/" - exit 0 -fi - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - # Configure; build; and install - mkdir -p "${LLVM_BUILD}" - cd "${LLVM_BUILD}" - - # Skip building if already finished - if [[ -e "${LLVM_BUILD}/.build_finished" ]]; then - exit 0 - fi - - - # Configure LLVM - if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then - CONFIG=(--enable-jit --prefix="${LLVM_INSTALL}") - if [[ "${ENABLE_OPTIMIZED}" == "1" ]]; then - CONFIG+=(--enable-optimized) - else - CONFIG+=(--disable-optimized) - fi - - if [[ "${DISABLE_ASSERTIONS}" == "1" ]]; then - CONFIG+=(--disable-assertions) - else - CONFIG+=(--enable-assertions) - fi - - if [[ "${ENABLE_DEBUG}" == "1" ]]; then - CONFIG+=(--enable-debug-runtime --enable-debug-symbols) - else - CONFIG+=(--disable-debug-symbols) - fi - CC=${CC} CXX=${CXX} CFLAGS="${LLVM_CFLAGS}" CXXFLAGS="${LLVM_CXXFLAGS}" LDFLAGS="${LLVM_LDFLAGS}" "${LLVM_BASE}/configure" "${CONFIG[@]}" - else - CONFIG=(-DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}") - # cmake build - if [[ "${ENABLE_OPTIMIZED}" == "1" && "${ENABLE_DEBUG}" != "1" ]]; then - CONFIG+=(-DCMAKE_BUILD_TYPE=Release) - fi - if [[ "${ENABLE_OPTIMIZED}" == "1" && "${ENABLE_DEBUG}" == "1" ]]; then - CONFIG+=(-DCMAKE_BUILD_TYPE=RelWithDebInfo) - fi - if [[ "${ENABLE_OPTIMIZED}" != "1" && "${ENABLE_DEBUG}" == "1" ]]; then - CONFIG+=(-DCMAKE_BUILD_TYPE=Debug) - fi - - if [[ "${DISABLE_ASSERTIONS}" == "1" ]]; then - CONFIG+=(-DLLVM_ENABLE_ASSERTIONS=Off) - else - CONFIG+=(-DLLVM_ENABLE_ASSERTIONS=On) - fi - - if [[ ! -z "${LLVM_CFLAGS}" ]] ; then - CONFIG+=(-DCMAKE_C_FLAGS="$LLVM_CFLAGS") - fi - - if [[ ! -z "${LLVM_CXXFLAGS}" ]] ; then - CONFIG+=(-DCMAKE_CXX_FLAGS="$LLVM_CXXFLAGS") - fi - - if [[ ! -z "${LLVM_LDFLAGS}" ]]; then - LDFLAGS="${LLVM_LDFLAGS}" - fi - - cmake "${CONFIG[@]}" "${LLVM_BASE}" - fi - - make -j$(nproc) - make install - - touch "${LLVM_BUILD}/.build_finished" - - cp "${LLVM_BUILD_BIN}/FileCheck" "${LLVM_INSTALL}/bin/" - cp "${LLVM_BUILD_BIN}/not" "${LLVM_INSTALL}/bin/" - - if [[ "${KEEP_BUILD}x" != "1x" ]]; then - rm -rf "${LLVM_BUILD}" - fi - - if [[ "${KEEP_SRC}x" != "1x" ]]; then - rm -rf "${LLVM_BASE}" - fi -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - # Use the brew provided package - brew install "llvm\@${LLVM_VERSION_MAJOR}" -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/scripts/build/p-clang-linux-ubuntu-16.04.inc b/scripts/build/p-clang-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..75023628 --- /dev/null +++ b/scripts/build/p-clang-linux-ubuntu-16.04.inc @@ -0,0 +1,66 @@ +install_binary_artifact_clang() { + local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}" + + # Check versions: no support for LLVM < 3.5 + [[ "${LLVM_VERSION_MAJOR}" -eq 3 ]] && [[ "${LLVM_VERSION_MINOR}" -lt 5 ]] && return 1 + + + local version="" + [[ "${LLVM_VERSION_MAJOR}" -le 6 ]] && version="-${LLVM_VERSION}" + [[ "${LLVM_VERSION_MAJOR}" -ge 7 ]] && version="-${LLVM_VERSION_MAJOR}" + + + if [[ "${LLVM_VERSION_MAJOR}" -eq 3 && "${LLVM_VERSION_MINOR}" -gt 7 ]]; then + # Add certificate + apt update -y + dependencies=( + ca-certificates + wget + ) + + apt -y --no-install-recommends install "${dependencies[@]}" + wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add - + + # Add repository + echo "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial${version} main" >> /etc/apt/sources.list + fi + + apt update -y + dependencies=( + "llvm${version}" + "clang${version}" + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +} + +setup_artifact_variables_clang() { + local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}" + local version="" + [[ "${LLVM_VERSION_MAJOR}" -le 6 ]] && version="-${LLVM_VERSION}" + [[ "${LLVM_VERSION_MAJOR}" -ge 7 ]] && version="-${LLVM_VERSION_MAJOR}" + + # Only set LLVM_CONFIG if not set yet + if [[ -z ${LLVM_CONFIG+x} ]]; then + LLVM_CONFIG=$(which "llvm-config${version}") + fi + + BITCODE_CC=$(which "clang${version}") + BITCODE_CXX=$(which "clang++${version}") + + SANITIZER_C_COMPILER="${BITCODE_CC}" + SANITIZER_CXX_COMPILER="${BITCODE_CXX}" +} + +# Check if the binary artifact is installed +is_installed_clang() { + # Check if llvm-config with the right version exists + which "llvm-config-${LLVM_VERSION}" +} + +get_docker_config_id_clang() { + return 0 +} diff --git a/scripts/build/p-clang-osx.inc b/scripts/build/p-clang-osx.inc new file mode 100644 index 00000000..fde236ca --- /dev/null +++ b/scripts/build/p-clang-osx.inc @@ -0,0 +1,13 @@ +# Package script for LLVM builds OSX +install_binary_artifact_clang () { + # Use the brew provided package + LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + brew install "llvm\@${LLVM_VERSION_MAJOR}" +} + +# Check if the binary artifact is installed +is_installed_clang() { + # Check if llvm-config with the right version exists + LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + [[ -f "/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" ]] +} diff --git a/scripts/build/p-gtest-linux-ubuntu-16.04.inc b/scripts/build/p-gtest-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..f636d321 --- /dev/null +++ b/scripts/build/p-gtest-linux-ubuntu-16.04.inc @@ -0,0 +1,12 @@ +install_build_dependencies_gtest() { + apt update -y + + dependencies=( + ca-certificates + wget + unzip + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +}
\ No newline at end of file diff --git a/scripts/build/p-gtest-osx.inc b/scripts/build/p-gtest-osx.inc new file mode 100644 index 00000000..3fe48e06 --- /dev/null +++ b/scripts/build/p-gtest-osx.inc @@ -0,0 +1,5 @@ +install_build_dependencies_gtest() { + # Install essential dependency + # Ignore if already installed + brew install wget || /usr/bin/true +} diff --git a/scripts/build/p-gtest.inc b/scripts/build/p-gtest.inc new file mode 100644 index 00000000..d4a2d498 --- /dev/null +++ b/scripts/build/p-gtest.inc @@ -0,0 +1,45 @@ +setup_build_variables_gtest() { + GTEST_INSTALL_PATH="${BASE}/googletest-release-${GTEST_VERSION}" + return 0 +} + +download_gtest() { + cd "${BASE}" || exit 1 + wget "https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip" + unzip -o "release-${GTEST_VERSION}.zip" + rm "release-${GTEST_VERSION}.zip" + touch "${GTEST_INSTALL_PATH}"/.is_installed +} + +build_gtest() { + return 0 +} + +install_gtest() { + return 0 +} + +is_installed_gtest() { + ( + setup_build_variables_gtest + [[ -f "${GTEST_INSTALL_PATH}"/.is_installed ]] + ) +} + +get_build_artifacts_gtest() { + ( + setup_build_variables_gtest + echo "${GTEST_INSTALL_PATH}" + ) +} + +setup_artifact_variables_gtest() { + setup_build_variables_gtest +} + +get_docker_config_id_gtest() { + ( + setup_build_variables_gtest + echo "${GTEST_VERSION}" + ) +}
\ No newline at end of file diff --git a/scripts/build/p-klee-linux-ubuntu-16.04.inc b/scripts/build/p-klee-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..b4ba3f33 --- /dev/null +++ b/scripts/build/p-klee-linux-ubuntu-16.04.inc @@ -0,0 +1,21 @@ +install_build_dependencies_klee() { + apt update -y + + dependencies=( + build-essential + cmake + python-pip #for lit + python-setuptools #for lit + python-wheel #for lit + zlib1g-dev + python3 + ) + + if [[ $(to_bool "${COVERAGE}") -eq 1 ]]; then + dependencies+=(lcov curl) + fi + + apt -y --no-install-recommends install "${dependencies[@]}" + + pip install lit +}
\ No newline at end of file diff --git a/scripts/build/build-travis.sh b/scripts/build/p-klee-osx.inc index a2287a2e..2aa5c3e8 100755..100644 --- a/scripts/build/build-travis.sh +++ b/scripts/build/p-klee-osx.inc @@ -1,11 +1,5 @@ -#!/bin/bash -# Build/setup all Travis dependencies if needed -set -e -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - export DOCKER_BUILD_DEPS_ONLY=1 - "${KLEE_SRC_TRAVIS}/scripts/build/build-docker.sh" -elif [[ "$TRAVIS_OS_NAME" == "osx" ]]; then - brew install ccache +# Build dependencies +install_build_dependencies_klee() { set +e brew upgrade python # upgrade to Python 3 brew install python@2 # install Python 2 (OSX version outdated + pip missing) @@ -16,10 +10,5 @@ elif [[ "$TRAVIS_OS_NAME" == "osx" ]]; then ln -s "${py2path}" /usr/local/bin/python ln -s "${pip2path}" /usr/local/bin/pip set -e - pip install lit==0.6.0 - export PATH="/usr/local/opt/ccache/libexec:$PATH" - "${KLEE_SRC_TRAVIS}/scripts/build/install-klee-deps.sh" -else - echo "UNKNOWN OS ${TRAVIS_OS_NAME}" - exit 1 -fi + pip install lit +}
\ No newline at end of file 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 diff --git a/scripts/build/p-llvm-linux-ubuntu-16.04.inc b/scripts/build/p-llvm-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..6bfc3105 --- /dev/null +++ b/scripts/build/p-llvm-linux-ubuntu-16.04.inc @@ -0,0 +1,98 @@ +# Build dependencies +install_build_dependencies_llvm() { + apt update -y + + dependencies=( + build-essential + autoconf + automake + groff + gcc + g++ + python-dev + make + subversion # To check out code + zlib1g-dev + cmake + ) + + if [[ "${SANITIZERS[*]}" == "memory" ]]; then + dependencies+=(ninja-build) + fi + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +} + +install_binary_artifact_llvm() { + local enable_optimized=$(to_bool "${ENABLE_OPTIMIZED}") + local enable_debug=$(to_bool "${ENABLE_DEBUG}") + local disable_assertions=$(to_bool "${DISABLE_ASSERTIONS}") + local requires_rtti=$(to_bool "${REQUIRES_RTTI}") + local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}" + + + # No support for LLVM packages with debug information, incompatible if requested otherwise + [[ "${enable_debug}" -eq 1 ]] && return 1 + + # Packages are build with assertions disabled, incompatible if requested otherwise + [[ "${disable_assertions}" -eq 0 ]] && return 1 + + # Packages are build with RTTI enabled, incompatible if requested otherwise + [[ "${requires_rtti}" -eq 0 ]] && return 1 + + # Enable/Disable optimized does not matter + + # Check versions: no support for LLVM < 3.8 + if [[ "${LLVM_VERSION_MAJOR}" -eq 3 ]]; then + [[ "${LLVM_VERSION_MINOR}" -lt 8 ]] && return 1 + fi + + # Add certificate + apt update -y + dependencies=( + ca-certificates + wget + ) + apt -y --no-install-recommends install "${dependencies[@]}" + wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add - + + local version="" + [[ "${LLVM_VERSION_MAJOR}" -le 6 ]] && version="-${LLVM_VERSION}" + [[ "${LLVM_VERSION_MAJOR}" -ge 7 ]] && version="-${LLVM_VERSION_MAJOR}" + + # Add repository + echo "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial${version} main" >> /etc/apt/sources.list + apt update -y + + dependencies=( + "llvm${version}" + "llvm${version}-dev" + "llvm${version}-runtime" + "clang${version}" + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +} + +# Check if the binary artifact is installed +is_installed_llvm() { + local lc="" + # Check if llvm-config with the right version exists + lc=$(which "llvm-config-${LLVM_VERSION}") + + [[ -z "${lc}" ]] && return 1 + + local rtti + rtti="$(${lc} --has-rtti)" + local assertion + assertion="$(${lc} --assertion-mode)" + local build_mode + build_mode="$(${lc} --build-mode)" + + # Check requested mode with mode of the found item + [[ $(to_bool "${REQUIRES_RTTI}") -eq $(to_bool "${rtti}") ]] || return 1 + [[ $(to_bool "${DISABLE_ASSERTIONS}") -ne $(to_bool "${assertion}") ]] || return 1 +}
\ No newline at end of file diff --git a/scripts/build/p-llvm-linux-ubuntu-18.04.inc b/scripts/build/p-llvm-linux-ubuntu-18.04.inc new file mode 100644 index 00000000..f83112db --- /dev/null +++ b/scripts/build/p-llvm-linux-ubuntu-18.04.inc @@ -0,0 +1,49 @@ +install_build_dependencies_llvm() { + apt update -y + + dependencies=( + build-essential + + autoconf + automake + groff + gcc + g++ + python-dev + make + subversion # Check out code + zlib1g-dev + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +} + +install_binary_artifact_llvm() { + apt update -y + + dependencies=( + "clang-${LLVM_VERSION}" + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +} + +# Check if the binary artifact is installed +is_installed_llvm() { + local lc="" + # Check if llvm-config with the right version exists + lc=$(which "llvm-config-${LLVM_VERSION}") + + local rtti + rtti="$(${lc} --has-rtti)" + local assertion + assertion="$(${lc} --assertion-mode)" + local build_mode + build_mode="$(${lc} --build-mode)" + + # Check requested mode with mode of the found item + [[ $(to_bool "${REQUIRES_RTTI}") -eq $(to_bool "${rtti}") ]] || return 1 + [[ $(to_bool "${DISABLE_ASSERTIONS}") -ne $(to_bool "${assertion}") ]] || return 1 +}
\ No newline at end of file diff --git a/scripts/build/p-llvm-osx.inc b/scripts/build/p-llvm-osx.inc new file mode 100644 index 00000000..05e423f3 --- /dev/null +++ b/scripts/build/p-llvm-osx.inc @@ -0,0 +1,21 @@ +# Package script for LLVM builds OSX +install_binary_artifact_llvm () { + # Use the brew provided package + LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + brew install "llvm\@${LLVM_VERSION_MAJOR}" +} + +# Check if the binary artifact is installed +is_installed_llvm() { + # Check if llvm-config with the right version exists + LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + [[ -f "/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" ]] +} + +setup_artifact_variables_llvm() { + LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + LLVM_CONFIG="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" + BITCODE_CC="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang" + BITCODE_CXX="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang++" + LLVM_INSTALL="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/" +} diff --git a/scripts/build/p-llvm.inc b/scripts/build/p-llvm.inc new file mode 100644 index 00000000..4e0740a2 --- /dev/null +++ b/scripts/build/p-llvm.inc @@ -0,0 +1,366 @@ +validate_build_config_llvm() { + # Check variables that are needed for building + [[ -n "${LLVM_SRC_BASE}" ]] || { echo "LLVM_SRC_BASE not set"; exit 1; } + [[ -n "${LLVM_VERSION_SHORT}" ]] || { echo "LLVM_VERSION_SHORT not set"; exit 1; } +} + +setup_build_variables_llvm() { + LLVM_SUFFIX="" + + local BuildMode="" + local enable_optimized=$(to_bool "${ENABLE_OPTIMIZED}") + local enable_debug=$(to_bool "${ENABLE_DEBUG}") + local disable_assertions=$(to_bool "${DISABLE_ASSERTIONS}") + local requires_rtti=$(to_bool "${REQUIRES_RTTI}") + + if [[ "${enable_optimized}" == "1" ]]; then + LLVM_SUFFIX+="_O" + BuildMode="Release" + else + LLVM_SUFFIX+="_NO" + fi + + if [[ ("${enable_debug}" == "1") || ("${enable_optimized}" != "1") ]]; then + LLVM_SUFFIX+="_D" + [ -z "$BuildMode" ] && BuildMode="Debug" || BuildMode="$BuildMode+Debug" + else + LLVM_SUFFIX+="_ND" + fi + + if [[ "${disable_assertions}" == "1" || -z "${disable_assertions}" ]]; then + LLVM_SUFFIX+="_NA" + else + LLVM_SUFFIX+="_A" + [ -z "$BuildMode" ] && BuildMode="Asserts" || BuildMode="$BuildMode+Asserts" + fi + + if [[ "${requires_rtti}" == "1" ]]; then + LLVM_SUFFIX+="_RTTI" + fi + + if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then + LLVM_SUFFIX+="${SANITIZER_SUFFIX}" + fi + + LLVM_SRC_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}" + LLVM_BUILD="${LLVM_SRC_BASE}-build${LLVM_SUFFIX}" + LLVM_INSTALL="${LLVM_SRC_BASE}-install${LLVM_SUFFIX}" + LLVM_BIN="${LLVM_INSTALL}/bin" + if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then + LLVM_BUILDMODE="$BuildMode" + LLVM_BUILD_BIN="${LLVM_BUILD}/${LLVM_BUILDMODE}/bin" + else + LLVM_BUILD_BIN="${LLVM_BUILD}/bin" + fi + + LLVM_CONFIG="${LLVM_BIN}/llvm-config" + BITCODE_CC="${LLVM_BIN}/clang" + BITCODE_CXX="${LLVM_BIN}/clang++" + + + for sanitizer in "${SANITIZERS[@]}"; do + [[ -z "${sanitizer}" ]] && continue + # Undefined Behaviour Sanitizer + if [ "${sanitizer}" == "memory" ]; then + SANITIZER_LLVM_UNINSTRUMENTED="${LLVM_BUILD}_uninstrumented" + SANITIZER_LLVM_LIBCXX="${LLVM_BUILD}_libcxx" + + SANITIZER_C_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang" + SANITIZER_CXX_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang++" + SANITIZER_CMAKE_C_COMPILER=("-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}") + SANITIZER_CMAKE_CXX_COMPILER=("-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}") + + MSAN_LINK_FLAGS=("-lc++abi" "-Wl,--rpath=${SANITIZER_LLVM_LIBCXX}/lib" "-L${SANITIZER_LLVM_LIBCXX}/lib") + MSAN_FLAGS=("${MSAN_LINK_FLAGS[@]}" -nostdinc++ + -isystem "${SANITIZER_LLVM_LIBCXX}/include" + -isystem "${SANITIZER_LLVM_LIBCXX}/include/c++/v1" + "-fsanitize=memory" + "-fsanitize-memory-track-origins" + -w -fno-omit-frame-pointer -g) + SANITIZER_CXX_FLAGS+=("${MSAN_FLAGS[@]}" "-stdlib=libc++") + SANITIZER_C_FLAGS+=("${MSAN_FLAGS[@]}") + SANITIZER_LD_FLAGS+=("${MSAN_LINK_FLAGS[@]}") + + # Use the uninstrumented compiler + BITCODE_CC="${SANITIZER_C_COMPILER}" + BITCODE_CXX="${SANITIZER_CXX_COMPILER}" + # But point to the instrumented llvm-config + LLVM_CONFIG="${LLVM_BIN}/llvm-config" + continue + fi + # Setup default sanitizer arguments + SANITIZER_C_COMPILER="${LLVM_BIN}/clang" + SANITIZER_CXX_COMPILER="${LLVM_BIN}/clang++" + done +} + +download_llvm() { + # Skip step if we already checked out code + [[ -f "${LLVM_SRC_BASE}/.src_checked_out" ]] && return 0 + + # Checkout LLVM code + svn co "http://llvm.org/svn/llvm-project/llvm/branches/release_${LLVM_VERSION_SHORT}" "${LLVM_SRC_BASE}" + cd "${LLVM_SRC_BASE}/tools" || (echo "Directory does not exist"; exit 1) + svn co "http://llvm.org/svn/llvm-project/cfe/branches/release_${LLVM_VERSION_SHORT}" clang + cd "${LLVM_SRC_BASE}/projects" || (echo "Directory does not exist"; exit 1) + svn co "http://llvm.org/svn/llvm-project/compiler-rt/branches/release_${LLVM_VERSION_SHORT}" compiler-rt + + if [[ ${LLVM_VERSION_SHORT} -gt 37 ]]; then + cd "${LLVM_SRC_BASE}/projects" || (echo "Directory does not exist"; exit 1) + svn co "http://llvm.org/svn/llvm-project/libcxx/branches/release_${LLVM_VERSION_SHORT}" libcxx + cd "${LLVM_SRC_BASE}/projects" || (echo "Directory does not exist"; exit 1) + svn co "http://llvm.org/svn/llvm-project/libcxxabi/branches/release_${LLVM_VERSION_SHORT}" libcxxabi + fi + + # Apply existing patches if needed + if [ -f "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch" ]; then + cd "${LLVM_SRC_BASE}" || (echo "Directory does not exist"; exit 1) + patch -p0 -i "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch" + fi + + touch "${LLVM_SRC_BASE}/.src_checked_out" +} + +build_llvm() { + local enable_optimized=$(to_bool "${ENABLE_OPTIMIZED}") + local enable_debug=$(to_bool "${ENABLE_DEBUG}") + local disable_assertions=$(to_bool "${DISABLE_ASSERTIONS}") + local requires_rtti=$(to_bool "${REQUIRES_RTTI}") + + # For memory sanitizer, we have a multi-stage build process + if [[ "${SANITIZER_BUILD}" == "memory" ]]; then + if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then + echo "Memory sanitizer builds for <= LLVM 3.7 are not supported" + exit 1 + fi + # Build uninstrumented compiler + mkdir -p "${SANITIZER_LLVM_UNINSTRUMENTED}" + cd "${SANITIZER_LLVM_UNINSTRUMENTED}" + cmake -GNinja -DCMAKE_BUILD_TYPE=Release "${LLVM_SRC_BASE}" + ninja + + # Build instrumented libc/libc++ + mkdir -p "${SANITIZER_LLVM_LIBCXX}" + cd "${SANITIZER_LLVM_LIBCXX}" + cmake -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo \ + -DLLVM_USE_SANITIZER=MemoryWithOrigins \ + "${SANITIZER_CMAKE_C_COMPILER}" \ + "${SANITIZER_CMAKE_CXX_COMPILER}" \ + "${LLVM_SRC_BASE}" + ninja cxx cxxabi + + # Build instrumented clang + mkdir -p "${LLVM_BUILD}" + cd "${LLVM_BUILD}" + C_F="${SANITIZER_C_FLAGS[*]}" + CXX_F="${SANITIZER_CXX_FLAGS[*]}" + LD_F="${SANITIZER_LD_FLAGS[*]}" + cmake -GNinja \ + "${SANITIZER_CMAKE_C_COMPILER[*]}" \ + "${SANITIZER_CMAKE_CXX_COMPILER[*]}" \ + -DCMAKE_C_FLAGS="$C_F" \ + -DCMAKE_CXX_FLAGS="${CXX_F}" \ + -DCMAKE_BUILD_TYPE=RelWithDebInfo \ + -DLLVM_ENABLE_ASSERTIONS=On \ + -DLLVM_USE_SANITIZER=MemoryWithOrigins \ + -DLLVM_ENABLE_LIBCXX=ON \ + -DCMAKE_EXE_LINKER_FLAGS="${LD_F}" \ + -DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}" \ + "${LLVM_SRC_BASE}" + # Build clang as a dependency and install all needed packages + ninja clang + return 0 + fi + + # Configure; build; and install + mkdir -p "${LLVM_BUILD}" + cd "${LLVM_BUILD}" + + # Skip building if already finished + [[ -e "${LLVM_BUILD}/.build_finished" ]] && return 0 + + + # Configure LLVM + if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then + local CONFIG=("--enable-jit" "--prefix=${LLVM_INSTALL}") + if [[ "${enable_optimized}" == "1" ]]; then + CONFIG+=(--enable-optimized) + else + CONFIG+=(--disable-optimized) + fi + + if [[ "${disable_assertions}" == "1" ]]; then + CONFIG+=(--disable-assertions) + else + CONFIG+=(--enable-assertions) + fi + + if [[ "${enable_debug}" == "1" ]]; then + CONFIG+=(--enable-debug-runtime --enable-debug-symbols) + else + CONFIG+=(--disable-debug-symbols) + fi + + local variables=() + if [[ -n "${CC:-}" ]]; then + variables+=("CC=${CC}") + fi + + if [[ -n "${CXX:-}" ]]; then + variables+=("CXX=${CXX}") + fi + + if [[ -n "${LDFLAGS:-}" ]]; then + variables+=("LDFLAGS=${LLVM_LDFLAGS}") + fi + + if [[ -n "${LLVM_CFLAGS:-}" ]]; then + variables+=("CFLAGS=${LLVM_CFLAGS}") + fi + + if [[ -n "${LLVM_CXXFLAGS:-}" ]]; then + variables+=("CXXFLAGS=${LLVM_CXXFLAGS}") + fi + + if [[ -n "${LLVM_LDFLAGS:-}" ]]; then + variables+=("LDFLAGS=${LLVM_LDFLAGS}") + fi + ${variables[@]+"${variables[@]}"} "${LLVM_SRC_BASE}/configure" "${CONFIG[@]}" + + else + CONFIG=( + "-DCMAKE_INSTALL_PREFIX=${LLVM_INSTALL}" + "-LLVM_BUILD_LLVM_DYLIB=TRUE" + ) + # cmake build + if [[ "${enable_optimized}" == "1" && "${enable_debug}" != "1" ]]; then + CONFIG+=("-DCMAKE_BUILD_TYPE=Release") + fi + if [[ "${enable_optimized}" == "1" && "${enable_debug}" == "1" ]]; then + CONFIG+=("-DCMAKE_BUILD_TYPE=RelWithDebInfo") + fi + if [[ "${enable_optimized}" != "1" && "${enable_debug}" == "1" ]]; then + CONFIG+=("-DCMAKE_BUILD_TYPE=Debug") + fi + + if [[ "${disable_assertions}" == "1" ]]; then + CONFIG+=("-DLLVM_ENABLE_ASSERTIONS=Off") + else + CONFIG+=("-DLLVM_ENABLE_ASSERTIONS=On") + fi + + if [[ -n "${LLVM_CFLAGS:-}" ]]; then + CONFIG+=("-DCMAKE_C_FLAGS=\"$LLVM_CFLAGS\"") + fi + + if [[ -n "${LLVM_CXXFLAGS:-}" ]]; then + CONFIG+=("-DCMAKE_CXX_FLAGS=\"$LLVM_CXXFLAGS\"") + fi + + if [[ "${requires_rtti}" -eq 1 ]]; then + CONFIG+=("-DLLVM_ENABLE_RTTI=TRUE") + fi + + # Remove unneeded targets + CONFIG+=( + -DLLVM_INCLUDE_EXAMPLES=OFF +# -DLLVM_INCLUDE_TESTS=OFF +# -DCLANG_INCLUDE_TESTS=OFF + -DLLVM_INCLUDE_BENCHMARKS=OFF + -DBUILD_SHARED_LIBS=ON + ) + + local variables=("") + + if [[ -n "${CC:-}" ]]; then + variables+=("CC=${CC}") + fi + + if [[ -n "${CXX:-}" ]]; then + variables+=("CXX=${CXX}") + fi + + if [[ -n "${LDFLAGS:-}" ]]; then + variables+=("LDFLAGS=${LLVM_LDFLAGS}") + fi + + if [[ -n "${variables[*]}" ]]; then + "${variables[*]}" cmake "${CONFIG[@]}" "${LLVM_SRC_BASE}" + else + cmake "${CONFIG[@]}" "${LLVM_SRC_BASE}" + fi + fi + + # Linking LLVM can require a lot of memory. + # First try multicore - if that doesn't work, try single core + (make "-j$(nproc)") || (make) || return 1 + touch "${LLVM_BUILD}/.build_finished" +} + +install_llvm() { + if [[ "${SANITIZER_BUILD}" != "memory" ]]; then + cd "${LLVM_BUILD}" + make "-j$(nproc)" install + cp "${LLVM_BUILD_BIN}/FileCheck" "${LLVM_INSTALL}/bin/" + cp "${LLVM_BUILD_BIN}/not" "${LLVM_INSTALL}/bin/" + + # Remove debug information from binaries + strip "${LLVM_INSTALL}/bin/"* || /bin/true + strip "${LLVM_INSTALL}/lib/libclang"* || /bin/true + strip "${LLVM_INSTALL}/lib/libLTO"* || /bin/true + else + # Handle memory sanitizer install + LLVM_PACKAGES=( \ + install-clang install-llvm-config install-llvm-objdump + install-llvm-link install-llvm-ar install-llvm-nm install-llvm-dis + install-clang-headers install-llvm-as + install-llvm-symbolizer install-LLVMSupport install-lli not FileCheck ) + + if [[ ${LLVM_VERSION_SHORT} -eq 38 ]]; then + LLVM_PACKAGES=("${LLVM_PACKAGES[@]}" installhdrs) + else + LLVM_PACKAGES=("${LLVM_PACKAGES[@]}" install-llvm-headers) + fi + + ninja "${LLVM_PACKAGES[@]}" + + for i in $(ninja -t targets |grep install-LLVM | cut -d : -f 1); do ninja "$i"; done + + cp "${LLVM_BUILD}/bin/FileCheck" "${LLVM_INSTALL}/bin/" + cp "${LLVM_BUILD}/bin/not" "${LLVM_INSTALL}/bin/" + fi + + touch "${LLVM_INSTALL}/.install_finished" +} + +# Check if the binary artifact is installed +is_installed_llvm() { + ( + setup_build_variables_llvm + # Check if the specific llvm-config exists + [[ -f "${LLVM_BUILD_BIN}/llvm-config" ]] + [[ -f "${LLVM_INSTALL}/.install_finished" ]] + ) || return 1 +} + +# Returns a unique id for this configuration +get_docker_config_id_llvm() { + ( + setup_build_variables_llvm + echo "${LLVM_VERSION_SHORT}${LLVM_SUFFIX}" + ) +} + +setup_artifact_variables_llvm() { + setup_build_variables_llvm +} + +get_build_artifacts_llvm() { + ( + setup_build_variables_llvm + echo "${LLVM_INSTALL}" + echo "${LLVM_SRC_BASE}" + [[ "${sanitizer}" == "memory" ]] && echo "${SANITIZER_LLVM_UNINSTRUMENTED}" + [[ "${sanitizer}" == "memory" ]] && echo "${SANITIZER_LLVM_LIBCXX}" + ) +}
\ No newline at end of file diff --git a/scripts/build/p-metasmt-linux-ubuntu-16.04.inc b/scripts/build/p-metasmt-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..063a5cd3 --- /dev/null +++ b/scripts/build/p-metasmt-linux-ubuntu-16.04.inc @@ -0,0 +1,27 @@ +setup_build_variables_metasmt() { + return 0 +} + +install_build_dependencies_metasmt() { + apt update -y + + dependencies=( + # libgmp, gperf (required by yices2) + gperf + libgmp-dev + + build-essential + git + wget + ca-certificates + cmake + zlib1g-dev + bison + flex + unzip + python + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +}
\ No newline at end of file diff --git a/scripts/build/p-metasmt.inc b/scripts/build/p-metasmt.inc new file mode 100644 index 00000000..a0b973a4 --- /dev/null +++ b/scripts/build/p-metasmt.inc @@ -0,0 +1,64 @@ +setup_build_variables_metasmt() { + METASMT_SRC_PATH="${BASE}/metaSMT-${METASMT_VERSION}" + METASMT_BUILD_PATH="${BASE}/metaSMT-${METASMT_VERSION}-build" + METASMT_INSTALL_PATH="${BASE}/metaSMT-${METASMT_VERSION}-install" + METASMT_DEPS_PATH="${BASE}/metaSMT-${METASMT_VERSION}-deps" +} + +download_metasmt() { + # Clone + git clone --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git "${METASMT_SRC_PATH}" + cd "${METASMT_SRC_PATH}" + git submodule update --init + # Bootstrap + git clone https://github.com/agra-uni-bremen/dependencies.git +} + +build_metasmt() { + cd "${METASMT_SRC_PATH}" + ./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off \ + --build stp-git-basic --build boolector-2.2.0 --build minisat-git \ + --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 --build Z3-4.4.1 \ + --build cvc4-1.5 \ + --deps "${METASMT_DEPS_PATH}/" \ + --install "${METASMT_INSTALL_PATH}/" \ + -j "$(nproc)" \ + "${METASMT_BUILD_PATH}" + + # Build + cd "${METASMT_BUILD_PATH}" + make +} + +install_metasmt() { + cd "${METASMT_BUILD_PATH}" + make install + touch "${METASMT_INSTALL_PATH}"/.is_installed +} + +get_docker_config_id_metasmt() { + echo "${METASMT_VERSION}" +} + +# Check if the binary artifact is installed +is_installed_metasmt() { + ( + setup_build_variables_metasmt + [[ -f "${METASMT_INSTALL_PATH}"/.is_installed ]] + ) +} + +get_docker_config_id_metasmt() { + ( + echo "${METASMT_VERSION}" + ) +} + +get_build_artifacts_metasmt() { + ( + setup_build_variables_metasmt + echo "${METASMT_INSTALL_PATH}/" + echo "${METASMT_BUILD_PATH}/" + echo "${METASMT_DEPS_PATH}/" + ) +}
\ No newline at end of file diff --git a/scripts/build/p-stp-linux-ubuntu-16.04.inc b/scripts/build/p-stp-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..f4030023 --- /dev/null +++ b/scripts/build/p-stp-linux-ubuntu-16.04.inc @@ -0,0 +1,19 @@ +#!/bin/bash +# Build dependencies +install_build_dependencies_stp() { + apt update -y + + dependencies=( + build-essential + + bison + ca-certificates + cmake + flex + git + zlib1g-dev + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +}
\ No newline at end of file diff --git a/scripts/build/p-stp-osx.inc b/scripts/build/p-stp-osx.inc new file mode 100644 index 00000000..60214b3c --- /dev/null +++ b/scripts/build/p-stp-osx.inc @@ -0,0 +1,7 @@ +install_build_dependencies_stp() { + dependencies=( + bison + flex + ) + brew install "${dependencies[@]}" +} diff --git a/scripts/build/p-stp.inc b/scripts/build/p-stp.inc new file mode 100644 index 00000000..9bbc90d9 --- /dev/null +++ b/scripts/build/p-stp.inc @@ -0,0 +1,113 @@ +#!/bin/bash +# Build scripts for STP + +# Variables that any artifact of this package might depend on +setup_build_variables_stp() { + STP_SUFFIX="${SANITIZER_SUFFIX}" + + MINISAT_BUILD_PATH="${BASE}/minisat-build${STP_SUFFIX}" + MINISAT_INSTALL_PATH="${BASE}/minisat-install${STP_SUFFIX}" + + STP_BUILD_PATH="${BASE}/stp-${STP_VERSION}-build${STP_SUFFIX}" + STP_INSTALL_PATH="${BASE}/stp-${STP_VERSION}-install${STP_SUFFIX}" + stp_url="https://github.com/stp/stp.git" + + return 0 +} + +download_stp() { + source "${DIR}/common-functions" + # Download minisat + git_clone_or_update https://github.com/stp/minisat "${BASE}/minisat" "master" + + # Download STP + git_clone_or_update "${stp_url}" "${BASE}/stp-${STP_VERSION}" "${STP_VERSION}" +} + +build_stp() { + local CFLAGS="" + local CXXFLAGS="" + local LDFLAGS="" + local cmake_general_args=() + + # Check if sanitizers should be used to build stp + if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then + CFLAGS="${SANITIZER_C_FLAGS[*]}" + CXXFLAGS="${SANITIZER_CXX_FLAGS[*]}" + LDFLAGS="${SANITIZER_LD_FLAGS[*]}" + + cmake_general_args=( + "-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}" + "-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}" + ) + fi + + mkdir -p "${MINISAT_BUILD_PATH}" + cd "${MINISAT_BUILD_PATH}" || return 1 + + local minisat_cmake_args=( + ${cmake_general_args[@]+"${cmake_general_args[@]}"} + "-DCMAKE_INSTALL_PREFIX=${MINISAT_INSTALL_PATH}" + ) + CFLAGS="${CFLAGS}" CXXFLAGS="${CXXFLAGS}" LDFLAGS="${LDFLAGS}" \ + cmake "${minisat_cmake_args[@]}" "${BASE}/minisat" + + # Try to build parallel + make "-j$(nproc)" || make + make install + + mkdir -p "${STP_BUILD_PATH}" + cd "${STP_BUILD_PATH}" || return 1 + + local stp_cmake_args=( + ${cmake_general_args[@]+"${cmake_general_args[@]}"} + # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 + "-DNO_BOOST:BOOL=ON" + "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" + "-DONLY_SIMPLE:BOOL=ON" + "-DCMAKE_PREFIX_PATH=${MINISAT_INSTALL_PATH}" + "-DCMAKE_INSTALL_PREFIX=${STP_INSTALL_PATH}" + ) + + CFLAGS="${CFLAGS}" CXXFLAGS="${CXXFLAGS}" LDFLAGS="${LDFLAGS}" \ + cmake "${stp_cmake_args[@]}" "${BASE}/stp-${STP_VERSION}" + + # Try to build parallel + make "-j$(nproc)" || make + make install + touch "${STP_INSTALL_PATH}/.stp_installed" +} + +install_stp() { + return 0 +} + +# Check if the binary artifact is installed +is_installed_stp() { + ( + setup_build_variables_stp + [[ -f "${STP_INSTALL_PATH}/.stp_installed" ]] + ) || return 1 +} + +setup_artifact_variables_stp() { + setup_build_variables_stp +} + +get_build_artifacts_stp() { + ( + setup_build_variables_stp + echo "${MINISAT_INSTALL_PATH}" + echo "${STP_INSTALL_PATH}" + ) +} + +get_docker_config_id_stp() { + ( + source "${DIR}/common-functions" + setup_build_variables_stp + + stp_remote_commit="$(get_git_hash "${stp_url}" "${STP_VERSION}")" + echo "${stp_remote_commit}${STP_SUFFIX}" + ) +}
\ No newline at end of file diff --git a/scripts/build/p-tcmalloc-linux-ubuntu-16.04.inc b/scripts/build/p-tcmalloc-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..26bf2da9 --- /dev/null +++ b/scripts/build/p-tcmalloc-linux-ubuntu-16.04.inc @@ -0,0 +1,13 @@ +install_build_dependencies_tcmalloc() { + apt update -y + + dependencies=( + build-essential + ca-certificates + cmake + git + wget + ) + + apt -y --no-install-recommends install "${dependencies[@]}" +}
\ No newline at end of file diff --git a/scripts/build/p-tcmalloc.inc b/scripts/build/p-tcmalloc.inc new file mode 100644 index 00000000..00a97626 --- /dev/null +++ b/scripts/build/p-tcmalloc.inc @@ -0,0 +1,49 @@ +setup_build_variables_tcmalloc() { + TCMALLOC_SRC_PATH="${BASE}/gperftools-${TCMALLOC_VERSION}" + TCMALLOC_INSTALL_PATH="${BASE}/tcmalloc-install-${TCMALLOC_VERSION}" + return 0 +} + +download_tcmalloc() { + # Get tcmalloc release + cd "${BASE}" + wget "https://github.com/gperftools/gperftools/releases/download/gperftools-${TCMALLOC_VERSION}/gperftools-${TCMALLOC_VERSION}.tar.gz" + tar xfz "gperftools-${TCMALLOC_VERSION}.tar.gz" +} + +build_tcmalloc() { + cd "${TCMALLOC_SRC_PATH}" + ./configure --disable-dependency-tracking --disable-cpu-profiler \ + --disable-heap-checker --disable-debugalloc --enable-minimal \ + --prefix="${TCMALLOC_INSTALL_PATH}" + make "-j$(nproc)" || make +} + +install_tcmalloc() { + cd "${TCMALLOC_SRC_PATH}" + make install + touch "${TCMALLOC_INSTALL_PATH}"/.is_installed +} + +is_installed_tcmalloc() { + ( + setup_build_variables_tcmalloc + [[ -f "${TCMALLOC_INSTALL_PATH}"/.is_installed ]] + ) || return 1 +} + +setup_artifact_variables_tcmalloc() { + setup_build_variables_tcmalloc +} + + +get_docker_config_id_tcmalloc() { + echo "${TCMALLOC_VERSION}" +} + +get_build_artifacts_tcmalloc() { + ( + setup_build_variables_tcmalloc + echo "${TCMALLOC_INSTALL_PATH}" + ) +}
\ No newline at end of file diff --git a/scripts/build/p-uclibc-linux-ubuntu-16.04.inc b/scripts/build/p-uclibc-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..36bdce58 --- /dev/null +++ b/scripts/build/p-uclibc-linux-ubuntu-16.04.inc @@ -0,0 +1,17 @@ +#!/bin/bash +# Build dependencies +install_build_dependencies_uclibc() { + apt update -y + + dependencies=( + build-essential + ca-certificates + git + python + libncurses5-dev + wget + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +}
\ No newline at end of file diff --git a/scripts/build/p-uclibc.inc b/scripts/build/p-uclibc.inc new file mode 100644 index 00000000..95af9751 --- /dev/null +++ b/scripts/build/p-uclibc.inc @@ -0,0 +1,49 @@ +# Build scripts for uclibc +setup_build_variables_uclibc() { + UCLIBC_PATH="${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" + uclibc_url="https://github.com/klee/klee-uclibc.git" +} + +download_uclibc() { + source "${DIR}/common-functions" + git_clone_or_update "${uclibc_url}" "${UCLIBC_PATH}" "${UCLIBC_VERSION}" +} + +build_uclibc() { + cd "${UCLIBC_PATH}" || return 1 + ./configure --make-llvm-lib --with-cc "${BITCODE_CC}" --with-llvm-config "${LLVM_CONFIG}" + make || return 1 + touch .is_installed +} + +install_uclibc() { + return 0 +} + +# Check if the binary artifact is installed +is_installed_uclibc() { + ( + setup_build_variables_uclibc + [[ -f "${UCLIBC_PATH}"/.is_installed ]] + ) || return 1 +} + +get_docker_config_id_uclibc() { + ( + source "${DIR}/common-functions" + setup_build_variables_uclibc + uclibc_remote_commit="$(get_git_hash "${uclibc_url}" "${UCLIBC_VERSION}")" + echo "${uclibc_remote_commit}_${LLVM_VERSION_SHORT}" + ) +} + +get_build_artifacts_uclibc() { + ( + setup_build_variables_uclibc + echo "${UCLIBC_PATH}" + ) +} + +setup_artifact_variables_uclibc() { + setup_build_variables_uclibc +}
\ No newline at end of file diff --git a/scripts/build/p-z3-linux-ubuntu-16.04.inc b/scripts/build/p-z3-linux-ubuntu-16.04.inc new file mode 100644 index 00000000..2f5e4086 --- /dev/null +++ b/scripts/build/p-z3-linux-ubuntu-16.04.inc @@ -0,0 +1,16 @@ +# Build dependencies Z3 +install_build_dependencies_z3() { + apt update -y + + dependencies=( + build-essential + + python + git + wget + ca-certificates + ) + + #Install essential dependencies + apt -y --no-install-recommends install "${dependencies[@]}" +}
\ No newline at end of file diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc new file mode 100644 index 00000000..bce11aab --- /dev/null +++ b/scripts/build/p-z3-osx.inc @@ -0,0 +1,13 @@ +install_binary_artifact_z3 () { + set +e + brew install python@2 + if [[ "X$?" != "X0" ]]; then + brew link --overwrite python@2 + fi + set -e + brew install z3 +} + +is_installed_z3() { + [[ -f "/usr/local/opt/z3/bin/z3" ]] +}
\ No newline at end of file diff --git a/scripts/build/p-z3.inc b/scripts/build/p-z3.inc new file mode 100644 index 00000000..f6db455b --- /dev/null +++ b/scripts/build/p-z3.inc @@ -0,0 +1,68 @@ +setup_build_variables_z3() { + Z3_SUFFIX="${SANITIZER_SUFFIX}" + Z3_SRC_PATH="${BASE}/z3-${Z3_VERSION}" + Z3_INSTALL_PATH="${BASE}/z3-${Z3_VERSION}-install${Z3_SUFFIX}" +} + +download_z3() { + mkdir -p "${Z3_SRC_PATH}" + cd "${Z3_SRC_PATH}" + wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1 +} + +build_z3() { + local CFLAGS="" + local CXXFLAGS="" + local LDFLAGS="" + local CC="" + local CXX="" + + # Check if sanitizers should be used to build z3 + if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then + CFLAGS="${SANITIZER_C_FLAGS[*]}" + CXXFLAGS="${SANITIZER_CXX_FLAGS[*]}" + LDFLAGS="${SANITIZER_LD_FLAGS[*]}" + + CC="${SANITIZER_C_COMPILER}" + CXX="${SANITIZER_CXX_COMPILER}" + fi + CFLAGS="${CFLAGS}" \ + CXXFLAGS="${CXXFLAGS}" \ + LDFLAGS="${LDFLAGS}" \ + CC="${CC}" \ + CXX="${CXX}" \ + python scripts/mk_make.py --prefix "${Z3_INSTALL_PATH}" -b "build${Z3_SUFFIX}" + cd "build${Z3_SUFFIX}" + make -j$(nproc) || make +} + +install_z3() { + cd "${Z3_SRC_PATH}/build${Z3_SUFFIX}" + make install + touch "${Z3_INSTALL_PATH}"/.is_installed +} + +is_installed_z3() { + ( + setup_build_variables_z3 + [[ -f "${Z3_INSTALL_PATH}"/.is_installed ]] + ) || return 1 +} + +get_build_artifacts_z3() { + ( + setup_build_variables_z3 + echo "${Z3_INSTALL_PATH}" + ) +} + +setup_artifact_variables_z3() { + setup_build_variables_z3 +} + +get_docker_config_id_z3() { + ( + setup_build_variables_z3 + echo "${Z3_VERSION}${Z3_SUFFIX}" + ) +} diff --git a/scripts/build/patches/llvm40.patch b/scripts/build/patches/llvm40.patch new file mode 100644 index 00000000..6cc9fe41 --- /dev/null +++ b/scripts/build/patches/llvm40.patch @@ -0,0 +1,77 @@ +--- ./projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.cc 2018-12-20 22:32:09.636508226 +0000 ++++ ../llvm-40-copy/projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.cc 2018-12-20 22:36:10.752698342 +0000 +@@ -607,8 +607,7 @@ uptr internal_prctl(int option, uptr arg + } + #endif + +-uptr internal_sigaltstack(const struct sigaltstack *ss, +- struct sigaltstack *oss) { ++uptr internal_sigaltstack(const void *ss, void *oss) { + return internal_syscall(SYSCALL(sigaltstack), (uptr)ss, (uptr)oss); + } + +--- ./projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.h 2018-12-20 22:32:10.020508531 +0000 ++++ ../llvm-40-copy/projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.h 2018-12-20 22:36:10.752698342 +0000 +@@ -21,7 +21,6 @@ + #include "sanitizer_platform_limits_posix.h" + + struct link_map; // Opaque type returned by dlopen(). +-struct sigaltstack; + + namespace __sanitizer { + // Dirent structure for getdents(). Note that this structure is different from +@@ -30,8 +29,7 @@ struct linux_dirent; + + // Syscall wrappers. + uptr internal_getdents(fd_t fd, struct linux_dirent *dirp, unsigned int count); +-uptr internal_sigaltstack(const struct sigaltstack* ss, +- struct sigaltstack* oss); ++uptr internal_sigaltstack(const void* ss, void* oss); + uptr internal_sigprocmask(int how, __sanitizer_sigset_t *set, + __sanitizer_sigset_t *oldset); + +--- ./projects/compiler-rt/lib/sanitizer_common/sanitizer_stoptheworld_linux_libcdep.cc 2018-12-20 22:32:09.456508085 +0000 ++++ ../llvm-40-copy/projects/compiler-rt/lib/sanitizer_common/sanitizer_stoptheworld_linux_libcdep.cc 2018-12-20 22:36:10.756698345 +0000 +@@ -275,7 +275,7 @@ static int TracerThread(void* argument) + + // Alternate stack for signal handling. + InternalScopedBuffer<char> handler_stack_memory(kHandlerStackSize); +- struct sigaltstack handler_stack; ++ stack_t handler_stack; + internal_memset(&handler_stack, 0, sizeof(handler_stack)); + handler_stack.ss_sp = handler_stack_memory.data(); + handler_stack.ss_size = kHandlerStackSize; +--- ./projects/compiler-rt/lib/tsan/rtl/tsan_platform_linux.cc 2018-12-20 22:32:15.780513072 +0000 ++++ ../llvm-40-copy/projects/compiler-rt/lib/tsan/rtl/tsan_platform_linux.cc 2018-12-20 22:36:10.756698345 +0000 +@@ -289,7 +289,7 @@ void InitializePlatform() { + int ExtractResolvFDs(void *state, int *fds, int nfd) { + #if SANITIZER_LINUX && !SANITIZER_ANDROID + int cnt = 0; +- __res_state *statp = (__res_state*)state; ++ struct __res_state *statp = (struct __res_state*)state; + for (int i = 0; i < MAXNS && cnt < nfd; i++) { + if (statp->_u._ext.nsaddrs[i] && statp->_u._ext.nssocks[i] != -1) + fds[cnt++] = statp->_u._ext.nssocks[i]; +diff -rup ./projects/libcxx/include/__locale ../llvm-40-copy/projects/libcxx/include/__locale +--- ./projects/libcxx/include/__locale 2018-12-20 22:33:14.484559356 +0000 ++++ ../llvm-40-copy/projects/libcxx/include/__locale 2018-12-20 22:34:34.432622394 +0000 +@@ -34,7 +34,7 @@ + # include <support/solaris/xlocale.h> + #elif defined(_NEWLIB_VERSION) + # include <support/newlib/xlocale.h> +-#elif (defined(__GLIBC__) || defined(__APPLE__) || defined(__FreeBSD__) \ ++#elif (defined(__APPLE__) || defined(__FreeBSD__) \ + || defined(__EMSCRIPTEN__) || defined(__IBMCPP__)) + # include <xlocale.h> + #elif defined(_LIBCPP_HAS_MUSL_LIBC) +--- ./projects/compiler-rt/lib/esan/esan_sideline_linux.cpp 2018-12-20 22:32:12.368510380 +0000 ++++ ../llvm-40-copy/projects/compiler-rt/lib/esan/esan_sideline_linux.cpp 2018-12-21 09:15:03.721823179 +0000 +@@ -70,7 +70,7 @@ int SidelineThread::runSideline(void *Ar + + // Set up a signal handler on an alternate stack for safety. + InternalScopedBuffer<char> StackMap(SigAltStackSize); +- struct sigaltstack SigAltStack; ++ stack_t SigAltStack; + SigAltStack.ss_sp = StackMap.data(); + SigAltStack.ss_size = SigAltStackSize; + SigAltStack.ss_flags = 0; diff --git a/scripts/build/run-coverage.sh b/scripts/build/run-coverage.sh deleted file mode 100755 index ceba8216..00000000 --- a/scripts/build/run-coverage.sh +++ /dev/null @@ -1,25 +0,0 @@ -#!/bin/bash - -set -e - -# We are going to build docker containers -export DOCKER_BUILD=1 - -# All scripts are located relative to this one -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -if [[ "a$COVERAGE" != "a1" ]]; then - exit 0 -fi - -function upload_coverage() { - file=$1 - tags=$2 - ci_env=$(bash <(curl -s https://codecov.io/env)) - docker run ${ci_env} -ti ${REPOSITORY}/klee:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} /bin/bash -c "cd /home/klee/klee_src && bash <(curl -s https://codecov.io/bash) -X gcov -y /home/klee/klee_src/.codecov.yml -f /home/klee/klee_build/coverage_all.info.${file} -F $tags" -} - -# FIXME Enable separated coverage tags again -upload_coverage systemtests systemtests_unittests -upload_coverage unittests systemtests_unittests diff --git a/scripts/build/run-tests.sh b/scripts/build/run-tests.sh new file mode 100755 index 00000000..f39dcad8 --- /dev/null +++ b/scripts/build/run-tests.sh @@ -0,0 +1,153 @@ +#!/bin/bash +set -e +set -u +DIR="$(cd "$(dirname "$0")" && pwd)" + + +coverage_setup() { + local build_dir="$1" + # Zero coverage for any file, e.g. previous tests + lcov -q --directory "${build_dir}" --no-external --zerocounters + # Create a baseline by capturing any file used for compilation, no execution yet + lcov -q --rc lcov_branch_coverage=1 --directory "${build_dir}" --base-directory="${KLEE_SRC}" --no-external --capture --initial --output-file coverage_base.info + lcov -q --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info + lcov -q --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info +} + +coverage_update() { + tags="$2" + codecov_suffix=(${tags// /}) + build_dir="$1" + # Create report + # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped) + lcov -q --rc lcov_branch_coverage=1 --directory "${build_dir}" --base-directory="${KLEE_SRC}" --no-external --capture --output-file coverage.info + # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests) + lcov -q --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info + lcov -q --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info + # Combine baseline and measured coverage + lcov -q --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info."${codecov_suffix}" + # Debug info + lcov -q --rc lcov_branch_coverage=1 --list coverage_all.info."${codecov_suffix}" +} + +run_tests() { + build_dir="$1" + KLEE_SRC="$(cd "${DIR}"/../../ && pwd)" + + # TODO change to pinpoint specific directory + cd "${build_dir}" + + ############################################################################### + # Unit tests + ############################################################################### + # Prepare coverage information if COVERAGE is set + if [ "${COVERAGE}" -eq 1 ]; then + coverage_setup "${build_dir}" + fi + make unittests + + # Generate and upload coverage if COVERAGE is set + if [ "${COVERAGE}" -eq 1 ]; then + coverage_update "${build_dir}" "unittests" + fi + + ############################################################################### + # lit tests + ############################################################################### + if [ "${COVERAGE}" -eq 1 ]; then + coverage_setup "${build_dir}" + fi + make systemtests || return 1 + + # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends + if [ "X${SOLVERS}" == "XmetaSMT" ]; then + available_metasmt_backends="btor stp z3 yices2 cvc4" + for backend in $available_metasmt_backends; do + if [ "X${METASMT_DEFAULT}" != "X$backend" ]; then + if [ "$backend" == "cvc4" ]; then + for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done & + fi + lit -v --param klee_opts=-metasmt-backend="$backend" --param kleaver_opts=-metasmt-backend="$backend" test/ + fi + done + fi + + # Generate and upload coverage if COVERAGE is set + if [ "${COVERAGE}" -eq 1 ]; then + coverage_update "${build_dir}" "systemtests" + fi +} + + + +function upload_coverage() { + file="$1" + tags="$2" + cd /home/klee/klee_src + bash <(curl -s https://codecov.io/bash) -X gcov -R /tmp/klee_src/ -y .codecov.yml -f /home/klee/klee_build/coverage_all.info."${file}" -F "$tags" +} + +function run_docker() { + docker_arguments=(docker run -u root --cap-add SYS_PTRACE -ti) + script_arguments=("--debug" '"/tmp/klee_build"*') + if [[ "${COVERAGE}" -eq 1 ]]; then + script_arguments+=("--coverage") + fi + + if [[ "${UPLOAD_COVERAGE}" -eq 1 ]]; then + docker_arguments+=($(bash <(curl -s https://codecov.io/env))) + script_arguments+=("--upload-coverage") + fi + + # Run the image that was build last with extended capabilities to allow tracing tests + "${docker_arguments[@]}" "$(docker images -q | head -n 1)" /bin/bash -i -c "ulimit -s 16384; source /home/klee/.bashrc; export; /tmp/klee_src/scripts/build/run-tests.sh ${script_arguments[*]}" +} + +main() { + local NAME + NAME=$(basename "${0}") + local RUN_DOCKER=0 + local COVERAGE=0 + local UPLOAD_COVERAGE=0 + local directory="" + + for i in "$@" ;do + case $i in + --debug) + set -x + ;; + --run-docker) + RUN_DOCKER=1 + ;; + --coverage) + COVERAGE=1 + ;; + --upload-coverage) + UPLOAD_COVERAGE=1 + ;; + -*) + echo "${NAME}: unknown argument: $i" + exit 1 + ;; + *) + directory="${i}" + ;; + esac + done + + + if [[ "${RUN_DOCKER}" -eq 1 ]]; then + run_docker "${COVERAGE}" + return 0 + fi + + run_tests "${directory}" + + # FIXME Enable separated coverage tags again + if [[ "${UPLOAD_COVERAGE}" -eq 1 ]]; then + upload_coverage systemtests systemtests_unittests + upload_coverage unittests systemtests_unittests + fi + } + +main "$@"
\ No newline at end of file diff --git a/scripts/build/solver-metasmt.sh b/scripts/build/solver-metasmt.sh deleted file mode 100755 index d8626149..00000000 --- a/scripts/build/solver-metasmt.sh +++ /dev/null @@ -1,39 +0,0 @@ -#!/bin/bash -x -set -e - -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -: ${METASMT_VERSION?"METASMT_VERSION not specified"} - -# Get Z3, libgmp, gperf (required by yices2) -apt update -apt -y --no-install-recommends install gperf libgmp-dev -apt clean -rm -rf /var/lib/apt/lists/* - -# Clone -git clone --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git "${BASE}/metaSMT" -cd "${BASE}/metaSMT" -git submodule update --init - -if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then - echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented" - exit 1 -fi - -# Bootstrap -git clone https://github.com/agra-uni-bremen/dependencies.git -./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off \ - --build stp-git-basic --build boolector-2.2.0 --build minisat-git \ - --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 --build Z3-4.4.1 \ - --build cvc4-1.5 - -# Build -make -C build install - -# Cleanup -if [[ "${STORAGE_SPACE_OPTIMIZED}x" == "1x" ]]; then - rm -rf deps/build - rm -rf deps/cache -fi diff --git a/scripts/build/solver-stp.sh b/scripts/build/solver-stp.sh deleted file mode 100755 index 2e65ca30..00000000 --- a/scripts/build/solver-stp.sh +++ /dev/null @@ -1,57 +0,0 @@ -#!/bin/bash -x - -# TODO: For OSX we can prepare bottled formulas for STP and minisat - -# Make sure we exit if there is a failure -set -e -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -cd ${BASE} -if [ "x${STP_VERSION}" != "x" ]; then - # Build minisat - git_clone_or_update https://github.com/stp/minisat "${BASE}/minisat" - mkdir -p "${BASE}/minisat/build" - cd "${BASE}/minisat/build" - MINISAT_DIR="$(pwd)" - if [[ "$TRAVIS_OS_NAME" == "linux" || "$TRAVIS_OS_NAME" == "osx" ]]; then - CFLAGS="${SANITIZER_C_FLAGS}" \ - CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - LDFLAGS="${SANITIZER_LD_FLAGS}" \ - cmake -DCMAKE_INSTALL_PREFIX="${BASE}/minisat-install" \ - ${SANITIZER_CMAKE_C_COMPILER} \ - ${SANITIZER_CMAKE_CXX_COMPILER} \ - "${BASE}/minisat" - else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 - fi - make - make install - - # Build STP - git_clone_or_update git://github.com/stp/stp.git "${BASE}/stp-${STP_VERSION}" ${STP_VERSION} - mkdir -p "${BASE}/stp-${STP_VERSION}-build" - cd "${BASE}/stp-${STP_VERSION}-build" - - STP_CMAKE_FLAGS=( \ - "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ - -DNO_BOOST:BOOL=ON \ - -DENABLE_PYTHON_INTERFACE:BOOL=OFF \ - ${SANITIZER_CMAKE_C_COMPILER} \ - ${SANITIZER_CMAKE_CXX_COMPILER} \ - ) - # Disabling building of shared libs is a workaround. - # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 - CFLAGS="${SANITIZER_C_FLAGS}" \ - CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - LDFLAGS="${SANITIZER_LD_FLAGS}" \ - cmake ${STP_CMAKE_FLAGS} \ - -DCMAKE_PREFIX_PATH="${BASE}/minisat-install" "${BASE}/stp-${STP_VERSION}" \ - -DCMAKE_INSTALL_PREFIX="${BASE}/stp-${STP_VERSION}-install" - make - make install -else - echo "No STP_VERSION given or empty" - exit 1 -fi diff --git a/scripts/build/solver-z3.sh b/scripts/build/solver-z3.sh deleted file mode 100755 index c6c3381d..00000000 --- a/scripts/build/solver-z3.sh +++ /dev/null @@ -1,34 +0,0 @@ -#!/bin/bash -x - -# Make sure we exit if there is a failure -set -e -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -if [[ -z "${Z3_VERSION}" ]] ; then - echo "Z3_VERSION is not defined" - exit 1 -fi - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - mkdir -p "${BASE}/z3-${Z3_VERSION}" - cd "${BASE}/z3-${Z3_VERSION}" - wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1 - LDFLAGS="${SANITIZER_LD_FLAGS}" \ - CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - python scripts/mk_make.py --prefix "${BASE}/z3-${Z3_VERSION}-install" - cd build - make -j$(nproc) - make install -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - set +e - brew install python@2 - if [[ "X$?" != "X0" ]]; then - brew link --overwrite python@2 - fi - set -e - brew install z3 -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/scripts/build/solvers.sh b/scripts/build/solvers.sh deleted file mode 100755 index 71ad0c2d..00000000 --- a/scripts/build/solvers.sh +++ /dev/null @@ -1,30 +0,0 @@ -#!/bin/bash -x -# Make sure we exit if there is a failure -set -e - -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -: ${SOLVERS?"Solvers must be specified"} -SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g') - -for solver in ${SOLVER_LIST}; do - echo "Getting solver ${solver}" - case ${solver} in - STP) - echo "STP" - "${DIR}/solver-stp.sh" - ;; - Z3) - echo "Z3" - "${DIR}/solver-z3.sh" - ;; - metaSMT) - echo "metaSMT" - "${DIR}/solver-metasmt.sh" - ;; - *) - echo "Unknown solver ${solver}" - exit 1 - esac -done diff --git a/scripts/build/tcmalloc.sh b/scripts/build/tcmalloc.sh deleted file mode 100755 index ea5596d0..00000000 --- a/scripts/build/tcmalloc.sh +++ /dev/null @@ -1,35 +0,0 @@ -#!/bin/bash -x -set -ev - -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - # Get tcmalloc release - if [[ ! -e "${BASE}/gperftools-${TCMALLOC_VERSION}" ]]; then - cd "${BASE}" - wget "https://github.com/gperftools/gperftools/releases/download/gperftools-${TCMALLOC_VERSION}/gperftools-${TCMALLOC_VERSION}.tar.gz" - tar xfz "gperftools-${TCMALLOC_VERSION}.tar.gz" - fi - cd "${BASE}/gperftools-${TCMALLOC_VERSION}" - ./configure --disable-dependency-tracking --disable-cpu-profiler \ - --disable-heap-checker --disable-debugalloc --enable-minimal \ - --prefix="${BASE}/tcmalloc-install" - make - make install - if [[ "${KEEP_BUILD}x" != "1x" ]]; then - rm -rf "${BASE}/gperftools-${TCMALLOC_VERSION}" - fi - - if [[ "${KEEP_SRC}x" != "1x" ]]; then - rm -f "${BASE}/gperftools-${TCMALLOC_VERSION}.tar.gz" - fi -elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then - if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then - echo "Error: Requested to install TCMalloc on macOS, which is not supported" - exit 1 - fi -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi diff --git a/scripts/build/testing-utils.sh b/scripts/build/testing-utils.sh deleted file mode 100755 index 8a855291..00000000 --- a/scripts/build/testing-utils.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/bash -x -# Make sure we exit if there is a failure -set -e - -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -# The New CMake build system just needs the GTest sources regardless -# of LLVM version. -cd "${BASE}" - -wget https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip -unzip -o release-${GTEST_VERSION}.zip -rm release-${GTEST_VERSION}.zip diff --git a/scripts/build/uclibc.sh b/scripts/build/uclibc.sh deleted file mode 100755 index 3440bedb..00000000 --- a/scripts/build/uclibc.sh +++ /dev/null @@ -1,37 +0,0 @@ -#!/bin/bash -x -# Build the uclibc library -# Make sure we exit if there is a failure -set -e -DIR="$(cd "$(dirname "$0")" && pwd)" -source "${DIR}/common-defaults.sh" - -if [[ -z "${KLEE_UCLIBC}" ]]; then - echo "KLEE_UCLIBC must be specified: 0 or branch/tag" - exit 1 -fi - -############################################################################### -# Handling LLVM configuration -############################################################################### -if [[ "$TRAVIS_OS_NAME" = "linux" || "$TRAVIS_OS_NAME" = "osx" ]] ; then - LLVM_CONFIG="${LLVM_BIN}/llvm-config" - KLEE_CC="${LLVM_BIN}/clang" - KLEE_CXX="${LLVM_BIN}/clang++" -else - echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" - exit 1 -fi - -############################################################################### -# klee-uclibc -############################################################################### -if [ "${KLEE_UCLIBC}" != "0" ]; then - if [[ "$TRAVIS_OS_NAME" = "osx" ]] ; then - echo "UCLibc is not supported Mac OSX" - exit 1 - fi - git_clone_or_update git://github.com/klee/klee-uclibc.git "${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" "${KLEE_UCLIBC}" - cd "${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" - ./configure --make-llvm-lib --with-cc ${KLEE_CC} --with-llvm-config ${LLVM_CONFIG} - make -fi diff --git a/scripts/build/v-clang.inc b/scripts/build/v-clang.inc new file mode 100644 index 00000000..16036f22 --- /dev/null +++ b/scripts/build/v-clang.inc @@ -0,0 +1,15 @@ +required_variables_clang=( + "LLVM_VERSION" +) + +artifact_dependency_clang=("sanitizer") + +setup_variables_clang() { + LLVM_VERSION_SHORT="${LLVM_VERSION/./}" +} + +export_variables_clang=( + "LLVM_CONFIG" + "BITCODE_CC" + "BITCODE_CXX" +)
\ No newline at end of file diff --git a/scripts/build/v-gtest.inc b/scripts/build/v-gtest.inc new file mode 100644 index 00000000..a48654f0 --- /dev/null +++ b/scripts/build/v-gtest.inc @@ -0,0 +1,7 @@ +# Build information for gtest +required_variables_gtest=( + "GTEST_VERSION" +) + +# Artifacts gtest depends on +artifact_dependency_gtest=("")
\ No newline at end of file diff --git a/scripts/build/v-klee.inc b/scripts/build/v-klee.inc new file mode 100644 index 00000000..d90892f4 --- /dev/null +++ b/scripts/build/v-klee.inc @@ -0,0 +1,42 @@ +# Build information for KLEE +required_variables_klee=( + "COVERAGE" + "USE_TCMALLOC" +) + +required_variables_check_klee() { + check_bool "COVERAGE" + check_bool "USE_TCMALLOC" +} + +# On which artifacts does KLEE depend on +artifact_dependency_klee(){ + local dependencies=("llvm" "solvers" "gtest") + if [[ "${OS}" != "osx" ]]; then + dependencies+=(uclibc) + fi + + if [[ "${USE_TCMALLOC}" -eq 1 ]]; then + dependencies+=("tcmalloc") + fi + + for d in "${dependencies[@]}"; do + echo "${d}" + done +} + +runtime_artifact_dependency_klee(){ + local dependencies=("") + if [[ "${OS}" != "osx" ]]; then + echo "uclibc" + fi + dependencies+=("llvm" "solvers" "gtest") + + if [[ "${USE_TCMALLOC}" -eq 1 ]]; then + dependencies+=("tcmalloc") + fi + + for d in "${dependencies[@]}"; do + echo "${d}" + done +} diff --git a/scripts/build/v-llvm.inc b/scripts/build/v-llvm.inc new file mode 100644 index 00000000..5ec6f713 --- /dev/null +++ b/scripts/build/v-llvm.inc @@ -0,0 +1,34 @@ +required_variables_llvm=( + "LLVM_VERSION" + "ENABLE_OPTIMIZED" + "ENABLE_DEBUG" + "DISABLE_ASSERTIONS" + "REQUIRES_RTTI" +) + +required_variables_check_llvm() { + check_bool "ENABLE_DEBUG" + check_bool "ENABLE_OPTIMIZED" + check_bool "DISABLE_ASSERTIONS" + check_bool "REQUIRES_RTTI" +} + +export_variables_llvm=( + "LLVM_CONFIG" + "BITCODE_CC" + "BITCODE_CXX" +) + +artifact_dependency_llvm=("sanitizer") + +setup_variables_llvm() { + LLVM_VERSION_SHORT="${LLVM_VERSION/./}" +} + +check_export_variables_llvm() { + # Check for variables set and not empty + [[ -n ${LLVM_CONFIG:-} ]] || (echo "LLVM_CONFIG not set"; exit 1) + [[ -n ${LLVM_INSTALL:-} ]] || (echo "LLVM_INSTALL not set"; exit 1) + [[ -n ${BITCODE_CC:-} ]] || (echo "BITCODE_CC not set"; exit 1) + [[ -n ${BITCODE_CXX:-} ]] || (echo "BITCODE_CXX not set"; exit 1) +}
\ No newline at end of file diff --git a/scripts/build/v-metasmt.inc b/scripts/build/v-metasmt.inc new file mode 100644 index 00000000..362126bb --- /dev/null +++ b/scripts/build/v-metasmt.inc @@ -0,0 +1,7 @@ +# Build information for metaSMT solver +required_variables_metasmt=( + "METASMT_VERSION" + "METASMT_DEFAULT" +) + +artifact_dependency_metasmt=("")
\ No newline at end of file diff --git a/scripts/build/v-sanitizer.inc b/scripts/build/v-sanitizer.inc new file mode 100644 index 00000000..be9b3b39 --- /dev/null +++ b/scripts/build/v-sanitizer.inc @@ -0,0 +1,88 @@ +#!/bin/bash +# Variables for sanitizer handling + +required_variables_sanitizer=( + "SANITIZER_BUILD" +) + +artifact_dependency_sanitizer=("") + +required_variables_check_sanitizer() { + # Allowe empty sanitizer builds + [[ -z "${SANITIZER_BUILD}" ]] && return 0 + + local sanitizers + IFS=":" read -r -a sanitizers <<< "${SANITIZER_BUILD}" + for sanitizer in "${sanitizers[@]}"; do + [[ -z "${sanitizer}" ]] && continue + [[ "${sanitizer}" == "address" ]] && continue + [[ "${sanitizer}" == "memory" ]] && continue + [[ "${sanitizer}" == "undefined" ]] && continue + + echo "Unknown sanitizer: $sanitizer" + exit 1 + done +} + +setup_variables_sanitizer() { + if [[ -z "${SANITIZER_BUILD}" ]]; then + SANITIZERS=("") + SANITIZER_SUFFIX="" + return 0 + fi + # Remove ":" separator + local sanitizers + local e + local sorted_sanitizers + + IFS=":" read -r -a sanitizers <<< "${SANITIZER_BUILD}" + sorted_sanitizers=( $( for e in "${sanitizers[@]}"; do echo "$e"; done | sort) ) + + + # Set variables used by clients. + ## Build variables + [[ -z ${SANITIZER_CXX_FLAGS+x} ]] && SANITIZER_CXX_FLAGS=("") + [[ -z ${SANITIZER_C_FLAGS+x} ]] && SANITIZER_C_FLAGS=("") + [[ -z ${SANITIZER_LD_FLAGS+x} ]] && SANITIZER_LD_FLAGS=("") + + # Docker_suffix + SANITIZER_SUFFIX="" + + local flags + for sanitizer in "${sorted_sanitizers[@]}"; do + [[ -z "${sanitizer}" ]] && continue + # AddressSanitizer + if [ "${sanitizer}" == "address" ]; then + echo "Using ASan" + flags=( "-fsanitize=address" "-fno-omit-frame-pointer" "-g") + SANITIZER_CXX_FLAGS+=("${flags[@]}") + SANITIZER_C_FLAGS+=("${flags[@]}") + SANITIZER_LD_FLAGS+=("${flags[@]}") + SANITIZER_SUFFIX+="_asan" + continue + fi + + # Undefined Behaviour Sanitizer + if [ "${sanitizer}" == "undefined" ]; then + echo "Using UBSan" + flags=("-fsanitize=undefined" "-fno-omit-frame-pointer" "-g") + SANITIZER_CXX_FLAGS+=("${flags[@]}") + SANITIZER_C_FLAGS+=("${flags[@]}") + SANITIZER_LD_FLAGS+=("${flags[@]}" "-lubsan" "-fuse-ld=gold") + SANITIZER_SUFFIX+="_ubsan" + continue + fi + + # Undefined Behaviour Sanitizer + if [ "${sanitizer}" == "memory" ]; then + echo "Using Memory Sanitizer" + SANITIZER_SUFFIX+="_memsan" + continue + fi + + echo "Unknown sanitizer: $sanitizer" + exit 1 + done + + SANITIZERS=("${sorted_sanitizers[@]}") + }
\ No newline at end of file diff --git a/scripts/build/v-sanitizer_compiler.inc b/scripts/build/v-sanitizer_compiler.inc new file mode 100644 index 00000000..e0cf2468 --- /dev/null +++ b/scripts/build/v-sanitizer_compiler.inc @@ -0,0 +1,21 @@ +# Meta-package for solvers +required_variables_sanitizer_compiler=("") + +# On which artifacts does STP depend on +artifact_dependency_sanitizer_compiler(){ + echo "sanitizer" + if [[ -n ${SANITIZER_BUILD+x} ]]; then + [[ "${SANITIZER_BUILD}" == "memory" ]] && echo "llvm" + [[ "${SANITIZER_BUILD}" != "memory" ]] && echo "clang" + fi +} + + +# Setup general variables +setup_variables_sanitizer_compiler() { + for sanitizer in "${SANITIZERS[@]}"; do + [[ -z "${sanitizer}" ]] && continue + SANITIZER_CMAKE_C_COMPILER=[""] + done + +}
\ No newline at end of file diff --git a/scripts/build/v-solvers.inc b/scripts/build/v-solvers.inc new file mode 100644 index 00000000..ad3f43f1 --- /dev/null +++ b/scripts/build/v-solvers.inc @@ -0,0 +1,63 @@ +# Meta-package for solvers +required_variables_solvers=( + "SOLVERS" +) + +required_variables_check_solvers() { + local solvers + IFS=":" read -r -a solvers <<< "${SOLVERS}" + [[ -z "${solvers[@]}" ]] && { echo "SOLVERS can't be empty"; exit 1; } + + for solver in "${solvers[@]}"; do + [[ -z "${solver}" ]] && continue + solver="$(to_lower ${solver})" + + [[ "${solver}" == "z3" ]] && continue + [[ "${solver}" == "stp" ]] && continue + [[ "${solver}" == "metasmt" ]] && continue + + echo "Unknown solver: \"$solver\"" + exit 1 + done +} + +# On which artifacts does SOLVERS depend on +artifact_dependency_solvers() { + # Setup variables first to get selected solvers + setup_variables_solvers + for solver in "${SELECTED_SOLVERS[@]}"; do + echo "${solver}" + done +} + +# On which artifacts does SOLVERS depend on +runtime_artifact_dependency_solvers() { + # Setup variables first to get selected solvers + setup_variables_solvers + for solver in "${SELECTED_SOLVERS[@]}"; do + echo "${solver}" + done +} + +# Setup general variables +setup_variables_solvers() { + local solvers + IFS=":" read -r -a solvers <<< "${SOLVERS}" + + SELECTED_SOLVERS=() + for solver in "${solvers[@]}"; do + [[ -z "${solver}" ]] && continue + solver="$(to_lower ${solver})" + [[ "${solver}" == "z3" ]] && SELECTED_SOLVERS+=("z3") && continue + [[ "${solver}" == "stp" ]] && SELECTED_SOLVERS+=("stp") && continue + [[ "${solver}" == "metasmt" ]] && SELECTED_SOLVERS+=("metasmt") && continue + + echo "Unknown solver: \"$solver\"" + exit 1 + done + + # Sort solvers + SELECTED_SOLVERS=( $( for e in "${SELECTED_SOLVERS[@]}"; do echo "$e"; done | sort|uniq) ) +# TODO Add specific suffix of each solver + SOLVER_SUFFIX=$(IFS=_ ; echo "${SELECTED_SOLVERS[*]}") +}
\ No newline at end of file diff --git a/scripts/build/v-stp.inc b/scripts/build/v-stp.inc new file mode 100644 index 00000000..9bbc28f1 --- /dev/null +++ b/scripts/build/v-stp.inc @@ -0,0 +1,8 @@ +# Build information for STP solver +required_variables_stp=( + "STP_VERSION" + "MINISAT_VERSION" +) + +# On which artifacts does STP depend on +artifact_dependency_stp=("sanitizer_compiler")
\ No newline at end of file diff --git a/scripts/build/v-tcmalloc.inc b/scripts/build/v-tcmalloc.inc new file mode 100644 index 00000000..e49b51c2 --- /dev/null +++ b/scripts/build/v-tcmalloc.inc @@ -0,0 +1,5 @@ +artifact_dependency_tcmalloc=("") + +required_variables_tcmalloc=( + "TCMALLOC_VERSION" +)
\ No newline at end of file diff --git a/scripts/build/v-uclibc.inc b/scripts/build/v-uclibc.inc new file mode 100644 index 00000000..e7a2f720 --- /dev/null +++ b/scripts/build/v-uclibc.inc @@ -0,0 +1,17 @@ +required_variables_uclibc=( + "UCLIBC_VERSION" + "LLVM_VERSION" +) + +artifact_dependency_uclibc(){ + # Add llvm if needed; otherwise only use clang package +# TODO this is quite distribution specific; should be handled in a more general case + local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" + local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}" + # Check versions: no support for LLVM < 3.5 + if [[ "${LLVM_VERSION_MAJOR}" -eq 3 ]]; then + [[ "${LLVM_VERSION_MINOR}" -lt 5 ]] && echo "llvm" + fi + + echo "clang" +}
\ No newline at end of file diff --git a/scripts/build/v-z3.inc b/scripts/build/v-z3.inc new file mode 100644 index 00000000..915336a3 --- /dev/null +++ b/scripts/build/v-z3.inc @@ -0,0 +1,7 @@ +# Build information for Z3 solver +required_variables_z3=( + "Z3_VERSION" +) + +# Artifacts Z3 depends on +artifact_dependency_z3=("sanitizer_compiler")
\ No newline at end of file |