https://gcc.gnu.org/bugzilla/show_bug.cgi?id=127305
Bug ID: 127305
Summary: aarch64-elf: cplxlower -> bitintlower changes memory
for _BitInt mul_overflow store
Product: gcc
Version: 17.0
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: middle-end
Assignee: unassigned at gcc dot gnu.org
Reporter: mikaseianatsu at proton dot me
Target Milestone: ---
For the following defined C program, Smtgcc reports that GCC's cplxlower ->
bitintlower transformation changes the contents of memory.
The issue reproduces with GCC main when targeting aarch64-elf. The same source
did not reproduce the transformation-validation failure on the native
x86_64-pc-linux-gnu build used during triage.
Testcase:
unsigned _BitInt(132) b;
int
main ()
{
__builtin_mul_overflow
(0x1100ffeeddccbbaa998877665544332211wb, 1, &b);
if ((b >> 8) != 0x100ffeeddccbbaa9988776655443322wb)
__builtin_abort ();
}
Expected behavior:
The program is defined.
The multiplication by 1 stores the converted result into the unsigned
_BitInt(132) object b. The original constant is wider than 132 bits, so the
stored value is the low 132 bits:
0x100ffeeddccbbaa998877665544332211
Shifting this value right by 8 bits gives:
0x100ffeeddccbbaa9988776655443322
Therefore the comparison is false and the program should not call
__builtin_abort.
Transformation-validation result:
Running Smtgcc's GIMPLE transformation validator against an aarch64-elf GCC
main build:
SMTGCC_TIMEOUT=5000 SMTGCC_SMT_SOLVER=z3 \
/gcc-main-build-aarch64-elf-tv/gcc/xgcc \
-B/gcc-main-build-aarch64-elf-tv/gcc \
-fplugin=/gcc-main-repro-gcc000025.utmmS0/aarch64-elf/smtgcc-tv.so \
-O2 -fno-strict-aliasing -S \
gcc3.c -o /tmp/gcc3.s
reports:
gcc3.c: In function 'main':
gcc3.c:4:1: note: cplxlower -> bitintlower:
Transformation is not correct (Memory)
.memory = (store ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x00)
#x000300000000001e
#x02)
.ptr = #x000300000000001e
.ptr = #x000300000000001e
src *.ptr: #x00
tgt *.ptr: #x02
src indef: #x00
tgt indef: #x00
tgt ub: false
The minimized testcase does not produce any "Not implemented" diagnostics from
Smtgcc in this run.
The mismatch is reported between cplxlower and bitintlower. The counterexample
shows one byte of memory changing from 0x00 to 0x02, while the target side is
not undefined (tgt ub: false).
The testcase was minimized from a cross-target correctness test derived from
gcc.dg/torture/bitint-95.c. The minimized source reproduces the validator
failure without the fuzzing mutation plugin.
Versions:
GCC source: g:d38b7b34f4dc69f896e1fbd984b859365f3dd282
GCC target: aarch64-elf
Smtgcc source: 0ac7560d44df10b003b703c7e4ee9d17a1a0e496
