From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x334.google.com (mail-wm1-x334.google.com [IPv6:2a00:1450:4864:20::334]) by sourceware.org (Postfix) with ESMTPS id AC01D3885522 for ; Thu, 6 Oct 2022 09:31:12 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org AC01D3885522 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-wm1-x334.google.com with SMTP id c3-20020a1c3503000000b003bd21e3dd7aso2441100wma.1 for ; Thu, 06 Oct 2022 02:31:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=iu+joWs0QHSVfXGZpBkz3Zf0YgwPm2bRICeCiv0FhC0=; b=XPz+TBlvWhEuBMEHmkuxHcHH51dk7VfxjVBTv78ImhfVeaEQz8Z/E9qYNwH7JqBYFr 3UzQKcPueRsB22cw0iosAWExBU6uZEKUjSlis0QVVC5prA316DL2Ha18QkcCQ5vO7OFh 1vnfPk8VYGS0PnnthMHQz6HoQTx3gZagQAm5edoZQVpk1FaplHD2uxCEXDdUgadHuCVA hOAHqrVQRb84e/xL1849wRjtzJ7D2DkeGkGdpMNt8uaqHn4s/BU70zqKQkvyjiM3e3ZP F4zQm76eX+J4JXHctgIvlka6Rww6NRQarFicVL/iYyR+IzyBs3uLG5SS3qFB7SJjDlQT wKwA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=iu+joWs0QHSVfXGZpBkz3Zf0YgwPm2bRICeCiv0FhC0=; b=0jaeCWrtq4rouHOPyMK4m07QzvqhCcsdTjtXJrROKTGiSsngzTzB3RWAcepRKAr5Xj ZSTkcmfBHyOW9G6om+NTSVedWJz6bgM0ThrymFE4nGTpBTBdh94qtt0o2DUicL0RdSca dRcT3uDixjAgIGkq64uwO5xlvZWAN5+JMZARKJlr3M91LvDnocO6ut9bnLiRZ42jWkFU vATqaQ0/PKmkXDTb9ujUw2OzjmHFuu5uHiEu0gqjhChibFOM/CMJfXWOPA/9s0m/qKkH rEH9mPgrq9Q3j5SnXIIZSxnoPqCF8JvYLxVkguz0gwzQBOCpd+IlxikC8Id+qwmlbAEC jRxw== X-Gm-Message-State: ACrzQf25dIvFDNwyj/wAHwJ0gwdQ9G4sjbVvf+o0+h1oNyxjSVSrKGVP kfme28udFwcmce9QYmn3MZKHd+nGNjTv+kUr X-Google-Smtp-Source: AMsMyM7n/aY3+9x+zQ86ItIvvOSDvUWxcPRzYhAx92RAdXlQDENx0cSalpn4IKOUUtZjxgz3GLVR2A== X-Received: by 2002:a05:600c:4f11:b0:3b4:bf6c:4566 with SMTP id l17-20020a05600c4f1100b003b4bf6c4566mr6114169wmq.34.1665048671570; Thu, 06 Oct 2022 02:31:11 -0700 (PDT) Received: from poulhies-Precision-5550.lan (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id bi26-20020a05600c3d9a00b003b476cabf1csm4141521wmb.26.2022.10.06.02.31.10 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 06 Oct 2022 02:31:10 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Alexandre Oliva Subject: [COMMITED] ada: hardened conditionals: exemplify codegen changes Date: Thu, 6 Oct 2022 11:31:08 +0200 Message-Id: <20221006093108.261899-1-poulhies@adacore.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-13.3 required=5.0 tests=BAYES_00,DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,GIT_PATCH_0,RCVD_IN_DNSWL_NONE,SPF_HELO_NONE,SPF_PASS,TXREP 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: From: Alexandre Oliva gcc/ada/ * doc/gnat_rm/security_hardening_features.rst: Add examples of codegen changes in hardened conditionals. * gnat_rm.texi: Regenerate. Tested on x86_64-pc-linux-gnu, committed on master. --- .../gnat_rm/security_hardening_features.rst | 51 ++++++++++++++++++- gcc/ada/gnat_rm.texi | 47 ++++++++++++++++- 2 files changed, 94 insertions(+), 4 deletions(-) diff --git a/gcc/ada/doc/gnat_rm/security_hardening_features.rst b/gcc/ada/doc/gnat_rm/security_hardening_features.rst index d8ea849c032..d7c02b94f36 100644 --- a/gcc/ada/doc/gnat_rm/security_hardening_features.rst +++ b/gcc/ada/doc/gnat_rm/security_hardening_features.rst @@ -203,11 +203,58 @@ activated by a separate command-line option. The option :switch:`-fharden-compares` enables hardening of compares that compute results stored in variables, adding verification that the -reversed compare yields the opposite result. +reversed compare yields the opposite result, turning: + +.. code-block:: ada + + B := X = Y; + + +into: + +.. code-block:: ada + + B := X = Y; + declare + NotB : Boolean := X /= Y; -- Computed independently of B. + begin + if B = NotB then + <__builtin_trap>; + end if; + end; + The option :switch:`-fharden-conditional-branches` enables hardening of compares that guard conditional branches, adding verification of -the reversed compare to both execution paths. +the reversed compare to both execution paths, turning: + +.. code-block:: ada + + if X = Y then + X := Z + 1; + else + Y := Z - 1; + end if; + + +into: + +.. code-block:: ada + + if X = Y then + if X /= Y then -- Computed independently of X = Y. + <__builtin_trap>; + end if; + X := Z + 1; + else + if X /= Y then -- Computed independently of X = Y. + null; + else + <__builtin_trap>; + end if; + Y := Z - 1; + end if; + These transformations are introduced late in the compilation pipeline, long after boolean expressions are decomposed into separate compares, diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index dad0092713e..e13dba037ff 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -28858,11 +28858,54 @@ activated by a separate command-line option. The option @code{-fharden-compares} enables hardening of compares that compute results stored in variables, adding verification that the -reversed compare yields the opposite result. +reversed compare yields the opposite result, turning: + +@example +B := X = Y; +@end example + +into: + +@example +B := X = Y; +declare + NotB : Boolean := X /= Y; -- Computed independently of B. +begin + if B = NotB then + <__builtin_trap>; + end if; +end; +@end example The option @code{-fharden-conditional-branches} enables hardening of compares that guard conditional branches, adding verification of -the reversed compare to both execution paths. +the reversed compare to both execution paths, turning: + +@example +if X = Y then + X := Z + 1; +else + Y := Z - 1; +end if; +@end example + +into: + +@example +if X = Y then + if X /= Y then -- Computed independently of X = Y. + <__builtin_trap>; + end if; + X := Z + 1; +else + if X /= Y then -- Computed independently of X = Y. + null; + else + <__builtin_trap>; + end if; + Y := Z - 1; +end if; +@end example These transformations are introduced late in the compilation pipeline, long after boolean expressions are decomposed into separate compares, -- 2.34.1