Krister Walfridsson via Gcc <gcc@gcc.gnu.org> writes:

> I have continued working on my translation validator, smtgcc [1]. Here
> is an update of what I have done since the end-of-year update.
>
>
> smtgcc-tv-backend
> -----------------
> The main focus has been improving the smtgcc-tv-backend tool which
> checks that the generated assembly is a refinement of the final GIMPLE
> IR.
>
> Highlights:
>  * Implemented most AArch64 SVE instructions
>  * Implemented most RISC-V vector instructions
>  * Improved performance
>
> There are still some limitations in the ABI support. This is not too
> problematic, as smtgcc reports "not implemented" instead of trying to
> analyze, so it avoids false positives. But it does restrict the range
> of code it can handle.
>
> The tool also still generates overly complicated SMT formulas for some
> common instructions, which makes tests time out unnecessarily.
>
>
> Add SMTGCC_ASM environment variable
> -----------------------------------
> The smtgcc-tv-backend tool verifies that the generated assembly is a
> refinement of the final GIMPLE IR. It is now possible to override the
> file used for reading the assembly by setting the SMTGCC_ASM
> environment variable. This is useful for testing the implementation of
> smtgcc, but can also be used to verify hand-written assembly by
> letting smtgcc-tv-backend compare the GIMPLE from the C function
> against the provided assembly code instead of the compiler-generated
> output.
>
>
> Caching
> -------
> smtgcc can now cache SMT queries in a Redis database, and use the
> cached result when an identical query is submitted. This speeds up
> continuous testing of GCC a lot.
>
>
> GCC testing
> -----------
> I am continuing with weekly runs of the GCC test suite. The testing is
> done with -fno-strict-aliasing and, for AArch64 and RISC-V,
> -fno-section-anchors, as type-based aliasing and section anchors are
> not yet supported by smtgcc.
>
> The tests are done on optimization levels:
>  * -O3
>  * -O2
>  * -Os
>  * -O1
>  * -O0
> and for the following target flags (where I typically only run a
> subset of targets each week):
>  * x86_64:
>     - <the default x86_64 arch>
>     - -march=x86-64-v2
>     - -march=x86-64-v3
>     - -march=x86-64-v4
>     - -m32
>  * AArch64
>     - <the default aarch64 arch>
>     - -march=armv8.9-a
>     - -march=armv9.5-a
>  * RISC-V
>     - -march=rv64gcbv
>     - -march=rv64gcv
>     - -march=rv64gcb
>     - -march=rv64gc
>     - -march=rv32gcbv
>     - -march=rv32gcv
>     - -march=rv32gcb
>     - -march=rv32gc
>
> Please let me know if there are additional configurations you would
> like me to include in the testing.
>

We sometimes get interesting bugs, especially with UBSAN
(-fsanitize=undefined), with SAVE_EXPR. PR120471 is one example and
PR120837 is another.

These two are FE issues though, so may not really be applicable.

It might be interesting to try -fhardened occasionally (which wraps up
several options that distributions build with).

I think anything that introduces instrumentation (so -fprofile-generate
may be another candidate, or in a sense, -fnon-call-exceptions) could be
interesting.

sam

Reply via email to