* [Ada] Make the functional Maps and Sets unbounded
@ 2022-06-02 9:09 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-06-02 9:09 UTC (permalink / raw)
To: gcc-patches; +Cc: Julien Bortolussi
[-- Attachment #1: Type: text/plain, Size: 913 bytes --]
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 18432 bytes --]
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)
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-06-02 9:09 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:09 [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).