From 564180dea58245ec1db9d2bab34d92a4e1629583 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Oct 2023 13:40:33 -0400 Subject: [PATCH 1/4] Add scripts for setup in AL2 --- scripts/setup/al2/install_cbmc.sh | 32 ++++++++++++++++++++++++++++ scripts/setup/al2/install_deps.sh | 31 +++++++++++++++++++++++++++ scripts/setup/al2/install_viewer.sh | 19 +++++++++++++++++ scripts/setup/al2/reinstall_cmake.sh | 24 +++++++++++++++++++++ 4 files changed, 106 insertions(+) create mode 100755 scripts/setup/al2/install_cbmc.sh create mode 100755 scripts/setup/al2/install_deps.sh create mode 100755 scripts/setup/al2/install_viewer.sh create mode 100755 scripts/setup/al2/reinstall_cmake.sh diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh new file mode 100755 index 000000000000..39af92e0693b --- /dev/null +++ b/scripts/setup/al2/install_cbmc.sh @@ -0,0 +1,32 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +# Source kani-dependencies to get CBMC_VERSION +source kani-dependencies + +if [ -z "${CBMC_VERSION:-}" ]; then + echo "$0: Error: CBMC_VERSION is not specified" + exit 1 +fi + +# Binaries are not released for AL2, so build from source +WORK_DIR=$(mktemp -d) +git clone \ + --branch develop --depth 1 \ + https://github.com/diffblue/cbmc \ + "${WORK_DIR}" + +pushd "${WORK_DIR}" + +mkdir build +git submodule update --init + +cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" +make -C build -j$(nproc) +sudo make -C build install + +popd +rm -rf "${WORK_DIR}" diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh new file mode 100755 index 000000000000..c9178b6537be --- /dev/null +++ b/scripts/setup/al2/install_deps.sh @@ -0,0 +1,31 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +# Dependencies. +DEPS=( + git + openssl-devel + python3-pip + wget +) + +set -x + +sudo yum -y update +sudo yum -y groupinstall "Development Tools" +sudo yum -y install "${DEPS[@]}" + +# Add Python package dependencies +python3 -m pip install autopep8 + +# Get the directory containing this script +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + +${SCRIPT_DIR}/reinstall_cmake.sh +${SCRIPT_DIR}/install_cbmc.sh +${SCRIPT_DIR}/install_viewer.sh +# The Kissat installation script is platform-independent, so is placed one level up +${SCRIPT_DIR}/../install_kissat.sh diff --git a/scripts/setup/al2/install_viewer.sh b/scripts/setup/al2/install_viewer.sh new file mode 100755 index 000000000000..c8ba7b7b838e --- /dev/null +++ b/scripts/setup/al2/install_viewer.sh @@ -0,0 +1,19 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +# Install cbmc-viewer + +# Source kani-dependencies to get CBMC_VIEWER_VERSION +source kani-dependencies + +if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then + echo "$0: Error: CBMC_VIEWER_VERSION is not specified" + exit 1 +fi + +set -x + +python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION diff --git a/scripts/setup/al2/reinstall_cmake.sh b/scripts/setup/al2/reinstall_cmake.sh new file mode 100755 index 000000000000..b6efa35094ce --- /dev/null +++ b/scripts/setup/al2/reinstall_cmake.sh @@ -0,0 +1,24 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eux + +CMAKE_VERSION="3.27.7" + +# Remove other versions of CMake +sudo yum -y remove cmake + +sudo rm -rf /tmp/cmake_installation +mkdir /tmp/cmake_installation +pushd /tmp/cmake_installation + +wget https://github.com/Kitware/CMake/releases/download/v"${CMAKE_VERSION}"/cmake-"${CMAKE_VERSION}".tar.gz +tar -xzvf cmake-"${CMAKE_VERSION}".tar.gz +cd cmake-"${CMAKE_VERSION}" + +./bootstrap +make -j$(nproc) +sudo make install + +popd \ No newline at end of file From 921b663ca13bcae90a80ef8c230c8c82e6511730 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 23 Oct 2023 11:29:55 -0400 Subject: [PATCH 2/4] Avoid cmake reinstall --- scripts/setup/al2/install_cbmc.sh | 4 ++-- scripts/setup/al2/install_deps.sh | 6 +++++- scripts/setup/al2/reinstall_cmake.sh | 24 ------------------------ 3 files changed, 7 insertions(+), 27 deletions(-) delete mode 100755 scripts/setup/al2/reinstall_cmake.sh diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh index 39af92e0693b..d12045483c1f 100755 --- a/scripts/setup/al2/install_cbmc.sh +++ b/scripts/setup/al2/install_cbmc.sh @@ -24,8 +24,8 @@ pushd "${WORK_DIR}" mkdir build git submodule update --init -cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" -make -C build -j$(nproc) +cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" +cmake3 --build build -- -j$(nproc) sudo make -C build install popd diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh index c9178b6537be..01675fc65774 100755 --- a/scripts/setup/al2/install_deps.sh +++ b/scripts/setup/al2/install_deps.sh @@ -5,7 +5,12 @@ set -eu # Dependencies. +# Note: CMake 3.8 or higher is required to build CBMC, but those versions are +# only available in AWS AMIs through `cmake3`. So we install `cmake3` and use it +# to build CBMC. DEPS=( + cmake + cmake3 git openssl-devel python3-pip @@ -24,7 +29,6 @@ python3 -m pip install autopep8 # Get the directory containing this script SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" -${SCRIPT_DIR}/reinstall_cmake.sh ${SCRIPT_DIR}/install_cbmc.sh ${SCRIPT_DIR}/install_viewer.sh # The Kissat installation script is platform-independent, so is placed one level up diff --git a/scripts/setup/al2/reinstall_cmake.sh b/scripts/setup/al2/reinstall_cmake.sh deleted file mode 100755 index b6efa35094ce..000000000000 --- a/scripts/setup/al2/reinstall_cmake.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eux - -CMAKE_VERSION="3.27.7" - -# Remove other versions of CMake -sudo yum -y remove cmake - -sudo rm -rf /tmp/cmake_installation -mkdir /tmp/cmake_installation -pushd /tmp/cmake_installation - -wget https://github.com/Kitware/CMake/releases/download/v"${CMAKE_VERSION}"/cmake-"${CMAKE_VERSION}".tar.gz -tar -xzvf cmake-"${CMAKE_VERSION}".tar.gz -cd cmake-"${CMAKE_VERSION}" - -./bootstrap -make -j$(nproc) -sudo make install - -popd \ No newline at end of file From 23949e20ed3c5102f818a0a3a6cd1bfc2f0973c1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 23 Oct 2023 13:53:56 -0400 Subject: [PATCH 3/4] Use version branch instead of develop --- scripts/setup/al2/install_cbmc.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh index d12045483c1f..34abcc52db93 100755 --- a/scripts/setup/al2/install_cbmc.sh +++ b/scripts/setup/al2/install_cbmc.sh @@ -15,7 +15,7 @@ fi # Binaries are not released for AL2, so build from source WORK_DIR=$(mktemp -d) git clone \ - --branch develop --depth 1 \ + --branch cbmc-${CBMC_VERSION} --depth 1 \ https://github.com/diffblue/cbmc \ "${WORK_DIR}" From 585be2e1b0b6ea23f27b09d13b7ea2a180228c31 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 23 Oct 2023 14:45:59 -0400 Subject: [PATCH 4/4] Install rustup too --- scripts/setup/al2/install_deps.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh index 01675fc65774..0010aa58bab4 100755 --- a/scripts/setup/al2/install_deps.sh +++ b/scripts/setup/al2/install_deps.sh @@ -33,3 +33,4 @@ ${SCRIPT_DIR}/install_cbmc.sh ${SCRIPT_DIR}/install_viewer.sh # The Kissat installation script is platform-independent, so is placed one level up ${SCRIPT_DIR}/../install_kissat.sh +${SCRIPT_DIR}/../install_rustup.sh