Adds proof harnesses for aws_byte_buf_write* functions (#361)

* Adds proof harness for aws_byte_buf_write function

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

@@ -73,11 +73,21 @@ void assert_array_list_equivalence(
  * it is necessary to select a non-deterministic byte from the rhs aws_byte_buf structure
  * (use save_byte_from_array function), so it can properly assert all bytes match.
  */
-void assert_byte_buf_equivalence(
+void assert_byte_cursor_equivalence(
     const struct aws_byte_buf *const lhs,
     const struct aws_byte_buf *const rhs,
     const struct store_byte_from_buffer *const rhs_byte);
 
+/**
+ * Asserts two aws_byte_cursor structures are equivalent. Prior to using this function,
+ * it is necessary to select a non-deterministic byte from the rhs aws_byte_cursor structure
+ * (use save_byte_from_array function), so it can properly assert all bytes match.
+ */
+void assert_byte_buf_equivalence(
+    const struct aws_byte_cursor *const lhs,
+    const struct aws_byte_cursor *const rhs,
+    const struct store_byte_from_buffer *const rhs_byte);
+
 /**
  * Nondeterministically selects a byte from a hash_table implementation and stores it into a
  * store_array_list_byte structure.

.cbmc-batch/jobs/aws_byte_buf_write_be16/Makefile

@@ -0,0 +1,32 @@
+# 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 += memcpy_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/memcpy_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_write_be16_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_write_be16/aws_byte_buf_write_be16_harness.c

@@ -0,0 +1,44 @@
+/*
+ * 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_be16_harness() {
+    /* parameters */
+    struct aws_byte_buf buf;
+    uint16_t x;
+
+    /* assumptions */
+    __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));
+
+    /* 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);
+
+    /* operation under verification */
+    if (aws_byte_buf_write_be16(&buf, x)) {
+        assert(buf.len == old.len + 2);
+        assert(old.capacity == buf.capacity);
+        assert(old.allocator == buf.allocator);
+    } 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_be16/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;memcpy_impl.0:11;--object-bits;8"
+goto: aws_byte_buf_write_be16_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_write_be32/Makefile

@@ -0,0 +1,32 @@
+# 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 += memcpy_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/memcpy_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_write_be32_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_write_be32/aws_byte_buf_write_be32_harness.c

@@ -0,0 +1,44 @@
+/*
+ * 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_be32_harness() {
+    /* parameters */
+    struct aws_byte_buf buf;
+    uint32_t x;
+
+    /* assumptions */
+    __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));
+
+    /* 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);
+
+    /* operation under verification */
+    if (aws_byte_buf_write_be32(&buf, x)) {
+        assert(buf.len == old.len + 4);
+        assert(old.capacity == buf.capacity);
+        assert(old.allocator == buf.allocator);
+    } 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_be32/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;memcpy_impl.0:11;--object-bits;8"
+goto: aws_byte_buf_write_be32_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_write_be64/Makefile

@@ -0,0 +1,32 @@
+# 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 += memcpy_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/memcpy_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_write_be64_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_write_be64/aws_byte_buf_write_be64_harness.c

@@ -0,0 +1,44 @@
+/*
+ * 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_be64_harness() {
+    /* parameters */
+    struct aws_byte_buf buf;
+    uint64_t x;
+
+    /* assumptions */
+    __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));
+
+    /* 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);
+
+    /* operation under verification */
+    if (aws_byte_buf_write_be64(&buf, x)) {
+        assert(buf.len == old.len + 8);
+        assert(old.capacity == buf.capacity);
+        assert(old.allocator == buf.allocator);
+    } 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_be64/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;memcpy_impl.0:11;--object-bits;8"
+goto: aws_byte_buf_write_be64_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/Makefile

@@ -0,0 +1,32 @@
+# 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 += memcpy_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/memcpy_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_write_from_whole_buffer_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/aws_byte_buf_write_from_whole_buffer_harness.c

@@ -0,0 +1,55 @@
+/*
+ * 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_from_whole_buffer_harness() {
+    /* parameters */
+    struct aws_byte_buf buf;
+    struct aws_byte_buf src;
+
+    /* assumptions */
+    __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));
+    __CPROVER_assume(aws_byte_buf_is_bounded(&src, MAX_BUFFER_SIZE));
+    ensure_byte_buf_has_allocated_buffer_member(&src);
+    __CPROVER_assume(aws_byte_buf_is_valid(&src));
+
+    /* save current state of the parameters */
+    struct aws_byte_buf buf_old = buf;
+    struct store_byte_from_buffer old_byte_from_buf;
+    save_byte_from_array(buf.buffer, buf.len, &old_byte_from_buf);
+    struct aws_byte_buf src_old = src;
+    struct store_byte_from_buffer old_byte_from_src;
+    save_byte_from_array(src.buffer, src.len, &old_byte_from_src);
+
+    /* operation under verification */
+    if (aws_byte_buf_write_from_whole_buffer(&buf, src)) {
+        assert(buf.len == buf_old.len + src.len);
+        assert(buf_old.capacity == buf.capacity);
+        assert(buf_old.allocator == buf.allocator);
+        if (src.len > 0 && buf.len > 0) {
+            assert_bytes_match(buf.buffer + buf_old.len, src.buffer, src.len);
+        }
+    } else {
+        assert_byte_buf_equivalence(&buf, &buf_old, &old_byte_from_buf);
+    }
+
+    assert(aws_byte_buf_is_valid(&buf));
+    assert(aws_byte_buf_is_valid(&src));
+    assert_byte_buf_equivalence(&src, &src_old, &old_byte_from_src);
+}

.cbmc-batch/jobs/aws_byte_buf_write_from_whole_buffer/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;memcpy_impl.0:11;--object-bits;8"
+goto: aws_byte_buf_write_from_whole_buffer_harness.goto
+expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_byte_buf_write_from_whole_cursor/Makefile

@@ -0,0 +1,32 @@
+# 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 += memcpy_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/memcpy_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_buf_write_from_whole_cursor_harness
+###########
+
+include ../Makefile.common