On Tue 2025-07-01 20:06:18, Krister Walfridsson via Gcc wrote: > 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.
Seems like work on smtgcc is going nicely. Good to hear! Have you considered -Ofast or some subset of the flags it enables? Perhaps that would uncover a lot of new bugs. I'm not familiar with the flags it enables enough to tell if that wouldn't be more work than it's worth, though. Filip Kastl > > 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/
