Re: Translation validation

[Richard Biener <richard.guenther@gmail.com>]

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