Merge branch 'autopar_rebase2' into autopar_develdevel/autopar_devel

Quickly commit changes in the rebase branch.

1 files changed, 216 insertions, 113 deletions

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 28484aa..b400268 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2019, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2020, 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- --
@@ -36,7 +36,6 @@ with Nlists;   use Nlists;
 with Nmake;    use Nmake;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
-with Sem_Eval; use Sem_Eval;
 with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
@@ -53,14 +52,16 @@ package body Exp_SPARK is
    -----------------------
 
    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
-   --  Replace occurrences of System'To_Address by calls to
-   --  System.Storage_Elements.To_Address
+   --  Perform attribute-reference-specific expansion
+
+   procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
+   --  Perform delta-aggregate-specific expansion
 
    procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
    --  Build the DIC procedure of a type when needed, if not already done
 
    procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
-   --  Perform loop statement-specific expansion
+   --  Perform loop-statement-specific expansion
 
    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
    --  Perform object-declaration-specific expansion
@@ -71,11 +72,8 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
    --  Rewrite operator /= based on operator = when defined explicitly
 
-   procedure Expand_SPARK_N_Selected_Component (N : Node_Id);
-   --  Insert explicit dereference if required
-
-   procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id);
-   --  Insert explicit dereference if required
+   procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
+   --  Common expansion for attribute Update and delta aggregates
 
    ------------------
    -- Expand_SPARK --
@@ -109,6 +107,9 @@ package body Exp_SPARK is
          when N_Attribute_Reference =>
             Expand_SPARK_N_Attribute_Reference (N);
 
+         when N_Delta_Aggregate =>
+            Expand_SPARK_N_Delta_Aggregate (N);
+
          when N_Expanded_Name
             | N_Identifier
          =>
@@ -138,14 +139,6 @@ package body Exp_SPARK is
                Expand_SPARK_N_Freeze_Type (Entity (N));
             end if;
 
-         when N_Indexed_Component
-            | N_Slice
-         =>
-            Expand_SPARK_N_Slice_Or_Indexed_Component (N);
-
-         when N_Selected_Component =>
-            Expand_SPARK_N_Selected_Component (N);
-
          --  In SPARK mode, no other constructs require expansion
 
          when others =>
@@ -153,6 +146,185 @@ package body Exp_SPARK is
       end case;
    end Expand_SPARK;
 
