From: Claire Dross Date: Wed, 10 Jul 2019 09:02:36 +0000 (+0000) Subject: [Ada] Fix possible crashes in GNATprove analysis of pointers X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1bc68e0d30bc801a279da653196d66d36312831b;p=gcc.git [Ada] Fix possible crashes in GNATprove analysis of pointers The new analysis of SPARK pointer rules could crash on some constructs. Now fixed. There is no impact on compilation. 2019-07-10 Claire Dross gcc/ada/ * sem_spark.adb (Check_Expression): Allow digits constraints as input. (Illegal_Global_Usage): Pass in the entity. (Is_Subpath_Expression): New function to allow different nodes as inner parts of a path expression. (Read_Indexes): Allow concatenation and aggregates with box expressions. Allow attributes Update and Loop_Entry. (Check_Expression): Allow richer membership test. (Check_Node): Ignore bodies of generics. (Get_Root_Object): Allow concatenation and attributes. From-SVN: r273348 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 86e35087f68..2ef2faf627a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,16 @@ +2019-07-10 Claire Dross + + * sem_spark.adb (Check_Expression): Allow digits constraints as + input. + (Illegal_Global_Usage): Pass in the entity. + (Is_Subpath_Expression): New function to allow different nodes + as inner parts of a path expression. + (Read_Indexes): Allow concatenation and aggregates with box + expressions. Allow attributes Update and Loop_Entry. + (Check_Expression): Allow richer membership test. + (Check_Node): Ignore bodies of generics. + (Get_Root_Object): Allow concatenation and attributes. + 2019-07-10 Hristian Kirtchev * sem_ch6.adb (Check_Discriminant_Conformance): Use Find_Type to diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index a9384b84c0d..150433321ee 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -640,7 +640,8 @@ package body Sem_SPARK is 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) + N_Subtype_Indication, + N_Digits_Constraint) or else Nkind (Expr) in N_Subexpr); procedure Check_Globals (Subp : Entity_Id); @@ -738,7 +739,7 @@ package body Sem_SPARK is -- the debugger to look into a hash table. pragma Unreferenced (Hp); - procedure Illegal_Global_Usage (N : Node_Or_Entity_Id); + procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id); pragma No_Return (Illegal_Global_Usage); -- A procedure that is called when deep globals or aliased globals are used -- without any global aspect. @@ -750,6 +751,9 @@ package body Sem_SPARK is function Is_Path_Expression (Expr : Node_Id) return Boolean; -- Return whether Expr corresponds to a path + function Is_Subpath_Expression (Expr : Node_Id) return Boolean; + -- Return True if Expr can be part of a path expression + function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean; -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost -- a prefix, in the sense that they could still refer to overlapping memory @@ -1302,7 +1306,9 @@ package body Sem_SPARK is begin -- Only SPARK bodies are analyzed - if No (Prag) or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On then + if No (Prag) + or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On + then return; end if; @@ -1312,9 +1318,8 @@ package body Sem_SPARK is and then Is_Anonymous_Access_Type (Etype (Spec_Id)) and then not Is_Traversal_Function (Spec_Id) then - Error_Msg_N - ("anonymous access type for result only allowed for traveral " - & "functions", Spec_Id); + Error_Msg_N ("anonymous access type for result only allowed for " + & "traveral functions", Spec_Id); return; end if; @@ -1568,7 +1573,7 @@ package body Sem_SPARK is -- Start of processing for Read_Indexes begin - if not Is_Path_Expression (Expr) then + if not Is_Subpath_Expression (Expr) then Error_Msg_N ("name expected here for move/borrow/observe", Expr); return; end if; @@ -1603,6 +1608,10 @@ package body Sem_SPARK is Read_Params (Expr); Check_Globals (Get_Called_Entity (Expr)); + when N_Op_Concat => + Read_Expression (Left_Opnd (Expr)); + Read_Expression (Right_Opnd (Expr)); + when N_Qualified_Expression | N_Type_Conversion | N_Unchecked_Type_Conversion @@ -1644,7 +1653,8 @@ package body Sem_SPARK is -- There can be only one element for a value of deep type -- in order to avoid aliasing. - if Is_Deep (Etype (Expression (Assoc))) + if not (Box_Present (Assoc)) + and then Is_Deep (Etype (Expression (Assoc))) and then not Is_Singleton_Choice (CL) then Error_Msg_F @@ -1655,7 +1665,9 @@ package body Sem_SPARK is -- The subexpressions of an aggregate are moved as part -- of the implicit assignments. - Move_Expression (Expression (Assoc)); + if not Box_Present (Assoc) then + Move_Expression (Expression (Assoc)); + end if; Next (Assoc); end loop; @@ -1689,12 +1701,28 @@ package body Sem_SPARK is -- The subexpressions of an aggregate are moved as part -- of the implicit assignments. - Move_Expression (Expression (Assoc)); + if not Box_Present (Assoc) then + Move_Expression (Expression (Assoc)); + end if; Next (Assoc); end loop; end; + when N_Attribute_Reference => + pragma Assert + (Get_Attribute_Id (Attribute_Name (Expr)) = + Attribute_Loop_Entry + or else + Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update); + + Read_Expression (Prefix (Expr)); + + if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update + then + Read_Expression_List (Expressions (Expr)); + end if; + when others => raise Program_Error; end case; @@ -1758,6 +1786,13 @@ package body Sem_SPARK is end if; return; + when N_Digits_Constraint => + Read_Expression (Digits_Expression (Expr)); + if Present (Range_Constraint (Expr)) then + Read_Expression (Range_Constraint (Expr)); + end if; + return; + when others => null; end case; @@ -1767,12 +1802,28 @@ package body Sem_SPARK is case N_Subexpr'(Nkind (Expr)) is when N_Binary_Op - | N_Membership_Test | N_Short_Circuit => Read_Expression (Left_Opnd (Expr)); Read_Expression (Right_Opnd (Expr)); + when N_Membership_Test => + Read_Expression (Left_Opnd (Expr)); + if Present (Right_Opnd (Expr)) then + Read_Expression (Right_Opnd (Expr)); + else + declare + Cases : constant List_Id := Alternatives (Expr); + Cur_Case : Node_Id := First (Cases); + + begin + while Present (Cur_Case) loop + Read_Expression (Cur_Case); + Next (Cur_Case); + end loop; + end; + end if; + when N_Unary_Op => Read_Expression (Right_Opnd (Expr)); @@ -1856,6 +1907,14 @@ package body Sem_SPARK is when Attribute_Modulus => null; + -- The following attributes apply to types; there are no + -- expressions to read. + + when Attribute_Class + | Attribute_Storage_Size + => + null; + -- Postconditions should not be analyzed when Attribute_Old @@ -2418,13 +2477,17 @@ package body Sem_SPARK is Check_Call_Statement (N); when N_Package_Body => - Check_Package_Body (N); + if not Is_Generic_Unit (Unique_Defining_Entity (N)) then + Check_Package_Body (N); + end if; when N_Subprogram_Body | N_Entry_Body | N_Task_Body => - Check_Callable_Body (N); + if not Is_Generic_Unit (Unique_Defining_Entity (N)) then + Check_Callable_Body (N); + end if; when N_Protected_Body => Check_List (Declarations (N)); @@ -3399,7 +3462,7 @@ package body Sem_SPARK is if not Inside_Elaboration and then C = null then - Illegal_Global_Usage (N); + Illegal_Global_Usage (N, N); end if; return (R => Unfolded, Tree_Access => C); @@ -3498,7 +3561,7 @@ package body Sem_SPARK is Through_Traversal : Boolean := True) return Entity_Id is begin - if not Is_Path_Expression (Expr) then + if not Is_Subpath_Expression (Expr) then Error_Msg_N ("name expected here for path", Expr); return Empty; end if; @@ -3517,12 +3580,13 @@ package body Sem_SPARK is return Get_Root_Object (Prefix (Expr), Through_Traversal); -- There is no root object for an (extension) aggregate, allocator, - -- or NULL. + -- concat, or NULL. when N_Aggregate | N_Allocator | N_Extension_Aggregate | N_Null + | N_Op_Concat => return Empty; @@ -3545,6 +3609,15 @@ package body Sem_SPARK is => return Get_Root_Object (Expression (Expr), Through_Traversal); + when N_Attribute_Reference => + pragma Assert + (Get_Attribute_Id (Attribute_Name (Expr)) = + Attribute_Loop_Entry + or else + Get_Attribute_Id (Attribute_Name (Expr)) = + Attribute_Update); + return Empty; + when others => raise Program_Error; end case; @@ -3646,9 +3719,10 @@ package body Sem_SPARK is -- Illegal_Global_Usage -- -------------------------- - procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is + procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id) + is begin - Error_Msg_NE ("cannot use global variable & of deep type", N, N); + Error_Msg_NE ("cannot use global variable & of deep type", N, E); Error_Msg_N ("\without prior declaration in a Global aspect", N); Errout.Finalize (Last_Call => True); Errout.Output_Messages; @@ -3668,7 +3742,7 @@ package body Sem_SPARK is when E_Array_Type | E_Array_Subtype => - return Is_Deep (Component_Type (Typ)); + return Is_Deep (Component_Type (Underlying_Type (Typ))); when Record_Kind => declare @@ -3860,6 +3934,23 @@ package body Sem_SPARK is end if; end Is_Prefix_Or_Almost; + --------------------------- + -- Is_Subpath_Expression -- + --------------------------- + + function Is_Subpath_Expression (Expr : Node_Id) return Boolean is + begin + return Is_Path_Expression (Expr) + or else (Nkind (Expr) = N_Attribute_Reference + and then + (Get_Attribute_Id (Attribute_Name (Expr)) = + Attribute_Update + or else + Get_Attribute_Id (Attribute_Name (Expr)) = + Attribute_Loop_Entry)) + or else Nkind (Expr) = N_Op_Concat; + end Is_Subpath_Expression; + --------------------------- -- Is_Traversal_Function -- --------------------------- @@ -4397,7 +4488,7 @@ package body Sem_SPARK is if not Inside_Elaboration and then Get (Current_Perm_Env, Root) = null then - Illegal_Global_Usage (Expr); + Illegal_Global_Usage (Expr, Root); end if; -- During elaboration, only the validity of operations is checked, no