Translation validation

Translation validation

[Krister Walfridsson]

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/

    /Krister

Re: Translation validation

[Richard Biener]

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

Re: Translation validation

[Krister Walfridsson]

On Wed, 14 Sep 2022, Richard Biener wrote:

> 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 ...)

This does not help when trying to find wrong-code bugs by compiling random 
source code with plugin1.py.  :(

But it helps when writing tests for plugin2.py, so I wrote a simple script 
that extracts the first operand from match.pd simplify expressions and 
uses that to generate test cases. For example,

   (simplify
    (mult (abs@1 @0) @1)
    (mult @0 @0))

is generated as

   int __GIMPLE () f (int a0)
   {
     int _0;
     int a1;
     int _2;
     int _3;

     _2 = a0;
     a1 = __ABS _2;
     _3 = a1;
     _0 = a1 * _3;
     return _0;
   }

This is not an optimal way to find bugs as many of the simplify 
expressions have additional restrictions in the replacement part, so many 
of my generated functions fail to trigger optimizations...

This did not find any wrong-code bugs, but it found two cases where 
match.pd is missing TYPE_OVERFLOW_SANITIZED checks: PR 106990.

    /Krister