[Ada] Implement static expression functions for Ada 202x (AI12-0075)

2020-06-17  Gary Dismukes  <dismukes@adacore.com>

gcc/ada/

	* aspects.ads (type Aspect_Id): Add Aspect_Static as a Boolean
	aspect, and update the Is_Representation_Aspect, Aspect_Names,
	and Aspect_Delay arrays.
	* exp_ch6.adb (Expand_Simple_Function_Return): In the case of a
	return for a static expression function, capture a copy of the
	expression of the return statement before it's expanded and
	reset its Analyzed flags. Then, just before leaving this
	procedure, if the expression was rewritten, set the
	Original_Node of the rewritten expression to the new copy and
	also set the Expression of the associated static expression
	function to designate that copy. This ensures that later copies
	of the expression made via New_Copy_Tree will fully copy all
	nodes of the expression tree.
	* inline.ads (Inline_Static_Expression_Function_Call): New
	procedure to evaluate and produce the result of a static call to
	a static expression function.
	* inline.adb: Add with and use for Sem_Res.
	(Establish_Actual_Mapping_For_Inlined_Call): New procedure
	extracted from code in Expand_Inlined_Call that traverses the
	actuals and formals of an inlined call and in some cases creates
	temporaries for holding the actuals, plus establishes an
	association between formals and actuals (via the Renamed_Object
	fields of the formals).
	(Formal_Is_Used_Once): Function removed from Expand_Inlined_Call
	and now nested in the above procedure.
	(Expand_Inlined_Call): Code for doing the formal/actual
	traversal is moved to Create_Actual_Temporaries and replaced
	with a call to that new procedure.
	(Inline_Static_Expression_Function_Call): New procedure to
	evaluate a static call to a static expression function,
	substituting actuals for their corresponding formals and
	producing a fully folded and static result expression. The
	function has subsidiary functions Replace_Formal and Reset_Sloc
	that take care of doing the mapping of formals to actuals and
	resetting the Slocs of subnodes of the mapped expression to that
	of the call so errors will be flagged on the call rather than
	function.
	* sem_ch6.adb (Analyze_Expression_Function): In the case of a
	static expression function, perform an additional preanalysis of
	the function's expression to ensure that it's a potentially
	static expression (according to the requirements of
	6.8(3.2/5-3.4/5)), and issue an error if it's not. The global
	flag Checking_Potentially_Static_Expression is set and unset
	around this checking.
	* sem_ch13.adb (Analyze_Aspect_Static): New procedure to enforce
	selected requirements of the new aspect Static on expression
	functions, including checking that the language version is
	Ada_2020 and that the entity to which it applies is an
	expression function whose formal parameters are of a static
	subtype and have mode 'in', its result subtype is a static
	subtype, and it has no pre- or postcondition aspects. A ???
	comment is added to indicate the need for adding checking that
	type invariants don't apply to the result type if the function
	is a boundary entity.
	(Analyze_One_Aspect): Call Analyze_Aspect_Static for aspect
	Static.
	* sem_elab.adb (Build_Call_Marker): Return without creating a
	call marker when the subprogram is a static expression function,
	since no ABE checking is needed for such functions.
	* sem_eval.ads (Checking_Potentially_Static_Expression): New
	function to return whether the checking for potentially static
	expressions is enabled.
	(Set_Checking_Potentially_Static_Expression): New procedure to
	enable or disable checking of potentially static expressions.
	* sem_eval.adb (Checking_For_Potentially_Static_Expression): New
	global flag for determining whether preanalysis of potentially
	static expression is being done, which affects the behavior of
	certain static evaluation routines.
	(Checking_Potentially_Static_Expression): New function to return
	whether the checking for potentially static expressions is
	enabled.
	(Eval_Call): When evaluating a call within a static expression
	function with checking of potentially static expression
	functions enabled, substitutes a static value in place of the
	call to allow folding of the expression.
	(Eval_Entity_Name): When evaluating a formal parameter of a
	static expression function with checking of potentially static
	expression functions enabled, substitutes a static value in
	place of the reference to the formal to allow folding of the
	expression.
	(Set_Checking_Potentially_Static_Expression): New procedure to
	enable or disable checking of potentially static expressions.
	* sem_res.adb (Resolve_Call): Test for a recursive call
	occurring within a static expression function and issue an error
	for such a call. Prevent the establishment of a transient scope
	in the case this is a call to a (string-returning) static
	expression function. When calling a static expression function,
	if no error has been posted on the function, call
	Inline_Static_Expression_Function_Call to convert the call into
	its equivalent static value.
	* sem_util.ads (Is_Static_Expression_Function): New function
	returning whether the subprogram entity passed to it is a static
	expression function.
	(Is_Static_Expression_Function_Call): New function to determine
	whether the call node passed to it is a static call to a static
	expression function.
	* sem_util.adb (Compile_Time_Constraint_Error): Suppress
	compile-time Constraint_Error reporting when checking for a
	potentially static expression.
	(Is_Static_Expression_Function): New function returning whether
	the subprogram entity passed to it is a static expression
	function by testing for the presence of aspect Static.
	(Has_All_Static_Actuals): New function in
	Is_Static_Expression_Function_Call that traverses the actual
	parameters of a function call and returns True only when all of
	the actuals are given by static expressions. In the case of a
	string-returning function, we call Resolve on each actual to
	ensure that their Is_Static_Expression flag properly reflects
	whether they're static, to allow suppressing creation of a
	transient scope within Resolve_Call. A prominent ??? comment is
	added to explain this rather unconventional call to Resolve.
	(Is_Static_Expression_Function_Call): New function that
	determines whether a node passed to it is a call to a static
	expression function all of whose actual parameters are given by
	static expressions.

12 files changed, 869 insertions, 262 deletions

diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index cf292ae..e6425a8 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -207,6 +207,7 @@ package Aspects is
       Aspect_Remote_Access_Type,            -- GNAT
       Aspect_Shared,                        -- GNAT (equivalent to Atomic)
       Aspect_Simple_Storage_Pool_Type,      -- GNAT
+      Aspect_Static,
       Aspect_Suppress_Debug_Info,           -- GNAT
       Aspect_Suppress_Initialization,       -- GNAT
       Aspect_Thread_Local_Storage,          -- GNAT
@@ -554,6 +555,7 @@ package Aspects is
       Aspect_Remote_Access_Type           => False,
       Aspect_Shared                       => True,
       Aspect_Simple_Storage_Pool_Type     => True,
+      Aspect_Static                       => False,
       Aspect_Suppress_Debug_Info          => False,
       Aspect_Suppress_Initialization      => False,
       Aspect_Thread_Local_Storage         => True,
@@ -679,6 +681,7 @@ package Aspects is
       Aspect_Size                         => Name_Size,
       Aspect_Small                        => Name_Small,
       Aspect_SPARK_Mode                   => Name_SPARK_Mode,
+      Aspect_Static                       => Name_Static,
       Aspect_Static_Predicate             => Name_Static_Predicate,
       Aspect_Storage_Pool                 => Name_Storage_Pool,
       Aspect_Storage_Size                 => Name_Storage_Size,
@@ -934,6 +937,7 @@ package Aspects is
       Aspect_Refined_State                => Never_Delay,
       Aspect_Relaxed_Initialization       => Never_Delay,
       Aspect_SPARK_Mode                   => Never_Delay,
