From e0201d823abfcbc3acadc1f78a0c94fdc8474dfe Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 9 Jul 2019 07:53:21 +0000 Subject: [PATCH] [Ada] Fix ownership checking for pointers in SPARK Checking of the readable status of sub-expressions occurring in the target path of an assignment should occur before the right-hand-side is moved or borrowed or observed. There is no impact on compilation. 2019-07-09 Yannick Moy gcc/ada/ * sem_spark.adb (Check_Expression): Change signature to take an Extended_Checking_Mode, for handling read permission checking of sub-expressions in an assignment. (Check_Parameter_Or_Global): Adapt to new behavior of Check_Expression for mode Assign. (Check_Safe_Pointers): Do not analyze generic bodies. (Check_Assignment): Separate checking of the target of an assignment. From-SVN: r273266 --- gcc/ada/ChangeLog | 11 +++++++ gcc/ada/sem_spark.adb | 74 +++++++++++++++++++++++++++++-------------- 2 files changed, 62 insertions(+), 23 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 02dc4ad71b8..9f6b789b983 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,14 @@ +2019-07-09 Yannick Moy + + * sem_spark.adb (Check_Expression): Change signature to take an + Extended_Checking_Mode, for handling read permission checking of + sub-expressions in an assignment. + (Check_Parameter_Or_Global): Adapt to new behavior of + Check_Expression for mode Assign. + (Check_Safe_Pointers): Do not analyze generic bodies. + (Check_Assignment): Separate checking of the target of an + assignment. + 2019-07-09 Eric Botcazou * repinfo.ads (JSON format): Adjust. diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index fb46e62296e..2b1991959ab 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -560,9 +560,13 @@ package body Sem_SPARK is -- has the right permission, and also updating permissions when a path is -- moved, borrowed, or observed. - type Checking_Mode is + type Extended_Checking_Mode is - (Read, + (Read_Subexpr, + -- Special value used for assignment, to check that subexpressions of + -- the assigned path are readable. + + Read, -- Default mode Move, @@ -591,6 +595,8 @@ package body Sem_SPARK is -- and extensions are set to Read_Only. ); + subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe; + type Result_Kind is (Folded, Unfolded); -- The type declaration to discriminate in the Perm_Or_Tree type @@ -631,7 +637,7 @@ package body Sem_SPARK is procedure Check_Declaration (Decl : Node_Id); - procedure Check_Expression (Expr : Node_Id; Mode : Checking_Mode); + procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode); pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint, N_Range_Constraint, N_Subtype_Indication) @@ -1421,8 +1427,10 @@ package body Sem_SPARK is -- Check_Expression -- ---------------------- - procedure Check_Expression (Expr : Node_Id; Mode : Checking_Mode) is - + procedure Check_Expression + (Expr : Node_Id; + Mode : Extended_Checking_Mode) + is -- Local subprograms function Is_Type_Name (Expr : Node_Id) return Boolean; @@ -1543,8 +1551,14 @@ package body Sem_SPARK is return; elsif Is_Path_Expression (Expr) then - Read_Indexes (Expr); - Process_Path (Expr, Mode); + if Mode /= Assign then + Read_Indexes (Expr); + end if; + + if Mode /= Read_Subexpr then + Process_Path (Expr, Mode); + end if; + return; end if; @@ -2511,6 +2525,10 @@ package body Sem_SPARK is Mode := Move; end case; + if Mode = Assign then + Check_Expression (Expr, Read_Subexpr); + end if; + Check_Expression (Expr, Mode); end Check_Parameter_Or_Global; @@ -2618,11 +2636,6 @@ package body Sem_SPARK is Reset (Current_Perm_Env); end Initialize; - -- Local variables - - Prag : Node_Id; - -- SPARK_Mode pragma in application - -- Start of processing for Check_Safe_Pointers begin @@ -2636,20 +2649,28 @@ package body Sem_SPARK is | N_Package_Declaration | N_Subprogram_Body => - Prag := SPARK_Pragma (Defining_Entity (N)); + declare + E : constant Entity_Id := Defining_Entity (N); + Prag : constant Node_Id := SPARK_Pragma (E); + -- SPARK_Mode pragma in application - if Present (Prag) then - if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then - Check_Node (N); - end if; + begin + if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then + null; - elsif Nkind (N) = N_Package_Body then - Check_List (Declarations (N)); + elsif Present (Prag) then + if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then + Check_Node (N); + end if; - elsif Nkind (N) = N_Package_Declaration then - Check_List (Private_Declarations (Specification (N))); - Check_List (Visible_Declarations (Specification (N))); - end if; + elsif Nkind (N) = N_Package_Body then + Check_List (Declarations (N)); + + elsif Nkind (N) = N_Package_Declaration then + Check_List (Private_Declarations (Specification (N))); + Check_List (Visible_Declarations (Specification (N))); + end if; + end; when others => null; @@ -2717,7 +2738,14 @@ package body Sem_SPARK is when N_Assignment_Statement => declare Target : constant Node_Id := Name (Stmt); + begin + -- Start with checking that the subexpressions of the target + -- path are readable, before possibly updating the permission + -- of these subexpressions in Check_Assignment. + + Check_Expression (Target, Read_Subexpr); + Check_Assignment (Target => Target, Expr => Expression (Stmt)); -- 2.30.2