diff --git a/seahorn/CMakeLists.txt b/seahorn/CMakeLists.txt index 54fd3d26..2c54e6ec 100644 --- a/seahorn/CMakeLists.txt +++ b/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) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_begin/CMakeLists.txt b/seahorn/jobs/linked_list_begin/CMakeLists.txt new file mode 100644 index 00000000..10bf4a71 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_begin/aws_linked_list_begin_harness.c b/seahorn/jobs/linked_list_begin/aws_linked_list_begin_harness.c new file mode 100644 index 00000000..bd008b96 --- /dev/null +++ b/seahorn/jobs/linked_list_begin/aws_linked_list_begin_harness.c @@ -0,0 +1,25 @@ +#include +#include +#include + +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; +} \ No newline at end of file diff --git a/seahorn/jobs/linked_list_end/CMakeLists.txt b/seahorn/jobs/linked_list_end/CMakeLists.txt new file mode 100644 index 00000000..5321fc21 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_end/aws_linked_list_end_harness.c b/seahorn/jobs/linked_list_end/aws_linked_list_end_harness.c new file mode 100644 index 00000000..fb3455ac --- /dev/null +++ b/seahorn/jobs/linked_list_end/aws_linked_list_end_harness.c @@ -0,0 +1,28 @@ +#include +#include +#include + +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; +} \ No newline at end of file diff --git a/seahorn/jobs/linked_list_front/CMakeLists.txt b/seahorn/jobs/linked_list_front/CMakeLists.txt new file mode 100644 index 00000000..6fc75918 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_front/aws_linked_list_front_harness.c b/seahorn/jobs/linked_list_front/aws_linked_list_front_harness.c new file mode 100644 index 00000000..99223236 --- /dev/null +++ b/seahorn/jobs/linked_list_front/aws_linked_list_front_harness.c @@ -0,0 +1,32 @@ + +#include +#include +#include + + + +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; +} diff --git a/seahorn/jobs/linked_list_init/CMakeLists.txt b/seahorn/jobs/linked_list_init/CMakeLists.txt new file mode 100644 index 00000000..651637d3 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_init/aws_linked_list_init_harness.c b/seahorn/jobs/linked_list_init/aws_linked_list_init_harness.c new file mode 100644 index 00000000..ee864450 --- /dev/null +++ b/seahorn/jobs/linked_list_init/aws_linked_list_init_harness.c @@ -0,0 +1,19 @@ +#include +#include +#include + +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; +} \ No newline at end of file diff --git a/seahorn/jobs/linked_list_next/CMakeLists.txt b/seahorn/jobs/linked_list_next/CMakeLists.txt new file mode 100644 index 00000000..e942b14e --- /dev/null +++ b/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) diff --git a/seahorn/jobs/linked_list_next/aws_linked_list_next_harness.c b/seahorn/jobs/linked_list_next/aws_linked_list_next_harness.c new file mode 100644 index 00000000..558f8243 --- /dev/null +++ b/seahorn/jobs/linked_list_next/aws_linked_list_next_harness.c @@ -0,0 +1,46 @@ +#include +#include +#include + +#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; +} \ No newline at end of file diff --git a/seahorn/jobs/linked_list_pop_front/CMakeLists.txt b/seahorn/jobs/linked_list_pop_front/CMakeLists.txt new file mode 100644 index 00000000..f6d8c9d4 --- /dev/null +++ b/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) diff --git a/seahorn/jobs/linked_list_pop_front/aws_linked_list_pop_front_harness.c b/seahorn/jobs/linked_list_pop_front/aws_linked_list_pop_front_harness.c new file mode 100644 index 00000000..d0f8563a --- /dev/null +++ b/seahorn/jobs/linked_list_pop_front/aws_linked_list_pop_front_harness.c @@ -0,0 +1,41 @@ +#include "nondet.h" +#include + +#include + +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; +} \ No newline at end of file diff --git a/seahorn/jobs/linked_list_rbegin/CMakeLists.txt b/seahorn/jobs/linked_list_rbegin/CMakeLists.txt deleted file mode 100644 index fa88c3a9..00000000 --- a/seahorn/jobs/linked_list_rbegin/CMakeLists.txt +++ /dev/null @@ -1,11 +0,0 @@ -# add head and tail to list size. -add_executable(linked_list_rbegin - aws_linked_list_rbegin_harness.c - ${SEA_LIB}/proof_allocators.c - ${SEA_LIB}/linked_list_helper.c) -target_compile_definitions(linked_list_rbegin - # We will use our own function for is_valid check hence AWS_DEEP_CHECK is off - PUBLIC SEA_DEEP_CHECKS=0 - MAX_LINKED_LIST_ITEM_ALLOCATION=${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE}) -sea_attach_bc(linked_list_rbegin) -sea_add_unsat_test(linked_list_rbegin) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_rend/CMakeLists.txt b/seahorn/jobs/linked_list_rend/CMakeLists.txt deleted file mode 100644 index addebe62..00000000 --- a/seahorn/jobs/linked_list_rend/CMakeLists.txt +++ /dev/null @@ -1,11 +0,0 @@ -# add head and tail to list size. -add_executable(linked_list_rend - aws_linked_list_rend_harness.c - ${SEA_LIB}/proof_allocators.c - ${SEA_LIB}/linked_list_helper.c) -target_compile_definitions(linked_list_rend - # We will use our own function for is_valid check hence AWS_DEEP_CHECK is off - PUBLIC SEA_DEEP_CHECKS=0 - MAX_LINKED_LIST_ITEM_ALLOCATION=${MAX_LINKED_LIST_ITEM_ALLOCATION_SIZE}) -sea_attach_bc(linked_list_rend) -sea_add_unsat_test(linked_list_rend) \ No newline at end of file diff --git a/seahorn/jobs/linked_list_reset/CMakeLists.txt b/seahorn/jobs/linked_list_reset/CMakeLists.txt new file mode 100644 index 00000000..23a82f70 --- /dev/null +++ b/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) diff --git a/seahorn/jobs/linked_list_reset/aws_linked_list_reset_harness.c b/seahorn/jobs/linked_list_reset/aws_linked_list_reset_harness.c new file mode 100644 index 00000000..3b275dd3 --- /dev/null +++ b/seahorn/jobs/linked_list_reset/aws_linked_list_reset_harness.c @@ -0,0 +1,24 @@ +#include +#include +#include + +#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; +} \ No newline at end of file diff --git a/seahorn/lib/linked_list_helper.c b/seahorn/lib/linked_list_helper.c index d411d953..e6e41935 100644 --- a/seahorn/lib/linked_list_helper.c +++ b/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(); } }