+   ----------------------------------
+   -- Expand_SPARK_Delta_Or_Update --
+   ----------------------------------
+
+   procedure Expand_SPARK_Delta_Or_Update
+     (Typ  : Entity_Id;
+      Aggr : Node_Id)
+   is
+      Assoc     : Node_Id;
+      Comp      : Node_Id;
+      Comp_Id   : Entity_Id;
+      Comp_Type : Entity_Id;
+      Expr      : Node_Id;
+      Index     : Node_Id;
+      Index_Typ : Entity_Id;
+      New_Assoc : Node_Id;
+
+   begin
+      --  Apply scalar range checks on the updated components, if needed
+
+      if Is_Array_Type (Typ) then
+
+         --  Multidimensional arrays
+
+         if Present (Next_Index (First_Index (Typ))) then
+            Assoc := First (Component_Associations (Aggr));
+
+            while Present (Assoc) loop
+               Expr      := Expression (Assoc);
+               Comp_Type := Component_Type (Typ);
+
+               if Is_Scalar_Type (Comp_Type) then
+                  Apply_Scalar_Range_Check (Expr, Comp_Type);
+               end if;
+
+               --  The current association contains a sequence of indexes
+               --  denoting an element of a multidimensional array:
+               --
+               --    (Index_1, ..., Index_N)
+
+               Expr := First (Choices (Assoc));
+
+               pragma Assert (Nkind (Aggr) = N_Aggregate);
+
+               while Present (Expr) loop
+                  Index     := First (Expressions (Expr));
+                  Index_Typ := First_Index (Typ);
+
+                  while Present (Index_Typ) loop
+                     Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+                     Next (Index);
+                     Next_Index (Index_Typ);
+                  end loop;
+
+                  Next (Expr);
+               end loop;
+
+               Next (Assoc);
+            end loop;
+
+         --  One-dimensional arrays
+
+         else
+            Assoc := First (Component_Associations (Aggr));
+
+            while Present (Assoc) loop
+               Expr      := Expression (Assoc);
+               Comp_Type := Component_Type (Typ);
+
+               if Is_Scalar_Type (Comp_Type) then
+                  Apply_Scalar_Range_Check (Expr, Comp_Type);
+               end if;
+
+               Index     := First (Choices (Assoc));
+               Index_Typ := First_Index (Typ);
+
+               while Present (Index) loop
+                  --  The index denotes a range of elements
+
+                  if Nkind (Index) = N_Range then
+                     Apply_Scalar_Range_Check
+                       (Low_Bound  (Index), Base_Type (Etype (Index_Typ)));
+                     Apply_Scalar_Range_Check
+                       (High_Bound (Index), Base_Type (Etype (Index_Typ)));
+
+                  --  Otherwise the index denotes a single element
+
+                  else
+                     Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+                  end if;
+
+                  Next (Index);
+               end loop;
+
+               Next (Assoc);
+            end loop;
+         end if;
+
+      else pragma Assert (Is_Record_Type (Typ));
+
+         --  If the aggregate has multiple component choices, e.g.:
+         --
+         --    X'Update (A | B | C => 123)
+         --
+         --  then each component might be of a different type and might or
+         --  might not require a range check. We first rewrite associations
+         --  into single-component choices, e.g.:
+         --
+         --    X'Update (A => 123, B => 123, C => 123)
+         --
+         --  and then apply range checks to individual copies of the
+         --  expressions. We do the same for delta aggregates, accordingly.
+
+         --  Iterate over associations of the original aggregate
+
+         Assoc := First (Component_Associations (Aggr));
+
+         --  Rewrite into a new aggregate and decorate
+
+         case Nkind (Aggr) is
+            when N_Aggregate =>
+               Rewrite
+                 (Aggr,
+                  Make_Aggregate
+                    (Sloc                   => Sloc (Aggr),
+                     Component_Associations => New_List));
+
+            when N_Delta_Aggregate =>
+               Rewrite
+                 (Aggr,
+                  Make_Delta_Aggregate
+                    (Sloc                   => Sloc (Aggr),
+                     Expression             => Expression (Aggr),
+                     Component_Associations => New_List));
+
+            when others =>
+               raise Program_Error;
+         end case;
+
+         Set_Etype (Aggr, Typ);
+
+         --  Populate the new aggregate with component associations
+
+         while Present (Assoc) loop
+            Expr := Expression (Assoc);
+            Comp := First (Choices (Assoc));
+
+            while Present (Comp) loop
+               Comp_Id   := Entity (Comp);
+               Comp_Type := Etype (Comp_Id);
+
+               New_Assoc :=
+                 Make_Component_Association
+                   (Sloc       => Sloc (Assoc),
+                    Choices    =>
+                      New_List
+                        (New_Occurrence_Of (Comp_Id, Sloc (Comp))),
+                    Expression => New_Copy_Tree (Expr));
+
+               --  New association must be attached to the aggregate before we
+               --  analyze it.
+
+               Append (New_Assoc, Component_Associations (Aggr));
+
+               Analyze_And_Resolve (Expression (New_Assoc), Comp_Type);
+
+               if Is_Scalar_Type (Comp_Type) then
+                  Apply_Scalar_Range_Check
+                    (Expression (New_Assoc), Comp_Type);
+               end if;
+
+               Next (Comp);
+            end loop;
+
+            Next (Assoc);
+         end loop;
+      end if;
+   end Expand_SPARK_Delta_Or_Update;
+
    --------------------------------
    -- Expand_SPARK_N_Freeze_Type --
    --------------------------------
@@ -200,36 +372,6 @@ package body Exp_SPARK is
              Parameter_Associations => New_List (Expr)));
          Analyze_And_Resolve (N, Typ);
 
-      --  Whenever possible, replace a prefix which is an enumeration literal
-      --  by the corresponding literal value.
-
-      elsif Attr_Id = Attribute_Enum_Rep then
-         declare
-            Exprs : constant List_Id := Expressions (N);
-         begin
-            if Is_Non_Empty_List (Exprs) then
-               Expr := First (Exprs);
-            else
-               Expr := Prefix (N);
-            end if;
-
-            --  If the argument is a literal, expand it
-
-            if Nkind (Expr) in N_Has_Entity
-              and then
-                (Ekind (Entity (Expr)) = E_Enumeration_Literal
-                 or else
-                   (Nkind (Expr) in N_Has_Entity
-                    and then Ekind (Entity (Expr)) = E_Constant
-                    and then Present (Renamed_Object (Entity (Expr)))
-                    and then Is_Entity_Name (Renamed_Object (Entity (Expr)))
-                    and then Ekind (Entity (Renamed_Object (Entity (Expr)))) =
-                      E_Enumeration_Literal))
-            then
-               Exp_Attr.Expand_N_Attribute_Reference (N);
-            end if;
-         end;
-
       elsif Attr_Id = Attribute_Object_Size
         or else Attr_Id = Attribute_Size
         or else Attr_Id = Attribute_Value_Size
