From: Yannick Moy Date: Mon, 16 Jan 2023 11:33:03 +0000 (+0000) Subject: ada: Add annotations for proof of termination of runtime units X-Git-Tag: basepoints/gcc-15~9290 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9c213cb8671e01578a3714ac136760f9452642aa;p=thirdparty%2Fgcc.git ada: Add annotations for proof of termination of runtime units 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. --- diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index 0ada7872572b..1e4a366c5fe3 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 7e8ac1cd0d3e..ace705d2e8ab 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 dee64ab9e0e1..0838d59d5f7c 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 ef3584382eb6..7c1e2fac1af5 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 2c24e1a69832..5651bdcdf3cf 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 dd7b0322b768..70aa4f8bcf31 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 14e78e44ee53..7a8a2bac996e 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 --