From: Claire Dross Date: Fri, 30 Apr 2021 08:24:30 +0000 (+0200) Subject: [Ada] Add Reference and Constant_Reference functions to formal containers X-Git-Tag: basepoints/gcc-13~6280 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=fdb5c200369c8ba56358a145e0c5c6c461ad5a45;p=thirdparty%2Fgcc.git [Ada] Add Reference and Constant_Reference functions to formal containers gcc/ada/ * libgnat/a-cfdlli.ads, libgnat/a-cfdlli.adb libgnat/a-cfinve.ads, libgnat/a-cfinve.adb, libgnat/a-cofove.ads, libgnat/a-cofove.adb, libgnat/a-coboho.ads, libgnat/a-coboho.adb (Constant_Reference): Get a read-only access to an element of the container. (At_End): Ghost functions used to express pledges in the postcondition of Reference. (Reference): Get a read-write access to an element of the container. * libgnat/a-cfhama.ads, libgnat/a-cfhama.adb, libgnat/a-cforma.ads, libgnat/a-cforma.adb: The full view of the Map type is no longer a tagged type, but a wrapper over this tagged type. This is to avoid issues with dispatching result in At_End functions. (Constant_Reference): Get a read-only access to an element of the container. (At_End): Ghost functions used to express pledges in the postcondition of Reference. (Reference): Get a read-write access to an element of the container. * libgnat/a-cfhase.ads, libgnat/a-cfhase.adb, libgnat/a-cforse.ads, libgnat/a-cforse.adb: The full view of the Map type is no longer a tagged type, but a wrapper over this tagged type. (Constant_Reference): Get a read-only access to an element of the container. * libgnat/a-cofuse.ads, libgnat/a-cofuve.ads (Copy_Element): Expression function used to cause SPARK to make sure Element_Type is copiable. * libgnat/a-cofuma.ads (Copy_Key): Expression function used to cause SPARK to make sure Key_Type is copiable. (Copy_Element): Expression function used to cause SPARK to make sure Element_Type is copiable. --- diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb index d96a8f6f2767..b289def23fa1 100644 --- a/gcc/ada/libgnat/a-cfdlli.adb +++ b/gcc/ada/libgnat/a-cfdlli.adb @@ -188,6 +188,22 @@ is Free (Container, X); end Clear; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased List; + Position : Cursor) return not null access constant Element_Type + is + begin + if not Has_Element (Container => Container, Position => Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + return Container.Nodes (Position.Node).Element'Access; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -1376,6 +1392,22 @@ is return (Node => Container.Nodes (Position.Node).Prev); end Previous; + --------------- + -- Reference -- + --------------- + + function Reference + (Container : not null access List; + Position : Cursor) return not null access Element_Type + is + begin + if not Has_Element (Container.all, Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + return Container.Nodes (Position.Node).Element'Access; + end Reference; + --------------------- -- Replace_Element -- --------------------- diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads index e3a2de6abd4f..8713d33bf348 100644 --- a/gcc/ada/libgnat/a-cfdlli.ads +++ b/gcc/ada/libgnat/a-cfdlli.ads @@ -387,6 +387,53 @@ is Model (Container), P.Get (Positions (Container), Position)); + function At_End (E : access constant List) return access constant List + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function At_End + (E : access constant Element_Type) return access constant Element_Type + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function Constant_Reference + (Container : aliased List; + Position : Cursor) return not null access constant Element_Type + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Constant_Reference'Result.all = + Element (Model (Container), P.Get (Positions (Container), Position)); + + function Reference + (Container : not null access List; + Position : Cursor) return not null access Element_Type + with + Global => null, + Pre => Has_Element (Container.all, Position), + Post => + Length (Container.all) = Length (At_End (Container).all) + + -- Cursors are preserved + + and Positions (Container.all) = Positions (At_End (Container).all) + + -- Container will have Result.all at position Position + + and At_End (Reference'Result).all = + Element (Model (At_End (Container).all), + P.Get (Positions (At_End (Container).all), Position)) + + -- All other elements are preserved + + and M.Equal_Except + (Model (Container.all), + Model (At_End (Container).all), + P.Get (Positions (At_End (Container).all), Position)); + procedure Move (Target : in out List; Source : in out List) with Global => null, Pre => Target.Capacity >= Length (Source), @@ -1609,7 +1656,7 @@ private type Node_Type is record Prev : Count_Type'Base := -1; Next : Count_Type; - Element : Element_Type; + Element : aliased Element_Type; end record; function "=" (L, R : Node_Type) return Boolean is abstract; diff --git a/gcc/ada/libgnat/a-cfhama.adb b/gcc/ada/libgnat/a-cfhama.adb index 17971b2158e6..179b40074f00 100644 --- a/gcc/ada/libgnat/a-cfhama.adb +++ b/gcc/ada/libgnat/a-cfhama.adb @@ -109,20 +109,21 @@ is ENode : Count_Type; begin - Node := Left.First.Node; + Node := First (Left).Node; while Node /= 0 loop ENode := Find (Container => Right, - Key => Left.Nodes (Node).Key).Node; + Key => Left.Content.Nodes (Node).Key).Node; if ENode = 0 or else - Right.Nodes (ENode).Element /= Left.Nodes (Node).Element + Right.Content.Nodes (ENode).Element /= + Left.Content.Nodes (Node).Element then return False; end if; - Node := HT_Ops.Next (Left, Node); + Node := HT_Ops.Next (Left.Content, Node); end loop; return True; @@ -145,7 +146,7 @@ is -------------------- procedure Insert_Element (Source_Node : Count_Type) is - N : Node_Type renames Source.Nodes (Source_Node); + N : Node_Type renames Source.Content.Nodes (Source_Node); begin Insert (Target, N.Key, N.Element); end Insert_Element; @@ -164,7 +165,7 @@ is Clear (Target); - Insert_Elements (Source); + Insert_Elements (Source.Content); end Assign; -------------- @@ -173,7 +174,7 @@ is function Capacity (Container : Map) return Count_Type is begin - return Container.Nodes'Length; + return Container.Content.Nodes'Length; end Capacity; ----------- @@ -182,9 +183,44 @@ is procedure Clear (Container : in out Map) is begin - HT_Ops.Clear (Container); + HT_Ops.Clear (Container.Content); end Clear; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Map; + Position : Cursor) return not null access constant Element_Type + is + begin + if not Has_Element (Container, Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + pragma Assert + (Vet (Container, Position), + "bad cursor in function Constant_Reference"); + + return Container.Content.Nodes (Position.Node).Element'Access; + end Constant_Reference; + + function Constant_Reference + (Container : aliased Map; + Key : Key_Type) return not null access constant Element_Type + is + Node : constant Count_Type := Find (Container, Key).Node; + + begin + if Node = 0 then + raise Constraint_Error with + "no element available because key not in map"; + end if; + + return Container.Content.Nodes (Node).Element'Access; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -214,18 +250,18 @@ is raise Capacity_Error; end if; - Target.Length := Source.Length; - Target.Free := Source.Free; + Target.Content.Length := Source.Content.Length; + Target.Content.Free := Source.Content.Free; H := 1; while H <= Source.Modulus loop - Target.Buckets (H) := Source.Buckets (H); + Target.Content.Buckets (H) := Source.Content.Buckets (H); H := H + 1; end loop; N := 1; while N <= Source.Capacity loop - Target.Nodes (N) := Source.Nodes (N); + Target.Content.Nodes (N) := Source.Content.Nodes (N); N := N + 1; end loop; @@ -255,7 +291,7 @@ is X : Count_Type; begin - Key_Ops.Delete_Key_Sans_Free (Container, Key, X); + Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X); if X = 0 then raise Constraint_Error with "attempt to delete key not in map"; @@ -273,7 +309,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in Delete"); - HT_Ops.Delete_Node_Sans_Free (Container, Position.Node); + HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node); Free (Container, Position.Node); Position := No_Element; @@ -292,7 +328,7 @@ is "no element available because key not in map"; end if; - return Container.Nodes (Node).Element; + return Container.Content.Nodes (Node).Element; end Element; function Element (Container : Map; Position : Cursor) return Element_Type is @@ -304,7 +340,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in function Element"); - return Container.Nodes (Position.Node).Element; + return Container.Content.Nodes (Position.Node).Element; end Element; --------------------- @@ -326,7 +362,7 @@ is procedure Exclude (Container : in out Map; Key : Key_Type) is X : Count_Type; begin - Key_Ops.Delete_Key_Sans_Free (Container, Key, X); + Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X); Free (Container, X); end Exclude; @@ -335,7 +371,7 @@ is ---------- function Find (Container : Map; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Ops.Find (Container, Key); + Node : constant Count_Type := Key_Ops.Find (Container.Content, Key); begin if Node = 0 then @@ -350,7 +386,7 @@ is ----------- function First (Container : Map) return Cursor is - Node : constant Count_Type := HT_Ops.First (Container); + Node : constant Count_Type := HT_Ops.First (Container.Content); begin if Node = 0 then @@ -407,7 +443,7 @@ is ---------- function Keys (Container : Map) return K.Sequence is - Position : Count_Type := HT_Ops.First (Container); + Position : Count_Type := HT_Ops.First (Container.Content); R : K.Sequence; begin @@ -415,8 +451,8 @@ is -- for their postconditions. while Position /= 0 loop - R := K.Add (R, Container.Nodes (Position).Key); - Position := HT_Ops.Next (Container, Position); + R := K.Add (R, Container.Content.Nodes (Position).Key); + Position := HT_Ops.Next (Container.Content, Position); end loop; return R; @@ -458,7 +494,7 @@ is ----------- function Model (Container : Map) return M.Map is - Position : Count_Type := HT_Ops.First (Container); + Position : Count_Type := HT_Ops.First (Container.Content); R : M.Map; begin @@ -469,10 +505,10 @@ is R := M.Add (Container => R, - New_Key => Container.Nodes (Position).Key, - New_Item => Container.Nodes (Position).Element); + New_Key => Container.Content.Nodes (Position).Key, + New_Item => Container.Content.Nodes (Position).Element); - Position := HT_Ops.Next (Container, Position); + Position := HT_Ops.Next (Container.Content, Position); end loop; return R; @@ -484,7 +520,7 @@ is function Positions (Container : Map) return P.Map is I : Count_Type := 1; - Position : Count_Type := HT_Ops.First (Container); + Position : Count_Type := HT_Ops.First (Container.Content); R : P.Map; begin @@ -494,7 +530,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); pragma Assert (P.Length (R) = I); - Position := HT_Ops.Next (Container, Position); + Position := HT_Ops.Next (Container.Content, Position); I := I + 1; end loop; @@ -511,8 +547,8 @@ is begin if X /= 0 then pragma Assert (X <= HT.Capacity); - HT.Nodes (X).Has_Element := False; - HT_Ops.Free (HT, X); + HT.Content.Nodes (X).Has_Element := False; + HT_Ops.Free (HT.Content, X); end if; end Free; @@ -525,8 +561,8 @@ is new HT_Ops.Generic_Allocate (Set_Element); begin - Allocate (HT, Node); - HT.Nodes (Node).Has_Element := True; + Allocate (HT.Content, Node); + HT.Content.Nodes (Node).Has_Element := True; end Generic_Allocate; ----------------- @@ -536,7 +572,7 @@ is function Has_Element (Container : Map; Position : Cursor) return Boolean is begin if Position.Node = 0 - or else not Container.Nodes (Position.Node).Has_Element + or else not Container.Content.Nodes (Position.Node).Has_Element then return False; else @@ -570,7 +606,7 @@ is if not Inserted then declare - N : Node_Type renames Container.Nodes (Position.Node); + N : Node_Type renames Container.Content.Nodes (Position.Node); begin N.Key := Key; N.Element := New_Item; @@ -625,7 +661,7 @@ is -- Start of processing for Insert begin - Local_Insert (Container, Key, Position.Node, Inserted); + Local_Insert (Container.Content, Key, Position.Node, Inserted); end Insert; procedure Insert @@ -668,7 +704,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in function Key"); - return Container.Nodes (Position.Node).Key; + return Container.Content.Nodes (Position.Node).Key; end Key; ------------ @@ -677,7 +713,7 @@ is function Length (Container : Map) return Count_Type is begin - return Container.Length; + return Container.Content.Length; end Length; ---------- @@ -688,7 +724,7 @@ is (Target : in out Map; Source : in out Map) is - NN : HT_Types.Nodes_Type renames Source.Nodes; + NN : HT_Types.Nodes_Type renames Source.Content.Nodes; X : Count_Type; Y : Count_Type; @@ -704,17 +740,17 @@ is Clear (Target); - if Source.Length = 0 then + if Source.Content.Length = 0 then return; end if; - X := HT_Ops.First (Source); + X := HT_Ops.First (Source.Content); while X /= 0 loop Insert (Target, NN (X).Key, NN (X).Element); -- optimize??? - Y := HT_Ops.Next (Source, X); + Y := HT_Ops.Next (Source.Content, X); - HT_Ops.Delete_Node_Sans_Free (Source, X); + HT_Ops.Delete_Node_Sans_Free (Source.Content, X); Free (Source, X); X := Y; @@ -743,7 +779,8 @@ is pragma Assert (Vet (Container, Position), "bad cursor in function Next"); declare - Node : constant Count_Type := HT_Ops.Next (Container, Position.Node); + Node : constant Count_Type := + HT_Ops.Next (Container.Content, Position.Node); begin if Node = 0 then @@ -759,6 +796,40 @@ is Position := Next (Container, Position); end Next; + --------------- + -- Reference -- + --------------- + + function Reference + (Container : not null access Map; + Position : Cursor) return not null access Element_Type + is + begin + if not Has_Element (Container.all, Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + pragma Assert + (Vet (Container.all, Position), "bad cursor in function Reference"); + + return Container.Content.Nodes (Position.Node).Element'Access; + end Reference; + + function Reference + (Container : not null access Map; + Key : Key_Type) return not null access Element_Type + is + Node : constant Count_Type := Find (Container.all, Key).Node; + + begin + if Node = 0 then + raise Constraint_Error with + "no element available because key not in map"; + end if; + + return Container.Content.Nodes (Node).Element'Access; + end Reference; + ------------- -- Replace -- ------------- @@ -768,7 +839,7 @@ is Key : Key_Type; New_Item : Element_Type) is - Node : constant Count_Type := Key_Ops.Find (Container, Key); + Node : constant Count_Type := Key_Ops.Find (Container.Content, Key); begin if Node = 0 then @@ -776,7 +847,7 @@ is end if; declare - N : Node_Type renames Container.Nodes (Node); + N : Node_Type renames Container.Content.Nodes (Node); begin N.Key := Key; N.Element := New_Item; @@ -801,7 +872,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in Replace_Element"); - Container.Nodes (Position.Node).Element := New_Item; + Container.Content.Nodes (Position.Node).Element := New_Item; end Replace_Element; ---------------------- @@ -841,7 +912,7 @@ is X : Count_Type; begin - if Container.Length = 0 then + if Container.Content.Length = 0 then return False; end if; @@ -849,7 +920,7 @@ is return False; end if; - if Container.Buckets'Length = 0 then + if Container.Content.Buckets'Length = 0 then return False; end if; @@ -857,15 +928,17 @@ is return False; end if; - if Container.Nodes (Position.Node).Next = Position.Node then + if Container.Content.Nodes (Position.Node).Next = Position.Node then return False; end if; X := - Container.Buckets - (Key_Ops.Index (Container, Container.Nodes (Position.Node).Key)); + Container.Content.Buckets + (Key_Ops.Index + (Container.Content, + Container.Content.Nodes (Position.Node).Key)); - for J in 1 .. Container.Length loop + for J in 1 .. Container.Content.Length loop if X = Position.Node then return True; end if; @@ -874,14 +947,14 @@ is return False; end if; - if X = Container.Nodes (X).Next then + if X = Container.Content.Nodes (X).Next then -- Prevent unnecessary looping return False; end if; - X := Container.Nodes (X).Next; + X := Container.Content.Nodes (X).Next; end loop; return False; diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads index e9b02682fda0..2b49c13df3f6 100644 --- a/gcc/ada/libgnat/a-cfhama.ads +++ b/gcc/ada/libgnat/a-cfhama.ads @@ -394,6 +394,95 @@ is Model (Container)'Old, Key (Container, Position)); + function At_End + (E : not null access constant Map) return not null access constant Map + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function At_End + (E : access constant Element_Type) return access constant Element_Type + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function Constant_Reference + (Container : aliased Map; + Position : Cursor) return not null access constant Element_Type + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Constant_Reference'Result.all = + Element (Model (Container), Key (Container, Position)); + + function Reference + (Container : not null access Map; + Position : Cursor) return not null access Element_Type + with + Global => null, + Pre => Has_Element (Container.all, Position), + Post => + + -- Order of keys and cursors is preserved + + Keys (At_End (Container).all) = Keys (Container.all) + and Positions (At_End (Container).all) = Positions (Container.all) + + -- The value designated by the result of Reference is now associated + -- with the key at position Position in Container. + + and Element (At_End (Container).all, Position) = + At_End (Reference'Result).all + + -- Elements associated with other keys are preserved + + and M.Same_Keys + (Model (At_End (Container).all), + Model (Container.all)) + and M.Elements_Equal_Except + (Model (At_End (Container).all), + Model (Container.all), + Key (At_End (Container).all, Position)); + + function Constant_Reference + (Container : aliased Map; + Key : Key_Type) return not null access constant Element_Type + with + Global => null, + Pre => Contains (Container, Key), + Post => + Constant_Reference'Result.all = Element (Model (Container), Key); + + function Reference + (Container : not null access Map; + Key : Key_Type) return not null access Element_Type + with + Global => null, + Pre => Contains (Container.all, Key), + Post => + + -- Order of keys and cursors is preserved + + Keys (At_End (Container).all) = Keys (Container.all) + and Positions (At_End (Container).all) = Positions (Container.all) + + -- The value designated by the result of Reference is now associated + -- with Key in Container. + + and Element (Model (At_End (Container).all), Key) = + At_End (Reference'Result).all + + -- Elements associated with other keys are preserved + + and M.Same_Keys + (Model (At_End (Container).all), + Model (Container.all)) + and M.Elements_Equal_Except + (Model (At_End (Container).all), + Model (Container.all), + Key); + procedure Move (Target : in out Map; Source : in out Map) with Global => null, Pre => Target.Capacity >= Length (Source), @@ -804,7 +893,7 @@ private type Node_Type is record Key : Key_Type; - Element : Element_Type; + Element : aliased Element_Type; Next : Count_Type; Has_Element : Boolean := False; end record; @@ -812,8 +901,9 @@ private package HT_Types is new Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type); - type Map (Capacity : Count_Type; Modulus : Hash_Type) is - new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; + type Map (Capacity : Count_Type; Modulus : Hash_Type) is record + Content : HT_Types.Hash_Table_Type (Capacity, Modulus); + end record; Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>); diff --git a/gcc/ada/libgnat/a-cfhase.adb b/gcc/ada/libgnat/a-cfhase.adb index 3679ca451e50..cdb8a98fd582 100644 --- a/gcc/ada/libgnat/a-cfhase.adb +++ b/gcc/ada/libgnat/a-cfhase.adb @@ -136,15 +136,16 @@ is ENode := Find (Container => Right, - Item => Left.Nodes (Node).Element).Node; + Item => Left.Content.Nodes (Node).Element).Node; if ENode = 0 - or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element + or else Right.Content.Nodes (ENode).Element /= + Left.Content.Nodes (Node).Element then return False; end if; - Node := HT_Ops.Next (Left, Node); + Node := HT_Ops.Next (Left.Content, Node); end loop; return True; @@ -166,7 +167,7 @@ is -------------------- procedure Insert_Element (Source_Node : Count_Type) is - N : Node_Type renames Source.Nodes (Source_Node); + N : Node_Type renames Source.Content.Nodes (Source_Node); X : Count_Type; B : Boolean; @@ -186,8 +187,8 @@ is raise Storage_Error with "not enough capacity"; -- SE or CE? ??? end if; - HT_Ops.Clear (Target); - Insert_Elements (Source); + HT_Ops.Clear (Target.Content); + Insert_Elements (Source.Content); end Assign; -------------- @@ -196,7 +197,7 @@ is function Capacity (Container : Set) return Count_Type is begin - return Container.Nodes'Length; + return Container.Content.Nodes'Length; end Capacity; ----------- @@ -205,9 +206,28 @@ is procedure Clear (Container : in out Set) is begin - HT_Ops.Clear (Container); + HT_Ops.Clear (Container.Content); end Clear; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Set; + Position : Cursor) return not null access constant Element_Type + is + begin + if not Has_Element (Container, Position) then + raise Constraint_Error with "Position cursor equals No_Element"; + end if; + + pragma Assert + (Vet (Container, Position), "bad cursor in function Element"); + + return Container.Content.Nodes (Position.Node).Element'Access; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -237,18 +257,18 @@ is raise Capacity_Error; end if; - Target.Length := Source.Length; - Target.Free := Source.Free; + Target.Content.Length := Source.Content.Length; + Target.Content.Free := Source.Content.Free; H := 1; while H <= Source.Modulus loop - Target.Buckets (H) := Source.Buckets (H); + Target.Content.Buckets (H) := Source.Content.Buckets (H); H := H + 1; end loop; N := 1; while N <= Source.Capacity loop - Target.Nodes (N) := Source.Nodes (N); + Target.Content.Nodes (N) := Source.Content.Nodes (N); N := N + 1; end loop; @@ -278,7 +298,7 @@ is X : Count_Type; begin - Element_Keys.Delete_Key_Sans_Free (Container, Item, X); + Element_Keys.Delete_Key_Sans_Free (Container.Content, Item, X); if X = 0 then raise Constraint_Error with "attempt to delete element not in set"; @@ -295,7 +315,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in Delete"); - HT_Ops.Delete_Node_Sans_Free (Container, Position.Node); + HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node); Free (Container, Position.Node); Position := No_Element; @@ -311,8 +331,8 @@ is Src_Node : Count_Type; Tgt_Node : Count_Type; - TN : Nodes_Type renames Target.Nodes; - SN : Nodes_Type renames Source.Nodes; + TN : Nodes_Type renames Target.Content.Nodes; + SN : Nodes_Type renames Source.Content.Nodes; begin if Target'Address = Source'Address then @@ -320,44 +340,45 @@ is return; end if; - Src_Length := Source.Length; + Src_Length := Source.Content.Length; if Src_Length = 0 then return; end if; - if Src_Length >= Target.Length then - Tgt_Node := HT_Ops.First (Target); + if Src_Length >= Target.Content.Length then + Tgt_Node := HT_Ops.First (Target.Content); while Tgt_Node /= 0 loop - if Element_Keys.Find (Source, TN (Tgt_Node).Element) /= 0 then + if Element_Keys.Find (Source.Content, TN (Tgt_Node).Element) /= 0 + then declare X : constant Count_Type := Tgt_Node; begin - Tgt_Node := HT_Ops.Next (Target, Tgt_Node); - HT_Ops.Delete_Node_Sans_Free (Target, X); + Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node); + HT_Ops.Delete_Node_Sans_Free (Target.Content, X); Free (Target, X); end; else - Tgt_Node := HT_Ops.Next (Target, Tgt_Node); + Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node); end if; end loop; return; else - Src_Node := HT_Ops.First (Source); + Src_Node := HT_Ops.First (Source.Content); Src_Last := 0; end if; while Src_Node /= Src_Last loop - Tgt_Node := Element_Keys.Find (Target, SN (Src_Node).Element); + Tgt_Node := Element_Keys.Find (Target.Content, SN (Src_Node).Element); if Tgt_Node /= 0 then - HT_Ops.Delete_Node_Sans_Free (Target, Tgt_Node); + HT_Ops.Delete_Node_Sans_Free (Target.Content, Tgt_Node); Free (Target, Tgt_Node); end if; - Src_Node := HT_Ops.Next (Source, Src_Node); + Src_Node := HT_Ops.Next (Source.Content, Src_Node); end loop; end Difference; @@ -373,7 +394,7 @@ is procedure Process (L_Node : Count_Type) is B : Boolean; - E : Element_Type renames Left.Nodes (L_Node).Element; + E : Element_Type renames Left.Content.Nodes (L_Node).Element; X : Count_Type; begin @@ -386,7 +407,7 @@ is -- Start of processing for Difference begin - Iterate (Left); + Iterate (Left.Content); end Difference; function Difference (Left : Set; Right : Set) return Set is @@ -403,7 +424,7 @@ is end if; if Length (Right) = 0 then - return Left.Copy; + return Copy (Left); end if; C := Length (Left); @@ -430,7 +451,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in function Element"); - return Container.Nodes (Position.Node).Element; + return Container.Content.Nodes (Position.Node).Element; end Element; --------------------- @@ -479,7 +500,7 @@ is -- Start of processing for Equivalent_Sets begin - return Is_Equivalent (Left, Right); + return Is_Equivalent (Left.Content, Right.Content); end Equivalent_Sets; --------------------- @@ -501,7 +522,7 @@ is procedure Exclude (Container : in out Set; Item : Element_Type) is X : Count_Type; begin - Element_Keys.Delete_Key_Sans_Free (Container, Item, X); + Element_Keys.Delete_Key_Sans_Free (Container.Content, Item, X); Free (Container, X); end Exclude; @@ -513,7 +534,8 @@ is (Container : Set; Item : Element_Type) return Cursor is - Node : constant Count_Type := Element_Keys.Find (Container, Item); + Node : constant Count_Type := + Element_Keys.Find (Container.Content, Item); begin if Node = 0 then @@ -528,7 +550,7 @@ is ----------- function First (Container : Set) return Cursor is - Node : constant Count_Type := HT_Ops.First (Container); + Node : constant Count_Type := HT_Ops.First (Container.Content); begin if Node = 0 then @@ -632,7 +654,7 @@ is -------------- function Elements (Container : Set) return E.Sequence is - Position : Count_Type := HT_Ops.First (Container); + Position : Count_Type := HT_Ops.First (Container.Content); R : E.Sequence; begin @@ -640,8 +662,8 @@ is -- for their postconditions. while Position /= 0 loop - R := E.Add (R, Container.Nodes (Position).Element); - Position := HT_Ops.Next (Container, Position); + R := E.Add (R, Container.Content.Nodes (Position).Element); + Position := HT_Ops.Next (Container.Content, Position); end loop; return R; @@ -710,7 +732,7 @@ is ----------- function Model (Container : Set) return M.Set is - Position : Count_Type := HT_Ops.First (Container); + Position : Count_Type := HT_Ops.First (Container.Content); R : M.Set; begin @@ -721,9 +743,9 @@ is R := M.Add (Container => R, - Item => Container.Nodes (Position).Element); + Item => Container.Content.Nodes (Position).Element); - Position := HT_Ops.Next (Container, Position); + Position := HT_Ops.Next (Container.Content, Position); end loop; return R; @@ -735,7 +757,7 @@ is function Positions (Container : Set) return P.Map is I : Count_Type := 1; - Position : Count_Type := HT_Ops.First (Container); + Position : Count_Type := HT_Ops.First (Container.Content); R : P.Map; begin @@ -745,7 +767,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); pragma Assert (P.Length (R) = I); - Position := HT_Ops.Next (Container, Position); + Position := HT_Ops.Next (Container.Content, Position); I := I + 1; end loop; @@ -762,8 +784,8 @@ is begin if X /= 0 then pragma Assert (X <= HT.Capacity); - HT.Nodes (X).Has_Element := False; - HT_Ops.Free (HT, X); + HT.Content.Nodes (X).Has_Element := False; + HT_Ops.Free (HT.Content, X); end if; end Free; @@ -774,8 +796,8 @@ is procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element); begin - Allocate (HT, Node); - HT.Nodes (Node).Has_Element := True; + Allocate (HT.Content, Node); + HT.Content.Nodes (Node).Has_Element := True; end Generic_Allocate; package body Generic_Keys with SPARK_Mode => Off is @@ -821,7 +843,7 @@ is X : Count_Type; begin - Key_Keys.Delete_Key_Sans_Free (Container, Key, X); + Key_Keys.Delete_Key_Sans_Free (Container.Content, Key, X); if X = 0 then raise Constraint_Error with "attempt to delete key not in set"; @@ -845,7 +867,7 @@ is raise Constraint_Error with "key not in map"; end if; - return Container.Nodes (Node).Element; + return Container.Content.Nodes (Node).Element; end Element; ------------------------- @@ -867,7 +889,7 @@ is procedure Exclude (Container : in out Set; Key : Key_Type) is X : Count_Type; begin - Key_Keys.Delete_Key_Sans_Free (Container, Key, X); + Key_Keys.Delete_Key_Sans_Free (Container.Content, Key, X); Free (Container, X); end Exclude; @@ -879,7 +901,7 @@ is (Container : Set; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Keys.Find (Container, Key); + Node : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin return (if Node = 0 then No_Element else (Node => Node)); end Find; @@ -927,7 +949,7 @@ is (Vet (Container, Position), "bad cursor in function Key"); declare - N : Node_Type renames Container.Nodes (Position.Node); + N : Node_Type renames Container.Content.Nodes (Position.Node); begin return Key (N.Element); end; @@ -942,14 +964,14 @@ is Key : Key_Type; New_Item : Element_Type) is - Node : constant Count_Type := Key_Keys.Find (Container, Key); + Node : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin if Node = 0 then raise Constraint_Error with "attempt to replace key not in set"; end if; - Replace_Element (Container, Node, New_Item); + Replace_Element (Container.Content, Node, New_Item); end Replace; end Generic_Keys; @@ -961,7 +983,7 @@ is function Has_Element (Container : Set; Position : Cursor) return Boolean is begin if Position.Node = 0 - or else not Container.Nodes (Position.Node).Has_Element + or else not Container.Content.Nodes (Position.Node).Has_Element then return False; end if; @@ -990,7 +1012,7 @@ is Insert (Container, New_Item, Position, Inserted); if not Inserted then - Container.Nodes (Position.Node).Element := New_Item; + Container.Content.Nodes (Position.Node).Element := New_Item; end if; end Include; @@ -1062,7 +1084,7 @@ is -- Start of processing for Insert begin - Local_Insert (Container, New_Item, Node, Inserted); + Local_Insert (Container.Content, New_Item, Node, Inserted); end Insert; ------------------ @@ -1071,29 +1093,29 @@ is procedure Intersection (Target : in out Set; Source : Set) is Tgt_Node : Count_Type; - TN : Nodes_Type renames Target.Nodes; + TN : Nodes_Type renames Target.Content.Nodes; begin if Target'Address = Source'Address then return; end if; - if Source.Length = 0 then + if Source.Content.Length = 0 then Clear (Target); return; end if; - Tgt_Node := HT_Ops.First (Target); + Tgt_Node := HT_Ops.First (Target.Content); while Tgt_Node /= 0 loop if Find (Source, TN (Tgt_Node).Element).Node /= 0 then - Tgt_Node := HT_Ops.Next (Target, Tgt_Node); + Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node); else declare X : constant Count_Type := Tgt_Node; begin - Tgt_Node := HT_Ops.Next (Target, Tgt_Node); - HT_Ops.Delete_Node_Sans_Free (Target, X); + Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node); + HT_Ops.Delete_Node_Sans_Free (Target.Content, X); Free (Target, X); end; end if; @@ -1111,7 +1133,7 @@ is ------------- procedure Process (L_Node : Count_Type) is - E : Element_Type renames Left.Nodes (L_Node).Element; + E : Element_Type renames Left.Content.Nodes (L_Node).Element; X : Count_Type; B : Boolean; @@ -1125,7 +1147,7 @@ is -- Start of processing for Intersection begin - Iterate (Left); + Iterate (Left.Content); end Intersection; function Intersection (Left : Set; Right : Set) return Set is @@ -1134,7 +1156,7 @@ is begin if Left'Address = Right'Address then - return Left.Copy; + return Copy (Left); end if; C := Count_Type'Min (Length (Left), Length (Right)); -- ??? @@ -1162,7 +1184,7 @@ is function Is_In (HT : Set; Key : Node_Type) return Boolean is begin - return Element_Keys.Find (HT, Key.Element) /= 0; + return Element_Keys.Find (HT.Content, Key.Element) /= 0; end Is_In; --------------- @@ -1171,7 +1193,7 @@ is function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is Subset_Node : Count_Type; - Subset_Nodes : Nodes_Type renames Subset.Nodes; + Subset_Nodes : Nodes_Type renames Subset.Content.Nodes; begin if Subset'Address = Of_Set'Address then @@ -1194,7 +1216,7 @@ is end if; end; - Subset_Node := HT_Ops.Next (Subset, Subset_Node); + Subset_Node := HT_Ops.Next (Subset.Content, Subset_Node); end loop; return True; @@ -1206,7 +1228,7 @@ is function Length (Container : Set) return Count_Type is begin - return Container.Length; + return Container.Content.Length; end Length; ---------- @@ -1216,7 +1238,7 @@ is -- Comments??? procedure Move (Target : in out Set; Source : in out Set) is - NN : HT_Types.Nodes_Type renames Source.Nodes; + NN : HT_Types.Nodes_Type renames Source.Content.Nodes; X, Y : Count_Type; begin @@ -1231,17 +1253,17 @@ is Clear (Target); - if Source.Length = 0 then + if Source.Content.Length = 0 then return; end if; - X := HT_Ops.First (Source); + X := HT_Ops.First (Source.Content); while X /= 0 loop Insert (Target, NN (X).Element); -- optimize??? - Y := HT_Ops.Next (Source, X); + Y := HT_Ops.Next (Source.Content, X); - HT_Ops.Delete_Node_Sans_Free (Source, X); + HT_Ops.Delete_Node_Sans_Free (Source.Content, X); Free (Source, X); X := Y; @@ -1269,7 +1291,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in Next"); - return (Node => HT_Ops.Next (Container, Position.Node)); + return (Node => HT_Ops.Next (Container.Content, Position.Node)); end Next; procedure Next (Container : Set; Position : in out Cursor) is @@ -1283,7 +1305,7 @@ is function Overlap (Left, Right : Set) return Boolean is Left_Node : Count_Type; - Left_Nodes : Nodes_Type renames Left.Nodes; + Left_Nodes : Nodes_Type renames Left.Content.Nodes; begin if Length (Right) = 0 or Length (Left) = 0 then @@ -1305,7 +1327,7 @@ is end if; end; - Left_Node := HT_Ops.Next (Left, Left_Node); + Left_Node := HT_Ops.Next (Left.Content, Left_Node); end loop; return False; @@ -1316,14 +1338,15 @@ is ------------- procedure Replace (Container : in out Set; New_Item : Element_Type) is - Node : constant Count_Type := Element_Keys.Find (Container, New_Item); + Node : constant Count_Type := + Element_Keys.Find (Container.Content, New_Item); begin if Node = 0 then raise Constraint_Error with "attempt to replace element not in set"; end if; - Container.Nodes (Node).Element := New_Item; + Container.Content.Nodes (Node).Element := New_Item; end Replace; --------------------- @@ -1343,7 +1366,7 @@ is pragma Assert (Vet (Container, Position), "bad cursor in Replace_Element"); - Replace_Element (Container, Position.Node, New_Item); + Replace_Element (Container.Content, Position.Node, New_Item); end Replace_Element; ---------------------- @@ -1394,7 +1417,7 @@ is procedure Process (Source_Node : Count_Type) is B : Boolean; - N : Node_Type renames Source.Nodes (Source_Node); + N : Node_Type renames Source.Content.Nodes (Source_Node); X : Count_Type; begin @@ -1419,7 +1442,7 @@ is return; end if; - Iterate (Source); + Iterate (Source.Content); end Symmetric_Difference; function Symmetric_Difference (Left : Set; Right : Set) return Set is @@ -1432,11 +1455,11 @@ is end if; if Length (Right) = 0 then - return Left.Copy; + return Copy (Left); end if; if Length (Left) = 0 then - return Right.Copy; + return Copy (Right); end if; C := Length (Left) + Length (Right); @@ -1478,7 +1501,7 @@ is ------------- procedure Process (Src_Node : Count_Type) is - N : Node_Type renames Source.Nodes (Src_Node); + N : Node_Type renames Source.Content.Nodes (Src_Node); E : Element_Type renames N.Element; X : Count_Type; @@ -1495,7 +1518,7 @@ is return; end if; - Iterate (Source); + Iterate (Source.Content); end Union; function Union (Left : Set; Right : Set) return Set is @@ -1504,15 +1527,15 @@ is begin if Left'Address = Right'Address then - return Left.Copy; + return Copy (Left); end if; if Length (Right) = 0 then - return Left.Copy; + return Copy (Left); end if; if Length (Left) = 0 then - return Right.Copy; + return Copy (Right); end if; C := Length (Left) + Length (Right); @@ -1535,11 +1558,11 @@ is declare S : Set renames Container; - N : Nodes_Type renames S.Nodes; + N : Nodes_Type renames S.Content.Nodes; X : Count_Type; begin - if S.Length = 0 then + if S.Content.Length = 0 then return False; end if; @@ -1551,9 +1574,10 @@ is return False; end if; - X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element)); + X := S.Content.Buckets + (Element_Keys.Index (S.Content, N (Position.Node).Element)); - for J in 1 .. S.Length loop + for J in 1 .. S.Content.Length loop if X = Position.Node then return True; end if; diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads index 5d578632a05d..9bcd8cedb4cc 100644 --- a/gcc/ada/libgnat/a-cfhase.ads +++ b/gcc/ada/libgnat/a-cfhase.ads @@ -515,6 +515,16 @@ is Position => Position) and Positions (Container) = Positions (Container)'Old; + function Constant_Reference + (Container : aliased Set; + Position : Cursor) return not null access constant Element_Type + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Constant_Reference'Result.all = + E.Get (Elements (Container), P.Get (Positions (Container), Position)); + procedure Move (Target : in out Set; Source : in out Set) with Global => null, Pre => Target.Capacity >= Length (Source), @@ -1462,7 +1472,7 @@ private type Node_Type is record - Element : Element_Type; + Element : aliased Element_Type; Next : Count_Type; Has_Element : Boolean := False; end record; @@ -1470,8 +1480,9 @@ private package HT_Types is new Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type); - type Set (Capacity : Count_Type; Modulus : Hash_Type) is - new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; + type Set (Capacity : Count_Type; Modulus : Hash_Type) is record + Content : HT_Types.Hash_Table_Type (Capacity, Modulus); + end record; use HT_Types; diff --git a/gcc/ada/libgnat/a-cfinve.adb b/gcc/ada/libgnat/a-cfinve.adb index 6ab4935c02a1..d0c7e82ac8f9 100644 --- a/gcc/ada/libgnat/a-cfinve.adb +++ b/gcc/ada/libgnat/a-cfinve.adb @@ -184,6 +184,28 @@ is Free (Container.Elements_Ptr); end Clear; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Vector; + Index : Index_Type) return not null access constant Element_Type + is + begin + if Index > Container.Last then + raise Constraint_Error with "Index is out of range"; + end if; + + declare + II : constant Int'Base := Int (Index) - Int (No_Index); + I : constant Capacity_Range := Capacity_Range (II); + + begin + return Constant_Reference (Elemsc (Container) (I)); + end; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -1180,6 +1202,32 @@ is Insert (Container, Index_Type'First, New_Item, Count); end Prepend; + --------------- + -- Reference -- + --------------- + + function Reference + (Container : not null access Vector; + Index : Index_Type) return not null access Element_Type + is + begin + if Index > Container.Last then + raise Constraint_Error with "Index is out of range"; + end if; + + declare + II : constant Int'Base := Int (Index) - Int (No_Index); + I : constant Capacity_Range := Capacity_Range (II); + + begin + if Container.Elements_Ptr = null then + return Reference (Container.Elements (I)'Access); + else + return Reference (Container.Elements_Ptr (I)'Access); + end if; + end; + end Reference; + --------------------- -- Replace_Element -- --------------------- diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads index 37dde920137e..9b9543756905 100644 --- a/gcc/ada/libgnat/a-cfinve.ads +++ b/gcc/ada/libgnat/a-cfinve.ads @@ -311,6 +311,48 @@ is Right => Model (Container), Position => Index); + function At_End (E : access constant Vector) return access constant Vector + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function At_End + (E : access constant Element_Type) return access constant Element_Type + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function Constant_Reference + (Container : aliased Vector; + Index : Index_Type) return not null access constant Element_Type + with + Global => null, + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => + Constant_Reference'Result.all = Element (Model (Container), Index); + + function Reference + (Container : not null access Vector; + Index : Index_Type) return not null access Element_Type + with + Global => null, + Pre => + Index in First_Index (Container.all) .. Last_Index (Container.all), + Post => + Length (Container.all) = Length (At_End (Container).all) + + -- Container will have Result.all at index Index + + and At_End (Reference'Result).all = + Element (Model (At_End (Container).all), Index) + + -- All other elements are preserved + + and M.Equal_Except + (Left => Model (Container.all), + Right => Model (At_End (Container).all), + Position => Index); + procedure Insert (Container : in out Vector; Before : Extended_Index; @@ -909,7 +951,7 @@ private use Holders; subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; - type Elements_Array is array (Array_Index range <>) of Holder; + type Elements_Array is array (Array_Index range <>) of aliased Holder; function "=" (L, R : Elements_Array) return Boolean is abstract; type Elements_Array_Ptr is access all Elements_Array; diff --git a/gcc/ada/libgnat/a-cforma.adb b/gcc/ada/libgnat/a-cforma.adb index f38461983899..45f9be73f558 100644 --- a/gcc/ada/libgnat/a-cforma.adb +++ b/gcc/ada/libgnat/a-cforma.adb @@ -133,19 +133,20 @@ is return True; end if; - Lst := Next (Left, Last (Left).Node); + Lst := Next (Left.Content, Last (Left).Node); Node := First (Left).Node; while Node /= Lst loop - ENode := Find (Right, Left.Nodes (Node).Key).Node; + ENode := Find (Right, Left.Content.Nodes (Node).Key).Node; if ENode = 0 or else - Left.Nodes (Node).Element /= Right.Nodes (ENode).Element + Left.Content.Nodes (Node).Element /= + Right.Content.Nodes (ENode).Element then return False; end if; - Node := Next (Left, Node); + Node := Next (Left.Content, Node); end loop; return True; @@ -166,7 +167,7 @@ is -------------------- procedure Append_Element (Source_Node : Count_Type) is - SN : Node_Type renames Source.Nodes (Source_Node); + SN : Node_Type renames Source.Content.Nodes (Source_Node); procedure Set_Element (Node : in out Node_Type); pragma Inline (Set_Element); @@ -193,7 +194,7 @@ is function New_Node return Count_Type is Result : Count_Type; begin - Allocate (Target, Result); + Allocate (Target.Content, Result); return Result; end New_Node; @@ -213,7 +214,7 @@ is begin Unconditional_Insert_Avec_Hint - (Tree => Target, + (Tree => Target.Content, Hint => 0, Key => SN.Key, Node => Target_Node); @@ -230,8 +231,8 @@ is raise Storage_Error with "not enough capacity"; -- SE or CE? ??? end if; - Tree_Operations.Clear_Tree (Target); - Append_Elements (Source); + Tree_Operations.Clear_Tree (Target.Content); + Append_Elements (Source.Content); end Assign; ------------- @@ -239,7 +240,7 @@ is ------------- function Ceiling (Container : Map; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Ops.Ceiling (Container, Key); + Node : constant Count_Type := Key_Ops.Ceiling (Container.Content, Key); begin if Node = 0 then @@ -255,7 +256,7 @@ is procedure Clear (Container : in out Map) is begin - Tree_Operations.Clear_Tree (Container); + Tree_Operations.Clear_Tree (Container.Content); end Clear; ----------- @@ -267,6 +268,40 @@ is return Node.Color; end Color; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Map; + Position : Cursor) return not null access constant Element_Type + is + begin + if not Has_Element (Container, Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + pragma Assert (Vet (Container.Content, Position.Node), + "bad cursor in function Constant_Reference"); + + return Container.Content.Nodes (Position.Node).Element'Access; + end Constant_Reference; + + function Constant_Reference + (Container : aliased Map; + Key : Key_Type) return not null access constant Element_Type + is + Node : constant Node_Access := Find (Container, Key).Node; + + begin + if Node = 0 then + raise Constraint_Error with + "no element available because key not in map"; + end if; + + return Container.Content.Nodes (Node).Element'Access; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -291,33 +326,33 @@ is return Target : Map (Count_Type'Max (Source.Capacity, Capacity)) do if Length (Source) > 0 then - Target.Length := Source.Length; - Target.Root := Source.Root; - Target.First := Source.First; - Target.Last := Source.Last; - Target.Free := Source.Free; + Target.Content.Length := Source.Content.Length; + Target.Content.Root := Source.Content.Root; + Target.Content.First := Source.Content.First; + Target.Content.Last := Source.Content.Last; + Target.Content.Free := Source.Content.Free; while Node <= Source.Capacity loop - Target.Nodes (Node).Element := - Source.Nodes (Node).Element; - Target.Nodes (Node).Key := - Source.Nodes (Node).Key; - Target.Nodes (Node).Parent := - Source.Nodes (Node).Parent; - Target.Nodes (Node).Left := - Source.Nodes (Node).Left; - Target.Nodes (Node).Right := - Source.Nodes (Node).Right; - Target.Nodes (Node).Color := - Source.Nodes (Node).Color; - Target.Nodes (Node).Has_Element := - Source.Nodes (Node).Has_Element; + Target.Content.Nodes (Node).Element := + Source.Content.Nodes (Node).Element; + Target.Content.Nodes (Node).Key := + Source.Content.Nodes (Node).Key; + Target.Content.Nodes (Node).Parent := + Source.Content.Nodes (Node).Parent; + Target.Content.Nodes (Node).Left := + Source.Content.Nodes (Node).Left; + Target.Content.Nodes (Node).Right := + Source.Content.Nodes (Node).Right; + Target.Content.Nodes (Node).Color := + Source.Content.Nodes (Node).Color; + Target.Content.Nodes (Node).Has_Element := + Source.Content.Nodes (Node).Has_Element; Node := Node + 1; end loop; while Node <= Target.Capacity loop N := Node; - Formal_Ordered_Maps.Free (Tree => Target, X => N); + Free (Tree => Target, X => N); Node := Node + 1; end loop; end if; @@ -335,25 +370,25 @@ is "Position cursor of Delete has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "Position cursor of Delete is bad"); - Tree_Operations.Delete_Node_Sans_Free (Container, + Tree_Operations.Delete_Node_Sans_Free (Container.Content, Position.Node); - Formal_Ordered_Maps.Free (Container, Position.Node); + Free (Container, Position.Node); Position := No_Element; end Delete; procedure Delete (Container : in out Map; Key : Key_Type) is - X : constant Node_Access := Key_Ops.Find (Container, Key); + X : constant Node_Access := Key_Ops.Find (Container.Content, Key); begin if X = 0 then raise Constraint_Error with "key not in map"; end if; - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Maps.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end Delete; ------------------ @@ -364,8 +399,8 @@ is X : constant Node_Access := First (Container).Node; begin if X /= 0 then - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Maps.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Delete_First; @@ -377,8 +412,8 @@ is X : constant Node_Access := Last (Container).Node; begin if X /= 0 then - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Maps.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Delete_Last; @@ -393,10 +428,10 @@ is "Position cursor of function Element has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "Position cursor of function Element is bad"); - return Container.Nodes (Position.Node).Element; + return Container.Content.Nodes (Position.Node).Element; end Element; @@ -408,7 +443,7 @@ is raise Constraint_Error with "key not in map"; end if; - return Container.Nodes (Node).Element; + return Container.Content.Nodes (Node).Element; end Element; --------------------- @@ -431,11 +466,11 @@ is ------------- procedure Exclude (Container : in out Map; Key : Key_Type) is - X : constant Node_Access := Key_Ops.Find (Container, Key); + X : constant Node_Access := Key_Ops.Find (Container.Content, Key); begin if X /= 0 then - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Maps.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Exclude; @@ -444,7 +479,7 @@ is ---------- function Find (Container : Map; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Ops.Find (Container, Key); + Node : constant Count_Type := Key_Ops.Find (Container.Content, Key); begin if Node = 0 then @@ -464,7 +499,7 @@ is return No_Element; end if; - return (Node => Container.First); + return (Node => Container.Content.First); end First; ------------------- @@ -477,7 +512,7 @@ is raise Constraint_Error with "map is empty"; end if; - return Container.Nodes (First (Container).Node).Element; + return Container.Content.Nodes (First (Container).Node).Element; end First_Element; --------------- @@ -490,7 +525,7 @@ is raise Constraint_Error with "map is empty"; end if; - return Container.Nodes (First (Container).Node).Key; + return Container.Content.Nodes (First (Container).Node).Key; end First_Key; ----------- @@ -498,7 +533,7 @@ is ----------- function Floor (Container : Map; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Ops.Floor (Container, Key); + Node : constant Count_Type := Key_Ops.Floor (Container.Content, Key); begin if Node = 0 then @@ -602,7 +637,7 @@ is ---------- function Keys (Container : Map) return K.Sequence is - Position : Count_Type := Container.First; + Position : Count_Type := Container.Content.First; R : K.Sequence; begin @@ -610,8 +645,8 @@ is -- for their postconditions. while Position /= 0 loop - R := K.Add (R, Container.Nodes (Position).Key); - Position := Tree_Operations.Next (Container, Position); + R := K.Add (R, Container.Content.Nodes (Position).Key); + Position := Tree_Operations.Next (Container.Content, Position); end loop; return R; @@ -628,7 +663,7 @@ is ----------- function Model (Container : Map) return M.Map is - Position : Count_Type := Container.First; + Position : Count_Type := Container.Content.First; R : M.Map; begin @@ -639,10 +674,10 @@ is R := M.Add (Container => R, - New_Key => Container.Nodes (Position).Key, - New_Item => Container.Nodes (Position).Element); + New_Key => Container.Content.Nodes (Position).Key, + New_Item => Container.Content.Nodes (Position).Element); - Position := Tree_Operations.Next (Container, Position); + Position := Tree_Operations.Next (Container.Content, Position); end loop; return R; @@ -701,7 +736,7 @@ is function Positions (Container : Map) return P.Map is I : Count_Type := 1; - Position : Count_Type := Container.First; + Position : Count_Type := Container.Content.First; R : P.Map; begin @@ -711,7 +746,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); pragma Assert (P.Length (R) = I); - Position := Tree_Operations.Next (Container, Position); + Position := Tree_Operations.Next (Container.Content, Position); I := I + 1; end loop; @@ -729,8 +764,8 @@ is X : Count_Type) is begin - Tree.Nodes (X).Has_Element := False; - Tree_Operations.Free (Tree, X); + Tree.Content.Nodes (X).Has_Element := False; + Tree_Operations.Free (Tree.Content, X); end Free; ---------------------- @@ -758,7 +793,7 @@ is return False; end if; - return Container.Nodes (Position.Node).Has_Element; + return Container.Content.Nodes (Position.Node).Has_Element; end Has_Element; ------------- @@ -778,7 +813,7 @@ is if not Inserted then declare - N : Node_Type renames Container.Nodes (Position.Node); + N : Node_Type renames Container.Content.Nodes (Position.Node); begin N.Key := Key; N.Element := New_Item; @@ -819,7 +854,7 @@ is X : Node_Access; begin - Allocate_Node (Container, X); + Allocate_Node (Container.Content, X); return X; end New_Node; @@ -827,7 +862,7 @@ is begin Insert_Sans_Hint - (Container, + (Container.Content, Key, Position.Node, Inserted); @@ -895,10 +930,10 @@ is "Position cursor of function Key has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "Position cursor of function Key is bad"); - return Container.Nodes (Position.Node).Key; + return Container.Content.Nodes (Position.Node).Key; end Key; ---------- @@ -911,7 +946,7 @@ is return No_Element; end if; - return (Node => Container.Last); + return (Node => Container.Content.Last); end Last; ------------------ @@ -924,7 +959,7 @@ is raise Constraint_Error with "map is empty"; end if; - return Container.Nodes (Last (Container).Node).Element; + return Container.Content.Nodes (Last (Container).Node).Element; end Last_Element; -------------- @@ -937,7 +972,7 @@ is raise Constraint_Error with "map is empty"; end if; - return Container.Nodes (Last (Container).Node).Key; + return Container.Content.Nodes (Last (Container).Node).Key; end Last_Key; -------------- @@ -955,7 +990,7 @@ is function Length (Container : Map) return Count_Type is begin - return Container.Length; + return Container.Content.Length; end Length; ---------- @@ -963,7 +998,7 @@ is ---------- procedure Move (Target : in out Map; Source : in out Map) is - NN : Tree_Types.Nodes_Type renames Source.Nodes; + NN : Tree_Types.Nodes_Type renames Source.Content.Nodes; X : Node_Access; begin @@ -989,7 +1024,7 @@ is Insert (Target, NN (X).Key, NN (X).Element); -- optimize??? - Tree_Operations.Delete_Node_Sans_Free (Source, X); + Tree_Operations.Delete_Node_Sans_Free (Source.Content, X); Formal_Ordered_Maps.Free (Source, X); end loop; end Move; @@ -1013,10 +1048,10 @@ is raise Constraint_Error; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Next"); - return (Node => Tree_Operations.Next (Container, Position.Node)); + return (Node => Tree_Operations.Next (Container.Content, Position.Node)); end Next; ------------ @@ -1047,12 +1082,12 @@ is raise Constraint_Error; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Previous"); declare Node : constant Count_Type := - Tree_Operations.Previous (Container, Position.Node); + Tree_Operations.Previous (Container.Content, Position.Node); begin if Node = 0 then @@ -1063,6 +1098,41 @@ is end; end Previous; + -------------- + -- Reference -- + -------------- + + function Reference + (Container : not null access Map; + Position : Cursor) return not null access Element_Type + is + begin + if not Has_Element (Container.all, Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + pragma Assert + (Vet (Container.Content, Position.Node), + "bad cursor in function Reference"); + + return Container.Content.Nodes (Position.Node).Element'Access; + end Reference; + + function Reference + (Container : not null access Map; + Key : Key_Type) return not null access Element_Type + is + Node : constant Count_Type := Find (Container.all, Key).Node; + + begin + if Node = 0 then + raise Constraint_Error with + "no element available because key not in map"; + end if; + + return Container.Content.Nodes (Node).Element'Access; + end Reference; + ------------- -- Replace -- ------------- @@ -1074,7 +1144,7 @@ is is begin declare - Node : constant Node_Access := Key_Ops.Find (Container, Key); + Node : constant Node_Access := Key_Ops.Find (Container.Content, Key); begin if Node = 0 then @@ -1082,7 +1152,7 @@ is end if; declare - N : Node_Type renames Container.Nodes (Node); + N : Node_Type renames Container.Content.Nodes (Node); begin N.Key := Key; N.Element := New_Item; @@ -1105,10 +1175,10 @@ is "Position cursor of Replace_Element has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "Position cursor of Replace_Element is bad"); - Container.Nodes (Position.Node).Element := New_Item; + Container.Content.Nodes (Position.Node).Element := New_Item; end Replace_Element; --------------- diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads index d32727ea9964..a1cad031c76f 100644 --- a/gcc/ada/libgnat/a-cforma.ads +++ b/gcc/ada/libgnat/a-cforma.ads @@ -400,6 +400,95 @@ is Model (Container)'Old, Key (Container, Position)); + function At_End + (E : not null access constant Map) return not null access constant Map + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function At_End + (E : access constant Element_Type) return access constant Element_Type + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function Constant_Reference + (Container : aliased Map; + Position : Cursor) return not null access constant Element_Type + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Constant_Reference'Result.all = + Element (Model (Container), Key (Container, Position)); + + function Reference + (Container : not null access Map; + Position : Cursor) return not null access Element_Type + with + Global => null, + Pre => Has_Element (Container.all, Position), + Post => + + -- Order of keys and cursors is preserved + + Keys (At_End (Container).all) = Keys (Container.all) + and Positions (At_End (Container).all) = Positions (Container.all) + + -- The value designated by the result of Reference is now associated + -- with the key at position Position in Container. + + and Element (At_End (Container).all, Position) = + At_End (Reference'Result).all + + -- Elements associated with other keys are preserved + + and M.Same_Keys + (Model (At_End (Container).all), + Model (Container.all)) + and M.Elements_Equal_Except + (Model (At_End (Container).all), + Model (Container.all), + Key (At_End (Container).all, Position)); + + function Constant_Reference + (Container : aliased Map; + Key : Key_Type) return not null access constant Element_Type + with + Global => null, + Pre => Contains (Container, Key), + Post => + Constant_Reference'Result.all = Element (Model (Container), Key); + + function Reference + (Container : not null access Map; + Key : Key_Type) return not null access Element_Type + with + Global => null, + Pre => Contains (Container.all, Key), + Post => + + -- Order of keys and cursors is preserved + + Keys (At_End (Container).all) = Keys (Container.all) + and Positions (At_End (Container).all) = Positions (Container.all) + + -- The value designated by the result of Reference is now associated + -- with Key in Container. + + and Element (Model (At_End (Container).all), Key) = + At_End (Reference'Result).all + + -- Elements associated with other keys are preserved + + and M.Same_Keys + (Model (At_End (Container).all), + Model (Container.all)) + and M.Elements_Equal_Except + (Model (At_End (Container).all), + Model (Container.all), + Key); + procedure Move (Target : in out Map; Source : in out Map) with Global => null, Pre => Target.Capacity >= Length (Source), @@ -1045,14 +1134,15 @@ private Right : Node_Access := 0; Color : Red_Black_Trees.Color_Type := Red; Key : Key_Type; - Element : Element_Type; + Element : aliased Element_Type; end record; package Tree_Types is new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); - type Map (Capacity : Count_Type) is - new Tree_Types.Tree_Type (Capacity) with null record; + type Map (Capacity : Count_Type) is record + Content : Tree_Types.Tree_Type (Capacity); + end record; Empty_Map : constant Map := (Capacity => 0, others => <>); diff --git a/gcc/ada/libgnat/a-cforse.adb b/gcc/ada/libgnat/a-cforse.adb index e5525b901e9d..7c45e4f12371 100644 --- a/gcc/ada/libgnat/a-cforse.adb +++ b/gcc/ada/libgnat/a-cforse.adb @@ -81,6 +81,10 @@ is -- Comments needed??? + procedure Assign + (Target : in out Tree_Types.Tree_Type; + Source : Tree_Types.Tree_Type); + generic with procedure Set_Element (Node : in out Node_Type); procedure Generic_Allocate @@ -90,13 +94,13 @@ is procedure Free (Tree : in out Set; X : Count_Type); procedure Insert_Sans_Hint - (Container : in out Set; + (Container : in out Tree_Types.Tree_Type; New_Item : Element_Type; Node : out Count_Type; Inserted : out Boolean); procedure Insert_With_Hint - (Dst_Set : in out Set; + (Dst_Set : in out Tree_Types.Tree_Type; Dst_Hint : Count_Type; Src_Node : Node_Type; Dst_Node : out Count_Type); @@ -141,7 +145,7 @@ is package Set_Ops is new Red_Black_Trees.Generic_Bounded_Set_Operations (Tree_Operations => Tree_Operations, - Set_Type => Set, + Set_Type => Tree_Types.Tree_Type, Assign => Assign, Insert_With_Hint => Insert_With_Hint, Is_Less => Is_Less_Node_Node); @@ -164,18 +168,19 @@ is return True; end if; - Lst := Next (Left, Last (Left).Node); + Lst := Next (Left.Content, Last (Left).Node); Node := First (Left).Node; while Node /= Lst loop - ENode := Find (Right, Left.Nodes (Node).Element).Node; + ENode := Find (Right, Left.Content.Nodes (Node).Element).Node; if ENode = 0 - or else Left.Nodes (Node).Element /= Right.Nodes (ENode).Element + or else Left.Content.Nodes (Node).Element /= + Right.Content.Nodes (ENode).Element then return False; end if; - Node := Next (Left, Node); + Node := Next (Left.Content, Node); end loop; return True; @@ -185,7 +190,10 @@ is -- Assign -- ------------ - procedure Assign (Target : in out Set; Source : Set) is + procedure Assign + (Target : in out Tree_Types.Tree_Type; + Source : Tree_Types.Tree_Type) + is procedure Append_Element (Source_Node : Count_Type); procedure Append_Elements is @@ -267,12 +275,18 @@ is Append_Elements (Source); end Assign; + procedure Assign (Target : in out Set; Source : Set) is + begin + Assign (Target.Content, Source.Content); + end Assign; + ------------- -- Ceiling -- ------------- function Ceiling (Container : Set; Item : Element_Type) return Cursor is - Node : constant Count_Type := Element_Keys.Ceiling (Container, Item); + Node : constant Count_Type := + Element_Keys.Ceiling (Container.Content, Item); begin if Node = 0 then @@ -288,7 +302,7 @@ is procedure Clear (Container : in out Set) is begin - Tree_Operations.Clear_Tree (Container); + Tree_Operations.Clear_Tree (Container.Content); end Clear; ----------- @@ -300,6 +314,25 @@ is return Node.Color; end Color; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Set; + Position : Cursor) return not null access constant Element_Type + is + begin + if not Has_Element (Container, Position) then + raise Constraint_Error with "Position cursor has no element"; + end if; + + pragma Assert (Vet (Container.Content, Position.Node), + "bad cursor in Element"); + + return Container.Content.Nodes (Position.Node).Element'Access; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -327,32 +360,32 @@ is end if; if Length (Source) > 0 then - Target.Length := Source.Length; - Target.Root := Source.Root; - Target.First := Source.First; - Target.Last := Source.Last; - Target.Free := Source.Free; + Target.Content.Length := Source.Content.Length; + Target.Content.Root := Source.Content.Root; + Target.Content.First := Source.Content.First; + Target.Content.Last := Source.Content.Last; + Target.Content.Free := Source.Content.Free; Node := 1; while Node <= Source.Capacity loop - Target.Nodes (Node).Element := - Source.Nodes (Node).Element; - Target.Nodes (Node).Parent := - Source.Nodes (Node).Parent; - Target.Nodes (Node).Left := - Source.Nodes (Node).Left; - Target.Nodes (Node).Right := - Source.Nodes (Node).Right; - Target.Nodes (Node).Color := - Source.Nodes (Node).Color; - Target.Nodes (Node).Has_Element := - Source.Nodes (Node).Has_Element; + Target.Content.Nodes (Node).Element := + Source.Content.Nodes (Node).Element; + Target.Content.Nodes (Node).Parent := + Source.Content.Nodes (Node).Parent; + Target.Content.Nodes (Node).Left := + Source.Content.Nodes (Node).Left; + Target.Content.Nodes (Node).Right := + Source.Content.Nodes (Node).Right; + Target.Content.Nodes (Node).Color := + Source.Content.Nodes (Node).Color; + Target.Content.Nodes (Node).Has_Element := + Source.Content.Nodes (Node).Has_Element; Node := Node + 1; end loop; while Node <= Target.Capacity loop N := Node; - Formal_Ordered_Sets.Free (Tree => Target, X => N); + Free (Tree => Target, X => N); Node := Node + 1; end loop; end if; @@ -370,25 +403,25 @@ is raise Constraint_Error with "Position cursor has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Delete"); - Tree_Operations.Delete_Node_Sans_Free (Container, + Tree_Operations.Delete_Node_Sans_Free (Container.Content, Position.Node); - Formal_Ordered_Sets.Free (Container, Position.Node); + Free (Container, Position.Node); Position := No_Element; end Delete; procedure Delete (Container : in out Set; Item : Element_Type) is - X : constant Count_Type := Element_Keys.Find (Container, Item); + X : constant Count_Type := Element_Keys.Find (Container.Content, Item); begin if X = 0 then raise Constraint_Error with "attempt to delete element not in set"; end if; - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Sets.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end Delete; ------------------ @@ -396,11 +429,11 @@ is ------------------ procedure Delete_First (Container : in out Set) is - X : constant Count_Type := Container.First; + X : constant Count_Type := Container.Content.First; begin if X /= 0 then - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Sets.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Delete_First; @@ -409,11 +442,11 @@ is ----------------- procedure Delete_Last (Container : in out Set) is - X : constant Count_Type := Container.Last; + X : constant Count_Type := Container.Content.Last; begin if X /= 0 then - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Sets.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Delete_Last; @@ -423,7 +456,7 @@ is procedure Difference (Target : in out Set; Source : Set) is begin - Set_Ops.Set_Difference (Target, Source); + Set_Ops.Set_Difference (Target.Content, Source.Content); end Difference; function Difference (Left, Right : Set) return Set is @@ -437,11 +470,12 @@ is end if; if Length (Right) = 0 then - return Left.Copy; + return Copy (Left); end if; return S : Set (Length (Left)) do - Assign (S, Set_Ops.Set_Difference (Left, Right)); + Assign + (S.Content, Set_Ops.Set_Difference (Left.Content, Right.Content)); end return; end Difference; @@ -455,10 +489,10 @@ is raise Constraint_Error with "Position cursor has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Element"); - return Container.Nodes (Position.Node).Element; + return Container.Content.Nodes (Position.Node).Element; end Element; ------------------------- @@ -506,7 +540,7 @@ is -- Start of processing for Equivalent_Sets begin - return Is_Equivalent (Left, Right); + return Is_Equivalent (Left.Content, Right.Content); end Equivalent_Sets; ------------- @@ -514,11 +548,11 @@ is ------------- procedure Exclude (Container : in out Set; Item : Element_Type) is - X : constant Count_Type := Element_Keys.Find (Container, Item); + X : constant Count_Type := Element_Keys.Find (Container.Content, Item); begin if X /= 0 then - Tree_Operations.Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Sets.Free (Container, X); + Tree_Operations.Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Exclude; @@ -527,7 +561,8 @@ is ---------- function Find (Container : Set; Item : Element_Type) return Cursor is - Node : constant Count_Type := Element_Keys.Find (Container, Item); + Node : constant Count_Type := + Element_Keys.Find (Container.Content, Item); begin if Node = 0 then @@ -547,7 +582,7 @@ is return No_Element; end if; - return (Node => Container.First); + return (Node => Container.Content.First); end First; ------------------- @@ -562,7 +597,7 @@ is end if; declare - N : Tree_Types.Nodes_Type renames Container.Nodes; + N : Tree_Types.Nodes_Type renames Container.Content.Nodes; begin return N (Fst).Element; end; @@ -575,7 +610,8 @@ is function Floor (Container : Set; Item : Element_Type) return Cursor is begin declare - Node : constant Count_Type := Element_Keys.Floor (Container, Item); + Node : constant Count_Type := + Element_Keys.Floor (Container.Content, Item); begin if Node = 0 then @@ -748,7 +784,7 @@ is -------------- function Elements (Container : Set) return E.Sequence is - Position : Count_Type := Container.First; + Position : Count_Type := Container.Content.First; R : E.Sequence; begin @@ -756,8 +792,8 @@ is -- for their postconditions. while Position /= 0 loop - R := E.Add (R, Container.Nodes (Position).Element); - Position := Tree_Operations.Next (Container, Position); + R := E.Add (R, Container.Content.Nodes (Position).Element); + Position := Tree_Operations.Next (Container.Content, Position); end loop; return R; @@ -873,7 +909,7 @@ is ----------- function Model (Container : Set) return M.Set is - Position : Count_Type := Container.First; + Position : Count_Type := Container.Content.First; R : M.Set; begin @@ -884,9 +920,9 @@ is R := M.Add (Container => R, - Item => Container.Nodes (Position).Element); + Item => Container.Content.Nodes (Position).Element); - Position := Tree_Operations.Next (Container, Position); + Position := Tree_Operations.Next (Container.Content, Position); end loop; return R; @@ -898,7 +934,7 @@ is function Positions (Container : Set) return P.Map is I : Count_Type := 1; - Position : Count_Type := Container.First; + Position : Count_Type := Container.Content.First; R : P.Map; begin @@ -908,7 +944,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); pragma Assert (P.Length (R) = I); - Position := Tree_Operations.Next (Container, Position); + Position := Tree_Operations.Next (Container.Content, Position); I := I + 1; end loop; @@ -923,8 +959,8 @@ is procedure Free (Tree : in out Set; X : Count_Type) is begin - Tree.Nodes (X).Has_Element := False; - Tree_Operations.Free (Tree, X); + Tree.Content.Nodes (X).Has_Element := False; + Tree_Operations.Free (Tree.Content, X); end Free; ---------------------- @@ -978,7 +1014,8 @@ is ------------- function Ceiling (Container : Set; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Keys.Ceiling (Container, Key); + Node : constant Count_Type := + Key_Keys.Ceiling (Container.Content, Key); begin if Node = 0 then @@ -1002,15 +1039,15 @@ is ------------ procedure Delete (Container : in out Set; Key : Key_Type) is - X : constant Count_Type := Key_Keys.Find (Container, Key); + X : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin if X = 0 then raise Constraint_Error with "attempt to delete key not in set"; end if; - Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Sets.Free (Container, X); + Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end Delete; ------------- @@ -1018,7 +1055,7 @@ is ------------- function Element (Container : Set; Key : Key_Type) return Element_Type is - Node : constant Count_Type := Key_Keys.Find (Container, Key); + Node : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin if Node = 0 then @@ -1026,7 +1063,7 @@ is end if; declare - N : Tree_Types.Nodes_Type renames Container.Nodes; + N : Tree_Types.Nodes_Type renames Container.Content.Nodes; begin return N (Node).Element; end; @@ -1052,11 +1089,11 @@ is ------------- procedure Exclude (Container : in out Set; Key : Key_Type) is - X : constant Count_Type := Key_Keys.Find (Container, Key); + X : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin if X /= 0 then - Delete_Node_Sans_Free (Container, X); - Formal_Ordered_Sets.Free (Container, X); + Delete_Node_Sans_Free (Container.Content, X); + Free (Container, X); end if; end Exclude; @@ -1065,7 +1102,7 @@ is ---------- function Find (Container : Set; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Keys.Find (Container, Key); + Node : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin return (if Node = 0 then No_Element else (Node => Node)); end Find; @@ -1075,7 +1112,7 @@ is ----------- function Floor (Container : Set; Key : Key_Type) return Cursor is - Node : constant Count_Type := Key_Keys.Floor (Container, Key); + Node : constant Count_Type := Key_Keys.Floor (Container.Content, Key); begin return (if Node = 0 then No_Element else (Node => Node)); end Floor; @@ -1225,11 +1262,11 @@ is "Position cursor has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Key"); declare - N : Tree_Types.Nodes_Type renames Container.Nodes; + N : Tree_Types.Nodes_Type renames Container.Content.Nodes; begin return Key (N (Position.Node).Element); end; @@ -1244,7 +1281,7 @@ is Key : Key_Type; New_Item : Element_Type) is - Node : constant Count_Type := Key_Keys.Find (Container, Key); + Node : constant Count_Type := Key_Keys.Find (Container.Content, Key); begin if not Has_Element (Container, (Node => Node)) then raise Constraint_Error with @@ -1265,7 +1302,7 @@ is if Position.Node = 0 then return False; else - return Container.Nodes (Position.Node).Has_Element; + return Container.Content.Nodes (Position.Node).Has_Element; end if; end Has_Element; @@ -1282,7 +1319,7 @@ is if not Inserted then declare - N : Tree_Types.Nodes_Type renames Container.Nodes; + N : Tree_Types.Nodes_Type renames Container.Content.Nodes; begin N (Position.Node).Element := New_Item; end; @@ -1300,7 +1337,7 @@ is Inserted : out Boolean) is begin - Insert_Sans_Hint (Container, New_Item, Position.Node, Inserted); + Insert_Sans_Hint (Container.Content, New_Item, Position.Node, Inserted); end Insert; procedure Insert @@ -1324,7 +1361,7 @@ is ---------------------- procedure Insert_Sans_Hint - (Container : in out Set; + (Container : in out Tree_Types.Tree_Type; New_Item : Element_Type; Node : out Count_Type; Inserted : out Boolean) @@ -1377,7 +1414,7 @@ is ---------------------- procedure Insert_With_Hint - (Dst_Set : in out Set; + (Dst_Set : in out Tree_Types.Tree_Type; Dst_Hint : Count_Type; Src_Node : Node_Type; Dst_Node : out Count_Type) @@ -1439,17 +1476,18 @@ is procedure Intersection (Target : in out Set; Source : Set) is begin - Set_Ops.Set_Intersection (Target, Source); + Set_Ops.Set_Intersection (Target.Content, Source.Content); end Intersection; function Intersection (Left, Right : Set) return Set is begin if Left'Address = Right'Address then - return Left.Copy; + return Copy (Left); end if; return S : Set (Count_Type'Min (Length (Left), Length (Right))) do - Assign (S, Set_Ops.Set_Intersection (Left, Right)); + Assign (S.Content, + Set_Ops.Set_Intersection (Left.Content, Right.Content)); end return; end Intersection; @@ -1503,7 +1541,7 @@ is function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is begin - return Set_Ops.Set_Subset (Subset, Of_Set => Of_Set); + return Set_Ops.Set_Subset (Subset.Content, Of_Set => Of_Set.Content); end Is_Subset; ---------- @@ -1514,7 +1552,7 @@ is begin return (if Length (Container) = 0 then No_Element - else (Node => Container.Last)); + else (Node => Container.Content.Last)); end Last; ------------------ @@ -1528,7 +1566,7 @@ is end if; declare - N : Tree_Types.Nodes_Type renames Container.Nodes; + N : Tree_Types.Nodes_Type renames Container.Content.Nodes; begin return N (Last (Container).Node).Element; end; @@ -1549,7 +1587,7 @@ is function Length (Container : Set) return Count_Type is begin - return Container.Length; + return Container.Content.Length; end Length; ---------- @@ -1557,7 +1595,7 @@ is ---------- procedure Move (Target : in out Set; Source : in out Set) is - N : Tree_Types.Nodes_Type renames Source.Nodes; + N : Tree_Types.Nodes_Type renames Source.Content.Nodes; X : Count_Type; begin @@ -1573,13 +1611,13 @@ is Clear (Target); loop - X := Source.First; + X := Source.Content.First; exit when X = 0; Insert (Target, N (X).Element); -- optimize??? - Tree_Operations.Delete_Node_Sans_Free (Source, X); - Formal_Ordered_Sets.Free (Source, X); + Tree_Operations.Delete_Node_Sans_Free (Source.Content, X); + Free (Source, X); end loop; end Move; @@ -1597,9 +1635,9 @@ is raise Constraint_Error; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Next"); - return (Node => Tree_Operations.Next (Container, Position.Node)); + return (Node => Tree_Operations.Next (Container.Content, Position.Node)); end Next; procedure Next (Container : Set; Position : in out Cursor) is @@ -1613,7 +1651,7 @@ is function Overlap (Left, Right : Set) return Boolean is begin - return Set_Ops.Set_Overlap (Left, Right); + return Set_Ops.Set_Overlap (Left.Content, Right.Content); end Overlap; ------------ @@ -1639,12 +1677,12 @@ is raise Constraint_Error; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Previous"); declare Node : constant Count_Type := - Tree_Operations.Previous (Container, Position.Node); + Tree_Operations.Previous (Container.Content, Position.Node); begin return (if Node = 0 then No_Element else (Node => Node)); end; @@ -1660,7 +1698,8 @@ is ------------- procedure Replace (Container : in out Set; New_Item : Element_Type) is - Node : constant Count_Type := Element_Keys.Find (Container, New_Item); + Node : constant Count_Type := + Element_Keys.Find (Container.Content, New_Item); begin if Node = 0 then @@ -1668,7 +1707,7 @@ is "attempt to replace element not in set"; end if; - Container.Nodes (Node).Element := New_Item; + Container.Content.Nodes (Node).Element := New_Item; end Replace; --------------------- @@ -1696,7 +1735,7 @@ is (Local_Insert_Post, Local_Insert_Sans_Hint); - NN : Tree_Types.Nodes_Type renames Tree.Nodes; + NN : Tree_Types.Nodes_Type renames Tree.Content.Nodes; -------------- -- New_Node -- @@ -1730,7 +1769,7 @@ is return; end if; - Hint := Element_Keys.Ceiling (Tree, Item); + Hint := Element_Keys.Ceiling (Tree.Content, Item); if Hint = 0 then null; @@ -1746,10 +1785,10 @@ is raise Program_Error with "attempt to replace existing element"; end if; - Tree_Operations.Delete_Node_Sans_Free (Tree, Node); + Tree_Operations.Delete_Node_Sans_Free (Tree.Content, Node); Local_Insert_With_Hint - (Tree => Tree, + (Tree => Tree.Content, Position => Hint, Key => Item, Node => Result, @@ -1770,7 +1809,7 @@ is "Position cursor has no element"; end if; - pragma Assert (Vet (Container, Position.Node), + pragma Assert (Vet (Container.Content, Position.Node), "bad cursor in Replace_Element"); Replace_Element (Container, Position.Node, New_Item); @@ -1830,7 +1869,7 @@ is procedure Symmetric_Difference (Target : in out Set; Source : Set) is begin - Set_Ops.Set_Symmetric_Difference (Target, Source); + Set_Ops.Set_Symmetric_Difference (Target.Content, Source.Content); end Symmetric_Difference; function Symmetric_Difference (Left, Right : Set) return Set is @@ -1840,15 +1879,17 @@ is end if; if Length (Right) = 0 then - return Left.Copy; + return Copy (Left); end if; if Length (Left) = 0 then - return Right.Copy; + return Copy (Right); end if; return S : Set (Length (Left) + Length (Right)) do - Assign (S, Set_Ops.Set_Symmetric_Difference (Left, Right)); + Assign + (S.Content, + Set_Ops.Set_Symmetric_Difference (Left.Content, Right.Content)); end return; end Symmetric_Difference; @@ -1861,7 +1902,7 @@ is Inserted : Boolean; begin return S : Set (Capacity => 1) do - Insert_Sans_Hint (S, New_Item, Node, Inserted); + Insert_Sans_Hint (S.Content, New_Item, Node, Inserted); pragma Assert (Inserted); end return; end To_Set; @@ -1872,21 +1913,21 @@ is procedure Union (Target : in out Set; Source : Set) is begin - Set_Ops.Set_Union (Target, Source); + Set_Ops.Set_Union (Target.Content, Source.Content); end Union; function Union (Left, Right : Set) return Set is begin if Left'Address = Right'Address then - return Left.Copy; + return Copy (Left); end if; if Length (Left) = 0 then - return Right.Copy; + return Copy (Right); end if; if Length (Right) = 0 then - return Left.Copy; + return Copy (Left); end if; return S : Set (Length (Left) + Length (Right)) do diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads index 12d2d3c4758b..e1d7c917a648 100644 --- a/gcc/ada/libgnat/a-cforse.ads +++ b/gcc/ada/libgnat/a-cforse.ads @@ -529,6 +529,16 @@ is Position => Position) and Positions (Container) = Positions (Container)'Old; + function Constant_Reference + (Container : aliased Set; + Position : Cursor) return not null access constant Element_Type + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Constant_Reference'Result.all = + E.Get (Elements (Container), P.Get (Positions (Container), Position)); + procedure Move (Target : in out Set; Source : in out Set) with Global => null, Pre => Target.Capacity >= Length (Source), @@ -1770,18 +1780,19 @@ private type Node_Type is record Has_Element : Boolean := False; - Parent : Count_Type := 0; - Left : Count_Type := 0; - Right : Count_Type := 0; - Color : Red_Black_Trees.Color_Type; - Element : Element_Type; + Parent : Count_Type := 0; + Left : Count_Type := 0; + Right : Count_Type := 0; + Color : Red_Black_Trees.Color_Type; + Element : aliased Element_Type; end record; package Tree_Types is new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); - type Set (Capacity : Count_Type) is - new Tree_Types.Tree_Type (Capacity) with null record; + type Set (Capacity : Count_Type) is record + Content : Tree_Types.Tree_Type (Capacity); + end record; use Red_Black_Trees; diff --git a/gcc/ada/libgnat/a-coboho.adb b/gcc/ada/libgnat/a-coboho.adb index 32346d045664..21b9f5485a28 100644 --- a/gcc/ada/libgnat/a-coboho.adb +++ b/gcc/ada/libgnat/a-coboho.adb @@ -65,6 +65,26 @@ package body Ada.Containers.Bounded_Holders is return Get (Left) = Get (Right); end "="; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Holder) return not null access constant Element_Type + is + begin + return Cast (Container'Address); + end Constant_Reference; + + --------- + -- Get -- + --------- + + function Get (Container : Holder) return Element_Type is + begin + return Cast (Container'Address).all; + end Get; + --------------- -- Put_Image -- --------------- @@ -79,14 +99,16 @@ package body Ada.Containers.Bounded_Holders is Array_After (S); end Put_Image; - --------- - -- Get -- - --------- + --------------- + -- Reference -- + --------------- - function Get (Container : Holder) return Element_Type is + function Reference + (Container : not null access Holder) return not null access Element_Type + is begin - return Cast (Container'Address).all; - end Get; + return Cast (Container.all'Address); + end Reference; --------- -- Set -- diff --git a/gcc/ada/libgnat/a-coboho.ads b/gcc/ada/libgnat/a-coboho.ads index 9dd73baed92b..086f19410c79 100644 --- a/gcc/ada/libgnat/a-coboho.ads +++ b/gcc/ada/libgnat/a-coboho.ads @@ -81,6 +81,12 @@ package Ada.Containers.Bounded_Holders is procedure Set (Container : in out Holder; New_Item : Element_Type); + function Constant_Reference + (Container : aliased Holder) return not null access constant Element_Type; + + function Reference + (Container : not null access Holder) return not null access Element_Type; + private -- The implementation uses low-level tricks (Address clauses and unchecked diff --git a/gcc/ada/libgnat/a-cofove.adb b/gcc/ada/libgnat/a-cofove.adb index a1f13edc408c..c7f4f06005e0 100644 --- a/gcc/ada/libgnat/a-cofove.adb +++ b/gcc/ada/libgnat/a-cofove.adb @@ -142,6 +142,22 @@ is Container.Last := No_Index; end Clear; + ------------------------ + -- Constant_Reference -- + ------------------------ + + function Constant_Reference + (Container : aliased Vector; + Index : Index_Type) return not null access constant Element_Type + is + begin + if Index > Container.Last then + raise Constraint_Error with "Index is out of range"; + end if; + + return Container.Elements (To_Array_Index (Index))'Access; + end Constant_Reference; + -------------- -- Contains -- -------------- @@ -1096,6 +1112,22 @@ is end; end Replace_Element; + --------------- + -- Reference -- + --------------- + + function Reference + (Container : not null access Vector; + Index : Index_Type) return not null access Element_Type + is + begin + if Index > Container.Last then + raise Constraint_Error with "Index is out of range"; + end if; + + return Container.Elements (To_Array_Index (Index))'Access; + end Reference; + ---------------------- -- Reserve_Capacity -- ---------------------- diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads index 61115ddc467c..a4ed7e5d385a 100644 --- a/gcc/ada/libgnat/a-cofove.ads +++ b/gcc/ada/libgnat/a-cofove.ads @@ -290,6 +290,48 @@ is Right => Model (Container), Position => Index); + function At_End (E : access constant Vector) return access constant Vector + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function At_End + (E : access constant Element_Type) return access constant Element_Type + is (E) + with Ghost, + Annotate => (GNATprove, At_End_Borrow); + + function Constant_Reference + (Container : aliased Vector; + Index : Index_Type) return not null access constant Element_Type + with + Global => null, + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => + Constant_Reference'Result.all = Element (Model (Container), Index); + + function Reference + (Container : not null access Vector; + Index : Index_Type) return not null access Element_Type + with + Global => null, + Pre => + Index in First_Index (Container.all) .. Last_Index (Container.all), + Post => + Length (Container.all) = Length (At_End (Container).all) + + -- Container will have Result.all at index Index + + and At_End (Reference'Result).all = + Element (Model (At_End (Container).all), Index) + + -- All other elements are preserved + + and M.Equal_Except + (Left => Model (Container.all), + Right => Model (At_End (Container).all), + Position => Index); + procedure Insert (Container : in out Vector; Before : Extended_Index; @@ -905,7 +947,7 @@ private pragma Inline (Contains); subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; - type Elements_Array is array (Array_Index range <>) of Element_Type; + type Elements_Array is array (Array_Index range <>) of aliased Element_Type; function "=" (L, R : Elements_Array) return Boolean is abstract; type Vector (Capacity : Capacity_Range) is record diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads index ca872e2288fd..a1dd76406a4a 100644 --- a/gcc/ada/libgnat/a-cofuma.ads +++ b/gcc/ada/libgnat/a-cofuma.ads @@ -302,6 +302,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Global => null, Pre => Has_Witness (Container, Witness); + function Copy_Key (Key : Key_Type) return Key_Type is (Key); + function Copy_Element (Item : Element_Type) return Element_Type is (Item); + -- Elements and Keys of maps are copied by numerous primitives in this + -- package. This function causes GNATprove to verify that such a copy is + -- valid (in particular, it does not break the ownership policy of SPARK, + -- i.e. it does not contain pointers that could be used to alias mutable + -- data). + --------------------------- -- Iteration Primitives -- --------------------------- diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads index d852be90263b..d0acba7a012f 100644 --- a/gcc/ada/libgnat/a-cofuse.ads +++ b/gcc/ada/libgnat/a-cofuse.ads @@ -249,6 +249,13 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is and Right <= Union'Result and Included_In_Union (Union'Result, Left, Right); + function Copy_Element (Item : Element_Type) return Element_Type is (Item); + -- Elements of containers are copied by numerous primitives in this + -- package. This function causes GNATprove to verify that such a copy is + -- valid (in particular, it does not break the ownership policy of SPARK, + -- i.e. it does not contain pointers that could be used to alias mutable + -- data). + --------------------------- -- Iteration Primitives -- --------------------------- diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads index bdd0e94db995..ee5273039d39 100644 --- a/gcc/ada/libgnat/a-cofuve.ads +++ b/gcc/ada/libgnat/a-cofuve.ads @@ -336,6 +336,13 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Lst => Last (Remove'Result), Offset => 1); + function Copy_Element (Item : Element_Type) return Element_Type is (Item); + -- Elements of containers are copied by numerous primitives in this + -- package. This function causes GNATprove to verify that such a copy is + -- valid (in particular, it does not break the ownership policy of SPARK, + -- i.e. it does not contain pointers that could be used to alias mutable + -- data). + --------------------------- -- Iteration Primitives -- ---------------------------