smtgcc mid-year update

[Krister Walfridsson]

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/