Extend the harness for priority queue s_swap with fc assertions (#415)

* Extend the harness for priority queue s_swap with functional correctness assertions

* Extend priority_queue_is_valid to check that all backpointers point to NULL or correctly allocated memory

* Stub out s_swap in s_sift harnesses to make them run in reasonable time

* Type and format check

* Introduce the AWS_DEEP_CHECKS macro to guard costly validity checks

* Add AWS_DEEP_CHECKS macro

Author: angelhof

.cbmc-batch/jobs/Makefile.common

@@ -70,6 +70,11 @@ CBMCFLAGS +=  --object-bits $(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC=1
 
+################################################################
+# Don't execute deep checks by default
+AWS_DEEP_CHECKS ?= 0
+DEFINES += -DAWS_DEEP_CHECKS=$(AWS_DEEP_CHECKS)
+
 ################################################################
 # We always override allocator functions with our own allocator
 # Removing the function from the goto program helps CBMC's

.cbmc-batch/jobs/aws_priority_queue_s_sift_down/Makefile

@@ -27,6 +27,7 @@ include ../Makefile.aws_priority_queue_sift
 # log(NUMBER_PRIO_QUEUE_ITEMS) times.
 UNWINDSET += aws_priority_queue_s_sift_down_harness.0:$(shell echo $$((1 + $(MAX_PRIORITY_QUEUE_ITEMS))))
 UNWINDSET += __CPROVER_file_local_priority_queue_c_s_sift_down.0:$(MAX_HEAP_HEIGHT)
+UNWINDSET += aws_priority_queue_backpointers_valid_deep.0:$(shell echo $$((1 + $(MAX_PRIORITY_QUEUE_ITEMS))))
 
 CBMCFLAGS += 
 
@@ -39,6 +40,9 @@ DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 DEPENDENCIES += $(SRCDIR)/source/priority_queue.c
 
+ABSTRACTIONS +=  $(HELPERDIR)/stubs/s_swap_override_no_op.c
+
+ADDITIONAL_REMOVE_FUNCTION_BODY += --remove-function-body __CPROVER_file_local_priority_queue_c_s_swap
 
 ENTRY = aws_priority_queue_s_sift_down_harness
 ###########

.cbmc-batch/jobs/aws_priority_queue_s_sift_down/aws_priority_queue_s_sift_down_harness.c

@@ -47,4 +47,5 @@ void aws_priority_queue_s_sift_down_harness() {
 
     /* Assert the postconditions */
     assert(aws_priority_queue_is_valid(&queue));
+    assert(aws_priority_queue_backpointers_valid_deep(&queue));
 }

.cbmc-batch/jobs/aws_priority_queue_s_sift_down/cbmc-batch.yaml

@@ -1,4 +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;aws_priority_queue_s_sift_down_harness.0:6,__CPROVER_file_local_priority_queue_c_s_sift_down.0:3;--object-bits;8"
+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;aws_priority_queue_s_sift_down_harness.0:6,__CPROVER_file_local_priority_queue_c_s_sift_down.0:3,aws_priority_queue_backpointers_valid_deep.0:6;--object-bits;8"
 goto: aws_priority_queue_s_sift_down_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_priority_queue_s_sift_either/Makefile

@@ -28,7 +28,7 @@ include ../Makefile.aws_priority_queue_sift
 UNWINDSET += __CPROVER_file_local_priority_queue_c_s_sift_down.0:$(MAX_HEAP_HEIGHT)
 UNWINDSET += __CPROVER_file_local_priority_queue_c_s_sift_up.0:$(MAX_HEAP_HEIGHT)
 UNWINDSET += aws_priority_queue_s_sift_either_harness.0:$(shell echo $$((1 + $(MAX_PRIORITY_QUEUE_ITEMS))))
-
+UNWINDSET += aws_priority_queue_backpointers_valid_deep.0:$(shell echo $$((1 + $(MAX_PRIORITY_QUEUE_ITEMS))))
 
 CBMCFLAGS += 
 
@@ -41,6 +41,9 @@ DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 DEPENDENCIES += $(SRCDIR)/source/priority_queue.c
 
+ABSTRACTIONS +=  $(HELPERDIR)/stubs/s_swap_override_no_op.c
+
+ADDITIONAL_REMOVE_FUNCTION_BODY += --remove-function-body __CPROVER_file_local_priority_queue_c_s_swap
 
 ENTRY = aws_priority_queue_s_sift_either_harness
 ###########

.cbmc-batch/jobs/aws_priority_queue_s_sift_either/aws_priority_queue_s_sift_either_harness.c

@@ -50,4 +50,5 @@ void aws_priority_queue_s_sift_either_harness() {
 
     /* Assert the postconditions */
     assert(aws_priority_queue_is_valid(&queue));
+    assert(aws_priority_queue_backpointers_valid_deep(&queue));
 }

.cbmc-batch/jobs/aws_priority_queue_s_sift_either/cbmc-batch.yaml

@@ -1,4 +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;__CPROVER_file_local_priority_queue_c_s_sift_down.0:3,__CPROVER_file_local_priority_queue_c_s_sift_up.0:3,aws_priority_queue_s_sift_either_harness.0:6;--object-bits;8"
+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;__CPROVER_file_local_priority_queue_c_s_sift_down.0:3,__CPROVER_file_local_priority_queue_c_s_sift_up.0:3,aws_priority_queue_s_sift_either_harness.0:6,aws_priority_queue_backpointers_valid_deep.0:6;--object-bits;8"
 goto: aws_priority_queue_s_sift_either_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_priority_queue_s_sift_up/Makefile

@@ -21,13 +21,13 @@ include ../Makefile.aws_priority_queue_sift
 # - 300s for MAX_PRIORITY_QUEUE_ITEMS=3 items
 # - 450s for MAX_PRIORITY_QUEUE_ITEMS=5 items 
 
-
 # Note:
 # In order to reach full coverage we need to unwind the harness loop
 # as many times as the number of queue items, and the sift down loop
 # log(NUMBER_PRIO_QUEUE_ITEMS) times.
 UNWINDSET += aws_priority_queue_s_sift_up_harness.0:$(shell echo $$((1 + $(MAX_PRIORITY_QUEUE_ITEMS))))
 UNWINDSET += __CPROVER_file_local_priority_queue_c_s_sift_up.0:$(MAX_HEAP_HEIGHT)
+UNWINDSET += aws_priority_queue_backpointers_valid_deep.0:$(shell echo $$((1 + $(MAX_PRIORITY_QUEUE_ITEMS))))
 
 CBMCFLAGS += 
 
@@ -40,6 +40,9 @@ DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 DEPENDENCIES += $(SRCDIR)/source/priority_queue.c
 
+ABSTRACTIONS +=  $(HELPERDIR)/stubs/s_swap_override_no_op.c
+
+ADDITIONAL_REMOVE_FUNCTION_BODY += --remove-function-body __CPROVER_file_local_priority_queue_c_s_swap
 
 ENTRY = aws_priority_queue_s_sift_up_harness
 ###########

.cbmc-batch/jobs/aws_priority_queue_s_sift_up/aws_priority_queue_s_sift_up_harness.c

@@ -50,4 +50,5 @@ void aws_priority_queue_s_sift_up_harness() {
 
     /* Assert the postconditions */
     assert(aws_priority_queue_is_valid(&queue));
+    assert(aws_priority_queue_backpointers_valid_deep(&queue));
 }

.cbmc-batch/jobs/aws_priority_queue_s_sift_up/cbmc-batch.yaml

@@ -1,4 +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;aws_priority_queue_s_sift_up_harness.0:6,__CPROVER_file_local_priority_queue_c_s_sift_up.0:3;--object-bits;8"
+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;aws_priority_queue_s_sift_up_harness.0:6,__CPROVER_file_local_priority_queue_c_s_sift_up.0:3,aws_priority_queue_backpointers_valid_deep.0:6;--object-bits;8"
 goto: aws_priority_queue_s_sift_up_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/jobs/aws_priority_queue_s_swap/Makefile

@@ -20,14 +20,15 @@ include ../Makefile.aws_array_list
 
 # This is the minimum bound to reach full coverage rate
 UNWINDSET += __CPROVER_file_local_array_list_c_aws_array_list_mem_swap.0:$(shell echo $$(($(MAX_ITEM_SIZE) + 1)))
+UNWINDSET += memcpy_impl.0:$(shell echo $$(($(MAX_ITEM_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_havoc.c
+DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
 DEPENDENCIES += $(SRCDIR)/source/array_list.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 DEPENDENCIES += $(SRCDIR)/source/priority_queue.c

.cbmc-batch/jobs/aws_priority_queue_s_swap/aws_priority_queue_s_swap_harness.c

@@ -43,9 +43,36 @@ void aws_priority_queue_s_swap_harness() {
             can_fail_malloc(sizeof(struct aws_priority_queue_node));
     }
 
+    /* save current state of the data structure */
+    struct aws_array_list old = queue.container;
+    struct store_byte_from_buffer old_byte;
+    save_byte_from_array((uint8_t *)old.data, old.current_size, &old_byte);
+
+    size_t item_sz = queue.container.item_size;
+    size_t offset;
+    __CPROVER_assume(offset < item_sz);
+    /* save a byte of the element at index a */
+    struct store_byte_from_buffer old_a_byte;
+    old_a_byte.index = a * item_sz + offset;
+    old_a_byte.byte = ((uint8_t *)queue.container.data)[old_a_byte.index];
+
+    /* save a byte of the element at index b */
+    struct store_byte_from_buffer old_b_byte;
+    old_b_byte.index = b * item_sz + offset;
+    old_b_byte.byte = ((uint8_t *)queue.container.data)[old_b_byte.index];
+
     /* Perform operation under verification */
     __CPROVER_file_local_priority_queue_c_s_swap(&queue, a, b);
 
     /* Assert the postconditions */
     assert(aws_priority_queue_is_valid(&queue));
+
+    /* All the elements in the container except for a and b should stay unchanged */
+    size_t ob_i = old_byte.index;
+    if (ob_i < a * item_sz && ob_i >= (a + 1) * item_sz && ob_i < b * item_sz && ob_i >= (b + 1) * item_sz) {
+        assert_array_list_equivalence(&queue.container, &old, &old_byte);
+    }
+    /* The new element at index a must be equal to the old element in index b and vice versa */
+    assert(old_a_byte.byte == ((uint8_t *)queue.container.data)[old_b_byte.index]);
+    assert(old_b_byte.byte == ((uint8_t *)queue.container.data)[old_a_byte.index]);
 }

.cbmc-batch/jobs/aws_priority_queue_s_swap/cbmc-batch.yaml

@@ -1,4 +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;__CPROVER_file_local_array_list_c_aws_array_list_mem_swap.0:3;--object-bits;8"
+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;__CPROVER_file_local_array_list_c_aws_array_list_mem_swap.0:3,memcpy_impl.0:3;--object-bits;8"
 goto: aws_priority_queue_s_swap_harness.goto
 expected: "SUCCESSFUL"

.cbmc-batch/stubs/s_swap_override_no_op.c

@@ -0,0 +1,47 @@
+/*
+ * 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.
+ */
+
+/**
+ * FUNCTION: s_swap
+ *
+ * This function overrides s_swap and only swaps the backpointer
+ * indexes. It is used to improve the running time of the CBMC proofs,
+ * as this function adds heavy overhead on the proofs, especially the
+ * ones that loop over the elements of the priority queue (such as
+ * s_sift_up, s_sift_down, s_sift_either).
+ *
+ * It is safe to stub s_swap out, as long as no assertions about the
+ * values of the elements in the priority queue are made
+ * afterwards. Therefore, this stub cannot be used in proofs about the
+ * order of the elements in the priority queue, or any other
+ * functional correctness property concerning the values of the
+ * elements in the queue.
+ *
+ */
+
+#include <aws/common/priority_queue.h>
+
+void __CPROVER_file_local_priority_queue_c_s_swap(struct aws_priority_queue *queue, size_t a, size_t b) {
+    assert(aws_priority_queue_is_valid(queue));
+    assert(a < queue->container.length);
+    assert(b < queue->container.length);
+    assert(aws_priority_queue_backpointer_index_valid(queue, a));
+    assert(aws_priority_queue_backpointer_index_valid(queue, b));
+
+    if (queue->backpointers.data) {
+        assert(queue->backpointers.length > a);
+        assert(queue->backpointers.length > b);
+    }
+}

include/aws/common/priority_queue.h

@@ -91,6 +91,26 @@ void aws_priority_queue_init_static(
     size_t item_size,
     aws_priority_queue_compare_fn *pred);
 
+/**
+ * Checks that the backpointer at a specific index of the queue is
+ * NULL or points to a correctly allocated aws_priority_queue_node.
+ */
+bool aws_priority_queue_backpointer_index_valid(const struct aws_priority_queue *const queue, size_t index);
+
+/**
+ * Checks that the backpointers of the priority queue are either NULL
+ * or correctly allocated to point at aws_priority_queue_nodes. This
+ * check is O(n), as it accesses every backpointer in a loop, and thus
+ * shouldn't be used carelessly.
+ */
+bool aws_priority_queue_backpointers_valid_deep(const struct aws_priority_queue *const queue);
+
+/**
+ * Checks that the backpointers of the priority queue satisfy validity
+ * constraints.
+ */
+bool aws_priority_queue_backpointers_valid(const struct aws_priority_queue *const queue);
+
 /**
  * Set of properties of a valid aws_priority_queue.
  */

source/priority_queue.c

@@ -25,6 +25,8 @@ static void s_swap(struct aws_priority_queue *queue, size_t a, size_t b) {
     AWS_PRECONDITION(aws_priority_queue_is_valid(queue));
     AWS_PRECONDITION(a < queue->container.length);
     AWS_PRECONDITION(b < queue->container.length);
+    AWS_PRECONDITION(aws_priority_queue_backpointer_index_valid(queue, a));
+    AWS_PRECONDITION(aws_priority_queue_backpointer_index_valid(queue, b));
 
     aws_array_list_swap(&queue->container, a, b);
 
@@ -49,6 +51,8 @@ static void s_swap(struct aws_priority_queue *queue, size_t a, size_t b) {
         }
     }
     AWS_POSTCONDITION(aws_priority_queue_is_valid(queue));
+    AWS_POSTCONDITION(aws_priority_queue_backpointer_index_valid(queue, a));
+    AWS_POSTCONDITION(aws_priority_queue_backpointer_index_valid(queue, b));
 }
 
 /* Precondition: with the exception of the given root element, the container must be
@@ -180,15 +184,35 @@ void aws_priority_queue_init_static(
     AWS_POSTCONDITION(aws_priority_queue_is_valid(queue));
 }
 
-bool aws_priority_queue_is_valid(const struct aws_priority_queue *const queue) {
-    /* Pointer validity checks */
+bool aws_priority_queue_backpointer_index_valid(const struct aws_priority_queue *const queue, size_t index) {
+    if (queue->backpointers.data == NULL) {
+        return true;
+    }
+    if (index < queue->backpointers.length) {
+        struct aws_priority_queue_node *node = ((struct aws_priority_queue_node **)queue->backpointers.data)[index];
+        return (node == NULL) || AWS_MEM_IS_WRITABLE(node, sizeof(struct aws_priority_queue_node));
+    }
+    return false;
+}
+
+bool aws_priority_queue_backpointers_valid_deep(const struct aws_priority_queue *const queue) {
     if (!queue) {
         return false;
     }
-    bool pred_is_valid = (queue->pred != NULL);
+    for (size_t i = 0; i < queue->backpointers.length; i++) {
+        if (!aws_priority_queue_backpointer_index_valid(queue, i)) {
+            return false;
+        }
+    }
+    return true;
+}
 
-    /* Internal container validity checks */
-    bool container_is_valid = aws_array_list_is_valid(&queue->container);
+bool aws_priority_queue_backpointers_valid(const struct aws_priority_queue *const queue) {
+    if (!queue) {
+        return false;
+    }
+
+    /* Internal container validity */
     bool backpointer_list_is_valid = aws_array_list_is_valid(&queue->backpointers);
 
     /* Backpointer struct should either be zero or should be
@@ -198,12 +222,33 @@ bool aws_priority_queue_is_valid(const struct aws_priority_queue *const queue) {
     bool backpointer_list_item_size = queue->backpointers.item_size == sizeof(struct aws_priority_queue_node *);
     bool lists_equal_lengths = queue->backpointers.length == queue->container.length;
     bool backpointers_non_zero_current_size = queue->backpointers.current_size > 0;
+
+    /* This check must be guarded, as it is not efficient, neither
+     * when running tests nor CBMC */
+#if (AWS_DEEP_CHECKS == 1)
+    bool backpointers_valid_deep = aws_priority_queue_backpointers_valid_deep(queue);
+#else
+    bool backpointers_valid_deep = true;
+#endif
     bool backpointers_zero =
         (queue->backpointers.current_size == 0 && queue->backpointers.length == 0 && queue->backpointers.data == NULL);
     bool backpointer_struct_is_valid =
-        backpointers_zero || (backpointer_list_item_size && lists_equal_lengths && backpointers_non_zero_current_size);
+        backpointers_zero || (backpointer_list_item_size && lists_equal_lengths && backpointers_non_zero_current_size &&
+                              backpointers_valid_deep);
+
+    return backpointer_list_is_valid && backpointer_struct_is_valid;
+}
+
+bool aws_priority_queue_is_valid(const struct aws_priority_queue *const queue) {
+    /* Pointer validity checks */
+    if (!queue) {
+        return false;
+    }
+    bool pred_is_valid = (queue->pred != NULL);
+    bool container_is_valid = aws_array_list_is_valid(&queue->container);
 
-    return pred_is_valid && container_is_valid && backpointer_list_is_valid && backpointer_struct_is_valid;
+    bool backpointers_valid = aws_priority_queue_backpointers_valid(queue);
+    return pred_is_valid && container_is_valid && backpointers_valid;
 }
 
 void aws_priority_queue_clean_up(struct aws_priority_queue *queue) {