On Tue, Sep 13, 2022 at 11:33 PM Krister Walfridsson via Gcc
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--gimple (but note all type, global variable and function
declarations are missing ...)
Richard.
>
> /Krister
