From: Arnaud Charlet Date: Thu, 27 Apr 2017 11:01:32 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6d25cadecc8f573fa66131b8a89c9047d596794;p=gcc.git [multiple changes] 2017-04-27 Hristian Kirtchev * sem_elab.adb Add new type Visited_Element and update the contents of table Elab_Visited. Various code clean up. (Check_Elab_Call): Determine whether a prior call to the same subprogram was already examined within the same context. (Check_Internal_Call_Continue): Register the subprogram being called as examined within a particular context. Do not suppress elaboration warnings. 2017-04-27 Gary Dismukes * xoscons.adb, osint.ads: Minor reformatting. 2017-04-27 Bob Duff * g-dyntab.ads, g-dyntab.adb: Misc cleanup. Rename Table_Count_Type --> Table_Last_Type, because the name was confusing (a "count" usually starts at zero). Add functionality supported or needed by other tables packages (Move, Release_Threshold). * g-table.ads, g-table.adb: This is now just a thin wrapper around g-dyntab.ads/g-dyntab.adb. Add functionality supported or needed by other tables packages (Save, Restore). * table.ads, table.adb: This is now just a thin wrapper around * g-table.ads/g-table.adb. * namet.h, scos.h, uintp.h: These files are reaching into the private data of some instances of g-table, whose names changed, so the above change requires some adjustment here. It now uses public interfaces. 2017-04-27 Bob Duff * namet.adb, namet.ads: Minor: remove unused procedures. 2017-04-27 Eric Botcazou * checks.adb (Apply_Scalar_Range_Check): Initialize Ok variable too. (Minimize_Eliminate_Overflows): Initialize Llo and Lhi. Add pragma Warnings on Rtype variable in nested block. * * exp_ch3.adb (Build_Init_Statements): Initialize VAR_LOC. * exp_ch4.adb (Expand_Concatenate): Initialize 3 variables. (Size_In_Storage_Elements): Add pragma Warnings on Res variable. * exp_ch7.adb (Build_Adjust_Statements): Initialize Bod_Stmts. (Process_Component_List_For_Finalize): Initialize Counter_Id. (Build_Finalize_Statements): Initialize Bod_Stmts. * exp_disp.adb (Expand_Dispatching_Call): Initialize SCIL_Node. 2017-04-27 Claire Dross * a-cfhama.adb, a-cfhamai.ads (=): Generic parameter removed to allow the use of regular equality over elements in contracts. (Formal_Model): Ghost package containing model functions that are used in subprogram contracts. (Current_To_Last): Removed, model functions should be used instead. (First_To_Previous): Removed, model functions should be used instead. (Strict_Equal): Removed, model functions should be used instead. (No_Overlap): Removed, model functions should be used instead. (Equivalent_Keys): Functions over cursors are removed. They were awkward with explicit container parameters. * a-cofuma.adb, a-cofuma.ads (Lift_Equivalent_Keys): New lemma (proof only) procedure to help GNATprove when equivalence over keys is not equality. From-SVN: r247320 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d8863a2f816..d68ec0edd37 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,68 @@ +2017-04-27 Hristian Kirtchev + + * sem_elab.adb Add new type Visited_Element + and update the contents of table Elab_Visited. Various code clean up. + (Check_Elab_Call): Determine whether a prior call to + the same subprogram was already examined within the same context. + (Check_Internal_Call_Continue): Register the subprogram being + called as examined within a particular context. Do not suppress + elaboration warnings. + +2017-04-27 Gary Dismukes + + * xoscons.adb, osint.ads: Minor reformatting. + +2017-04-27 Bob Duff + + * g-dyntab.ads, g-dyntab.adb: Misc cleanup. Rename + Table_Count_Type --> Table_Last_Type, because the name + was confusing (a "count" usually starts at zero). Add + functionality supported or needed by other tables packages + (Move, Release_Threshold). + * g-table.ads, g-table.adb: This is now just a thin wrapper + around g-dyntab.ads/g-dyntab.adb. Add functionality supported + or needed by other tables packages (Save, Restore). + * table.ads, table.adb: This is now just a thin wrapper around + * g-table.ads/g-table.adb. + * namet.h, scos.h, uintp.h: These files are reaching into the + private data of some instances of g-table, whose names changed, + so the above change requires some adjustment here. It now uses + public interfaces. + +2017-04-27 Bob Duff + + * namet.adb, namet.ads: Minor: remove unused procedures. + +2017-04-27 Eric Botcazou + + * checks.adb (Apply_Scalar_Range_Check): Initialize Ok variable too. + (Minimize_Eliminate_Overflows): Initialize Llo and Lhi. + Add pragma Warnings on Rtype variable in nested block. * + * exp_ch3.adb (Build_Init_Statements): Initialize VAR_LOC. + * exp_ch4.adb (Expand_Concatenate): Initialize 3 variables. + (Size_In_Storage_Elements): Add pragma Warnings on Res variable. + * exp_ch7.adb (Build_Adjust_Statements): Initialize Bod_Stmts. + (Process_Component_List_For_Finalize): Initialize Counter_Id. + (Build_Finalize_Statements): Initialize Bod_Stmts. + * exp_disp.adb (Expand_Dispatching_Call): Initialize SCIL_Node. + +2017-04-27 Claire Dross + + * a-cfhama.adb, a-cfhamai.ads (=): Generic parameter removed to + allow the use of regular equality over elements in contracts. + (Formal_Model): Ghost package containing model functions that are + used in subprogram contracts. + (Current_To_Last): Removed, model + functions should be used instead. + (First_To_Previous): Removed, model functions should be used instead. + (Strict_Equal): Removed, model functions should be used instead. + (No_Overlap): Removed, model functions should be used instead. + (Equivalent_Keys): Functions over cursors are removed. They were + awkward with explicit container parameters. + * a-cofuma.adb, a-cofuma.ads (Lift_Equivalent_Keys): New lemma + (proof only) procedure to help GNATprove when equivalence over + keys is not equality. + 2017-04-27 Hristian Kirtchev * exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb, diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb index 7fd9b7f7bb4..c292701093e 100644 --- a/gcc/ada/a-cfhama.adb +++ b/gcc/ada/a-cfhama.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -237,35 +237,6 @@ is return Target; end Copy; - --------------------- - -- Current_To_Last -- - --------------------- - - function Current_To_Last (Container : Map; Current : Cursor) return Map is - Curs : Cursor := First (Container); - C : Map (Container.Capacity, Container.Modulus) := - Copy (Container, Container.Capacity); - Node : Count_Type; - - begin - if Curs = No_Element then - Clear (C); - return C; - - elsif Current /= No_Element and not Has_Element (Container, Current) then - raise Constraint_Error; - - else - while Curs.Node /= Current.Node loop - Node := Curs.Node; - Delete (C, Curs); - Curs := Next (Container, (Node => Node)); - end loop; - - return C; - end if; - end Current_To_Last; - --------------------- -- Default_Modulus -- --------------------- @@ -304,6 +275,7 @@ is HT_Ops.Delete_Node_Sans_Free (Container, Position.Node); Free (Container, Position.Node); + Position := No_Element; end Delete; ------------- @@ -346,79 +318,6 @@ is return Equivalent_Keys (Key, Node.Key); end Equivalent_Keys; - function Equivalent_Keys - (Left : Map; - CLeft : Cursor; - Right : Map; - CRight : Cursor) return Boolean - is - begin - if not Has_Element (Left, CLeft) then - raise Constraint_Error with - "Left cursor of Equivalent_Keys has no element"; - end if; - - if not Has_Element (Right, CRight) then - raise Constraint_Error with - "Right cursor of Equivalent_Keys has no element"; - end if; - - pragma Assert (Vet (Left, CLeft), - "Left cursor of Equivalent_Keys is bad"); - pragma Assert (Vet (Right, CRight), - "Right cursor of Equivalent_Keys is bad"); - - declare - LN : Node_Type renames Left.Nodes (CLeft.Node); - RN : Node_Type renames Right.Nodes (CRight.Node); - begin - return Equivalent_Keys (LN.Key, RN.Key); - end; - end Equivalent_Keys; - - function Equivalent_Keys - (Left : Map; - CLeft : Cursor; - Right : Key_Type) return Boolean - is - begin - if not Has_Element (Left, CLeft) then - raise Constraint_Error with - "Left cursor of Equivalent_Keys has no element"; - end if; - - pragma Assert (Vet (Left, CLeft), - "Left cursor in Equivalent_Keys is bad"); - - declare - LN : Node_Type renames Left.Nodes (CLeft.Node); - begin - return Equivalent_Keys (LN.Key, Right); - end; - end Equivalent_Keys; - - function Equivalent_Keys - (Left : Key_Type; - Right : Map; - CRight : Cursor) return Boolean - is - begin - if Has_Element (Right, CRight) then - raise Constraint_Error with - "Right cursor of Equivalent_Keys has no element"; - end if; - - pragma Assert (Vet (Right, CRight), - "Right cursor of Equivalent_Keys is bad"); - - declare - RN : Node_Type renames Right.Nodes (CRight.Node); - - begin - return Equivalent_Keys (Left, RN.Key); - end; - end Equivalent_Keys; - ------------- -- Exclude -- ------------- @@ -460,37 +359,109 @@ is return (Node => Node); end First; - ----------------------- - -- First_To_Previous -- - ----------------------- + ------------------ + -- Formal_Model -- + ------------------ - function First_To_Previous - (Container : Map; - Current : Cursor) return Map is - Curs : Cursor; - C : Map (Container.Capacity, Container.Modulus) := - Copy (Container, Container.Capacity); - Node : Count_Type; + package body Formal_Model is - begin - Curs := Current; + ---------- + -- Keys -- + ---------- - if Curs = No_Element then - return C; + function Keys (Container : Map) return K.Sequence is + Position : Count_Type := HT_Ops.First (Container); + R : K.Sequence; - elsif not Has_Element (Container, Curs) then - raise Constraint_Error; + begin + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. - else - while Curs.Node /= 0 loop - Node := Curs.Node; - Delete (C, Curs); - Curs := Next (Container, (Node => Node)); + while Position /= 0 loop + R := K.Add (R, Container.Nodes (Position).Key); + Position := HT_Ops.Next (Container, Position); end loop; - return C; - end if; - end First_To_Previous; + return R; + end Keys; + + ---------------------------- + -- Lift_Abstraction_Level -- + ---------------------------- + + procedure Lift_Abstraction_Level (Container : Map) is null; + + ----------------------- + -- Mapping_preserved -- + ----------------------- + + function Mapping_Preserved + (K_Left : K.Sequence; + K_Right : K.Sequence; + P_Left : P.Map; + P_Right : P.Map) return Boolean + is + begin + for C of P_Left loop + if not P.Has_Key (P_Right, C) + or else P.Get (P_Left, C) > K.Length (K_Left) + or else P.Get (P_Right, C) > K.Length (K_Right) + or else K.Get (K_Left, P.Get (P_Left, C)) /= + K.Get (K_Right, P.Get (P_Right, C)) + then + return False; + end if; + end loop; + + return True; + end Mapping_Preserved; + + ----------- + -- Model -- + ----------- + + function Model (Container : Map) return M.Map is + Position : Count_Type := HT_Ops.First (Container); + R : M.Map; + + begin + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + + while Position /= 0 loop + R := M.Add (Container => R, + New_Key => Container.Nodes (Position).Key, + New_Item => Container.Nodes (Position).Element); + Position := HT_Ops.Next (Container, Position); + end loop; + + return R; + end Model; + + --------------- + -- Positions -- + --------------- + + function Positions (Container : Map) return P.Map is + I : Count_Type := 1; + Position : Count_Type := HT_Ops.First (Container); + R : P.Map; + + begin + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + + while Position /= 0 loop + R := P.Add (R, (Node => Position), I); + pragma Assert (P.Length (R) = I); + Position := HT_Ops.Next (Container, Position); + I := I + 1; + end loop; + + return R; + end Positions; + + end Formal_Model; ---------- -- Free -- @@ -747,40 +718,6 @@ is Position := Next (Container, Position); end Next; - ------------- - -- Overlap -- - ------------- - - function Overlap (Left, Right : Map) return Boolean is - Left_Node : Count_Type; - Left_Nodes : Nodes_Type renames Left.Nodes; - - begin - if Length (Right) = 0 or Length (Left) = 0 then - return False; - end if; - - if Left'Address = Right'Address then - return True; - end if; - - Left_Node := First (Left).Node; - while Left_Node /= 0 loop - declare - N : Node_Type renames Left_Nodes (Left_Node); - E : Key_Type renames N.Key; - begin - if Find (Right, E).Node /= 0 then - return True; - end if; - end; - - Left_Node := HT_Ops.Next (Left, Left_Node); - end loop; - - return False; - end Overlap; - ------------- -- Replace -- ------------- @@ -850,35 +787,6 @@ is Node.Next := Next; end Set_Next; - ------------------ - -- Strict_Equal -- - ------------------ - - function Strict_Equal (Left, Right : Map) return Boolean is - CuL : Cursor := First (Left); - CuR : Cursor := First (Right); - - begin - if Length (Left) /= Length (Right) then - return False; - end if; - - while CuL.Node /= 0 or else CuR.Node /= 0 loop - if CuL.Node /= CuR.Node - or else - Left.Nodes (CuL.Node).Element /= Right.Nodes (CuR.Node).Element - or else Left.Nodes (CuL.Node).Key /= Right.Nodes (CuR.Node).Key - then - return False; - end if; - - CuL := Next (Left, CuL); - CuR := Next (Right, CuR); - end loop; - - return True; - end Strict_Equal; - --------- -- Vet -- --------- diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads index 8d6e96a3c58..bc10de02574 100644 --- a/gcc/ada/a-cfhama.ads +++ b/gcc/ada/a-cfhama.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2017, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -44,17 +44,11 @@ -- and its previous version C'Old) for expressing properties, which is not -- possible if cursors encapsulate an access to the underlying container. --- There are four new functions: - --- function Strict_Equal (Left, Right : Map) return Boolean; --- function Overlap (Left, Right : Map) return Boolean; --- function First_To_Previous (Container : Map; Current : Cursor) --- return Map; --- function Current_To_Last (Container : Map; Current : Cursor) --- return Map; - --- See detailed specifications for these subprograms +-- Iteration over maps is done using the Iterable aspect which is SPARK +-- compatible. For of iteration ranges over keys instead of elements. +with Ada.Containers.Functional_Vectors; +with Ada.Containers.Functional_Maps; private with Ada.Containers.Hash_Tables; generic @@ -63,77 +57,267 @@ generic with function Hash (Key : Key_Type) return Hash_Type; with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; - with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Hashed_Maps with - Pure, SPARK_Mode is - pragma Annotate (GNATprove, External_Axiomatization); pragma Annotate (CodePeer, Skip_Analysis); type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, Next => Next, Has_Element => Has_Element, - Element => Element), - Default_Initial_Condition => Is_Empty (Map); + Element => Key), + Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0; pragma Preelaborable_Initialization (Map); - type Cursor is private; - pragma Preelaborable_Initialization (Cursor); - Empty_Map : constant Map; - No_Element : constant Cursor; + type Cursor is record + Node : Count_Type; + end record; + + No_Element : constant Cursor := (Node => 0); + + function Length (Container : Map) return Count_Type with + Global => null, + Post => Length'Result <= Container.Capacity; + + pragma Unevaluated_Use_Of_Old (Allow); + + package Formal_Model with Ghost is + subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; + + package M is new Ada.Containers.Functional_Maps + (Element_Type => Element_Type, + Key_Type => Key_Type, + Equivalent_Keys => Equivalent_Keys); + + function "=" + (Left : M.Map; + Right : M.Map) return Boolean renames M."="; + + function "<=" + (Left : M.Map; + Right : M.Map) return Boolean renames M."<="; + + package K is new Ada.Containers.Functional_Vectors + (Element_Type => Key_Type, + Index_Type => Positive_Count_Type); + + function "=" + (Left : K.Sequence; + Right : K.Sequence) return Boolean renames K."="; + + function "<" + (Left : K.Sequence; + Right : K.Sequence) return Boolean renames K."<"; + + function "<=" + (Left : K.Sequence; + Right : K.Sequence) return Boolean renames K."<="; + + package P is new Ada.Containers.Functional_Maps + (Key_Type => Cursor, + Element_Type => Positive_Count_Type, + Equivalent_Keys => "="); + + function "=" + (Left : P.Map; + Right : P.Map) return Boolean renames P."="; + + function "<=" + (Left : P.Map; + Right : P.Map) return Boolean renames P."<="; + + function Mapping_Preserved + (K_Left : K.Sequence; + K_Right : K.Sequence; + P_Left : P.Map; + P_Right : P.Map) return Boolean + with + Ghost, + Global => null, + Post => + (if Mapping_Preserved'Result then + + -- Right contains all the cursors of Left + + P.Keys_Included (P_Left, P_Right) + + -- Mappings from cursors to elements induced by K_Left, P_Left + -- and K_Right, P_Right are the same. + + and (for all C of P_Left => + K.Get (K_Left, P.Get (P_Left, C)) = + K.Get (K_Right, P.Get (P_Right, C)))); + + function Model (Container : Map) return M.Map with + -- The highlevel model of a map is a map from keys to elements. Neither + -- cursors nor order of elements are represented in this model. Keys are + -- modeled up to equivalence. + + Ghost, + Global => null; + + function Keys (Container : Map) return K.Sequence with + -- The Keys sequence represents the underlying list structure of maps + -- that is used for iteration. It stores the actual values of keys in + -- the map. It does not model cursors nor elements. + + Ghost, + Global => null, + Post => + K.Length (Keys'Result) = Length (Container) + + -- It only contains keys contained in Model + + and (for all Key of Keys'Result => + M.Has_Key (Model (Container), Key)) + + -- It contains all the keys contained in Model + + and + (for all Key of Model (Container) => + (for some L of Keys'Result => Equivalent_Keys (L, Key))) + + -- It has no duplicate + + and + (for all I in 1 .. Length (Container) => + (for all J in 1 .. Length (Container) => + (if Equivalent_Keys + (K.Get (Keys'Result, I), K.Get (Keys'Result, J)) + then I = J))); + pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys); + + function Positions (Container : Map) return P.Map with + -- The Positions map is used to model cursors. It only contains valid + -- cursors and map them to their position in the container. + + Ghost, + Global => null, + Post => + not P.Has_Key (Positions'Result, No_Element) + + -- Positions of cursors are smaller than the container's length. + + and then + (for all I of Positions'Result => + P.Get (Positions'Result, I) in 1 .. Length (Container) + + -- No two cursors have the same position. Note that we do not + -- state that there is a cursor in the map for each position, as + -- it is rarely needed. + + and then + (for all J of Positions'Result => + (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) + then I = J))); + + procedure Lift_Abstraction_Level (Container : Map) with + -- Lift_Abstraction_Level is a ghost procedure that does nothing but + -- assume that we can access to the same elements by iterating over + -- positions or cursors. + -- This information is not generally useful except when switching from + -- a lowlevel, cursor aware view of a container, to a highlevel + -- position based view. + + Ghost, + Global => null, + Post => + (for all Key of Keys (Container) => + (for some I of Positions (Container) => + K.Get (Keys (Container), P.Get (Positions (Container), I)) = + Key)); + + function Contains + (C : M.Map; + K : Key_Type) return Boolean renames M.Has_Key; + -- To improve readability of contracts, we rename the function used to + -- search for a key in the model to Contains. + + function Element + (C : M.Map; + K : Key_Type) return Element_Type renames M.Get; + -- To improve readability of contracts, we rename the function used to + -- access an element in the model to Element. + end Formal_Model; + use Formal_Model; function "=" (Left, Right : Map) return Boolean with - Global => null; + Global => null, + Post => "="'Result = (Model (Left) = Model (Right)); function Capacity (Container : Map) return Count_Type with - Global => null; + Global => null, + Post => Capacity'Result = Container.Capacity; procedure Reserve_Capacity (Container : in out Map; Capacity : Count_Type) with Global => null, - Pre => Capacity <= Container.Capacity; - - function Length (Container : Map) return Count_Type with - Global => null; + Pre => Capacity <= Container.Capacity, + Post => Model (Container) = Model (Container)'Old; function Is_Empty (Container : Map) return Boolean with - Global => null; + Global => null, + Post => Is_Empty'Result = M.Is_Empty (Model (Container)); procedure Clear (Container : in out Map) with - Global => null; + Global => null, + Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); procedure Assign (Target : in out Map; Source : Map) with Global => null, - Pre => Target.Capacity >= Length (Source); + Pre => Target.Capacity >= Length (Source), + Post => + Model (Target) = Model (Source) + and Length (Source) = Length (Target) + + -- Actual keys are preserved + + and + (for all Key of Keys (Source) => + Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key); function Copy (Source : Map; Capacity : Count_Type := 0) return Map with Global => null, - Pre => Capacity = 0 or else Capacity >= Source.Capacity; + Pre => Capacity = 0 or else Capacity >= Source.Capacity, + Post => + Model (Copy'Result) = Model (Source) + and Keys (Copy'Result) = Keys (Source) + and Positions (Copy'Result) = Positions (Source) + and (if Capacity = 0 then + Copy'Result.Capacity = Source.Capacity + else + Copy'Result.Capacity = Capacity); -- Copy returns a container stricty equal to Source. It must have -- the same cursors associated with each element. Therefore: - -- - capacity=0 means use container.capacity as capacity of target + -- - capacity=0 means use Source.Capacity as capacity of target -- - the modulus cannot be changed. function Key (Container : Map; Position : Cursor) return Key_Type with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + Key'Result = + K.Get (Keys (Container), P.Get (Positions (Container), Position)); + pragma Annotate (GNATprove, Inline_For_Proof, Key); function Element (Container : Map; Position : Cursor) return Element_Type with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + Element'Result = Element (Model (Container), Key (Container, Position)); + pragma Annotate (GNATprove, Inline_For_Proof, Element); procedure Replace_Element (Container : in out Map; @@ -141,11 +325,40 @@ is New_Item : Element_Type) with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + + -- Order of keys and cursors are preserved + + Keys (Container) = Keys (Container)'Old + and Positions (Container) = Positions (Container)'Old + + -- New_Item is now associated to the key at position Position in + -- Container. + + and Element (Container, Position) = New_Item + + -- Elements associated to other keys are preserved + + and M.Same_Keys (Model (Container), Model (Container)'Old) + and M.Elements_Equal_Except + (Model (Container), + Model (Container)'Old, + Key (Container, Position)); procedure Move (Target : in out Map; Source : in out Map) with Global => null, - Pre => Target.Capacity >= Length (Source); + Pre => Target.Capacity >= Length (Source), + Post => + Model (Target) = Model (Source)'Old + and Length (Source)'Old = Length (Target) + and Length (Source) = 0 + + -- Actual keys are preserved + + and + (for all Key of Keys (Source)'Old => + Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key); procedure Insert (Container : in out Map; @@ -154,8 +367,55 @@ is Position : out Cursor; Inserted : out Boolean) with - Global => null, - Pre => Length (Container) < Container.Capacity; + Global => null, + Pre => + Length (Container) < Container.Capacity or Contains (Container, Key), + Post => + Contains (Container, Key) + and Has_Element (Container, Position) + and Equivalent_Keys + (Formal_Hashed_Maps.Key (Container, Position), Key), + Contract_Cases => + + -- If Key is already in Container, it is not modified and Inserted is + -- set to False. + + (Contains (Container, Key) => + not Inserted + and Model (Container) = Model (Container)'Old + and Keys (Container) = Keys (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, Key is inserted in Container and Inserted is set to True + + others => + Inserted + and Length (Container) = Length (Container)'Old + 1 + + -- Key now maps to New_Item + + and Formal_Hashed_Maps.Key (Container, Position) = Key + and Element (Model (Container), Key) = New_Item + + -- Other keys are preserved + + and Model (Container)'Old <= Model (Container) + and M.Keys_Included_Except + (Model (Container), + Model (Container)'Old, + Key) + + -- Mapping from cursors to keys are preserved + + and Mapping_Preserved + (K_Left => Keys (Container)'Old, + K_Right => Keys (Container), + P_Left => Positions (Container)'Old, + P_Right => Positions (Container)) + and P.Keys_Included_Except + (Positions (Container), + Positions (Container)'Old, + Position)); procedure Insert (Container : in out Map; @@ -163,16 +423,100 @@ is New_Item : Element_Type) with Global => null, - Pre => Length (Container) < Container.Capacity - and then (not Contains (Container, Key)); + Pre => + Length (Container) < Container.Capacity + and then (not Contains (Container, Key)), + Post => + Length (Container) = Length (Container)'Old + 1 + and Contains (Container, Key) + + -- Key now maps to New_Item + + and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key + and Element (Model (Container), Key) = New_Item + + -- Other keys are preserved + + and Model (Container)'Old <= Model (Container) + and M.Keys_Included_Except + (Model (Container), + Model (Container)'Old, + Key) + + -- Mapping from cursors to keys are preserved + + and Mapping_Preserved + (K_Left => Keys (Container)'Old, + K_Right => Keys (Container), + P_Left => Positions (Container)'Old, + P_Right => Positions (Container)) + and P.Keys_Included_Except + (Positions (Container), + Positions (Container)'Old, + Find (Container, Key)); procedure Include (Container : in out Map; Key : Key_Type; New_Item : Element_Type) with - Global => null, - Pre => Length (Container) < Container.Capacity; + Global => null, + Pre => + Length (Container) < Container.Capacity or Contains (Container, Key), + Post => + Contains (Container, Key) and Element (Container, Key) = New_Item, + Contract_Cases => + + -- If Key is already in Container, Key is mapped to New_Item + + (Contains (Container, Key) => + + -- Cursors are preserved + + Positions (Container) = Positions (Container)'Old + + -- The key equivalent to Key in Container is replaced by Key + + and K.Get (Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) = + Key + and K.Equal_Except + (Keys (Container)'Old, + Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) + + -- Elements associated to other keys are preserved + + and M.Same_Keys (Model (Container), Model (Container)'Old) + and M.Elements_Equal_Except + (Model (Container), + Model (Container)'Old, + Key), + + -- Otherwise, Key is inserted in Container + + others => + Length (Container) = Length (Container)'Old + 1 + + -- Other keys are preserved + + and Model (Container)'Old <= Model (Container) + and M.Keys_Included_Except + (Model (Container), + Model (Container)'Old, + Key) + + -- Mapping from cursors to keys are preserved + + and Mapping_Preserved + (K_Left => Keys (Container)'Old, + K_Right => Keys (Container), + P_Left => Positions (Container)'Old, + P_Right => Positions (Container)) + and P.Keys_Included_Except + (Positions (Container), + Positions (Container)'Old, + Find (Container, Key))); procedure Replace (Container : in out Map; @@ -180,98 +524,212 @@ is New_Item : Element_Type) with Global => null, - Pre => Contains (Container, Key); + Pre => Contains (Container, Key), + Post => + + -- Cursors are preserved + + Positions (Container) = Positions (Container)'Old + + -- The key equivalent to Key in Container is replaced by Key + + and K.Get (Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) = Key + and K.Equal_Except + (Keys (Container)'Old, + Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) + + -- New_Item is now associated to the Key in Container + + and Element (Model (Container), Key) = New_Item + + -- Elements associated to other keys are preserved + + and M.Same_Keys (Model (Container), Model (Container)'Old) + and M.Elements_Equal_Except + (Model (Container), + Model (Container)'Old, + Key); procedure Exclude (Container : in out Map; Key : Key_Type) with - Global => null; + Global => null, + Post => not Contains (Container, Key), + Contract_Cases => + + -- If Key is not in Container, nothing is changed + + (not Contains (Container, Key) => + Model (Container) = Model (Container)'Old + and Keys (Container) = Keys (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, Key is removed from Container + + others => + Length (Container) = Length (Container)'Old - 1 + + -- Other keys are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + + -- Mapping from cursors to keys are preserved + + and Mapping_Preserved + (K_Left => Keys (Container), + K_Right => Keys (Container)'Old, + P_Left => Positions (Container), + P_Right => Positions (Container)'Old) + and P.Keys_Included_Except + (Positions (Container)'Old, + Positions (Container), + Find (Container, Key)'Old)); procedure Delete (Container : in out Map; Key : Key_Type) with Global => null, - Pre => Contains (Container, Key); + Pre => Contains (Container, Key), + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Key is no longer in Container + + and not Contains (Container, Key) + + -- Other keys are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + + -- Mapping from cursors to keys are preserved + + and Mapping_Preserved + (K_Left => Keys (Container), + K_Right => Keys (Container)'Old, + P_Left => Positions (Container), + P_Right => Positions (Container)'Old) + and P.Keys_Included_Except + (Positions (Container)'Old, + Positions (Container), + Find (Container, Key)'Old); procedure Delete (Container : in out Map; Position : in out Cursor) with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + Position = No_Element + and Length (Container) = Length (Container)'Old - 1 + + -- The key at position Position is no longer in Container + + and not Contains (Container, Key (Container, Position)'Old) + and not P.Has_Key (Positions (Container), Position'Old) + + -- Other keys are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Key (Container, Position)'Old) + + -- Mapping from cursors to keys are preserved + + and Mapping_Preserved + (K_Left => Keys (Container), + K_Right => Keys (Container)'Old, + P_Left => Positions (Container), + P_Right => Positions (Container)'Old) + and P.Keys_Included_Except + (Positions (Container)'Old, + Positions (Container), + Position'Old); function First (Container : Map) return Cursor with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 => + First'Result = No_Element, + + others => + Has_Element (Container, First'Result) + and P.Get (Positions (Container), First'Result) = 1); function Next (Container : Map; Position : Cursor) return Cursor with - Global => null, - Pre => Has_Element (Container, Position) or else Position = No_Element; + Global => null, + Pre => + Has_Element (Container, Position) or else Position = No_Element, + Contract_Cases => + (Position = No_Element + or else P.Get (Positions (Container), Position) = Length (Container) + => + Next'Result = No_Element, + + others => + Has_Element (Container, Next'Result) + and then P.Get (Positions (Container), Next'Result) = + P.Get (Positions (Container), Position) + 1); procedure Next (Container : Map; Position : in out Cursor) with - Global => null, - Pre => Has_Element (Container, Position) or else Position = No_Element; + Global => null, + Pre => + Has_Element (Container, Position) or else Position = No_Element, + Contract_Cases => + (Position = No_Element + or else P.Get (Positions (Container), Position) = Length (Container) + => + Position = No_Element, + + others => + Has_Element (Container, Position) + and then P.Get (Positions (Container), Position) = + P.Get (Positions (Container), Position'Old) + 1); function Find (Container : Map; Key : Key_Type) return Cursor with - Global => null; + Global => null, + Contract_Cases => - function Contains (Container : Map; Key : Key_Type) return Boolean with - Global => null; + -- If Key is not is not contained in Container, Find returns No_Element - function Element (Container : Map; Key : Key_Type) return Element_Type with - Global => null, - Pre => Contains (Container, Key); + (not Contains (Model (Container), Key) => + Find'Result = No_Element, - function Has_Element (Container : Map; Position : Cursor) return Boolean - with - Global => null; + -- Otherwise, Find returns a valid cusror in Container - function Equivalent_Keys - (Left : Map; - CLeft : Cursor; - Right : Map; - CRight : Cursor) return Boolean - with - Global => null; + others => + P.Has_Key (Positions (Container), Find'Result) - function Equivalent_Keys - (Left : Map; - CLeft : Cursor; - Right : Key_Type) return Boolean - with - Global => null; + -- The key designated by the result of Find is Key - function Equivalent_Keys - (Left : Key_Type; - Right : Map; - CRight : Cursor) return Boolean - with - Global => null; - - function Default_Modulus (Capacity : Count_Type) return Hash_Type with - Global => null; + and Equivalent_Keys + (Formal_Hashed_Maps.Key (Container, Find'Result), Key)); - function Strict_Equal (Left, Right : Map) return Boolean with - Ghost, - Global => null; - -- Strict_Equal returns True if the containers are physically equal, i.e. - -- they are structurally equal (function "=" returns True) and that they - -- have the same set of cursors. + function Contains (Container : Map; Key : Key_Type) return Boolean with + Global => null, + Post => Contains'Result = Contains (Model (Container), Key); + pragma Annotate (GNATprove, Inline_For_Proof, Contains); - function First_To_Previous (Container : Map; Current : Cursor) return Map - with - Ghost, + function Element (Container : Map; Key : Key_Type) return Element_Type with Global => null, - Pre => Has_Element (Container, Current) or else Current = No_Element; + Pre => Contains (Container, Key), + Post => Element'Result = Element (Model (Container), Key); + pragma Annotate (GNATprove, Inline_For_Proof, Element); - function Current_To_Last (Container : Map; Current : Cursor) return Map + function Has_Element (Container : Map; Position : Cursor) return Boolean with - Ghost, Global => null, - Pre => Has_Element (Container, Current) or else Current = No_Element; - -- First_To_Previous returns a container containing all elements preceding - -- Current (excluded) in Container. Current_To_Last returns a container - -- containing all elements following Current (included) in Container. - -- These two new functions can be used to express invariant properties in - -- loops which iterate over containers. First_To_Previous returns the part - -- of the container already scanned and Current_To_Last the part not - -- scanned yet. - - function Overlap (Left, Right : Map) return Boolean with + Post => + Has_Element'Result = P.Has_Key (Positions (Container), Position); + pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); + + function Default_Modulus (Capacity : Count_Type) return Hash_Type with Global => null; - -- Overlap returns True if the containers have common keys private pragma SPARK_Mode (Off); @@ -302,12 +760,6 @@ private use HT_Types; - type Cursor is record - Node : Count_Type; - end record; - Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>); - No_Element : constant Cursor := (Node => 0); - end Ada.Containers.Formal_Hashed_Maps; diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb index e4ee1988a5a..38e481be571 100644 --- a/gcc/ada/a-cofuma.adb +++ b/gcc/ada/a-cofuma.adb @@ -93,8 +93,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is K : constant Key_Type := Get (Left.Keys, I); begin if not Equivalent_Keys (K, New_Key) - and then Get (Right.Elements, Find (Right.Keys, K)) /= - Get (Left.Elements, I) + and then + (Find (Right.Keys, K) = 0 + or else Get (Right.Elements, Find (Right.Keys, K)) /= + Get (Left.Elements, I)) then return False; end if; @@ -116,8 +118,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is begin if not Equivalent_Keys (K, X) and then not Equivalent_Keys (K, Y) - and then Get (Right.Elements, Find (Right.Keys, K)) /= - Get (Left.Elements, I) + and then + (Find (Right.Keys, K) = 0 + or else Get (Right.Elements, Find (Right.Keys, K)) /= + Get (Left.Elements, I)) then return False; end if; @@ -229,6 +233,16 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is return Length (Container.Elements); end Length; + -------------------------- + -- Lift_Equivalent_Keys -- + -------------------------- + + procedure Lift_Equivalent_Keys + (Container : Map; + Left : Key_Type; + Right : Key_Type) + is null; + --------------- -- Same_Keys -- --------------- diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index 9d3bb9786bc..1172d118952 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -48,6 +48,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is -- Maps are empty when default initialized. -- "For in" quantification over maps should not be used. -- "For of" quantification over maps iterates over keys. + -- Note that, for proof, for of quantification is understood modulo + -- equivalence (quantification includes keys equivalent to keys of the + -- map). ----------------------- -- Basic operations -- @@ -71,6 +74,22 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Global => null; -- Return the number of mappings in Container + procedure Lift_Equivalent_Keys + (Container : Map; + Left : Key_Type; + Right : Key_Type) + -- Lemma function which can be called manually to allow GNATprove to deduce + -- that Has_Key and Get always return the same result on equivalent keys. + + with + Ghost, + Global => null, + Pre => Equivalent_Keys (Left, Right), + Post => + Has_Key (Container, Left) = Has_Key (Container, Right) + and (if Has_Key (Container, Left) then + Get (Container, Left) = Get (Container, Right)); + ------------------------ -- Property Functions -- ------------------------ @@ -162,12 +181,12 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is with Global => null, - Pre => Keys_Included_Except (Left, Right, New_Key), Post => Elements_Equal_Except'Result = (for all Key of Left => (if not Equivalent_Keys (Key, New_Key) then - Get (Left, Key) = Get (Right, Key))); + Has_Key (Right, Key) + and then Get (Left, Key) = Get (Right, Key))); function Elements_Equal_Except (Left : Map; @@ -179,14 +198,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is with Global => null, - Pre => Keys_Included_Except (Left, Right, X, Y), Post => Elements_Equal_Except'Result = (for all Key of Left => (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y) then - Get (Left, Key) = Get (Right, Key))); + Has_Key (Right, Key) + and then Get (Left, Key) = Get (Right, Key))); ---------------------------- -- Construction Functions -- diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 2833fff87a1..8ed4893e7f9 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -2738,7 +2738,7 @@ package body Checks is S_Typ : Entity_Id; Arr : Node_Id := Empty; -- initialize to prevent warning Arr_Typ : Entity_Id := Empty; -- initialize to prevent warning - OK : Boolean; + OK : Boolean := False; -- initialize to prevent warning Is_Subscr_Ref : Boolean; -- Set true if Expr is a subscript @@ -7936,7 +7936,8 @@ package body Checks is Rlo, Rhi : Uint; -- Ranges of values for right operand (operator case) - Llo, Lhi : Uint; + Llo : Uint := No_Uint; -- initialize to prevent warning + Lhi : Uint := No_Uint; -- initialize to prevent warning -- Ranges of values for left operand (operator case) LLIB : constant Entity_Id := Base_Type (Standard_Long_Long_Integer); @@ -8238,6 +8239,7 @@ package body Checks is else declare Rtype : Entity_Id; + pragma Warnings (Off, Rtype); New_Alts : List_Id; New_Exp : Node_Id; diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 094f70e0eab..8520de4e6b7 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -3174,7 +3174,7 @@ package body Exp_Ch3 is if Present (Variant_Part (Comp_List)) then declare Variant_Alts : constant List_Id := New_List; - Var_Loc : Source_Ptr; + Var_Loc : Source_Ptr := No_Location; Variant : Node_Id; begin diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index e247c8b6f8a..21d2621b53e 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -2700,7 +2700,7 @@ package body Exp_Ch4 is -- last operand is always retained, in case it provides the bounds for -- a null result. - Opnd : Node_Id; + Opnd : Node_Id := Empty; -- Current operand being processed in the loop through operands. After -- this loop is complete, always contains the last operand (which is not -- the same as Operands (NN), since null operands are skipped). @@ -2742,13 +2742,13 @@ package body Exp_Ch4 is -- This is either an integer literal node, or an identifier reference to -- a constant entity initialized to the appropriate value. - Last_Opnd_Low_Bound : Node_Id; + Last_Opnd_Low_Bound : Node_Id := Empty; -- A tree node representing the low bound of the last operand. This -- need only be set if the result could be null. It is used for the -- special case of setting the right low bound for a null result. -- This is of type Ityp. - Last_Opnd_High_Bound : Node_Id; + Last_Opnd_High_Bound : Node_Id := Empty; -- A tree node representing the high bound of the last operand. This -- need only be set if the result could be null. It is used for the -- special case of setting the right high bound for a null result. @@ -4036,6 +4036,7 @@ package body Exp_Ch4 is declare Len : Node_Id; Res : Node_Id; + pragma Warnings (Off, Res); begin for J in 1 .. Number_Dimensions (E) loop diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 8f52966249a..0a9bc0ed828 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -6722,7 +6722,7 @@ package body Exp_Ch7 is -- Local variables - Bod_Stmts : List_Id; + Bod_Stmts : List_Id := No_List; Finalizer_Decls : List_Id := No_List; Rec_Def : Node_Id; @@ -7068,7 +7068,7 @@ package body Exp_Ch7 is -- Local variables Alts : List_Id; - Counter_Id : Entity_Id; + Counter_Id : Entity_Id := Empty; Decl : Node_Id; Decl_Id : Entity_Id; Decl_Typ : Entity_Id; @@ -7305,7 +7305,7 @@ package body Exp_Ch7 is -- Local variables - Bod_Stmts : List_Id; + Bod_Stmts : List_Id := No_List; Finalizer_Decls : List_Id := No_List; Rec_Def : Node_Id; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 4bdd525d90c..0a6a03b7fd5 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -673,7 +673,7 @@ package body Exp_Disp is -- Local variables New_Node : Node_Id; - SCIL_Node : Node_Id; + SCIL_Node : Node_Id := Empty; SCIL_Related_Node : Node_Id := Call_Node; -- Start of processing for Expand_Dispatching_Call diff --git a/gcc/ada/g-dyntab.adb b/gcc/ada/g-dyntab.adb index 8210419844c..384d5137817 100644 --- a/gcc/ada/g-dyntab.adb +++ b/gcc/ada/g-dyntab.adb @@ -34,6 +34,7 @@ pragma Compiler_Unit_Warning; with GNAT.Heap_Sort_G; with Ada.Unchecked_Deallocation; +with System; package body GNAT.Dynamic_Tables is @@ -44,7 +45,7 @@ package body GNAT.Dynamic_Tables is -- Local Subprograms -- ----------------------- - procedure Grow (T : in out Instance; New_Last : Table_Count_Type); + procedure Grow (T : in out Instance; New_Last : Table_Last_Type); -- This is called when we are about to set the value of Last to a value -- that is larger than Last_Allocated. This reallocates the table to the -- larger size, as indicated by New_Last. At the time this is called, @@ -128,14 +129,12 @@ package body GNAT.Dynamic_Tables is begin if T.Table = Empty then - pragma Assert (T.P.Last_Allocated = First - 1); - pragma Assert (T.P.Last = First - 1); + pragma Assert (T.P = (Last_Allocated | Last => First - 1)); null; else Free (Temp); T.Table := Empty; - T.P.Last_Allocated := First - 1; - T.P.Last := First - 1; + T.P := (Last_Allocated | Last => First - 1); end if; end Free; @@ -143,7 +142,7 @@ package body GNAT.Dynamic_Tables is -- Grow -- ---------- - procedure Grow (T : in out Instance; New_Last : Table_Count_Type) is + procedure Grow (T : in out Instance; New_Last : Table_Last_Type) is -- Note: Type Alloc_Ptr below needs to be declared locally so we know -- the bounds. That means that the collection is local, so is finalized @@ -158,7 +157,7 @@ package body GNAT.Dynamic_Tables is subtype Table_Length_Type is Table_Index_Type'Base range 0 .. Table_Index_Type'Base'Last; - Old_Last_Allocated : constant Table_Count_Type := T.P.Last_Allocated; + Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated; Old_Allocated_Length : constant Table_Length_Type := Old_Last_Allocated - First + 1; @@ -241,24 +240,82 @@ package body GNAT.Dynamic_Tables is Free (T); end Init; + -------------- + -- Is_Empty -- + -------------- + + function Is_Empty (T : Instance) return Boolean is + Result : constant Boolean := T.P.Last = Table_Low_Bound - 1; + begin + pragma Assert (Result = (T.Table = Empty)); + return Result; + end Is_Empty; + ---------- -- Last -- ---------- - function Last (T : Instance) return Table_Count_Type is + function Last (T : Instance) return Table_Last_Type is begin return T.P.Last; end Last; + ---------- + -- Move -- + ---------- + + procedure Move (From, To : in out Instance) is + begin + pragma Assert (Is_Empty (To)); + To := From; + + From.Table := Empty; + From.Locked := False; + From.P.Last_Allocated := Table_Low_Bound - 1; + From.P.Last := Table_Low_Bound - 1; + pragma Assert (Is_Empty (From)); + end Move; + ------------- -- Release -- ------------- procedure Release (T : in out Instance) is - pragma Assert (not T.Locked); - Old_Last_Allocated : constant Table_Count_Type := T.P.Last_Allocated; + Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated; + + function New_Last_Allocated return Table_Last_Type; + -- Compute the new value of Last_Allocated. This is normally equal to + -- Last, but if Release_Threshold /= 0, then we need to take that into + -- account. + + function New_Last_Allocated return Table_Last_Type is + subtype Table_Length_Type is Table_Index_Type'Base + range 0 .. Table_Index_Type'Base'Last; + Length : constant Table_Length_Type := T.P.Last - First + 1; + Comp_Size_In_Bytes : constant Table_Length_Type := + Table_Type'Component_Size / System.Storage_Unit; + Length_Threshold : constant Table_Length_Type := + Table_Length_Type (Release_Threshold) / Comp_Size_In_Bytes; + begin + if Release_Threshold = 0 + or else Length < Length_Threshold + then + return T.P.Last; + else + declare + Extra_Length : constant Table_Length_Type := Length / 1000; + begin + return (Length + Extra_Length) - 1 + First; + end; + end if; + end New_Last_Allocated; + + New_Last_Alloc : constant Table_Last_Type := New_Last_Allocated; + + -- Start of processing for Release + begin - if T.P.Last /= T.P.Last_Allocated then + if New_Last_Alloc < T.P.Last_Allocated then pragma Assert (T.P.Last < T.P.Last_Allocated); pragma Assert (T.Table /= Empty); @@ -272,23 +329,21 @@ package body GNAT.Dynamic_Tables is new Ada.Unchecked_Conversion (Table_Ptr, Old_Alloc_Ptr); subtype Alloc_Type is - Table_Type (First .. First + T.P.Last - 1); + Table_Type (First .. New_Last_Alloc); type Alloc_Ptr is access all Alloc_Type; function To_Table_Ptr is - new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr); + new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr); Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table); - New_Table : constant Alloc_Ptr := - new Alloc_Type'(Old_Table (Alloc_Type'Range)); + New_Table : constant Alloc_Ptr := new Alloc_Type; begin - T.P.Last_Allocated := T.P.Last; + New_Table (Alloc_Type'Range) := Old_Table (Alloc_Type'Range); + T.P.Last_Allocated := New_Last_Alloc; Free (Old_Table); T.Table := To_Table_Ptr (New_Table); end; end if; - - pragma Assert (T.P.Last = T.P.Last_Allocated); end Release; -------------- @@ -329,8 +384,7 @@ package body GNAT.Dynamic_Tables is -- Set_Last -- -------------- - procedure Set_Last (T : in out Instance; New_Val : Table_Count_Type) is - pragma Assert (not T.Locked); + procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type) is begin if New_Val > T.P.Last_Allocated then Grow (T, New_Val); diff --git a/gcc/ada/g-dyntab.ads b/gcc/ada/g-dyntab.ads index eb7181565db..9bfccc2822e 100644 --- a/gcc/ada/g-dyntab.ads +++ b/gcc/ada/g-dyntab.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2000-2016, AdaCore -- +-- Copyright (C) 2000-2017, AdaCore -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -36,13 +36,10 @@ -- arrays as closely as possible with the one additional capability of -- dynamically modifying the value of the Last attribute. --- This package provides a facility similar to that of GNAT.Table, except --- that this package declares a type that can be used to define dynamic --- instances of the table, while an instantiation of GNAT.Table creates a --- single instance of the table type. +-- This package provides a facility similar to that of Ada.Containers.Vectors. -- Note that these three interfaces should remain synchronized to keep as much --- coherency as possible among these three related units: +-- coherency as possible among these related units: -- -- GNAT.Dynamic_Tables -- GNAT.Table @@ -56,9 +53,10 @@ generic type Table_Component_Type is private; type Table_Index_Type is range <>; - Table_Low_Bound : Table_Index_Type; - Table_Initial : Positive := 8; - Table_Increment : Natural := 100; + Table_Low_Bound : Table_Index_Type; + Table_Initial : Positive := 8; + Table_Increment : Natural := 100; + Release_Threshold : Natural := 0; -- size in bytes package GNAT.Dynamic_Tables is @@ -69,15 +67,42 @@ package GNAT.Dynamic_Tables is -- The lower bound of Table_Index_Type is ignored. - pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First); + -- Table_Component_Type must not be a type with controlled parts. - function First return Table_Index_Type; - pragma Inline (First); - -- Export First as synonym for Table_Low_Bound (parallel with use of Last) + -- The Table_Initial value controls the allocation of the table when + -- it is first allocated. + + -- The Table_Increment value controls the amount of increase, if the + -- table has to be increased in size. The value given is a percentage + -- value (e.g. 100 = increase table size by 100%, i.e. double it). + + -- The Last and Set_Last subprograms provide control over the current + -- logical allocation. They are quite efficient, so they can be used + -- freely (expensive reallocation occurs only at major granularity + -- chunks controlled by the allocation parameters). + + -- Note: we do not make the table components aliased, since this would + -- restrict the use of table for discriminated types. If it is necessary + -- to take the access of a table element, use Unrestricted_Access. + + -- WARNING: On HPPA, the virtual addressing approach used in this unit + -- is incompatible with the indexing instructions on the HPPA. So when + -- using this unit, compile your application with -mdisable-indexing. + + -- WARNING: If the table is reallocated, then the address of all its + -- components will change. So do not capture the address of an element + -- and then use the address later after the table may be reallocated. + -- One tricky case of this is passing an element of the table to a + -- subprogram by reference where the table gets reallocated during + -- the execution of the subprogram. The best rule to follow is never + -- to pass a table element as a parameter except for the case of IN + -- mode parameters with scalar values. + + pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First); subtype Valid_Table_Index_Type is Table_Index_Type'Base range Table_Low_Bound .. Table_Index_Type'Base'Last; - subtype Table_Count_Type is Table_Index_Type'Base + subtype Table_Last_Type is Table_Index_Type'Base range Table_Low_Bound - 1 .. Table_Index_Type'Base'Last; -- Table_Component_Type must not be a type with controlled parts. @@ -112,7 +137,7 @@ package GNAT.Dynamic_Tables is -- Table : Table_Type renames T.Table (First .. Last (T)); - -- and the refer to components of Table. + -- and then refer to components of Table. type Table_Ptr is access all Big_Table_Type; for Table_Ptr'Storage_Size use 0; @@ -132,7 +157,7 @@ package GNAT.Dynamic_Tables is -- an empty array. type Instance is record - Table : aliased Table_Ptr := + Table : Table_Ptr := Empty_Table_Array_Ptr_To_Table_Ptr (Empty_Table_Array'Access); -- The table itself. The lower bound is the value of First. Logically -- the upper bound is the current value of Last (although the actual @@ -143,35 +168,50 @@ package GNAT.Dynamic_Tables is -- to ensure bounds checking, as in: -- -- Tab : Table_Type renames X.Table (First .. X.Last); + -- + -- Note: The Table component must come first. See declarations of + -- SCO_Unit_Table and SCO_Table in scos.h. Locked : Boolean := False; - -- Table expansion is permitted only if this switch is set to False. A - -- client may set Locked to True, in which case any attempt to expand - -- the table will cause an assertion failure. Note that while a table - -- is locked, its address in memory remains fixed and unchanging. + -- Table expansion is permitted only if this is False. A client may set + -- Locked to True, in which case any attempt to expand the table will + -- cause an assertion failure. Note that while a table is locked, its + -- address in memory remains fixed and unchanging. P : Table_Private; end record; + function Is_Empty (T : Instance) return Boolean; + procedure Init (T : in out Instance); -- Reinitializes the table to empty. There is no need to call this before -- using a table; tables default to empty. - function Last (T : Instance) return Table_Count_Type; + function First return Table_Index_Type; + pragma Inline (First); + -- Export First as synonym for Table_Low_Bound (parallel with use of Last) + + function Last (T : Instance) return Table_Last_Type; pragma Inline (Last); -- Returns the current value of the last used entry in the table, which can -- then be used as a subscript for Table. procedure Release (T : in out Instance); -- Storage is allocated in chunks according to the values given in the - -- Table_Initial and Table_Increment parameters. A call to Release releases - -- all storage that is allocated, but is not logically part of the current - -- array value. Current array values are not affected by this call. + -- Table_Initial and Table_Increment parameters. If Release_Threshold is 0 + -- or the length of the table does not exceed this threshold then a call to + -- Release releases all storage that is allocated, but is not logically + -- part of the current array value; otherwise the call to Release leaves + -- the current array value plus 0.1% of the current table length free + -- elements located at the end of the table. This parameter facilitates + -- reopening large tables and adding a few elements without allocating a + -- chunk of memory. In both cases current array values are not affected by + -- this call. procedure Free (T : in out Instance); -- Same as Init - procedure Set_Last (T : in out Instance; New_Val : Table_Count_Type); + procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type); pragma Inline (Set_Last); -- This procedure sets Last to the indicated value. If necessary the table -- is reallocated to accommodate the new value (i.e. on return the @@ -205,8 +245,11 @@ package GNAT.Dynamic_Tables is pragma Inline (Set_Item); -- Put Item in the table at position Index. If Index points to an existing -- item (i.e. it is in the range First .. Last (T)), the item is replaced. - -- Otherwise (i.e. Index > Last (T), the table is expanded, and Last is set - -- to Index. + -- Otherwise (i.e. Index > Last (T)), the table is expanded, and Last is + -- set to Index. + + procedure Move (From, To : in out Instance); + -- Moves from From to To, and sets From to empty procedure Allocate (T : in out Instance; Num : Integer := 1); pragma Inline (Allocate); @@ -236,11 +279,11 @@ package GNAT.Dynamic_Tables is private type Table_Private is record - Last_Allocated : Table_Count_Type := Table_Low_Bound - 1; + Last_Allocated : Table_Last_Type := Table_Low_Bound - 1; -- Subscript of the maximum entry in the currently allocated table. -- Initial value ensures that we initially allocate the table. - Last : Table_Count_Type := Table_Low_Bound - 1; + Last : Table_Last_Type := Table_Low_Bound - 1; -- Current value of Last function -- Invariant: Last <= Last_Allocated diff --git a/gcc/ada/g-table.adb b/gcc/ada/g-table.adb index c5c5891336a..1c122d73a52 100644 --- a/gcc/ada/g-table.adb +++ b/gcc/ada/g-table.adb @@ -29,8 +29,6 @@ -- -- ------------------------------------------------------------------------------ -with GNAT.Heap_Sort_G; - with System; use System; with System.Memory; use System.Memory; @@ -38,53 +36,20 @@ with Ada.Unchecked_Conversion; package body GNAT.Table is - Min : constant Integer := Integer (Table_Low_Bound); - -- Subscript of the minimum entry in the currently allocated table - - Max : Integer; - -- Subscript of the maximum entry in the currently allocated table - - Length : Integer := 0; - -- Number of entries in currently allocated table. The value of zero - -- ensures that we initially allocate the table. - - Last_Val : Integer; - -- Current value of Last - - ----------------------- - -- Local Subprograms -- - ----------------------- - - procedure Reallocate; - -- Reallocate the existing table according to the current value stored - -- in Max. Works correctly to do an initial allocation if the table - -- is currently null. - - pragma Warnings (Off); - -- Turn off warnings. The following unchecked conversions are only used - -- internally in this package, and cannot never result in any instances - -- of improperly aliased pointers for the client of the package. - - function To_Address is new Ada.Unchecked_Conversion (Table_Ptr, Address); - function To_Pointer is new Ada.Unchecked_Conversion (Address, Table_Ptr); - - pragma Warnings (On); - -------------- -- Allocate -- -------------- - function Allocate (Num : Integer := 1) return Table_Index_Type is - Old_Last : constant Integer := Last_Val; - + procedure Allocate (Num : Integer := 1) is begin - Last_Val := Last_Val + Num; - - if Last_Val > Max then - Reallocate; - end if; + Tab.Allocate (The_Instance, Num); + end Allocate; - return Table_Index_Type (Old_Last + 1); + function Allocate (Num : Integer := 1) return Valid_Table_Index_Type is + Result : constant Valid_Table_Index_Type := Last + 1; + begin + Allocate (Num); + return Result; end Allocate; ------------ @@ -93,7 +58,7 @@ package body GNAT.Table is procedure Append (New_Val : Table_Component_Type) is begin - Set_Item (Table_Index_Type (Last_Val + 1), New_Val); + Tab.Append (The_Instance, New_Val); end Append; ---------------- @@ -102,9 +67,7 @@ package body GNAT.Table is procedure Append_All (New_Vals : Table_Type) is begin - for J in New_Vals'Range loop - Append (New_Vals (J)); - end loop; + Tab.Append_All (The_Instance, New_Vals); end Append_All; -------------------- @@ -113,7 +76,7 @@ package body GNAT.Table is procedure Decrement_Last is begin - Last_Val := Last_Val - 1; + Tab.Decrement_Last (The_Instance); end Decrement_Last; ----------- @@ -122,7 +85,7 @@ package body GNAT.Table is function First return Table_Index_Type is begin - return Table_Low_Bound; + return Tab.First; end First; -------------- @@ -130,12 +93,9 @@ package body GNAT.Table is -------------- procedure For_Each is - Quit : Boolean := False; + procedure For_Each is new Tab.For_Each (Action); begin - for Index in Table_Low_Bound .. Table_Index_Type (Last_Val) loop - Action (Index, Table (Index), Quit); - exit when Quit; - end loop; + For_Each (The_Instance); end For_Each; ---------- @@ -144,9 +104,7 @@ package body GNAT.Table is procedure Free is begin - Free (To_Address (Table)); - Table := null; - Length := 0; + Tab.Free (The_Instance); end Free; -------------------- @@ -155,201 +113,85 @@ package body GNAT.Table is procedure Increment_Last is begin - Last_Val := Last_Val + 1; - - if Last_Val > Max then - Reallocate; - end if; + Tab.Increment_Last (The_Instance); end Increment_Last; + -------------- + -- Is_Empty -- + -------------- + + function Is_Empty return Boolean is + begin + return Tab.Is_Empty (The_Instance); + end Is_Empty; + ---------- -- Init -- ---------- procedure Init is - Old_Length : constant Integer := Length; - begin - Last_Val := Min - 1; - Max := Min + Table_Initial - 1; - Length := Max - Min + 1; - - -- If table is same size as before (happens when table is never - -- expanded which is a common case), then simply reuse it. Note - -- that this also means that an explicit Init call right after - -- the implicit one in the package body is harmless. - - if Old_Length = Length then - return; - - -- Otherwise we can use Reallocate to get a table of the right size. - -- Note that Reallocate works fine to allocate a table of the right - -- initial size when it is first allocated. - - else - Reallocate; - end if; + Tab.Init (The_Instance); end Init; ---------- -- Last -- ---------- - function Last return Table_Index_Type is + function Last return Table_Last_Type is begin - return Table_Index_Type (Last_Val); + return Tab.Last (The_Instance); end Last; - ---------------- - -- Reallocate -- - ---------------- - - procedure Reallocate is - New_Size : size_t; - New_Length : Long_Long_Integer; - - begin - if Max < Last_Val then - pragma Assert (not Locked); - - -- Now increment table length until it is sufficiently large. Use - -- the increment value or 10, which ever is larger (the reason - -- for the use of 10 here is to ensure that the table does really - -- increase in size (which would not be the case for a table of - -- length 10 increased by 3% for instance). Do the intermediate - -- calculation in Long_Long_Integer to avoid overflow. - - while Max < Last_Val loop - New_Length := - Long_Long_Integer (Length) * - (100 + Long_Long_Integer (Table_Increment)) / 100; - Length := Integer'Max (Integer (New_Length), Length + 10); - Max := Min + Length - 1; - end loop; - end if; - - New_Size := - size_t ((Max - Min + 1) * - (Table_Type'Component_Size / Storage_Unit)); - - if Table = null then - Table := To_Pointer (Alloc (New_Size)); - - elsif New_Size > 0 then - Table := - To_Pointer (Realloc (Ptr => To_Address (Table), - Size => New_Size)); - end if; - - if Length /= 0 and then Table = null then - raise Storage_Error; - end if; - - end Reallocate; - ------------- -- Release -- ------------- procedure Release is begin - Length := Last_Val - Integer (Table_Low_Bound) + 1; - Max := Last_Val; - Reallocate; + Tab.Release (The_Instance); end Release; + ------------- + -- Restore -- + ------------- + + procedure Restore (T : in out Saved_Table) is + begin + Init; + Tab.Move (From => T, To => The_Instance); + end Restore; + + ---------- + -- Save -- + ---------- + + function Save return Saved_Table is + Result : Saved_Table; + begin + Tab.Move (From => The_Instance, To => Result); + return Result; + end Save; + -------------- -- Set_Item -- -------------- procedure Set_Item - (Index : Table_Index_Type; - Item : Table_Component_Type) + (Index : Valid_Table_Index_Type; + Item : Table_Component_Type) is - -- If Item is a value within the current allocation, and we are going to - -- reallocate, then we must preserve an intermediate copy here before - -- calling Increment_Last. Otherwise, if Table_Component_Type is passed - -- by reference, we are going to end up copying from storage that might - -- have been deallocated from Increment_Last calling Reallocate. - - subtype Allocated_Table_T is - Table_Type (Table'First .. Table_Index_Type (Max + 1)); - -- A constrained table subtype one element larger than the currently - -- allocated table. - - Allocated_Table_Address : constant System.Address := - Table.all'Address; - -- Used for address clause below (we can't use non-static expression - -- Table.all'Address directly in the clause because some older versions - -- of the compiler do not allow it). - - Allocated_Table : Allocated_Table_T; - pragma Import (Ada, Allocated_Table); - pragma Suppress (Range_Check, On => Allocated_Table); - for Allocated_Table'Address use Allocated_Table_Address; - -- Allocated_Table represents the currently allocated array, plus one - -- element (the supplementary element is used to have a convenient - -- way of computing the address just past the end of the current - -- allocation). Range checks are suppressed because this unit uses - -- direct calls to System.Memory for allocation, and this can yield - -- misaligned storage (and we cannot rely on the bootstrap compiler - -- supporting specifically disabling alignment checks, so we need to - -- suppress all range checks). It is safe to suppress this check here - -- because we know that a (possibly misaligned) object of that type - -- does actually exist at that address. ??? We should really improve - -- the allocation circuitry here to - -- guarantee proper alignment. - - Need_Realloc : constant Boolean := Integer (Index) > Max; - -- True if this operation requires storage reallocation (which may - -- involve moving table contents around). - begin - -- If we're going to reallocate, check whether Item references an - -- element of the currently allocated table. - - if Need_Realloc - and then Allocated_Table'Address <= Item'Address - and then Item'Address < - Allocated_Table (Table_Index_Type (Max + 1))'Address - then - -- If so, save a copy on the stack because Increment_Last will - -- reallocate storage and might deallocate the current table. - - declare - Item_Copy : constant Table_Component_Type := Item; - begin - Set_Last (Index); - Table (Index) := Item_Copy; - end; - - else - -- Here we know that either we won't reallocate (case of Index < Max) - -- or that Item is not in the currently allocated table. - - if Integer (Index) > Last_Val then - Set_Last (Index); - end if; - - Table (Index) := Item; - end if; + Tab.Set_Item (The_Instance, Index, Item); end Set_Item; -------------- -- Set_Last -- -------------- - procedure Set_Last (New_Val : Table_Index_Type) is + procedure Set_Last (New_Val : Table_Last_Type) is begin - if Integer (New_Val) < Last_Val then - Last_Val := Integer (New_Val); - else - Last_Val := Integer (New_Val); - - if Last_Val > Max then - Reallocate; - end if; - end if; + Tab.Set_Last (The_Instance, New_Val); end Set_Last; ---------------- @@ -357,69 +199,9 @@ package body GNAT.Table is ---------------- procedure Sort_Table is - - Temp : Table_Component_Type; - -- A temporary position to simulate index 0 - - -- Local subprograms - - function Index_Of (Idx : Natural) return Table_Index_Type; - -- Return index of Idx'th element of table - - function Lower_Than (Op1, Op2 : Natural) return Boolean; - -- Compare two components - - procedure Move (From : Natural; To : Natural); - -- Move one component - - package Heap_Sort is new GNAT.Heap_Sort_G (Move, Lower_Than); - - -------------- - -- Index_Of -- - -------------- - - function Index_Of (Idx : Natural) return Table_Index_Type is - J : constant Integer'Base := Table_Index_Type'Pos (First) + Idx - 1; - begin - return Table_Index_Type'Val (J); - end Index_Of; - - ---------- - -- Move -- - ---------- - - procedure Move (From : Natural; To : Natural) is - begin - if From = 0 then - Table (Index_Of (To)) := Temp; - elsif To = 0 then - Temp := Table (Index_Of (From)); - else - Table (Index_Of (To)) := Table (Index_Of (From)); - end if; - end Move; - - ---------------- - -- Lower_Than -- - ---------------- - - function Lower_Than (Op1, Op2 : Natural) return Boolean is - begin - if Op1 = 0 then - return Lt (Temp, Table (Index_Of (Op2))); - elsif Op2 = 0 then - return Lt (Table (Index_Of (Op1)), Temp); - else - return Lt (Table (Index_Of (Op1)), Table (Index_Of (Op2))); - end if; - end Lower_Than; - - -- Start of processing for Sort_Table - + procedure Sort_Table is new Tab.Sort_Table (Lt); begin - Heap_Sort.Sort (Natural (Last - First) + 1); + Sort_Table (The_Instance); end Sort_Table; -begin - Init; end GNAT.Table; diff --git a/gcc/ada/g-table.ads b/gcc/ada/g-table.ads index d27b3224224..c2c33244d95 100644 --- a/gcc/ada/g-table.ads +++ b/gcc/ada/g-table.ads @@ -29,198 +29,117 @@ -- -- ------------------------------------------------------------------------------ --- Resizable one dimensional array support +-- This package provides a singleton version of GNAT.Dynamic_Tables +-- (g-dyntab.ads). See that package for documentation. This package just +-- declares a single instance of GNAT.Dynamic_Tables.Instance, and provides +-- wrappers for all the subprograms, passing that single instance. --- This package provides an implementation of dynamically resizable one --- dimensional arrays. The idea is to mimic the normal Ada semantics for --- arrays as closely as possible with the one additional capability of --- dynamically modifying the value of the Last attribute. +-- Note that these three interfaces should remain synchronized to keep as much +-- coherency as possible among these related units: +-- +-- GNAT.Dynamic_Tables +-- GNAT.Table +-- Table (the compiler unit) --- This package provides a facility similar to that of GNAT.Dynamic_Tables, --- except that this package declares a single instance of the table type, --- while an instantiation of GNAT.Dynamic_Tables creates a type that can be --- used to define dynamic instances of the table. +pragma Compiler_Unit_Warning; --- Note that this interface should remain synchronized with those in --- GNAT.Dynamic_Tables and the GNAT compiler source unit Table to keep --- as much coherency as possible between these three related units. +with GNAT.Dynamic_Tables; generic type Table_Component_Type is private; type Table_Index_Type is range <>; - Table_Low_Bound : Table_Index_Type; - Table_Initial : Positive; - Table_Increment : Natural; + Table_Low_Bound : Table_Index_Type; + Table_Initial : Positive := 8; + Table_Increment : Natural := 100; + Table_Name : String := ""; -- for debugging printouts + pragma Unreferenced (Table_Name); + Release_Threshold : Natural := 0; package GNAT.Table is pragma Elaborate_Body; - -- Table_Component_Type and Table_Index_Type specify the type of the - -- array, Table_Low_Bound is the lower bound. Table_Index_Type must be an - -- integer type. The effect is roughly to declare: - - -- Table : array (Table_Index_Type range Table_Low_Bound .. <>) - -- of Table_Component_Type; - - -- Note: since the upper bound can be one less than the lower - -- bound for an empty array, the table index type must be able - -- to cover this range, e.g. if the lower bound is 1, then the - -- Table_Index_Type should be Natural rather than Positive. - - -- Table_Component_Type may be any Ada type, except that controlled - -- types are not supported. Note however that default initialization - -- will NOT occur for array components. - - -- The Table_Initial values controls the allocation of the table when - -- it is first allocated, either by default, or by an explicit Init call. - - -- The Table_Increment value controls the amount of increase, if the - -- table has to be increased in size. The value given is a percentage - -- value (e.g. 100 = increase table size by 100%, i.e. double it). - - -- The Last and Set_Last subprograms provide control over the current - -- logical allocation. They are quite efficient, so they can be used - -- freely (expensive reallocation occurs only at major granularity - -- chunks controlled by the allocation parameters). - - -- Note: we do not make the table components aliased, since this would - -- restrict the use of table for discriminated types. If it is necessary - -- to take the access of a table element, use Unrestricted_Access. - - -- WARNING: On HPPA, the virtual addressing approach used in this unit - -- is incompatible with the indexing instructions on the HPPA. So when - -- using this unit, compile your application with -mdisable-indexing. - - -- WARNING: If the table is reallocated, then the address of all its - -- components will change. So do not capture the address of an element - -- and then use the address later after the table may be reallocated. - -- One tricky case of this is passing an element of the table to a - -- subprogram by reference where the table gets reallocated during - -- the execution of the subprogram. The best rule to follow is never - -- to pass a table element as a parameter except for the case of IN - -- mode parameters with scalar values. - - type Table_Type is - array (Table_Index_Type range <>) of Table_Component_Type; - subtype Big_Table_Type is - Table_Type (Table_Low_Bound .. Table_Index_Type'Last); - -- We work with pointers to a bogus array type that is constrained - -- with the maximum possible range bound. This means that the pointer - -- is a thin pointer, which is more efficient. Since subscript checks - -- in any case must be on the logical, rather than physical bounds, - -- safety is not compromised by this approach. These types should never - -- be used by the client. - - type Table_Ptr is access all Big_Table_Type; - for Table_Ptr'Storage_Size use 0; - -- The table is actually represented as a pointer to allow reallocation. - -- This type should never be used by the client. - - Table : aliased Table_Ptr := null; - -- The table itself. The lower bound is the value of Low_Bound. - -- Logically the upper bound is the current value of Last (although - -- the actual size of the allocated table may be larger than this). - -- The program may only access and modify Table entries in the range - -- First .. Last. - - Locked : Boolean := False; - -- Table expansion is permitted only if this switch is set to False. A - -- client may set Locked to True, in which case any attempt to expand - -- the table will cause an assertion failure. Note that while a table - -- is locked, its address in memory remains fixed and unchanging. + package Tab is new GNAT.Dynamic_Tables + (Table_Component_Type, + Table_Index_Type, + Table_Low_Bound, + Table_Initial, + Table_Increment, + Release_Threshold); + + subtype Valid_Table_Index_Type is Tab.Valid_Table_Index_Type; + subtype Table_Last_Type is Tab.Table_Last_Type; + subtype Table_Type is Tab.Table_Type; + subtype Big_Table_Type is Tab.Big_Table_Type; + + subtype Table_Ptr is Tab.Table_Ptr; + + The_Instance : Tab.Instance; + Table : Table_Ptr renames The_Instance.Table; + Locked : Boolean renames The_Instance.Locked; + + function Is_Empty return Boolean; procedure Init; - -- This procedure allocates a new table of size Initial (freeing any - -- previously allocated larger table). It is not necessary to call - -- Init when a table is first instantiated (since the instantiation does - -- the same initialization steps). However, it is harmless to do so, and - -- Init is convenient in reestablishing a table for new use. - function Last return Table_Index_Type; + function First return Table_Index_Type; + pragma Inline (First); + + function Last return Table_Last_Type; pragma Inline (Last); - -- Returns the current value of the last used entry in the table, which - -- can then be used as a subscript for Table. Note that the only way to - -- modify Last is to call the Set_Last procedure. Last must always be - -- used to determine the logically last entry. procedure Release; - -- Storage is allocated in chunks according to the values given in the - -- Initial and Increment parameters. A call to Release releases all - -- storage that is allocated, but is not logically part of the current - -- array value. Current array values are not affected by this call. procedure Free; - -- Free all allocated memory for the table. A call to Init is required - -- before any use of this table after calling Free. - function First return Table_Index_Type; - pragma Inline (First); - -- Export First as synonym for Table_Low_Bound (parallel with use of Last) - - procedure Set_Last (New_Val : Table_Index_Type); + procedure Set_Last (New_Val : Table_Last_Type); pragma Inline (Set_Last); - -- This procedure sets Last to the indicated value. If necessary the - -- table is reallocated to accommodate the new value (i.e. on return - -- the allocated table has an upper bound of at least Last). If Set_Last - -- reduces the size of the table, then logically entries are removed - -- from the table. If Set_Last increases the size of the table, then - -- new entries are logically added to the table. procedure Increment_Last; pragma Inline (Increment_Last); - -- Adds 1 to Last (same as Set_Last (Last + 1) procedure Decrement_Last; pragma Inline (Decrement_Last); - -- Subtracts 1 from Last (same as Set_Last (Last - 1) procedure Append (New_Val : Table_Component_Type); pragma Inline (Append); - -- Equivalent to: - -- x.Increment_Last; - -- x.Table (x.Last) := New_Val; - -- i.e. the table size is increased by one, and the given new item - -- stored in the newly created table element. procedure Append_All (New_Vals : Table_Type); - -- Appends all components of New_Vals procedure Set_Item - (Index : Table_Index_Type; + (Index : Valid_Table_Index_Type; Item : Table_Component_Type); pragma Inline (Set_Item); - -- Put Item in the table at position Index. The table is expanded if the - -- current table length is less than Index and in that case Last is set to - -- Index. Item will replace any value already present in the table at this - -- position. - function Allocate (Num : Integer := 1) return Table_Index_Type; + subtype Saved_Table is Tab.Instance; + -- Type used for Save/Restore subprograms + + function Save return Saved_Table; + -- Resets table to empty, but saves old contents of table in returned + -- value, for possible later restoration by a call to Restore. + + procedure Restore (T : in out Saved_Table); + -- Given a Saved_Table value returned by a prior call to Save, restores + -- the table to the state it was in at the time of the Save call. + + procedure Allocate (Num : Integer := 1); + function Allocate (Num : Integer := 1) return Valid_Table_Index_Type; pragma Inline (Allocate); - -- Adds Num to Last, and returns the old value of Last + 1. Note that - -- this function has the possible side effect of reallocating the table. - -- This means that a reference X.Table (X.Allocate) is incorrect, since - -- the call to X.Allocate may modify the results of calling X.Table. + -- Adds Num to Last. The function version also returns the old value of + -- Last + 1. Note that this function has the possible side effect of + -- reallocating the table. This means that a reference X.Table (X.Allocate) + -- is incorrect, since the call to X.Allocate may modify the results of + -- calling X.Table. generic with procedure Action - (Index : Table_Index_Type; + (Index : Valid_Table_Index_Type; Item : Table_Component_Type; Quit : in out Boolean) is <>; procedure For_Each; - -- Calls procedure Action for each component of the table, or until - -- one of these calls set Quit to True. generic with function Lt (Comp1, Comp2 : Table_Component_Type) return Boolean; procedure Sort_Table; - -- This procedure sorts the components of the table into ascending - -- order making calls to Lt to do required comparisons, and using - -- assignments to move components around. The Lt function returns True - -- if Comp1 is less than Comp2 (in the sense of the desired sort), and - -- False if Comp1 is greater than Comp2. For equal objects it does not - -- matter if True or False is returned (it is slightly more efficient - -- to return False). The sort is not stable (the order of equal items - -- in the table is not preserved). end GNAT.Table; diff --git a/gcc/ada/namet.adb b/gcc/ada/namet.adb index aed85313451..20dd504b018 100644 --- a/gcc/ada/namet.adb +++ b/gcc/ada/namet.adb @@ -36,6 +36,7 @@ with Debug; use Debug; with Opt; use Opt; with Output; use Output; +with System; use System; with Tree_IO; use Tree_IO; with Widechar; use Widechar; @@ -1093,15 +1094,6 @@ package body Namet is Name_Entries.Release; end Lock; - ------------------------ - -- Name_Chars_Address -- - ------------------------ - - function Name_Chars_Address return System.Address is - begin - return Name_Chars.Table (0)'Address; - end Name_Chars_Address; - ---------------- -- Name_Enter -- ---------------- @@ -1139,15 +1131,6 @@ package body Namet is return Name_Enter (Buf); end Name_Enter; - -------------------------- - -- Name_Entries_Address -- - -------------------------- - - function Name_Entries_Address return System.Address is - begin - return Name_Entries.Table (First_Name_Id)'Address; - end Name_Entries_Address; - ------------------------ -- Name_Entries_Count -- ------------------------ diff --git a/gcc/ada/namet.ads b/gcc/ada/namet.ads index b2a2ed5fe81..124f7782036 100644 --- a/gcc/ada/namet.ads +++ b/gcc/ada/namet.ads @@ -32,7 +32,6 @@ with Alloc; with Hostparm; use Hostparm; with Table; -with System; use System; with Types; use Types; package Namet is @@ -564,13 +563,6 @@ package Namet is -- Like Write_Name, except that the name written is the decoded name, as -- described for Append_Decoded. - function Name_Chars_Address return System.Address; - -- Return starting address of name characters table (used in Back_End call - -- to Gigi). - - function Name_Entries_Address return System.Address; - -- Return starting address of Names table (used in Back_End call to Gigi) - function Name_Entries_Count return Nat; -- Return current number of entries in the names table diff --git a/gcc/ada/namet.h b/gcc/ada/namet.h index a016f93b93d..84255a807fa 100644 --- a/gcc/ada/namet.h +++ b/gcc/ada/namet.h @@ -6,7 +6,7 @@ * * * C Header File * * * - * Copyright (C) 1992-2016, Free Software Foundation, Inc. * + * Copyright (C) 1992-2017, Free Software Foundation, Inc. * * * * GNAT is free software; you can redistribute it and/or modify it under * * terms of the GNU General Public License as published by the Free Soft- * @@ -45,11 +45,11 @@ struct Name_Entry }; /* Pointer to names table vector. */ -#define Names_Ptr namet__name_entries__table +#define Names_Ptr namet__name_entries__tab__the_instance extern struct Name_Entry *Names_Ptr; /* Pointer to name characters table. */ -#define Name_Chars_Ptr namet__name_chars__table +#define Name_Chars_Ptr namet__name_chars__tab__the_instance extern char *Name_Chars_Ptr; /* This is Hostparm.Max_Line_Length. */ diff --git a/gcc/ada/osint.ads b/gcc/ada/osint.ads index 4712b9885f8..2805bfe62ad 100644 --- a/gcc/ada/osint.ads +++ b/gcc/ada/osint.ads @@ -662,7 +662,7 @@ package Osint is -- The suffixes used for the ALI files function Prep_Suffix return String; - -- The suffix used for pre-processed files + -- The suffix used for preprocessed files private diff --git a/gcc/ada/scos.h b/gcc/ada/scos.h index 6c1f545af95..4fb396ca630 100644 --- a/gcc/ada/scos.h +++ b/gcc/ada/scos.h @@ -45,8 +45,10 @@ struct SCO_Unit_Table_Entry typedef struct SCO_Unit_Table_Entry *SCO_Unit_Table_Type; -extern SCO_Unit_Table_Type scos__sco_unit_table__table; -#define SCO_Unit_Table scos__sco_unit_table__table +/* The following depends on the fact that The_Instance.Table + is the first component. */ +extern SCO_Unit_Table_Type scos__sco_unit_table__the_instance; +#define SCO_Unit_Table scos__sco_unit_table__the_instance extern Int scos__sco_unit_table__first(void); #define SCO_Unit_Table_First scos__sco_unit_table__first @@ -74,8 +76,10 @@ struct SCO_Table_Entry typedef struct SCO_Table_Entry *SCO_Table_Type; -extern SCO_Table_Type scos__sco_table__table; -#define SCO_Table scos__sco_table__table +/* The following depends on the fact that The_Instance.Table + is the first component. */ +extern SCO_Table_Type scos__sco_table__the_instance; +#define SCO_Table scos__sco_table__the_instance extern Int scos__sco_table__first(void); #define SCO_Table_First scos__sco_table__first diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 6bf6dfdb728..2579ab5eaff 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -65,36 +65,51 @@ package body Sem_Elab is -- Elab_Call.Last) indicates the current depth of recursion and is used to -- identify the outer level. - type Elab_Call_Entry is record + type Elab_Call_Element is record Cloc : Source_Ptr; Ent : Entity_Id; end record; package Elab_Call is new Table.Table - (Table_Component_Type => Elab_Call_Entry, + (Table_Component_Type => Elab_Call_Element, Table_Index_Type => Int, Table_Low_Bound => 1, Table_Initial => 50, Table_Increment => 100, Table_Name => "Elab_Call"); - -- This table is initialized at the start of each outer level call. It - -- holds the entities for all subprograms that have been examined for this - -- particular outer level call, and is used to prevent both infinite - -- recursion, and useless reanalysis of bodies already seen + -- The following table records all calls that have been processed starting + -- from an outer level call. The table prevents both infinite recursion and + -- useless reanalysis of calls within the same context. The use of context + -- is important because it allows for proper checks in more complex code: + + -- if ... then + -- Call; -- requires a check + -- Call; -- does not need a check thanks to the table + -- elsif ... then + -- Call; -- requires a check, different context + -- end if; + + -- Call; -- requires a check, different context + + type Visited_Element is record + Subp_Id : Entity_Id; + -- The entity of the subprogram being called + + Context : Node_Id; + -- The context where the call to the subprogram occurs + end record; package Elab_Visited is new Table.Table - (Table_Component_Type => Entity_Id, + (Table_Component_Type => Visited_Element, Table_Index_Type => Int, Table_Low_Bound => 1, Table_Initial => 200, Table_Increment => 100, Table_Name => "Elab_Visited"); - -- This table stores calls to Check_Internal_Call that are delayed until - -- all generics are instantiated and in particular until after all generic - -- bodies have been inserted. We need to delay, because we need to be able - -- to look through the inserted bodies. + -- The following table records delayed calls which must be examined after + -- all generic bodies have been instantiated. type Delay_Element is record N : Node_Id; @@ -743,7 +758,7 @@ package body Sem_Elab is loop if (Suppress_Elaboration_Warnings (Ent) - or else Elaboration_Checks_Suppressed (Ent)) + or else Elaboration_Checks_Suppressed (Ent)) and then (Inst_Case or else No (Alias (Ent))) then return; @@ -913,17 +928,17 @@ package body Sem_Elab is Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (C_Scope))); end if; - -- Do not give a warning if the with'ed unit is internal and the - -- caller is not internal (since the binder always elaborates - -- internal units first). + -- Do not give a warning if the with'ed unit is internal and the caller + -- is not internal (since the binder always elaborates internal units + -- first). - if Callee_Unit_Internal and (not Caller_Unit_Internal) then + if Callee_Unit_Internal and not Caller_Unit_Internal then return; end if; - -- For now, if debug flag -gnatdE is not set, do no checking for - -- one internal unit withing another. This fixes the problem with - -- the sgi build and storage errors. To be resolved later ??? + -- For now, if debug flag -gnatdE is not set, do no checking for one + -- internal unit withing another. This fixes the problem with the sgi + -- build and storage errors. To be resolved later ??? if (Callee_Unit_Internal and Caller_Unit_Internal) and not Debug_Flag_EE @@ -1151,7 +1166,7 @@ package body Sem_Elab is -- All_Errors_Mode. if not All_Errors_Mode and not Dynamic_Elaboration_Checks then - Set_Suppress_Elaboration_Warnings (W_Scope, True); + Set_Suppress_Elaboration_Warnings (W_Scope); end if; end if; @@ -1218,8 +1233,8 @@ package body Sem_Elab is then Error_Msg_Node_2 := W_Scope; Error_Msg_NE - ("info: call to& in elaboration code " & - "requires pragma Elaborate_All on&?$?", N, E); + ("info: call to& in elaboration code requires pragma " + & "Elaborate_All on&?$?", N, E); end if; -- Set indication for binder to generate Elaborate_All @@ -1623,14 +1638,22 @@ package body Sem_Elab is return; end if; - -- Nothing to do if this is a recursive call (i.e. a call to - -- an entity that is already in the Elab_Call stack) + -- Determine whether a prior call to the same subprogram was already + -- examined within the same context. If this is the case, then there is + -- no need to proceed with the various warnings and checks because the + -- work was already done for the previous call. - for J in 1 .. Elab_Visited.Last loop - if Ent = Elab_Visited.Table (J) then - return; - end if; - end loop; + declare + Self : constant Visited_Element := + (Subp_Id => Ent, Context => Parent (N)); + + begin + for Index in 1 .. Elab_Visited.Last loop + if Self = Elab_Visited.Table (Index) then + return; + end if; + end loop; + end; -- See if we need to analyze this reference. We analyze it if either of -- the following conditions is met: @@ -2394,14 +2417,19 @@ package body Sem_Elab is Outer_Level_Sloc := Loc; end if; - Elab_Visited.Append (E); - -- If the call is to a function that renames a literal, no check needed if Ekind (E) = E_Enumeration_Literal then return; end if; + -- Register the subprogram as examined within this particular context. + -- This ensures that calls to the same subprogram but in different + -- contexts receive warnings and checks of their own since the calls + -- may be reached through different flow paths. + + Elab_Visited.Append ((Subp_Id => E, Context => Parent (N))); + Sbody := Unit_Declaration_Node (E); if not Nkind_In (Sbody, N_Subprogram_Body, N_Package_Body) then @@ -2422,8 +2450,8 @@ package body Sem_Elab is then null; - -- If we have the instantiation case we are done, since we now - -- know that the body of the generic appeared earlier. + -- If we have the instantiation case we are done, since we now know that + -- the body of the generic appeared earlier. elsif Inst_Case then return; @@ -2579,26 +2607,22 @@ package body Sem_Elab is if GNATprove_Mode then null; - -- Deal with dynamic elaboration check + -- Generate an elaboration check elsif not Elaboration_Checks_Suppressed (E) then Set_Elaboration_Entity_Required (E); - -- Case of no elaboration entity allocated yet + -- Create a declaration of the elaboration entity, and insert it + -- prior to the subprogram or the generic unit, within the same + -- scope. Since the subprogram may be overloaded, create a unique + -- entity. if No (Elaboration_Entity (E)) then - - -- Create object declaration for elaboration entity, and put it - -- just in front of the spec of the subprogram or generic unit, - -- in the same scope as this unit. The subprogram may be over- - -- loaded, so make the name of elaboration entity unique by - -- means of a numeric suffix. - declare Loce : constant Source_Ptr := Sloc (E); Ent : constant Entity_Id := Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (E), 'E', -1)); + New_External_Name (Chars (E), 'E', -1)); begin Set_Elaboration_Entity (E, Ent); @@ -2629,12 +2653,15 @@ package body Sem_Elab is end; end if; - -- Generate check of the elaboration counter + -- Generate: + -- if Enn = 0 then + -- raise Program_Error with "access before elaboration"; + -- end if; Insert_Elab_Check (N, - Make_Attribute_Reference (Loc, - Attribute_Name => Name_Elaborated, - Prefix => New_Occurrence_Of (E, Loc))); + Make_Attribute_Reference (Loc, + Attribute_Name => Name_Elaborated, + Prefix => New_Occurrence_Of (E, Loc))); end if; -- Generate the warning @@ -2657,8 +2684,8 @@ package body Sem_Elab is ("instantiation of& may occur before body is seen False); end if; end if; - - -- Set flag to suppress further warnings on same subprogram - -- unless in all errors mode - - if not All_Errors_Mode then - Set_Suppress_Elaboration_Warnings (E); - end if; end Check_Internal_Call_Continue; --------------------------- @@ -2909,32 +2929,32 @@ package body Sem_Elab is elsif Dynamic_Elaboration_Checks then if not Elaboration_Checks_Suppressed (Ent) and then not Cunit_SC - and then - not Restriction_Active (No_Entry_Calls_In_Elaboration_Code) + and then not Restriction_Active + (No_Entry_Calls_In_Elaboration_Code) then -- Runtime elaboration check required. Generate check of the -- elaboration counter for the unit containing the entity. Insert_Elab_Check (N, Make_Attribute_Reference (Loc, - Attribute_Name => Name_Elaborated, - Prefix => - New_Occurrence_Of (Spec_Entity (Task_Scope), Loc))); + Prefix => + New_Occurrence_Of (Spec_Entity (Task_Scope), Loc), + Attribute_Name => Name_Elaborated)); end if; else -- Force the binder to elaborate other unit first - if not Suppress_Elaboration_Warnings (Ent) + if Elab_Info_Messages + and then not Suppress_Elaboration_Warnings (Ent) and then not Elaboration_Checks_Suppressed (Ent) - and then Elab_Info_Messages and then not Suppress_Elaboration_Warnings (Task_Scope) and then not Elaboration_Checks_Suppressed (Task_Scope) then Error_Msg_Node_2 := Task_Scope; Error_Msg_NE - ("info: activation of an instance of task type&" & - " requires pragma Elaborate_All on &?$?", N, Ent); + ("info: activation of an instance of task type & requires " + & "pragma Elaborate_All on &?$?", N, Ent); end if; Activate_Elaborate_All_Desirable (N, Task_Scope); @@ -2988,18 +3008,19 @@ package body Sem_Elab is Subp : Entity_Id; Scop : Entity_Id) is - Elab_Unit : Entity_Id; + Elab_Unit : Entity_Id; -- Check whether this is a call to an Initialize subprogram for a -- controlled type. Note that Call can also be a 'Access attribute -- reference, which now generates an elaboration check. - Init_Call : constant Boolean := - Nkind (Call) = N_Procedure_Call_Statement - and then Chars (Subp) = Name_Initialize - and then Comes_From_Source (Subp) - and then Present (Parameter_Associations (Call)) - and then Is_Controlled (Etype (First_Actual (Call))); + Init_Call : constant Boolean := + Nkind (Call) = N_Procedure_Call_Statement + and then Chars (Subp) = Name_Initialize + and then Comes_From_Source (Subp) + and then Present (Parameter_Associations (Call)) + and then Is_Controlled (Etype (First_Actual (Call))); + begin -- If the unit is mentioned in a with_clause of the current unit, it is -- visible, and we can set the elaboration flag. @@ -3008,13 +3029,13 @@ package body Sem_Elab is or else (Is_Child_Unit (Scop) and then Is_Visible_Lib_Unit (Scop)) then Activate_Elaborate_All_Desirable (Call, Scop); - Set_Suppress_Elaboration_Warnings (Scop, True); + Set_Suppress_Elaboration_Warnings (Scop); return; end if; -- If this is not an initialization call or a call using object notation - -- we know that the unit of the called entity is in the context, and - -- we can set the flag as well. The unit need not be visible if the call + -- we know that the unit of the called entity is in the context, and we + -- can set the flag as well. The unit need not be visible if the call -- occurs within an instantiation. if Is_Init_Proc (Subp) @@ -3025,7 +3046,7 @@ package body Sem_Elab is else Activate_Elaborate_All_Desirable (Call, Scop); - Set_Suppress_Elaboration_Warnings (Scop, True); + Set_Suppress_Elaboration_Warnings (Scop); return; end if; @@ -3070,7 +3091,7 @@ package body Sem_Elab is end if; Activate_Elaborate_All_Desirable (Call, Elab_Unit); - Set_Suppress_Elaboration_Warnings (Elab_Unit, True); + Set_Suppress_Elaboration_Warnings (Elab_Unit); end Set_Elaboration_Constraint; ------------------------ @@ -3616,23 +3637,22 @@ package body Sem_Elab is if No (Corresponding_Body (N)) then declare Loc : constant Source_Ptr := Sloc (N); - B : Node_Id; - Formals : constant List_Id := Copy_Parameter_List (Ent); - Nam : constant Entity_Id := + Formals : constant List_Id := Copy_Parameter_List (Ent); + Nam : constant Entity_Id := Make_Defining_Identifier (Loc, Chars (Ent)); - Spec : Node_Id; - Stats : constant List_Id := - New_List - (Make_Raise_Program_Error (Loc, + Stats : constant List_Id := + New_List ( + Make_Raise_Program_Error (Loc, Reason => PE_Access_Before_Elaboration)); + Spec : Node_Id; begin if Ekind (Ent) = E_Function then Spec := Make_Function_Specification (Loc, - Defining_Unit_Name => Nam, + Defining_Unit_Name => Nam, Parameter_Specifications => Formals, - Result_Definition => + Result_Definition => New_Copy_Tree (Result_Definition (Specification (N)))); @@ -3645,17 +3665,16 @@ package body Sem_Elab is else Spec := Make_Procedure_Specification (Loc, - Defining_Unit_Name => Nam, + Defining_Unit_Name => Nam, Parameter_Specifications => Formals); end if; - B := Make_Subprogram_Body (Loc, - Specification => Spec, - Declarations => New_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, Stats)); - Insert_After (N, B); - Analyze (B); + Insert_After_And_Analyze (N, + Make_Subprogram_Body (Loc, + Specification => Spec, + Declarations => New_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, Stats))); end; end if; end; diff --git a/gcc/ada/table.adb b/gcc/ada/table.adb index 2c7eb0c4a66..5d4522b449a 100644 --- a/gcc/ada/table.adb +++ b/gcc/ada/table.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -29,9 +29,6 @@ -- -- ------------------------------------------------------------------------------ -with Debug; use Debug; -with Opt; use Opt; -with Output; use Output; with System; use System; with Tree_IO; use Tree_IO; @@ -39,370 +36,20 @@ with System.Memory; use System.Memory; with Unchecked_Conversion; -pragma Elaborate_All (Output); - package body Table is package body Table is - Min : constant Int := Int (Table_Low_Bound); - -- Subscript of the minimum entry in the currently allocated table - - Length : Int := 0; - -- Number of entries in currently allocated table. The value of zero - -- ensures that we initially allocate the table. - - ----------------------- - -- Local Subprograms -- - ----------------------- - - procedure Reallocate; - -- Reallocate the existing table according to the current value stored - -- in Max. Works correctly to do an initial allocation if the table - -- is currently null. - function Tree_Get_Table_Address return Address; -- Return Null_Address if the table length is zero, -- Table (First)'Address if not. - pragma Warnings (Off); - -- Turn off warnings. The following unchecked conversions are only used - -- internally in this package, and cannot never result in any instances - -- of improperly aliased pointers for the client of the package. - - function To_Address is new Unchecked_Conversion (Table_Ptr, Address); - function To_Pointer is new Unchecked_Conversion (Address, Table_Ptr); - - pragma Warnings (On); - - ------------ - -- Append -- - ------------ - - procedure Append (New_Val : Table_Component_Type) is - begin - Set_Item (Table_Index_Type (Last_Val + 1), New_Val); - end Append; - - ---------------- - -- Append_All -- - ---------------- - - procedure Append_All (New_Vals : Table_Type) is - begin - for J in New_Vals'Range loop - Append (New_Vals (J)); - end loop; - end Append_All; - - -------------------- - -- Decrement_Last -- - -------------------- - - procedure Decrement_Last is - begin - Last_Val := Last_Val - 1; - end Decrement_Last; - - ---------- - -- Free -- - ---------- - - procedure Free is - begin - Free (To_Address (Table)); - Table := null; - Length := 0; - end Free; - - -------------------- - -- Increment_Last -- - -------------------- - - procedure Increment_Last is - begin - Last_Val := Last_Val + 1; - - if Last_Val > Max then - Reallocate; - end if; - end Increment_Last; - - ---------- - -- Init -- - ---------- - - procedure Init is - Old_Length : constant Int := Length; - - begin - Locked := False; - Last_Val := Min - 1; - Max := Min + (Table_Initial * Table_Factor) - 1; - Length := Max - Min + 1; - - -- If table is same size as before (happens when table is never - -- expanded which is a common case), then simply reuse it. Note - -- that this also means that an explicit Init call right after - -- the implicit one in the package body is harmless. - - if Old_Length = Length then - return; - - -- Otherwise we can use Reallocate to get a table of the right size. - -- Note that Reallocate works fine to allocate a table of the right - -- initial size when it is first allocated. - - else - Reallocate; - end if; - end Init; - - ---------- - -- Last -- - ---------- - - function Last return Table_Index_Type is - begin - return Table_Index_Type (Last_Val); - end Last; - - ---------------- - -- Reallocate -- - ---------------- - - procedure Reallocate is - New_Size : Memory.size_t; - New_Length : Long_Long_Integer; - - begin - if Max < Last_Val then - pragma Assert (not Locked); - - -- Make sure that we have at least the initial allocation. This - -- is needed in cases where a zero length table is written out. - - Length := Int'Max (Length, Table_Initial); - - -- Now increment table length until it is sufficiently large. Use - -- the increment value or 10, which ever is larger (the reason - -- for the use of 10 here is to ensure that the table does really - -- increase in size (which would not be the case for a table of - -- length 10 increased by 3% for instance). Do the intermediate - -- calculation in Long_Long_Integer to avoid overflow. - - while Max < Last_Val loop - New_Length := - Long_Long_Integer (Length) * - (100 + Long_Long_Integer (Table_Increment)) / 100; - Length := Int'Max (Int (New_Length), Length + 10); - Max := Min + Length - 1; - end loop; - - if Debug_Flag_D then - Write_Str ("--> Allocating new "); - Write_Str (Table_Name); - Write_Str (" table, size = "); - Write_Int (Max - Min + 1); - Write_Eol; - end if; - end if; - - -- Do the intermediate calculation in size_t to avoid signed overflow - - New_Size := - Memory.size_t (Max - Min + 1) * - (Table_Type'Component_Size / Storage_Unit); - - if Table = null then - Table := To_Pointer (Alloc (New_Size)); - - elsif New_Size > 0 then - Table := - To_Pointer (Realloc (Ptr => To_Address (Table), - Size => New_Size)); - end if; - - if Length /= 0 and then Table = null then - Set_Standard_Error; - Write_Str ("available memory exhausted"); - Write_Eol; - Set_Standard_Output; - raise Unrecoverable_Error; - end if; - end Reallocate; - - ------------- - -- Release -- - ------------- - - procedure Release is - Extra_Length : Int; - Size : Memory.size_t; - - begin - Length := Last_Val - Int (Table_Low_Bound) + 1; - Size := Memory.size_t (Length) * - (Table_Type'Component_Size / Storage_Unit); - - -- If the size of the table exceeds the release threshold then leave - -- space to store as many extra elements as 0.1% of the table length. - - if Release_Threshold > 0 - and then Size > Memory.size_t (Release_Threshold) - then - Extra_Length := Length / 1000; - Length := Length + Extra_Length; - Max := Int (Table_Low_Bound) + Length - 1; - - if Debug_Flag_D then - Write_Str ("--> Release_Threshold reached (length="); - Write_Int (Int (Size)); - Write_Str ("): leaving room space for "); - Write_Int (Extra_Length); - Write_Str (" components"); - Write_Eol; - end if; - else - Max := Last_Val; - end if; - - Reallocate; - end Release; - - ------------- - -- Restore -- - ------------- - - procedure Restore (T : Saved_Table) is - begin - Free (To_Address (Table)); - Last_Val := T.Last_Val; - Max := T.Max; - Table := T.Table; - Length := Max - Min + 1; - end Restore; - - ---------- - -- Save -- - ---------- - - function Save return Saved_Table is - Res : Saved_Table; - - begin - Res.Last_Val := Last_Val; - Res.Max := Max; - Res.Table := Table; - - Table := null; - Length := 0; - Init; - return Res; - end Save; - - -------------- - -- Set_Item -- - -------------- - - procedure Set_Item - (Index : Table_Index_Type; - Item : Table_Component_Type) - is - -- If Item is a value within the current allocation, and we are going - -- to reallocate, then we must preserve an intermediate copy here - -- before calling Increment_Last. Otherwise, if Table_Component_Type - -- is passed by reference, we are going to end up copying from - -- storage that might have been deallocated from Increment_Last - -- calling Reallocate. - - subtype Allocated_Table_T is - Table_Type (Table'First .. Table_Index_Type (Max + 1)); - -- A constrained table subtype one element larger than the currently - -- allocated table. - - Allocated_Table_Address : constant System.Address := - Table.all'Address; - -- Used for address clause below (we can't use non-static expression - -- Table.all'Address directly in the clause because some older - -- versions of the compiler do not allow it). - - Allocated_Table : Allocated_Table_T; - pragma Import (Ada, Allocated_Table); - pragma Suppress (Range_Check, On => Allocated_Table); - for Allocated_Table'Address use Allocated_Table_Address; - -- Allocated_Table represents the currently allocated array, plus one - -- element (the supplementary element is used to have a convenient - -- way of computing the address just past the end of the current - -- allocation). Range checks are suppressed because this unit - -- uses direct calls to System.Memory for allocation, and this can - -- yield misaligned storage (and we cannot rely on the bootstrap - -- compiler supporting specifically disabling alignment checks, so we - -- need to suppress all range checks). It is safe to suppress this - -- check here because we know that a (possibly misaligned) object - -- of that type does actually exist at that address. - -- ??? We should really improve the allocation circuitry here to - -- guarantee proper alignment. - - Need_Realloc : constant Boolean := Int (Index) > Max; - -- True if this operation requires storage reallocation (which may - -- involve moving table contents around). - - begin - -- If we're going to reallocate, check whether Item references an - -- element of the currently allocated table. - - if Need_Realloc - and then Allocated_Table'Address <= Item'Address - and then Item'Address < - Allocated_Table (Table_Index_Type (Max + 1))'Address - then - -- If so, save a copy on the stack because Increment_Last will - -- reallocate storage and might deallocate the current table. - - declare - Item_Copy : constant Table_Component_Type := Item; - begin - Set_Last (Index); - Table (Index) := Item_Copy; - end; - - else - -- Here we know that either we won't reallocate (case of Index < - -- Max) or that Item is not in the currently allocated table. - - if Int (Index) > Last_Val then - Set_Last (Index); - end if; - - Table (Index) := Item; - end if; - end Set_Item; - - -------------- - -- Set_Last -- - -------------- - - procedure Set_Last (New_Val : Table_Index_Type) is - begin - if Int (New_Val) < Last_Val then - Last_Val := Int (New_Val); - - else - Last_Val := Int (New_Val); - - if Last_Val > Max then - Reallocate; - end if; - end if; - end Set_Last; - ---------------------------- -- Tree_Get_Table_Address -- ---------------------------- function Tree_Get_Table_Address return Address is begin - if Length = 0 then + if Is_Empty then return Null_Address; else return Table (First)'Address; @@ -418,15 +65,15 @@ package body Table is -- does an implicit Release. procedure Tree_Read is + Last : Int; begin - Tree_Read_Int (Max); - Last_Val := Max; - Length := Max - Min + 1; - Reallocate; + Init; + Tree_Read_Int (Last); + Set_Last (Table_Last_Type (Last)); Tree_Read_Data (Tree_Get_Table_Address, - (Last_Val - Int (First) + 1) * + (Last - Int (First) + 1) * -- Note the importance of parenthesizing the following division -- to avoid the possibility of intermediate overflow. @@ -446,11 +93,9 @@ package body Table is Tree_Write_Int (Int (Last)); Tree_Write_Data (Tree_Get_Table_Address, - (Last_Val - Int (First) + 1) * + (Int (Last - First) + 1) * (Table_Type'Component_Size / Storage_Unit)); end Tree_Write; - begin - Init; end Table; end Table; diff --git a/gcc/ada/table.ads b/gcc/ada/table.ads index 29b6fb009bf..70626655492 100644 --- a/gcc/ada/table.ads +++ b/gcc/ada/table.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -29,16 +29,20 @@ -- -- ------------------------------------------------------------------------------ --- This package provides an implementation of dynamically resizable one --- dimensional arrays. The idea is to mimic the normal Ada semantics for --- arrays as closely as possible with the one additional capability of --- dynamically modifying the value of the Last attribute. +-- This package is a wrapper for GNAT.Table, for use in the compiler front +-- end. It adds the Tree_Write/Tree_Read functionality; everything else is +-- just a renaming of GNAT.Table. See GNAT.Table (g-table.ads) and +-- GNAT.Dynamic_Tables (g-dyntab.ads) for documentation. --- Note that this interface should remain synchronized with those in --- GNAT.Table and GNAT.Dynamic_Tables to keep coherency between these --- three related units. +-- Note that these three interfaces should remain synchronized to keep as much +-- coherency as possible among these related units: +-- +-- GNAT.Dynamic_Tables +-- GNAT.Table +-- Table (the compiler unit) with Types; use Types; +with GNAT.Table; package Table is pragma Elaborate_Body; @@ -50,83 +54,30 @@ package Table is Table_Low_Bound : Table_Index_Type; Table_Initial : Pos; Table_Increment : Nat; - Table_Name : String; + Table_Name : String; -- for debugging printouts Release_Threshold : Nat := 0; package Table is - -- Table_Component_Type and Table_Index_Type specify the type of the - -- array, Table_Low_Bound is the lower bound. Table_Index_Type must be - -- an integer type. The effect is roughly to declare: - - -- Table : array (Table_Index_Type range Table_Low_Bound .. <>) - -- of Table_Component_Type; - - -- Note: since the upper bound can be one less than the lower - -- bound for an empty array, the table index type must be able - -- to cover this range, e.g. if the lower bound is 1, then the - -- Table_Index_Type should be Natural rather than Positive. - - -- Table_Component_Type may be any Ada type, except that controlled - -- types are not supported. Note however that default initialization - -- will NOT occur for array components. - - -- The Table_Initial values controls the allocation of the table when - -- it is first allocated, either by default, or by an explicit Init - -- call. The value used is Opt.Table_Factor * Table_Initial. - - -- The Table_Increment value controls the amount of increase, if the - -- table has to be increased in size. The value given is a percentage - -- value (e.g. 100 = increase table size by 100%, i.e. double it). - - -- The Table_Name parameter is simply use in debug output messages it - -- has no other usage, and is not referenced in non-debugging mode. - - -- The Last and Set_Last subprograms provide control over the current - -- logical allocation. They are quite efficient, so they can be used - -- freely (expensive reallocation occurs only at major granularity - -- chunks controlled by the allocation parameters). - - -- Note: We do not make the table components aliased, since this would - -- restrict the use of table for discriminated types. If it is necessary - -- to take the access of a table element, use Unrestricted_Access. - - -- WARNING: On HPPA, the virtual addressing approach used in this unit - -- is incompatible with the indexing instructions on the HPPA. So when - -- using this unit, compile your application with -mdisable-indexing. - - -- WARNING: If the table is reallocated, then the address of all its - -- components will change. So do not capture the address of an element - -- and then use the address later after the table may be reallocated. - -- One tricky case of this is passing an element of the table to a - -- subprogram by reference where the table gets reallocated during - -- the execution of the subprogram. The best rule to follow is never - -- to pass a table element as a parameter except for the case of IN - -- mode parameters with scalar values. - - type Table_Type is - array (Table_Index_Type range <>) of Table_Component_Type; - - subtype Big_Table_Type is - Table_Type (Table_Low_Bound .. Table_Index_Type'Last); - -- We work with pointers to a bogus array type that is constrained - -- with the maximum possible range bound. This means that the pointer - -- is a thin pointer, which is more efficient. Since subscript checks - -- in any case must be on the logical, rather than physical bounds, - -- safety is not compromised by this approach. - - type Table_Ptr is access all Big_Table_Type; - for Table_Ptr'Storage_Size use 0; - -- The table is actually represented as a pointer to allow reallocation - - Table : aliased Table_Ptr := null; - -- The table itself. The lower bound is the value of Low_Bound. - -- Logically the upper bound is the current value of Last (although - -- the actual size of the allocated table may be larger than this). - -- The program may only access and modify Table entries in the range - -- First .. Last. - - Locked : Boolean := False; + package Tab is new GNAT.Table + (Table_Component_Type, + Table_Index_Type, + Table_Low_Bound, + Positive (Table_Initial), + Natural (Table_Increment), + Table_Name, + Natural (Release_Threshold)); + + subtype Valid_Table_Index_Type is Tab.Valid_Table_Index_Type; + subtype Table_Last_Type is Tab.Table_Last_Type; + subtype Table_Type is Tab.Table_Type; + subtype Big_Table_Type is Tab.Big_Table_Type; + + subtype Table_Ptr is Tab.Table_Ptr; + + Table : Table_Ptr renames Tab.Table; + + Locked : Boolean renames Tab.Locked; -- Table expansion is permitted only if this switch is set to False. A -- client may set Locked to True, in which case any attempt to expand -- the table will cause an assertion failure. Note that while a table @@ -136,110 +87,39 @@ package Table is -- not move during processing, which means that they cannot be expanded. -- The Locked flag is used to enforce this restriction. - procedure Init; - -- This procedure allocates a new table of size Initial (freeing any - -- previously allocated larger table). It is not necessary to call - -- Init when a table is first instantiated (since the instantiation does - -- the same initialization steps). However, it is harmless to do so, and - -- Init is convenient in reestablishing a table for new use. - - function Last return Table_Index_Type; - pragma Inline (Last); - -- Returns the current value of the last used entry in the table, which - -- can then be used as a subscript for Table. Note that the only way to - -- modify Last is to call the Set_Last procedure. Last must always be - -- used to determine the logically last entry. - - procedure Release; - -- Storage is allocated in chunks according to the values given in the - -- Initial and Increment parameters. If Release_Threshold is 0 or the - -- length of the table does not exceed this threshold then a call to - -- Release releases all storage that is allocated, but is not logically - -- part of the current array value; otherwise the call to Release leaves - -- the current array value plus 0.1% of the current table length free - -- elements located at the end of the table (this parameter facilitates - -- reopening large tables and adding a few elements without allocating a - -- chunk of memory). In both cases current array values are not affected - -- by this call. - - procedure Free; - -- Free all allocated memory for the table. A call to init is required - -- before any use of this table after calling Free. - - First : constant Table_Index_Type := Table_Low_Bound; - -- Export First as synonym for Low_Bound (parallel with use of Last) - - procedure Set_Last (New_Val : Table_Index_Type); - pragma Inline (Set_Last); - -- This procedure sets Last to the indicated value. If necessary the - -- table is reallocated to accommodate the new value (i.e. on return - -- the allocated table has an upper bound of at least Last). If Set_Last - -- reduces the size of the table, then logically entries are removed - -- from the table. If Set_Last increases the size of the table, then - -- new entries are logically added to the table. - - procedure Increment_Last; - pragma Inline (Increment_Last); - -- Adds 1 to Last (same as Set_Last (Last + 1) - - procedure Decrement_Last; - pragma Inline (Decrement_Last); - -- Subtracts 1 from Last (same as Set_Last (Last - 1) - - procedure Append (New_Val : Table_Component_Type); - pragma Inline (Append); - -- Equivalent to: - -- x.Increment_Last; - -- x.Table (x.Last) := New_Val; - -- i.e. the table size is increased by one, and the given new item - -- stored in the newly created table element. - - procedure Append_All (New_Vals : Table_Type); - -- Appends all components of New_Vals + function Is_Empty return Boolean renames Tab.Is_Empty; - procedure Set_Item - (Index : Table_Index_Type; - Item : Table_Component_Type); - pragma Inline (Set_Item); - -- Put Item in the table at position Index. The table is expanded if - -- current table length is less than Index and in that case Last is set - -- to Index. Item will replace any value already present in the table - -- at this position. + procedure Init renames Tab.Init; - type Saved_Table is private; - -- Type used for Save/Restore subprograms + function First return Table_Index_Type renames Tab.First; + function Last return Table_Last_Type renames Tab.Last; - function Save return Saved_Table; - -- Resets table to empty, but saves old contents of table in returned - -- value, for possible later restoration by a call to Restore. + procedure Release renames Tab.Release; - procedure Restore (T : Saved_Table); - -- Given a Saved_Table value returned by a prior call to Save, restores - -- the table to the state it was in at the time of the Save call. + procedure Free renames Tab.Free; - procedure Tree_Write; - -- Writes out contents of table using Tree_IO + procedure Set_Last (New_Val : Table_Last_Type) renames Tab.Set_Last; - procedure Tree_Read; - -- Initializes table by reading contents previously written with the - -- Tree_Write call (also using Tree_IO). + procedure Increment_Last renames Tab.Increment_Last; + procedure Decrement_Last renames Tab.Decrement_Last; - private + procedure Append (New_Val : Table_Component_Type) renames Tab.Append; + procedure Append_All (New_Vals : Table_Type) renames Tab.Append_All; - Last_Val : Int; - -- Current value of Last. Note that we declare this in the private part - -- because we don't want the client to modify Last except through one of - -- the official interfaces (since a modification to Last may require a - -- reallocation of the table). + procedure Set_Item + (Index : Valid_Table_Index_Type; + Item : Table_Component_Type) renames Tab.Set_Item; - Max : Int; - -- Subscript of the maximum entry in the currently allocated table + subtype Saved_Table is Tab.Saved_Table; + function Save return Saved_Table renames Tab.Save; + procedure Restore (T : in out Saved_Table) renames Tab.Restore; - type Saved_Table is record - Last_Val : Int; - Max : Int; - Table : Table_Ptr; - end record; + procedure Tree_Write; + -- Writes out contents of table using Tree_IO + + procedure Tree_Read; + -- Initializes table by reading contents previously written with the + -- Tree_Write call, also using Tree_IO. end Table; end Table; diff --git a/gcc/ada/uintp.h b/gcc/ada/uintp.h index fafa13903b8..5263b1ba822 100644 --- a/gcc/ada/uintp.h +++ b/gcc/ada/uintp.h @@ -6,7 +6,7 @@ * * * C Header File * * * - * Copyright (C) 1992-2016, Free Software Foundation, Inc. * + * Copyright (C) 1992-2017, Free Software Foundation, Inc. * * * * GNAT is free software; you can redistribute it and/or modify it under * * terms of the GNU General Public License as published by the Free Soft- * @@ -101,11 +101,11 @@ extern Boolean UI_Lt (Uint, Uint); the integer value itself. The origin of the Uints_Ptr table is adjusted so that a Uint value of Uint_Bias indexes the first element. */ -#define Uints_Ptr (uintp__uints__table - Uint_Table_Start) -extern struct Uint_Entry *uintp__uints__table; +#define Uints_Ptr (uintp__uints__tab__the_instance - Uint_Table_Start) +extern struct Uint_Entry *uintp__uints__tab__the_instance; -#define Udigits_Ptr uintp__udigits__table -extern int *uintp__udigits__table; +#define Udigits_Ptr uintp__udigits__tab__the_instance +extern int *uintp__udigits__tab__the_instance; #ifdef __cplusplus } diff --git a/gcc/ada/xoscons.adb b/gcc/ada/xoscons.adb index 8eecb298f36..39a39f3b79a 100644 --- a/gcc/ada/xoscons.adb +++ b/gcc/ada/xoscons.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2008-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2008-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -26,7 +26,7 @@ -- The base name of the template file is given by Argument (1). This program -- generates the spec for this specified unit (let's call it UNIT_NAME). --- It works in conjunction with a C template file which must be pre-processed +-- It works in conjunction with a C template file which must be preprocessed -- and compiled using the cross compiler. Two input files are used: -- - the preprocessed C file: UNIT_NAME-tmplt.i -- - the generated assembly file: UNIT_NAME-tmplt.s