+      Aspect_Static                       => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,
       Aspect_Unimplemented                => Never_Delay,
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 6ca5fd6..2d065aa 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -7284,9 +7284,33 @@ package body Exp_Ch6 is
                  Reason => PE_Accessibility_Check_Failed));
       end Check_Against_Result_Level;
 
+      --  Local Data
+
+      New_Copy_Of_Exp : Node_Id := Empty;
+
    --  Start of processing for Expand_Simple_Function_Return
 
    begin
+      --  For static expression functions, the expression of the function
+      --  needs to be available in a form that can be replicated later for
+      --  calls, but rewriting of the return expression in the body created
+      --  for expression functions will cause the original expression to no
+      --  longer be properly copyable via New_Copy_Tree, because the Parent
+      --  fields of the nodes will now point to nodes in the rewritten tree,
+      --  and New_Copy_Tree won't copy the deeper nodes of the original tree.
+      --  So we work around that by making a copy of the expression tree
+      --  before any rewriting occurs, and replacing the original expression
+      --  tree with this copy (see the end of this procedure). We also reset
+      --  the Analyzed flags on the nodes in the tree copy to ensure that
+      --  later copies of the tree will be fully reanalyzed. This copying
+      --  is of course rather inelegant, to say the least, and it would be
+      --  nice if there were a way to avoid it. ???
+
+      if Is_Static_Expression_Function (Scope_Id) then
+         New_Copy_Of_Exp := New_Copy_Tree (Exp);
+         Reset_Analyzed_Flags (New_Copy_Of_Exp);
+      end if;
+
       if Is_Class_Wide_Type (R_Type)
         and then not Is_Class_Wide_Type (Exp_Typ)
         and then Nkind (Exp) /= N_Type_Conversion
@@ -7997,6 +8021,21 @@ package body Exp_Ch6 is
          Rewrite (Exp, Convert_To (Utyp, Relocate_Node (Exp)));
          Analyze_And_Resolve (Exp);
       end if;
