https://gcc.gnu.org/bugzilla/show_bug.cgi?id=122063
Bug ID: 122063
Summary: Unexpected overflow check before fixed-point
multiplication
Product: gcc
Version: 15.2.1
Status: UNCONFIRMED
Severity: normal
Priority: P3
Component: ada
Assignee: unassigned at gcc dot gnu.org
Reporter: d.van.raaij at gmail dot com
CC: dkm at gcc dot gnu.org
Target Milestone: ---
While experimenting with fixed-point arithmetic in SPARK/Ada, I found that
GNATprove claims subprogram `Divide_By_10' shown below to be free of run-time
errors while this is not the case after compiling the code with GNAT. At this
point, it's not completely clear to me whether the issue is with GNATprove or
GNAT, but I tend to think that that GNATprove is correct and that the issue is
with GNAT.
The subprogram converts a 32-bit unsigned integer `V' into a 32-bit wide
fixed-point typed variable `R1'. The type of `R1', `Q32_0', is defined to have
no fractional digits so its range should match the range of type `Unsigned_32`.
This is asserted by GNATprove. The converted value `R1' is then multiplied by a
value `C' of type `Q0_32'. This type ranges only from 0.0 to 1.0
(non-inclusive). The result of the multiplication is then stored in a 64-bit
wide variable of type `Q32_32'. This type contains the values `Q32_0' as an
exact subset. Now, as the multiplication involves only an integer between 0 and
2**32 (non-inclusive) and a value between 0.0 and 1.0 (non-inclusive), I tend
to think that the operation cannot overflow if the type of the result also
ranges from 0 to 2**32 (non-inclusive).
When looking at the assembly output, it is clear that GNAT disagrees and does
insert an overflow check. Values that are equal-or-larger than 16#A000_0000#
(larger than "-1610612737" in the disassembly below) cause a Constrain_Error to
appear.
Incidentally, increasing the size of type `Q0_32' from 32 to 33 causes the
overflow check disappear while the assembly performing the arithmetic
operations remains the same.
**divide_by_10.adb**
with Interfaces; use Interfaces;
function Divide_By_10 (V : Unsigned_32) return Unsigned_32 with SPARK_Mode Is
type Q0_32 is delta 2.0 ** (-32) range 0.0 .. 2.0 ** 0 - 2.0 ** (-32)
with Size => 32, Small => 2.0 ** (-32);
type Q32_0 is delta 2.0 ** ( 0) range 0.0 .. 2.0 ** 32 - 2.0 ** ( 0)
with Size => 32, Small => 2.0 ** (0);
type Q32_32 is delta 2.0 ** (-32) range 0.0 .. 2.0 ** 32 - 2.0 ** (-32)
with Size => 64, Small => 2.0 ** (-32);
C : constant Q0_32 := 4.0 / 5.0 + Q0_32'Small; -- 16#CCCC_CCCD#;
R1 : constant Q32_0 := Q32_0 (V);
R2 : constant Q32_32 := C * R1; -- C * U64 (V)
begin
pragma Assert (for all N in Unsigned_32'Range => N = Unsigned_32 (Q32_0
(N)));
pragma Assert (for all N in Unsigned_32'Range => N = Unsigned_32 (Q32_32
(N)));
return Unsigned_32 (R2) / 8; -- Shift_Right (R2, U32'Size + 3);
end Divide_By_10;
**output** (GNATprove FSF 15)
$ gnatprove --level=2 --report=provers divide_by_10.adb
No project file given, using default.gpr
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
divide_by_10.adb:3:10: info: implicit aspect Always_Terminates on
"Divide_By_10" has been proved, subprogram will terminate
divide_by_10.adb:13:35: info: range check proved (CVC5: 1 VC; Z3: 1 VC)
divide_by_10.adb:14:30: info: overflow check proved (CVC5: 2 VC)
divide_by_10.adb:14:30: info: range check proved (CVC5: 2 VC)
divide_by_10.adb:17:19: info: assertion proved (Z3: 1 VC)
divide_by_10.adb:17:70: info: range check proved (Z3: 1 VC)
divide_by_10.adb:17:78: info: range check proved (CVC5: 1 VC; Z3: 1 VC)
divide_by_10.adb:18:19: info: assertion proved (altergo: 1 VC)
divide_by_10.adb:18:70: info: range check proved (altergo: 1 VC)
divide_by_10.adb:18:78: info: range check proved (CVC5: 1 VC; Z3: 1 VC)
divide_by_10.adb:20:24: info: range check proved (Z3: 1 VC)
divide_by_10.adb:20:28: info: division check proved (CVC5: 1 VC)
Summary logged in /home/dvraaij/fixp/gnatprove/gnatprove.out
**output** (disassembly)
$ gcc -O2 -S -masm=intel -c divide_by_10.adb -o -
[...]
_ada_divide_by_10:
.LFB1:
.cfi_startproc
cmp edi, -1610612737 <<< Overflow check
ja .L7
mov eax, edi
mov edx, 3435973837
imul rax, rdx
shr rax, 35
ret
.L7:
push rax
.cfi_def_cfa_offset 16
mov esi, 14
mov edi, OFFSET FLAT:.LC0
call __gnat_rcheck_CE_Overflow_Check
.cfi_endproc
[...]
**output** (GCC version)
$ gcc -v
Using built-in specs.
COLLECT_GCC=/usr/bin/gcc
COLLECT_LTO_WRAPPER=/usr/libexec/gcc/x86_64-redhat-linux/15/lto-wrapper
OFFLOAD_TARGET_NAMES=nvptx-none:amdgcn-amdhsa
OFFLOAD_TARGET_DEFAULT=1
Target: x86_64-redhat-linux
Configured with: ../configure --enable-bootstrap
--enable-languages=c,c++,fortran,objc,obj-c++,ada,go,d,m2,cobol,lto
--prefix=/usr --mandir=/usr/share/man --infodir=/usr/share/info
--with-bugurl=http://bugzilla.redhat.com/bugzilla --enable-shared
--enable-threads=posix --enable-checking=release --enable-multilib
--with-system-zlib --enable-__cxa_atexit --disable-libunwind-exceptions
--enable-gnu-unique-object --enable-linker-build-id
--with-gcc-major-version-only --enable-libstdcxx-backtrace
--with-libstdcxx-zoneinfo=/usr/share/zoneinfo --with-linker-hash-style=gnu
--enable-plugin --enable-initfini-array
--with-isl=/builddir/build/BUILD/gcc-15.2.1-build/gcc-15.2.1-20250808/obj-x86_64-redhat-linux/isl-install
--enable-offload-targets=nvptx-none,amdgcn-amdhsa --enable-offload-defaulted
--without-cuda-driver --enable-gnu-indirect-function --enable-cet
--with-tune=generic --with-arch_32=i686 --build=x86_64-redhat-linux
--with-build-config=bootstrap-lto --enable-link-serialization=1
Thread model: posix
Supported LTO compression algorithms: zlib zstd
gcc version 15.2.1 20250808 (Red Hat 15.2.1-1) (GCC)
