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/

Reply via email to