[Ada] More precise handling of Size/Object_Size in GNATprove

GNATprove does a partial expansion which did not allow getting the
most precise value for attributes Size/Object_Size. Now fixed.

There is no impact on compilation.

2019-08-12  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* exp_attr.adb, exp_attr.ads (Expand_Size_Attribute): New
	procedure to share part of the attribute expansion with
	GNATprove mode.
	(Expand_N_Attribute_Reference): Extract part of the
	Size/Object_Size expansion in the new procedure
	Expand_Size_Attribute.
	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand
	Size/Object_Size attributes using the new procedure
	Expand_Size_Attribute.

From-SVN: r274290

gcc/ada/ChangeLog

 2019-08-12  Yannick Moy  <moy@adacore.com>
 
+	* exp_attr.adb, exp_attr.ads (Expand_Size_Attribute): New
+	procedure to share part of the attribute expansion with
+	GNATprove mode.
+	(Expand_N_Attribute_Reference): Extract part of the
+	Size/Object_Size expansion in the new procedure
+	Expand_Size_Attribute.
+	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Expand
+	Size/Object_Size attributes using the new procedure
+	Expand_Size_Attribute.
+
+2019-08-12  Yannick Moy  <moy@adacore.com>
+
 	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Only
 	expand Enum_Rep attribute when its parameter is a literal.
 

gcc/ada/exp_attr.adb