+
+      --  If a new copy of a static expression function's expression was made
+      --  (see the beginning of this procedure's statement part), then we now
+      --  replace the original expression tree with the copy and also change
+      --  the Original_Node field of the rewritten expression to point to that
+      --  copy. It would be nice to find a way to avoid this???
+
+      if Present (New_Copy_Of_Exp) then
+         Set_Expression
+           (Original_Node (Subprogram_Spec (Scope_Id)), New_Copy_Of_Exp);
+
+         if Exp /= Original_Node (Exp) then
+            Set_Original_Node (Exp, New_Copy_Of_Exp);
+         end if;
+      end if;
    end Expand_Simple_Function_Return;
 
    -----------------------
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index e49b83e..d1a6ee3 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -47,6 +47,7 @@ with Sem_Ch8;  use Sem_Ch8;
 with Sem_Ch10; use Sem_Ch10;
 with Sem_Ch12; use Sem_Ch12;
 with Sem_Prag; use Sem_Prag;
+with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
 with Sinput;   use Sinput;
@@ -265,6 +266,19 @@ package body Inline is
    --  Make entry in Inlined table for subprogram E, or return table index
    --  that already holds E.
 
+   procedure Establish_Actual_Mapping_For_Inlined_Call
+     (N                     : Node_Id;
+      Subp                  : Entity_Id;
+      Decls                 : List_Id;
+      Body_Or_Expr_To_Check : Node_Id);
+   --  Establish a mapping from formals to actuals in the call N for the target
+   --  subprogram Subp, and create temporaries or renamings when needed for the
+   --  actuals that are expressions (except for actuals given by simple entity
+   --  names or literals) or that are scalars that require copying to preserve
+   --  semantics. Any temporary objects that are created are inserted in Decls.
+   --  Body_Or_Expr_To_Check indicates the target body (or possibly expression
+   --  of an expression function), which may be traversed to count formal uses.
+
    function Get_Code_Unit_Entity (E : Entity_Id) return Entity_Id;
    pragma Inline (Get_Code_Unit_Entity);
    --  Return the entity node for the unit containing E. Always return the spec
@@ -307,6 +321,10 @@ package body Inline is
    --    Unmodified
    --    Unreferenced
 
+   procedure Reset_Actual_Mapping_For_Inlined_Call (Subp : Entity_Id);
+   --  Reset the Renamed_Object flags on the formals of Subp, which can be set
+   --  by a call to Establish_Actual_Mapping_For_Inlined_Call.
+
    ------------------------------
    -- Deferred Cleanup Actions --
    ------------------------------
@@ -2791,6 +2809,280 @@ package body Inline is
       end loop;
    end Cleanup_Scopes;
 
+   procedure Establish_Actual_Mapping_For_Inlined_Call
+     (N                     : Node_Id;
+      Subp                  : Entity_Id;
+      Decls                 : List_Id;
+      Body_Or_Expr_To_Check : Node_Id)
+   is
+
+      function Formal_Is_Used_Once (Formal : Entity_Id) return Boolean;
+      --  Determine whether a formal parameter is used only once in
+      --  Body_Or_Expr_To_Check.
+
+      -------------------------
+      -- Formal_Is_Used_Once --
+      -------------------------
+
+      function Formal_Is_Used_Once (Formal : Entity_Id) return Boolean is
+         Use_Counter : Int := 0;
+
+         function Count_Uses (N : Node_Id) return Traverse_Result;
+         --  Traverse the tree and count the uses of the formal parameter.
+         --  In this case, for optimization purposes, we do not need to
+         --  continue the traversal once more than one use is encountered.
+
+         ----------------
+         -- Count_Uses --
+         ----------------
+
+         function Count_Uses (N : Node_Id) return Traverse_Result is
+         begin
+            --  The original node is an identifier
+
+            if Nkind (N) = N_Identifier
+              and then Present (Entity (N))
+
+               --  Original node's entity points to the one in the copied body
+
+              and then Nkind (Entity (N)) = N_Identifier
+              and then Present (Entity (Entity (N)))
+
+               --  The entity of the copied node is the formal parameter
+
+              and then Entity (Entity (N)) = Formal
+            then
+               Use_Counter := Use_Counter + 1;
+
+               if Use_Counter > 1 then
+
+                  --  Denote more than one use and abandon the traversal
+
+                  Use_Counter := 2;
+                  return Abandon;
+
+               end if;
+            end if;
+
+            return OK;
+         end Count_Uses;
+
+         procedure Count_Formal_Uses is new Traverse_Proc (Count_Uses);
+
+      --  Start of processing for Formal_Is_Used_Once
+
+      begin
+         Count_Formal_Uses (Body_Or_Expr_To_Check);
+         return Use_Counter = 1;
+      end Formal_Is_Used_Once;
+
+      -- Local Data --
+
+      F        : Entity_Id;
+      A        : Node_Id;
+      Decl     : Node_Id;
+      Loc      : constant Source_Ptr := Sloc (N);
+      New_A    : Node_Id;
+      Temp     : Entity_Id;
+      Temp_Typ : Entity_Id;
+
+   --  Start of processing for Establish_Actual_Mapping_For_Inlined_Call
+
+   begin
+      F := First_Formal (Subp);
+      A := First_Actual (N);
+      while Present (F) loop
+         if Present (Renamed_Object (F)) then
+
+            --  If expander is active, it is an error to try to inline a
+            --  recursive program. In GNATprove mode, just indicate that the
+            --  inlining will not happen, and mark the subprogram as not always
+            --  inlined.
+
+            if GNATprove_Mode then
+               Cannot_Inline
+                 ("cannot inline call to recursive subprogram?", N, Subp);
+               Set_Is_Inlined_Always (Subp, False);
+            else
+               Error_Msg_N
+                 ("cannot inline call to recursive subprogram", N);
+            end if;
+
+            return;
+         end if;
+
+         --  Reset Last_Assignment for any parameters of mode out or in out, to
+         --  prevent spurious warnings about overwriting for assignments to the
+         --  formal in the inlined code.
+
+         if Is_Entity_Name (A) and then Ekind (F) /= E_In_Parameter then
+            Set_Last_Assignment (Entity (A), Empty);
+         end if;
+
+         --  If the argument may be a controlling argument in a call within
+         --  the inlined body, we must preserve its class-wide nature to ensure
+         --  that dynamic dispatching will take place subsequently. If the
+         --  formal has a constraint, then it must be preserved to retain the
+         --  semantics of the body.
+
+         if Is_Class_Wide_Type (Etype (F))
+           or else (Is_Access_Type (Etype (F))
+                     and then Is_Class_Wide_Type (Designated_Type (Etype (F))))
+         then
+            Temp_Typ := Etype (F);
+
+         elsif Base_Type (Etype (F)) = Base_Type (Etype (A))
+           and then Etype (F) /= Base_Type (Etype (F))
+           and then Is_Constrained (Etype (F))
+         then
+            Temp_Typ := Etype (F);
+
+         else
+            Temp_Typ := Etype (A);
+         end if;
+
+         --  If the actual is a simple name or a literal, no need to
+         --  create a temporary, object can be used directly.
+
+         --  If the actual is a literal and the formal has its address taken,
+         --  we cannot pass the literal itself as an argument, so its value
+         --  must be captured in a temporary. Skip this optimization in
+         --  GNATprove mode, to make sure any check on a type conversion
+         --  will be issued.
+
+         if (Is_Entity_Name (A)
+              and then
+                (not Is_Scalar_Type (Etype (A))
+                  or else Ekind (Entity (A)) = E_Enumeration_Literal)
+              and then not GNATprove_Mode)
+
+         --  When the actual is an identifier and the corresponding formal is
+         --  used only once in the original body, the formal can be substituted
+         --  directly with the actual parameter. Skip this optimization in
+         --  GNATprove mode, to make sure any check on a type conversion
+         --  will be issued.
+
+           or else
+             (Nkind (A) = N_Identifier
+               and then Formal_Is_Used_Once (F)
+               and then not GNATprove_Mode)
+
+           or else
+             (Nkind_In (A, N_Real_Literal,
+                           N_Integer_Literal,
+                           N_Character_Literal)
+               and then not Address_Taken (F))
+         then
+            if Etype (F) /= Etype (A) then
+               Set_Renamed_Object
+                 (F, Unchecked_Convert_To (Etype (F), Relocate_Node (A)));
+            else
+               Set_Renamed_Object (F, A);
+            end if;
+
+         else
+            Temp := Make_Temporary (Loc, 'C');
+
+            --  If the actual for an in/in-out parameter is a view conversion,
+            --  make it into an unchecked conversion, given that an untagged
+            --  type conversion is not a proper object for a renaming.
+
+            --  In-out conversions that involve real conversions have already
+            --  been transformed in Expand_Actuals.
+
+            if Nkind (A) = N_Type_Conversion
+              and then Ekind (F) /= E_In_Parameter
+            then
+               New_A :=
+                 Make_Unchecked_Type_Conversion (Loc,
+                   Subtype_Mark => New_Occurrence_Of (Etype (F), Loc),
+                   Expression   => Relocate_Node (Expression (A)));
+
+            --  In GNATprove mode, keep the most precise type of the actual for
+            --  the temporary variable, when the formal type is unconstrained.
+            --  Otherwise, the AST may contain unexpected assignment statements
+            --  to a temporary variable of unconstrained type renaming a local
+            --  variable of constrained type, which is not expected by
+            --  GNATprove.
+
+            elsif Etype (F) /= Etype (A)
+              and then (not GNATprove_Mode or else Is_Constrained (Etype (F)))
+            then
+               New_A    := Unchecked_Convert_To (Etype (F), Relocate_Node (A));
+               Temp_Typ := Etype (F);
+
+            else
+               New_A := Relocate_Node (A);
+            end if;
+
+            Set_Sloc (New_A, Sloc (N));
+
+            --  If the actual has a by-reference type, it cannot be copied,
+            --  so its value is captured in a renaming declaration. Otherwise
+            --  declare a local constant initialized with the actual.
+
+            --  We also use a renaming declaration for expressions of an array
+            --  type that is not bit-packed, both for efficiency reasons and to
+            --  respect the semantics of the call: in most cases the original
+            --  call will pass the parameter by reference, and thus the inlined
+            --  code will have the same semantics.
+
+            --  Finally, we need a renaming declaration in the case of limited
+            --  types for which initialization cannot be by copy either.
+
+            if Ekind (F) = E_In_Parameter
+              and then not Is_By_Reference_Type (Etype (A))
+              and then not Is_Limited_Type (Etype (A))
+              and then
+                (not Is_Array_Type (Etype (A))
+                  or else not Is_Object_Reference (A)
+                  or else Is_Bit_Packed_Array (Etype (A)))
+            then
+               Decl :=
+                 Make_Object_Declaration (Loc,
+                   Defining_Identifier => Temp,
+                   Constant_Present    => True,
+                   Object_Definition   => New_Occurrence_Of (Temp_Typ, Loc),
+                   Expression          => New_A);
+
+            else
+               --  In GNATprove mode, make an explicit copy of input
+               --  parameters when formal and actual types differ, to make
+               --  sure any check on the type conversion will be issued.
+               --  The legality of the copy is ensured by calling first
+               --  Call_Can_Be_Inlined_In_GNATprove_Mode.
+
+               if GNATprove_Mode
+                 and then Ekind (F) /= E_Out_Parameter
+                 and then not Same_Type (Etype (F), Etype (A))
+               then
+                  pragma Assert (not Is_By_Reference_Type (Etype (A)));
+                  pragma Assert (not Is_Limited_Type (Etype (A)));
+
+                  Append_To (Decls,
+                    Make_Object_Declaration (Loc,
+                      Defining_Identifier => Make_Temporary (Loc, 'C'),
+                      Constant_Present    => True,
+                      Object_Definition   => New_Occurrence_Of (Temp_Typ, Loc),
+                      Expression          => New_Copy_Tree (New_A)));
+               end if;
+
+               Decl :=
+                 Make_Object_Renaming_Declaration (Loc,
+                   Defining_Identifier => Temp,
+                   Subtype_Mark        => New_Occurrence_Of (Temp_Typ, Loc),
+                   Name                => New_A);
+            end if;
+
+            Append (Decl, Decls);
+            Set_Renamed_Object (F, Temp);
+         end if;
+
+         Next_Formal (F);
+         Next_Actual (A);
+      end loop;
+   end Establish_Actual_Mapping_For_Inlined_Call;
+
    -------------------------
    -- Expand_Inlined_Call --
    -------------------------
@@ -2816,15 +3108,11 @@ package body Inline is
       Blk      : Node_Id;
       Decl     : Node_Id;
       Exit_Lab : Entity_Id := Empty;
-      F        : Entity_Id;
-      A        : Node_Id;
       Lab_Decl : Node_Id   := Empty;
       Lab_Id   : Node_Id;
-      New_A    : Node_Id;
       Num_Ret  : Nat       := 0;
       Ret_Type : Entity_Id;
       Temp     : Entity_Id;
-      Temp_Typ : Entity_Id;
 
       Is_Unc      : Boolean;
       Is_Unc_Decl : Boolean;
@@ -2890,9 +3178,6 @@ package body Inline is
       --  If procedure body has no local variables, inline body without
       --  creating block, otherwise rewrite call with block.
 
-      function Formal_Is_Used_Once (Formal : Entity_Id) return Boolean;
-      --  Determine whether a formal parameter is used only once in Orig_Bod
-
       -----------------------------------
       -- Declare_Postconditions_Result --
       -----------------------------------
@@ -3409,62 +3694,6 @@ package body Inline is
          end if;
       end Rewrite_Procedure_Call;
 
-      -------------------------
-      -- Formal_Is_Used_Once --
-      -------------------------
-
-      function Formal_Is_Used_Once (Formal : Entity_Id) return Boolean is
-         Use_Counter : Int := 0;
-
-         function Count_Uses (N : Node_Id) return Traverse_Result;
-         --  Traverse the tree and count the uses of the formal parameter.
-         --  In this case, for optimization purposes, we do not need to
-         --  continue the traversal once more than one use is encountered.
-
-         ----------------
-         -- Count_Uses --
-         ----------------
-
-         function Count_Uses (N : Node_Id) return Traverse_Result is
-         begin
-            --  The original node is an identifier
-
-            if Nkind (N) = N_Identifier
-              and then Present (Entity (N))
-
-               --  Original node's entity points to the one in the copied body
-
-              and then Nkind (Entity (N)) = N_Identifier
-              and then Present (Entity (Entity (N)))
-
-               --  The entity of the copied node is the formal parameter
-
-              and then Entity (Entity (N)) = Formal
-            then
-               Use_Counter := Use_Counter + 1;
-
-               if Use_Counter > 1 then
-
-                  --  Denote more than one use and abandon the traversal
-
-                  Use_Counter := 2;
-                  return Abandon;
-
-               end if;
-            end if;
-
-            return OK;
-         end Count_Uses;
-
-         procedure Count_Formal_Uses is new Traverse_Proc (Count_Uses);
-
-      --  Start of processing for Formal_Is_Used_Once
-
-      begin
-         Count_Formal_Uses (Orig_Bod);
-         return Use_Counter = 1;
-      end Formal_Is_Used_Once;
-
    --  Start of processing for Expand_Inlined_Call
 
    begin
@@ -3694,198 +3923,7 @@ package body Inline is
       --  Create temporaries for the actuals that are expressions, or that are
       --  scalars and require copying to preserve semantics.
 
-      F := First_Formal (Subp);
-      A := First_Actual (N);
-      while Present (F) loop
-         if Present (Renamed_Object (F)) then
-
-            --  If expander is active, it is an error to try to inline a
-            --  recursive program. In GNATprove mode, just indicate that the
-            --  inlining will not happen, and mark the subprogram as not always
-            --  inlined.
-
-            if GNATprove_Mode then
-               Cannot_Inline
-                 ("cannot inline call to recursive subprogram?", N, Subp);
-               Set_Is_Inlined_Always (Subp, False);
-            else
-               Error_Msg_N
-                 ("cannot inline call to recursive subprogram", N);
-            end if;
-
-            return;
-         end if;
-
-         --  Reset Last_Assignment for any parameters of mode out or in out, to
-         --  prevent spurious warnings about overwriting for assignments to the
-         --  formal in the inlined code.
-
-         if Is_Entity_Name (A) and then Ekind (F) /= E_In_Parameter then
-            Set_Last_Assignment (Entity (A), Empty);
-         end if;
-
-         --  If the argument may be a controlling argument in a call within
-         --  the inlined body, we must preserve its classwide nature to insure
-         --  that dynamic dispatching take place subsequently. If the formal
-         --  has a constraint it must be preserved to retain the semantics of
-         --  the body.
-
-         if Is_Class_Wide_Type (Etype (F))
-           or else (Is_Access_Type (Etype (F))
-                     and then Is_Class_Wide_Type (Designated_Type (Etype (F))))
-         then
-            Temp_Typ := Etype (F);
-
-         elsif Base_Type (Etype (F)) = Base_Type (Etype (A))
-           and then Etype (F) /= Base_Type (Etype (F))
-           and then Is_Constrained (Etype (F))
-         then
-            Temp_Typ := Etype (F);
-
-         else
-            Temp_Typ := Etype (A);
-         end if;
-
-         --  If the actual is a simple name or a literal, no need to
-         --  create a temporary, object can be used directly.
-
-         --  If the actual is a literal and the formal has its address taken,
-         --  we cannot pass the literal itself as an argument, so its value
-         --  must be captured in a temporary. Skip this optimization in
-         --  GNATprove mode, to make sure any check on a type conversion
-         --  will be issued.
-
-         if (Is_Entity_Name (A)
-              and then
-                (not Is_Scalar_Type (Etype (A))
-                  or else Ekind (Entity (A)) = E_Enumeration_Literal)
-              and then not GNATprove_Mode)
-
-         --  When the actual is an identifier and the corresponding formal is
-         --  used only once in the original body, the formal can be substituted
-         --  directly with the actual parameter. Skip this optimization in
-         --  GNATprove mode, to make sure any check on a type conversion
-         --  will be issued.
-
-           or else
-             (Nkind (A) = N_Identifier
-               and then Formal_Is_Used_Once (F)
-               and then not GNATprove_Mode)
-
-           or else
-             (Nkind_In (A, N_Real_Literal,
-                           N_Integer_Literal,
-                           N_Character_Literal)
-               and then not Address_Taken (F))
-         then
-            if Etype (F) /= Etype (A) then
-               Set_Renamed_Object
-                 (F, Unchecked_Convert_To (Etype (F), Relocate_Node (A)));
-            else
-               Set_Renamed_Object (F, A);
-            end if;
-
-         else
-            Temp := Make_Temporary (Loc, 'C');
-
-            --  If the actual for an in/in-out parameter is a view conversion,
-            --  make it into an unchecked conversion, given that an untagged
-            --  type conversion is not a proper object for a renaming.
-
-            --  In-out conversions that involve real conversions have already
-            --  been transformed in Expand_Actuals.
-
-            if Nkind (A) = N_Type_Conversion
-              and then Ekind (F) /= E_In_Parameter
-            then
-               New_A :=
-                 Make_Unchecked_Type_Conversion (Loc,
-                   Subtype_Mark => New_Occurrence_Of (Etype (F), Loc),
-                   Expression   => Relocate_Node (Expression (A)));
-
-            --  In GNATprove mode, keep the most precise type of the actual for
-            --  the temporary variable, when the formal type is unconstrained.
-            --  Otherwise, the AST may contain unexpected assignment statements
-            --  to a temporary variable of unconstrained type renaming a local
-            --  variable of constrained type, which is not expected by
-            --  GNATprove.
-
-            elsif Etype (F) /= Etype (A)
-              and then (not GNATprove_Mode or else Is_Constrained (Etype (F)))
-            then
-               New_A    := Unchecked_Convert_To (Etype (F), Relocate_Node (A));
-               Temp_Typ := Etype (F);
-
-            else
-               New_A := Relocate_Node (A);
-            end if;
-
-            Set_Sloc (New_A, Sloc (N));
-
-            --  If the actual has a by-reference type, it cannot be copied,
-            --  so its value is captured in a renaming declaration. Otherwise
-            --  declare a local constant initialized with the actual.
-
-            --  We also use a renaming declaration for expressions of an array
-            --  type that is not bit-packed, both for efficiency reasons and to
-            --  respect the semantics of the call: in most cases the original
-            --  call will pass the parameter by reference, and thus the inlined
-            --  code will have the same semantics.
-
-            --  Finally, we need a renaming declaration in the case of limited
-            --  types for which initialization cannot be by copy either.
-
-            if Ekind (F) = E_In_Parameter
-              and then not Is_By_Reference_Type (Etype (A))
-              and then not Is_Limited_Type (Etype (A))
-              and then
-                (not Is_Array_Type (Etype (A))
-                  or else not Is_Object_Reference (A)
-                  or else Is_Bit_Packed_Array (Etype (A)))
-            then
-               Decl :=
-                 Make_Object_Declaration (Loc,
-                   Defining_Identifier => Temp,
-                   Constant_Present    => True,
-                   Object_Definition   => New_Occurrence_Of (Temp_Typ, Loc),
-                   Expression          => New_A);
-
-            else
-               --  In GNATprove mode, make an explicit copy of input
-               --  parameters when formal and actual types differ, to make
-               --  sure any check on the type conversion will be issued.
-               --  The legality of the copy is ensured by calling first
-               --  Call_Can_Be_Inlined_In_GNATprove_Mode.
-
-               if GNATprove_Mode
-                 and then Ekind (F) /= E_Out_Parameter
-                 and then not Same_Type (Etype (F), Etype (A))
-               then
-                  pragma Assert (not Is_By_Reference_Type (Etype (A)));
-                  pragma Assert (not Is_Limited_Type (Etype (A)));
-
-                  Append_To (Decls,
-                    Make_Object_Declaration (Loc,
-                      Defining_Identifier => Make_Temporary (Loc, 'C'),
-                      Constant_Present    => True,
-                      Object_Definition   => New_Occurrence_Of (Temp_Typ, Loc),
-                      Expression          => New_Copy_Tree (New_A)));
-               end if;
-
-               Decl :=
-                 Make_Object_Renaming_Declaration (Loc,
-                   Defining_Identifier => Temp,
-                   Subtype_Mark        => New_Occurrence_Of (Temp_Typ, Loc),
-                   Name                => New_A);
-            end if;
-
-            Append (Decl, Decls);
-            Set_Renamed_Object (F, Temp);
-         end if;
-
-         Next_Formal (F);
-         Next_Actual (A);
-      end loop;
+      Establish_Actual_Mapping_For_Inlined_Call (N, Subp, Decls, Orig_Bod);
 
       --  Establish target of function call. If context is not assignment or
       --  declaration, create a temporary as a target. The declaration for the
@@ -4148,11 +4186,7 @@ package body Inline is
 
       --  Cleanup mapping between formals and actuals for other expansions
 
-      F := First_Formal (Subp);
-      while Present (F) loop
-         Set_Renamed_Object (F, Empty);
-         Next_Formal (F);
-      end loop;
+      Reset_Actual_Mapping_For_Inlined_Call (Subp);
    end Expand_Inlined_Call;
 
    --------------------------
@@ -4598,6 +4632,128 @@ package body Inline is
       Backend_Not_Inlined_Subps := No_Elist;
    end Initialize;
 
+   --------------------------------------------
+   -- Inline_Static_Expression_Function_Call --
+   --------------------------------------------
+
+   procedure Inline_Static_Expression_Function_Call
+     (N : Node_Id; Subp : Entity_Id)
+   is
+
+      function Replace_Formal (N : Node_Id) return Traverse_Result;
+      --  Replace each occurrence of a formal with the corresponding actual,
+      --  using the mapping created by Establish_Mapping_For_Inlined_Call.
+
+      function Reset_Sloc (Nod : Node_Id) return Traverse_Result;
+      --  Reset the Sloc of a node to that of the call itself, so that errors
+      --  will be flagged on the call to the static expression function itself
+      --  rather than on the expression of the function's declaration.
+
+      --------------------
+      -- Replace_Formal --
+      --------------------
+
+      function Replace_Formal (N : Node_Id) return Traverse_Result is
+         A   : Entity_Id;
+         E   : Entity_Id;
+
+      begin
+         if Is_Entity_Name (N) and then Present (Entity (N)) then
+            E := Entity (N);
+
+            if Is_Formal (E) and then Scope (E) = Subp then
+               A := Renamed_Object (E);
+
+               if Nkind (A) = N_Defining_Identifier then
+                  Rewrite (N, New_Occurrence_Of (A, Sloc (N)));
+
+               --  Literal cases
+
+               else
+                  Rewrite (N, New_Copy (A));
+               end if;
+            end if;
+
+            return Skip;
+
+         else
+            return OK;
+         end if;
+      end Replace_Formal;
+
+      procedure Replace_Formals is new Traverse_Proc (Replace_Formal);
+
+      ------------------
+      -- Process_Sloc --
+      ------------------
+
+      function Reset_Sloc (Nod : Node_Id) return Traverse_Result is
+      begin
+         Set_Sloc (Nod, Sloc (N));
+         Set_Comes_From_Source (Nod, False);
+
+         return OK;
+      end Reset_Sloc;
+
+      procedure Reset_Slocs is new Traverse_Proc (Reset_Sloc);
+
+   --  Start of processing for Inline_Static_Expression_Function_Call
+
+   begin
+      pragma Assert (Is_Static_Expression_Function_Call (N));
+
+      declare
+         Decls     : constant List_Id := New_List;
+         Func_Expr : constant Node_Id :=
+                       Expression_Of_Expression_Function (Subp);
+         Expr_Copy : constant Node_Id := New_Copy_Tree (Func_Expr);
+
+      begin
+         --  Create a mapping from formals to actuals, also creating temps in
+         --  Decls, when needed, to hold the actuals.
+
+         Establish_Actual_Mapping_For_Inlined_Call (N, Subp, Decls, Func_Expr);
+
+         Insert_Actions (N, Decls);
+
+         --  Now substitute actuals for their corresponding formal references
+         --  within the expression.
+
+         Replace_Formals (Expr_Copy);
+
+         Reset_Slocs (Expr_Copy);
+
+         --  Apply a qualified expression with the function's result subtype,
+         --  to ensure that we check the expression against any constraint
+         --  or predicate, which will cause the call to be illegal if the
+         --  folded expression doesn't satisfy them. (The predicate case
+         --  might not get checked if the subtype hasn't been frozen yet,
+         --  which can happen if this static expression happens to be what
+         --  causes the freezing, because Has_Static_Predicate doesn't get
+         --  set on the subtype until it's frozen and Build_Predicates is
+         --  called. It's not clear how to address this case. ???)
+
+         Rewrite (Expr_Copy,
+           Make_Qualified_Expression (Sloc (Expr_Copy),
+             Subtype_Mark =>
+               New_Occurrence_Of (Etype (N), Sloc (Expr_Copy)),
+             Expression =>
+               Relocate_Node (Expr_Copy)));
+
+         Set_Etype (Expr_Copy, Etype (N));
+
+         Analyze_And_Resolve (Expr_Copy, Etype (N));
+
+         --  Finally rewrite the function call as the folded static result
+
+         Rewrite (N, Expr_Copy);
+
+         --  Cleanup mapping between formals and actuals for other expansions
+
+         Reset_Actual_Mapping_For_Inlined_Call (Subp);
+      end;
+   end Inline_Static_Expression_Function_Call;
+
    ------------------------
    -- Instantiate_Bodies --
    ------------------------
@@ -5002,4 +5158,18 @@ package body Inline is
       end loop;
    end Remove_Dead_Instance;
 
+   -------------------------------------------
+   -- Reset_Actual_Mapping_For_Inlined_Call --
+   -------------------------------------------
+
+   procedure Reset_Actual_Mapping_For_Inlined_Call (Subp : Entity_Id) is
+      F : Entity_Id := First_Formal (Subp);
+
+   begin
+      while Present (F) loop
+         Set_Renamed_Object (F, Empty);
+         Next_Formal (F);
+      end loop;
+   end Reset_Actual_Mapping_For_Inlined_Call;
+
 end Inline;
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index 05042be..a7f4aab 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -227,6 +227,12 @@ package Inline is
    --  Check a list of statements, Stats, that make inlining of Subp not
    --  worthwhile, including any tasking statement, nested at any level.
 
+   procedure Inline_Static_Expression_Function_Call
+     (N : Node_Id; Subp : Entity_Id);
+   --  Evaluate static call to a static expression function Subp, substituting
+   --  actuals in place of references to their corresponding formals and
+   --  rewriting the call N as a fully folded and static result expression.
+
    procedure List_Inlining_Info;
    --  Generate listing of calls inlined by the frontend plus listing of
    --  calls to inline subprograms passed to the backend.
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 583bb98..abd482e 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1792,6 +1792,9 @@ package body Sem_Ch13 is
             procedure Analyze_Aspect_Relaxed_Initialization;
             --  Perform analysis of aspect Relaxed_Initialization
 
+            procedure Analyze_Aspect_Static;
+            --  Ada 202x (AI12-0075): Perform analysis of aspect Static
+
             procedure Make_Aitem_Pragma
               (Pragma_Argument_Associations : List_Id;
                Pragma_Name                  : Name_Id);
@@ -2309,6 +2312,129 @@ package body Sem_Ch13 is
                end if;
             end Analyze_Aspect_Relaxed_Initialization;
 
+            ---------------------------
+            -- Analyze_Aspect_Static --
+            ---------------------------
+
+            procedure Analyze_Aspect_Static is
+            begin
+               if Ada_Version < Ada_2020 then
+                  Error_Msg_N
+                    ("aspect % is an Ada 202x feature", Aspect);
+                  Error_Msg_N ("\compile with -gnat2020", Aspect);
+
+                  return;
+
+               --  The aspect applies only to expression functions that
+               --  statisfy the requirements for a static expression function
+               --  (such as having an expression that is predicate-static).
+
+               elsif not Is_Expression_Function (E) then
+                  Error_Msg_N
+                    ("aspect % requires expression function", Aspect);
+
+                  return;
+
+               --  Ada 202x (AI12-0075): Check that the function satisfies
+               --  several requirements of static expression functions as
+               --  specified in RM 6.8(5.1-5.8). Note that some of the
+               --  requirements given there are checked elsewhere.
+
+               else
+                  --  The expression of the expression function must be a
+                  --  potentially static expression (RM 202x 6.8(3.2-3.4)).
+                  --  That's checked in Sem_Ch6.Analyze_Expression_Function.
+
+                  --  The function must not contain any calls to itself, which
+                  --  is checked in Sem_Res.Resolve_Call.
+
+                  --  Each formal must be of mode in and have a static subtype
+
+                  declare
+                     Formal : Entity_Id := First_Formal (E);
+                  begin
+                     while Present (Formal) loop
+                        if Ekind (Formal) /= E_In_Parameter then
+                           Error_Msg_N
+                             ("aspect % requires formals of mode IN",
+                              Aspect);
+
+                           return;
+                        end if;
+
+                        if not Is_Static_Subtype (Etype (Formal)) then
+                           Error_Msg_N
+                             ("aspect % requires formals with static subtypes",
+                              Aspect);
+
+                           return;
+                        end if;
+
+                        Next_Formal (Formal);
+                     end loop;
+                  end;
+
+                  --  The function's result subtype must be a static subtype
+
+                  if not Is_Static_Subtype (Etype (E)) then
+                     Error_Msg_N
+                       ("aspect % requires function with result of "
+                        & "a static subtype",
+                        Aspect);
+
+                     return;
+                  end if;
+
+                  --  Check that the function does not have any applicable
+                  --  precondition or postcondition expression.
+
+                  for Asp in Pre_Post_Aspects loop
+                     if Has_Aspect (E, Asp) then
+                        Error_Msg_N
+                          ("this aspect not allowed for static expression "
+                             & "functions", Find_Aspect (E, Asp));
+
+                        return;
+                     end if;
+                  end loop;
+
+                  --  ??? TBD: Must check that "for result type R, if the
+                  --  function is a boundary entity for type R (see 7.3.2),
+                  --  no type invariant applies to type R; if R has a
+                  --  component type C, a similar rule applies to C."
+               end if;
+
+               --  Preanalyze the expression (if any) when the aspect resides
+               --  in a generic unit. (Is this generic-related code necessary
+               --  for this aspect? It's modeled on what's done for aspect
+               --  Disable_Controlled. ???)
+
+               if Inside_A_Generic then
+                  if Present (Expr) then
+                     Preanalyze_And_Resolve (Expr, Any_Boolean);
+                  end if;
+
+               --  Otherwise the aspect resides in a nongeneric context
+
+               else
+                  --  When the expression statically evaluates to True, the
+                  --  expression function is treated as a static function.
+                  --  Otherwise the aspect appears without an expression and
+                  --  defaults to True.
+
+                  if Present (Expr) then
+                     Analyze_And_Resolve (Expr, Any_Boolean);
+
+                     --  Error if the boolean expression is not static
+
+                     if not Is_OK_Static_Expression (Expr) then
+                        Error_Msg_N
+                          ("expression of aspect % must be static", Aspect);
+                     end if;
+                  end if;
+               end if;
+            end Analyze_Aspect_Static;
+
             -----------------------
             -- Make_Aitem_Pragma --
             -----------------------
@@ -4057,6 +4183,12 @@ package body Sem_Ch13 is
                   elsif A_Id = Aspect_Disable_Controlled then
                      Analyze_Aspect_Disable_Controlled;
                      goto Continue;
+
+                  --  Ada 202x (AI12-0075): static expression functions
+
+                  elsif A_Id = Aspect_Static then
+                     Analyze_Aspect_Static;
+                     goto Continue;
                   end if;
 
                   --  Library unit aspects require special handling in the case
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index b60133a..d0d13dd 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -552,6 +552,37 @@ package body Sem_Ch6 is
                   Check_Limited_Return (Original_Node (N), Expr, Typ);
                   End_Scope;
                end if;
+
+               --  In the case of an expression function marked with the
+               --  aspect Static, we need to check the requirement that the
+               --  function's expression is a potentially static expression.
+               --  This is done by making a full copy of the expression tree
+               --  and performing a special preanalysis on that tree with
+               --  the global flag Checking_Potentially_Static_Expression
+               --  enabled. If the resulting expression is static, then it's
+               --  OK, but if not, that means the expression violates the
+               --  requirements of the Ada 202x RM in 4.9(3.2/5-3.4/5) and
+               --  we flag an error.
+
+               if Is_Static_Expression_Function (Def_Id) then
+                  if not Is_Static_Expression (Expr) then
+                     declare
+                        Exp_Copy : constant Node_Id := New_Copy_Tree (Expr);
+                     begin
+                        Set_Checking_Potentially_Static_Expression (True);
+
+                        Preanalyze_Formal_Expression (Exp_Copy, Typ);
+
+                        if not Is_Static_Expression (Exp_Copy) then
+                           Error_Msg_N
+                             ("static expression function requires "
+                                & "potentially static expression", Expr);
+                        end if;
+
+                        Set_Checking_Potentially_Static_Expression (False);
+                     end;
+                  end if;
+               end if;
             end if;
          end;
       end if;
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 8aa1ca7..50f0feb 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -3685,6 +3685,11 @@ package body Sem_Elab is
       then
          return;
 
+      --  Static expression functions require no ABE processing
+
+      elsif Is_Static_Expression_Function (Subp_Id) then
+         return;
+
       --  Source calls to source targets are always considered because they
       --  reflect the original call graph.
 
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index 077e59d..8fc90a5 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -131,6 +131,11 @@ package body Sem_Eval is
    --  Range membership may either be statically known to be in range or out
    --  of range, or not statically known. Used for Test_In_Range below.
 
+   Checking_For_Potentially_Static_Expression : Boolean := False;
+   --  Global flag that is set True during Analyze_Static_Expression_Function
+   --  in order to verify that the result expression of a static expression
+   --  function is a potentially static function (see RM202x 6.8(5.3)).
+
    -----------------------
    -- Local Subprograms --
    -----------------------
@@ -639,6 +644,15 @@ package body Sem_Eval is
       end if;
    end Check_String_Literal_Length;
 
+   --------------------------------------------
+   -- Checking_Potentially_Static_Expression --
+   --------------------------------------------
+
+   function Checking_Potentially_Static_Expression return Boolean is
+   begin
+      return Checking_For_Potentially_Static_Expression;
+   end Checking_Potentially_Static_Expression;
+
    --------------------
    -- Choice_Matches --
    --------------------
@@ -2224,6 +2238,38 @@ package body Sem_Eval is
 
             Resolve (N, Typ);
          end if;
+
+      --  Ada 202x (AI12-0075): If checking for potentially static expressions
+      --  is enabled and we have a call to a static expression function,
+      --  substitute a static value for the call, to allow folding the
+      --  expression. This supports checking the requirement of RM 6.8(5.3/5)
+      --  in Analyze_Expression_Function.
+
+      elsif Checking_Potentially_Static_Expression
+        and then Is_Static_Expression_Function_Call (N)
+      then
+         if Is_Integer_Type (Typ) then
+            Fold_Uint (N, Uint_1, Static => True);
+            return;
+
+         elsif Is_Real_Type (Typ) then
+            Fold_Ureal (N, Ureal_1, Static => True);
+            return;
+
+         elsif Is_Enumeration_Type (Typ) then
+            Fold_Uint
+              (N,
+               Expr_Value (Type_Low_Bound (Base_Type (Typ))),
+               Static => True);
+            return;
+
+         elsif Is_String_Type (Typ) then
+            Fold_Str
+              (N,
+               Strval (Make_String_Literal (Sloc (N), "")),
+               Static => True);
+            return;
+         end if;
       end if;
    end Eval_Call;
 
@@ -2504,6 +2550,39 @@ package body Sem_Eval is
 
             return;
          end if;
+
+      --  Ada 202x (AI12-0075): If checking for potentially static expressions
+      --  is enabled and we have a reference to a formal parameter of mode in,
+      --  substitute a static value for the reference, to allow folding the
+      --  expression. This supports checking the requirement of RM 6.8(5.3/5)
+      --  in Analyze_Expression_Function.
+
+      elsif Ekind (Def_Id) = E_In_Parameter
+        and then Checking_Potentially_Static_Expression
+        and then Is_Static_Expression_Function (Scope (Def_Id))
+      then
+         if Is_Integer_Type (Etype (Def_Id)) then
+            Fold_Uint (N, Uint_1, Static => True);
+            return;
+
+         elsif Is_Real_Type (Etype (Def_Id)) then
+            Fold_Ureal (N, Ureal_1, Static => True);
+            return;
+
+         elsif Is_Enumeration_Type (Etype (Def_Id)) then
+            Fold_Uint
+              (N,
+               Expr_Value (Type_Low_Bound (Base_Type (Etype (Def_Id)))),
+               Static => True);
+            return;
+
+         elsif Is_String_Type (Etype (Def_Id)) then
+            Fold_Str
+              (N,
+               Strval (Make_String_Literal (Sloc (N), "")),
+               Static => True);
+            return;
+         end if;
       end if;
 
       --  Fall through if the name is not static
@@ -5934,6 +6013,21 @@ package body Sem_Eval is
       Set_Is_Static_Expression (N, Stat);
    end Rewrite_In_Raise_CE;
 
+   ------------------------------------------------
+   -- Set_Checking_Potentially_Static_Expression --
+   ------------------------------------------------
+
+   procedure Set_Checking_Potentially_Static_Expression (Value : Boolean) is
+   begin
+      --  Verify that we're not currently checking for a potentially static
+      --  expression unless we're disabling such checking.
+
+      pragma Assert
+        (not Checking_For_Potentially_Static_Expression or else not Value);
+
+      Checking_For_Potentially_Static_Expression := Value;
+   end Set_Checking_Potentially_Static_Expression;
+
    ---------------------
    -- String_Type_Len --
    ---------------------
diff --git a/gcc/ada/sem_eval.ads b/gcc/ada/sem_eval.ads
index 6f2c8d4..97160ee 100644
--- a/gcc/ada/sem_eval.ads
+++ b/gcc/ada/sem_eval.ads
@@ -165,6 +165,14 @@ package Sem_Eval is
    --  In the former case, if the target type, Ttyp is constrained, then a
    --  check is made to see if the string literal is of appropriate length.
 
+   function Checking_Potentially_Static_Expression return Boolean;
+   --  Returns True if the checking for potentially static expressions is
+   --  enabled; otherwise returns False.
+
+   procedure Set_Checking_Potentially_Static_Expression (Value : Boolean);
+   --  Enables checking for potentially static expressions if Value is True,
+   --  and disables such checking if Value is False.
+
    type Compare_Result is (LT, LE, EQ, GT, GE, NE, Unknown);
    subtype Compare_GE is Compare_Result range EQ .. GE;
    subtype Compare_LE is Compare_Result range LT .. EQ;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index bdd954f..ee3a9ac 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6560,6 +6560,7 @@ package body Sem_Res is
 
          if Same_Or_Aliased_Subprograms (Nam, Scop)
            and then not Restriction_Active (No_Recursion)
+           and then not Is_Static_Expression_Function (Scop)
            and then Check_Infinite_Recursion (N)
          then
             --  Here we detected and flagged an infinite recursion, so we do
@@ -6577,6 +6578,20 @@ package body Sem_Res is
             Scope_Loop : while Scop /= Standard_Standard loop
                if Same_Or_Aliased_Subprograms (Nam, Scop) then
 
+                  --  Ada 202x (AI12-0075): Static expression function are
+                  --  never allowed to make a recursive call, as specified
+                  --  by 6.8(5.4/5).
+
+                  if Is_Static_Expression_Function (Scop) then
+                     Error_Msg_N
+                       ("recursive call not allowed in static expression "
+                          & "function", N);
+
+                     Set_Error_Posted (Scop);
+
+                     exit Scope_Loop;
+                  end if;
+
                   --  Although in general case, recursion is not statically
                   --  checkable, the case of calling an immediately containing
                   --  subprogram is easy to catch.
@@ -6714,6 +6729,11 @@ package body Sem_Res is
       --  is already present. It may not be available if e.g. the subprogram is
       --  declared in a child instance.
 
+      --  g) If the subprogram is a static expression function and the call is
+      --  a static call (the actuals are all static expressions), then we never
+      --  want to create a transient scope (this could occur in the case of a
+      --  static string-returning call).
+
       if Is_Inlined (Nam)
         and then Has_Pragma_Inline (Nam)
         and then Nkind (Unit_Declaration_Node (Nam)) = N_Subprogram_Declaration
