From 05b77088c086863aa3e5c0456b9a0c0075e05a6d Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 14 Aug 2019 09:51:21 +0000 Subject: [PATCH] [Ada] Check SPARK restriction on Old/Loop_Entry with pointers --#! r336866 --#! no-mail SPARK RM rule 3.10(14) restricts the use of Old and Loop_Entry attributes on prefixes of an owning or observing type (i.e. a type with access inside). There is no impact on compilation. 2019-08-14 Yannick Moy gcc/ada/ * sem_spark.adb (Check_Old_Loop_Entry): New procedure to check correct use of Old and Loop_Entry. (Check_Node): Check subprogram contracts. (Check_Pragma): Check Loop_Variant. (Check_Safe_Pointers): Apply checking to library-level subprogram declarations as well, in order to check their contract. From-SVN: r274453 --- gcc/ada/ChangeLog | 10 ++++ gcc/ada/sem_spark.adb | 125 ++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 130 insertions(+), 5 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 250d174b032..cef5e8cc5a0 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2019-08-14 Yannick Moy + + * sem_spark.adb (Check_Old_Loop_Entry): New procedure to check + correct use of Old and Loop_Entry. + (Check_Node): Check subprogram contracts. + (Check_Pragma): Check Loop_Variant. + (Check_Safe_Pointers): Apply checking to library-level + subprogram declarations as well, in order to check their + contract. + 2019-08-14 Yannick Moy * sem_spark.adb (Is_Subpath_Expression): Take into account diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 542f694978b..37c6b4d1e03 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -663,6 +663,9 @@ package body Sem_SPARK is procedure Check_Node (N : Node_Id); -- Main traversal procedure to check safe pointer usage + procedure Check_Old_Loop_Entry (N : Node_Id); + -- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry + procedure Check_Package_Body (Pack : Node_Id); procedure Check_Package_Spec (Pack : Node_Id); @@ -2583,6 +2586,43 @@ package body Sem_SPARK is ---------------- procedure Check_Node (N : Node_Id) is + + procedure Check_Subprogram_Contract (N : Node_Id); + -- Check the postcondition-like contracts for use of 'Old + + ------------------------------- + -- Check_Subprogram_Contract -- + ------------------------------- + + procedure Check_Subprogram_Contract (N : Node_Id) is + begin + if Nkind (N) = N_Subprogram_Declaration + or else Acts_As_Spec (N) + then + declare + E : constant Entity_Id := Unique_Defining_Entity (N); + Post : constant Node_Id := + Get_Pragma (E, Pragma_Postcondition); + Cases : constant Node_Id := + Get_Pragma (E, Pragma_Contract_Cases); + begin + Check_Old_Loop_Entry (Post); + Check_Old_Loop_Entry (Cases); + end; + + elsif Nkind (N) = N_Subprogram_Body then + declare + E : constant Entity_Id := Defining_Entity (N); + Ref_Post : constant Node_Id := + Get_Pragma (E, Pragma_Refined_Post); + begin + Check_Old_Loop_Entry (Ref_Post); + end; + end if; + end Check_Subprogram_Contract; + + -- Start of processing for Check_Node + begin case Nkind (N) is when N_Declaration => @@ -2602,14 +2642,17 @@ package body Sem_SPARK is Check_Package_Body (N); end if; - when N_Subprogram_Body - | N_Entry_Body - | N_Task_Body - => + when N_Subprogram_Body => if not Is_Generic_Unit (Unique_Defining_Entity (N)) then + Check_Subprogram_Contract (N); Check_Callable_Body (N); end if; + when N_Entry_Body + | N_Task_Body + => + Check_Callable_Body (N); + when N_Protected_Body => Check_List (Declarations (N)); @@ -2622,6 +2665,9 @@ package body Sem_SPARK is when N_Pragma => Check_Pragma (N); + when N_Subprogram_Declaration => + Check_Subprogram_Contract (N); + -- Ignored constructs for pointer checking when N_Abstract_Subprogram_Declaration @@ -2655,7 +2701,6 @@ package body Sem_SPARK is | N_Procedure_Instantiation | N_Raise_xxx_Error | N_Record_Representation_Clause - | N_Subprogram_Declaration | N_Subprogram_Renaming_Declaration | N_Task_Type_Declaration | N_Use_Package_Clause @@ -2677,6 +2722,65 @@ package body Sem_SPARK is end case; end Check_Node; + -------------------------- + -- Check_Old_Loop_Entry -- + -------------------------- + + procedure Check_Old_Loop_Entry (N : Node_Id) is + + function Check_Attribute (N : Node_Id) return Traverse_Result; + + --------------------- + -- Check_Attribute -- + --------------------- + + function Check_Attribute (N : Node_Id) return Traverse_Result is + Attr_Id : Attribute_Id; + Aname : Name_Id; + Pref : Node_Id; + + begin + if Nkind (N) = N_Attribute_Reference then + Attr_Id := Get_Attribute_Id (Attribute_Name (N)); + Aname := Attribute_Name (N); + + if Attr_Id = Attribute_Old + or else Attr_Id = Attribute_Loop_Entry + then + Pref := Prefix (N); + + if Is_Deep (Etype (Pref)) then + if Nkind (Pref) /= N_Function_Call then + if Emit_Messages then + Error_Msg_Name_1 := Aname; + Error_Msg_N + ("prefix of % attribute must be a function call " + & "(SPARK RM 3.10(14))", Pref); + end if; + + elsif Is_Traversal_Function_Call (Pref) then + if Emit_Messages then + Error_Msg_Name_1 := Aname; + Error_Msg_N + ("prefix of % attribute should not call a traversal " + & "function (SPARK RM 3.10(14))", Pref); + end if; + end if; + end if; + end if; + end if; + + return OK; + end Check_Attribute; + + procedure Check_All is new Traverse_Proc (Check_Attribute); + + -- Start of processing for Check_Old_Loop_Entry + + begin + Check_All (N); + end Check_Old_Loop_Entry; + ------------------------ -- Check_Package_Body -- ------------------------ @@ -2869,8 +2973,18 @@ package body Sem_SPARK is Expr : constant Node_Id := Expression (Arg2); begin Check_Expression (Expr, Read); + + -- Prefix of Loop_Entry should be checked inside any assertion + -- where it may appear. + + Check_Old_Loop_Entry (Expr); end; + -- Prefix of Loop_Entry should be checked inside a Loop_Variant + + when Pragma_Loop_Variant => + Check_Old_Loop_Entry (Prag); + -- There is no need to check contracts, as these can only access -- inputs and outputs of the subprogram. Inputs are checked -- independently for R permission. Outputs are checked @@ -2963,6 +3077,7 @@ package body Sem_SPARK is when N_Package_Body | N_Package_Declaration + | N_Subprogram_Declaration | N_Subprogram_Body => declare