From a6fecb06710ff3bae9dbad6cf480a4934a84bb3c Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 9 Oct 2020 15:59:24 +0200 Subject: [PATCH] [Ada] Minimize side-effect removal in GNATprove mode gcc/ada/ * exp_util.adb (Remove_Side_Effects): Only remove side-effects in GNATprove mode when this is useful. * sem_res.adb (Set_Slice_Subtype): Make sure in GNATprove mode to define the Itype when needed, so that run-time errors can be analyzed. * sem_util.adb (Enclosing_Declaration): Correctly take into account renaming declarations. --- gcc/ada/exp_util.adb | 40 +++++++++++++++++++++++++++++----------- gcc/ada/sem_res.adb | 5 +++-- gcc/ada/sem_util.adb | 2 ++ 3 files changed, 34 insertions(+), 13 deletions(-) diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index bec7456c336..fa30e8f7de3 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -11124,6 +11124,12 @@ package body Exp_Util is -- otherwise it generates an internal temporary. The created temporary -- entity is marked as internal. + function Possible_Side_Effect_In_SPARK (Exp : Node_Id) return Boolean; + -- Computes whether a side-effect is possible in SPARK, which should + -- be handled by removing it from the expression for GNATprove. Note + -- that other side-effects related to volatile variables are handled + -- separately. + --------------------- -- Build_Temporary -- --------------------- @@ -11159,6 +11165,26 @@ package body Exp_Util is return Temp_Id; end Build_Temporary; + ----------------------------------- + -- Possible_Side_Effect_In_SPARK -- + ----------------------------------- + + function Possible_Side_Effect_In_SPARK (Exp : Node_Id) return Boolean is + begin + -- Side-effect removal in SPARK should only occur when not inside a + -- generic and not doing a preanalysis, inside an object renaming or + -- a type declaration or a for-loop iteration scheme. + + return not Inside_A_Generic + and then Full_Analysis + and then Nkind (Enclosing_Declaration (Exp)) in + N_Full_Type_Declaration + | N_Iterator_Specification + | N_Loop_Parameter_Specification + | N_Object_Renaming_Declaration + | N_Subtype_Declaration; + end Possible_Side_Effect_In_SPARK; + -- Local variables Loc : constant Source_Ptr := Sloc (Exp); @@ -11176,11 +11202,11 @@ package body Exp_Util is begin -- Handle cases in which there is nothing to do. In GNATprove mode, -- removal of side effects is useful for the light expansion of - -- renamings. This removal should only occur when not inside a - -- generic and not doing a preanalysis. + -- renamings. if not Expander_Active - and (Inside_A_Generic or not Full_Analysis or not GNATprove_Mode) + and then not + (GNATprove_Mode and then Possible_Side_Effect_In_SPARK (Exp)) then return; @@ -11218,14 +11244,6 @@ package body Exp_Util is and then Is_Class_Wide_Type (Etype (Exp)) then return; - - -- An expression which is in SPARK mode is considered side effect free - -- if the resulting value is captured by a variable or a constant. - - elsif GNATprove_Mode - and then Nkind (Parent (Exp)) = N_Object_Declaration - then - return; end if; -- The remaining processing is done with all checks suppressed diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index f522da005b1..c169467fa77 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -12438,9 +12438,10 @@ package body Sem_Res is -- the point where actions for the slice are analyzed). Note that this -- is different from freezing the itype immediately, which might be -- premature (e.g. if the slice is within a transient scope). This needs - -- to be done only if expansion is enabled. + -- to be done only if expansion is enabled, or in GNATprove mode to + -- capture the associated run-time exceptions if any. - elsif Expander_Active then + elsif Expander_Active or GNATprove_Mode then Ensure_Defined (Typ => Slice_Subtype, N => N); end if; end Set_Slice_Subtype; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index db348ec7550..34714729df4 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -7859,6 +7859,8 @@ package body Sem_Util is or else Nkind (Decl) in N_Later_Decl_Item or else + Nkind (Decl) in N_Renaming_Declaration + or else Nkind (Decl) = N_Number_Declaration) loop Decl := Parent (Decl); -- 2.30.2