From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ej1-x62e.google.com (mail-ej1-x62e.google.com [IPv6:2a00:1450:4864:20::62e]) by sourceware.org (Postfix) with ESMTPS id 5DF2B3857369 for ; Thu, 2 Jun 2022 09:09:08 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 5DF2B3857369 Received: by mail-ej1-x62e.google.com with SMTP id u12so8701709eja.8 for ; Thu, 02 Jun 2022 02:09:08 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=Pp7PmCWFG1dGCx59/jYtl4QPvp2jR2Zsc4H35Fnudfg=; b=X4ikFDux+/M3bHwV+qWZyIUgBwqVgW5JfecvoQsIxSw8papisznZsDYMrmRtu/sm81 HqVPKzpRAr/r3oaZfj2vZ4pIflNawVmhgCiBfjK+3eoiw9+HIW4WGEuNoUKmreN4t1nA BHeLZUrCO1YlSACBSDzBcurBXPXxZC/PuPH0yx75Ag1mqJ4TD9k4kW0qgF6iJDyBvZjf sBqCLIcshos8u5dkOr6b+fMsgnOmwEt/bkN0NFMkVzcbAPc2hamcqo8zTF3YXYYHnbKl WtRjnDrfvATXrXCs/Pq9Gl8UK+mA27q31A6Gdf9uujRUakC6Dqhbz0hNdEj0aRAHmOzu kyvQ== X-Gm-Message-State: AOAM532sTIgZLR7+5omLER2778bVDC/nhSO9lSjZtHJMh5xVjKPqUQWe 0ENMJpX1PTxzrAhwtpJnv9l8Xn668MZClw== X-Google-Smtp-Source: ABdhPJyNGc22M0L73/kGQkBDIutBB+ZvROPrI/U+nThgJ+WiS+8o8WK7d3/FxeY7F79oQorJrsSGfA== X-Received: by 2002:a17:907:9485:b0:6ff:1012:1b94 with SMTP id dm5-20020a170907948500b006ff10121b94mr3295663ejc.39.1654160947168; Thu, 02 Jun 2022 02:09:07 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id f7-20020a170906560700b006fef5088792sm1552981ejq.108.2022.06.02.02.09.06 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 02 Jun 2022 02:09:06 -0700 (PDT) Date: Thu, 2 Jun 2022 09:09:06 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Julien Bortolussi Subject: [Ada] Make the functional Maps and Sets unbounded Message-ID: <20220602090906.GA1010850@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="TB36FDmn/VVEgNH/" Content-Disposition: inline X-Spam-Status: No, score=-12.8 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, FILL_THIS_FORM, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_FILL_THIS_FORM_LOAN, 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-List-Received-Date: Thu, 02 Jun 2022 09:09:11 -0000 --TB36FDmn/VVEgNH/ Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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. Tested on x86_64-pc-linux-gnu, committed on trunk 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. --TB36FDmn/VVEgNH/ Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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 --- 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) --TB36FDmn/VVEgNH/--