Krister Walfridsson via Gcc <gcc@gcc.gnu.org> writes: > 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. >
We sometimes get interesting bugs, especially with UBSAN (-fsanitize=undefined), with SAVE_EXPR. PR120471 is one example and PR120837 is another. These two are FE issues though, so may not really be applicable. It might be interesting to try -fhardened occasionally (which wraps up several options that distributions build with). I think anything that introduces instrumentation (so -fprofile-generate may be another candidate, or in a sense, -fnon-call-exceptions) could be interesting. sam