@@ -6725,6 +6745,7 @@ package body Sem_Res is
         or else Is_Build_In_Place_Function (Nam)
         or else Is_Intrinsic_Subprogram (Nam)
         or else Is_Inlinable_Expression_Function (Nam)
+        or else Is_Static_Expression_Function_Call (N)
       then
          null;
 
@@ -6989,12 +7010,26 @@ package body Sem_Res is
 
       Warn_On_Overlapping_Actuals (Nam, N);
 
+      --  Ada 202x (AI12-0075): If the call is a static call to a static
+      --  expression function, then we want to "inline" the call, replacing
+      --  it with the folded static result. This is not done if the checking
+      --  for a potentially static expression is enabled or if an error has
+      --  been posted on the call (which may be due to the check for recursive
+      --  calls, in which case we don't want to fall into infinite recursion
+      --  when doing the inlining).
+
+      if not Checking_Potentially_Static_Expression
+        and then Is_Static_Expression_Function_Call (N)
+        and then not Error_Posted (Ultimate_Alias (Nam))
+      then
+         Inline_Static_Expression_Function_Call (N, Ultimate_Alias (Nam));
+
       --  In GNATprove mode, expansion is disabled, but we want to inline some
       --  subprograms to facilitate formal verification. Indirect calls through
       --  a subprogram type or within a generic cannot be inlined. Inlining is
       --  performed only for calls subject to SPARK_Mode on.
 
