From 0105b220fd18c3ea00e8b165ca6be64ec2d2682a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Jul 2026 04:03:48 +0200 Subject: [PATCH] Make string_hash independent of char signedness (#10163) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `string_hash`'s tail-byte handling reads bytes through plain `char`, whose signedness is implementation-defined. On signed-char platforms (x86_64 Linux, macOS) bytes ≥ `0x80` are sign-extended before entering the hash state (e.g. `c+=((unsigned)data[10]<<24);` becomes `c += 0xFF80xxxx` instead of `c += 0x0080xxxx`); on unsigned-char platforms (Linux aarch64) they are not. Hashes of byte strings containing such bytes therefore differ across platforms. This is not just cosmetic: `mpz_manager::hash` feeds the digit arrays of large numerals through `string_hash`, so AST hashes of bit-vector constants like `(_ bv36028797018963968 64)` (= 2^55, whose digit bytes include `0x80`) differ between architectures. AST hashes determine hash table layouts throughout the solver, so preprocessing and search take platform-dependent paths for byte-identical input. Observed impact (Z3 4.15.3 release binaries as well as local gcc-13 builds, identical `.smt2` input generated by CBMC from the [mldsa-native](https://github.com/pq-code-package/mldsa-native) verification suite — quantifiers + arrays + bit-vectors, ~120k lines): | instance | x86_64 | aarch64 | |---|---|---| | instance A | 643 s | 11.7 s | | instance B | 22.8 s | 1578 s | Tracing AST construction on both hosts showed the first divergence at the registration of the numeral `2^55`, whose node hash was `2587296535` on x86_64 vs `808470355` on aarch64, with identical mpz digit arrays; from that point on, hash table iteration orders (and consequently `ctx-simplify` steps, quantifier instantiation order, and case-split order) diverge. With this patch, instance A solves in ~21 s on x86_64 (down from 643 s), matching the aarch64 behaviour class. The fix casts the tail bytes to `unsigned char`, matching the 4-byte-chunk path (which is already signedness-independent via `memcpy` into `unsigned`). Note that hash values on signed-char platforms change for inputs containing bytes ≥ `0x80` (pure-ASCII symbol names are unaffected). (Found while investigating cross-platform proof-time instability reported in diffblue/cbmc#8991.) Co-authored-by: Kiro --- src/util/hash.cpp | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/util/hash.cpp b/src/util/hash.cpp index 9d36dd2238..7084bfb572 100644 --- a/src/util/hash.cpp +++ b/src/util/hash.cpp @@ -53,38 +53,38 @@ unsigned string_hash(std::string_view str, unsigned init_value) { c += length; switch(len) { /* all the case statements fall through */ case 11: - c+=((unsigned)data[10]<<24); + c+=((unsigned)(unsigned char)data[10]<<24); Z3_fallthrough; case 10: - c+=((unsigned)data[9]<<16); + c+=((unsigned)(unsigned char)data[9]<<16); Z3_fallthrough; case 9 : - c+=((unsigned)data[8]<<8); + c+=((unsigned)(unsigned char)data[8]<<8); Z3_fallthrough; /* the first byte of c is reserved for the length */ case 8 : - b+=((unsigned)data[7]<<24); + b+=((unsigned)(unsigned char)data[7]<<24); Z3_fallthrough; case 7 : - b+=((unsigned)data[6]<<16); + b+=((unsigned)(unsigned char)data[6]<<16); Z3_fallthrough; case 6 : - b+=((unsigned)data[5]<<8); + b+=((unsigned)(unsigned char)data[5]<<8); Z3_fallthrough; case 5 : - b+=data[4]; + b+=(unsigned char)data[4]; Z3_fallthrough; case 4 : - a+=((unsigned)data[3]<<24); + a+=((unsigned)(unsigned char)data[3]<<24); Z3_fallthrough; case 3 : - a+=((unsigned)data[2]<<16); + a+=((unsigned)(unsigned char)data[2]<<16); Z3_fallthrough; case 2 : - a+=((unsigned)data[1]<<8); + a+=((unsigned)(unsigned char)data[1]<<8); Z3_fallthrough; case 1 : - a+=data[0]; + a+=(unsigned char)data[0]; /* case 0: nothing left to add */ break; }