I have continued working on my translation validator, smtgcc [1]. Here is
an update of what I have done since the end-of-year update.
smtgcc-tv-backend
-----------------
The main focus has been improving the smtgcc-tv-backend tool which checks
that the generated assembly is a refinement of the final GIMPLE IR.
Highlights:
* Implemented most AArch64 SVE instructions
* Implemented most RISC-V vector instructions
* Improved performance
There are still some limitations in the ABI support. This is not too
problematic, as smtgcc reports "not implemented" instead of trying to
analyze, so it avoids false positives. But it does restrict the range of
code it can handle.
The tool also still generates overly complicated SMT formulas for some
common instructions, which makes tests time out unnecessarily.
Add SMTGCC_ASM environment variable
-----------------------------------
The smtgcc-tv-backend tool verifies that the generated assembly is a
refinement of the final GIMPLE IR. It is now possible to override the file
used for reading the assembly by setting the SMTGCC_ASM environment
variable. This is useful for testing the implementation of smtgcc, but can
also be used to verify hand-written assembly by letting smtgcc-tv-backend
compare the GIMPLE from the C function against the provided assembly code
instead of the compiler-generated output.
Caching
-------
smtgcc can now cache SMT queries in a Redis database, and use the cached
result when an identical query is submitted. This speeds up continuous
testing of GCC a lot.
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
* -Os
* -O1
* -O0
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
Please let me know if there are additional configurations you would like
me to include in the testing.
One GCC bug complicates this work: PR118669, which causes smtgcc to report
many spurious vectorization failures for AArch64 and RISC-V. In practice,
this forces me to ignore all failures in the vectorization pass.
Reported GCC bugs
-----------------
Most GCC bugs I have reported have been fixed, but there is currently one
open bug where GCC generates incorrect code: PR113703.
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: PR106883, PR106884, PR109626, PR110760,
PR111257, PR111280, PR111494, PR113590, PR114056, PR118669, PR119720.
Plans
-----
In the coming months, I plan to continue improving the current
functionality. In particular:
* Add the remaining AArch64 and RISC-V instructions
* Implement full ABI support for AArch64 and RISC-V
* Add support for restrict
* Improve handling of uninitialized memory
* Improve handling of pointer provenance
* Fix false positives
* Improve performance
/Krister
[1] https://github.com/kristerw/smtgcc/