-      if GNATprove_Mode
+      elsif GNATprove_Mode
         and then SPARK_Mode = On
         and then Is_Overloadable (Nam)
         and then not Inside_A_Generic
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 43bffc9..5f15107 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5846,7 +5846,14 @@ package body Sem_Util is
          --  will happen when something is evaluated if it never will be
          --  evaluated.
 
-         if not Is_Statically_Unevaluated (N) then
+         --  Suppress error reporting when checking that the expression of a
+         --  static expression function is a potentially static expression,
+         --  because we don't want additional errors being reported during the
+         --  preanalysis of the expression (see Analyze_Expression_Function).
+
+         if not Is_Statically_Unevaluated (N)
+           and then not Checking_Potentially_Static_Expression
+         then
             if Present (Ent) then
                Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
             else
@@ -18442,6 +18449,73 @@ package body Sem_Util is
           or else Nkind (N) = N_Procedure_Call_Statement;
    end Is_Statement;
 
+   ------------------------------------
+   --  Is_Static_Expression_Function --
+   ------------------------------------
+
+   function Is_Static_Expression_Function (Subp : Entity_Id) return Boolean is
+   begin
+      return Is_Expression_Function (Subp)
+        and then Has_Aspect (Subp, Aspect_Static)
+        and then
+          (No (Find_Value_Of_Aspect (Subp, Aspect_Static))
+            or else Is_True (Static_Boolean
+                               (Find_Value_Of_Aspect (Subp, Aspect_Static))));
+   end Is_Static_Expression_Function;
+
+   -----------------------------------------
+   --  Is_Static_Expression_Function_Call --
+   -----------------------------------------
+
+   function Is_Static_Expression_Function_Call (Call : Node_Id) return Boolean
+   is
+
+      function Has_All_Static_Actuals (Call : Node_Id) return Boolean;
+      --  Return whether all actual parameters of Call are static expressions
+
+      function Has_All_Static_Actuals (Call : Node_Id) return Boolean is
+         Actual        : Node_Id := First_Actual (Call);
+         String_Result : constant Boolean :=
+                           Is_String_Type (Etype (Entity (Name (Call))));
+
+      begin
+         while Present (Actual) loop
+            if not Is_Static_Expression (Actual) then
+
+               --  ??? In the string-returning case we want to avoid a call
+               --  being made to Establish_Transient_Scope in Resolve_Call,
+               --  but at the point where that's tested for (which now includes
+               --  a call to test Is_Static_Expression_Function_Call), the
+               --  actuals of the call haven't been resolved, so expressions
+               --  of the actuals may not have been marked Is_Static_Expression
+               --  yet, so we force them to be resolved here, so we can tell if
+               --  they're static. Calling Resolve here is admittedly a kludge,
+               --  and we limit this call to string-returning cases. ???
+
+               if String_Result then
+                  Resolve (Actual);
+               end if;
+
+               --  Test flag again in case it's now True due to above Resolve
+
+               if not Is_Static_Expression (Actual) then
+                  return False;
+               end if;
+            end if;
+
+            Next_Actual (Actual);
+         end loop;
+
+         return True;
+      end Has_All_Static_Actuals;
+
+   begin
+      return Nkind (Call) = N_Function_Call
+        and then Is_Entity_Name (Name (Call))
+        and then Is_Static_Expression_Function (Entity (Name (Call)))
+        and then Has_All_Static_Actuals (Call);
+   end Is_Static_Expression_Function_Call;
+
    ----------------------------------------
    --  Is_Subcomponent_Of_Atomic_Object  --
    ----------------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 6cd626e..caefa05 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2070,6 +2070,15 @@ package Sem_Util is
    --  the N_Statement_Other_Than_Procedure_Call subtype from Sinfo).
    --  Note that a label is *not* a statement, and will return False.
 
+   function Is_Static_Expression_Function (Subp : Entity_Id) return Boolean;
+   --  Determine whether subprogram Subp denotes a static expression function,
+   --  which is an expression function with the aspect Static with value True.
+
+   function Is_Static_Expression_Function_Call (Call : Node_Id) return Boolean;
+   --  Determine whether Call is a static call to a static expression function,
+   --  meaning that the name of the call denotes a static expression function
+   --  and all of the call's actual parameters are given by static expressions.
+
    function Is_Subcomponent_Of_Atomic_Object (N : Node_Id) return Boolean;
    --  Determine whether arbitrary node N denotes a reference to a subcomponent
    --  of an atomic object as per RM C.6(7).