From a211917585ca978a84123c4c934f2f68bb545bcd Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 22 Jul 2019 13:58:23 +0000 Subject: [PATCH] [Ada] Adapt ownership checking in SPARK to traversal functions A traversal function, especially when implemented as an expression function, may need to return an if-expression or case-expression, while still respecting Legality Rule SPARK RM 3.10(5). This case is now allowed in GNATprove. There is no impact on compilation. 2019-07-22 Yannick Moy gcc/ada/ * sem_spark.adb (Get_Root_Object, Is_Path_Expression, Is_Subpath_Expression): Add parameter Is_Traversal to adapt these functions to the case of paths returned from a traversal function. (Read_Indexes): Handle the case of an if-expression or case-expression. (Check_Statement): Check Emit_Messages only when issuing an error message. This is important as Emit_Messages may store the information that an error was detected. From-SVN: r273693 --- gcc/ada/ChangeLog | 12 +++ gcc/ada/sem_spark.adb | 223 ++++++++++++++++++++++++++++++++++++++---- 2 files changed, 217 insertions(+), 18 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8bb8d34f305..17d21f54306 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2019-07-22 Yannick Moy + + * sem_spark.adb (Get_Root_Object, Is_Path_Expression, + Is_Subpath_Expression): Add parameter Is_Traversal to adapt + these functions to the case of paths returned from a traversal + function. + (Read_Indexes): Handle the case of an if-expression or + case-expression. + (Check_Statement): Check Emit_Messages only when issuing an + error message. This is important as Emit_Messages may store the + information that an error was detected. + 2019-07-22 Eric Botcazou * checks.adb (Apply_Type_Conversion_Checks): Do not set diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 67aa4537c1d..0de51f866fa 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -715,10 +715,14 @@ package body Sem_SPARK is function Get_Root_Object (Expr : Node_Id; - Through_Traversal : Boolean := True) return Entity_Id; + Through_Traversal : Boolean := True; + Is_Traversal : Boolean := False) return Entity_Id; -- Return the root of the path expression Expr, or Empty for an allocator, -- NULL, or a function call. Through_Traversal is True if it should follow - -- through calls to traversal functions. + -- through calls to traversal functions. Is_Traversal is True if this + -- corresponds to a value returned from a traversal function, which should + -- allow if-expressions and case-expressions that refer to the same root, + -- even if the paths are not the same in all branches. generic with procedure Handle_Parameter_Or_Global @@ -745,11 +749,19 @@ package body Sem_SPARK is -- A procedure that is called when deep globals or aliased globals are used -- without any global aspect. - function Is_Path_Expression (Expr : Node_Id) return Boolean; - -- Return whether Expr corresponds to a path + function Is_Path_Expression + (Expr : Node_Id; + Is_Traversal : Boolean := False) return Boolean; + -- Return whether Expr corresponds to a path. Is_Traversal is True if this + -- corresponds to a value returned from a traversal function, which should + -- allow if-expressions and case-expressions. - function Is_Subpath_Expression (Expr : Node_Id) return Boolean; - -- Return True if Expr can be part of a path expression + function Is_Subpath_Expression + (Expr : Node_Id; + Is_Traversal : Boolean := False) return Boolean; + -- Return True if Expr can be part of a path expression. Is_Traversal is + -- True if this corresponds to a value returned from a traversal function, + -- which should allow if-expressions and case-expressions. function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean; -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost @@ -1749,6 +1761,31 @@ package body Sem_SPARK is end loop; end; + when N_If_Expression => + declare + Cond : constant Node_Id := First (Expressions (Expr)); + Then_Part : constant Node_Id := Next (Cond); + Else_Part : constant Node_Id := Next (Then_Part); + begin + Read_Expression (Cond); + Read_Indexes (Then_Part); + Read_Indexes (Else_Part); + end; + + when N_Case_Expression => + declare + Cases : constant List_Id := Alternatives (Expr); + Cur_Case : Node_Id := First (Cases); + + begin + Read_Expression (Expression (Expr)); + + while Present (Cur_Case) loop + Read_Indexes (Expression (Cur_Case)); + Next (Cur_Case); + end loop; + end; + when N_Attribute_Reference => pragma Assert (Get_Attribute_Id (Attribute_Name (Expr)) = @@ -3115,14 +3152,14 @@ package body Sem_SPARK is if Is_Anonymous_Access_Type (Return_Typ) then pragma Assert (Is_Traversal_Function (Subp)); - if Nkind (Expr) /= N_Null and then Emit_Messages then + if Nkind (Expr) /= N_Null then declare Expr_Root : constant Entity_Id := - Get_Root_Object (Expr); + Get_Root_Object (Expr, Is_Traversal => True); Param : constant Entity_Id := First_Formal (Subp); begin - if Param /= Expr_Root then + if Param /= Expr_Root and then Emit_Messages then Error_Msg_NE ("returned value must be rooted in " & "traversed parameter & " @@ -3642,10 +3679,31 @@ package body Sem_SPARK is function Get_Root_Object (Expr : Node_Id; - Through_Traversal : Boolean := True) return Entity_Id + Through_Traversal : Boolean := True; + Is_Traversal : Boolean := False) return Entity_Id is + function GRO (Expr : Node_Id) return Entity_Id; + -- Local wrapper on the actual function, to propagate the values of + -- optional parameters. + + --------- + -- GRO -- + --------- + + function GRO (Expr : Node_Id) return Entity_Id is + begin + return Get_Root_Object (Expr, Through_Traversal, Is_Traversal); + end GRO; + + Get_Root_Object : Boolean; + pragma Unmodified (Get_Root_Object); + -- Local variable to mask the name of function Get_Root_Object, to + -- prevent direct call. Instead GRO wrapper should be called. + + -- Start of processing for Get_Root_Object + begin - if not Is_Subpath_Expression (Expr) then + if not Is_Subpath_Expression (Expr, Is_Traversal) then if Emit_Messages then Error_Msg_N ("name expected here for path", Expr); end if; @@ -3663,7 +3721,7 @@ package body Sem_SPARK is | N_Selected_Component | N_Slice => - return Get_Root_Object (Prefix (Expr), Through_Traversal); + return GRO (Prefix (Expr)); -- There is no root object for an (extension) aggregate, allocator, -- concat, or NULL. @@ -3684,7 +3742,7 @@ package body Sem_SPARK is if Through_Traversal and then Is_Traversal_Function_Call (Expr) then - return Get_Root_Object (First_Actual (Expr), Through_Traversal); + return GRO (First_Actual (Expr)); else return Empty; end if; @@ -3693,7 +3751,7 @@ package body Sem_SPARK is | N_Type_Conversion | N_Unchecked_Type_Conversion => - return Get_Root_Object (Expression (Expr), Through_Traversal); + return GRO (Expression (Expr)); when N_Attribute_Reference => pragma Assert @@ -3706,6 +3764,69 @@ package body Sem_SPARK is Attribute_Image); return Empty; + when N_If_Expression => + if Is_Traversal then + declare + Cond : constant Node_Id := First (Expressions (Expr)); + Then_Part : constant Node_Id := Next (Cond); + Else_Part : constant Node_Id := Next (Then_Part); + Then_Root : constant Entity_Id := GRO (Then_Part); + Else_Root : constant Entity_Id := GRO (Else_Part); + begin + if Nkind (Then_Part) = N_Null then + return Else_Root; + elsif Nkind (Else_Part) = N_Null then + return Then_Part; + elsif Then_Root = Else_Root then + return Then_Root; + else + if Emit_Messages then + Error_Msg_N + ("same name expected here in each branch", Expr); + end if; + return Empty; + end if; + end; + else + if Emit_Messages then + Error_Msg_N ("name expected here for path", Expr); + end if; + return Empty; + end if; + + when N_Case_Expression => + if Is_Traversal then + declare + Cases : constant List_Id := Alternatives (Expr); + Cur_Case : Node_Id := First (Cases); + Cur_Root : Entity_Id; + Common_Root : Entity_Id := Empty; + + begin + while Present (Cur_Case) loop + Cur_Root := GRO (Expression (Cur_Case)); + + if Common_Root = Empty then + Common_Root := Cur_Root; + elsif Common_Root /= Cur_Root then + if Emit_Messages then + Error_Msg_N + ("same name expected here in each branch", Expr); + end if; + return Empty; + end if; + Next (Cur_Case); + end loop; + + return Common_Root; + end; + else + if Emit_Messages then + Error_Msg_N ("name expected here for path", Expr); + end if; + return Empty; + end if; + when others => raise Program_Error; end case; @@ -3876,7 +3997,30 @@ package body Sem_SPARK is -- Is_Path_Expression -- ------------------------ - function Is_Path_Expression (Expr : Node_Id) return Boolean is + function Is_Path_Expression + (Expr : Node_Id; + Is_Traversal : Boolean := False) return Boolean + is + function IPE (Expr : Node_Id) return Boolean; + -- Local wrapper on the actual function, to propagate the values of + -- optional parameter Is_Traversal. + + --------- + -- IPE -- + --------- + + function IPE (Expr : Node_Id) return Boolean is + begin + return Is_Path_Expression (Expr, Is_Traversal); + end IPE; + + Is_Path_Expression : Boolean; + pragma Unmodified (Is_Path_Expression); + -- Local variable to mask the name of function Is_Path_Expression, to + -- prevent direct call. Instead IPE wrapper should be called. + + -- Start of processing for Is_Path_Expression + begin case Nkind (Expr) is when N_Expanded_Name @@ -3907,7 +4051,47 @@ package body Sem_SPARK is | N_Type_Conversion | N_Unchecked_Type_Conversion => - return Is_Path_Expression (Expression (Expr)); + return IPE (Expression (Expr)); + + -- When returning from a traversal function, consider an + -- if-expression as a possible path expression. + + when N_If_Expression => + if Is_Traversal then + declare + Cond : constant Node_Id := First (Expressions (Expr)); + Then_Part : constant Node_Id := Next (Cond); + Else_Part : constant Node_Id := Next (Then_Part); + begin + return IPE (Then_Part) + and then IPE (Else_Part); + end; + else + return False; + end if; + + -- When returning from a traversal function, consider + -- a case-expression as a possible path expression. + + when N_Case_Expression => + if Is_Traversal then + declare + Cases : constant List_Id := Alternatives (Expr); + Cur_Case : Node_Id := First (Cases); + + begin + while Present (Cur_Case) loop + if not IPE (Expression (Cur_Case)) then + return False; + end if; + Next (Cur_Case); + end loop; + + return True; + end; + else + return False; + end if; when others => return False; @@ -4033,9 +4217,12 @@ package body Sem_SPARK is -- Is_Subpath_Expression -- --------------------------- - function Is_Subpath_Expression (Expr : Node_Id) return Boolean is + function Is_Subpath_Expression + (Expr : Node_Id; + Is_Traversal : Boolean := False) return Boolean + is begin - return Is_Path_Expression (Expr) + return Is_Path_Expression (Expr, Is_Traversal) or else (Nkind (Expr) = N_Attribute_Reference and then (Get_Attribute_Id (Attribute_Name (Expr)) = -- 2.30.2