From 5deb159b77f234d369e87503c4d2a2361ceaa962 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 1 Aug 2024 17:38:19 +0000 Subject: [PATCH 1/6] Update sections for struct-level attribute --- library/kani_macros/src/lib.rs | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 4e3a8d6f9f5b..648c9959d818 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -103,11 +103,14 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// Allow users to auto generate `Arbitrary` implementations by using /// `#[derive(Arbitrary)]` macro. /// -/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint()]` -/// attribute can be added to its fields to indicate a type safety invariant -/// condition ``. Since `kani::any()` is always expected to produce -/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further -/// constrain the objects generated with `kani::any()`**. +/// ## Type safety specification with the `#[safety_constraint(...)]` attribute +/// +/// When using `#[derive(Arbitrary)]` on a struct, the +/// `#[safety_constraint()]` attribute can be added to either the struct +/// or its fields (but not both) to indicate a type safety invariant condition +/// ``. Since `kani::any()` is always expected to produce type-safe +/// values, **adding `#[safety_constraint(...)]` to the struct or any of its +/// fields will further constrain the objects generated with `kani::any()`**. /// /// For example, the `check_positive` harness in this code is expected to /// pass: @@ -126,7 +129,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// } /// ``` /// -/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous +/// But using the `#[safety_constraint(...)]` attribute can lead to vacuous /// results when the values are over-constrained. For example, in this code /// the `check_positive` harness will pass too: /// @@ -167,10 +170,14 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// Allow users to auto generate `Invariant` implementations by using /// `#[derive(Invariant)]` macro. /// -/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint()]` -/// attribute can be added to its fields to indicate a type safety invariant -/// condition ``. This will ensure that the gets additionally checked when -/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro. +/// ## Type safety specification with the `#[safety_constraint(...)]` attribute +/// +/// When using `#[derive(Invariant)]` on a struct, the +/// `#[safety_constraint()]` attribute can be added to either the struct +/// or its fields (but not both) to indicate a type safety invariant condition +/// ``. This will ensure that the type-safety condition gets additionally +/// checked when using the `is_safe()` method automatically generated by the +/// `#[derive(Invariant)]` macro. /// /// For example, the `check_positive` harness in this code is expected to /// fail: From 178fa41026782a29995fb5092618cf88d54f5a31 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 1 Aug 2024 18:15:04 +0000 Subject: [PATCH 2/6] Add notes on struct vs. fields --- library/kani_macros/src/lib.rs | 78 ++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 648c9959d818..74229c23724a 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -161,6 +161,45 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// As usual, we recommend users to defend against these behaviors by using /// `kani::cover!(...)` checks and watching out for unreachable assertions in /// their project's code. +/// +/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields +/// +/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added +/// to to either the struct or its fields, but not to both. Adding the +/// `#[safety_constraint(...)]` attribute to both the struct and its fields will +/// result in an error. +/// +/// In practice, only one type of specification is need. If the condition for +/// the type safety invariant involves a relation between two or more struct +/// fields, the struct-level attribute should be used. Otherwise, using the +/// `#[safety_constraint(...)]` is recommended since it helps with readability. +/// +/// For example, if we were defining a custom vector `MyVector` and wanted to +/// specify that the inner vector's length is always less than or equal to its +/// capacity, we should do it as follows: +/// +/// ``` +/// #[derive(Arbitrary)] +/// #[safety_constraint(vector.len() <= *capacity)] +/// struct MyVector { +/// vector: Vec, +/// capacity: usize, +/// } +/// ``` +/// +/// However, if we were defining a struct whose fields are not related in any +/// way, we would prefer using the `#[safety_constraint(...)]` attribute in its +/// fields: +/// +/// ``` +/// #[derive(Arbitrary)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` #[proc_macro_error] #[proc_macro_derive(Arbitrary, attributes(safety_constraint))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { @@ -219,6 +258,45 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// /// Note: the assignments to `obj` and `inner` are made so that we can treat the /// fields as if they were references. +/// +/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields +/// +/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added +/// to to either the struct or its fields, but not to both. Adding the +/// `#[safety_constraint(...)]` attribute to both the struct and its fields will +/// result in an error. +/// +/// In practice, only one type of specification is need. If the condition for +/// the type safety invariant involves a relation between two or more struct +/// fields, the struct-level attribute should be used. Otherwise, using the +/// `#[safety_constraint(...)]` is recommended since it helps with readability. +/// +/// For example, if we were defining a custom vector `MyVector` and wanted to +/// specify that the inner vector's length is always less than or equal to its +/// capacity, we should do it as follows: +/// +/// ``` +/// #[derive(Invariant)] +/// #[safety_constraint(vector.len() <= *capacity)] +/// struct MyVector { +/// vector: Vec, +/// capacity: usize, +/// } +/// ``` +/// +/// However, if we were defining a struct whose fields are not related in any +/// way, we would prefer using the `#[safety_constraint(...)]` attribute in its +/// fields: +/// +/// ``` +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` #[proc_macro_error] #[proc_macro_derive(Invariant, attributes(safety_constraint))] pub fn derive_invariant(item: TokenStream) -> TokenStream { From d4771010a505ad5298dd29f043a4dc4d5b0261ac Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 1 Aug 2024 18:15:49 +0000 Subject: [PATCH 3/6] Remove `rs` from code blocks --- library/kani_macros/src/lib.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 74229c23724a..8b1843375125 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -115,7 +115,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// For example, the `check_positive` harness in this code is expected to /// pass: /// -/// ```rs +/// ``` /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0)] @@ -133,7 +133,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// results when the values are over-constrained. For example, in this code /// the `check_positive` harness will pass too: /// -/// ```rs +/// ``` /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)] @@ -221,7 +221,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// For example, the `check_positive` harness in this code is expected to /// fail: /// -/// ```rs +/// ``` /// #[derive(kani::Invariant)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0)] @@ -246,7 +246,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// For example, for the `AlwaysPositive` struct from above, we will generate /// the following implementation: /// -/// ```rs +/// ``` /// impl kani::Invariant for AlwaysPositive { /// fn is_safe(&self) -> bool { /// let obj = self; From 90b5d5a2896ddc21d785d6c4480694b372f7556a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 1 Aug 2024 19:25:03 +0000 Subject: [PATCH 4/6] Use `rust` for code blocks --- library/kani_macros/src/lib.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 8b1843375125..8b21d235f58b 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -115,7 +115,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// For example, the `check_positive` harness in this code is expected to /// pass: /// -/// ``` +/// ```rust /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0)] @@ -133,7 +133,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// results when the values are over-constrained. For example, in this code /// the `check_positive` harness will pass too: /// -/// ``` +/// ```rust /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)] @@ -178,7 +178,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// specify that the inner vector's length is always less than or equal to its /// capacity, we should do it as follows: /// -/// ``` +/// ```rust /// #[derive(Arbitrary)] /// #[safety_constraint(vector.len() <= *capacity)] /// struct MyVector { @@ -191,7 +191,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// way, we would prefer using the `#[safety_constraint(...)]` attribute in its /// fields: /// -/// ``` +/// ```rust /// #[derive(Arbitrary)] /// struct PositivePoint { /// #[safety_constraint(*x >= 0)] @@ -221,7 +221,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// For example, the `check_positive` harness in this code is expected to /// fail: /// -/// ``` +/// ```rust /// #[derive(kani::Invariant)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0)] @@ -246,7 +246,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// For example, for the `AlwaysPositive` struct from above, we will generate /// the following implementation: /// -/// ``` +/// ```rust /// impl kani::Invariant for AlwaysPositive { /// fn is_safe(&self) -> bool { /// let obj = self; @@ -275,7 +275,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// specify that the inner vector's length is always less than or equal to its /// capacity, we should do it as follows: /// -/// ``` +/// ```rust /// #[derive(Invariant)] /// #[safety_constraint(vector.len() <= *capacity)] /// struct MyVector { @@ -288,7 +288,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// way, we would prefer using the `#[safety_constraint(...)]` attribute in its /// fields: /// -/// ``` +/// ```rust /// #[derive(Invariant)] /// struct PositivePoint { /// #[safety_constraint(*x >= 0)] From 6f05ae75275d0d43c1612fbdf62db0dd99190996 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Thu, 1 Aug 2024 15:28:20 -0400 Subject: [PATCH 5/6] Update library/kani_macros/src/lib.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani_macros/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 8b21d235f58b..394d13ef8295 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -172,7 +172,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// In practice, only one type of specification is need. If the condition for /// the type safety invariant involves a relation between two or more struct /// fields, the struct-level attribute should be used. Otherwise, using the -/// `#[safety_constraint(...)]` is recommended since it helps with readability. +/// `#[safety_constraint(...)]` on field(s) is recommended since it helps with readability. /// /// For example, if we were defining a custom vector `MyVector` and wanted to /// specify that the inner vector's length is always less than or equal to its From b3c2c5a7ed8dacd70d06cd0b975996999c7cc156 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Thu, 1 Aug 2024 15:29:11 -0400 Subject: [PATCH 6/6] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani_macros/src/lib.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 394d13ef8295..6fe0979f08bc 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -165,7 +165,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields /// /// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added -/// to to either the struct or its fields, but not to both. Adding the +/// to either the struct or its fields, but not to both. Adding the /// `#[safety_constraint(...)]` attribute to both the struct and its fields will /// result in an error. /// @@ -188,7 +188,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// ``` /// /// However, if we were defining a struct whose fields are not related in any -/// way, we would prefer using the `#[safety_constraint(...)]` attribute in its +/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its /// fields: /// /// ```rust @@ -262,7 +262,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields /// /// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added -/// to to either the struct or its fields, but not to both. Adding the +/// to either the struct or its fields, but not to both. Adding the /// `#[safety_constraint(...)]` attribute to both the struct and its fields will /// result in an error. /// @@ -285,7 +285,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// ``` /// /// However, if we were defining a struct whose fields are not related in any -/// way, we would prefer using the `#[safety_constraint(...)]` attribute in its +/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its /// fields: /// /// ```rust