Byte update with a symbolic size starting mid-element never writes the following element (unsound)

[bardiharborow]

CBMC version: 6.11.0 (cbmc-6.11.0)
Operating system: macOS 26.3, arm64
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: all three assertions pass
What happened instead: assertions 2 and 3 fail

#include <stdint.h>
#include <string.h>

int main()
{
  unsigned n;
  __CPROVER_assume(n == 3 || n == 4);
  unsigned char src[4] = {0xAA, 0xBB, 0xCC, 0xDD};
  uint32_t dst[2] = {0, 0};
  memcpy((unsigned char *)dst + 2, src, n);
  unsigned char *b = (unsigned char *)dst;
  __CPROVER_assert(b[2] == 0xAA && b[3] == 0xBB, "first element copied");
  __CPROVER_assert(b[4] == 0xCC, "byte 4 copied");
  __CPROVER_assert(n != 4 || b[5] == 0xDD, "byte 5 copied");
}

[main.assertion.1] line 15 first element copied: SUCCESS
[main.assertion.2] line 16 byte 4 copied: FAILURE
[main.assertion.3] line 17 byte 5 copied: FAILURE
VERIFICATION FAILED

The copy starts at byte 2 of dst[0] and writes 3 or 4 bytes, so bytes 4 and, for n == 4, 5 belong to dst[1]. CBMC finds a trace in which dst[1] keeps its old value. The result is unsound.

Which cases are affected

The copy size must be symbolic, the destination must be an array of multi-byte elements, and the copy must start at a non-zero offset inside an element such that the update reaches one element further than ceil(n / sizeof(element)) elements. memcpy, memmove, memset and __CPROVER_array_replace are all affected.

Cause

Symex produces a byte_update whose value has a non-constant size. The lowering goes to lower_byte_update_array_vector_unbounded. The index of the last updated element is computed from the size alone (L1717 to L1728):

last_index = first_index + (bound + subtype_size - 1) / subtype_size - 1

This does not include the offset of the update inside the first element (update_offset = src.offset() mod subtype_size, computed in the caller at L1823). With offset 2 and n == 3 the update covers bytes 2 to 4 and therefore elements 0 and 1, but last_index is 0. The comprehension's upper bound (L1742) then excludes every index from 1 onwards, so dst[1] is never written.

The correct value is first_index + (update_offset + bound - 1) / subtype_size, or equivalently first_index + ceil((bound - initial_bytes) / subtype_size) with initial_bytes = min(subtype_size - update_offset, bound), which is already available in this function.

Note that including the element is not enough on its own: the value of the last element is computed by a byte update at a negative offset that the bit-vector lowering cannot apply (see the sibling issue), so both need to be fixed together for this example to pass.