From c5d771de01b652b018e6ad9f4af9e0b56f726a00 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 6 Jun 2025 08:10:20 -0700 Subject: [PATCH 1/5] put quantifiers to unstable --- .../src/codegen_cprover_gotoc/overrides/hooks.rs | 3 +++ kani_metadata/src/unstable.rs | 2 ++ library/kani_core/src/lib.rs | 10 ++++++++++ 3 files changed, 15 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 6c6319baf4eb..3b62f4707f67 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -817,6 +817,9 @@ fn handle_quantifier( span: Span, quantifier_kind: QuantifierKind, ) -> Stmt { + if gcx.queries.args().unstable_features.contains(&"loop-contracts".to_string()) { + panic!("Unstable feature Quantifier is not enable") + } let loc = gcx.codegen_span_stable(span); let target = target.unwrap(); let lower_bound = &fargs[0]; diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 65fd0c9a0716..b08b18a0167c 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -106,6 +106,8 @@ pub enum UnstableFeature { /// Automatically check that no invalid value is produced which is considered UB in Rust. /// Note that this does not include checking uninitialized value. ValidValueChecks, + /// Enable quantifiers + Quantifiers, } impl UnstableFeature { diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index fcff99c32f80..ce484dde6d41 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -627,6 +627,11 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } + #[crate::kani::unstable_feature( + feature = "quantifiers", + issue = 4134, + reason = "experimental quantifiers" + )] #[inline(never)] #[kanitool::fn_marker = "ForallHook"] pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool @@ -636,6 +641,11 @@ macro_rules! kani_intrinsics { predicate(lower_bound) } + #[crate::kani::unstable_feature( + feature = "quantifiers", + issue = 4134, + reason = "experimental quantifiers" + )] #[inline(never)] #[kanitool::fn_marker = "ExistsHook"] pub fn kani_exists(lower_bound: T, upper_bound: T, predicate: F) -> bool From 3b5408535f31ae2d85aa6ccb747f947a92b78599 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 6 Jun 2025 08:10:55 -0700 Subject: [PATCH 2/5] add flag to tests --- tests/expected/quantifiers/assert_with_exists_fail.rs | 1 + tests/expected/quantifiers/assert_with_exists_pass.rs | 1 + tests/expected/quantifiers/assert_with_forall_fail.rs | 1 + tests/expected/quantifiers/assert_with_forall_pass.rs | 1 + tests/expected/quantifiers/assume_with_exists_fail.rs | 1 + tests/expected/quantifiers/contracts_fail.rs | 2 +- .../quantifiers/quantifier_with_no_external_variable.rs | 2 +- tests/kani/Quantifiers/array.rs | 1 + tests/kani/Quantifiers/contracts.rs | 2 +- tests/kani/Quantifiers/even.rs | 1 + tests/kani/Quantifiers/from_raw_part_fixme.rs | 1 + tests/kani/Quantifiers/no_array.rs | 1 + 12 files changed, 12 insertions(+), 3 deletions(-) diff --git a/tests/expected/quantifiers/assert_with_exists_fail.rs b/tests/expected/quantifiers/assert_with_exists_fail.rs index 3e2c6cdb3781..20a2aa8934b0 100644 --- a/tests/expected/quantifiers/assert_with_exists_fail.rs +++ b/tests/expected/quantifiers/assert_with_exists_fail.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn exists_assert_harness() { diff --git a/tests/expected/quantifiers/assert_with_exists_pass.rs b/tests/expected/quantifiers/assert_with_exists_pass.rs index 7d43d6117729..c364a968610c 100644 --- a/tests/expected/quantifiers/assert_with_exists_pass.rs +++ b/tests/expected/quantifiers/assert_with_exists_pass.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn exists_assert_harness() { diff --git a/tests/expected/quantifiers/assert_with_forall_fail.rs b/tests/expected/quantifiers/assert_with_forall_fail.rs index c9bb7bbf62dd..ec2cab5c4e98 100644 --- a/tests/expected/quantifiers/assert_with_forall_fail.rs +++ b/tests/expected/quantifiers/assert_with_forall_fail.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn forall_assert_harness() { diff --git a/tests/expected/quantifiers/assert_with_forall_pass.rs b/tests/expected/quantifiers/assert_with_forall_pass.rs index 5ebf73e7c0ee..1ba7d93053ff 100644 --- a/tests/expected/quantifiers/assert_with_forall_pass.rs +++ b/tests/expected/quantifiers/assert_with_forall_pass.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn forall_assert_harness() { diff --git a/tests/expected/quantifiers/assume_with_exists_fail.rs b/tests/expected/quantifiers/assume_with_exists_fail.rs index f6df36a6942d..0148ac991304 100644 --- a/tests/expected/quantifiers/assume_with_exists_fail.rs +++ b/tests/expected/quantifiers/assume_with_exists_fail.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn exists_assume_harness() { diff --git a/tests/expected/quantifiers/contracts_fail.rs b/tests/expected/quantifiers/contracts_fail.rs index a1b87ebc8633..022188f46d95 100644 --- a/tests/expected/quantifiers/contracts_fail.rs +++ b/tests/expected/quantifiers/contracts_fail.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts +// kani-flags: -Zfunction-contracts -Z quantifiers /// Copy only first 7 elements and left the last one unchanged. #[kani::ensures(|ret| { unsafe{ diff --git a/tests/expected/quantifiers/quantifier_with_no_external_variable.rs b/tests/expected/quantifiers/quantifier_with_no_external_variable.rs index dabf4d9f2137..f0c8a84362b7 100644 --- a/tests/expected/quantifiers/quantifier_with_no_external_variable.rs +++ b/tests/expected/quantifiers/quantifier_with_no_external_variable.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT - +// kani-flags: -Z quantifiers /// Quantifier with no external variable in the closure #[kani::proof] diff --git a/tests/kani/Quantifiers/array.rs b/tests/kani/Quantifiers/array.rs index b59eccd614fb..b077d53fd6da 100644 --- a/tests/kani/Quantifiers/array.rs +++ b/tests/kani/Quantifiers/array.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn vec_assert_forall_harness() { diff --git a/tests/kani/Quantifiers/contracts.rs b/tests/kani/Quantifiers/contracts.rs index d8e36c194774..7df87d2996b9 100644 --- a/tests/kani/Quantifiers/contracts.rs +++ b/tests/kani/Quantifiers/contracts.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts +// kani-flags: -Zfunction-contracts -Zquantifiers #[kani::requires(i==0)] #[kani::ensures(|ret| { diff --git a/tests/kani/Quantifiers/even.rs b/tests/kani/Quantifiers/even.rs index e7f74440d85a..0fd369446baf 100644 --- a/tests/kani/Quantifiers/even.rs +++ b/tests/kani/Quantifiers/even.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn quantifier_even_harness() { diff --git a/tests/kani/Quantifiers/from_raw_part_fixme.rs b/tests/kani/Quantifiers/from_raw_part_fixme.rs index 2f06161847bf..88a711e963d1 100644 --- a/tests/kani/Quantifiers/from_raw_part_fixme.rs +++ b/tests/kani/Quantifiers/from_raw_part_fixme.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers //! FIXME: diff --git a/tests/kani/Quantifiers/no_array.rs b/tests/kani/Quantifiers/no_array.rs index 9681e4ccf0fa..802dda296d64 100644 --- a/tests/kani/Quantifiers/no_array.rs +++ b/tests/kani/Quantifiers/no_array.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z quantifiers #[kani::proof] fn forall_assert_harness() { From 88e169851ab797df99d666914ca519adfc5173e2 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 6 Jun 2025 08:34:51 -0700 Subject: [PATCH 3/5] remove hook check --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 3b62f4707f67..6c6319baf4eb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -817,9 +817,6 @@ fn handle_quantifier( span: Span, quantifier_kind: QuantifierKind, ) -> Stmt { - if gcx.queries.args().unstable_features.contains(&"loop-contracts".to_string()) { - panic!("Unstable feature Quantifier is not enable") - } let loc = gcx.codegen_span_stable(span); let target = target.unwrap(); let lower_bound = &fargs[0]; From 81eda82c1312366481ea5adf4d41066a9e84764b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 6 Jun 2025 18:34:51 -0400 Subject: [PATCH 4/5] alphabetical order; link to rfc --- kani_metadata/src/unstable.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 7d5eec86c527..a332b9973bb8 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -99,6 +99,8 @@ pub enum UnstableFeature { /// Allow replacing certain items with stubs (mocks). /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html) Stubbing, + /// Enable quantifiers [RFC 10](https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html) + Quantifiers, /// Automatically check that uninitialized memory is not used. UninitChecks, /// Enable an unstable option or subcommand. @@ -106,8 +108,6 @@ pub enum UnstableFeature { /// Automatically check that no invalid value is produced which is considered UB in Rust. /// Note that this does not include checking uninitialized value. ValidValueChecks, - /// Enable quantifiers - Quantifiers, } impl UnstableFeature { From b9ea427bdd46aeb3eb022a9801994b872f5f7942 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 6 Jun 2025 18:35:41 -0400 Subject: [PATCH 5/5] link to quantifiers request issue instead --- library/kani_core/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index ce484dde6d41..8d2f0c6605d6 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -629,7 +629,7 @@ macro_rules! kani_intrinsics { #[crate::kani::unstable_feature( feature = "quantifiers", - issue = 4134, + issue = 2546, reason = "experimental quantifiers" )] #[inline(never)] @@ -643,7 +643,7 @@ macro_rules! kani_intrinsics { #[crate::kani::unstable_feature( feature = "quantifiers", - issue = 4134, + issue = 2546, reason = "experimental quantifiers" )] #[inline(never)]