On Tue, Sep 13, 2022 at 11:33 PM Krister Walfridsson via Gcc <gcc@gcc.gnu.org> wrote: > > I have implemented a tool for translation validation (similar to Alive2 > for LLVM). The tool takes GIMPLE IR for two functions and checks that the > second is a refinement of the first. That is, > * The returned value is the same for both functions for all input that > does not invoke undefined behavior. > * The second does not have any undefined behavior that the first does not > have. > * The global memory is the same after invoking both functions with input > that does not invoke undefined behavior. > > The implementation is rather limited, but I have already found a few bugs > in GCC (PR 106513, 106523, 106744, 106883, and 106884) by running the tool > on the c-c++-common, gcc.c-torture, gcc.dg, and gcc.misc-tests test > suites. > > The tool is available at https://github.com/kristerw/pysmtgcc and there > is some additional information in the blog post > https://kristerw.github.io/2022/09/13/translation-validation/
Nice! Note that the folding/peephole optimizations done early can be avoided when you separate opportunities in the source to multiple statements, like change int a, b; a = b + 1 - b; to a = b + 1; a = a - b; note that parts of the folding optimizations are shared between GENERIC and GIMPLE (those generated from match.pd), so those will be exercised. Fully exercising and verifying the fold-const.cc only optimizations which happen on GENERIC only is indeed going to be difficult. Another way to avoid some of the pre-SSA optimizations is to feed the plugin with input from the GIMPLE frontend. Look at gcc/testsuite/gcc.dg/gimplefe-*.c for examples, IL can be dumped roughly in a format suitable as GIMPLE frontend input by dumping with -fdump-tree-<opt>-gimple (but note all type, global variable and function declarations are missing ...) Richard. > > /Krister
