diff --git a/tests/script-based-pre/cargo_list/list.sh b/tests/script-based-pre/cargo_list/list.sh deleted file mode 100755 index 6b1ab80b0f5f..000000000000 --- a/tests/script-based-pre/cargo_list/list.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Check that the JSON file produced by `cargo kani list` is correct. -# Note that the list.expected file omits the value for "kani-version" -# to avoid having to update the test every time we bump versions. - -cargo kani list -Z list -Z function-contracts --format json -cat "kani-list.json" diff --git a/tests/script-based-pre/cargo_list/Cargo.toml b/tests/script-based-pre/cargo_list_json/Cargo.toml similarity index 100% rename from tests/script-based-pre/cargo_list/Cargo.toml rename to tests/script-based-pre/cargo_list_json/Cargo.toml diff --git a/tests/script-based-pre/cargo_list/config.yml b/tests/script-based-pre/cargo_list_json/config.yml similarity index 100% rename from tests/script-based-pre/cargo_list/config.yml rename to tests/script-based-pre/cargo_list_json/config.yml diff --git a/tests/script-based-pre/cargo_list/list.expected b/tests/script-based-pre/cargo_list_json/list.expected similarity index 100% rename from tests/script-based-pre/cargo_list/list.expected rename to tests/script-based-pre/cargo_list_json/list.expected diff --git a/tests/script-based-pre/cargo_list_json/list.sh b/tests/script-based-pre/cargo_list_json/list.sh new file mode 100755 index 000000000000..a9865f5e6b5d --- /dev/null +++ b/tests/script-based-pre/cargo_list_json/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the json file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) + +# Check that Kani prints the absolute path to kani-list.json +absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.json + exit 0 +else + echo "Test failed: Absolute path to kani-list.json is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/cargo_list/src/lib.rs b/tests/script-based-pre/cargo_list_json/src/lib.rs similarity index 100% rename from tests/script-based-pre/cargo_list/src/lib.rs rename to tests/script-based-pre/cargo_list_json/src/lib.rs diff --git a/tests/script-based-pre/cargo_list/src/standard_harnesses.rs b/tests/script-based-pre/cargo_list_json/src/standard_harnesses.rs similarity index 100% rename from tests/script-based-pre/cargo_list/src/standard_harnesses.rs rename to tests/script-based-pre/cargo_list_json/src/standard_harnesses.rs diff --git a/tests/script-based-pre/cargo_list_md/Cargo.toml b/tests/script-based-pre/cargo_list_md/Cargo.toml new file mode 100644 index 000000000000..2f213d2fccd7 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_list" +version = "0.1.0" +edition = "2021" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/kani_list/config.yml b/tests/script-based-pre/cargo_list_md/config.yml similarity index 100% rename from tests/script-based-pre/kani_list/config.yml rename to tests/script-based-pre/cargo_list_md/config.yml diff --git a/tests/script-based-pre/cargo_list_md/kani-list.md b/tests/script-based-pre/cargo_list_md/kani-list.md new file mode 100644 index 000000000000..9e913345e664 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/kani-list.md @@ -0,0 +1,14 @@ + +Contracts: +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----------------------------- | -------------------------------------------------------------- | +| | example::implementation::bar | example::verify::check_bar | +| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | example::implementation::func | example::verify::check_func | +| | example::prep::parse | NONE | +| Total | 4 | 4 | + + +Standard Harnesses (#[kani::proof]): +1. standard_harnesses::example::verify::check_modify +2. standard_harnesses::example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/cargo_list_md/list.expected b/tests/script-based-pre/cargo_list_md/list.expected new file mode 100644 index 000000000000..9e913345e664 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/list.expected @@ -0,0 +1,14 @@ + +Contracts: +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----------------------------- | -------------------------------------------------------------- | +| | example::implementation::bar | example::verify::check_bar | +| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | example::implementation::func | example::verify::check_func | +| | example::prep::parse | NONE | +| Total | 4 | 4 | + + +Standard Harnesses (#[kani::proof]): +1. standard_harnesses::example::verify::check_modify +2. standard_harnesses::example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/cargo_list_md/list.sh b/tests/script-based-pre/cargo_list_md/list.sh new file mode 100755 index 000000000000..e35c4835c42e --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the MD file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) + +# Check that Kani prints the absolute path to kani-list.md +absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.md + exit 0 +else + echo "Test failed: Absolute path to kani-list.md is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/cargo_list_md/src/lib.rs b/tests/script-based-pre/cargo_list_md/src/lib.rs new file mode 100644 index 000000000000..e7382a9124a3 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/src/lib.rs @@ -0,0 +1,68 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test replicates the module structure from the running example in the list RFC. +//! It ensures that the list command works across modules, and with modifies clauses, history expressions, and generic functions. + +mod standard_harnesses; + +#[cfg(kani)] +mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + pub mod implementation { + #[kani::requires(*x < 4)] + #[kani::requires(*x > 2)] + #[kani::ensures(|_| old(*x - 1) == *x)] + #[kani::ensures(|_| *x == 4)] + #[kani::modifies(x)] + pub fn bar(x: &mut u32) { + *x += 1; + } + + #[kani::requires(*x < 100)] + #[kani::modifies(x)] + pub fn func(x: &mut i32) { + *x *= 1; + } + + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x + } + } + + mod verify { + use crate::example::implementation; + + #[kani::proof_for_contract(implementation::bar)] + fn check_bar() { + let mut x = 7; + implementation::bar(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u32() { + let mut x: u32 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u64() { + let mut x: u64 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::func)] + fn check_func() { + let mut x = 7; + implementation::func(&mut x); + } + } +} diff --git a/tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs b/tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs new file mode 100644 index 000000000000..5df490461d0c --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test that the cargo list command can find Kani attributes across multiple files. + +#[cfg(kani)] +mod example { + mod verify { + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +} diff --git a/tests/script-based-pre/kani_list/list.sh b/tests/script-based-pre/kani_list/list.sh deleted file mode 100755 index e7bb6f081044..000000000000 --- a/tests/script-based-pre/kani_list/list.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Check that the JSON file produced by `kani list` is correct. -# Note that the list.expected file omits the value for "kani-version" -# to avoid having to update the test every time we bump versions. - -kani list -Z list -Z function-contracts src/lib.rs --format json -cat "kani-list.json" diff --git a/tests/script-based-pre/kani_list_json/config.yml b/tests/script-based-pre/kani_list_json/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/kani_list_json/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: list.sh +expected: list.expected diff --git a/tests/script-based-pre/kani_list/list.expected b/tests/script-based-pre/kani_list_json/list.expected similarity index 100% rename from tests/script-based-pre/kani_list/list.expected rename to tests/script-based-pre/kani_list_json/list.expected diff --git a/tests/script-based-pre/kani_list_json/list.sh b/tests/script-based-pre/kani_list_json/list.sh new file mode 100755 index 000000000000..a70938ffcea9 --- /dev/null +++ b/tests/script-based-pre/kani_list_json/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the JSON file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) + +# Check that Kani prints the absolute path to kani-list.json +absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.json + exit 0 +else + echo "Test failed: Absolute path to kani-list.json is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/kani_list/src/lib.rs b/tests/script-based-pre/kani_list_json/src/lib.rs similarity index 100% rename from tests/script-based-pre/kani_list/src/lib.rs rename to tests/script-based-pre/kani_list_json/src/lib.rs diff --git a/tests/script-based-pre/kani_list_md/.gitignore b/tests/script-based-pre/kani_list_md/.gitignore new file mode 100644 index 000000000000..3d32673cae4b --- /dev/null +++ b/tests/script-based-pre/kani_list_md/.gitignore @@ -0,0 +1 @@ +kani-list.md \ No newline at end of file diff --git a/tests/script-based-pre/kani_list_md/config.yml b/tests/script-based-pre/kani_list_md/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/kani_list_md/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: list.sh +expected: list.expected diff --git a/tests/script-based-pre/kani_list_md/list.expected b/tests/script-based-pre/kani_list_md/list.expected new file mode 100644 index 000000000000..eb4ca335d678 --- /dev/null +++ b/tests/script-based-pre/kani_list_md/list.expected @@ -0,0 +1,14 @@ + +Contracts: +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----------------------------- | -------------------------------------------------------------- | +| | example::implementation::bar | example::verify::check_bar | +| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | example::implementation::func | example::verify::check_func | +| | example::prep::parse | NONE | +| Total | 4 | 4 | + + +Standard Harnesses (#[kani::proof]): +1. example::verify::check_modify +2. example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/kani_list_md/list.sh b/tests/script-based-pre/kani_list_md/list.sh new file mode 100755 index 000000000000..e35c4835c42e --- /dev/null +++ b/tests/script-based-pre/kani_list_md/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the MD file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) + +# Check that Kani prints the absolute path to kani-list.md +absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.md + exit 0 +else + echo "Test failed: Absolute path to kani-list.md is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/kani_list_md/src/lib.rs b/tests/script-based-pre/kani_list_md/src/lib.rs new file mode 100644 index 000000000000..69dbba5a9e0f --- /dev/null +++ b/tests/script-based-pre/kani_list_md/src/lib.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test replicates the module structure from the running example in the list RFC. +//! It ensures that the list command across modules, and with modifies clauses, history expressions, and generic functions. + +mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + pub mod implementation { + #[kani::requires(*x < 4)] + #[kani::requires(*x > 2)] + #[kani::ensures(|_| old(*x - 1) == *x)] + #[kani::ensures(|_| *x == 4)] + #[kani::modifies(x)] + pub fn bar(x: &mut u32) { + *x += 1; + } + + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x + } + + #[kani::requires(*x < 100)] + #[kani::modifies(x)] + pub fn func(x: &mut i32) { + *x *= 1; + } + } + + mod verify { + use crate::example::implementation; + + #[kani::proof_for_contract(implementation::bar)] + fn check_bar() { + let mut x = 7; + implementation::bar(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u32() { + let mut x: u32 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u64() { + let mut x: u64 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::func)] + fn check_func() { + let mut x = 7; + implementation::func(&mut x); + } + + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +}