From 584b52902b4b1bbcabc0e5bdd4196bd223d2f5a8 Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Fri, 5 Jul 2019 07:01:45 +0000 Subject: [PATCH] [Ada] Ada.Containers.Formal_Vectors: make vectors always bounded 2019-07-05 Claire Dross gcc/ada/ * libgnat/a-cofove.ads, libgnat/a-cofove.adb: Definite formal vectors are now always bounded so that they do not need to be limited anymore. From-SVN: r273102 --- gcc/ada/ChangeLog | 6 ++ gcc/ada/libgnat/a-cofove.adb | 183 ++++++----------------------------- gcc/ada/libgnat/a-cofove.ads | 59 ++--------- 3 files changed, 44 insertions(+), 204 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index aac81ea1f93..42fa71bddd4 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2019-07-05 Claire Dross + + * libgnat/a-cofove.ads, libgnat/a-cofove.adb: Definite formal + vectors are now always bounded so that they do not need to be + limited anymore. + 2019-07-05 Dmitriy Anisimkov * libgnat/g-traceb.ads, libgnat/g-traceb.adb (Call_Chain): New diff --git a/gcc/ada/libgnat/a-cofove.adb b/gcc/ada/libgnat/a-cofove.adb index f9675abdeac..c848ad83990 100644 --- a/gcc/ada/libgnat/a-cofove.adb +++ b/gcc/ada/libgnat/a-cofove.adb @@ -26,7 +26,6 @@ ------------------------------------------------------------------------------ with Ada.Containers.Generic_Array_Sort; -with Ada.Unchecked_Deallocation; with System; use type System.Address; @@ -34,41 +33,10 @@ package body Ada.Containers.Formal_Vectors with SPARK_Mode => Off is - Growth_Factor : constant := 2; - -- When growing a container, multiply current capacity by this. Doubling - -- leads to amortized linear-time copying. - type Int is range System.Min_Int .. System.Max_Int; - procedure Free is - new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); - - type Maximal_Array_Ptr is access all Elements_Array (Array_Index) - with Storage_Size => 0; - type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index) - with Storage_Size => 0; - - function Elems (Container : in out Vector) return Maximal_Array_Ptr; - function Elemsc - (Container : Vector) return Maximal_Array_Ptr_Const; - -- Returns a pointer to the Elements array currently in use -- either - -- Container.Elements_Ptr or a pointer to Container.Elements. We work with - -- pointers to a bogus array subtype that is constrained with the maximum - -- possible bounds. This means that the pointer is a thin pointer. This is - -- necessary because 'Unrestricted_Access doesn't work when it produces - -- access-to-unconstrained and is returned from a function. - -- - -- Note that this is dangerous: make sure calls to this use an indexed - -- component or slice that is within the bounds 1 .. Length (Container). - - function Get_Element - (Container : Vector; - Position : Capacity_Range) return Element_Type; - function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base; - function Current_Capacity (Container : Vector) return Capacity_Range; - procedure Insert_Space (Container : in out Vector; Before : Extended_Index; @@ -89,7 +57,7 @@ is end if; for J in 1 .. Length (Left) loop - if Get_Element (Left, J) /= Get_Element (Right, J) then + if Left.Elements (J) /= Right.Elements (J) then return False; end if; end loop; @@ -148,7 +116,7 @@ is return; end if; - if Bounded and then Target.Capacity < LS then + if Target.Capacity < LS then raise Constraint_Error; end if; @@ -162,11 +130,7 @@ is function Capacity (Container : Vector) return Capacity_Range is begin - return - (if Bounded then - Container.Capacity - else - Capacity_Range'Last); + return Container.Capacity; end Capacity; ----------- @@ -176,10 +140,6 @@ is procedure Clear (Container : in out Vector) is begin Container.Last := No_Index; - - -- Free element, note that this is OK if Elements_Ptr is null - - Free (Container.Elements_Ptr); end Clear; -------------- @@ -215,24 +175,11 @@ is end if; return Target : Vector (C) do - Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS); + Target.Elements (1 .. LS) := Source.Elements (1 .. LS); Target.Last := Source.Last; end return; end Copy; - ---------------------- - -- Current_Capacity -- - ---------------------- - - function Current_Capacity (Container : Vector) return Capacity_Range is - begin - return - (if Container.Elements_Ptr = null then - Container.Elements'Length - else - Container.Elements_Ptr.all'Length); - end Current_Capacity; - ------------ -- Delete -- ------------ @@ -333,7 +280,7 @@ is -- so we just slide down to Index the elements that weren't deleted. declare - EA : Maximal_Array_Ptr renames Elems (Container); + EA : Elements_Array renames Container.Elements; Idx : constant Count_Type := EA'First + Off; begin EA (Idx .. Old_Len - Count) := EA (Idx + Count .. Old_Len); @@ -418,32 +365,10 @@ is II : constant Int'Base := Int (Index) - Int (No_Index); I : constant Capacity_Range := Capacity_Range (II); begin - return Get_Element (Container, I); + return Container.Elements (I); end; end Element; - ----------- - -- Elems -- - ----------- - - function Elems (Container : in out Vector) return Maximal_Array_Ptr is - begin - return - (if Container.Elements_Ptr = null then - Container.Elements'Unrestricted_Access - else - Container.Elements_Ptr.all'Unrestricted_Access); - end Elems; - - function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is - begin - return - (if Container.Elements_Ptr = null then - Container.Elements'Unrestricted_Access - else - Container.Elements_Ptr.all'Unrestricted_Access); - end Elemsc; - ---------------- -- Find_Index -- ---------------- @@ -459,7 +384,7 @@ is begin K := Capacity_Range (Int (Index) - Int (No_Index)); for Indx in Index .. Last loop - if Get_Element (Container, K) = Item then + if Container.Elements (K) = Item then return Indx; end if; @@ -478,7 +403,7 @@ is if Is_Empty (Container) then raise Constraint_Error with "Container is empty"; else - return Get_Element (Container, 1); + return Container.Elements (1); end if; end First_Element; @@ -622,7 +547,7 @@ is begin for Position in 1 .. Length (Container) loop - R := M.Add (R, Elemsc (Container) (Position)); + R := M.Add (R, Container.Elements (Position)); end loop; return R; @@ -684,8 +609,8 @@ is begin for J in 1 .. L - 1 loop - if Get_Element (Container, J + 1) < - Get_Element (Container, J) + if Container.Elements (J + 1) < + Container.Elements (J) then return False; end if; @@ -712,7 +637,7 @@ is if Container.Last <= Index_Type'First then return; else - Sort (Elems (Container) (1 .. Len)); + Sort (Container.Elements (1 .. Len)); end if; end Sort; @@ -744,16 +669,6 @@ is New_Length : constant Count_Type := I + Length (Source); begin - if not Bounded - and then Current_Capacity (Target) < Capacity_Range (New_Length) - then - Reserve_Capacity - (Target, - Capacity_Range'Max - (Current_Capacity (Target) * Growth_Factor, - Capacity_Range (New_Length))); - end if; - if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then Target.Last := No_Index + Index_Type'Base (New_Length); @@ -764,8 +679,8 @@ is end; declare - TA : Maximal_Array_Ptr renames Elems (Target); - SA : Maximal_Array_Ptr renames Elems (Source); + TA : Elements_Array renames Target.Elements; + SA : Elements_Array renames Source.Elements; begin J := Length (Target); @@ -792,18 +707,6 @@ is end Generic_Sorting; - ----------------- - -- Get_Element -- - ----------------- - - function Get_Element - (Container : Vector; - Position : Capacity_Range) return Element_Type - is - begin - return Elemsc (Container) (Position); - end Get_Element; - ----------------- -- Has_Element -- ----------------- @@ -844,7 +747,7 @@ is J := To_Array_Index (Before); - Elems (Container) (J .. J - 1 + Count) := (others => New_Item); + Container.Elements (J .. J - 1 + Count) := (others => New_Item); end Insert; procedure Insert @@ -876,7 +779,7 @@ is B := To_Array_Index (Before); - Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N); + Container.Elements (B .. B + N - 1) := New_Item.Elements (1 .. N); end Insert; ------------------ @@ -1053,19 +956,8 @@ is J := To_Array_Index (Before); - -- Increase the capacity of container if needed - - if not Bounded - and then Current_Capacity (Container) < Capacity_Range (New_Length) - then - Reserve_Capacity - (Container, - Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor, - Capacity_Range (New_Length))); - end if; - declare - EA : Maximal_Array_Ptr renames Elems (Container); + EA : Elements_Array renames Container.Elements; begin if Before <= Container.Last then @@ -1105,7 +997,7 @@ is if Is_Empty (Container) then raise Constraint_Error with "Container is empty"; else - return Get_Element (Container, Length (Container)); + return Container.Elements (Length (Container)); end if; end Last_Element; @@ -1143,7 +1035,7 @@ is return; end if; - if Bounded and then Target.Capacity < LS then + if Target.Capacity < LS then raise Constraint_Error; end if; @@ -1194,7 +1086,7 @@ is I : constant Capacity_Range := Capacity_Range (II); begin - Elems (Container) (I) := New_Item; + Container.Elements (I) := New_Item; end; end Replace_Element; @@ -1207,24 +1099,8 @@ is Capacity : Capacity_Range) is begin - if Bounded then - if Capacity > Container.Capacity then - raise Constraint_Error with "Capacity is out of range"; - end if; - - else - if Capacity > Formal_Vectors.Current_Capacity (Container) then - declare - New_Elements : constant Elements_Array_Ptr := - new Elements_Array (1 .. Capacity); - L : constant Capacity_Range := Length (Container); - - begin - New_Elements (1 .. L) := Elemsc (Container) (1 .. L); - Free (Container.Elements_Ptr); - Container.Elements_Ptr := New_Elements; - end; - end if; + if Capacity > Container.Capacity then + raise Constraint_Error with "Capacity is out of range"; end if; end Reserve_Capacity; @@ -1241,7 +1117,7 @@ is declare I, J : Capacity_Range; E : Elements_Array renames - Elems (Container) (1 .. Length (Container)); + Container.Elements (1 .. Length (Container)); begin I := 1; @@ -1282,7 +1158,7 @@ is K := Capacity_Range (Int (Last) - Int (No_Index)); for Indx in reverse Index_Type'First .. Last loop - if Get_Element (Container, K) = Item then + if Container.Elements (K) = Item then return Indx; end if; @@ -1318,8 +1194,8 @@ is II : constant Int'Base := Int (I) - Int (No_Index); JJ : constant Int'Base := Int (J) - Int (No_Index); - EI : Element_Type renames Elems (Container) (Capacity_Range (II)); - EJ : Element_Type renames Elems (Container) (Capacity_Range (JJ)); + EI : Element_Type renames Container.Elements (Capacity_Range (II)); + EJ : Element_Type renames Container.Elements (Capacity_Range (JJ)); EI_Copy : constant Element_Type := EI; @@ -1388,10 +1264,9 @@ is Last := Index_Type (Last_As_Int); return - (Capacity => Length, - Last => Last, - Elements_Ptr => <>, - Elements => (others => New_Item)); + (Capacity => Length, + Last => Last, + Elements => (others => New_Item)); end; end To_Vector; diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads index 635ef489476..5b62664097c 100644 --- a/gcc/ada/libgnat/a-cofove.ads +++ b/gcc/ada/libgnat/a-cofove.ads @@ -40,12 +40,6 @@ with Ada.Containers.Functional_Vectors; generic type Index_Type is range <>; type Element_Type is private; - - Bounded : Boolean := True; - -- If True, the containers are bounded; the initial capacity is the maximum - -- size, and heap allocation will be avoided. If False, the containers can - -- grow via heap allocation. - package Ada.Containers.Formal_Vectors with SPARK_Mode is @@ -73,17 +67,8 @@ is subtype Capacity_Range is Count_Type range 0 .. Last_Count; - type Vector (Capacity : Capacity_Range) is limited private with + type Vector (Capacity : Capacity_Range) is private with Default_Initial_Condition => Is_Empty (Vector); - -- In the bounded case, Capacity is the capacity of the container, which - -- never changes. In the unbounded case, Capacity is the initial capacity - -- of the container, and operations such as Reserve_Capacity and Append can - -- increase the capacity. The capacity never shrinks, except in the case of - -- Clear. - -- - -- Note that all objects of type Vector are constrained, including in the - -- unbounded case; you can't assign from one object to another if the - -- Capacity is different. function Length (Container : Vector) return Capacity_Range with Global => null, @@ -220,11 +205,7 @@ is function Capacity (Container : Vector) return Capacity_Range with Global => null, Post => - Capacity'Result = - (if Bounded then - Container.Capacity - else - Capacity_Range'Last); + Capacity'Result = Container.Capacity; pragma Annotate (GNATprove, Inline_For_Proof, Capacity); procedure Reserve_Capacity @@ -232,7 +213,7 @@ is Capacity : Capacity_Range) with Global => null, - Pre => (if Bounded then Capacity <= Container.Capacity), + Pre => Capacity <= Container.Capacity, Post => Model (Container) = Model (Container)'Old; function Is_Empty (Container : Vector) return Boolean with @@ -242,13 +223,10 @@ is procedure Clear (Container : in out Vector) with Global => null, Post => Length (Container) = 0; - -- Note that this reclaims storage in the unbounded case. You need to call - -- this before a container goes out of scope in order to avoid storage - -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. procedure Assign (Target : in out Vector; Source : Vector) with Global => null, - Pre => (if Bounded then Length (Source) <= Target.Capacity), + Pre => Length (Source) <= Target.Capacity, Post => Model (Target) = Model (Source); function Copy @@ -256,7 +234,7 @@ is Capacity : Capacity_Range := 0) return Vector with Global => null, - Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), + Pre => (Capacity = 0 or Length (Source) <= Capacity), Post => Model (Copy'Result) = Model (Source) and (if Capacity = 0 then @@ -267,7 +245,7 @@ is procedure Move (Target : in out Vector; Source : in out Vector) with Global => null, - Pre => (if Bounded then Length (Source) <= Capacity (Target)), + Pre => Length (Source) <= Capacity (Target), Post => Model (Target) = Model (Source)'Old and Length (Source) = 0; function Element @@ -894,30 +872,11 @@ private type Elements_Array is array (Array_Index range <>) of Element_Type; function "=" (L, R : Elements_Array) return Boolean is abstract; - type Elements_Array_Ptr is access all Elements_Array; - - type Vector (Capacity : Capacity_Range) is limited record - - -- In the bounded case, the elements are stored in Elements. In the - -- unbounded case, the elements are initially stored in Elements, until - -- we run out of room, then we switch to Elements_Ptr. - - Last : Extended_Index := No_Index; - Elements_Ptr : Elements_Array_Ptr := null; - Elements : aliased Elements_Array (1 .. Capacity); + type Vector (Capacity : Capacity_Range) is record + Last : Extended_Index := No_Index; + Elements : Elements_Array (1 .. Capacity); end record; - -- The primary reason Vector is limited is that in the unbounded case, once - -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will - -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr, - -- so for example "Append (X, ...);" will modify BOTH X and Y. That would - -- allow SPARK to "prove" things that are false. We could fix that by - -- making Vector a controlled type, and override Adjust to make a deep - -- copy, but finalization is not allowed in SPARK. - -- - -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not - -- allowed on Vectors. - function Empty_Vector return Vector is ((Capacity => 0, others => <>)); -- 2.30.2