From 17e59a115b98de550d4e4590e55cf18effbc84e5 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 17 Feb 2025 10:07:14 -0500 Subject: [PATCH 1/4] restore file after adding concrete playback test --- tests/script-based-pre/cargo_playback_array/config.yml | 4 ++-- .../{playback_target.expected => playback_array.expected} | 0 .../{playback_target.sh => playback_array.sh} | 2 ++ 3 files changed, 4 insertions(+), 2 deletions(-) rename tests/script-based-pre/cargo_playback_array/{playback_target.expected => playback_array.expected} (100%) rename tests/script-based-pre/cargo_playback_array/{playback_target.sh => playback_array.sh} (90%) diff --git a/tests/script-based-pre/cargo_playback_array/config.yml b/tests/script-based-pre/cargo_playback_array/config.yml index 99bfe39f95a5..88b420e8a6f0 100644 --- a/tests/script-based-pre/cargo_playback_array/config.yml +++ b/tests/script-based-pre/cargo_playback_array/config.yml @@ -1,4 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -script: playback_target.sh -expected: playback_target.expected +script: playback_array.sh +expected: playback_array.expected diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.expected b/tests/script-based-pre/cargo_playback_array/playback_array.expected similarity index 100% rename from tests/script-based-pre/cargo_playback_array/playback_target.expected rename to tests/script-based-pre/cargo_playback_array/playback_array.expected diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.sh b/tests/script-based-pre/cargo_playback_array/playback_array.sh similarity index 90% rename from tests/script-based-pre/cargo_playback_array/playback_target.sh rename to tests/script-based-pre/cargo_playback_array/playback_array.sh index 17eaa66a01c6..d26e340dd60b 100755 --- a/tests/script-based-pre/cargo_playback_array/playback_target.sh +++ b/tests/script-based-pre/cargo_playback_array/playback_array.sh @@ -24,4 +24,6 @@ cargo kani --concrete-playback inplace -Z concrete-playback check_playback -Z concrete-playback cargo clean +# Undo adding the concrete playback test +git restore src/lib.rs popd > /dev/null From 6a0b1d8abac57e5b00f6c32ea3e31f8bd3403ebc Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 17 Feb 2025 14:31:17 -0500 Subject: [PATCH 2/4] use temp file instead of git restore --- .../cargo_playback_array/playback_array.sh | 29 ------------------- .../sample_crate/Cargo.toml | 10 ------- .../src/lib.rs => playback_array/array.rs} | 0 .../config.yml | 0 .../playback_array.expected | 0 .../playback_array/playback_array.sh | 18 ++++++++++++ 6 files changed, 18 insertions(+), 39 deletions(-) delete mode 100755 tests/script-based-pre/cargo_playback_array/playback_array.sh delete mode 100644 tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml rename tests/script-based-pre/{cargo_playback_array/sample_crate/src/lib.rs => playback_array/array.rs} (100%) rename tests/script-based-pre/{cargo_playback_array => playback_array}/config.yml (100%) rename tests/script-based-pre/{cargo_playback_array => playback_array}/playback_array.expected (100%) create mode 100755 tests/script-based-pre/playback_array/playback_array.sh diff --git a/tests/script-based-pre/cargo_playback_array/playback_array.sh b/tests/script-based-pre/cargo_playback_array/playback_array.sh deleted file mode 100755 index d26e340dd60b..000000000000 --- a/tests/script-based-pre/cargo_playback_array/playback_array.sh +++ /dev/null @@ -1,29 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set +e - -function check_playback { - local OUTPUT=output.log - cargo kani playback "${@}" >& $OUTPUT - # Sort output so we can rely on the order. - echo "$(grep "test verify::.* ok" $OUTPUT | sort)" - echo - echo "======= Raw Output =======" - cat $OUTPUT - echo "==========================" - echo - rm $OUTPUT -} - -pushd sample_crate > /dev/null -cargo clean - -cargo kani --concrete-playback inplace -Z concrete-playback -check_playback -Z concrete-playback - -cargo clean -# Undo adding the concrete playback test -git restore src/lib.rs -popd > /dev/null diff --git a/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml deleted file mode 100644 index 202362506011..000000000000 --- a/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -[package] -name = "sample_crate" -version = "0.1.0" -edition = "2021" -doctest = false - -[lints.rust] -unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs b/tests/script-based-pre/playback_array/array.rs similarity index 100% rename from tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs rename to tests/script-based-pre/playback_array/array.rs diff --git a/tests/script-based-pre/cargo_playback_array/config.yml b/tests/script-based-pre/playback_array/config.yml similarity index 100% rename from tests/script-based-pre/cargo_playback_array/config.yml rename to tests/script-based-pre/playback_array/config.yml diff --git a/tests/script-based-pre/cargo_playback_array/playback_array.expected b/tests/script-based-pre/playback_array/playback_array.expected similarity index 100% rename from tests/script-based-pre/cargo_playback_array/playback_array.expected rename to tests/script-based-pre/playback_array/playback_array.expected diff --git a/tests/script-based-pre/playback_array/playback_array.sh b/tests/script-based-pre/playback_array/playback_array.sh new file mode 100755 index 000000000000..78cff27274aa --- /dev/null +++ b/tests/script-based-pre/playback_array/playback_array.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -o pipefail +set -o nounset + +RS_FILE="modified.rs" +cp array.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace + +echo "[TEST] Run test..." +kani playback -Z concrete-playback ${RS_FILE} + +# Cleanup +rm ${RS_FILE} From 4eea90fdb1e55082dd78e1f3684dbef4ec0b175d Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Feb 2025 10:09:36 -0500 Subject: [PATCH 3/4] Apply suggestions from code review Co-authored-by: Michael Tautschnig --- .../script-based-pre/playback_array/playback_array.sh | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/tests/script-based-pre/playback_array/playback_array.sh b/tests/script-based-pre/playback_array/playback_array.sh index 78cff27274aa..507d9babed20 100755 --- a/tests/script-based-pre/playback_array/playback_array.sh +++ b/tests/script-based-pre/playback_array/playback_array.sh @@ -2,9 +2,16 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT +set -e set -o pipefail set -o nounset +cleanup() +{ + rm ${RS_FILE} +} +trap cleanup EXIT + RS_FILE="modified.rs" cp array.rs ${RS_FILE} @@ -13,6 +20,3 @@ kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace echo "[TEST] Run test..." kani playback -Z concrete-playback ${RS_FILE} - -# Cleanup -rm ${RS_FILE} From 0e9906eef58d1b3d201f90769f956e9a68fa348f Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Feb 2025 11:45:31 -0500 Subject: [PATCH 4/4] pipe to true on commands we expect to fail --- tests/script-based-pre/playback_array/playback_array.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/script-based-pre/playback_array/playback_array.sh b/tests/script-based-pre/playback_array/playback_array.sh index 507d9babed20..3cceb8da6297 100755 --- a/tests/script-based-pre/playback_array/playback_array.sh +++ b/tests/script-based-pre/playback_array/playback_array.sh @@ -16,7 +16,7 @@ RS_FILE="modified.rs" cp array.rs ${RS_FILE} echo "[TEST] Generate test..." -kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace || true echo "[TEST] Run test..." -kani playback -Z concrete-playback ${RS_FILE} +kani playback -Z concrete-playback ${RS_FILE} || true