public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-948] [Ada] Make the functional Maps and Sets unbounded
@ 2022-06-02 9:10 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-06-02 9:10 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:2a466ee093827650cd33fe877c1043441c4e9427
commit r13-948-g2a466ee093827650cd33fe877c1043441c4e9427
Author: Julien Bortolussi <bortolussi@adacore.com>
Date: Tue Apr 26 12:02:59 2022 +0200
[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:
---
gcc/ada/libgnat/a-cfdlli.adb | 10 +++++++++-
gcc/ada/libgnat/a-cfhama.adb | 12 +++++++++++-
gcc/ada/libgnat/a-cfhase.adb | 2 +-
gcc/ada/libgnat/a-cfhase.ads | 35 ++++++++++++++++++++++-------------
gcc/ada/libgnat/a-cforma.adb | 12 +++++++++++-
gcc/ada/libgnat/a-cforse.adb | 2 +-
gcc/ada/libgnat/a-cforse.ads | 35 ++++++++++++++++++++++-------------
gcc/ada/libgnat/a-cofuma.adb | 7 +++++--
gcc/ada/libgnat/a-cofuma.ads | 9 +++++----
gcc/ada/libgnat/a-cofuse.adb | 11 +++++++----
gcc/ada/libgnat/a-cofuse.ads | 14 ++++++--------
11 files changed, 100 insertions(+), 49 deletions(-)
diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb
index 7b23ad79232..bbb8fd449a7 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 0b60a010512..bdf2c61d61e 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 544ad2bfa79..34afa554c5f 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 1a40118013e..80ce9485b2d 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 79f25f8b6cc..38d15e7bb09 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 3b64511f52e..e5cddde4985 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 a736b48ba71..f6a033f680f 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 0fcdbdc0e97..f83b4d829f7 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 f240e1e41ef..d01c4b4dd22 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 77adb1d6414..bbb3f7e96f9 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 6cd340bed26..29f1e9f979f 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)
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-06-02 9:10 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-06-02 9:10 [gcc r13-948] [Ada] Make the functional Maps and Sets unbounded Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).