From a84b84f59478fcb5d273d5af95a4054cc00d0d72 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 23 Apr 2022 20:07:49 +0000 Subject: [PATCH 1/4] Basic tests for `size_of_val` and `min_alig_of_val` --- .../Intrinsics/AlignOfVal/align_of_basic.rs | 44 +++++++++++++++++++ .../Intrinsics/SizeOfVal/size_of_basic.rs | 44 +++++++++++++++++++ 2 files changed, 88 insertions(+) create mode 100644 tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs create mode 100644 tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs new file mode 100644 index 000000000000..209af588b78b --- /dev/null +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs @@ -0,0 +1,44 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we get the expected results for the `min_align_of_val` intrinsic +// with common data types +#![feature(core_intrinsics)] +use std::intrinsics::min_align_of_val; + +struct MyStruct { + val: u32, +} + +enum MyEnum { + Variant +} + +#[kani::proof] +fn main() { + // Scalar types + unsafe { + assert!(min_align_of_val(&0i8) == 1); + assert!(min_align_of_val(&0i16) == 2); + assert!(min_align_of_val(&0i32) == 4); + assert!(min_align_of_val(&0i64) == 8); + assert!(min_align_of_val(&0i128) == 8); + assert!(min_align_of_val(&0isize) == 8); + assert!(min_align_of_val(&0u8) == 1); + assert!(min_align_of_val(&0u16) == 2); + assert!(min_align_of_val(&0u32) == 4); + assert!(min_align_of_val(&0u64) == 8); + assert!(min_align_of_val(&0u128) == 8); + assert!(min_align_of_val(&0usize) == 8); + assert!(min_align_of_val(&0f32) == 4); + assert!(min_align_of_val(&0f64) == 8); + assert!(min_align_of_val(&false) == 1); + assert!(min_align_of_val(&(0 as char)) == 4); + // Compound types (tuple and array) + assert!(min_align_of_val(&(0i32, 0i32)) == 4); + assert!(min_align_of_val(&[0i32; 5]) == 4); + // Custom data types (struct and enum) + assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4); + assert!(min_align_of_val(&MyEnum::Variant) == 1); + } +} diff --git a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs new file mode 100644 index 000000000000..545a0587b217 --- /dev/null +++ b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs @@ -0,0 +1,44 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we get the expected results for the `size_of_val` intrinsic +// with common data types +#![feature(core_intrinsics)] +use std::intrinsics::size_of_val; + +struct MyStruct { + val: u32, +} + +enum MyEnum { + Variant +} + +#[kani::proof] +fn main() { + // Scalar types + unsafe { + assert!(size_of_val(&0i8) == 1); + assert!(size_of_val(&0i16) == 2); + assert!(size_of_val(&0i32) == 4); + assert!(size_of_val(&0i64) == 8); + assert!(size_of_val(&0i128) == 16); + assert!(size_of_val(&0isize) == 8); + assert!(size_of_val(&0u8) == 1); + assert!(size_of_val(&0u16) == 2); + assert!(size_of_val(&0u32) == 4); + assert!(size_of_val(&0u64) == 8); + assert!(size_of_val(&0u128) == 16); + assert!(size_of_val(&0usize) == 8); + assert!(size_of_val(&0f32) == 4); + assert!(size_of_val(&0f64) == 8); + assert!(size_of_val(&false) == 1); + assert!(size_of_val(&(0 as char)) == 4); + // Compound types (tuple and array) + assert!(size_of_val(&(0i32, 0i32)) == 8); + assert!(size_of_val(&[0i32; 5]) == 20); + // Custom data types (struct and enum) + assert!(size_of_val(&MyStruct { val: 0u32 }) == 4); + assert!(size_of_val(&MyEnum::Variant) == 0); + } +} From cbee7b6d43afd47de63d02f522fc69c3a8c6f102 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 23 Apr 2022 20:34:16 +0000 Subject: [PATCH 2/4] Fix format --- .../Intrinsics/AlignOfVal/align_of_basic.rs | 48 +++++++++---------- .../Intrinsics/SizeOfVal/size_of_basic.rs | 48 +++++++++---------- 2 files changed, 48 insertions(+), 48 deletions(-) diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs index 209af588b78b..47009935e5c6 100644 --- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs @@ -11,34 +11,34 @@ struct MyStruct { } enum MyEnum { - Variant + Variant, } #[kani::proof] fn main() { - // Scalar types unsafe { - assert!(min_align_of_val(&0i8) == 1); - assert!(min_align_of_val(&0i16) == 2); - assert!(min_align_of_val(&0i32) == 4); - assert!(min_align_of_val(&0i64) == 8); - assert!(min_align_of_val(&0i128) == 8); - assert!(min_align_of_val(&0isize) == 8); - assert!(min_align_of_val(&0u8) == 1); - assert!(min_align_of_val(&0u16) == 2); - assert!(min_align_of_val(&0u32) == 4); - assert!(min_align_of_val(&0u64) == 8); - assert!(min_align_of_val(&0u128) == 8); - assert!(min_align_of_val(&0usize) == 8); - assert!(min_align_of_val(&0f32) == 4); - assert!(min_align_of_val(&0f64) == 8); - assert!(min_align_of_val(&false) == 1); - assert!(min_align_of_val(&(0 as char)) == 4); - // Compound types (tuple and array) - assert!(min_align_of_val(&(0i32, 0i32)) == 4); - assert!(min_align_of_val(&[0i32; 5]) == 4); - // Custom data types (struct and enum) - assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4); - assert!(min_align_of_val(&MyEnum::Variant) == 1); + // Scalar types + assert!(min_align_of_val(&0i8) == 1); + assert!(min_align_of_val(&0i16) == 2); + assert!(min_align_of_val(&0i32) == 4); + assert!(min_align_of_val(&0i64) == 8); + assert!(min_align_of_val(&0i128) == 8); + assert!(min_align_of_val(&0isize) == 8); + assert!(min_align_of_val(&0u8) == 1); + assert!(min_align_of_val(&0u16) == 2); + assert!(min_align_of_val(&0u32) == 4); + assert!(min_align_of_val(&0u64) == 8); + assert!(min_align_of_val(&0u128) == 8); + assert!(min_align_of_val(&0usize) == 8); + assert!(min_align_of_val(&0f32) == 4); + assert!(min_align_of_val(&0f64) == 8); + assert!(min_align_of_val(&false) == 1); + assert!(min_align_of_val(&(0 as char)) == 4); + // Compound types (tuple and array) + assert!(min_align_of_val(&(0i32, 0i32)) == 4); + assert!(min_align_of_val(&[0i32; 5]) == 4); + // Custom data types (struct and enum) + assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4); + assert!(min_align_of_val(&MyEnum::Variant) == 1); } } diff --git a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs index 545a0587b217..5fe3886f66ef 100644 --- a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs +++ b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs @@ -11,34 +11,34 @@ struct MyStruct { } enum MyEnum { - Variant + Variant, } #[kani::proof] fn main() { - // Scalar types unsafe { - assert!(size_of_val(&0i8) == 1); - assert!(size_of_val(&0i16) == 2); - assert!(size_of_val(&0i32) == 4); - assert!(size_of_val(&0i64) == 8); - assert!(size_of_val(&0i128) == 16); - assert!(size_of_val(&0isize) == 8); - assert!(size_of_val(&0u8) == 1); - assert!(size_of_val(&0u16) == 2); - assert!(size_of_val(&0u32) == 4); - assert!(size_of_val(&0u64) == 8); - assert!(size_of_val(&0u128) == 16); - assert!(size_of_val(&0usize) == 8); - assert!(size_of_val(&0f32) == 4); - assert!(size_of_val(&0f64) == 8); - assert!(size_of_val(&false) == 1); - assert!(size_of_val(&(0 as char)) == 4); - // Compound types (tuple and array) - assert!(size_of_val(&(0i32, 0i32)) == 8); - assert!(size_of_val(&[0i32; 5]) == 20); - // Custom data types (struct and enum) - assert!(size_of_val(&MyStruct { val: 0u32 }) == 4); - assert!(size_of_val(&MyEnum::Variant) == 0); + // Scalar types + assert!(size_of_val(&0i8) == 1); + assert!(size_of_val(&0i16) == 2); + assert!(size_of_val(&0i32) == 4); + assert!(size_of_val(&0i64) == 8); + assert!(size_of_val(&0i128) == 16); + assert!(size_of_val(&0isize) == 8); + assert!(size_of_val(&0u8) == 1); + assert!(size_of_val(&0u16) == 2); + assert!(size_of_val(&0u32) == 4); + assert!(size_of_val(&0u64) == 8); + assert!(size_of_val(&0u128) == 16); + assert!(size_of_val(&0usize) == 8); + assert!(size_of_val(&0f32) == 4); + assert!(size_of_val(&0f64) == 8); + assert!(size_of_val(&false) == 1); + assert!(size_of_val(&(0 as char)) == 4); + // Compound types (tuple and array) + assert!(size_of_val(&(0i32, 0i32)) == 8); + assert!(size_of_val(&[0i32; 5]) == 20); + // Custom data types (struct and enum) + assert!(size_of_val(&MyStruct { val: 0u32 }) == 4); + assert!(size_of_val(&MyEnum::Variant) == 0); } } From 26d979bca7619acb2e4923b61de9e01d4a945572 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Apr 2022 14:45:25 +0000 Subject: [PATCH 3/4] Add cases for `repr(C)` struct --- tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs | 7 +++++++ tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs | 7 +++++++ 2 files changed, 14 insertions(+) diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs index 47009935e5c6..78491817441a 100644 --- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs @@ -10,6 +10,12 @@ struct MyStruct { val: u32, } +#[repr(C)] +struct CStruct { + a: u8, + b: i32, +} + enum MyEnum { Variant, } @@ -40,5 +46,6 @@ fn main() { // Custom data types (struct and enum) assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4); assert!(min_align_of_val(&MyEnum::Variant) == 1); + assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4); } } diff --git a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs index 5fe3886f66ef..9781ac181f46 100644 --- a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs +++ b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs @@ -10,6 +10,12 @@ struct MyStruct { val: u32, } +#[repr(C)] +struct CStruct { + a: u8, + b: i32, +} + enum MyEnum { Variant, } @@ -40,5 +46,6 @@ fn main() { // Custom data types (struct and enum) assert!(size_of_val(&MyStruct { val: 0u32 }) == 4); assert!(size_of_val(&MyEnum::Variant) == 0); + assert!(size_of_val(&CStruct { a: 0u8, b: 0i32 }) == 8); } } From dd2f755aa9a03fa2b569757d51a2a0f445d13058 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 27 Apr 2022 00:53:05 +0000 Subject: [PATCH 4/4] Add note --- tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs | 3 ++- tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs | 5 +++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs index 78491817441a..8bbfeadf98dc 100644 --- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Check that we get the expected results for the `min_align_of_val` intrinsic -// with common data types +// with common data types. Note that these tests assume an x86_64 architecture, +// which is the only architecture supported by Kani at the moment. #![feature(core_intrinsics)] use std::intrinsics::min_align_of_val; diff --git a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs index 9781ac181f46..411f1769738b 100644 --- a/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs +++ b/tests/kani/Intrinsics/SizeOfVal/size_of_basic.rs @@ -1,8 +1,9 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that we get the expected results for the `size_of_val` intrinsic -// with common data types +// Check that we get the expected results for the `size_of_val` intrinsic with +// common data types. Note that these tests assume an x86_64 architecture, which +// is the only architecture supported by Kani at the moment. #![feature(core_intrinsics)] use std::intrinsics::size_of_val;