From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ej1-x634.google.com (mail-ej1-x634.google.com [IPv6:2a00:1450:4864:20::634]) by sourceware.org (Postfix) with ESMTPS id 6748E38AA245 for ; Wed, 14 Sep 2022 06:10:45 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 6748E38AA245 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=gmail.com Received: by mail-ej1-x634.google.com with SMTP id bj12so32214864ejb.13 for ; Tue, 13 Sep 2022 23:10:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:from:to:cc:subject:date; bh=xGrTvsk9axGHl6DJv6cahkLAZNbpoHj3CGaKmV5mk28=; b=Z2ytDgBSwEicAhJNDANTeng3m5xCRGRs9E10mAOKv3hqKvx7iJYFDKxCA6WF/Ha+Fm 6X1JlEoYmPrggZo+8BHIA+IhyQXmJ44LKgs+s0jMCq/wmiSe8jRSoHThRlLfbhi1c9o4 YpPgEr78KKmSmnBwXFF7Xj6Y/Es98j+2YH1rNIi6nrx1ki43Dg0cECz+QYuRmd9oqHw+ n0cyzk4NnNp579bB2AqEeCDiQ1/uXyt9CTZn+2B9tB+xHo6QBkOstRLkqMx+qOU/a2R1 SCqILYJQ3dIGZOUVisush4dB7WxJTIXTp9t+/V3zak9oNrnJh2s2Rt2gkLZswlhJ7opO 0ZgQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:x-gm-message-state:from:to:cc:subject:date; bh=xGrTvsk9axGHl6DJv6cahkLAZNbpoHj3CGaKmV5mk28=; b=NmfCq6noje5IofKtKpLITMmkaWIXpAo6XaoN2oX+OhrJUXbb1HXasvMZmBtNyYPHbN h7KBxRIChjAQ+FMWGECgYqzAOEszzT3xNNXlZ7H0aU5I6O957FXWghVf1NxU8SjP3Si7 gHwGHoPmCxKEpOOP8tC2pMZEnaItAaHzD2FtEjmjk/VHjiS5/3pN4zBC8fkZujJ5crUH FJp4X06BY1w1e9T1L7fgg+Zt6bXRwG0NKau59KgVghloOdko1vqoJ/LAHHodW/xjS9S1 8DwC14uMXpv2r3Y4hKxCxfoKPRmzqx9PdpDi0A1GuSIHeJHdlCgEU6v3g8kKhBPx1ZXk CBIw== X-Gm-Message-State: ACgBeo1kR0x/wGdSOX0EMQEwzJySw4xO07QdeV6YpuT8DHUCLLVFQme7 ZcxgtvgN8OyXpdTng14r3jekvb7tec6/FCo4noM= X-Google-Smtp-Source: AA6agR6j6Jvg8nAw+d/PlvHomdBSdLRPUGARAPGATr+aQOtvo+bMrn1fMYro/5k9yIv53Iac1gQyFFMx3EQzmJDhu3s= X-Received: by 2002:a17:907:7632:b0:76f:f6e7:36cf with SMTP id jy18-20020a170907763200b0076ff6e736cfmr25568996ejc.442.1663135843872; Tue, 13 Sep 2022 23:10:43 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Richard Biener Date: Wed, 14 Sep 2022 08:10:31 +0200 Message-ID: Subject: Re: Translation validation To: Krister Walfridsson Cc: gcc@gcc.gnu.org Content-Type: text/plain; charset="UTF-8" X-Spam-Status: No, score=-2.1 required=5.0 tests=BAYES_00,DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FROM,RCVD_IN_DNSWL_NONE,SPF_HELO_NONE,SPF_PASS,TXREP,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: 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