+2016-04-18 Bob Duff <duff@adacore.com>
+
+ * a-cuprqu.ads: Change the representation of List_Type from a
+ singly-linked list to a doubly-linked list. In addition, add a
+ pointer Next_Unequal, which points past a possibly-long chain
+ of equal-priority items. This increases efficiency, especially
+ in the case of many equal-priority items.
+ * a-cuprqu.adb (Dequeue, Enqueue): Rewrite algorithms to take
+ advantage of new data structure.
+ (Finalize): Rewrite in terms of Dequeue, for simplicity.
+
+2016-04-18 Yannick Moy <moy@adacore.com>
+
+ * contracts.adb (Analyze_Object_Contract,
+ Analyze_Protected_Contract): Remove tests performed in GNATprove.
+ * sem_util.adb, sem_util.ads (Has_Full_Default_Initialization):
+ Remove query for tests performed in GNATprove.
+
2016-04-18 Ed Schonberg <schonberg@adacore.com>
* sem_aggr.adb (Resolve_Record_Aggregate): If
-- Local Subprograms --
-----------------------
+ function Before_Or_Equal (X, Y : Queue_Priority) return Boolean;
+ -- True if X is before or equal to Y. Equal means both Before(X,Y) and
+ -- Before(Y,X) are False.
+
procedure Free is
- new Ada.Unchecked_Deallocation (Node_Type, Node_Access);
+ new Ada.Unchecked_Deallocation (Node_Type, Node_Access);
+
+ ---------------------
+ -- Before_Or_Equal --
+ ---------------------
+
+ function Before_Or_Equal (X, Y : Queue_Priority) return Boolean is
+ begin
+ return (if Before (X, Y) then True else not Before (Y, X));
+ end Before_Or_Equal;
-------------
-- Dequeue --
(List : in out List_Type;
Element : out Queue_Interfaces.Element_Type)
is
- X : Node_Access;
+ H : constant Node_Access := List.Header'Unchecked_Access;
+ pragma Assert (List.Length /= 0);
+ pragma Assert (List.Header.Next /= H);
+ -- List can't be empty; see the barrier
- begin
- Element := List.First.Element;
+ pragma Assert
+ (List.Header.Next.Next = H or else
+ Before_Or_Equal (Get_Priority (List.Header.Next.Element),
+ Get_Priority (List.Header.Next.Next.Element)));
+ -- The first item is before-or-equal to the second
- X := List.First;
- List.First := List.First.Next;
+ pragma Assert
+ (List.Header.Next.Next_Unequal = H or else
+ Before (Get_Priority (List.Header.Next.Element),
+ Get_Priority (List.Header.Next.Next_Unequal.Element)));
+ -- The first item is before its Next_Unequal item
- if List.First = null then
- List.Last := null;
- end if;
+ -- The highest-priority item is always first; just remove it and
+ -- return that element.
- List.Length := List.Length - 1;
+ X : Node_Access := List.Header.Next;
+
+ -- Start of processing for Dequeue
+ begin
+ Element := X.Element;
+ X.Next.Prev := H;
+ List.Header.Next := X.Next;
+ List.Header.Next_Unequal := X.Next;
+ List.Length := List.Length - 1;
Free (X);
end Dequeue;
-- dequeue an item. If it's false, it means no item is dequeued, and
-- we return False as the Success value.
- if List.Length = 0
- or else Before (At_Least, Get_Priority (List.First.Element))
- then
- Success := False;
- return;
- end if;
+ Success := List.Length > 0
+ and then
+ not Before (At_Least, Get_Priority (List.Header.Next.Element));
- List.Dequeue (Element);
- Success := True;
+ if Success then
+ List.Dequeue (Element);
+ end if;
end Dequeue;
-------------
New_Item : Queue_Interfaces.Element_Type)
is
P : constant Queue_Priority := Get_Priority (New_Item);
+ H : constant Node_Access := List.Header'Unchecked_Access;
+
+ function Next return Node_Access;
+ -- The node before which we wish to insert the new node
+
+ ----------
+ -- Next --
+ ----------
+
+ function Next return Node_Access is
+ begin
+ return Result : Node_Access := H.Next_Unequal do
+ while Result /= H
+ and then not Before (P, Get_Priority (Result.Element))
+ loop
+ Result := Result.Next_Unequal;
+ end loop;
+ end return;
+ end Next;
- Node : Node_Access;
- Prev : Node_Access;
-
- begin
- Node := new Node_Type'(New_Item, null);
-
- if List.First = null then
- List.First := Node;
- List.Last := List.First;
+ -- Local varaibles
- else
- Prev := List.First;
+ Prev : constant Node_Access := Next.Prev;
+ -- The node after which we wish to insert the new node. So Prev must
+ -- be the header, or be higher or equal priority to the new item.
+ -- Prev.Next must be the header, or be lower priority than the
+ -- new item.
- if Before (P, Get_Priority (Prev.Element)) then
- Node.Next := List.First;
- List.First := Node;
+ pragma Assert
+ (Prev = H or else Before_Or_Equal (Get_Priority (Prev.Element), P));
+ pragma Assert
+ (Prev.Next = H
+ or else Before (P, Get_Priority (Prev.Next.Element)));
+ pragma Assert (Prev.Next = Prev.Next_Unequal);
- else
- while Prev.Next /= null loop
- if Before (P, Get_Priority (Prev.Next.Element)) then
- Node.Next := Prev.Next;
- Prev.Next := Node;
+ Node : constant Node_Access :=
+ new Node_Type'(New_Item,
+ Prev => Prev,
+ Next => Prev.Next,
+ Next_Unequal => Prev.Next);
- exit;
- end if;
+ -- Start of processing for Enqueue
- Prev := Prev.Next;
- end loop;
+ begin
+ Prev.Next.Prev := Node;
+ Prev.Next := Node;
- if Prev.Next = null then
- List.Last.Next := Node;
- List.Last := Node;
- end if;
- end if;
+ if List.Length = 0 then
+ List.Header.Next_Unequal := Node;
end if;
List.Length := List.Length + 1;
--------------
procedure Finalize (List : in out List_Type) is
- X : Node_Access;
+ Ignore : Queue_Interfaces.Element_Type;
begin
- while List.First /= null loop
- X := List.First;
- List.First := List.First.Next;
- Free (X);
+ while List.Length > 0 loop
+ List.Dequeue (Ignore);
end loop;
end Finalize;
private
+ -- List_Type is implemented as a circular doubly-linked list with a
+ -- dummy header node; Prev and Next are the links. The list is in
+ -- decreasing priority order, so the highest-priority item is always
+ -- first. (If there are multiple items with the highest priority, the
+ -- oldest one is first.) Header.Element is undefined and not used.
+ --
+ -- In addition, Next_Unequal points to the next item with a different
+ -- (i.e. strictly lower) priority. This is used to speed up the search
+ -- for the next lower-priority item, in cases where there are many items
+ -- with the same priority.
+ --
+ -- An empty list has Header.Prev, Header.Next, and Header.Next_Unequal
+ -- all pointing to Header. A nonempty list has Header.Next_Unequal
+ -- pointing to the first "real" item, and the last item has Next_Unequal
+ -- pointing back to Header.
+
type Node_Type;
- type Node_Access is access Node_Type;
+ type Node_Access is access all Node_Type;
type Node_Type is limited record
- Element : Queue_Interfaces.Element_Type;
- Next : Node_Access;
+ Element : Queue_Interfaces.Element_Type;
+ Prev, Next : Node_Access := Node_Type'Unchecked_Access;
+ Next_Unequal : Node_Access := Node_Type'Unchecked_Access;
end record;
type List_Type is new Ada.Finalization.Limited_Controlled with record
- First, Last : Node_Access;
- Length : Count_Type := 0;
- Max_Length : Count_Type := 0;
+ Header : aliased Node_Type;
+ Length : Count_Type := 0;
+ Max_Length : Count_Type := 0;
end record;
overriding procedure Finalize (List : in out List_Type);
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
AR_Val : Boolean := False;
AW_Val : Boolean := False;
- Encap_Id : Entity_Id;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
Items : Node_Id;
Obj_Id);
end if;
end if;
-
- -- A variable whose Part_Of pragma specifies a single concurrent
- -- type as encapsulator must be (SPARK RM 9.4):
- -- * Of a type that defines full default initialization, or
- -- * Declared with a default value, or
- -- * Imported
-
- Encap_Id := Encapsulating_State (Obj_Id);
-
- if Present (Encap_Id)
- and then Is_Single_Concurrent_Object (Encap_Id)
- and then not Has_Full_Default_Initialization (Etype (Obj_Id))
- and then not Has_Initial_Value (Obj_Id)
- and then not Is_Imported (Obj_Id)
- then
- Error_Msg_N ("& requires full default initialization", Obj_Id);
-
- Error_Msg_Name_1 := Chars (Encap_Id);
- Error_Msg_N
- (Fix_Msg (Encap_Id, "\object acts as constituent of single "
- & "protected type %"), Obj_Id);
- end if;
end if;
end if;
procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
Items : constant Node_Id := Contract (Prot_Id);
- Mode : SPARK_Mode_Type;
begin
-- Do not analyze a contract multiple times
Set_Analyzed (Items);
end if;
end if;
-
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related protected unit.
-
- Save_SPARK_Mode_And_Set (Prot_Id, Mode);
-
- -- A protected type must define full default initialization
- -- (SPARK RM 9.4). This check is relevant only when SPARK_Mode is on as
- -- it is not a standard Ada legality rule.
-
- if SPARK_Mode = On
- and then not Has_Full_Default_Initialization (Prot_Id)
- then
- Error_Msg_N
- ("protected type & must define full default initialization",
- Prot_Id);
- end if;
-
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
-
- Restore_SPARK_Mode (Mode);
end Analyze_Protected_Contract;
-------------------------------------------
end if;
end Has_Enabled_Property;
- -------------------------------------
- -- Has_Full_Default_Initialization --
- -------------------------------------
-
- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
- Arg : Node_Id;
- Comp : Entity_Id;
- Prag : Node_Id;
-
- begin
- -- A private type and its full view is fully default initialized when it
- -- is subject to pragma Default_Initial_Condition without an argument or
- -- with a non-null argument. Since any type may act as the full view of
- -- a private type, this check must be performed prior to the specialized
- -- tests below.
-
- if Has_Default_Init_Cond (Typ)
- or else Has_Inherited_Default_Init_Cond (Typ)
- then
- Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-
- -- Pragma Default_Initial_Condition must be present if one of the
- -- related entity flags is set.
-
- pragma Assert (Present (Prag));
- Arg := First (Pragma_Argument_Associations (Prag));
-
- -- A non-null argument guarantees full default initialization
-
- if Present (Arg) then
- return Nkind (Arg) /= N_Null;
-
- -- Otherwise the missing argument defaults the pragma to "True" which
- -- is considered a non-null argument (see above).
-
- else
- return True;
- end if;
- end if;
-
- -- A scalar type is fully default initialized if it is subject to aspect
- -- Default_Value.
-
- if Is_Scalar_Type (Typ) then
- return Has_Default_Aspect (Typ);
-
- -- An array type is fully default initialized if its element type is
- -- scalar and the array type carries aspect Default_Component_Value or
- -- the element type is fully default initialized.
-
- elsif Is_Array_Type (Typ) then
- return
- Has_Default_Aspect (Typ)
- or else Has_Full_Default_Initialization (Component_Type (Typ));
-
- -- A protected type, record type or type extension is fully default
- -- initialized if all its components either carry an initialization
- -- expression or have a type that is fully default initialized. The
- -- parent type of a type extension must be fully default initialized.
-
- elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
-
- -- Inspect all entities defined in the scope of the type, looking for
- -- uninitialized components.
-
- Comp := First_Entity (Typ);
- while Present (Comp) loop
- if Ekind (Comp) = E_Component
- and then Comes_From_Source (Comp)
- and then No (Expression (Parent (Comp)))
- and then not Has_Full_Default_Initialization (Etype (Comp))
- then
- return False;
- end if;
-
- Next_Entity (Comp);
- end loop;
-
- -- Ensure that the parent type of a type extension is fully default
- -- initialized.
-
- if Etype (Typ) /= Typ
- and then not Has_Full_Default_Initialization (Etype (Typ))
- then
- return False;
- end if;
-
- -- If we get here, then all components and parent portion are fully
- -- default initialized.
-
- return True;
-
- -- A task type is fully default initialized by default
-
- elsif Is_Task_Type (Typ) then
- return True;
-
- -- Otherwise the type is not fully default initialized
-
- else
- return False;
- end if;
- end Has_Full_Default_Initialization;
-
--------------------
-- Has_Infinities --
--------------------
-- Determine whether subprogram Subp_Id has an effectively volatile formal
-- parameter or returns an effectively volatile value.
- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ defines "full default initialization" as
- -- specified by SPARK RM 3.1. To qualify as such, the type must be
- -- * A scalar type with specified Default_Value
- -- * An array-of-scalar type with specified Default_Component_Value
- -- * An array type whose element type defines full default initialization
- -- * A protected type, record type or type extension whose components
- -- either include a default expression or have a type which defines
- -- full default initialization. In the case of type extensions, the
- -- parent type defines full default initialization.
- -- * A task type
- -- * A private type whose Default_Initial_Condition is non-null
-
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.
projects / gcc.git / commitdiff