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: 1146900 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-506912-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="JUHkHJFy"; 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 467lML2lW5z9sN1 for ; Wed, 14 Aug 2019 19:55: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=nQ9hatxa0v2FuzYOAg1XccibPWX/PXRM6NEkZ9NxbODXH3FuKU 6DNzzK3Jrt2eRM8jxePFqU5KZYXxL1FIejURWVf4rW6BOeu0KyuwR4/ymL58gAst 6RqYHrh1jorXnLvCaNMe9ea3u2zgY/hvOLzkngSwaylz7Ps/v6pDdkfy4= 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=YpVMjd5K4PiQwjkWdGA5XtmpQPc=; b=JUHkHJFyrCqtaQHQ95Nn hc3wkSKoyrtgSrNQ39NY2gjdxv8eD3VRpu+SsvAQqC//PR3Ly/5yJp4ZqPT3HrF2 o3ZOjxnjeaCJ60AK8q1D3SeoFZSST49L4xg7XhjqRMXYaOnrdkxzC/qtAHsv0yot GkrQlBjPRkJrMnpztfAZmic= Received: (qmail 74529 invoked by alias); 14 Aug 2019 09:53:23 -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 74300 invoked by uid 89); 14 Aug 2019 09:53:22 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.3 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, SPF_NEUTRAL autolearn=ham version=3.3.1 spammy= X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 14 Aug 2019 09:53:19 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hxpy0-0007wM-Tx for gcc-patches@gcc.gnu.org; Wed, 14 Aug 2019 05:53:18 -0400 Received: from rock.gnat.com ([205.232.38.15]:55196) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hxpy0-0007vQ-NT for gcc-patches@gcc.gnu.org; Wed, 14 Aug 2019 05:53:16 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 9FD5656104; 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 oPvMTAqIE5xi; 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 8DBB311626C; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 8AD2D6CC; 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] Check SPARK restriction on Old/Loop_Entry with pointers Message-ID: <20190814095312.GA52071@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 205.232.38.15 X-IsSubscribed: yes SPARK RM rule 3.10(14) restricts the use of Old and Loop_Entry attributes on prefixes of an owning or observing type (i.e. a type with access inside). 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 (Check_Old_Loop_Entry): New procedure to check correct use of Old and Loop_Entry. (Check_Node): Check subprogram contracts. (Check_Pragma): Check Loop_Variant. (Check_Safe_Pointers): Apply checking to library-level subprogram declarations as well, in order to check their contract. --- gcc/ada/sem_spark.adb +++ gcc/ada/sem_spark.adb @@ -663,6 +663,9 @@ package body Sem_SPARK is procedure Check_Node (N : Node_Id); -- Main traversal procedure to check safe pointer usage + procedure Check_Old_Loop_Entry (N : Node_Id); + -- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry + procedure Check_Package_Body (Pack : Node_Id); procedure Check_Package_Spec (Pack : Node_Id); @@ -2583,6 +2586,43 @@ package body Sem_SPARK is ---------------- procedure Check_Node (N : Node_Id) is + + procedure Check_Subprogram_Contract (N : Node_Id); + -- Check the postcondition-like contracts for use of 'Old + + ------------------------------- + -- Check_Subprogram_Contract -- + ------------------------------- + + procedure Check_Subprogram_Contract (N : Node_Id) is + begin + if Nkind (N) = N_Subprogram_Declaration + or else Acts_As_Spec (N) + then + declare + E : constant Entity_Id := Unique_Defining_Entity (N); + Post : constant Node_Id := + Get_Pragma (E, Pragma_Postcondition); + Cases : constant Node_Id := + Get_Pragma (E, Pragma_Contract_Cases); + begin + Check_Old_Loop_Entry (Post); + Check_Old_Loop_Entry (Cases); + end; + + elsif Nkind (N) = N_Subprogram_Body then + declare + E : constant Entity_Id := Defining_Entity (N); + Ref_Post : constant Node_Id := + Get_Pragma (E, Pragma_Refined_Post); + begin + Check_Old_Loop_Entry (Ref_Post); + end; + end if; + end Check_Subprogram_Contract; + + -- Start of processing for Check_Node + begin case Nkind (N) is when N_Declaration => @@ -2602,14 +2642,17 @@ package body Sem_SPARK is Check_Package_Body (N); end if; - when N_Subprogram_Body - | N_Entry_Body - | N_Task_Body - => + when N_Subprogram_Body => if not Is_Generic_Unit (Unique_Defining_Entity (N)) then + Check_Subprogram_Contract (N); Check_Callable_Body (N); end if; + when N_Entry_Body + | N_Task_Body + => + Check_Callable_Body (N); + when N_Protected_Body => Check_List (Declarations (N)); @@ -2622,6 +2665,9 @@ package body Sem_SPARK is when N_Pragma => Check_Pragma (N); + when N_Subprogram_Declaration => + Check_Subprogram_Contract (N); + -- Ignored constructs for pointer checking when N_Abstract_Subprogram_Declaration @@ -2655,7 +2701,6 @@ package body Sem_SPARK is | N_Procedure_Instantiation | N_Raise_xxx_Error | N_Record_Representation_Clause - | N_Subprogram_Declaration | N_Subprogram_Renaming_Declaration | N_Task_Type_Declaration | N_Use_Package_Clause @@ -2677,6 +2722,65 @@ package body Sem_SPARK is end case; end Check_Node; + -------------------------- + -- Check_Old_Loop_Entry -- + -------------------------- + + procedure Check_Old_Loop_Entry (N : Node_Id) is + + function Check_Attribute (N : Node_Id) return Traverse_Result; + + --------------------- + -- Check_Attribute -- + --------------------- + + function Check_Attribute (N : Node_Id) return Traverse_Result is + Attr_Id : Attribute_Id; + Aname : Name_Id; + Pref : Node_Id; + + begin + if Nkind (N) = N_Attribute_Reference then + Attr_Id := Get_Attribute_Id (Attribute_Name (N)); + Aname := Attribute_Name (N); + + if Attr_Id = Attribute_Old + or else Attr_Id = Attribute_Loop_Entry + then + Pref := Prefix (N); + + if Is_Deep (Etype (Pref)) then + if Nkind (Pref) /= N_Function_Call then + if Emit_Messages then + Error_Msg_Name_1 := Aname; + Error_Msg_N + ("prefix of % attribute must be a function call " + & "(SPARK RM 3.10(14))", Pref); + end if; + + elsif Is_Traversal_Function_Call (Pref) then + if Emit_Messages then + Error_Msg_Name_1 := Aname; + Error_Msg_N + ("prefix of % attribute should not call a traversal " + & "function (SPARK RM 3.10(14))", Pref); + end if; + end if; + end if; + end if; + end if; + + return OK; + end Check_Attribute; + + procedure Check_All is new Traverse_Proc (Check_Attribute); + + -- Start of processing for Check_Old_Loop_Entry + + begin + Check_All (N); + end Check_Old_Loop_Entry; + ------------------------ -- Check_Package_Body -- ------------------------ @@ -2869,8 +2973,18 @@ package body Sem_SPARK is Expr : constant Node_Id := Expression (Arg2); begin Check_Expression (Expr, Read); + + -- Prefix of Loop_Entry should be checked inside any assertion + -- where it may appear. + + Check_Old_Loop_Entry (Expr); end; + -- Prefix of Loop_Entry should be checked inside a Loop_Variant + + when Pragma_Loop_Variant => + Check_Old_Loop_Entry (Prag); + -- There is no need to check contracts, as these can only access -- inputs and outputs of the subprogram. Inputs are checked -- independently for R permission. Outputs are checked @@ -2963,6 +3077,7 @@ package body Sem_SPARK is when N_Package_Body | N_Package_Declaration + | N_Subprogram_Declaration | N_Subprogram_Body => declare