diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d223409e..6277150e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -3,21 +3,54 @@ # by the CI docker runners. image: "binaryanalysisplatform/bap:latest" -# JOB: run the tests for WP. -run_wp_tests: +# Order of job-executions (prevents jobs from running in parallel): +stages: + - build_bildb + - run_unit_tests + - run_integration_tests + +# JOB: build BilDB. +build_bildb: + stage: build_bildb + + tags: + - docker + + script: + - make -C bildb + +# JOB: run unit tests for WP. +run_unit_tests: + stage: run_unit_tests tags: - docker script: - make test -C wp - -# JOB: build BilDB. -build_bildb: + - bash -x bin/unit-tests/run-tests.bash --report-results + +# JOB: run integration tests for WP. +run_integration_tests: + stage: run_integration_tests tags: - docker script: - - make -C bildb + # Install APT dependencies. + - >- + sudo -E apt install -y + qemu gcc-arm-linux-gnueabi binutils-arm-linux-gnueabi cmake + + + # Install other dependencies (non-sudo). + - bash -x bin/setup/install-dependencies.bash --report-results + + # Source environment variables and install cbat tools. + - . bin/common-lib/env.bash + - make -C wp + + - make test -C wp + - bash -x bin/integration-tests/run-tests.bash --report-results diff --git a/bin/common-lib/env.bash b/bin/common-lib/env.bash new file mode 100644 index 00000000..4044d7b6 --- /dev/null +++ b/bin/common-lib/env.bash @@ -0,0 +1,18 @@ +# -------------------------------------------------------------- +# +# This script provides some environment variables +# used for running some of the tools. +# +# -------------------------------------------------------------- + +# Minizinc variables +MINIZINC_URL=https://github.com/MiniZinc/MiniZincIDE/releases/download/2.5.3/MiniZincIDE-2.5.3-bundle-linux-x86_64.tgz +MINIZINC_BUNDLE=MiniZincIDE-2.5.3-bundle-linux-x86_64 +MINIZINC_DIR="${HOME}/${MINIZINC_BUNDLE}" +export PATH="${MINIZINC_DIR}/bin":"${PATH}" +export LD_LIBRARY_PATH="${MINIZINC_DIR}/lib":"${LD_LIBRARY_PATH}" + +# Boolector variables +BOOLECTOR_URL=https://github.com/boolector/boolector +BOOLECTOR_DIR="${HOME}/boolector" +export PATH="${BOOLECTOR_DIR}/build/bin":"${PATH}" diff --git a/bin/common-lib/slack.bash b/bin/common-lib/slack.bash new file mode 100644 index 00000000..7cdac93d --- /dev/null +++ b/bin/common-lib/slack.bash @@ -0,0 +1,96 @@ +# ------------------------------- +# +# Utilities for slack integration +# +# ------------------------------- + +# DESC: Checks if SLACK_USERNAME is defined +# OUTPUT: 0 if SLACK_USERNAME is defined, 1 otherwise +there_is_a_SLACK_USERNAME () { + if [ -z "${SLACK_USERNAME+x}" ]; + then return 1; + else return 0; + fi +} + +# DESC: Checks if SLACK_URL is defined +# OUTPUT: 0 if SLACK_URL is defined, 1 otherwise +there_is_a_SLACK_URL () { + if [ -z "${SLACK_URL}" ]; + then return 1; + else return 0; + fi +} + +# DESC: Creates a payload JSON file. +# ARGS: Takes in ${1} argument that must be "true" in order + # to print full report. +# OUTPUT: The exit code of the attempt to write the file. +build_slack_payload () { + local MESSAGE + local BAP + local BRANCH + local COMMIT + local DATA + local TEXT + local VERBOSE + VERBOSE="${1}" + MESSAGE="$(cat "${MSG_FILE}")" + BAP="$(cat "${BAP_VERSION_FILE}")" + BRANCH="$(cat "${GIT_BRANCH_FILE}")" + COMMIT="$(sed -z -e 's/\n/\\n/g' -e 's/\"/\\"/g' "${GIT_COMMIT_FILE}")" + DATA="$(sed -z \ + -e 's/\n/\\n/g' \ + -e 's/\"/\\"/g' \ + -e 's/'\''/\'\''/g' \ + -e 's/'\`'/'\`'/g' \ + "${REPORT_FILE}")" + TEXT="STATUS: ${MESSAGE}" + TEXT="${TEXT}\nBAP: ${BAP}" + TEXT="${TEXT}\nBRANCH: ${BRANCH}" + TEXT="${TEXT}\nCOMMIT:\n\`\`\`\n${COMMIT}\n\`\`\`" + if [[ "${VERBOSE}" == "true" ]]; then + TEXT="${TEXT}\nOUTPUT:\n\`\`\`\n${DATA}\n\`\`\`" + fi + echo "{ + \"username\":\"${SLACK_USERNAME}\", + \"text\":\"${TEXT}\" + }" > "${SLACK_FILE}" +} + +#DESC: Prints the payload created in build_slack_payload +print_payload () { + echo "printing payload:" + echo "MESSAGE: $(cat "${MSG_FILE}")" + echo "BAP: $(cat "${BAP_VERSION_FILE}")" + echo "BRANCH: $(cat "${GIT_BRANCH_FILE}")" + echo "COMMIT: $(cat "${GIT_COMMIT_FILE}")" + echo "DATA: $(cat "${REPORT_FILE}")" +} + +# DESC: Posts a message to slack +# OUTPUT: The exit code of the curl/POST command +post_to_slack () { + local OUTPUT + local RESULT + OUTPUT="$(curl \ + --http1.1 \ + -X POST \ + -H "Content-Type: application/json" \ + -d @"${SLACK_FILE}" \ + "${SLACK_URL}")" + RESULT=${?} + echo "${OUTPUT}" + return ${RESULT} +} + +# DESC: Reports the current status to slack +# ARGS: Takes in ${1} argument that must be "true" in order + # to print full report. +# OUTPUT: Exit code of the attempt to send status to slack +report_to_slack () { + build_slack_payload "${1}" + print_payload + post_to_slack +} + diff --git a/bin/common-lib/utils.bash b/bin/common-lib/utils.bash new file mode 100644 index 00000000..4ddf4a51 --- /dev/null +++ b/bin/common-lib/utils.bash @@ -0,0 +1,126 @@ +# -------------------------------------------------------------- +# +# This script provides some basic utilities +# (used when running system tests). +# +# --------------------------------------------------------------# DESC +# Check if this script is running with bash +# RETURNS +# - 0 if this script is running with bash +# - 1 if not +is_bash () { + if [ -z "${BASH_VERSION}" ]; + then return 1; + else return 0; + fi +} +# DESC +# Returns the filename of this script +get_me () { + echo "$(basename "${0}")" +} +# DESC +# Prints a help hint +help_hint () { + local ME + ME="$(get_me)" + echo "See ${ME} --help for usage." +} +# DESC +# Constructs a tmp dir for use by this script +# RETURNS +# The tmp dir name +create_tmp_dir () { + local DIR_NAME + local ME + ME="$(get_me)" + DIR_NAME="$(mktemp -d "${TMPDIR:-/tmp/}${ME}.XXXXXXXXXXXX")" + echo "${DIR_NAME}" +} +# Setup tmp dir/files +TMP_SCRATCH_DIR="$(create_tmp_dir)" +MSG_FILE="${TMP_SCRATCH_DIR}/message.txt" +REPORT_FILE="${TMP_SCRATCH_DIR}/report.txt" +SLACK_FILE="${TMP_SCRATCH_DIR}/data.json" +BAP_VERSION_FILE="${TMP_SCRATCH_DIR}/bap-version.txt" +GIT_BRANCH_FILE="${TMP_SCRATCH_DIR}/git-branch.txt" +GIT_COMMIT_FILE="${TMP_SCRATCH_DIR}/git-commit.txt" +echo "Initializing message...no message yet" > "${MSG_FILE}" +echo "Initializing report...nothing to report yet" > "${REPORT_FILE}" +echo '{"username":"None yet","text":"Nothing yet"}' > "${SLACK_FILE}" +echo "No BAP version to report yet" > "${BAP_VERSION_FILE}" +echo "No branch to report yet" > "${GIT_BRANCH_FILE}" +echo "No commit to report yet" > "${GIT_COMMIT_FILE}" + +# DESC +# Get filepath to the REPORT_FILE. +# ARGS +# - 1 : If "true" then return REPORT_FILE. +# Otherwise, return /dev/null. +report_file () { + if [[ "${1}" == "true" ]]; then + echo "${REPORT_FILE}" + else + echo "/dev/null" + fi +} +# DESC +# Record the BAP version +bap_version () { + bap --version > "${BAP_VERSION_FILE}" + echo "BAP_VERSION: $(cat "${BAP_VERSION_FILE}")" +} + +# DESC +# Record the current GIT branch +git_branch () { + git branch > "${GIT_BRANCH_FILE}" + echo "GIT_BRANCH: $(cat "${GIT_BRANCH_FILE}")" + } + +# DESC +# Record the current GIT commit +git_commit () { + git log -1 > "${GIT_COMMIT_FILE}" + if [[ -z "$(cat "${GIT_COMMIT_FILE}")" ]]; then + echo "${CI_COMMIT_MESSAGE}" > "${GIT_COMMIT_FILE}" + if [[ -z "$(cat "${GIT_COMMIT_FILE}")" ]]; then + echo "No commit message could be obtained" > "${GIT_COMMIT_FILE}" + fi + fi + echo -e "GIT_COMMIT:\n$(cat "${GIT_COMMIT_FILE}")" +} + +# DESC +# Cleans up files we've written +clean_up () { + rm -rf "${TMP_SCRATCH_DIR}" +} +# DESC +# Print that we're halting, along with the contents of ${MSG_FILE}. +fail () { + echo "Halting" + echo "$(cat "${MSG_FILE}")" +} +# Ensure we're using Bash. +is_bash +if [ ${?} -ne 0 ]; then + echo "Halting." + echo "This script must be executed with Bash." + return 1 +fi +# Where are we? +THIS_SCRIPT="${BASH_SOURCE[0]}" +COMMON_LIB_DIR="$(cd "$(dirname "${THIS_SCRIPT}")" && pwd)" +# Ensure we can find the root of the repo. +REPO_ROOT="$(cd "${COMMON_LIB_DIR}"/../../ && pwd)" +if [ ! -f "${REPO_ROOT}"/.gitlab-ci.yml ]; then + echo "Halting." + echo "Cannot find the repo root." + echo "Looked in REPO ROOT: '${REPO_ROOT}'" + echo "But could not find a .gitlab-ci.yml file." + exit 1 +fi +# Where these scripts are all kept. +BIN_DIR="${REPO_ROOT}/bin" + diff --git a/bin/integration-tests/run-tests.bash b/bin/integration-tests/run-tests.bash new file mode 100644 index 00000000..5e78849a --- /dev/null +++ b/bin/integration-tests/run-tests.bash @@ -0,0 +1,106 @@ +# ------------------------- +# +# Run the integration tests +# +# ------------------------- + +# Define useful paths +THIS_SCRIPT="${BASH_SOURCE[0]}" +THIS_DIR="$(cd "$(dirname "${THIS_SCRIPT}")" && pwd)" +COMMON_LIB_DIR="$(cd "${THIS_DIR}/../common-lib" && pwd)" + +# Include needed libraries +. "${COMMON_LIB_DIR}/utils.bash" +. "${COMMON_LIB_DIR}/slack.bash" + +# Report progress to slack? +REPORT_PROGRESS="false" + +usage () { + echo "USAGE: bash [OPTIONS]" + echo "" + echo " Run the integration tests." + echo "" + echo "OPTIONS" + echo " -h | --help Print this help and exit" + echo " --report-results Report the results to slack" +} + +# Parse command line arguments +while (( "${#}" )); do + case "${1}" in + + -h|--help) + usage + exit 1 + ;; + + --report-results) + REPORT_RESULTS="true" + ;; + + *) + echo "Unrecognized argument: ${1}" + help_hint + exit 1 + ;; + + esac + shift +done + +# Call `clean up` before the script ends +# When OS throws signal, one is exit. +# When throws exits, catch it, then call cleanup, +# Then rethrow exit +trap clean_up EXIT + +# Ensures we have a slack URL to post with +if [[ "${REPORT_RESULTS}" == "true" ]]; then + there_is_a_SLACK_USERNAME + if [ ${?} -ne 0 ]; then + echo "Halting." + echo "Need a SLACK_USERNAME environment variable." + echo "Export one to proceed." + exit 1 + fi + there_is_a_SLACK_URL + if [ ${?} -ne 0 ]; then + echo "Halting." + echo "Need a SLACK_URL environment variable." + echo "Export one to proceed." + exit 1 + fi +fi + +# Where to record progress +REPORT="$(report_file "${REPORT_RESULTS}")" + +# Record some useful info +bap_version +git_branch +git_commit + +echo "" + +# Prep for the test runs. +make -C "${REPO_ROOT}"/wp clean 2>&1 | tee "${REPORT_FILE}" + +# Run the integration tests. +make -C "${REPO_ROOT}"/wp test.plugin.integration 2>&1 | tee -a "${REPORT_FILE}" +TEST_RESULT="${?}" +echo "REPORT:" +cat "${REPORT_FILE}" +if [[ "${TEST_RESULT}" != "0" ]]; then + echo "Integration tests failed" > "${MSG_FILE}" #summary + if [[ "${REPORT_RESULTS}" == "true" ]]; then + report_to_slack "true" + fi + fail + exit 1 +else + echo "Integration tests passed" > "${MSG_FILE}" + if [[ "${REPORT_RESULTS}" == "true" ]]; then + report_to_slack "false" + fi +fi diff --git a/bin/setup/install-dependencies.bash b/bin/setup/install-dependencies.bash new file mode 100644 index 00000000..3b8ca257 --- /dev/null +++ b/bin/setup/install-dependencies.bash @@ -0,0 +1,131 @@ +# -------------------------------------------------------------- +# +# Install dependencies used by the tools. +# +# -------------------------------------------------------------- + +# Define some paths. +THIS_SCRIPT="${BASH_SOURCE[0]}" +THIS_DIR="$(cd "$(dirname "${THIS_SCRIPT}")" && pwd)" +COMMON_LIB_DIR="$(cd "${THIS_DIR}/../common-lib" && pwd)" + +# Include the relevant libraries. +. "${COMMON_LIB_DIR}/utils.bash" +. "${COMMON_LIB_DIR}/slack.bash" +. "${COMMON_LIB_DIR}/env.bash" + +# Report progress to slack? +REPORT_RESULTS="false" + +# Usage message +usage () { + echo "USAGE: bash $(get_me) [OPTIONS]" + echo "" + echo " Install dependencies for the tools." + echo "" + echo "OPTIONS" + echo " -h | --help Print this help and exit" + echo " --report-results Report the results to slack" +} + +# Parse the command line arguments. +while (( "${#}" )); do + case "${1}" in + + -h|--help) + usage + exit 1 + ;; + + --report-results) + REPORT_RESULTS="true" + ;; + + *) + echo "Unrecognized argument: ${1}" + help_hint + exit 1 + ;; + + esac + shift +done + +# Call `clean_up` before the script exits. +trap clean_up EXIT + +# Ensure we have a slack username and URL to post with. +if [[ "${REPORT_RESULTS}" == "true" ]]; then + there_is_a_SLACK_USERNAME + if [ ${?} -ne 0 ]; then + echo "Halting." + echo "Need a SLACK_USERNAME environment variable." + echo "Export one to proceed." + exit 1 + fi + there_is_a_SLACK_URL + if [ ${?} -ne 0 ]; then + echo "Halting." + echo "Need a SLACK_URL environment variable." + echo "Export one to proceed." + exit 1 + fi +fi + +# Where to record progress. +REPORT="$(report_file "${REPORT_RESULTS}")" + +# Record some useful info. +bap_version +git_commit + +echo "" + +# If boolector isn't already installed, install it. +which boolector > /dev/null 2>&1 +if [[ "${?}" != "0" ]]; then + CURRENT_DIR="$(pwd)" + cd "${HOME}" + if [ -d "${BOOLECTOR_DIR}" ]; then + echo "Can't git pull the boolector repo" > "${MSG_FILE}" + echo "Halting." >> "${REPORT_FILE}" + echo "Want to pull the boolector repo, but can't." >> "${REPORT_FILE}" + echo "${BOOLECTOR_DIR} already exists." >> "${REPORT_FILE}" + echo "$(cat "${MSG_FILE}")" + echo "$(cat "${REPORT_FILE}")" + if [[ "${REPORT_RESULTS}" == "true" ]]; then + report_to_slack + fi + exit 1 + fi + git clone "${BOOLECTOR_URL}" + cd boolector + ./contrib/setup-lingeling.sh + ./contrib/setup-btor2tools.sh + ./configure.sh && cd build && make + cd "${CURRENT_DIR}" +fi + +# Make sure boolector got installed. +which boolector > /dev/null 2>&1 +if [[ "${?}" != "0" ]]; then + echo "Unable to find boolector" > "${MSG_FILE}" + echo "Halting." > "${REPORT_FILE}" + echo "Boolector does not seem to be installed.." >> "${REPORT_FILE}" + echo "Tried 'which boolector' but got nothing." >> "${REPORT_FILE}" + echo "$(cat "${MSG_FILE}")" + echo "$(cat "${REPORT_FILE}")" + if [[ "${REPORT_RESULTS}" == "true" ]]; then + report_to_slack + fi + exit 1 +else + echo "- Boolector is installed." | tee -a "${REPORT_FILE}" +fi + +# Finish up. +echo "Done." | tee -a "${REPORT_FILE}" +if [[ "${REPORT_RESULTS}" == "true" ]]; then + echo "Installed dependencies" > "${MSG_FILE}" + report_to_slack +fi diff --git a/bin/unit-tests/run-tests.bash b/bin/unit-tests/run-tests.bash new file mode 100644 index 00000000..11d74028 --- /dev/null +++ b/bin/unit-tests/run-tests.bash @@ -0,0 +1,106 @@ +# ------------------------- +# +# Run the unit tests +# +# ------------------------- + +# Define useful paths +THIS_SCRIPT="${BASH_SOURCE[0]}" +THIS_DIR="$(cd "$(dirname "${THIS_SCRIPT}")" && pwd)" +COMMON_LIB_DIR="$(cd "${THIS_DIR}/../common-lib" && pwd)" + +# Include needed libraries +. "${COMMON_LIB_DIR}/utils.bash" +. "${COMMON_LIB_DIR}/slack.bash" + +# Report progress to slack? +REPORT_PROGRESS="false" + +usage () { + echo "USAGE: bash [OPTIONS]" + echo "" + echo " Run the unit tests." + echo "" + echo "OPTIONS" + echo " -h | --help Print this help and exit" + echo " --report-results Report the results to slack" +} + +# Parse command line arguments +while (( "${#}" )); do + case "${1}" in + + -h|--help) + usage + exit 1 + ;; + + --report-results) + REPORT_RESULTS="true" + ;; + + *) + echo "Unrecognized argument: ${1}" + help_hint + exit 1 + ;; + + esac + shift +done + +# Call `clean up` before the script ends +# When OS throws signal, one is exit. +# When throws exits, catch it, then call cleanup, +# Then rethrow exit +trap clean_up EXIT + +# Ensures we have a slack URL to post with +if [[ "${REPORT_RESULTS}" == "true" ]]; then + there_is_a_SLACK_USERNAME + if [ ${?} -ne 0 ]; then + echo "Halting." + echo "Need a SLACK_USERNAME environment variable." + echo "Export one to proceed." + exit 1 + fi + there_is_a_SLACK_URL + if [ ${?} -ne 0 ]; then + echo "Halting." + echo "Need a SLACK_URL environment variable." + echo "Export one to proceed." + exit 1 + fi +fi + +# Where to record progress +REPORT="$(report_file "${REPORT_RESULTS}")" + +# Record some useful info +bap_version +git_branch +git_commit + +echo "" + +# Prep for the test runs. +make -C "${REPO_ROOT}"/wp clean 2>&1 | tee "${REPORT_FILE}" + +# Run the unit tests. +make -C "${REPO_ROOT}"/wp test 2>&1 | tee -a "${REPORT_FILE}" +TEST_RESULT="${?}" +echo "REPORT:" +cat "${REPORT_FILE}" +if [[ "${TEST_RESULT}" != "0" ]]; then + echo "Unit tests failed" > "${MSG_FILE}" #summary + if [[ "${REPORT_RESULTS}" == "true" ]]; then + report_to_slack "true" + fi + fail + exit 1 +else + echo "Unit tests passed" > "${MSG_FILE}" + if [[ "${REPORT_RESULTS}" == "true" ]]; then + report_to_slack "false" + fi +fi diff --git a/wp/plugin/tests/integration/test_wp_integration.ml b/wp/plugin/tests/integration/test_wp_integration.ml index f1df6c9e..f8a01900 100644 --- a/wp/plugin/tests/integration/test_wp_integration.ml +++ b/wp/plugin/tests/integration/test_wp_integration.ml @@ -31,7 +31,7 @@ let integration_tests = List.append [ ~checker:(Some (check_list models)))); "Hash function" >: ( - let registers = get_register_args 5 `x86_64 in + let registers = get_register_args 5 X86_target.amd64 in test_plugin "hash_function" sat ~reg_list:(registers |> StringSet.of_list) ~checker:(Some (check_bad_hash_function registers))); diff --git a/wp/plugin/tests/test_libs/test_wp_utils.ml b/wp/plugin/tests/test_libs/test_wp_utils.ml index 1f4d2f5c..b2fefaec 100644 --- a/wp/plugin/tests/test_libs/test_wp_utils.ml +++ b/wp/plugin/tests/test_libs/test_wp_utils.ml @@ -293,9 +293,9 @@ let check_bad_hash_function (registers : string list) : ((string StringMap.t) -> - Short (60.0 s) - Long (600.0 s) - Huge (1800.0 s) - but by default, CBAT uses a custom length of 20.0 seconds. *) + but by default, CBAT uses a custom length of 40.0 seconds. *) let test_plugin - ?length:(length = Custom_length 20.0) + ?length:(length = Custom_length 40.0) ?script:(script = "run_wp.sh") ?args:(args = []) ?reg_list:(reg_list = StringSet.empty)