Byte update with a symbolic size at a non-zero offset into a scalar overwrites bytes beyond the size (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 four assertions pass
What happened instead: assertions 3 and 4 fail

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

int main()
{
  unsigned n;
  __CPROVER_assume(n == 1 || n == 2);
  unsigned char src[2] = {0xAA, 0xBB};
  uint32_t x = 0x44332211u, orig = x;
  memcpy((unsigned char *)&x + 1, src, n);
  unsigned char *b = (unsigned char *)&x, *o = (unsigned char *)&orig;
  __CPROVER_assert(b[0] == o[0], "byte 0 unchanged");
  __CPROVER_assert(b[1] == 0xAA, "byte 1 copied");
  __CPROVER_assert(n != 1 || b[2] == o[2], "byte 2 unchanged when n == 1");
  __CPROVER_assert(b[3] == o[3], "byte 3 unchanged");
}

[main.assertion.1] line 15 byte 0 unchanged: SUCCESS
[main.assertion.2] line 16 byte 1 copied: SUCCESS
[main.assertion.3] line 17 byte 2 unchanged when n == 1: FAILURE
[main.assertion.4] line 18 byte 3 unchanged: FAILURE
VERIFICATION FAILED

The copy writes one or two bytes starting at byte 1 of x. CBMC finds traces in which byte 3 of x changes for either value of n, and in which byte 2 changes for n == 1. The counterexample has byte 2 equal to the old byte 1 and byte 3 equal to the old byte 2. The result is unsound.

Which cases are affected

The copy size must be symbolic, the target must be a scalar (or the first element of an array, where the error is masked by a separate bug in the array lowering), the offset inside the target must be non-zero, and the size must be smaller than the number of bytes from the offset to the end of the target. memcpy, memmove, memset and __CPROVER_array_replace are all affected. The same code path is also reached through lower_byte_update_single_element whenever an update bound is symbolic.

Cause

Symex produces a byte_update of x at offset 1 whose value has a non-constant size. The lowering goes to the bit-vector case of lower_byte_update. Because the value size is not constant, it instantiates sizeof(x) bytes of the value (L2425) and then, for each byte i, replaces the update byte by the original byte i of x when i >= bound (L2456 to L2475):

update_bytes[i] = i < bound ? value[i] : original[i]

The original bytes are taken from offset 0 of x. The whole update word is then shifted left by the update offset (L2535) and combined with x under a mask that covers all sizeof(x) bytes from the offset. So the substituted original bytes land at position offset + i instead of i. With offset 1 and n == 1, bytes 1 to 3 of x become value[0], original[1], original[2], whereas bytes 2 and 3 must keep original[2] and original[3].

Substituting original bytes is only correct when the offset is zero. Instead, the mask should only cover the bytes below the bound (a concatenation of per-byte masks i < bound ? 0xff : 0x00, in the same byte order as the value), the value should be masked with it, and both should then be shifted by the offset.