Added Linked_list_tests

seahorn/CMakeLists.txt

@@ -119,15 +119,20 @@ add_subdirectory(jobs/byte_cursor_from_buf)
 add_subdirectory(jobs/byte_cursor_from_c_str)
 add_subdirectory(jobs/byte_cursor_from_string)
 add_subdirectory(jobs/linked_list_back)
+add_subdirectory(jobs/linked_list_front)
+add_subdirectory(jobs/linked_list_begin)
+add_subdirectory(jobs/linked_list_end)
 add_subdirectory(jobs/linked_list_remove)
+add_subdirectory(jobs/linked_list_init)
+add_subdirectory(jobs/linked_list_reset)
+add_subdirectory(jobs/linked_list_next)
 add_subdirectory(jobs/linked_list_pop_back)
+add_subdirectory(jobs/linked_list_pop_front)
 add_subdirectory(jobs/linked_list_push_back)
 add_subdirectory(jobs/linked_list_push_front)
 add_subdirectory(jobs/linked_list_swap_contents)
 add_subdirectory(jobs/linked_list_insert_after)
 add_subdirectory(jobs/linked_list_insert_before)
-add_subdirectory(jobs/linked_list_rbegin)
-add_subdirectory(jobs/linked_list_rend)
 add_subdirectory(jobs/string_bytes)
 add_subdirectory(jobs/string_compare)
 add_subdirectory(jobs/string_eq)
@@ -140,4 +145,4 @@ add_subdirectory(jobs/string_eq_c_str_ignore_case)
 add_subdirectory(jobs/string_eq_ignore_case)
 add_subdirectory(jobs/string_new_from_array)
 add_subdirectory(jobs/string_new_from_c_str)
-add_subdirectory(jobs/string_new_from_string)
+add_subdirectory(jobs/string_new_from_string)

seahorn/jobs/linked_list_begin/CMakeLists.txt

@@ -0,0 +1,5 @@
+add_executable(linked_list_begin
+  aws_linked_list_begin_harness.c
+  ${SEA_LIB}/linked_list_helper.c)
+sea_attach_bc(linked_list_begin)
+sea_add_unsat_test(linked_list_begin)

seahorn/jobs/linked_list_begin/aws_linked_list_begin_harness.c

@@ -0,0 +1,25 @@
+#include <seahorn/seahorn.h>
+#include <aws/common/linked_list.h>
+#include <linked_list_helper.h>
+
+int main () {
+    /* data structure */
+    struct aws_linked_list list;
+    size_t size;
+    struct saved_aws_linked_list to_save = {0};
+
+    sea_nd_init_aws_linked_list_from_head(&list, &size);
+    struct aws_linked_list_node *start = list.head.next;
+    aws_linked_list_save_to_tail(&list, size, start, &to_save);
+
+     /* Assume the preconditions. The function requires that list != NULL */
+    assume(size > 0);
+
+    /* perform operation under verification */
+    struct aws_linked_list_node *rval = aws_linked_list_begin(&list);
+
+    /* assertions */
+    sassert(rval == start);
+    sassert(is_aws_list_unchanged_to_tail(&list, &to_save));
+    return 0;
+}

seahorn/jobs/linked_list_end/CMakeLists.txt

@@ -0,0 +1,5 @@
+add_executable(linked_list_end
+  aws_linked_list_end_harness.c
+  ${SEA_LIB}/linked_list_helper.c)
+sea_attach_bc(linked_list_end)
+sea_add_unsat_test(linked_list_end)

seahorn/jobs/linked_list_end/aws_linked_list_end_harness.c

@@ -0,0 +1,28 @@
+#include <seahorn/seahorn.h>
+#include <aws/common/linked_list.h>
+#include <linked_list_helper.h>
+
+int main() {
+    /* data structure */
+    struct aws_linked_list list;
+    struct saved_aws_linked_list to_save = {0};
+    size_t size;
+
+    sea_nd_init_aws_linked_list_from_tail(&list, &size);
+    struct aws_linked_list_node *start = &list.tail;
+    aws_linked_list_save_to_head(&list, size, start, &to_save);
+
+     /* Assume the preconditions. The function requires that list != NULL */
+    assume(size > 0);
+
+    /* perform operation under verification */
+    struct aws_linked_list_node const *rval = aws_linked_list_end(&list);
+
+    /* assertions */
+    sassert(rval == start);
+    sassert(aws_linked_list_node_prev_is_valid(rval));
+    sassert(rval->next == NULL);
+    sassert(is_aws_list_unchanged_to_head(&list, &to_save));
+
+    return 0;
+}

seahorn/jobs/linked_list_front/CMakeLists.txt

@@ -0,0 +1,5 @@
+add_executable(linked_list_front
+  aws_linked_list_front_harness.c
+  ${SEA_LIB}/linked_list_helper.c)
+sea_attach_bc(linked_list_front)
+sea_add_unsat_test(linked_list_front)

