Adds proof harnesses for aws_byte_cursor_eq* functions (#386)

* Adds pre and postconditions to aws_byte_cursor_eq and aws_byte_cursor_eq_ignore_case functions

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Adds a proof harness for aws_byte_cursor_eq function

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Adds a proof harness for aws_byte_cursor_eq_ignore_case function

Signed-off-by: Felipe R. Monteiro <[email protected]>

.cbmc-batch/jobs/aws_byte_cursor_eq/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 += memcmp.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/memcmp_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_cursor_eq_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_cursor_eq/aws_byte_cursor_eq_harness.c

@@ -0,0 +1,62 @@
+/*
+ * 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/proof_allocators.h>
+
+void aws_byte_cursor_eq_harness() {
+    /* parameters */
+    struct aws_byte_cursor lhs;
+    struct aws_byte_cursor rhs;
+
+    /* assumptions */
+    __CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE));
+    ensure_byte_cursor_has_allocated_buffer_member(&lhs);
+    __CPROVER_assume(aws_byte_cursor_is_valid(&lhs));
+    if (nondet_bool()) {
+        rhs = lhs;
+    } else {
+        __CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE));
+        ensure_byte_cursor_has_allocated_buffer_member(&rhs);
+        __CPROVER_assume(aws_byte_cursor_is_valid(&rhs));
+    }
+
+    /* save current state of the data structure */
+    struct aws_byte_cursor old_lhs = lhs;
+    struct store_byte_from_buffer old_byte_from_lhs;
+    save_byte_from_array(lhs.ptr, lhs.len, &old_byte_from_lhs);
+    struct aws_byte_cursor old_rhs = rhs;
+    struct store_byte_from_buffer old_byte_from_rhs;
+    save_byte_from_array(rhs.ptr, rhs.len, &old_byte_from_rhs);
+
+    /* operation under verification */
+    if (aws_byte_cursor_eq((nondet_bool() ? &lhs : NULL), (nondet_bool() ? &rhs : NULL))) {
+        assert(lhs.len == rhs.len);
+        if (lhs.len > 0) {
+            assert_bytes_match(lhs.ptr, rhs.ptr, lhs.len);
+        }
+    }
+
+    /* assertions */
+    assert(aws_byte_cursor_is_valid(&lhs));
+    assert(aws_byte_cursor_is_valid(&rhs));
+    if (lhs.len != 0) {
+        assert_byte_from_buffer_matches(lhs.ptr, &old_byte_from_lhs);
+    }
+    if (rhs.len != 0) {
+        assert_byte_from_buffer_matches(rhs.ptr, &old_byte_from_rhs);
+    }
+}

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

.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/Makefile

@@ -0,0 +1,33 @@
+# 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 += memcmp.0:$(shell echo $$(($(MAX_BUFFER_SIZE) + 1)))
+UNWINDSET += aws_array_eq_ignore_case.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/memcmp_override.c
+DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/common.c
+
+ENTRY = aws_byte_cursor_eq_ignore_case_harness
+###########
+
+include ../Makefile.common

.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/aws_byte_cursor_eq_ignore_case_harness.c

@@ -0,0 +1,59 @@
+/*
+ * 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/proof_allocators.h>
+
+void aws_byte_cursor_eq_ignore_case_harness() {
+    /* parameters */
+    struct aws_byte_cursor lhs;
+    struct aws_byte_cursor rhs;
+
+    /* assumptions */
+    __CPROVER_assume(aws_byte_cursor_is_bounded(&lhs, MAX_BUFFER_SIZE));
+    ensure_byte_cursor_has_allocated_buffer_member(&lhs);
+    __CPROVER_assume(aws_byte_cursor_is_valid(&lhs));
+    if (nondet_bool()) {
+        rhs = lhs;
+    } else {
+        __CPROVER_assume(aws_byte_cursor_is_bounded(&rhs, MAX_BUFFER_SIZE));
+        ensure_byte_cursor_has_allocated_buffer_member(&rhs);
+        __CPROVER_assume(aws_byte_cursor_is_valid(&rhs));
+    }
+
+    /* save current state of the data structure */
+    struct aws_byte_cursor old_lhs = lhs;
+    struct store_byte_from_buffer old_byte_from_lhs;
+    save_byte_from_array(lhs.ptr, lhs.len, &old_byte_from_lhs);
+    struct aws_byte_cursor old_rhs = rhs;
+    struct store_byte_from_buffer old_byte_from_rhs;
+    save_byte_from_array(rhs.ptr, rhs.len, &old_byte_from_rhs);
+
+    /* operation under verification */
+    if (aws_byte_cursor_eq_ignore_case((nondet_bool() ? &lhs : NULL), (nondet_bool() ? &rhs : NULL))) {
+        assert(lhs.len == rhs.len);
+    }
+
+    /* assertions */
+    assert(aws_byte_cursor_is_valid(&lhs));
+    assert(aws_byte_cursor_is_valid(&rhs));
+    if (lhs.len != 0) {
+        assert_byte_from_buffer_matches(lhs.ptr, &old_byte_from_lhs);
+    }
+    if (rhs.len != 0) {
+        assert_byte_from_buffer_matches(rhs.ptr, &old_byte_from_rhs);
+    }
+}

.cbmc-batch/jobs/aws_byte_cursor_eq_ignore_case/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;memcmp.0:11,aws_array_eq_ignore_case.0:11;--object-bits;8"
+goto: aws_byte_cursor_eq_ignore_case_harness.goto
+expected: "SUCCESSFUL"

source/byte_buf.c

@@ -272,13 +272,17 @@ int aws_byte_buf_cat(struct aws_byte_buf *dest, size_t number_of_args, ...) {
 }
 
 bool aws_byte_cursor_eq(const struct aws_byte_cursor *a, const struct aws_byte_cursor *b) {
-    AWS_ASSERT(a && b);
-    return aws_array_eq(a->ptr, a->len, b->ptr, b->len);
+    AWS_PRECONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
+    bool rv = aws_array_eq(a->ptr, a->len, b->ptr, b->len);
+    AWS_POSTCONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
+    return rv;
 }
 
 bool aws_byte_cursor_eq_ignore_case(const struct aws_byte_cursor *a, const struct aws_byte_cursor *b) {
-    AWS_ASSERT(a && b);
-    return aws_array_eq_ignore_case(a->ptr, a->len, b->ptr, b->len);
+    AWS_PRECONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
+    bool rv = aws_array_eq_ignore_case(a->ptr, a->len, b->ptr, b->len);
+    AWS_POSTCONDITION(aws_byte_cursor_is_valid(a) && aws_byte_cursor_is_valid(b));
+    return rv;
 }
 
 /* Every possible uint8_t value, lowercased */