From b53085eaa43962476579e531d12e42cea55a0d29 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Tue, 9 Apr 2019 19:11:51 -0400 Subject: [PATCH] Math.h functionality for powers of 2 (#302) * aws_is_power_of_two() and aws_round_up_to_power_of_two() functions, as well as tests and CBMC proofs for them * fix cursor test overflow, and use SIZE_BITS consistently --- .cbmc-batch/jobs/aws_is_power_of_two/Makefile | 20 +++++ .../aws_is_power_of_two_harness.c | 29 +++++++ .../jobs/aws_is_power_of_two/cbmc-batch.yaml | 4 + .../aws_round_up_to_power_of_two/Makefile | 22 ++++++ .../aws_round_up_to_power_of_two_harness.c | 38 +++++++++ .../cbmc-batch.yaml | 4 + include/aws/common/math.h | 64 +++++++++++++-- tests/CMakeLists.txt | 2 + tests/cursor_test.c | 12 +-- tests/math_test.c | 78 +++++++++++++++++-- 10 files changed, 251 insertions(+), 22 deletions(-) create mode 100644 .cbmc-batch/jobs/aws_is_power_of_two/Makefile create mode 100644 .cbmc-batch/jobs/aws_is_power_of_two/aws_is_power_of_two_harness.c create mode 100644 .cbmc-batch/jobs/aws_is_power_of_two/cbmc-batch.yaml create mode 100644 .cbmc-batch/jobs/aws_round_up_to_power_of_two/Makefile create mode 100644 .cbmc-batch/jobs/aws_round_up_to_power_of_two/aws_round_up_to_power_of_two_harness.c create mode 100644 .cbmc-batch/jobs/aws_round_up_to_power_of_two/cbmc-batch.yaml diff --git a/.cbmc-batch/jobs/aws_is_power_of_two/Makefile b/.cbmc-batch/jobs/aws_is_power_of_two/Makefile new file mode 100644 index 000000000..34a26dad2 --- /dev/null +++ b/.cbmc-batch/jobs/aws_is_power_of_two/Makefile @@ -0,0 +1,20 @@ +# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"). You may not use +# this file except in compliance with the License. A copy of the License is +# located at +# +# http://aws.amazon.com/apache2.0/ +# +# or in the "license" file accompanying this file. This file is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +# implied. See the License for the specific language governing permissions and +# limitations under the License. + +########### +CBMCFLAGS += + +ENTRY = aws_is_power_of_two_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_is_power_of_two/aws_is_power_of_two_harness.c b/.cbmc-batch/jobs/aws_is_power_of_two/aws_is_power_of_two_harness.c new file mode 100644 index 000000000..b9ad94ec0 --- /dev/null +++ b/.cbmc-batch/jobs/aws_is_power_of_two/aws_is_power_of_two_harness.c @@ -0,0 +1,29 @@ +/* + * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). You may not use + * this file except in compliance with the License. A copy of the License is + * located at + * + * http://aws.amazon.com/apache2.0/ + * + * or in the "license" file accompanying this file. This file is distributed on an + * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + * implied. See the License for the specific language governing permissions and + * limitations under the License. + */ + +#include + +void aws_is_power_of_two_harness() { + size_t test_val; + bool rval = aws_is_power_of_two(test_val); +#if ULONG_MAX == SIZE_MAX + int popcount = __builtin_popcountl(test_val); +#elif ULLONG_MAX == SIZE_MAX + int popcount = __builtin_popcountll(test_val); +#else +# error +#endif + assert(rval == (popcount == 1)); +} diff --git a/.cbmc-batch/jobs/aws_is_power_of_two/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_is_power_of_two/cbmc-batch.yaml new file mode 100644 index 000000000..44b99e669 --- /dev/null +++ b/.cbmc-batch/jobs/aws_is_power_of_two/cbmc-batch.yaml @@ -0,0 +1,4 @@ +jobos: ubuntu16 +cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions" +goto: aws_is_power_of_two_harness.goto +expected: "SUCCESSFUL" diff --git a/.cbmc-batch/jobs/aws_round_up_to_power_of_two/Makefile b/.cbmc-batch/jobs/aws_round_up_to_power_of_two/Makefile new file mode 100644 index 000000000..6008443e2 --- /dev/null +++ b/.cbmc-batch/jobs/aws_round_up_to_power_of_two/Makefile @@ -0,0 +1,22 @@ +# Copyright 2018 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"). You may not use +# this file except in compliance with the License. A copy of the License is +# located at +# +# http://aws.amazon.com/apache2.0/ +# +# or in the "license" file accompanying this file. This file is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +# implied. See the License for the specific language governing permissions and +# limitations under the License. + +########### +CBMCFLAGS += + +DEPENDENCIES += $(HELPERDIR)/stubs/error.c + +ENTRY = aws_round_up_to_power_of_two_harness +########### + +include ../Makefile.common diff --git a/.cbmc-batch/jobs/aws_round_up_to_power_of_two/aws_round_up_to_power_of_two_harness.c b/.cbmc-batch/jobs/aws_round_up_to_power_of_two/aws_round_up_to_power_of_two_harness.c new file mode 100644 index 000000000..153510482 --- /dev/null +++ b/.cbmc-batch/jobs/aws_round_up_to_power_of_two/aws_round_up_to_power_of_two_harness.c @@ -0,0 +1,38 @@ +/* + * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). You may not use + * this file except in compliance with the License. A copy of the License is + * located at + * + * http://aws.amazon.com/apache2.0/ + * + * or in the "license" file accompanying this file. This file is distributed on an + * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + * implied. See the License for the specific language governing permissions and + * limitations under the License. + */ + +#include + +void aws_round_up_to_power_of_two_harness() { + size_t test_val; + size_t result; + int rval = aws_round_up_to_power_of_two(test_val, &result); + +#if ULONG_MAX == SIZE_MAX + int popcount = __builtin_popcountl(result); +#elif ULLONG_MAX == SIZE_MAX + int popcount = __builtin_popcountll(result); +#else +# error +#endif + if (rval == AWS_OP_SUCCESS) { + assert(popcount == 1); + assert(test_val <= result); + assert(test_val >= result >> 1); + } else { + // Only fail if rounding up would cause us to overflow. + assert(test_val > ((SIZE_MAX >> 1) + 1)); + } +} diff --git a/.cbmc-batch/jobs/aws_round_up_to_power_of_two/cbmc-batch.yaml b/.cbmc-batch/jobs/aws_round_up_to_power_of_two/cbmc-batch.yaml new file mode 100644 index 000000000..b54155278 --- /dev/null +++ b/.cbmc-batch/jobs/aws_round_up_to_power_of_two/cbmc-batch.yaml @@ -0,0 +1,4 @@ +jobos: ubuntu16 +cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions" +goto: aws_round_up_to_power_of_two_harness.goto +expected: "SUCCESSFUL" diff --git a/include/aws/common/math.h b/include/aws/common/math.h index 591c1a520..6617784b1 100644 --- a/include/aws/common/math.h +++ b/include/aws/common/math.h @@ -19,8 +19,21 @@ #include #include +#include #include +/* The number of bits in a size_t variable */ +#if SIZE_MAX == UINT32_MAX +# define SIZE_BITS 32 +#elif SIZE_MAX == UINT64_MAX +# define SIZE_BITS 64 +#else +# error "Target not supported" +#endif + +/* The largest power of two that can be stored in a size_t */ +#define SIZE_MAX_POWER_OF_TWO (((size_t)1) << (SIZE_BITS - 1)) + #ifdef __cplusplus extern "C" { #endif @@ -104,9 +117,9 @@ AWS_COMMON_API int aws_add_u32_checked(uint32_t a, uint32_t b, uint32_t *r); * Multiplies a * b. If the result overflows, returns SIZE_MAX. */ AWS_STATIC_IMPL size_t aws_mul_size_saturating(size_t a, size_t b) { -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 return (size_t)aws_mul_u32_saturating(a, b); -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 return (size_t)aws_mul_u64_saturating(a, b); #else # error "Target not supported" @@ -118,9 +131,9 @@ AWS_STATIC_IMPL size_t aws_mul_size_saturating(size_t a, size_t b) { * overflows, returns AWS_OP_ERR; otherwise returns AWS_OP_SUCCESS. */ AWS_STATIC_IMPL int aws_mul_size_checked(size_t a, size_t b, size_t *r) { -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 return aws_mul_u32_checked(a, b, (uint32_t *)r); -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 return aws_mul_u64_checked(a, b, (uint64_t *)r); #else # error "Target not supported" @@ -131,9 +144,9 @@ AWS_STATIC_IMPL int aws_mul_size_checked(size_t a, size_t b, size_t *r) { * Adds a + b. If the result overflows returns SIZE_MAX. */ AWS_STATIC_IMPL size_t aws_add_size_saturating(size_t a, size_t b) { -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 return (size_t)aws_add_u32_saturating(a, b); -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 return (size_t)aws_add_u64_saturating(a, b); #else # error "Target not supported" @@ -146,15 +159,50 @@ AWS_STATIC_IMPL size_t aws_add_size_saturating(size_t a, size_t b) { */ AWS_STATIC_IMPL int aws_add_size_checked(size_t a, size_t b, size_t *r) { -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 return aws_add_u32_checked(a, b, (uint32_t *)r); -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 return aws_add_u64_checked(a, b, (uint64_t *)r); #else # error "Target not supported" #endif } +/** + * Function to check if x is power of 2 + */ +AWS_STATIC_IMPL bool aws_is_power_of_two(const size_t x) { + /* First x in the below expression is for the case when x is 0 */ + return x && (!(x & (x - 1))); +} + +/** + * Function to find the smallest result that is power of 2 >= n. Returns AWS_OP_ERR if this cannot + * be done without overflow + */ +AWS_STATIC_IMPL int aws_round_up_to_power_of_two(size_t n, size_t *result) { + if (n == 0) { + *result = 1; + return AWS_OP_SUCCESS; + } + if (n > SIZE_MAX_POWER_OF_TWO) { + return aws_raise_error(AWS_ERROR_OVERFLOW_DETECTED); + } + + n--; + n |= n >> 1; + n |= n >> 2; + n |= n >> 4; + n |= n >> 8; + n |= n >> 16; +#if SIZE_BITS == 64 + n |= n >> 32; +#endif + n++; + *result = n; + return AWS_OP_SUCCESS; +} + #if _MSC_VER # pragma warning(pop) #endif /* _MSC_VER */ diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 7fb09af16..6cef36511 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -152,6 +152,8 @@ add_test_case(test_hash_churn) add_test_case(test_hash_table_cleanup_idempotent) add_test_case(test_hash_table_byte_cursor_create_find) +add_test_case(test_is_power_of_two) +add_test_case(test_round_up_to_power_of_two) add_test_case(test_mul_size_checked) add_test_case(test_mul_size_saturating) add_test_case(test_mul_u32_checked) diff --git a/tests/cursor_test.c b/tests/cursor_test.c index a580794d7..93eeba5fa 100644 --- a/tests/cursor_test.c +++ b/tests/cursor_test.c @@ -44,9 +44,9 @@ static int s_nospec_index_test_fn(struct aws_allocator *allocator, void *ctx) { ASSERT_UINT_EQUALS(0, aws_nospec_mask(4, 4)); ASSERT_UINT_EQUALS(UINTPTR_MAX, aws_nospec_mask(4, 5)); - ASSERT_UINT_EQUALS(UINTPTR_MAX, aws_nospec_mask(SSIZE_MAX - 1, SSIZE_MAX)); - ASSERT_UINT_EQUALS(0, aws_nospec_mask(SSIZE_MAX + 1, SSIZE_MAX)); - ASSERT_UINT_EQUALS(0, aws_nospec_mask(SSIZE_MAX, SSIZE_MAX + 1)); + ASSERT_UINT_EQUALS(UINTPTR_MAX, aws_nospec_mask((SIZE_MAX >> 1) - 1, (SIZE_MAX >> 1))); + ASSERT_UINT_EQUALS(0, aws_nospec_mask((SIZE_MAX >> 1) + 1, (SIZE_MAX >> 1))); + ASSERT_UINT_EQUALS(0, aws_nospec_mask((SIZE_MAX >> 1), (SIZE_MAX >> 1) + 1)); return 0; } @@ -88,8 +88,8 @@ static int s_test_byte_cursor_advance_internal( ASSERT_ADVANCE(5, 5); ASSERT_NOADVANCE(6, 5); - ASSERT_NOADVANCE(SSIZE_MAX + 1, SSIZE_MAX); - ASSERT_NOADVANCE(SSIZE_MAX, (size_t)SSIZE_MAX + 1); + ASSERT_NOADVANCE((SIZE_MAX >> 1) + 1, (SIZE_MAX >> 1)); + ASSERT_NOADVANCE((SIZE_MAX >> 1), (SIZE_MAX >> 1) + 1); return 0; } @@ -353,4 +353,4 @@ static int s_test_byte_cursor_trim_basic(struct aws_allocator *allocator, void * return 0; } -AWS_TEST_CASE(test_byte_cursor_trim_basic, s_test_byte_cursor_trim_basic) \ No newline at end of file +AWS_TEST_CASE(test_byte_cursor_trim_basic, s_test_byte_cursor_trim_basic) diff --git a/tests/math_test.c b/tests/math_test.c index 451adafb2..2ffd7e2df 100644 --- a/tests/math_test.c +++ b/tests/math_test.c @@ -39,6 +39,68 @@ (unsigned long long)(result)); \ } while (0) +AWS_TEST_CASE(test_is_power_of_two, s_test_is_power_of_two_fn) +static int s_test_is_power_of_two_fn(struct aws_allocator *allocator, void *ctx) { + (void)allocator; + (void)ctx; + + ASSERT_FALSE(aws_is_power_of_two(0)); + for (size_t i = 0; i < SIZE_BITS; ++i) { + const size_t ith_power = (size_t)1 << i; + ASSERT_TRUE(aws_is_power_of_two(ith_power)); + ASSERT_FALSE(aws_is_power_of_two(ith_power + 9)); + ASSERT_FALSE(aws_is_power_of_two(ith_power - 9)); + ASSERT_FALSE(aws_is_power_of_two(ith_power + 100)); + ASSERT_FALSE(aws_is_power_of_two(ith_power - 100)); + } + return 0; +} + +#define CHECK_ROUND_OVERFLOWS(a) \ + do { \ + size_t result_val; \ + ASSERT_TRUE(aws_round_up_to_power_of_two((a), &result_val)); \ + } while (0) + +#define CHECK_ROUND_SUCCEEDS(a, r) \ + do { \ + size_t result_val; \ + ASSERT_FALSE(aws_round_up_to_power_of_two((a), &result_val)); \ + ASSERT_TRUE(aws_is_power_of_two(result_val)); \ + ASSERT_INT_EQUALS( \ + (uint64_t)result_val, \ + (uint64_t)(r), \ + "Expected %s(%016llx) = %016llx; got %016llx", \ + "aws_round_up_to_power_of_two", \ + (unsigned long long)(a), \ + (unsigned long long)(r), \ + (unsigned long long)(result_val)); \ + } while (0) + +AWS_TEST_CASE(test_round_up_to_power_of_two, s_test_round_up_to_power_of_two_fn) +static int s_test_round_up_to_power_of_two_fn(struct aws_allocator *allocator, void *ctx) { + (void)allocator; + (void)ctx; + + /*special case 0, 1 and 2, where subtracting from the number doesn't cause it to round back up */ + CHECK_ROUND_SUCCEEDS(0, 1); + CHECK_ROUND_SUCCEEDS(1, 1); + CHECK_ROUND_SUCCEEDS(2, 2); + + for (size_t i = 2; i < SIZE_BITS - 1; ++i) { + const size_t ith_power = (size_t)1 << i; + CHECK_ROUND_SUCCEEDS(ith_power, ith_power); + CHECK_ROUND_SUCCEEDS(ith_power - 1, ith_power); + CHECK_ROUND_SUCCEEDS(ith_power + 1, ith_power << 1); + } + + /* Special case for the largest representable power of two, where addition causes overflow */ + CHECK_ROUND_SUCCEEDS(SIZE_MAX_POWER_OF_TWO, SIZE_MAX_POWER_OF_TWO); + CHECK_ROUND_SUCCEEDS(SIZE_MAX_POWER_OF_TWO - 1, SIZE_MAX_POWER_OF_TWO); + CHECK_ROUND_OVERFLOWS(SIZE_MAX_POWER_OF_TWO + 1); + return 0; +} + AWS_TEST_CASE(test_mul_u64_saturating, s_test_mul_u64_saturating_fn) static int s_test_mul_u64_saturating_fn(struct aws_allocator *allocator, void *ctx) { (void)allocator; @@ -96,7 +158,7 @@ static int s_test_mul_size_saturating_fn(struct aws_allocator *allocator, void * (void)allocator; (void)ctx; -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 CHECK_SAT(aws_mul_size_saturating, 0, 0, 0); CHECK_SAT(aws_mul_size_saturating, 0, 1, 0); CHECK_SAT(aws_mul_size_saturating, 0, ~0U, 0); @@ -114,7 +176,7 @@ static int s_test_mul_size_saturating_fn(struct aws_allocator *allocator, void * CHECK_SAT(aws_mul_size_saturating, 0xFFFE, 0xFFFE, 0xFFFC0004U); CHECK_SAT(aws_mul_size_saturating, 0x1FFFF, 0x1FFFF, 0xFFFFFFFFU); CHECK_SAT(aws_mul_size_saturating, ~0U, ~0U, ~0U); -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 CHECK_SAT(aws_mul_size_saturating, 0, 0, 0); CHECK_SAT(aws_mul_size_saturating, 0, 1, 0); CHECK_SAT(aws_mul_size_saturating, 0, ~0LLU, 0); @@ -229,7 +291,7 @@ static int s_test_mul_size_checked_fn(struct aws_allocator *allocator, void *ctx (void)allocator; (void)ctx; -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 CHECK_NO_OVF(aws_mul_size_checked, size_t, 0, 0, 0); CHECK_NO_OVF(aws_mul_size_checked, size_t, 0, 1, 0); CHECK_NO_OVF(aws_mul_size_checked, size_t, 0, ~0u, 0); @@ -247,7 +309,7 @@ static int s_test_mul_size_checked_fn(struct aws_allocator *allocator, void *ctx CHECK_NO_OVF(aws_mul_size_checked, size_t, 0xFFFE, 0xFFFE, 0xFFFC0004u); CHECK_OVF(aws_mul_size_checked, size_t, 0x1FFFF, 0x1FFFF); CHECK_OVF(aws_mul_size_checked, size_t, ~0u, ~0u); -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 CHECK_NO_OVF(aws_mul_size_checked, size_t, 0, 0, 0); CHECK_NO_OVF(aws_mul_size_checked, size_t, 0, 1, 0); CHECK_NO_OVF(aws_mul_size_checked, size_t, 0, ~0LLU, 0); @@ -276,10 +338,10 @@ static int s_test_add_size_checked_fn(struct aws_allocator *allocator, void *ctx (void)allocator; (void)ctx; -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 const uint32_t HALF_MAX = UINT32_MAX / 2; const uint32_t ACTUAL_MAX = UINT32_MAX; -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 const uint64_t HALF_MAX = UINT64_MAX / 2; const uint64_t ACTUAL_MAX = UINT64_MAX; #else @@ -314,10 +376,10 @@ static int s_test_add_size_saturating_fn(struct aws_allocator *allocator, void * (void)allocator; (void)ctx; -#if SIZE_MAX == UINT32_MAX +#if SIZE_BITS == 32 const uint32_t HALF_MAX = UINT32_MAX / 2; const uint32_t ACTUAL_MAX = UINT32_MAX; -#elif SIZE_MAX == UINT64_MAX +#elif SIZE_BITS == 64 const uint64_t HALF_MAX = UINT64_MAX / 2; const uint64_t ACTUAL_MAX = UINT64_MAX; #else