I have continued working on my translation validator, smtgcc [1]. Here is
an update of the current status.
Performance
-----------
During the last year, I have reduced the number of timeouts in my normal
GCC test runs by about 90%:
* About half of this improvement comes from adding support for the
Bitwuzla SMT solver, which is much faster for the kind of SMT formulas
generated by smtgcc.
* The other half comes from better canonicalization, etc. in the smtgcc
representation.
I have identified many similar optimization opportunities, and I expect
another 90% reduction in the future!
Running smtgcc on real software
-------------------------------
Smtgcc is now good enough to find issues when compiling real-world
software. I have not yet done any large-scale testing, but, for example,
PR125296 and PR125668 were found by compiling the Linux kernel with smtgcc
enabled.
smtgcc-tv-backend
-----------------
The smtgcc-tv-backend tool checks that the generated assembly is a
refinement of the final GIMPLE IR. This now supports:
* AArch64
- Up to -march=armv9.5-a
* RISC-V
- Both RV32 and RV64 targets
- GCB profile
- Partial support for the V extension
* BPF
* SH (limited support)
* m68k (limited support)
GCC testing
-----------
I am continuing with weekly runs of the GCC test suite. The testing is
done with -fno-strict-aliasing and, for AArch64 and RISC-V,
-fno-section-anchors, as type-based aliasing and section anchors are not
yet supported by smtgcc.
The tests are done on optimization levels:
* -O3
* -O2
* -O1
* -O0
* -Os
* -Og
and for the following target flags (where I typically only run a subset of
targets each week):
* x86_64:
- <the default x86_64 arch>
- -march=x86-64-v2
- -march=x86-64-v3
- -march=x86-64-v4
- -m32
* AArch64
- <the default aarch64 arch>
- -march=armv8.9-a
- -march=armv9.5-a
* RISC-V
- -march=rv64gcbv
- -march=rv64gcv
- -march=rv64gcb
- -march=rv64gc
- -march=rv32gcbv
- -march=rv32gcv
- -march=rv32gcb
- -march=rv32gc
* BPF
- -mlittle-endian -mcpu=v4
* SH
- -ml -m4-single
* m68k
- <using the default>
Reported GCC bugs
-----------------
Most GCC bugs I have reported have been fixed, but there is currently
three open bugs where GCC generates incorrect code: PR113703, PR122948,
PR123765.
I have also reported several bugs where optimizations perform invalid
transformations that introduce new undefined behavior, although these do
not, in practice, miscompile code with the current pass ordering. The
following are still open: PR106884, PR109626, PR110760, PR111257,
PR111280, PR113590, PR114032, PR114056, PR119720, PR120980, PR120981,
PR120982, PR124525, PR124526, PR124527, PR125260, PR125295.
Plans
-----
I plan to continue improving the current functionality. In particular:
* Support more __builtin and internal functions.
* Add missing instructions to the assembly checking.
* Add missing ABI support to the assembly checking.
* Improve performance.
/Krister
[1] https://github.com/kristerw/smtgcc/
