From 995d28c7551ce6a65bd34355169106aab9ee65b6 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 9 Jul 2019 07:53:45 +0000 Subject: [PATCH] [Ada] Handle implicit moves in SPARK ownership pointer support Allocator expressions and sub-expressions of (extension) aggregates are implicitly the source of assignments in Ada. Thus, they should be moved when of a deep type when checking ownership rules in SPARK. There is no impact on compilation. 2019-07-09 Yannick Moy gcc/ada/ * sem_spark.adb (Check_Expression): Handle correctly implicit assignments as part of allocators and (extension) aggregates. (Get_Root_Object): Adapt for new path expressions. (Is_Path_Expression): Return True for (extension) aggregate. From-SVN: r273271 --- gcc/ada/ChangeLog | 7 ++ gcc/ada/sem_spark.adb | 208 ++++++++++++++++++++++++++++++++---------- 2 files changed, 167 insertions(+), 48 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c0ba4af07b8..86b02b36cb4 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2019-07-09 Yannick Moy + + * sem_spark.adb (Check_Expression): Handle correctly implicit + assignments as part of allocators and (extension) aggregates. + (Get_Root_Object): Adapt for new path expressions. + (Is_Path_Expression): Return True for (extension) aggregate. + 2019-07-09 Piotr Trojanek * einfo.ads: Fix a typo. diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 6f27d20452d..bbd727987c6 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -1436,6 +1436,13 @@ package body Sem_SPARK is function Is_Type_Name (Expr : Node_Id) return Boolean; -- Detect when a path expression is in fact a type name + procedure Move_Expression (Expr : Node_Id); + -- Some subexpressions are only analyzed in Move mode. This is a + -- specialized version of Check_Expression for that case. + + procedure Move_Expression_List (L : List_Id); + -- Call Move_Expression on every expression in the list L + procedure Read_Expression (Expr : Node_Id); -- Most subexpressions are only analyzed in Read mode. This is a -- specialized version of Check_Expression for that case. @@ -1458,6 +1465,36 @@ package body Sem_SPARK is and then Is_Type (Entity (Expr)); end Is_Type_Name; + --------------------- + -- Move_Expression -- + --------------------- + + -- Distinguish the case where the argument is a path expression that + -- needs explicit moving. + + procedure Move_Expression (Expr : Node_Id) is + begin + if Is_Path_Expression (Expr) then + Check_Expression (Expr, Move); + else + Read_Expression (Expr); + end if; + end Move_Expression; + + -------------------------- + -- Move_Expression_List -- + -------------------------- + + procedure Move_Expression_List (L : List_Id) is + N : Node_Id; + begin + N := First (L); + while Present (N) loop + Move_Expression (N); + Next (N); + end loop; + end Move_Expression_List; + --------------------- -- Read_Expression -- --------------------- @@ -1489,7 +1526,26 @@ package body Sem_SPARK is -- Local subprograms + function Is_Singleton_Choice (Choices : List_Id) return Boolean; + -- Return whether Choices is a singleton choice + procedure Read_Param (Formal : Entity_Id; Actual : Node_Id); + -- Call Read_Expression on the actual + + ------------------------- + -- Is_Singleton_Choice -- + ------------------------- + + function Is_Singleton_Choice (Choices : List_Id) return Boolean is + Choice : constant Node_Id := First (Choices); + begin + return List_Length (Choices) = 1 + and then Nkind (Choice) /= N_Others_Choice + and then not Nkind_In (Choice, N_Subtype_Indication, N_Range) + and then not + (Nkind_In (Choice, N_Identifier, N_Expanded_Name) + and then Is_Type (Entity (Choice))); + end Is_Singleton_Choice; ---------------- -- Read_Param -- @@ -1526,8 +1582,11 @@ package body Sem_SPARK is Read_Indexes (Prefix (Expr)); Read_Expression (Discrete_Range (Expr)); + -- The argument of an allocator is moved as part of the implicit + -- assignment. + when N_Allocator => - Read_Expression (Expression (Expr)); + Move_Expression (Expression (Expr)); when N_Function_Call => Read_Params (Expr); @@ -1539,6 +1598,91 @@ package body Sem_SPARK is => Read_Indexes (Expression (Expr)); + when N_Aggregate => + declare + Assocs : constant List_Id := Component_Associations (Expr); + CL : List_Id; + Assoc : Node_Id := Nlists.First (Assocs); + Choice : Node_Id; + + begin + -- The subexpressions of an aggregate are moved as part + -- of the implicit assignments. Handle the positional + -- components first. + + Move_Expression_List (Expressions (Expr)); + + -- Handle the named components next. + + while Present (Assoc) loop + CL := Choices (Assoc); + + -- For an array aggregate, we should also check that the + -- expressions used in choices are readable. + + if Is_Array_Type (Etype (Expr)) then + Choice := Nlists.First (CL); + while Present (Choice) loop + if Nkind (Choice) /= N_Others_Choice then + Read_Expression (Choice); + end if; + Next (Choice); + end loop; + end if; + + -- There can be only one element for a value of deep type + -- in order to avoid aliasing. + + if Is_Deep (Etype (Expression (Assoc))) + and then not Is_Singleton_Choice (CL) + then + Error_Msg_F ("singleton choice required" + & " to prevent aliasing", First (CL)); + end if; + + -- The subexpressions of an aggregate are moved as part + -- of the implicit assignments. + + Move_Expression (Expression (Assoc)); + + Next (Assoc); + end loop; + end; + + when N_Extension_Aggregate => + declare + Exprs : constant List_Id := Expressions (Expr); + Assocs : constant List_Id := Component_Associations (Expr); + CL : List_Id; + Assoc : Node_Id := Nlists.First (Assocs); + + begin + Move_Expression (Ancestor_Part (Expr)); + + -- No positional components allowed at this stage + + if Present (Exprs) then + raise Program_Error; + end if; + + while Present (Assoc) loop + CL := Choices (Assoc); + + -- Only singleton components allowed at this stage + + if not Is_Singleton_Choice (CL) then + raise Program_Error; + end if; + + -- The subexpressions of an aggregate are moved as part + -- of the implicit assignments. + + Move_Expression (Expression (Assoc)); + + Next (Assoc); + end loop; + end; + when others => raise Program_Error; end case; @@ -1759,45 +1903,6 @@ package body Sem_SPARK is Read_Expression (Condition (Expr)); end; - when N_Aggregate => - declare - Assocs : constant List_Id := Component_Associations (Expr); - Assoc : Node_Id := First (Assocs); - CL : List_Id; - Choice : Node_Id; - - begin - while Present (Assoc) loop - - -- An array aggregate with a single component association - -- may have a nonstatic choice expression that needs to be - -- analyzed. This can only occur for a single choice that - -- is not the OTHERS one. - - if Is_Array_Type (Etype (Expr)) then - CL := Choices (Assoc); - if List_Length (CL) = 1 then - Choice := First (CL); - if Nkind (Choice) /= N_Others_Choice then - Read_Expression (Choice); - end if; - end if; - end if; - - -- The expression in the component association also needs to - -- be analyzed. - - Read_Expression (Expression (Assoc)); - Next (Assoc); - end loop; - - Read_Expression_List (Expressions (Expr)); - end; - - when N_Extension_Aggregate => - Read_Expression (Ancestor_Part (Expr)); - Read_Expression_List (Expressions (Expr)); - when N_Character_Literal | N_Numeric_Or_String_Literal | N_Operator_Symbol @@ -1818,9 +1923,11 @@ package body Sem_SPARK is -- Path expressions are handled before this point - when N_Allocator + when N_Aggregate + | N_Allocator | N_Expanded_Name | N_Explicit_Dereference + | N_Extension_Aggregate | N_Function_Call | N_Identifier | N_Indexed_Component @@ -3283,7 +3390,7 @@ package body Sem_SPARK is return (R => Unfolded, Tree_Access => C); end; - -- For a non-terminal path, we get the permission tree of its + -- For a nonterminal path, we get the permission tree of its -- prefix, and then get the subtree associated with the extension, -- if unfolded. If folded, we return the permission associated with -- children. @@ -3389,9 +3496,12 @@ package body Sem_SPARK is => return Get_Root_Object (Prefix (Expr), Through_Traversal); - -- There is no root object for an allocator or NULL + -- There is no root object for an (extension) aggregate, allocator, + -- or NULL. - when N_Allocator + when N_Aggregate + | N_Allocator + | N_Extension_Aggregate | N_Null => return Empty; @@ -3596,10 +3706,12 @@ package body Sem_SPARK is when N_Null => return True; - -- Object returned by a allocator or function call corresponds to - -- a path. + -- Object returned by an (extension) aggregate, an allocator, or + -- a function call corresponds to a path. - when N_Allocator + when N_Aggregate + | N_Allocator + | N_Extension_Aggregate | N_Function_Call => return True; @@ -4763,7 +4875,7 @@ package body Sem_SPARK is return C; end; - -- For a non-terminal path, we set the permission tree of its prefix, + -- For a nonterminal path, we set the permission tree of its prefix, -- and then we extract from the returned pointer the subtree and -- assign an adequate permission to it, if unfolded. If folded, -- we unroll the tree one level. -- 2.30.2