[multiple changes]

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.

From-SVN: r235121

6 files changed, 131 insertions, 222 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cea9413..fbdfabc 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,21 @@
+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
diff --git a/gcc/ada/a-cuprqu.adb b/gcc/ada/a-cuprqu.adb
index e694786..fb02f09 100644
--- a/gcc/ada/a-cuprqu.adb
+++ b/gcc/ada/a-cuprqu.adb
@@ -37,8 +37,21 @@ package body Ada.Containers.Unbounded_Priority_Queues is
       -- 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 --
@@ -48,20 +61,36 @@ package body Ada.Containers.Unbounded_Priority_Queues is
         (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;
 
@@ -93,15 +122,13 @@ package body Ada.Containers.Unbounded_Priority_Queues is
          --  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;
 
       -------------
@@ -113,41 +140,55 @@ package body Ada.Containers.Unbounded_Priority_Queues is
          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;
@@ -162,12 +203,10 @@ package body Ada.Containers.Unbounded_Priority_Queues is
       --------------
 
       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;
 
diff --git a/gcc/ada/a-cuprqu.ads b/gcc/ada/a-cuprqu.ads
index 4cc000d..1a23983 100644
--- a/gcc/ada/a-cuprqu.ads
+++ b/gcc/ada/a-cuprqu.ads
@@ -81,18 +81,35 @@ package Ada.Containers.Unbounded_Priority_Queues is
 
    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);
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 35a9fd0..f937b68 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -660,7 +660,6 @@ package body Contracts is
       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;
@@ -872,28 +871,6 @@ package body Contracts is
                      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;
 
@@ -1137,7 +1114,6 @@ package body Contracts is
 
    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
@@ -1149,30 +1125,6 @@ package body Contracts is
             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;
 
    -------------------------------------------
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 1146b9d..35b0888 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -9046,110 +9046,6 @@ package body Sem_Util is
       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 --
    --------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index d8a9b52..e868c83 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1034,19 +1034,6 @@ package Sem_Util is
    --  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.