From: Krister Walfridsson <krister.walfridsson@gmail.com>
To: gcc@gcc.gnu.org
Subject: Translation validation
Date: Tue, 13 Sep 2022 21:31:51 +0000 (UTC) [thread overview]
Message-ID: <Pine.NEB.4.64.2209132124440.8497@gateway.kwa> (raw)
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
next reply other threads:[~2022-09-13 21:32 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-09-13 21:31 Krister Walfridsson [this message]
2022-09-14 6:10 ` Richard Biener
2022-09-20 23:40 ` Krister Walfridsson
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=Pine.NEB.4.64.2209132124440.8497@gateway.kwa \
--to=krister.walfridsson@gmail.com \
--cc=gcc@gcc.gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).