forked from model-checking/kani
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Ease setup in Amazon Linux 2 (model-checking#2833)
Adds a set of scripts to automate building and installing most dependencies in Amazon Linux 2 environments. This will make it easier to provide ARM64 binaries for Linux (see model-checking#2805). The installation of dependencies isn't minimal but improves our situation w.r.t. AL2. Testing done manually on remote AL2 ARM64 instances, after running this I'm able to run the regression successfully. ### Callouts * Hasn't been tested on AL2 x86.
- Loading branch information
1 parent
dd0379d
commit 9c9c07c
Showing
3 changed files
with
87 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 cbmc-${CBMC_VERSION} --depth 1 \ | ||
https://github.com/diffblue/cbmc \ | ||
"${WORK_DIR}" | ||
|
||
pushd "${WORK_DIR}" | ||
|
||
mkdir build | ||
git submodule update --init | ||
|
||
cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" | ||
cmake3 --build build -- -j$(nproc) | ||
sudo make -C build install | ||
|
||
popd | ||
rm -rf "${WORK_DIR}" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
#!/bin/bash | ||
# Copyright Kani Contributors | ||
# SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
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 | ||
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}/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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |