`memmove` and `memcpy` of non-bool type with symbolic count fails

[zhuyutian57]

I try to write a harness program to prove the correctness of memmove and memcpy with symbolic count. The program is shown below.

HARNESS_MEMMOVE creates an array with length 10 and initializes its elements one by one via nondet_int. Then, two pointers src_ptr and dst_ptr are created. The assumptions set the constraints for memmove. Then, memmove(dst_ptr, src_ptr, count * sizeof(TYPE)) is executed.

The verification task is to verify the destination memory holds the copied content. Thus, before memmove, src_value caches the copied values in src_ptr[i] where i is a non-deterministic location in [src_index, src_index + count). After memmove, the assertion check src_value = dst_ptr[i].

HARNESS_MEMCPY does the same things with two different arrays, which already guarantees that the memories are disjoint.

The program is expected to be successfully verified, regardless of the TYPE value. However, the verification only succeeds for the bool type and fails for the integer type. Why?

#include <assert.h>
#include <string.h>
#include <stdint.h>
#include <stdbool.h>
#include <limits.h>

// Declare CBMC non-deterministic function
int nondet_int(void);

// Generic harness function macro
#define HARNESS_MEMMOVE(TYPE, ARRAY_SIZE) \
void harness_memmove_##TYPE(void) { \
    /* Create an array */ \
    TYPE array[ARRAY_SIZE] = {0}; \
    for (int i = 0; i < ARRAY_SIZE; i++) { \
        array[i] = (TYPE)nondet_int(); \
    } \
    \
    /* Create two non-deterministic pointers that locate inside the array */ \
    int src_index = nondet_int(); \
    __CPROVER_assume(src_index >= 0 && src_index < ARRAY_SIZE); \
    TYPE *src_ptr = &array[src_index]; \
    \
    int dst_index = nondet_int(); \
    __CPROVER_assume(dst_index >= 0 && dst_index < ARRAY_SIZE); \
    TYPE *dst_ptr = &array[dst_index]; \
    \
    /* Symbolic count for copy */ \
    int count = nondet_int(); \
    \
    /* Pre-conditions: ensure we can copy count elements */ \
    __CPROVER_assume(count >= 0); \
    /* Ensure source has enough elements */ \
    __CPROVER_assume(count <= ARRAY_SIZE - src_index); \
    /* Ensure destination has enough space */ \
    __CPROVER_assume(count <= ARRAY_SIZE - dst_index); \
    \
    /* Set source value before copy (for verification) */ \
    int i = nondet_int(); \
    __CPROVER_assume(i >= 0 && i < count); \
    TYPE src_value = src_ptr[i]; \
    \
    /* Perform copy: copy count elements from src to dst */ \
    memmove(dst_ptr, src_ptr, count * sizeof(TYPE)); \
    \
    /* Post-condition: destination should have the copied values */ \
    if (count > 0) { \
        __CPROVER_assert(src_value == dst_ptr[i], "destination should have copied value"); \
    } \
}

// Generic harness function macro for memcpy (non-overlapping using two arrays)
#define HARNESS_MEMCPY(TYPE, ARRAY_SIZE) \
void harness_memcpy_##TYPE(void) { \
    /* Create two separate arrays - guarantees non-overlapping */ \
    TYPE src_array[ARRAY_SIZE] = {0}; \
    TYPE dst_array[ARRAY_SIZE] = {0}; \
    for (int i = 0; i < ARRAY_SIZE; i++) { \
        src_array[i] = (TYPE)nondet_int(); \
        dst_array[i] = (TYPE)nondet_int(); \
    } \
    \
    /* Create two non-deterministic pointers that locate inside their respective arrays */ \
    int src_index = nondet_int(); \
    __CPROVER_assume(src_index >= 0 && src_index < ARRAY_SIZE); \
    TYPE *src_ptr = &src_array[src_index]; \
    \
    int dst_index = nondet_int(); \
    __CPROVER_assume(dst_index >= 0 && dst_index < ARRAY_SIZE); \
    TYPE *dst_ptr = &dst_array[dst_index]; \
    \
    /* Symbolic count for copy */ \
    int count = nondet_int(); \
    \
    /* Pre-conditions: ensure we can copy count elements */ \
    __CPROVER_assume(count >= 0); \
    /* Ensure source has enough elements */ \
    __CPROVER_assume(count <= ARRAY_SIZE - src_index); \
    /* Ensure destination has enough space */ \
    __CPROVER_assume(count <= ARRAY_SIZE - dst_index); \
    /* Non-overlapping is guaranteed by using two separate arrays */ \
    \
    /* Set source value before copy (for verification) */ \
    int i = nondet_int(); \
    __CPROVER_assume(i >= 0 && i < count); \
    TYPE src_value = src_ptr[i]; \
    \
    /* Perform copy: copy count elements from src to dst (non-overlapping) */ \
    memcpy(dst_ptr, src_ptr, count * sizeof(TYPE)); \
    \
    /* Post-condition: destination should have the copied values */ \
    if (count > 0) { \
        __CPROVER_assert(src_value == dst_ptr[i], "destination should have copied value"); \
    } \
}

HARNESS_MEMMOVE(bool, 10)

HARNESS_MEMMOVE(int, 10)

HARNESS_MEMCPY(bool, 10)

HARNESS_MEMCPY(int, 10)

int main() {
    harness_memmove_bool(); // Success
    harness_memmove_int(); // Fail
    harness_memcpy_bool(); // Success
    harness_memcpy_int(); // Fail
    return 0;
}