Merge branch 'main' into toolchain-2023-10-19

Cargo.lock

@@ -1256,9 +1256,9 @@ dependencies = [
 
 [[package]]
 name = "tracing"
-version = "0.1.39"
+version = "0.1.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee2ef2af84856a50c1d430afce2fdded0a4ec7eda868db86409b4543df0797f9"
+checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef"
 dependencies = [
  "pin-project-lite",
  "tracing-attributes",

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 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}"

scripts/setup/al2/install_deps.sh

@@ -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

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