I have continued working on my translation validator, smtgcc [1], over the
last few months. Here's an update on what has happened since my talk at
the GNU Tools Cauldron [2].
Improvements
------------
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:
* Fixed the RISC-V 64-bit pointer problem, so both RV32 and RV64 now work.
* Fixed lots of corner cases where we failed to parse the assembly.
* Added support for the RISC-V B extensions.
* Added partial support for the RISC-V V extensions.
* Added support for the AArch64 architecture.
AArch64 support is still a bit limited: the ABI is not fully implemented,
and checking is slow and often times out because the current
implementation generates overly complicated SMT formulas for some common
instructions.
Reported GCC bugs
-----------------
Most GCC bugs I have reported have been fixed, but there are currently
three open bugs where GCC generates incorrect code: PR113703, PR117186,
PR118174. I also claim that PR117688 still happens even though it is
marked as resolved -- I will investigate it a bit more before reopening
the PR.
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, PR117927.
GCC testing
-----------
I have been running smtgcc over the GCC test suite weekly, and it seems to
detect a newly introduced bug roughly every month. I plan to continue
doing this in the coming months as well.
But running smtgcc on the test suite is not the best use case for the tool
-- it only detects bugs where the test triggers an unrelated bug compared
to what the test is checking, which should be uncommon. I therefore plan
to start testing by compiling real-world code and doing some fuzzing. One
problem is that this often finds the open bugs mentioned in the previous
section, making it time-consuming to check if each new issue is a repeat.
For example, running yarpgen gives me a few failure reports per day of
PR106883.
/Krister
[1] https://github.com/kristerw/smtgcc/
[2] https://www.youtube.com/watch?v=vrkR7jKcFpw
