diff mbox series

[COMMITTED] ada: Add annotations for proof of termination of runtime units

Message ID 20230515094434.1409071-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Add annotations for proof of termination of runtime units |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès May 15, 2023, 9:44 a.m. UTC 
  From: Yannick Moy <moy@adacore.com>

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 mbox series

Patch

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 --