Add aws_byte_buf_reset() function (awslabs#342)

Author: danielsn

.cbmc-batch/jobs/aws_byte_buf_reset/Makefile

@@ -0,0 +1,31 @@
+# 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 ../Makefile.aws_byte_buf
+UNWINDSET += memset_impl.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/source/utils.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memset_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_reset_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_reset/aws_byte_buf_reset_harness.c

@@ -0,0 +1,37 @@
+/*
+ * 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/byte_buf.h>
+#include <proof_helpers/make_common_data_structures.h>
+#include <proof_helpers/utils.h>
+
+void aws_byte_buf_reset_harness() {
+    struct aws_byte_buf buf;
+
+    __CPROVER_assume(aws_byte_buf_is_bounded(&buf, MAX_BUFFER_SIZE));
+    ensure_byte_buf_has_allocated_buffer_member(&buf);
+    __CPROVER_assume(aws_byte_buf_is_valid(&buf));
+
+    struct aws_byte_buf old = buf;
+    bool zero_contents;
+    aws_byte_buf_reset(&buf, zero_contents);
+    assert(buf.len == 0);
+    assert(buf.allocator == old.allocator);
+    assert(buf.buffer == old.buffer);
+    assert(buf.capacity == old.capacity);
+    if (zero_contents) {
+        assert_all_bytes_are(buf.buffer, 0, buf.capacity);
+    }
+}

.cbmc-batch/jobs/aws_byte_buf_reset/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;--unwindset;memset_impl.0:11;--object-bits;8"
+goto: aws_byte_buf_reset_harness.goto
+expected: "SUCCESSFUL"

include/aws/common/byte_buf.h

@@ -162,6 +162,13 @@ void aws_byte_buf_clean_up(struct aws_byte_buf *buf);
 AWS_COMMON_API
 void aws_byte_buf_clean_up_secure(struct aws_byte_buf *buf);
 
+/**
+ * Resets the len of the buffer to 0, but does not free the memory. The buffer can then be reused.
+ * Optionally zeroes the contents, if the "zero_contents" flag is true.
+ */
+AWS_COMMON_API
+void aws_byte_buf_reset(struct aws_byte_buf *buf, bool zero_contents);
+
 /**
  * Sets all bytes of buffer to zero and resets len to zero.
  */

source/byte_buf.c

@@ -74,6 +74,13 @@ bool aws_byte_cursor_is_valid(const struct aws_byte_cursor *cursor) {
            ((cursor->len == 0) || (cursor->len > 0 && cursor->ptr && AWS_MEM_IS_WRITABLE(cursor->ptr, cursor->len)));
 }
 
+void aws_byte_buf_reset(struct aws_byte_buf *buf, bool zero_contents) {
+    if (zero_contents) {
+        aws_byte_buf_secure_zero(buf);
+    }
+    buf->len = 0;
+}
+
 void aws_byte_buf_clean_up(struct aws_byte_buf *buf) {
     AWS_PRECONDITION(aws_byte_buf_is_valid(buf));
     if (buf->allocator && buf->buffer) {

tests/CMakeLists.txt

@@ -221,6 +221,7 @@ add_test_case(test_byte_buf_append_lookup_success)
 add_test_case(test_byte_buf_append_lookup_failure)
 add_test_case(test_byte_buf_reserve)
 add_test_case(test_byte_buf_reserve_relative)
+add_test_case(test_byte_buf_reset)
 add_test_case(test_byte_cursor_compare_lexical)
 add_test_case(test_byte_cursor_compare_lookup)
 

tests/byte_buf_test.c

@@ -591,6 +591,47 @@ static int s_test_byte_buf_append_lookup_success(struct aws_allocator *allocator
 }
 AWS_TEST_CASE(test_byte_buf_append_lookup_success, s_test_byte_buf_append_lookup_success)
 
+static int s_test_reset_body(struct aws_byte_buf *buffer) {
+    struct aws_byte_cursor to_lower_cursor = aws_byte_cursor_from_c_str((char *)s_to_lower_test->bytes);
+
+    ASSERT_TRUE(
+        aws_byte_buf_append_with_lookup(buffer, &to_lower_cursor, aws_lookup_table_to_lower_get()) == AWS_OP_SUCCESS);
+    ASSERT_TRUE(buffer->len == s_to_lower_test->len);
+    for (size_t i = 0; i < s_to_lower_test->len; ++i) {
+        uint8_t value = buffer->buffer[i];
+        ASSERT_TRUE(value > 'Z' || value < 'A');
+    }
+    return 0;
+}
+static int s_test_byte_buf_reset(struct aws_allocator *allocator, void *ctx) {
+    (void)ctx;
+
+    struct aws_byte_buf buffer;
+    aws_byte_buf_init(&buffer, allocator, s_to_lower_test->len);
+    ASSERT_SUCCESS(s_test_reset_body(&buffer));
+
+    size_t old_cap = buffer.capacity;
+    aws_byte_buf_reset(&buffer, false);
+    ASSERT_TRUE(buffer.len == 0);
+    ASSERT_TRUE(buffer.capacity == old_cap);
+    ASSERT_SUCCESS(s_test_reset_body(&buffer));
+
+    old_cap = buffer.capacity;
+    aws_byte_buf_reset(&buffer, true);
+    ASSERT_TRUE(buffer.len == 0);
+    ASSERT_TRUE(buffer.capacity == old_cap);
+    for (size_t i = 0; i < buffer.capacity; i++) {
+        ASSERT_TRUE(buffer.buffer[i] == 0);
+    }
+    ASSERT_SUCCESS(s_test_reset_body(&buffer));
+
+    aws_byte_buf_clean_up(&buffer);
+    /* check that reset succeeds even on an empty buffer */
+    aws_byte_buf_reset(&buffer, true);
+    return 0;
+}
+AWS_TEST_CASE(test_byte_buf_reset, s_test_byte_buf_reset)
+
 static int s_test_byte_buf_append_lookup_failure(struct aws_allocator *allocator, void *ctx) {
     (void)ctx;
 

tests/encoding_test.c

@@ -40,7 +40,6 @@ static int s_run_hex_encoding_test_case(
     memset(allocation.buffer, 0xdd, allocation.capacity);
 
     struct aws_byte_buf output = aws_byte_buf_from_empty_array(allocation.buffer + 1, output_size);
-    output.len = 0;
 
     ASSERT_SUCCESS(aws_hex_encode(&to_encode, &output), "encode call should have succeeded");
 
@@ -69,12 +68,7 @@ static int s_run_hex_encoding_test_case(
     memset(allocation.buffer, 0xdd, allocation.capacity);
 
     ASSERT_INT_EQUALS(test_str_size - 1, output_size, "Output size on string should be %d", test_str_size - 1);
-
-    output.capacity = output_size;
-    if (output.capacity == 0) {
-        output.buffer = NULL;
-    }
-    output.len = 0;
+    aws_byte_buf_reset(&output, false);
 
     struct aws_byte_cursor expected_buf = aws_byte_cursor_from_array(expected, expected_size - 1);
     ASSERT_SUCCESS(aws_hex_decode(&expected_buf, &output), "decode call should have succeeded");
@@ -314,7 +308,6 @@ static int s_run_base64_encoding_test_case(
     memset(allocation.buffer, 0xdd, allocation.capacity);
 
     struct aws_byte_buf output = aws_byte_buf_from_empty_array(allocation.buffer + 1, output_size);
-    output.len = 0;
 
     ASSERT_SUCCESS(aws_base64_encode(&to_encode, &output), "encode call should have succeeded");
 
@@ -349,7 +342,6 @@ static int s_run_base64_encoding_test_case(
     memset(allocation.buffer, 0xdd, allocation.capacity);
 
     output = aws_byte_buf_from_empty_array(allocation.buffer + 1, output_size);
-    output.len = 0;
 
     struct aws_byte_cursor expected_buf = aws_byte_cursor_from_array(expected, expected_size - 1);
     ASSERT_SUCCESS(aws_base64_decode(&expected_buf, &output), "decode call should have succeeded");