From patchwork Wed Aug 14 09:53:12 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1146895 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-506907-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="Uae4CBfI"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 467lLB4x2kz9sDQ for ; Wed, 14 Aug 2019 19:54:42 +1000 (AEST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=raNGrKdpGCYmjRxFMOtX+Hh5+euzkpQCLYuy0GhPphb9gSBu0l xldpezlGHEBgUr5h0RlvLBSEEg8VnBasOHPVQnjQrOmJE5h7VDdEUW6EzW2+xZW7 +JjGTXAqf9q0DdakPTBvIrQQzNKW2063uW0rTjvrQgsWvcC2LqygjqB/c= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=RrHiBEYeQQInjCT1SqihMpxLkjM=; b=Uae4CBfIpHSr6w/+xC6A nKq72eLznVuSqOBC/bhWCzTKeNfxiO/uxq0TQ4ul2W7oN6IBbjdP2B1vhkcdZQNF WIppPROcEKXzOQx9BKfTzsRx4uSDAuc1kyofZmR3pnC2vkCJh2lsTGKtaWiDJqTi 75rkzsltM2fdfmUN3JbeBDE= Received: (qmail 73800 invoked by alias); 14 Aug 2019 09:53:19 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 73720 invoked by uid 89); 14 Aug 2019 09:53:19 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-11.1 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.1 spammy=sk:N_Itera, Explanation, Component_Type, sk:n_itera X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 14 Aug 2019 09:53:16 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id BF51F56106; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id p13G2kExLIvk; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id AD1C711626C; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id A8C6B6CC; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Date: Wed, 14 Aug 2019 05:53:12 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Expose part of ownership checking for use in GNATprove Message-ID: <20190814095312.GA52107@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes GNATprove needs to be able to call a subset of the ownership legality rules from marking. This is provided by a new function Sem_SPARK.Is_Legal. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-14 Yannick Moy gcc/ada/ * sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed for use in GNATprove, to test legality rules not related to permissions. (Check_Declaration_Legality): Extract the part of Check_Declaration that checks rules not related to permissions. (Check_Declaration): Call the new Check_Declaration_Legality. (Check_Type_Legality): Rename of Check_Type. Introduce parameters to force or not checking, and update a flag detecting illegalities. (Check_Node): Ignore attribute references in statement position. --- gcc/ada/sem_spark.adb +++ gcc/ada/sem_spark.adb @@ -637,6 +637,14 @@ package body Sem_SPARK is procedure Check_Declaration (Decl : Node_Id); + procedure Check_Declaration_Legality + (Decl : Node_Id; + Force : Boolean; + Legal : in out Boolean); + -- Check the legality of declaration Decl regarding rules not related to + -- permissions. Update Legal to False if a rule is violated. Issue an + -- error message if Force is True and Emit_Messages returns True. + procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode); pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint, N_Range_Constraint, @@ -686,7 +694,10 @@ package body Sem_SPARK is procedure Check_Statement (Stmt : Node_Id); - procedure Check_Type (Typ : Entity_Id); + procedure Check_Type_Legality + (Typ : Entity_Id; + Force : Boolean; + Legal : in out Boolean); -- Check that type Typ is either not deep, or that it is an observing or -- owning type according to SPARK RM 3.10 @@ -1138,11 +1149,12 @@ package body Sem_SPARK is Expr_Root : Entity_Id; Perm : Perm_Kind; Status : Error_Status; + Dummy : Boolean := True; -- Start of processing for Check_Assignment begin - Check_Type (Target_Typ); + Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy); if Is_Anonymous_Access_Type (Target_Typ) then Check_Source_Of_Borrow_Or_Observe (Expr, Status); @@ -1410,11 +1422,18 @@ package body Sem_SPARK is Target : constant Entity_Id := Defining_Identifier (Decl); Target_Typ : constant Node_Id := Etype (Target); Expr : Node_Id; + Dummy : Boolean := True; begin + -- Start with legality rules not related to permissions + + Check_Declaration_Legality (Decl, Force => True, Legal => Dummy); + + -- Now check permission-related legality rules + case N_Declaration'(Nkind (Decl)) is when N_Full_Type_Declaration => - Check_Type (Target); + null; -- ??? What about component declarations with defaults. @@ -1424,7 +1443,105 @@ package body Sem_SPARK is when N_Object_Declaration => Expr := Expression (Decl); - Check_Type (Target_Typ); + if Present (Expr) then + Check_Assignment (Target => Target, + Expr => Expr); + end if; + + if Is_Deep (Target_Typ) then + declare + Tree : constant Perm_Tree_Access := + new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => True, + Explanation => Decl, + Permission => Read_Write, + Children_Permission => Read_Write)); + begin + Set (Current_Perm_Env, Target, Tree); + end; + end if; + + when N_Iterator_Specification => + null; + + when N_Loop_Parameter_Specification => + null; + + -- Checking should not be called directly on these nodes + + when N_Function_Specification + | N_Entry_Declaration + | N_Procedure_Specification + | N_Component_Declaration + => + raise Program_Error; + + -- Ignored constructs for pointer checking + + when N_Formal_Object_Declaration + | N_Formal_Type_Declaration + | N_Incomplete_Type_Declaration + | N_Private_Extension_Declaration + | N_Private_Type_Declaration + | N_Protected_Type_Declaration + => + null; + + -- The following nodes are rewritten by semantic analysis + + when N_Expression_Function => + raise Program_Error; + end case; + end Check_Declaration; + + -------------------------------- + -- Check_Declaration_Legality -- + -------------------------------- + + procedure Check_Declaration_Legality + (Decl : Node_Id; + Force : Boolean; + Legal : in out Boolean) + is + function Original_Emit_Messages return Boolean renames Emit_Messages; + + function Emit_Messages return Boolean; + -- Local wrapper around generic formal parameter Emit_Messages, to + -- check the value of parameter Force before calling the original + -- Emit_Messages, and setting Legal to False. + + ------------------- + -- Emit_Messages -- + ------------------- + + function Emit_Messages return Boolean is + begin + Legal := False; + return Force and then Original_Emit_Messages; + end Emit_Messages; + + -- Local variables + + Target : constant Entity_Id := Defining_Identifier (Decl); + Target_Typ : constant Node_Id := Etype (Target); + Expr : Node_Id; + + -- Start of processing for Check_Declaration_Legality + + begin + case N_Declaration'(Nkind (Decl)) is + when N_Full_Type_Declaration => + Check_Type_Legality (Target, Force, Legal); + + when N_Subtype_Declaration => + null; + + when N_Object_Declaration => + Expr := Expression (Decl); + + Check_Type_Legality (Target_Typ, Force, Legal); -- A declaration of a stand-alone object of an anonymous access -- type shall have an explicit initial value and shall occur @@ -1453,26 +1570,6 @@ package body Sem_SPARK is end if; end if; - if Present (Expr) then - Check_Assignment (Target => Target, - Expr => Expr); - end if; - - if Is_Deep (Target_Typ) then - declare - Tree : constant Perm_Tree_Access := - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => True, - Explanation => Decl, - Permission => Read_Write, - Children_Permission => Read_Write)); - begin - Set (Current_Perm_Env, Target, Tree); - end; - end if; - when N_Iterator_Specification => null; @@ -1504,7 +1601,7 @@ package body Sem_SPARK is when N_Expression_Function => raise Program_Error; end case; - end Check_Declaration; + end Check_Declaration_Legality; ---------------------- -- Check_Expression -- @@ -2668,6 +2765,12 @@ package body Sem_SPARK is when N_Subprogram_Declaration => Check_Subprogram_Contract (N); + -- Attribute references in statement position are not supported in + -- SPARK and will be rejected by GNATprove. + + when N_Attribute_Reference => + null; + -- Ignored constructs for pointer checking when N_Abstract_Subprogram_Declaration @@ -3503,13 +3606,38 @@ package body Sem_SPARK is end case; end Check_Statement; - ---------------- - -- Check_Type -- - ---------------- + ------------------------- + -- Check_Type_Legality -- + ------------------------- + + procedure Check_Type_Legality + (Typ : Entity_Id; + Force : Boolean; + Legal : in out Boolean) + is + function Original_Emit_Messages return Boolean renames Emit_Messages; + + function Emit_Messages return Boolean; + -- Local wrapper around generic formal parameter Emit_Messages, to + -- check the value of parameter Force before calling the original + -- Emit_Messages, and setting Legal to False. + + ------------------- + -- Emit_Messages -- + ------------------- + + function Emit_Messages return Boolean is + begin + Legal := False; + return Force and then Original_Emit_Messages; + end Emit_Messages; + + -- Local variables - procedure Check_Type (Typ : Entity_Id) is Check_Typ : constant Entity_Id := Retysp (Typ); + -- Start of processing for Check_Type_Legality + begin case Type_Kind'(Ekind (Check_Typ)) is when Access_Kind => @@ -3519,7 +3647,7 @@ package body Sem_SPARK is => null; when E_Access_Subtype => - Check_Type (Base_Type (Check_Typ)); + Check_Type_Legality (Base_Type (Check_Typ), Force, Legal); when E_Access_Attribute_Type => if Emit_Messages then Error_Msg_N ("access attribute not allowed in SPARK", @@ -3546,7 +3674,7 @@ package body Sem_SPARK is when E_Array_Type | E_Array_Subtype => - Check_Type (Component_Type (Check_Typ)); + Check_Type_Legality (Component_Type (Check_Typ), Force, Legal); when Record_Kind => if Is_Deep (Check_Typ) @@ -3569,7 +3697,7 @@ package body Sem_SPARK is -- Ignore components which are not visible in SPARK if Component_Is_Visible_In_SPARK (Comp) then - Check_Type (Etype (Comp)); + Check_Type_Legality (Etype (Comp), Force, Legal); end if; Next_Component_Or_Discriminant (Comp); end loop; @@ -3595,7 +3723,7 @@ package body Sem_SPARK is => null; end case; - end Check_Type; + end Check_Type_Legality; -------------- -- Get_Expl -- @@ -4141,6 +4269,24 @@ package body Sem_SPARK is end case; end Is_Deep; + -------------- + -- Is_Legal -- + -------------- + + function Is_Legal (N : Node_Id) return Boolean is + Legal : Boolean := True; + + begin + case Nkind (N) is + when N_Declaration => + Check_Declaration_Legality (N, Force => False, Legal => Legal); + when others => + null; + end case; + + return Legal; + end Is_Legal; + ---------------------- -- Is_Local_Context -- ---------------------- --- gcc/ada/sem_spark.ads +++ gcc/ada/sem_spark.ads @@ -152,6 +152,12 @@ generic package Sem_SPARK is + function Is_Legal (N : Node_Id) return Boolean; + -- Test the legality of a node wrt ownership-checking rules. This does not + -- check rules related to the validity of permissions associated with paths + -- from objects, so that it can be called from GNATprove on code of library + -- units analyzed in SPARK_Mode Auto. + procedure Check_Safe_Pointers (N : Node_Id); -- The entry point of this package. It analyzes a node and reports errors -- when there are violations of ownership rules.