From patchwork Mon May 15 09:44:34 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 94065 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:b0ea:0:b0:3b6:4342:cba0 with SMTP id b10csp6795992vqo; Mon, 15 May 2023 02:58:31 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ72rHjKHU7vORZbZyoOMAB7bLDYuoH207ECVGFl1PRAdP4SVwQk6TSULIZ9kWsi41rZ5b9Z X-Received: by 2002:a17:907:9287:b0:959:6fb2:1c3b with SMTP id bw7-20020a170907928700b009596fb21c3bmr28719801ejc.39.1684144711301; Mon, 15 May 2023 02:58:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684144711; cv=none; d=google.com; s=arc-20160816; b=f2WV5Pv9YyJltAPEUwx+yYklEdqKrOVd2Lq43YanISfw6BEfEQhT/mLpBLHoHsiEk2 zN0fNLviAnMR73YvneBHv3hwoKc8BuVOmgUnb3xt25qGUFm5pICf+B+sT3wQxiv8pePS rjfjRfK1dmFKo1W3SQow5iWGFPd5fFgmmwvY52vesAQ2PCa2mXVAVRM33IzPptWIed73 vuzXo3du1SJgUOAAxLFa0OzjHP2VW1wH9Cho5srwpn34r6RHqzTZU/aDkQ9IuU2kXm4H dvKFghqLQ9aQJtQlyNaKnVQT+s+R3/VJeFQeK435M92ssFbV5LvLY3lSwc8MijIn7YwC 7QWQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=OZ9urXAxydTGqfU5OOyR/FcuwhrQ4MMzn0qJiIOCr80=; b=cL4LNX7+bd/k/hECSMzQi9tSuclnUqgMrXmJYA4llRjMwAgKQzLytvk02e6Hrdtx52 4NiJsYfZzg543XjyFSgJ8dfBWA6FWrT1j2UYWKnI4DgtI2gReCSR/RMpX54RYrvCx8+x XIUVZVKJejkcaAa8b22ezptLxHBvzqhIMWvwkSDkboSYoF0ETmoAogtns/CNKEM4nXNo ZEJ1GFSAU+3GFI25ncMUlWqApT+9czUHBLVLMyb4LWVmIt8yAhuMA5MAgA2oETounJB7 J3Hdd5rY3P3503nWW0/j1ttXHPsyPGlN8y9JRYxBD+0buxcm1BJxOSrQs6Z8A9OcfijZ fpTw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=P0nLzybe; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id s11-20020a17090699cb00b0096aa7d25d32si4851106ejn.265.2023.05.15.02.58.30 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 May 2023 02:58:31 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=P0nLzybe; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id B1608389941A for ; Mon, 15 May 2023 09:52:00 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org B1608389941A DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684144320; bh=OZ9urXAxydTGqfU5OOyR/FcuwhrQ4MMzn0qJiIOCr80=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=P0nLzybeyMZtiYG7psnJ49+RRBickbNkFWhnArHazTizDqI6u/VaCCAo0h6sZm3M0 mIT2a8hSACY78/t42QSIWFNOBC3y+go3IUlRV1Ri/kOfFmxGDZX1VnATZYknqjxqjJ e7Jpce1YkA9nDUDFzuk73SyQBlSuSRmVqkZ9P1+s= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x336.google.com (mail-wm1-x336.google.com [IPv6:2a00:1450:4864:20::336]) by sourceware.org (Postfix) with ESMTPS id E27A03881D25 for ; Mon, 15 May 2023 09:44:37 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org E27A03881D25 Received: by mail-wm1-x336.google.com with SMTP id 5b1f17b1804b1-3f4c6c4b425so34897175e9.2 for ; Mon, 15 May 2023 02:44:37 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684143876; x=1686735876; 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=OZ9urXAxydTGqfU5OOyR/FcuwhrQ4MMzn0qJiIOCr80=; b=avalk4LiTvkXJrYb8pFsqduJ1T+6GuIrwU6ADNacOVIf9JWhBy0rExJ2Mq6zfAL66V 6IVxU2s8cuSBV7ovOEhIoEP47cZRKPR44xttvlaVPB55N8rI52D5BVh7364Pz8pvadVR V/EfivJCxtc0UPhmOCev/0KaD4JQamrGER3/5QQWZsYRiYWln1MHhxDWVTAxPcL9uMPX 2jnYkAUXil6dClnnXu4S3py0IML6tHJ98HBRRO0a3fwqYNaaJkXKgi9mbu1gQXq4n8yX cJprV+l7+gWJXULwCx2j8wVrWezG+DLzXNGSY70xov4E2mBHuXTxBIp7iE7MLqkfxK04 TF9g== X-Gm-Message-State: AC+VfDx1V8N8NSaWs26B98Zt7zFgvsvpGK3hj5EC0kk0BDaQror8QBi6 jjq9AKr+0dzsTugf1T05sGp4LsoFifQHzH6mGzc2qA== X-Received: by 2002:a1c:771a:0:b0:3f4:fd37:fe7c with SMTP id t26-20020a1c771a000000b003f4fd37fe7cmr4735161wmi.31.1684143876629; Mon, 15 May 2023 02:44:36 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id x16-20020a05600c21d000b003f318be9442sm36682021wmj.40.2023.05.15.02.44.35 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 15 May 2023 02:44:36 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Add annotations for proof of termination of runtime units Date: Mon, 15 May 2023 11:44:34 +0200 Message-Id: <20230515094434.1409071-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.4 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, 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 X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1765953724748534563?= X-GMAIL-MSGID: =?utf-8?q?1765953724748534563?= From: Yannick Moy String-manipulating functions should always terminate. Add justification for the termination of Mapping function parameter, and loop variants where needed. This is needed for GNATprove to prove termination. gcc/ada/ * libgnat/a-strbou.ads: Add justifications for Mapping. * libgnat/a-strfix.adb: Same. * libgnat/a-strfix.ads: Same. * libgnat/a-strsea.adb: Same. * libgnat/a-strsea.ads: Same. * libgnat/a-strsup.adb: Same and add loop variants. * libgnat/a-strsup.ads: Same and add specification of termination. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strbou.ads | 6 ++++++ gcc/ada/libgnat/a-strfix.adb | 12 ++++++++++++ gcc/ada/libgnat/a-strfix.ads | 6 ++++++ gcc/ada/libgnat/a-strsea.adb | 18 ++++++++++++++++++ gcc/ada/libgnat/a-strsea.ads | 3 +++ gcc/ada/libgnat/a-strsup.adb | 14 ++++++++++++++ gcc/ada/libgnat/a-strsup.ads | 7 +++++++ 7 files changed, 66 insertions(+) diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index 0ada7872572..1e4a366c5fe 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -1341,6 +1341,9 @@ package Ada.Strings.Bounded with SPARK_Mode is (for all K in 1 .. Length (Source) => Element (Translate'Result, K) = Mapping (Element (Source, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); procedure Translate (Source : in out Bounded_String; @@ -1352,6 +1355,9 @@ package Ada.Strings.Bounded with SPARK_Mode is (for all K in 1 .. Length (Source) => Element (Source, K) = Mapping (Element (Source'Old, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); --------------------------------------- -- String Transformation Subprograms -- diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index 7e8ac1cd0d3..ace705d2e8a 100644 --- a/gcc/ada/libgnat/a-strfix.adb +++ b/gcc/ada/libgnat/a-strfix.adb @@ -773,12 +773,18 @@ package body Ada.Strings.Fixed with SPARK_Mode is do for J in Source'Range loop Result (J - (Source'First - 1)) := Mapping.all (Source (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (for all K in Source'First .. J => Result (K - (Source'First - 1))'Initialized); pragma Loop_Invariant (for all K in Source'First .. J => Result (K - (Source'First - 1)) = Mapping (Source (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; end return; end Translate; @@ -791,9 +797,15 @@ package body Ada.Strings.Fixed with SPARK_Mode is begin for J in Source'Range loop Source (J) := Mapping.all (Source (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (for all K in Source'First .. J => Source (K) = Mapping (Source'Loop_Entry (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; end Translate; diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index dee64ab9e0e..0838d59d5f7 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -754,6 +754,9 @@ package Ada.Strings.Fixed with SPARK_Mode is = Mapping (Source (J))), Global => null, Annotate => (GNATprove, Always_Return); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); function Translate (Source : String; @@ -796,6 +799,9 @@ package Ada.Strings.Fixed with SPARK_Mode is (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))), Global => null, Annotate => (GNATprove, Always_Return); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); procedure Translate (Source : in out String; diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb index ef3584382eb..7c1e2fac1af 100644 --- a/gcc/ada/libgnat/a-strsea.adb +++ b/gcc/ada/libgnat/a-strsea.adb @@ -185,6 +185,9 @@ package body Ada.Strings.Search with SPARK_Mode is Ind := Ind + 1; for K in Pattern'Range loop if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Assert (not (Match (Source, Pattern, Mapping, Ind))); goto Cont; end if; @@ -192,6 +195,9 @@ package body Ada.Strings.Search with SPARK_Mode is pragma Loop_Invariant (for all J in Pattern'First .. K => Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; pragma Assert (Match (Source, Pattern, Mapping, Ind)); @@ -489,12 +495,18 @@ package body Ada.Strings.Search with SPARK_Mode is if Pattern (K) /= Mapping.all (Source (Ind + (K - Pattern'First))) then + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); goto Cont1; end if; pragma Loop_Invariant (for all J in Pattern'First .. K => Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; pragma Assert (Match (Source, Pattern, Mapping, Ind)); @@ -515,12 +527,18 @@ package body Ada.Strings.Search with SPARK_Mode is if Pattern (K) /= Mapping.all (Source (Ind + (K - Pattern'First))) then + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); goto Cont2; end if; pragma Loop_Invariant (for all J in Pattern'First .. K => Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; return Ind; diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads index 2c24e1a6983..5651bdcdf3c 100644 --- a/gcc/ada/libgnat/a-strsea.ads +++ b/gcc/ada/libgnat/a-strsea.ads @@ -74,6 +74,9 @@ package Ada.Strings.Search with SPARK_Mode is and then Source'Length > 0 and then From in Source'First .. Source'Last - (Pattern'Length - 1), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); function Match (Source : String; diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb index dd7b0322b76..70aa4f8bcf3 100644 --- a/gcc/ada/libgnat/a-strsup.adb +++ b/gcc/ada/libgnat/a-strsup.adb @@ -1570,6 +1570,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is (for all K in 1 .. Indx => Result.Data (K) = Item (Item'First + (K - 1) mod Ilen)); + pragma Loop_Variant (Increases => Indx); end loop; Result.Data (Indx + 1 .. Max_Length) := Super_String_Data @@ -1609,6 +1610,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is (for all K in Indx + 1 .. Max_Length => Result.Data (K) = Item (Item'Last - (Max_Length - K) mod Ilen)); + pragma Loop_Variant (Decreases => Indx); end loop; Result.Data (1 .. Indx) := @@ -1845,10 +1847,16 @@ package body Ada.Strings.Superbounded with SPARK_Mode is begin for J in 1 .. Source.Current_Length loop Result.Data (J) := Mapping.all (Source.Data (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (Result.Data (1 .. J)'Initialized); pragma Loop_Invariant (for all K in 1 .. J => Result.Data (K) = Mapping (Source.Data (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; Result.Current_Length := Source.Current_Length; @@ -1862,9 +1870,15 @@ package body Ada.Strings.Superbounded with SPARK_Mode is begin for J in 1 .. Source.Current_Length loop Source.Data (J) := Mapping.all (Source.Data (J)); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); pragma Loop_Invariant (for all K in 1 .. J => Source.Data (K) = Mapping (Source'Loop_Entry.Data (K))); + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); end loop; end Super_Translate; diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 14e78e44ee5..7a8a2bac996 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -53,6 +53,7 @@ with Ada.Strings.Text_Buffers; package Ada.Strings.Superbounded with SPARK_Mode is pragma Preelaborate; + pragma Annotate (GNATprove, Always_Return, Superbounded); -- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is -- derived from Super_String, with the constraint of the maximum length. @@ -1406,6 +1407,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is Super_Element (Super_Translate'Result, K) = Mapping (Super_Element (Source, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); procedure Super_Translate (Source : in out Super_String; @@ -1418,6 +1422,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is Super_Element (Source, K) = Mapping (Super_Element (Source'Old, K))), Global => null; + pragma Annotate (GNATprove, False_Positive, + "call via access-to-subprogram", + "function Mapping must always terminate"); --------------------------------------- -- String Transformation Subprograms --