seahorn/jobs/linked_list_front/aws_linked_list_front_harness.c

@@ -0,0 +1,32 @@
+
+#include <seahorn/seahorn.h>
+#include <aws/common/linked_list.h>
+#include <linked_list_helper.h>
+
+
+
+int main() {
+    /* data structure */
+    struct aws_linked_list list;
+    size_t size;
+    struct saved_aws_linked_list to_save = {0};
+
+    sea_nd_init_aws_linked_list_from_head(&list, &size);
+    struct aws_linked_list_node *start = list.head.next;
+    aws_linked_list_save_to_tail(&list, size, start, &to_save);
+
+    /* Assume the preconditions. The function requires that list != NULL */
+    assume(size > 1);
+
+    /* perform operation under verification */
+    struct aws_linked_list_node *front = aws_linked_list_front(&list);
+
+    // -- list is ok
+    sassert(list.head.prev == NULL);
+    sassert(list.tail.next == NULL);
+
+    /* assertions */
+    sassert(start == front);
+    sassert(is_aws_list_unchanged_to_tail(&list, &to_save));
+    return 0;
+}

seahorn/jobs/linked_list_init/CMakeLists.txt

@@ -0,0 +1,13 @@
+# add head and tail to list size.
+MATH(EXPR UNROLL_BOUND "${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE} + 2")
+add_executable(linked_list_init
+  aws_linked_list_init_harness.c
+  ${SEA_LIB}/proof_allocators.c
+  ${SEA_LIB}/linked_list_helper.c)
+target_compile_definitions(linked_list_init
+  # We will use our own function for is_valid check hence AWS_DEEP_CHECK is off
+  PUBLIC AWS_DEEP_CHECKS=0
+  MAX_BUFFER_SIZE=${MAX_BUFFER_SIZE}
+  MAX_LINKED_LIST_ITEM_ALLOCATION=${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE})
+sea_attach_bc(linked_list_init)
+sea_add_unsat_test(linked_list_init)

seahorn/jobs/linked_list_init/aws_linked_list_init_harness.c

@@ -0,0 +1,19 @@
+#include <seahorn/seahorn.h>
+#include <aws/common/linked_list.h>
+#include <linked_list_helper.h>
+
+int main () {
+    /* data structure */
+    struct aws_linked_list list;
+
+    /* perform operation under verification */
+    aws_linked_list_init(&list);
+
+    /* assertions */
+    sassert(sea_aws_linked_list_is_valid(&list, 0));
+    sassert(aws_linked_list_empty(&list));
+    sassert(list.head.next == &list.tail);
+    sassert(list.tail.prev == &list.head);
+
+    return 0;
+}

seahorn/jobs/linked_list_next/CMakeLists.txt

@@ -0,0 +1,13 @@
+# add head and tail to list size.
+MATH(EXPR UNROLL_BOUND "${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE} + 2")
+add_executable(linked_list_next
+  aws_linked_list_next_harness.c
+  ${SEA_LIB}/proof_allocators.c
+  ${SEA_LIB}/linked_list_helper.c)
+target_compile_definitions(linked_list_next
+  # We will use our own function for is_valid check hence AWS_DEEP_CHECK is off
+  PUBLIC AWS_DEEP_CHECKS=0
+  MAX_BUFFER_SIZE=${MAX_BUFFER_SIZE}
+  MAX_LINKED_LIST_ITEM_ALLOCATION=${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE})
+sea_attach_bc(linked_list_next)
+sea_add_unsat_test(linked_list_next)

seahorn/jobs/linked_list_next/aws_linked_list_next_harness.c

@@ -0,0 +1,46 @@
+#include <seahorn/seahorn.h>
+#include <aws/common/linked_list.h>
+#include <linked_list_helper.h>
+
+#include "nondet.h"
+
+int main() {
+    /* data structure */
+    struct aws_linked_list list;
+
+    struct aws_linked_list_node node;  // Preconditions require node to not be NULL
+    struct aws_linked_list_node after; // Preconditions require after to not be NULL
+
+    /* Assume the preconditions */
+    void *front = nd_voidp();
+    void *back = nd_voidp();
+
+    list.head.prev = NULL;
+    list.head.next = nd_voidp();
+    node.prev = front;
+    node.next = &after;
+    after.prev = &node;
+    after.next = back;
+    list.tail.prev = nd_voidp();
+    list.tail.next = NULL;
+
+    /* perform operation under verification */
+    struct aws_linked_list_node *rval = aws_linked_list_next(&node);
+
+    /* assertions */
+    sassert(aws_linked_list_node_next_is_valid(&node));
+    sassert(aws_linked_list_node_prev_is_valid(rval));
+    sassert(rval == &after);
+
+    sassert(rval->prev == &node);
+    sassert(rval->next == back);
+
+    sassert(node.next == rval);
+    sassert(node.prev == front);
+
+    // -- list is ok
+    sassert(list.head.prev == NULL);
+    sassert(list.tail.next == NULL);
+
+    return 0;
+}