@@ -3598,8 +3598,8 @@ package body Exp_Attr is
       --    Result_Type (System.Fore (Universal_Real (Type'First)),
       --                              Universal_Real (Type'Last))
 
-      --  Note that we know that the type is a non-static subtype, or Fore
-      --  would have itself been computed dynamically in Eval_Attribute.
+      --  Note that we know that the type is a nonstatic subtype, or Fore would
+      --  have itself been computed dynamically in Eval_Attribute.
 
       when Attribute_Fore =>
          Rewrite (N,
@@ -5849,7 +5849,6 @@ package body Exp_Attr is
          | Attribute_VADS_Size
       =>
          Size : declare
-            Siz      : Uint;
             New_Node : Node_Id;
 
          begin
@@ -5961,128 +5960,12 @@ package body Exp_Attr is
                Rewrite (N, New_Node);
                Analyze_And_Resolve (N, Typ);
                return;
-
-            --  Case of known RM_Size of a type
-
-            elsif (Id = Attribute_Size or else Id = Attribute_Value_Size)
-              and then Is_Entity_Name (Pref)
-              and then Is_Type (Entity (Pref))
-              and then Known_Static_RM_Size (Entity (Pref))
-            then
-               Siz := RM_Size (Entity (Pref));
-
-            --  Case of known Esize of a type
-
-            elsif Id = Attribute_Object_Size
-              and then Is_Entity_Name (Pref)
-              and then Is_Type (Entity (Pref))
-              and then Known_Static_Esize (Entity (Pref))
-            then
-               Siz := Esize (Entity (Pref));
-
-            --  Case of known size of object
-
-            elsif Id = Attribute_Size
-              and then Is_Entity_Name (Pref)
-              and then Is_Object (Entity (Pref))
-              and then Known_Esize (Entity (Pref))
-              and then Known_Static_Esize (Entity (Pref))
-            then
-               Siz := Esize (Entity (Pref));
-
-            --  For an array component, we can do Size in the front end if the
-            --  component_size of the array is set.
-
-            elsif Nkind (Pref) = N_Indexed_Component then
-               Siz := Component_Size (Etype (Prefix (Pref)));
-
-            --  For a record component, we can do Size in the front end if
-            --  there is a component clause, or if the record is packed and the
-            --  component's size is known at compile time.
-
-            elsif Nkind (Pref) = N_Selected_Component then
-               declare
-                  Rec  : constant Entity_Id := Etype (Prefix (Pref));
-                  Comp : constant Entity_Id := Entity (Selector_Name (Pref));
-
-               begin
-                  if Present (Component_Clause (Comp)) then
-                     Siz := Esize (Comp);
-
-                  elsif Is_Packed (Rec) then
-                     Siz := RM_Size (Ptyp);
-
-                  else
-                     Apply_Universal_Integer_Attribute_Checks (N);
-                     return;
-                  end if;
-               end;
-
-            --  All other cases are handled by the back end
-
-            else
-               Apply_Universal_Integer_Attribute_Checks (N);
-
-               --  If Size is applied to a formal parameter that is of a packed
-               --  array subtype, then apply Size to the actual subtype.
-
-               if Is_Entity_Name (Pref)
-                 and then Is_Formal (Entity (Pref))
-                 and then Is_Array_Type (Ptyp)
-                 and then Is_Packed (Ptyp)
-               then
-                  Rewrite (N,
-                    Make_Attribute_Reference (Loc,
-                      Prefix         =>
-                        New_Occurrence_Of (Get_Actual_Subtype (Pref), Loc),
-                      Attribute_Name => Name_Size));
-                  Analyze_And_Resolve (N, Typ);
-               end if;
-
-               --  If Size applies to a dereference of an access to
-               --  unconstrained packed array, the back end needs to see its
-               --  unconstrained nominal type, but also a hint to the actual
-               --  constrained type.
-
-               if Nkind (Pref) = N_Explicit_Dereference
-                 and then Is_Array_Type (Ptyp)
-                 and then not Is_Constrained (Ptyp)
-                 and then Is_Packed (Ptyp)
-               then
-                  Set_Actual_Designated_Subtype (Pref,
-                    Get_Actual_Subtype (Pref));
-               end if;
-
-               return;
             end if;
 
-            --  Common processing for record and array component case
-
-            if Siz /= No_Uint and then Siz /= 0 then
-               declare
-                  CS : constant Boolean := Comes_From_Source (N);
-
-               begin
-                  Rewrite (N, Make_Integer_Literal (Loc, Siz));
-
-                  --  This integer literal is not a static expression. We do
-                  --  not call Analyze_And_Resolve here, because this would
-                  --  activate the circuit for deciding that a static value
-                  --  was out of range, and we don't want that.
-
-                  --  So just manually set the type, mark the expression as
-                  --  non-static, and then ensure that the result is checked
-                  --  properly if the attribute comes from source (if it was
-                  --  internally generated, we never need a constraint check).
-
-                  Set_Etype (N, Typ);
-                  Set_Is_Static_Expression (N, False);
+            --  Call Expand_Size_Attribute to do the final part of the
+            --  expansion which is shared with GNATprove expansion.
 
-                  if CS then
-                     Apply_Constraint_Check (N, Typ);
-                  end if;
-               end;
-            end if;
+            Expand_Size_Attribute (N);
          end Size;
 
       ------------------
@@ -7608,6 +7491,140 @@ package body Exp_Attr is
       end if;
    end Expand_Pred_Succ_Attribute;
 
+   ---------------------------
+   -- Expand_Size_Attribute --
+   ---------------------------
+
+   procedure Expand_Size_Attribute (N : Node_Id) is
+      Loc   : constant Source_Ptr   := Sloc (N);
+      Typ   : constant Entity_Id    := Etype (N);
+      Pref  : constant Node_Id      := Prefix (N);
+      Ptyp  : constant Entity_Id    := Etype (Pref);
+      Id    : constant Attribute_Id := Get_Attribute_Id (Attribute_Name (N));
+      Siz   : Uint;
+
+   begin
+      --  Case of known RM_Size of a type
+
+      if (Id = Attribute_Size or else Id = Attribute_Value_Size)
+        and then Is_Entity_Name (Pref)
+        and then Is_Type (Entity (Pref))
+        and then Known_Static_RM_Size (Entity (Pref))
+      then
+         Siz := RM_Size (Entity (Pref));
+
+      --  Case of known Esize of a type
+
+      elsif Id = Attribute_Object_Size
+        and then Is_Entity_Name (Pref)
+        and then Is_Type (Entity (Pref))
+        and then Known_Static_Esize (Entity (Pref))
+      then
+         Siz := Esize (Entity (Pref));
+
+      --  Case of known size of object
+
+      elsif Id = Attribute_Size
+        and then Is_Entity_Name (Pref)
+        and then Is_Object (Entity (Pref))
+        and then Known_Esize (Entity (Pref))
+        and then Known_Static_Esize (Entity (Pref))
+      then
+         Siz := Esize (Entity (Pref));
+
+      --  For an array component, we can do Size in the front end if the
+      --  component_size of the array is set.
+
+      elsif Nkind (Pref) = N_Indexed_Component then
+         Siz := Component_Size (Etype (Prefix (Pref)));
+
+      --  For a record component, we can do Size in the front end if there is a
+      --  component clause, or if the record is packed and the component's size
+      --  is known at compile time.
+
+      elsif Nkind (Pref) = N_Selected_Component then
+         declare
+            Rec  : constant Entity_Id := Etype (Prefix (Pref));
+            Comp : constant Entity_Id := Entity (Selector_Name (Pref));
+
+         begin
+            if Present (Component_Clause (Comp)) then
+               Siz := Esize (Comp);
+
+            elsif Is_Packed (Rec) then
+               Siz := RM_Size (Ptyp);
+
+            else
+               Apply_Universal_Integer_Attribute_Checks (N);
+               return;
+            end if;
+         end;
+
+      --  All other cases are handled by the back end
+
+      else
+         Apply_Universal_Integer_Attribute_Checks (N);
+
+         --  If Size is applied to a formal parameter that is of a packed
+         --  array subtype, then apply Size to the actual subtype.
+
+         if Is_Entity_Name (Pref)
+           and then Is_Formal (Entity (Pref))
+           and then Is_Array_Type (Ptyp)
+           and then Is_Packed (Ptyp)
+         then
+            Rewrite (N,
+              Make_Attribute_Reference (Loc,
+                Prefix         =>
+                  New_Occurrence_Of (Get_Actual_Subtype (Pref), Loc),
+                Attribute_Name => Name_Size));
+            Analyze_And_Resolve (N, Typ);
+         end if;
+
+         --  If Size applies to a dereference of an access to unconstrained
+         --  packed array, the back end needs to see its unconstrained nominal
+         --  type, but also a hint to the actual constrained type.
+
+         if Nkind (Pref) = N_Explicit_Dereference
+           and then Is_Array_Type (Ptyp)
+           and then not Is_Constrained (Ptyp)
+           and then Is_Packed (Ptyp)
+         then
+            Set_Actual_Designated_Subtype (Pref, Get_Actual_Subtype (Pref));
+         end if;
+
+         return;
+      end if;
+
+      --  Common processing for record and array component case
+
+      if Siz /= No_Uint and then Siz /= 0 then
+         declare
+            CS : constant Boolean := Comes_From_Source (N);
+
+         begin
+            Rewrite (N, Make_Integer_Literal (Loc, Siz));
+
+            --  This integer literal is not a static expression. We do not
+            --  call Analyze_And_Resolve here, because this would activate
+            --  the circuit for deciding that a static value was out of range,
+            --  and we don't want that.
+
+            --  So just manually set the type, mark the expression as
+            --  nonstatic, and then ensure that the result is checked
+            --  properly if the attribute comes from source (if it was
+            --  internally generated, we never need a constraint check).
+
+            Set_Etype (N, Typ);
+            Set_Is_Static_Expression (N, False);
+
+            if CS then
+               Apply_Constraint_Check (N, Typ);
+            end if;
+         end;
+      end if;
+   end Expand_Size_Attribute;
+
    -----------------------------
    -- Expand_Update_Attribute --
    -----------------------------

gcc/ada/exp_attr.ads

@@ -31,4 +31,9 @@ package Exp_Attr is
 
    procedure Expand_N_Attribute_Reference (N : Node_Id);
 
+   procedure Expand_Size_Attribute (N : Node_Id);
+   --  Handles part of the expansion of attributes 'Object_Size, 'Size,
+   --  'Value_Size, and 'VADS_Size, so that it can also be used in the special
+   --  expansion in GNATprove mode.
+
 end Exp_Attr;

gcc/ada/exp_spark.adb

@@ -227,6 +227,13 @@ package body Exp_SPARK is
             end if;
          end;
 
+      elsif Attr_Id = Attribute_Object_Size
+        or else Attr_Id = Attribute_Size
+        or else Attr_Id = Attribute_Value_Size
+        or else Attr_Id = Attribute_VADS_Size
+      then
+         Exp_Attr.Expand_Size_Attribute (N);
+
       --  For attributes which return Universal_Integer, introduce a conversion
       --  to the expected type with the appropriate check flags set.
 
@@ -241,10 +248,6 @@ package body Exp_SPARK is
         or else Attr_Id = Attribute_Pos
         or else Attr_Id = Attribute_Position
         or else Attr_Id = Attribute_Range_Length
-        or else Attr_Id = Attribute_Object_Size
-        or else Attr_Id = Attribute_Size
-        or else Attr_Id = Attribute_Value_Size
-        or else Attr_Id = Attribute_VADS_Size
         or else Attr_Id = Attribute_Aft
         or else Attr_Id = Attribute_Max_Alignment_For_Allocation
       then