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

@@ -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

.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 <aws/common/math.h>
+
+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));
+}

.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"

.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

.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 <aws/common/math.h>
+
+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));
+    }
+}

.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"

include/aws/common/math.h

@@ -19,8 +19,21 @@
 #include <aws/common/common.h>
 #include <aws/common/config.h>
 
+#include <limits.h>
 #include <stdlib.h>
 
+/* 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 */

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)

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)
+AWS_TEST_CASE(test_byte_cursor_trim_basic, s_test_byte_cursor_trim_basic)