@@ -258,41 +400,23 @@ package body Exp_SPARK is
          --  flag as the compiler assumes attributes always fit in this type.
          --  Since in SPARK_Mode we do not take Storage_Error into account, we
          --  cannot make this assumption and need to produce a check.
-         --  ??? It should be enough to add this check for attributes 'Length
-         --  and 'Range_Length when the type is as big as Long_Long_Integer.
+         --  ??? It should be enough to add this check for attributes
+         --  'Length, 'Range_Length and 'Pos when the type is as big
+         --  as Long_Long_Integer.
 
          declare
-            Typ : Entity_Id := Empty;
+            Typ : Entity_Id;
          begin
-            if Attr_Id = Attribute_Range_Length then
+            if Attr_Id = Attribute_Range_Length
+              or else Attr_Id = Attribute_Pos
+            then
                Typ := Etype (Prefix (N));
 
             elsif Attr_Id = Attribute_Length then
-               Typ := Etype (Prefix (N));
-
-               declare
-                  Indx : Node_Id;
-                  J    : Int;
-
-               begin
-                  if Is_Access_Type (Typ) then
-                     Typ := Designated_Type (Typ);
-                  end if;
-
-                  if No (Expressions (N)) then
-                     J := 1;
-                  else
-                     J := UI_To_Int (Expr_Value (First (Expressions (N))));
-                  end if;
-
-                  Indx := First_Index (Typ);
-                  while J > 1 loop
-                     Next_Index (Indx);
-                     J := J - 1;
-                  end loop;
+               Typ := Get_Index_Subtype (N);
 
-                  Typ := Etype (Indx);
-               end;
+            else
+               Typ := Empty;
             end if;
 
             Apply_Universal_Integer_Attribute_Checks (N);
@@ -300,6 +424,9 @@ package body Exp_SPARK is
             if Present (Typ)
               and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
             then
+               --  ??? This should rather be a range check, but this would
+               --  crash GNATprove which somehow recovers the proper kind
+               --  of check anyway.
                Set_Do_Overflow_Check (N);
             end if;
          end;
@@ -317,9 +444,21 @@ package body Exp_SPARK is
                      Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
             Analyze_And_Resolve (N, Standard_Boolean);
          end if;
+
+      elsif Attr_Id = Attribute_Update then
+         Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
       end if;
    end Expand_SPARK_N_Attribute_Reference;
 
+   ------------------------------------
+   -- Expand_SPARK_N_Delta_Aggregate --
+   ------------------------------------
+
+   procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is
+   begin
+      Expand_SPARK_Delta_Or_Update (Etype (N), N);
+   end Expand_SPARK_N_Delta_Aggregate;
+
    -----------------------------------
    -- Expand_SPARK_N_Loop_Statement --
    -----------------------------------
@@ -500,7 +639,7 @@ package body Exp_SPARK is
    begin
       --  Replace a reference to a renaming with the actual renamed object
 
-      if Ekind (Obj_Id) in Object_Kind then
+      if Is_Object (Obj_Id) then
          Ren := Renamed_Object (Obj_Id);
 
          if Present (Ren) then
@@ -533,40 +672,4 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Potential_Renaming;
 
-   ---------------------------------------
-   -- Expand_SPARK_N_Selected_Component --
-   ---------------------------------------
-
-   procedure Expand_SPARK_N_Selected_Component (N : Node_Id) is
-      Pref : constant Node_Id   := Prefix (N);
-      Typ  : constant Entity_Id := Underlying_Type (Etype (Pref));
-
-   begin
-      if Present (Typ) and then Is_Access_Type (Typ) then
-
-         --  First set prefix type to proper access type, in case it currently
-         --  has a private (non-access) view of this type.
-
-         Set_Etype (Pref, Typ);
-
-         Insert_Explicit_Dereference (Pref);
-         Analyze_And_Resolve (Pref, Designated_Type (Typ));
-      end if;
-   end Expand_SPARK_N_Selected_Component;
-
-   -----------------------------------------------
-   -- Expand_SPARK_N_Slice_Or_Indexed_Component --
-   -----------------------------------------------
-
-   procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id) is
-      Pref : constant Node_Id   := Prefix (N);
-      Typ  : constant Entity_Id := Etype (Pref);
-
-   begin
-      if Is_Access_Type (Typ) then
-         Insert_Explicit_Dereference (Pref);
-         Analyze_And_Resolve (Pref, Designated_Type (Typ));
-      end if;
-   end Expand_SPARK_N_Slice_Or_Indexed_Component;
-
 end Exp_SPARK;