smtgcc mid-year update
Update on smtgcc, a translation validator for GCC, highlighting performance improvements, real-world testing, backend support, and ongoing GCC test suite runs.
Krister Walfridsson provides a mid-year update on smtgcc, his translation validator for GCC. Significant performance improvements have been achieved, reducing timeouts by 90% through the addition of the Bitwuzla SMT solver and better canonicalization. Smtgcc is now capable of finding issues in real-world software, with two bugs found during Linux kernel compilation. The smtgcc-tv-backend now supports AArch64, RISC-V, BPF, SH, and m68k targets. Weekly runs of the GCC test suite continue, with testing focused on specific optimization levels and architectures, and with known limitations regarding type-based aliasing and section anchors.
- proposer
Provides a status update on smtgcc, detailing performance improvements, expanded backend support, and its use in testing real-world software and the GCC test suite.
In Details
This is a status report for 'smtgcc', a tool that acts as a translation validator for GCC. It checks that the generated assembly code is a refinement of the GIMPLE Intermediate Representation (IR). The report details improvements in performance (aided by the Bitwuzla SMT solver), expanded backend support (AArch64, RISC-V, BPF, SH, m68k), and its usage in finding bugs in real software like the Linux kernel and in the GCC test suite itself. Notably, smtgcc currently does not support strict aliasing or section anchors, requiring specific testing configurations.
- smtgcc
- A translation validator for GCC that checks if the generated assembly code correctly reflects the GIMPLE Intermediate Representation.
- SMT solver
- Satisfiability Modulo Theories solver, a tool used in program analysis to determine the satisfiability of logical formulas.
- GIMPLE
- GCC's Internal Representation (IR) used after the parsing and initial tree construction stages, optimized before generating machine code.
- Canonicalization
- The process of converting data into a standard or canonical form, often used to simplify comparisons or processing.
- Translation validator
- A tool that verifies the correctness of a translation process, in this case, ensuring the compiler's IR is accurately translated to assembly.