All AWS-C-Common tasks redefine library functions (undefined behavior)

[PhilippWendler]

All tasks in c/aws-c-common define functions with a name that is also the name of a standard library function (e.g., abort or memcpy). This is undefined behavior, which follows from § 7.1.3 of the C11 standard.

In the past we did take action in such cases and removed or renamed the offending declarations (examples d2c4a04 of #572, b71c984, and 918cb36).

However, for a library like AWS C Common implementing such functions might make sense, and we could also change the rules accordingly to allow this (if a function body is given, that would take precedence, otherwise the semantics defined by the standard should be used).

On the other hand, those tasks that are actually intended to model implementations of standard functions (mempy_*.i and memset_*.i) do not contain problematic functions for the respective functions, they use different identifiers. So there seems toe exist little reason why we should allow this in other tasks.

Furthermore, I am not sure whether tools that are based on compilers might have a problem with the existence of such definitions.

Anyway, all tasks contain a definition of abort (which calls __VERIFIER_error). Note that already the existence of such a definition is enough to cause undefined behavior. However, I also checked in which tasks abort is syntactically reachable according to CPAchecker to see whether me might be able to just delete this function. It is used in these 10 tasks:

aws_priority_queue_pop_harness.i
aws_priority_queue_push_harness.i
aws_priority_queue_push_ref_harness.i
aws_priority_queue_remove_harness.i
aws_ring_buffer_acquire_harness.i
aws_ring_buffer_acquire_up_to_harness.i
aws_ring_buffer_buf_belongs_to_pool_harness.i
aws_ring_buffer_clean_up_harness.i
aws_ring_buffer_init_harness.i
aws_ring_buffer_release_harness.i

The function qsort is defined (and used) in only one task:

aws_array_list_sort_harness.i

The following 53 tasks contain a definition of memcpy, memmove or memset (I checked with grep -Rl '^void \*\(memcpy\|memmove\|memset\)(.*{' *.i):

aws_array_list_back_harness.i
aws_array_list_copy_harness.i
aws_array_list_ensure_capacity_harness.i
aws_array_list_erase_harness.i
aws_array_list_front_harness.i
aws_array_list_get_at_harness.i
aws_array_list_get_at_ptr_harness.i
aws_array_list_pop_back_harness.i
aws_array_list_pop_front_harness.i
aws_array_list_pop_front_n_harness.i
aws_array_list_push_back_harness.i
aws_array_list_set_at_harness.i
aws_array_list_shrink_to_fit_harness.i
aws_array_list_swap_harness.i
aws_byte_buf_advance_harness.i
aws_byte_buf_append_dynamic_harness.i
aws_byte_buf_append_harness.i
aws_byte_buf_append_with_lookup_harness.i
aws_byte_buf_clean_up_harness.i
aws_byte_buf_clean_up_secure_harness.i
aws_byte_buf_init_copy_from_cursor_harness.i
aws_byte_buf_init_copy_harness.i
aws_byte_buf_reserve_harness.i
aws_byte_buf_reserve_relative_harness.i
aws_byte_buf_reset_harness.i
aws_byte_buf_secure_zero_harness.i
aws_byte_buf_write_be16_harness.i
aws_byte_buf_write_be32_harness.i
aws_byte_buf_write_be64_harness.i
aws_byte_buf_write_from_whole_buffer_harness.i
aws_byte_buf_write_from_whole_cursor_harness.i
aws_byte_buf_write_u8_harness.i
aws_hash_table_clean_up_harness.i
aws_hash_table_clear_harness.i
aws_hash_table_create_harness.i
aws_hash_table_init_unbounded_harness.i
aws_hash_table_put_harness.i
aws_hash_table_remove_harness.i
aws_priority_queue_capacity_harness.i
aws_priority_queue_clean_up_harness.i
aws_priority_queue_init_dynamic_harness.i
aws_priority_queue_init_static_harness.i
aws_priority_queue_pop_harness.i
aws_priority_queue_push_harness.i
aws_priority_queue_push_ref_harness.i
aws_priority_queue_remove_harness.i
aws_priority_queue_size_harness.i
aws_priority_queue_s_remove_node_harness.i
aws_priority_queue_s_sift_down_harness.i
aws_priority_queue_s_sift_either_harness.i
aws_priority_queue_s_sift_up_harness.i
aws_priority_queue_s_swap_harness.i
aws_priority_queue_top_harness.i

One of these three functions is syntactically reachable in these 37 tasks:

aws_array_list_back_harness.i
aws_array_list_copy_harness.i
aws_array_list_ensure_capacity_harness.i
aws_array_list_erase_harness.i
aws_array_list_front_harness.i
aws_array_list_get_at_harness.i
aws_array_list_pop_back_harness.i
aws_array_list_pop_front_harness.i
aws_array_list_pop_front_n_harness.i
aws_array_list_push_back_harness.i
aws_array_list_set_at_harness.i
aws_array_list_shrink_to_fit_harness.i
aws_array_list_swap_harness.i
aws_byte_buf_advance_harness.i
aws_byte_buf_append_dynamic_harness.i
aws_byte_buf_append_harness.i
aws_byte_buf_clean_up_secure_harness.i
aws_byte_buf_init_copy_from_cursor_harness.i
aws_byte_buf_init_copy_harness.i
aws_byte_buf_reset_harness.i
aws_byte_buf_secure_zero_harness.i
aws_byte_buf_write_be16_harness.i
aws_byte_buf_write_be32_harness.i
aws_byte_buf_write_be64_harness.i
aws_byte_buf_write_from_whole_buffer_harness.i
aws_byte_buf_write_from_whole_cursor_harness.i
aws_byte_buf_write_u8_harness.i
aws_hash_table_clean_up_harness.i
aws_hash_table_clear_harness.i
aws_hash_table_remove_harness.i
aws_priority_queue_clean_up_harness.i
aws_priority_queue_init_dynamic_harness.i
aws_priority_queue_init_static_harness.i
aws_priority_queue_pop_harness.i
aws_priority_queue_push_harness.i
aws_priority_queue_push_ref_harness.i
aws_priority_queue_remove_harness.i

@gernst What is the best way to fix these problems using the build system that creates the tasks from the original files?

[gernst]

Let's keep the issue open until we have automated the renaming. I cannot promise, however, when I will be able to do this.