memcpy/memset through a pointer that may point to one of two arrays of different sizes reads and writes the wrong bytes (spurious failures and unsound results) #9237

Activity

1. repowazdogz-droid commented on Nov 3, 2026

   

   repowazdogz-droid

   on Nov 3, 2026

   More actions

   I reproduced this independently, checking CBMC's verdict against concrete execution.

   False proof. With the issue's unsound.c shape:

   #include <string.h>
   #include <assert.h>
   _Bool nondet_bool(void);
   int main(void) {
     char x[2] = {0, 0};
     char y[1] = {0};
     char src[2] = {1, 2};
     _Bool c = nondet_bool();
     char *p = c ? x : y;
     unsigned long n = (p == x) ? 2 : 1;
     memcpy(p, src, n);
     if (p == x) assert(x[1] == 0); /* false: memcpy wrote 2 there */
     return 0;
   }

   • CBMC 6.11.0 (Homebrew) and develop at 03bd0722: assertion x[1] == 0: SUCCESS, VERIFICATION SUCCESSFUL.
   • The same file built with clang -O0 -fsanitize=address,undefined and nondet_bool() returning 1: Assertion failed: (x[1] == 0), exit 134. With 0 it exits 0.

   spurious.c and the memset variant gave the reverse (CBMC FAILED, both concrete runs exit 0). The swapped and equal-size forms agree with execution.

   Kani. The unsound_copy_into_either_of_two_arrays harness from model-checking/kani#5065, run with Kani 0.67.0 (which bundles CBMC 6.8.0), also reports VERIFICATION SUCCESSFUL, while a plain cargo test of the same body gives x[1] == 2. So it predates 6.11.0.

   Where. This matches the account in the issue. In process_array_expr (src/goto-symex/symex_clean_expr.cpp, lines 42 to 50 at 03bd0722) the false case is byte-extracted to the true case's type and the if takes that type, so when the true case is the smaller object the larger one is truncated. memcpy, memmove and memset all reach it through array_copy, array_replace and array_set.

   Why I'm not proposing a patch. I tried extracting both branches to a covering type (the larger one for constant sizes, a byte array of the maximum size for symbolic sizes). It fixes the three programs above, but on its own it is not safe:

   • On 1,772 generated single-claim programs checked against exhaustive concrete execution, it adds 24 false proofs that the baseline does not have, all with int[1] and char[1] candidates and a non-constant length. They disappear when combined with Fix byte_update lowering for updates of symbolic size #9380. Smallest one: CBMC baseline correctly fails it, the patch alone proves it, and Fix byte_update lowering for updates of symbolic size #9380 alone or with the patch fails it again.

   #include <assert.h>
   #include <string.h>
   
   _Bool nondet_bool(void);
   
   int main(void)
   {
     unsigned char src[4] = {100, 101, 102, 103};
     _Bool c = nondet_bool();
     int t0[1] = {0};
     char t1[1] = {20};
     void *p = c ? (void *)t0 : (void *)t1;
     unsigned long n = c ? 4 : 1;
     memcpy(p, src, n);
     if(c)
       assert(((unsigned char *)t0)[0] == 0);
     return 0;
   }

   • Under --no-simplify it hits an invariant failure on constant-offset writes. Simplifying that size removed the abort but turned those programs into false proofs and false failures.

   My attempted repair is not sound in isolation. Combining it with #9380 eliminated the additional false proofs in my tested corpus, but I have not established that this combination is generally sound. I have not tested #9187.