smtgcc mid-year update

I have continued working on my translation validator, smtgcc [1]. Here is 
an update of the current status.


Performance
-----------
During the last year, I have reduced the number of timeouts in my normal 
GCC test runs by about 90%:
  * About half of this improvement comes from adding support for the
    Bitwuzla SMT solver, which is much faster for the kind of SMT formulas
    generated by smtgcc.
  * The other half comes from better canonicalization, etc. in the smtgcc
    representation.

I have identified many similar optimization opportunities, and I expect 
another 90% reduction in the future!


Running smtgcc on real software
-------------------------------
Smtgcc is now good enough to find issues when compiling real-world 
software. I have not yet done any large-scale testing, but, for example, 
PR125296 and PR125668 were found by compiling the Linux kernel with smtgcc 
enabled.


smtgcc-tv-backend
-----------------
The smtgcc-tv-backend tool checks that the generated assembly is a 
refinement of the final GIMPLE IR. This now supports:
  * AArch64
     - Up to -march=armv9.5-a
  * RISC-V
     - Both RV32 and RV64 targets
     - GCB profile
     - Partial support for the V extension
  * BPF
  * SH (limited support)
  * m68k (limited support)


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
   * -O1
   * -O0
   * -Os
   * -Og
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
   * BPF
      - -mlittle-endian -mcpu=v4
   * SH
      - -ml -m4-single
   * m68k
      - <using the default>


Reported GCC bugs
-----------------
Most GCC bugs I have reported have been fixed, but there is currently 
three open bugs where GCC generates incorrect code: PR113703, PR122948, 
PR123765.

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: PR106884, PR109626, PR110760, PR111257, 
PR111280, PR113590, PR114032, PR114056, PR119720, PR120980, PR120981, 
PR120982, PR124525, PR124526, PR124527, PR125260, PR125295.


Plans
-----
I plan to continue improving the current functionality. In particular:
  * Support more __builtin and internal functions.
  * Add missing instructions to the assembly checking.
  * Add missing ABI support to the assembly checking.
  * Improve performance.


     /Krister


[1] https://github.com/kristerw/smtgcc/