Byte buf utility functions - append that grows, append with internal …

…tolower, reserve (#297)

* Byte buf append function that grows when capacity limit hit
* Byte buf reserve
* Byte buf append with lookup table translation

.cbmc-batch/include/proof_helpers/make_common_data_structures.h

@@ -37,6 +37,31 @@
 #define ASSUME_BOUNDED_ARRAY_LIST(list, max_initial_item_allocation, max_item_size)                                    \
     list = make_bounded_array_list((max_initial_item_allocation), (max_item_size))
 
+/*
+ * Checks whether aws_byte_buf is bounded by max_size
+ */
+bool is_bounded_byte_buf(struct aws_byte_buf *buf, size_t max_size);
+
+/*
+ * Checks whether aws_byte_buf has the correct allocator
+ */
+bool is_byte_buf_expected_alloc(struct aws_byte_buf *buf);
+
+/*
+ * Ensures aws_byte_buf has a proper allocated buffer member
+ */
+void ensure_byte_buf_has_allocated_buffer_member(struct aws_byte_buf *buf);
+
+/*
+ * Checks whether aws_byte_cursor is bounded by max_size
+ */
+bool is_bounded_byte_cursor(struct aws_byte_cursor *cursor, size_t max_size);
+
+/*
+ * Ensures aws_byte_cursor has a proper allocated buffer member
+ */
+void ensure_byte_cursor_has_allocated_buffer_member(struct aws_byte_cursor *cursor);
+
 /**
  * Makes an array list, with as much nondet as possible, defined initial_item_allocation and defined item_size
  */

.cbmc-batch/include/proof_helpers/proof_allocators.h

@@ -32,6 +32,13 @@ static void *can_fail_malloc_allocator(struct aws_allocator *allocator, size_t s
 
 void *can_fail_malloc(size_t size);
 
+/**
+ * CBMC considers malloc always successed for any given size. However, a real machine
+ * can only provide the available size from the pointer until the end of the address space.
+ * This function models the real machine behaviour.
+ */
+void *bounded_malloc(size_t size);
+
 static void can_fail_free(struct aws_allocator *allocator, void *ptr);
 
 static void *can_fail_realloc(struct aws_allocator *allocator, void *ptr, size_t oldsize, size_t newsize);

.cbmc-batch/jobs/aws_byte_buf_append_dynamic/Makefile

@@ -0,0 +1,29 @@
+# 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.
+
+###########
+CBMC_UNWINDSET =
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_append_dynamic_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_append_dynamic/aws_byte_buf_append_dynamic_harness.c

@@ -0,0 +1,33 @@
+/*
+ * Copyright 2010-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.
+ */
+
+#include <aws/common/byte_buf.h>
+#include <proof_helpers/make_common_data_structures.h>
+
+void aws_byte_buf_append_dynamic_harness() {
+    struct aws_byte_buf to;
+    __CPROVER_assume(aws_byte_buf_is_valid(&to));
+    ensure_byte_buf_has_allocated_buffer_member(&to);
+
+    struct aws_byte_cursor from;
+    __CPROVER_assume(aws_byte_cursor_is_valid(&from));
+    ensure_byte_cursor_has_allocated_buffer_member(&from);
+
+    aws_byte_buf_append_dynamic(&to, &from);
+
+    assert(aws_byte_buf_is_valid(&to));
+    assert(is_byte_buf_expected_alloc(&to));
+    assert(aws_byte_cursor_is_valid(&from));
+}

.cbmc-batch/jobs/aws_byte_buf_append_dynamic/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--function;aws_byte_buf_append_dynamic_harness"
+goto: aws_byte_buf_append_dynamic_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/Makefile

@@ -0,0 +1,34 @@
+# 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.
+
+###########
+# This size is suficcient to get full code coverage 
+MAX_BUF_SIZE ?= 10
+DEFINES += -DMAX_BUF_SIZE=$(MAX_BUF_SIZE)
+
+#A hash entry is 24 bytes, which is 3 iters. So we need 3 * MAX_TABLE_SIZE + 1
+UNWINDSET += aws_byte_buf_append_with_lookup.0:$(shell echo $$(($(MAX_BUF_SIZE) + 1)))
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_append_with_lookup_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/aws_byte_buf_append_with_lookup_harness.c

@@ -0,0 +1,40 @@
+/*
+ * Copyright 2010-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.
+ */
+
+#include <aws/common/byte_buf.h>
+#include <proof_helpers/make_common_data_structures.h>
+
+void aws_byte_buf_append_with_lookup_harness() {
+    struct aws_byte_buf to;
+    __CPROVER_assume(is_bounded_byte_buf(&to, MAX_BUF_SIZE));
+    __CPROVER_assume(aws_byte_buf_is_valid(&to));
+    ensure_byte_buf_has_allocated_buffer_member(&to);
+
+    struct aws_byte_cursor from;
+    __CPROVER_assume(is_bounded_byte_cursor(&from, MAX_BUF_SIZE));
+    __CPROVER_assume(aws_byte_cursor_is_valid(&from));
+    ensure_byte_cursor_has_allocated_buffer_member(&from);
+
+    /**
+     * The specification for the function requires that the buffer
+     * be at least 256 bytes.
+     */
+    uint8_t *lookup_table[256];
+    aws_byte_buf_append_with_lookup(&to, &from, lookup_table);
+
+    assert(aws_byte_buf_is_valid(&to));
+    assert(is_byte_buf_expected_alloc(&to));
+    assert(aws_byte_cursor_is_valid(&from));
+}

.cbmc-batch/jobs/aws_byte_buf_append_with_lookup/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--unwindset;aws_byte_buf_append_with_lookup.0:11;--function;aws_byte_buf_append_with_lookup_harness"
+goto: aws_byte_buf_append_with_lookup_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_reserve/Makefile

@@ -0,0 +1,29 @@
+# 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.
+
+###########
+CBMC_UNWINDSET =
+
+CBMCFLAGS +=
+
+DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
+DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
+DEPENDENCIES += $(HELPERDIR)/stubs/error.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override_no_op.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_reserve_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_reserve/aws_byte_buf_reserve_harness.c

@@ -0,0 +1,33 @@
+/*
+ * Copyright 2010-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.
+ */
+
+#include <aws/common/byte_buf.h>
+#include <proof_helpers/make_common_data_structures.h>
+
+void aws_byte_buf_reserve_harness() {
+    struct aws_byte_buf buf;
+    __CPROVER_assume(aws_byte_buf_is_valid(&buf));
+    ensure_byte_buf_has_allocated_buffer_member(&buf);
+
+    struct aws_byte_buf old = buf;
+    size_t requested_capacity;
+    int rval = aws_byte_buf_reserve(&buf, requested_capacity);
+
+    if (rval == AWS_OP_SUCCESS) {
+        assert(buf.capacity >= requested_capacity);
+    }
+    assert(aws_byte_buf_is_valid(&buf));
+    assert(is_byte_buf_expected_alloc(&buf));
+}

.cbmc-batch/jobs/aws_byte_buf_reserve/cbmc-batch.yaml

@@ -0,0 +1,4 @@
+jobos: ubuntu16
+cbmcflags: "--bounds-check;--pointer-check;--div-by-zero-check;--signed-overflow-check;--unsigned-overflow-check;--pointer-overflow-check;--undefined-shift-check;--float-overflow-check;--nan-check;--unwinding-assertions;--function;aws_byte_buf_reserve_harness"
+goto: aws_byte_buf_reserve_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/source/make_common_data_structures.c

@@ -21,6 +21,27 @@
 #include <stdint.h>
 #include <stdlib.h>
 
+bool is_bounded_byte_buf(struct aws_byte_buf *buf, size_t max_size) {
+    return buf->capacity <= max_size;
+}
+
+bool is_byte_buf_expected_alloc(struct aws_byte_buf *buf) {
+    return (buf->allocator == can_fail_allocator());
+}
+
+void ensure_byte_buf_has_allocated_buffer_member(struct aws_byte_buf *buf) {
+    buf->allocator = can_fail_allocator();
+    buf->buffer = bounded_malloc(sizeof(*(buf->buffer)) * buf->capacity);
+}
+
+bool is_bounded_byte_cursor(struct aws_byte_cursor *cursor, size_t max_size) {
+    return cursor->len <= max_size;
+}
+
+void ensure_byte_cursor_has_allocated_buffer_member(struct aws_byte_cursor *cursor) {
+    cursor->ptr = bounded_malloc(cursor->len);
+}
+
 struct aws_array_list *make_arbitrary_array_list(size_t initial_item_allocation, size_t item_size) {
     struct aws_array_list *list;
     /* Assume list is allocated */

.cbmc-batch/source/proof_allocators.c

@@ -38,6 +38,17 @@ void *can_fail_malloc(size_t size) {
     return (nondet) ? NULL : malloc(size);
 }
 
+void *bounded_malloc(size_t size) {
+    void *rval = malloc(size);
+    /*
+     * Malloc can only perform a successful allocation up to the amount of
+     * remaining memory: i.e. from the pointer until the end of the address space.
+     * On reasonable architectures, SIZE_MAX is the same # of bits as the address space.
+     */
+    __CPROVER_assume(size < SIZE_MAX - (size_t)(rval));
+    return rval;
+}
+
 static void can_fail_free(struct aws_allocator *allocator, void *ptr) {
     (void)allocator;
     free(ptr);

.cbmc-batch/stubs/memcpy_override_no_op.c

@@ -35,8 +35,8 @@ void *memcpy_impl(void *dst, const void *src, size_t n) {
         __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
             ((const char *)src >= (const char *)dst + n) || ((const char *)dst >= (const char *)src + n),
         "memcpy src/dst overlap");
-    __CPROVER_precondition(__CPROVER_r_ok(src, n), "memcpy source region readable");
-    __CPROVER_precondition(__CPROVER_w_ok(dst, n), "memcpy destination region writeable");
+    __CPROVER_precondition(src != NULL && __CPROVER_r_ok(src, n), "memcpy source region readable");
+    __CPROVER_precondition(dst != NULL && __CPROVER_w_ok(dst, n), "memcpy destination region writeable");
 
     return dst;
 }

include/aws/common/byte_buf.h

@@ -113,6 +113,18 @@ bool aws_array_eq_c_str_ignore_case(const void *array, size_t array_len, const c
 AWS_COMMON_API
 int aws_byte_buf_init(struct aws_byte_buf *buf, struct aws_allocator *allocator, size_t capacity);
 
+/**
+ * Set of properties of a valid aws_byte_buf.
+ */
+AWS_COMMON_API
+bool aws_byte_buf_is_valid(const struct aws_byte_buf *buf);
+
+/**
+ * Set of properties of a valid aws_byte_cursor.
+ */
+AWS_COMMON_API
+bool aws_byte_cursor_is_valid(const struct aws_byte_cursor *cursor);
+
 /**
  * Copies src buffer into dest and sets the correct len and capacity.
  * A new memory zone is allocated for dest->buffer. When dest is no longer needed it will have to be cleaned-up using
@@ -289,6 +301,40 @@ bool aws_byte_cursor_satisfies_pred(const struct aws_byte_cursor *source, aws_by
 AWS_COMMON_API
 int aws_byte_buf_append(struct aws_byte_buf *to, const struct aws_byte_cursor *from);
 
+/**
+ * Copies from to to while converting bytes via the passed in lookup table.
+ * If to is too small, AWS_ERROR_DEST_COPY_TOO_SMALL will be
+ * returned. dest->len will contain the amount of data actually copied to dest.
+ *
+ * from and to should not be the same buffer (overlap is not handled)
+ * lookup_table must be at least 256 bytes
+ */
+AWS_COMMON_API
+int aws_byte_buf_append_with_lookup(
+    struct aws_byte_buf *to,
+    const struct aws_byte_cursor *from,
+    const uint8_t *lookup_table);
+
+/**
+ * Copies from to to. If to is too small, the buffer will be grown appropriately and
+ * the old contents copied to, before the new contents are appended.
+ *
+ * If the grow fails (overflow or OOM), then an error will be returned.
+ *
+ * from and to may be the same buffer, permitting copying a buffer into itself.
+ */
+AWS_COMMON_API
+int aws_byte_buf_append_dynamic(struct aws_byte_buf *to, const struct aws_byte_cursor *from);
+
+/**
+ * Attempts to increase the capacity of a buffer to the requested capacity
+ *
+ * If the the buffer's capacity is currently larger than the request capacity, the
+ * function does nothing (no shrink is performed).
+ */
+AWS_COMMON_API
+int aws_byte_buf_reserve(struct aws_byte_buf *buffer, size_t requested_capacity);
+
 /**
  * Concatenates a variable number of struct aws_byte_buf * into destination.
  * Number of args must be greater than 1. If dest is too small,
@@ -361,6 +407,14 @@ uint64_t aws_hash_array_ignore_case(const void *array, size_t len);
 AWS_COMMON_API
 uint64_t aws_hash_byte_cursor_ptr_ignore_case(const void *item);
 
+/**
+ * Returns a lookup table for bytes that is the identity transformation with the exception
+ * of uppercase ascii characters getting replaced with lowercase characters.  Used in
+ * caseless comparisons.
+ */
+AWS_COMMON_API
+const uint8_t *aws_lookup_table_to_lower_get(void);
+
 AWS_EXTERN_C_END
 
 /**