Bug: Ultimate C translation generates incorrect Boogie implementation for `memcpy(...)` and `memmove(...)`

[bahnwaerter]

The current C translation generates an incorrect Boogie implementation for the C memory management functions memcpy(...) and memmove(...). This issue can be reproduced with Ultimate Automizer (0.3.1-dev-00d43373f5 with OpenJDK 21.0.9) using any C program that contains at least a memcpy(...) or memmove(...) usage. The generated Boogie implementation for memcpy(...) looks like this, for example:

// [...]
#t~loopctr1359 := 0;
while (#t~loopctr1359 % 18446744073709551616 < size % 18446744073709551616)
{
    call write~unchecked~int(#memory_int[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 4);
    call write~unchecked~int(#memory_int[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 8);
    call write~unchecked~int(#memory_int[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 2);
    call write~unchecked~int(#memory_int[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 4);
    call write~unchecked~real(#memory_real[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 4);
    call write~unchecked~int(#memory_int[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 1);
    call write~unchecked~real(#memory_real[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 8);
    call write~unchecked~int(#memory_int[{ base: src!base + #t~loopctr1359 }], { base: dest!base + #t~loopctr1359 }, 1);
    #t~loopctr1359 := 1 + #t~loopctr1359;
}
// [...]

The incorrect Boogie implementation is generated when using the default C translation (integer mode). The issue is located in the ConstructMemcpyOrMemmove.constructMemcpyOrMemmoveDataLoopAssignment method, where write accesses to the heap memory arrays are generated incorrectly. The write accesses within the loop (for the copy operation) stem from the issue that a write call is generated for each CPrimitive instead for each heap memory array. This incorrect behavior most likely results from the alternative implementation for the C translation in bitvector mode.

The currently generated Boogie implementation has two drawbacks:

• It is unclear whether the implementation of memcpy(...) and memmove(...) is sound.
• The implementation can lead to performance issues during verification.