seahorn/jobs/linked_list_pop_front/CMakeLists.txt

@@ -0,0 +1,13 @@
+# add head and tail to list size.
+MATH(EXPR UNROLL_BOUND "${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE} + 2")
+add_executable(linked_list_pop_front
+  aws_linked_list_pop_front_harness.c
+  ${SEA_LIB}/proof_allocators.c
+  ${SEA_LIB}/linked_list_helper.c)
+target_compile_definitions(linked_list_pop_front
+  # We will use our own function for is_valid check hence AWS_DEEP_CHECK is off
+  PUBLIC AWS_DEEP_CHECKS=0
+  MAX_BUFFER_SIZE=${MAX_BUFFER_SIZE}
+  MAX_LINKED_LIST_ITEM_ALLOCATION=${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE})
+sea_attach_bc(linked_list_pop_front)
+sea_add_unsat_test(linked_list_pop_front)

seahorn/jobs/linked_list_pop_front/aws_linked_list_pop_front_harness.c

@@ -0,0 +1,41 @@
+#include "nondet.h"
+#include <aws/common/linked_list.h>
+
+#include <seahorn/seahorn.h>
+
+int main(void) {
+  /* data structure */
+  struct aws_linked_list list;
+  size_t size;
+
+  sea_nd_init_aws_linked_list_from_head(&list, &size);
+  assume(size > 0);
+
+  struct aws_linked_list_node *old_head_next = list.head.next->next;
+  struct aws_linked_list_node *old_third_node = list.head.next->next->next;
+  struct aws_linked_list_node *list_tail = list.tail.prev;
+
+  /* perform operation under verification */
+  struct aws_linked_list_node *ret = aws_linked_list_pop_front(&list);
+
+  // -- removed node is detached
+  sassert(ret->next == NULL);
+  sassert(ret->prev == NULL);
+
+  // -- head of list is properly updated
+  sassert(list.head.next == old_head_next);
+
+  // -- list is ok
+  sassert(list.head.prev == NULL);
+  sassert(list.tail.next == NULL);
+
+  sassert(list.head.next == old_third_node);
+
+  // -- accessible memory is not modified
+  if (size > 1)
+    sassert(list.tail.prev == list_tail);
+  else
+    sassert(aws_linked_list_empty(&list));
+
+  return 0;
+}

seahorn/jobs/linked_list_reset/CMakeLists.txt

@@ -0,0 +1,13 @@
+# add head and tail to list size.
+MATH(EXPR UNROLL_BOUND "${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE} + 2")
+add_executable(linked_list_reset
+  aws_linked_list_reset_harness.c
+  ${SEA_LIB}/proof_allocators.c
+  ${SEA_LIB}/linked_list_helper.c)
+target_compile_definitions(linked_list_reset
+  # We will use our own function for is_valid check hence AWS_DEEP_CHECK is off
+  PUBLIC AWS_DEEP_CHECKS=0
+  MAX_BUFFER_SIZE=${MAX_BUFFER_SIZE}
+  MAX_LINKED_LIST_ITEM_ALLOCATION=${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE})
+sea_attach_bc(linked_list_reset)
+sea_add_unsat_test(linked_list_reset)

seahorn/jobs/linked_list_reset/aws_linked_list_reset_harness.c

@@ -0,0 +1,24 @@
+#include <seahorn/seahorn.h>
+#include <aws/common/linked_list.h>
+#include <linked_list_helper.h>
+
+#include "nondet.h"
+
+int main () {
+    /* data structure */
+    struct aws_linked_list_node node; // Preconditions require node to not be NULL
+    void *front = nd_voidp();
+    void *back = nd_voidp();
+    node.next = front;
+    node.prev = back;
+
+    /* perform operation under verification */
+    aws_linked_list_node_reset(&node);
+
+    /* assertions */
+    sassert(AWS_IS_ZEROED(node));
+    sassert(node.next == NULL);
+    sassert(node.prev == NULL);
+
+    return 0;
+}

seahorn/lib/linked_list_helper.c

@@ -278,15 +278,13 @@ void aws_linked_list_save_to_head(struct aws_linked_list *list, size_t size,
   }
 }
 
-void aws_linked_list_attach_after(struct aws_linked_list_node *after,
-                                  struct aws_linked_list_node *to_attach,
-                                  bool directly_attached) {
-  if (directly_attached) {
-    after->next = to_attach;
-    to_attach->prev = after;
+void attach_nodeA_to_nodeB(struct aws_linked_list_node *nodeA, struct aws_linked_list_node *nodeB, bool directlyAttached) {
+  if (directlyAttached) {
+    nodeA->next = nodeB;
+    nodeB->prev = nodeA;
   } else {
-    after->next = nd_voidp();
-    to_attach->prev = nd_voidp();
+    nodeA->next = nd_voidp();
+    nodeB->prev = nd_voidp();
   }
 }