From: Arnaud Charlet Date: Thu, 27 Apr 2017 10:56:46 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6dd86c75d670c3f7ec6bf58c2b9b0950cd5db84a;p=gcc.git [multiple changes] 2017-04-27 Ed Schonberg * freeze.adb (Build_Inherited_Condition_Pragmas): New procedure, subsidiary of Check_Inherited_Conditions, to build pragmas for an operation whose ancestor has classwide pre/postconditions. This is used both to check the legality of the inheritance in Ada and in SPARK, and to determine whether a wrapper is needed for an inherited operation. * exp_util.adb (Build_Class_Wide_Expression, Replace_Entity): Improve placement of error message for inherited classwide conditions that become illegal on type derivation. 2017-04-27 Yannick Moy * sem_ch12.adb (Analyze_Generic_Package_Declaration): Set SPARK_Mode from context on generic package. * sem_ch7.adb (Analyze_Package_Declaration): Simplify code to remove useless test. 2017-04-27 Claire Dross * a-cofuve.ads (Range_Shifted): Rewrite precondition to avoid overflows in computations. * a-cofove.ads (Capacity_Range): Rewrite last bound to avoid overflows in computations. (Insert): Rewrite precondition to avoid overflows in computations. * a-cfinve.ads (Capacity_Range): Rewrite last bound to avoid overflows in computations. (Insert): Rewrite precondition to avoid overflows in computations. From-SVN: r247318 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 3e64117e84b..d4025dc378d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,33 @@ +2017-04-27 Ed Schonberg + + * freeze.adb (Build_Inherited_Condition_Pragmas): New procedure, + subsidiary of Check_Inherited_Conditions, to build pragmas for an + operation whose ancestor has classwide pre/postconditions. This + is used both to check the legality of the inheritance in Ada + and in SPARK, and to determine whether a wrapper is needed for + an inherited operation. + * exp_util.adb (Build_Class_Wide_Expression, Replace_Entity): + Improve placement of error message for inherited classwide + conditions that become illegal on type derivation. + +2017-04-27 Yannick Moy + + * sem_ch12.adb (Analyze_Generic_Package_Declaration): Set + SPARK_Mode from context on generic package. + * sem_ch7.adb (Analyze_Package_Declaration): Simplify code to remove + useless test. + +2017-04-27 Claire Dross + + * a-cofuve.ads (Range_Shifted): Rewrite precondition to avoid + overflows in computations. + * a-cofove.ads (Capacity_Range): Rewrite last bound to avoid + overflows in computations. + (Insert): Rewrite precondition to avoid overflows in computations. + * a-cfinve.ads (Capacity_Range): Rewrite last bound to avoid + overflows in computations. + (Insert): Rewrite precondition to avoid overflows in computations. + 2017-04-27 Steve Baird * exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads index 56aee851444..5ef2b1edd79 100644 --- a/gcc/ada/a-cfinve.ads +++ b/gcc/ada/a-cfinve.ads @@ -63,8 +63,18 @@ is No_Index : constant Extended_Index := Extended_Index'First; - subtype Capacity_Range is - Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); + Last_Count : constant Count_Type := + (if Index_Type'Last < Index_Type'First then 0 + elsif Index_Type'Last < -1 + or else Index_Type'Pos (Index_Type'First) > + Index_Type'Pos (Index_Type'Last) - Count_Type'Last + then Index_Type'Pos (Index_Type'Last) - + Index_Type'Pos (Index_Type'First) + 1 + else Count_Type'Last); + -- Maximal capacity of any vector. It is the minimum of the size of the + -- index range and the last possible Count_Type. + + subtype Capacity_Range is Count_Type range 0 .. Last_Count; type Vector (Capacity : Capacity_Range) is limited private with Default_Initial_Condition => Is_Empty (Vector); @@ -295,7 +305,8 @@ is Pre => Length (Container) <= Capacity (Container) - Length (New_Item) and (Before in Index_Type'First .. Last_Index (Container) - or Before - 1 = Last_Index (Container)), + or (Before /= No_Index + and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Length (New_Item) @@ -369,7 +380,8 @@ is Pre => Length (Container) <= Capacity (Container) - Count and (Before in Index_Type'First .. Last_Index (Container) - or Before - 1 = Last_Index (Container)), + or (Before /= No_Index + and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Count diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index c7a93dfd15a..5ad0e87c377 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -57,8 +57,18 @@ is No_Index : constant Extended_Index := Extended_Index'First; - subtype Capacity_Range is - Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); + Last_Count : constant Count_Type := + (if Index_Type'Last < Index_Type'First then 0 + elsif Index_Type'Last < -1 + or else Index_Type'Pos (Index_Type'First) > + Index_Type'Pos (Index_Type'Last) - Count_Type'Last + then Index_Type'Pos (Index_Type'Last) - + Index_Type'Pos (Index_Type'First) + 1 + else Count_Type'Last); + -- Maximal capacity of any vector. It is the minimum of the size of the + -- index range and the last possible Count_Type. + + subtype Capacity_Range is Count_Type range 0 .. Last_Count; type Vector (Capacity : Capacity_Range) is limited private with Default_Initial_Condition => Is_Empty (Vector); @@ -289,7 +299,8 @@ is Pre => Length (Container) <= Capacity (Container) - Length (New_Item) and (Before in Index_Type'First .. Last_Index (Container) - or Before - 1 = Last_Index (Container)), + or (Before /= No_Index + and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Length (New_Item) @@ -363,7 +374,8 @@ is Pre => Length (Container) <= Capacity (Container) - Count and (Before in Index_Type'First .. Last_Index (Container) - or Before - 1 = Last_Index (Container)), + or (Before /= No_Index + and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Count diff --git a/gcc/ada/a-cofuve.ads b/gcc/ada/a-cofuve.ads index d02864e4329..db1edd5f122 100644 --- a/gcc/ada/a-cofuve.ads +++ b/gcc/ada/a-cofuve.ads @@ -225,10 +225,16 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Global => null, Pre => Lst <= Last (Left) - and Offset in - Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. - (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) - - Index_Type'Pos (Lst), + and then + (if Offset < 0 then + Index_Type'Pos (Index_Type'Base'First) - Offset <= + Index_Type'Pos (Index_Type'First)) + and then + (if Fst <= Lst then + Offset in + Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. + (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) - + Index_Type'Pos (Lst)), Post => Range_Shifted'Result = ((for all I in Fst .. Lst => diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index c9e099e4511..0828c9b5b7f 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1135,9 +1135,17 @@ package body Exp_Util is and then Is_Abstract_Subprogram (Entity (N)) then Error_Msg_Sloc := Sloc (Current_Scope); - Error_Msg_NE - ("cannot call abstract subprogram in inherited condition " - & "for&#", N, Current_Scope); + -- Error_Msg_Node_1 := Entity (N); + Error_Msg_Node_2 := Subp; + if Comes_From_Source (Subp) then + Error_Msg_NE + ("cannot call abstract subprogram& in inherited " + & "condition for&#", Subp, Entity (N)); + else + Error_Msg_NE + ("cannot call abstract subprogram& in inherited " + & "condition for inherited&#", Subp, Entity (N)); + end if; -- In SPARK mode, reject an inherited condition for an -- inherited operation if it contains a call to an overriding diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 5b0946c3587..b1fb3d38fcf 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -1400,20 +1400,72 @@ package body Freeze is procedure Check_Inherited_Conditions (R : Entity_Id) is Prim_Ops : constant Elist_Id := Primitive_Operations (R); - A_Post : Node_Id; - A_Pre : Node_Id; Decls : List_Id; Needs_Wrapper : Boolean; - New_Prag : Node_Id; Op_Node : Elmt_Id; Par_Prim : Entity_Id; Prim : Entity_Id; + --------------------------------------- + -- Build_Inherited_Condition_Pragmas -- + --------------------------------------- + + procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id); + -- Build corresponding pragmas for an operation whose ancestor has + -- class-wide pre/postconditions. If the operation is inherited, the + -- pragmas force the creation of a wrapper for the inherited operation. + -- If the ancestor is being overridden, the pragmas are constructed only + -- to verify their legality, in case they contain calls to other + -- primitives that may haven been overridden. + + procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is + A_Post : Node_Id; + A_Pre : Node_Id; + New_Prag : Node_Id; + + begin + A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition); + if Present (A_Pre) and then Class_Present (A_Pre) then + New_Prag := New_Copy_Tree (A_Pre); + Build_Class_Wide_Expression + (Prag => New_Prag, + Subp => Prim, + Par_Subp => Par_Prim, + Adjust_Sloc => False, + Needs_Wrapper => Needs_Wrapper); + + if Needs_Wrapper + and then not Comes_From_Source (Subp) + and then Expander_Active + then + Append (New_Prag, Decls); + end if; + end if; + + A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition); + + if Present (A_Post) and then Class_Present (A_Post) then + New_Prag := New_Copy_Tree (A_Post); + Build_Class_Wide_Expression + (Prag => New_Prag, + Subp => Prim, + Par_Subp => Par_Prim, + Adjust_Sloc => False, + Needs_Wrapper => Needs_Wrapper); + + if Needs_Wrapper + and then not Comes_From_Source (Subp) + and then Expander_Active + then + Append (New_Prag, Decls); + end if; + end if; + end Build_Inherited_Condition_Pragmas; + begin Op_Node := First_Elmt (Prim_Ops); while Present (Op_Node) loop - Prim := Node (Op_Node); - Needs_Wrapper := False; + Prim := Node (Op_Node); -- Map the overridden primitive to the overriding one. This takes -- care of all overridings and is done only once. @@ -1421,7 +1473,29 @@ package body Freeze is if Present (Overridden_Operation (Prim)) and then Comes_From_Source (Prim) then - Update_Primitives_Mapping (Overridden_Operation (Prim), Prim); + Par_Prim := Overridden_Operation (Prim); + Update_Primitives_Mapping (Par_Prim, Prim); + end if; + + Next_Elmt (Op_Node); + end loop; + + -- Now perform validity checks on the inherited conditions of + -- overriding operations, for conformance with LSP, and apply + -- SPARK-specific restrictions on inherited conditions. + + Op_Node := First_Elmt (Prim_Ops); + while Present (Op_Node) loop + Prim := Node (Op_Node); + if Present (Overridden_Operation (Prim)) + and then Comes_From_Source (Prim) + then + Par_Prim := Overridden_Operation (Prim); + + -- Analyze the contract items of the overridden operation, before + -- they are rewritten as pragmas. + + Analyze_Entry_Or_Subprogram_Contract (Par_Prim); -- In SPARK mode this is where we can collect the inherited -- conditions, because we do not create the Check pragmas that @@ -1429,28 +1503,27 @@ package body Freeze is -- overriding operations. if SPARK_Mode = On then + Collect_Inherited_Class_Wide_Conditions (Prim); - -- Analyze the contract items of the parent operation, before - -- they are rewritten when inherited. - - Analyze_Entry_Or_Subprogram_Contract - (Overridden_Operation (Prim)); + else - -- Now verify the legality of inherited contracts for LSP - -- conformance. + -- Build the corresponding pragmas to check for legality + -- of the inherited condition. - Collect_Inherited_Class_Wide_Conditions (Prim); + Build_Inherited_Condition_Pragmas (Prim); end if; end if; Next_Elmt (Op_Node); end loop; - -- In all cases, we examine inherited operations to check whether they - -- require a wrapper to handle inherited conditions that call other - -- primitives, so that LSP can be verified/enforced. + -- Now examine the inherited operations to check whether they require + -- a wrapper to handle inherited conditions that call other primitives, + -- so that LSP can be verified/enforced. Op_Node := First_Elmt (Prim_Ops); + Needs_Wrapper := False; + while Present (Op_Node) loop Decls := Empty_List; Prim := Node (Op_Node); @@ -1458,45 +1531,19 @@ package body Freeze is if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then Par_Prim := Alias (Prim); - -- Analyze the contract items of the parent operation, before - -- they are rewritten when inherited. + -- Analyze the contract items of the parent operation, and + -- determine whether a wrapper is needed. This is determined + -- when the condition is rewritten in sem_prag, using the + -- mapping between overridden and overriding operations built + -- in the loop above. Analyze_Entry_Or_Subprogram_Contract (Par_Prim); - - A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition); - - if Present (A_Pre) and then Class_Present (A_Pre) then - New_Prag := New_Copy_Tree (A_Pre); - Build_Class_Wide_Expression - (Prag => New_Prag, - Subp => Prim, - Par_Subp => Par_Prim, - Adjust_Sloc => False, - Needs_Wrapper => Needs_Wrapper); - - if Needs_Wrapper then - Append (New_Prag, Decls); - end if; - end if; - - A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition); - - if Present (A_Post) and then Class_Present (A_Post) then - New_Prag := New_Copy_Tree (A_Post); - Build_Class_Wide_Expression - (Prag => New_Prag, - Subp => Prim, - Par_Subp => Par_Prim, - Adjust_Sloc => False, - Needs_Wrapper => Needs_Wrapper); - - if Needs_Wrapper then - Append (New_Prag, Decls); - end if; - end if; + Build_Inherited_Condition_Pragmas (Prim); end if; - if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim) then + if Needs_Wrapper and then not Is_Abstract_Subprogram (Par_Prim) + and then Expander_Active + then -- We need to build a new primitive that overrides the inherited -- one, and whose inherited expression has been updated above. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 78bd751e2b1..17b559c5292 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3382,6 +3382,13 @@ package body Sem_Ch12 is Set_Ekind (Id, E_Generic_Package); Set_Etype (Id, Standard_Void_Type); + -- Set SPARK_Mode from context + + Set_SPARK_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Id); + Set_SPARK_Aux_Pragma_Inherited (Id); + -- Analyze aspects now, so that generated pragmas appear in the -- declarations before building and analyzing the generic copy. diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 2174f2b08f6..6b2383a3903 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -975,22 +975,20 @@ package body Sem_Ch7 is Set_Ekind (Id, E_Package); Set_Etype (Id, Standard_Void_Type); - -- Set SPARK_Mode from context only for non-generic package + -- Set SPARK_Mode from context - if Ekind (Id) = E_Package then - Set_SPARK_Pragma (Id, SPARK_Mode_Pragma); - Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma); - Set_SPARK_Pragma_Inherited (Id); - Set_SPARK_Aux_Pragma_Inherited (Id); + Set_SPARK_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Id); + Set_SPARK_Aux_Pragma_Inherited (Id); - -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in - -- case the body of this package is instantiated or inlined later and - -- out of context. The body uses this attribute to restore the value - -- of the global flag. + -- Save the state of flag Ignore_SPARK_Mode_Pragmas_In_Instance in case + -- the body of this package is instantiated or inlined later and out + -- of context. The body uses this attribute to restore the value of + -- the global flag. - if Ignore_SPARK_Mode_Pragmas_In_Instance then - Set_Ignore_SPARK_Mode_Pragmas (Id); - end if; + if Ignore_SPARK_Mode_Pragmas_In_Instance then + Set_Ignore_SPARK_Mode_Pragmas (Id); end if; -- Analyze aspect specifications immediately, since we need to recognize