diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 88215bdf0317..1837c4cc8a82 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -80,9 +80,6 @@ for testp in "${TESTS[@]}"; do --quiet --no-fail-fast done -# Check codegen for the standard library -time "$SCRIPT_DIR"/std-lib-regression.sh - # We rarely benefit from re-using build artifacts in the firecracker test, # and we often end up with incompatible leftover artifacts: # "error[E0514]: found crate `serde_derive` compiled by an incompatible version of rustc" diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh deleted file mode 100755 index b010da4581f6..000000000000 --- a/scripts/std-lib-regression.sh +++ /dev/null @@ -1,86 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Test for platform -PLATFORM=$(uname -sp) -if [[ $PLATFORM == "Linux x86_64" ]] -then - TARGET="x86_64-unknown-linux-gnu" - # 'env' necessary to avoid bash built-in 'time' - WRAPPER="env time -v" -elif [[ $PLATFORM == "Darwin i386" ]] -then - # Temporarily disabled (in CI) to keeps CI times down - # See https://github.com/model-checking/kani/issues/1578 - exit 0 - - TARGET="x86_64-apple-darwin" - # mac 'time' doesn't have -v - WRAPPER="" -elif [[ $PLATFORM == "Darwin arm" ]] -then - TARGET="aarch64-apple-darwin" - # mac 'time' doesn't have -v - WRAPPER="" -else - echo - echo "Std-Lib codegen regression only works on Linux or OSX x86 platforms, skipping..." - echo - exit 0 -fi - -# Get Kani root -SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" -KANI_DIR=$(dirname "$SCRIPT_DIR") - -echo -echo "Starting Kani codegen for the Rust standard library..." -echo - -cd /tmp -if [ -d std_lib_test ] -then - rm -rf std_lib_test -fi -cargo new std_lib_test --lib -cd std_lib_test - -# Add some content to the rust file including an std function that is non-generic. -echo ' -pub fn main() { - assert!("2021".parse::().unwrap() == 2021); -} -' > src/lib.rs - -# Until we add support to this via our bundle, rebuild the kani library too. -echo " -kani = {path=\"${KANI_DIR}/library/kani\"} -" >> Cargo.toml - -# Use same nightly toolchain used to build Kani -cp ${KANI_DIR}/rust-toolchain.toml . - -echo "Starting cargo build with Kani" -export RUST_BACKTRACE=1 -export RUSTC_LOG=error - -RUST_FLAGS=( - "--kani-compiler" - "-Cpanic=abort" - "-Zalways-encode-mir" - "-Cllvm-args=--backend=cprover" - "-Cllvm-args=--ignore-global-asm" - "-Cllvm-args=--reachability=pub_fns" - "-Cllvm-args=--build-std" -) -export RUSTFLAGS="${RUST_FLAGS[@]}" -export RUSTC="$KANI_DIR/target/kani/bin/kani-compiler" -# Compile rust to iRep -$WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET - -echo -echo "Finished Kani codegen for the Rust standard library successfully..." -echo diff --git a/tests/script-based-pre/std_codegen/codegen_std.expected b/tests/script-based-pre/std_codegen/codegen_std.expected new file mode 100644 index 000000000000..ae155f0ecf44 --- /dev/null +++ b/tests/script-based-pre/std_codegen/codegen_std.expected @@ -0,0 +1,3 @@ +[TEST] Copy standard library from the current toolchain +[TEST] Modify library +------ Build succeeded ------- diff --git a/tests/script-based-pre/std_codegen/codegen_std.sh b/tests/script-based-pre/std_codegen/codegen_std.sh new file mode 100755 index 000000000000..c78b2a3c5f45 --- /dev/null +++ b/tests/script-based-pre/std_codegen/codegen_std.sh @@ -0,0 +1,71 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Test that we can codegen the entire standard library. +# 1. Make a copy of the rust standard library. +# 2. Add a few Kani definitions to it +# 3. Run Kani compiler + +set -e +set -u + +KANI_DIR=$(git rev-parse --show-toplevel) +TMP_DIR="tmp_dir" + +rm -rf ${TMP_DIR} +mkdir ${TMP_DIR} + +cp -r dummy ${TMP_DIR} + +# Create a custom standard library. +echo "[TEST] Copy standard library from the current toolchain" +SYSROOT=$(rustc --print sysroot) +STD_PATH="${SYSROOT}/lib/rustlib/src/rust/library" +cp -r "${STD_PATH}" "${TMP_DIR}" + +# Insert Kani definitions. +CORE_CODE=' +#[cfg(kani)] +kani_core::kani_lib!(core); +' + +echo "[TEST] Modify library" +echo "${CORE_CODE}" >> ${TMP_DIR}/library/core/src/lib.rs + +# Note: Prepending with sed doesn't work on MacOs the same way it does in linux. +# sed -i '1s/^/#![cfg_attr(kani, feature(kani))]\n/' ${TMP_DIR}/library/std/src/lib.rs +cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs +echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs +cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs + +export RUST_BACKTRACE=1 +export RUSTC_LOG=error +export __CARGO_TESTS_ONLY_SRC_ROOT=$(readlink -f ${TMP_DIR})/library +RUST_FLAGS=( + "--kani-compiler" + "-Cpanic=abort" + "-Zalways-encode-mir" + "-Cllvm-args=--backend=cprover" + "-Cllvm-args=--ignore-global-asm" + "-Cllvm-args=--reachability=pub_fns" + "-L${KANI_DIR}/target/kani/no_core/lib" + "--extern=kani_core" + "--cfg=kani" + "-Zcrate-attr=feature(register_tool)" + "-Zcrate-attr=register_tool(kanitool)" +) +export RUSTFLAGS="${RUST_FLAGS[@]}" +export RUSTC="$KANI_DIR/target/kani/bin/kani-compiler" +export KANI_LOGS=kani_compiler::kani_middle=debug +TARGET=$(rustc -vV | awk '/^host/ { print $2 }') + +pushd ${TMP_DIR}/dummy > /dev/null +# Compile the standard library to iRep +cargo build --verbose -Z build-std --lib --target ${TARGET} +popd > /dev/null + +echo "------ Build succeeded -------" + +# Cleanup +rm -r ${TMP_DIR} diff --git a/tests/script-based-pre/std_codegen/config.yml b/tests/script-based-pre/std_codegen/config.yml new file mode 100644 index 000000000000..c5f720824c6e --- /dev/null +++ b/tests/script-based-pre/std_codegen/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: codegen_std.sh +expected: codegen_std.expected diff --git a/tests/script-based-pre/std_codegen/dummy/Cargo.toml b/tests/script-based-pre/std_codegen/dummy/Cargo.toml new file mode 100644 index 000000000000..a6e852d46050 --- /dev/null +++ b/tests/script-based-pre/std_codegen/dummy/Cargo.toml @@ -0,0 +1,9 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "dummy" +version = "0.1.0" +edition = "2021" + +[workspace] diff --git a/tests/script-based-pre/std_codegen/dummy/src/lib.rs b/tests/script-based-pre/std_codegen/dummy/src/lib.rs new file mode 100644 index 000000000000..9349fee3a608 --- /dev/null +++ b/tests/script-based-pre/std_codegen/dummy/src/lib.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Just a dummy file. We are interested in the standard library only + +pub fn void() { + todo!() +}