From: Julien Bortolussi Date: Tue, 26 Apr 2022 10:02:59 +0000 (+0200) Subject: [Ada] Make the functional Maps and Sets unbounded X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=2a466ee093827650cd33fe877c1043441c4e9427;p=platform%2Fupstream%2Fgcc.git [Ada] Make the functional Maps and Sets unbounded Before this patch, the Functional Sets ans Maps were bounded both from the user and the implementation points of view. To make them closer to mathematical Sets ans Maps, this patch removes the bounds from the contracts. Note that, in practice, they are still bounded by Count_Type'Last, even if the user is not aware of it anymore. This patch removed constraints on length of sets and maps from the preconditions of functions. The function Length and Num_Overlaps now return a Big_Natural. gcc/ada/ * libgnat/a-cofuse.ads, libgnat/a-cofuse.adb, libgnat/a-cofuma.ads, libgnat/a-cofuma.adb: Make Length and Num_Overlaps return Big_Natural. * libgnat/a-cforse.ads, libgnat/a-cforse.adb, libgnat/a-cforma.adb, libgnat/a-cfhase.ads, libgnat/a-cfhase.adb, libgnat/a-cfhama.adb, libgnat/a-cfdlli.adb: Adapt code to handle Big_Integers instead of Count_Type. --- diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb index 7b23ad7..bbb8fd4 100644 --- a/gcc/ada/libgnat/a-cfdlli.adb +++ b/gcc/ada/libgnat/a-cfdlli.adb @@ -29,9 +29,17 @@ with Ada.Containers.Stable_Sorting; use Ada.Containers.Stable_Sorting; with System; use type System.Address; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + package body Ada.Containers.Formal_Doubly_Linked_Lists with SPARK_Mode => Off is + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + use Conversions; + ----------------------- -- Local Subprograms -- ----------------------- @@ -809,7 +817,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = To_Big_Integer (I)); Position := Container.Nodes (Position).Next; I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cfhama.adb b/gcc/ada/libgnat/a-cfhama.adb index 0b60a01..bdf2c61 100644 --- a/gcc/ada/libgnat/a-cfhama.adb +++ b/gcc/ada/libgnat/a-cfhama.adb @@ -33,6 +33,9 @@ pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Formal_Keys); with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + with System; use type System.Address; package body Ada.Containers.Formal_Hashed_Maps with @@ -71,6 +74,13 @@ is function Vet (Container : Map; Position : Cursor) return Boolean with Inline; + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + -------------------------- -- Local Instantiations -- -------------------------- @@ -526,7 +536,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := HT_Ops.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cfhase.adb b/gcc/ada/libgnat/a-cfhase.adb index 544ad2b..34afa55 100644 --- a/gcc/ada/libgnat/a-cfhase.adb +++ b/gcc/ada/libgnat/a-cfhase.adb @@ -753,7 +753,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := HT_Ops.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads index 1a40118..80ce948 100644 --- a/gcc/ada/libgnat/a-cfhase.ads +++ b/gcc/ada/libgnat/a-cfhase.ads @@ -48,6 +48,8 @@ with Ada.Containers.Functional_Maps; with Ada.Containers.Functional_Sets; with Ada.Containers.Functional_Vectors; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; private with Ada.Containers.Hash_Tables; generic @@ -70,6 +72,13 @@ is pragma Assertion_Policy (Contract_Cases => Ignore); pragma Annotate (CodePeer, Skip_Analysis); + -- Convert Count_Type to Big_Interger. + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, Next => Next, @@ -261,7 +270,7 @@ is Ghost, Global => null, - Post => M.Length (Model'Result) = Length (Container); + Post => M.Length (Model'Result) = Big (Length (Container)); function Elements (Container : Set) return E.Sequence with -- The Elements sequence represents the underlying list structure of @@ -859,9 +868,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target), Post => - Length (Target) = Length (Target)'Old + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) - + Length (Source) + + Big (Length (Source)) -- Elements already in Target are still in Target @@ -907,9 +916,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Union'Result) = Length (Left) + Big (Length (Union'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) - + Length (Right) + + Big (Length (Right)) -- Elements of Left and Right are in the result of Union @@ -946,7 +955,7 @@ is procedure Intersection (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = + Big (Length (Target)) = M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -982,7 +991,7 @@ is function Intersection (Left, Right : Set) return Set with Global => null, Post => - Length (Intersection'Result) = + Big (Length (Intersection'Result)) = M.Num_Overlaps (Model (Left), Model (Right)) -- Elements in the result of Intersection are in Left and Right @@ -1012,7 +1021,7 @@ is procedure Difference (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -1048,7 +1057,7 @@ is function Difference (Left, Right : Set) return Set with Global => null, Post => - Length (Difference'Result) = Length (Left) - + Big (Length (Difference'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) -- Elements of the result of Difference are in Left @@ -1085,9 +1094,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target) + Length (Target and Source), Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + - Length (Source) + Big (Length (Source)) -- Elements of the difference were not both in Source and in Target @@ -1125,9 +1134,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Symmetric_Difference'Result) = Length (Left) - + Big (Length (Symmetric_Difference'Result)) = Big (Length (Left)) - 2 * M.Num_Overlaps (Model (Left), Model (Right)) + - Length (Right) + Big (Length (Right)) -- Elements of the difference were not both in Left and Right diff --git a/gcc/ada/libgnat/a-cforma.adb b/gcc/ada/libgnat/a-cforma.adb index 79f25f8..38d15e7 100644 --- a/gcc/ada/libgnat/a-cforma.adb +++ b/gcc/ada/libgnat/a-cforma.adb @@ -32,12 +32,22 @@ pragma Elaborate_All with Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys; pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys); +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + with System; use type System.Address; package body Ada.Containers.Formal_Ordered_Maps with SPARK_Mode => Off is + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + ----------------------------- -- Node Access Subprograms -- ----------------------------- @@ -745,7 +755,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := Tree_Operations.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cforse.adb b/gcc/ada/libgnat/a-cforse.adb index 3b64511..e5cddde 100644 --- a/gcc/ada/libgnat/a-cforse.adb +++ b/gcc/ada/libgnat/a-cforse.adb @@ -943,7 +943,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := Tree_Operations.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads index a736b48..f6a033f 100644 --- a/gcc/ada/libgnat/a-cforse.ads +++ b/gcc/ada/libgnat/a-cforse.ads @@ -49,6 +49,8 @@ with Ada.Containers.Functional_Maps; with Ada.Containers.Functional_Sets; with Ada.Containers.Functional_Vectors; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; private with Ada.Containers.Red_Black_Trees; generic @@ -67,6 +69,13 @@ is pragma Assertion_Policy (Contract_Cases => Ignore); pragma Annotate (CodePeer, Skip_Analysis); + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + function Equivalent_Elements (Left, Right : Element_Type) return Boolean with Global => null, @@ -341,7 +350,7 @@ is Ghost, Global => null, - Post => M.Length (Model'Result) = Length (Container); + Post => M.Length (Model'Result) = Big (Length (Container)); function Elements (Container : Set) return E.Sequence with -- The Elements sequence represents the underlying list structure of @@ -990,9 +999,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target), Post => - Length (Target) = Length (Target)'Old + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) - + Length (Source) + + Big (Length (Source)) -- Elements already in Target are still in Target @@ -1038,9 +1047,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Union'Result) = Length (Left) + Big (Length (Union'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) - + Length (Right) + + Big (Length (Right)) -- Elements of Left and Right are in the result of Union @@ -1076,7 +1085,7 @@ is procedure Intersection (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = + Big (Length (Target)) = M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -1111,7 +1120,7 @@ is function Intersection (Left, Right : Set) return Set with Global => null, Post => - Length (Intersection'Result) = + Big (Length (Intersection'Result)) = M.Num_Overlaps (Model (Left), Model (Right)) -- Elements in the result of Intersection are in Left and Right @@ -1139,7 +1148,7 @@ is procedure Difference (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -1174,7 +1183,7 @@ is function Difference (Left, Right : Set) return Set with Global => null, Post => - Length (Difference'Result) = Length (Left) - + Big (Length (Difference'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) -- Elements of the result of Difference are in Left @@ -1209,9 +1218,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target) + Length (Target and Source), Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + - Length (Source) + Big (Length (Source)) -- Elements of the difference were not both in Source and in Target @@ -1248,9 +1257,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Symmetric_Difference'Result) = Length (Left) - + Big (Length (Symmetric_Difference'Result)) = Big (Length (Left)) - 2 * M.Num_Overlaps (Model (Left), Model (Right)) + - Length (Right) + Big (Length (Right)) -- Elements of the difference were not both in Left and Right diff --git a/gcc/ada/libgnat/a-cofuma.adb b/gcc/ada/libgnat/a-cofuma.adb index 0fcdbdc..f83b4d8 100644 --- a/gcc/ada/libgnat/a-cofuma.adb +++ b/gcc/ada/libgnat/a-cofuma.adb @@ -34,6 +34,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is use Key_Containers; use Element_Containers; + package Conversions is new Signed_Conversions (Int => Count_Type); + use Conversions; + --------- -- "=" -- --------- @@ -245,9 +248,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is -- Length -- ------------ - function Length (Container : Map) return Count_Type is + function Length (Container : Map) return Big_Natural is begin - return Length (Container.Elements); + return To_Big_Integer (Length (Container.Elements)); end Length; ------------ diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads index f240e1e..d01c4b4 100644 --- a/gcc/ada/libgnat/a-cofuma.ads +++ b/gcc/ada/libgnat/a-cofuma.ads @@ -32,6 +32,9 @@ pragma Ada_2012; private with Ada.Containers.Functional_Base; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + generic type Key_Type (<>) is private; type Element_Type (<>) is private; @@ -97,7 +100,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is (Equivalent_Keys (K, Key) = (Witness (Container, Key) = Witness (Container, K))))); - function Length (Container : Map) return Count_Type with + function Length (Container : Map) return Big_Natural with Global => null; -- Return the number of mappings in Container @@ -233,9 +236,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is with Global => null, - Pre => - not Has_Key (Container, New_Key) - and Length (Container) < Count_Type'Last, + Pre => not Has_Key (Container, New_Key), Post => Length (Container) + 1 = Length (Add'Result) and Has_Key (Add'Result, New_Key) diff --git a/gcc/ada/libgnat/a-cofuse.adb b/gcc/ada/libgnat/a-cofuse.adb index 77adb1d..bbb3f7e 100644 --- a/gcc/ada/libgnat/a-cofuse.adb +++ b/gcc/ada/libgnat/a-cofuse.adb @@ -34,6 +34,9 @@ pragma Ada_2012; package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is use Containers; + package Conversions is new Signed_Conversions (Int => Count_Type); + use Conversions; + --------- -- "=" -- --------- @@ -135,8 +138,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is -- Length -- ------------ - function Length (Container : Set) return Count_Type is - (Length (Container.Content)); + function Length (Container : Set) return Big_Natural is + (To_Big_Integer (Length (Container.Content))); ----------------- -- Not_In_Both -- @@ -161,8 +164,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is -- Num_Overlaps -- ------------------ - function Num_Overlaps (Left : Set; Right : Set) return Count_Type is - (Num_Overlaps (Left.Content, Right.Content)); + function Num_Overlaps (Left : Set; Right : Set) return Big_Natural is + (To_Big_Integer (Num_Overlaps (Left.Content, Right.Content))); ------------ -- Remove -- diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads index 6cd340b..29f1e9f 100644 --- a/gcc/ada/libgnat/a-cofuse.ads +++ b/gcc/ada/libgnat/a-cofuse.ads @@ -32,6 +32,9 @@ pragma Ada_2012; private with Ada.Containers.Functional_Base; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + generic type Element_Type (<>) is private; @@ -79,7 +82,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is (if (for some E of Container => Equivalent_Elements (E, Item)) then Contains'Result)); - function Length (Container : Set) return Count_Type with + function Length (Container : Set) return Big_Natural with Global => null; -- Return the number of elements in Container @@ -183,7 +186,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is No_Overlap'Result = (for all Item of Left => not Contains (Right, Item)); - function Num_Overlaps (Left : Set; Right : Set) return Count_Type with + function Num_Overlaps (Left : Set; Right : Set) return Big_Natural with -- Number of elements that are both in Left and Right Global => null, @@ -206,9 +209,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- Return a new set containing all the elements of Container plus E Global => null, - Pre => - not Contains (Container, Item) - and Length (Container) < Count_Type'Last, + Pre => not Contains (Container, Item), Post => Length (Add'Result) = Length (Container) + 1 and Contains (Add'Result, Item) @@ -245,9 +246,6 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- Returns the union of Left and Right Global => null, - Pre => - Length (Left) - Num_Overlaps (Left, Right) <= - Count_Type'Last - Length (Right), Post => Length (Union'Result) = Length (Left) - Num_Overlaps (Left, Right) + Length (Right)