Adds proof harness for aws_byte_buf_write function (#360)

* Adds proof harness for aws_byte_buf_write function

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

@@ -18,6 +18,7 @@
 #include <aws/common/array_list.h>
 #include <aws/common/byte_buf.h>
 #include <proof_helpers/nondet.h>
+#include <proof_helpers/proof_allocators.h>
 #include <stddef.h>
 #include <stdint.h>
 

.cbmc-batch/jobs/aws_byte_buf_init_copy/Makefile

@@ -12,8 +12,7 @@
 # limitations under the License.
 
 ###########
-MAX_BUFFER_SIZE ?= 10
-DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE)
+include ../Makefile.aws_byte_buf
 
 UNWINDSET += memcpy_impl.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
 

.cbmc-batch/jobs/aws_byte_buf_write/Makefile

@@ -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 ../Makefile.aws_byte_buf
+
+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 += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_write_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_write/aws_byte_buf_write_harness.c

@@ -0,0 +1,46 @@
+/*
+ * 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>
+
+void aws_byte_buf_write_harness() {
+    /* parameters */
+    struct aws_byte_buf buf;
+    size_t len;
+    uint8_t *array = can_fail_malloc(len);
+
+    /* assumptions */
+    ensure_byte_buf_has_allocated_buffer_member(&buf);
+    __CPROVER_assume(aws_byte_buf_is_valid(&buf));
+
+    /* save current state of the parameters */
+    struct aws_byte_buf old = buf;
+    struct store_byte_from_buffer old_byte_from_buf;
+    save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf);
+
+    if (aws_byte_buf_write((nondet_bool() ? &buf : NULL), array, len)) {
+        assert(buf.len == old.len + len);
+        assert(old.capacity == buf.capacity);
+        assert(old.allocator == buf.allocator);
+        if (len > 0 && buf.len > 0) {
+            assert_bytes_match(buf.buffer + old.len, array, len);
+        }
+    } else {
+        assert_byte_buf_equivalence(&buf, &old, &old_byte_from_buf);
+    }
+
+    assert(aws_byte_buf_is_valid(&buf));
+}

.cbmc-batch/jobs/aws_byte_buf_write/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;--object-bits;8"
+goto: aws_byte_buf_write_harness.goto
+expected: "SUCCESSFUL"

include/aws/common/byte_buf.h

@@ -802,14 +802,17 @@ AWS_STATIC_IMPL bool aws_byte_buf_write(
     struct aws_byte_buf *AWS_RESTRICT buf,
     const uint8_t *AWS_RESTRICT src,
     size_t len) {
+    AWS_PRECONDITION(aws_byte_buf_is_valid(buf) && AWS_MEM_IS_WRITABLE(src, len));
 
     if (buf->len > (SIZE_MAX >> 1) || len > (SIZE_MAX >> 1) || buf->len + len > buf->capacity) {
+        AWS_POSTCONDITION(aws_byte_buf_is_valid(buf));
         return false;
     }
 
     memcpy(buf->buffer + buf->len, src, len);
     buf->len += len;
 
+    AWS_POSTCONDITION(aws_byte_buf_is_valid(buf));
     return true;
 }
 

tests/cursor_test.c

@@ -223,7 +223,7 @@ static int s_byte_cursor_limit_tests_fn(struct aws_allocator *allocator, void *c
     ASSERT_UINT_EQUALS(0, arr[1]);
 
     cur.len = 0;
-    buffer.capacity = 0;
+    aws_byte_buf_clean_up(&buffer);
     ASSERT_FALSE(aws_byte_cursor_read_u8(&cur, &u8));
     ASSERT_UINT_EQUALS(0, u8);
     ASSERT_FALSE(aws_byte_buf_write_u8(&buffer, 0));