mirror of
https://github.com/Z3Prover/z3
synced 2026-07-24 07:52:33 +00:00
0105b220fd
`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 <kiro-agent@users.noreply.github.com>
95 lines
2.4 KiB
C++
95 lines
2.4 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
hash.cpp
|
|
|
|
Abstract:
|
|
|
|
Basic hash computation support.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2006-09-11.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
|
|
#include "util/debug.h"
|
|
#include "util/hash.h"
|
|
#include <string.h>
|
|
|
|
static unsigned read_unsigned(const char *s) {
|
|
unsigned n;
|
|
memcpy(&n, s, sizeof(unsigned));
|
|
return n;
|
|
}
|
|
|
|
// I'm using Bob Jenkin's hash function.
|
|
// http://burtleburtle.net/bob/hash/doobs.html
|
|
unsigned string_hash(std::string_view str, unsigned init_value) {
|
|
unsigned a, b, c, len;
|
|
const char * data = str.data();
|
|
unsigned length = static_cast<unsigned>(str.length());
|
|
|
|
/* Set up the internal state */
|
|
len = length;
|
|
a = b = 0x9e3779b9; /* the golden ratio; an arbitrary value */
|
|
c = init_value; /* the previous hash value */
|
|
|
|
/*---------------------------------------- handle most of the key */
|
|
SASSERT(sizeof(unsigned) == 4);
|
|
while (len >= 12) {
|
|
a += read_unsigned(data);
|
|
b += read_unsigned(data+4);
|
|
c += read_unsigned(data+8);
|
|
mix(a,b,c);
|
|
data += 12; len -= 12;
|
|
}
|
|
|
|
/*------------------------------------- handle the last 11 bytes */
|
|
c += length;
|
|
switch(len) { /* all the case statements fall through */
|
|
case 11:
|
|
c+=((unsigned)(unsigned char)data[10]<<24);
|
|
Z3_fallthrough;
|
|
case 10:
|
|
c+=((unsigned)(unsigned char)data[9]<<16);
|
|
Z3_fallthrough;
|
|
case 9 :
|
|
c+=((unsigned)(unsigned char)data[8]<<8);
|
|
Z3_fallthrough;
|
|
/* the first byte of c is reserved for the length */
|
|
case 8 :
|
|
b+=((unsigned)(unsigned char)data[7]<<24);
|
|
Z3_fallthrough;
|
|
case 7 :
|
|
b+=((unsigned)(unsigned char)data[6]<<16);
|
|
Z3_fallthrough;
|
|
case 6 :
|
|
b+=((unsigned)(unsigned char)data[5]<<8);
|
|
Z3_fallthrough;
|
|
case 5 :
|
|
b+=(unsigned char)data[4];
|
|
Z3_fallthrough;
|
|
case 4 :
|
|
a+=((unsigned)(unsigned char)data[3]<<24);
|
|
Z3_fallthrough;
|
|
case 3 :
|
|
a+=((unsigned)(unsigned char)data[2]<<16);
|
|
Z3_fallthrough;
|
|
case 2 :
|
|
a+=((unsigned)(unsigned char)data[1]<<8);
|
|
Z3_fallthrough;
|
|
case 1 :
|
|
a+=(unsigned char)data[0];
|
|
/* case 0: nothing left to add */
|
|
break;
|
|
}
|
|
mix(a,b,c);
|
|
/*-------------------------------------------- report the result */
|
|
return c;
|
|
}
|
|
|