From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lf1-x12d.google.com (mail-lf1-x12d.google.com [IPv6:2a00:1450:4864:20::12d]) by sourceware.org (Postfix) with ESMTPS id D85863858407 for ; Tue, 13 Sep 2022 21:32:01 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org D85863858407 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-lf1-x12d.google.com with SMTP id s6so10936731lfo.7 for ; Tue, 13 Sep 2022 14:32:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:message-id:subject:to:date:from:from:to:cc:subject :date; bh=RqFKzCdkjIKtr8H6t2ghMjL76e4wdwEKAa4wVTP26ks=; b=UqRE5Ad0yk1QHQ18nN0zAp9DdXC+bSrNytOOa6gf+a398pN8DzqNzbA253nZN/zu0t 37QvkE0ZBRlERGNXmklk4pwgsiSHGM/LfjnNZuSnvXJ/z8MjzS3MBYJVE3h8u2gRiIr/ +844efhrmxw1jUkdkqRb3mTad+0C8Fv1ySuBGG72xe6OmPJRCjoCoYhRc3IiIHVmMikN gaaHos1lcwZgvbbwLxeFE36CMUG+VYFCFlKhugvmdN3auIpWb7h3Flgbn/nUwd+6dbEM ZmB1EVpenegYIgJwwmGZYpBI9/r38gOBvb4EjYrg3yxMsLO+chOUeQF8Lt94VTBfwFzj jWpg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:message-id:subject:to:date:from:x-gm-message-state :from:to:cc:subject:date; bh=RqFKzCdkjIKtr8H6t2ghMjL76e4wdwEKAa4wVTP26ks=; b=p7ivSrZAyniJKH6hZFg4K/0/FIwyTQMbndH5kSS3J6E04xlJmG/rk7T8f/aZVGzZBr Ad28Svck4icIqSHYGEUHhArULwKZUreMNc9Yv/v0T49Tm6GakAnschmLVkibo8kbSqm3 rnv9OzNvTFij7bJlyQ7auP8Betmk0Jwh8ytQM5zpId5dA6Ob0c4hjo4DlPsoVLKlUJ3E WGoVUUIC6DfmYfgmeet/Bz+cwEPPa4aSqtXWokO0tCsOGPbTWAmc+LmHFTLL1CIbjr4Y OlJa/+1RwjEnpzYK0CNj86BWYaYtQ0t6zsc2l3NirZEC5xIjvF87/hVFqd9So/5CnoNN A61g== X-Gm-Message-State: ACgBeo1ESUijSWVWlHCBUXGItTKoWphpca+Z5CD9ZDrBOGmwADgF1Vq4 tfJE2M5alfDoNCrpdETtQgP5IgA94cc= X-Google-Smtp-Source: AA6agR6JirRjp75g0HrDioSgc3D2m0niQnSbKZt8vYvyvC/lmYZGKnp+4kvJ1VrOvSXNIFk0JNyBUQ== X-Received: by 2002:a05:6512:2281:b0:49b:37d8:2adb with SMTP id f1-20020a056512228100b0049b37d82adbmr2801832lfu.635.1663104720301; Tue, 13 Sep 2022 14:32:00 -0700 (PDT) Received: from [192.168.0.14] (c83-254-134-90.bredband.tele2.se. [83.254.134.90]) by smtp.gmail.com with ESMTPSA id r12-20020a2e94cc000000b0026be23f24efsm1527092ljh.18.2022.09.13.14.31.59 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 13 Sep 2022 14:31:59 -0700 (PDT) From: Krister Walfridsson X-Google-Original-From: Krister Walfridsson Date: Tue, 13 Sep 2022 21:31:51 +0000 (UTC) To: gcc@gcc.gnu.org Subject: Translation validation Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Spam-Status: No, score=-1.3 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: 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