From patchwork Wed Apr 27 12:38:02 2016 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 615612 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org 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 3qvzz23kR6z9ssM for ; Wed, 27 Apr 2016 22:38:38 +1000 (AEST) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=g7XUn6GH; dkim-atps=neutral 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=nHwsFKTPA2cSzjiJBrINZ4ac/YNKsb6qZYssYveeGL6fDUlex4 J8Dmr/9Y6E9fFTXdZ4sI2CjCEknJj7kDb60JZeTiDRperU2M612/nCn5Q7ODGDT4 PpQIR1YX++sCW45XCjpM88LBJSz3aDXTjsn1e2zdXQMXCfb56fDEs9sCY= 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=VwfjZNl3EY6Ksw/TSBcgf/SqTkM=; b=g7XUn6GHSwWGqxrHtSSl 3z366Eo47W1TevsSQyA4FC1DX2Yp2tMEtRbnBZTL1DiNteyhF+7qcQiSHDGoGrsb BNn73koXf5tSVeRRH8+y/9qy6o4WYmjbh0f6Mt0g9ORPhuWmgOV4DBVUtVEvtgr0 vZka3LdWPMjvC9fMURDOEJY= Received: (qmail 58086 invoked by alias); 27 Apr 2016 12:38:15 -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 58050 invoked by uid 89); 27 Apr 2016 12:38:14 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=2.3 required=5.0 tests=AWL, BAYES_50, KAM_ASCII_DIVIDERS, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_NONE autolearn=no version=3.3.2 spammy=nam, Entity_Id, entity_id, elsif 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 (AES256-SHA encrypted) ESMTPS; Wed, 27 Apr 2016 12:38:04 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id BB0C9116B8B; Wed, 27 Apr 2016 08:38:02 -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 luosv1bl15Zy; Wed, 27 Apr 2016 08:38:02 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id A76A5116AD2; Wed, 27 Apr 2016 08:38:02 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id A6578370; Wed, 27 Apr 2016 08:38:02 -0400 (EDT) Date: Wed, 27 Apr 2016 08:38:02 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Missing error on illegal use of volatile object Message-ID: <20160427123802.GA63916@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch updates the resolution of actual parameters to flags all effectively volatile objects with enabled property Async_Writers or Effective_Reads which appear in the actual as illegal because the context is interfering. ------------ -- Source -- ------------ -- volatiles.ads package Volatiles with SPARK_Mode is type Vol_Int is new Integer with Volatile; function Vol_Func_1 (Obj : Vol_Int) return Vol_Int with Volatile_Function; function Vol_Func_2 (Obj : Vol_Int) return Boolean with Volatile_Function; Obj : Vol_Int := 0; Error_1 : Vol_Int := Obj - Obj; -- Error Error_2 : Vol_Int := Vol_Func_1 (1 + Obj); -- Error Error_3 : Boolean := Vol_Func_2 (1 + Vol_Func_1 (1 + Obj)); -- Error end Volatiles; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c volatiles.ads volatiles.ads:12:25: volatile object cannot appear in this context (SPARK RM 7.1.3(12)) volatiles.ads:12:31: volatile object cannot appear in this context (SPARK RM 7.1.3(12)) volatiles.ads:13:41: volatile object cannot appear in this context (SPARK RM 7.1.3(11)) volatiles.ads:14:57: volatile object cannot appear in this context (SPARK RM 7.1.3(11)) Tested on x86_64-pc-linux-gnu, committed on trunk 2016-04-27 Hristian Kirtchev * sem_res.adb (Flag_Effectively_Volatile_Objects): New routine. (Resolve_Actuals): Flag effectively volatile objects with enabled property Async_Writers or Effective_Reads as illegal. * sem_util.adb (Is_OK_Volatile_Context): Comment reformatting. Index: sem_res.adb =================================================================== --- sem_res.adb (revision 235481) +++ sem_res.adb (working copy) @@ -3107,6 +3107,10 @@ -- interpretation, but the form of the actual can only be determined -- once the primitive operation is identified. + procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id); + -- Emit an error concerning the illegal usage of an effectively volatile + -- object in interfering context (SPARK RM 7.13(12)). + procedure Insert_Default; -- If the actual is missing in a call, insert in the actuals list -- an instance of the default expression. The insertion is always @@ -3360,6 +3364,55 @@ end if; end Check_Prefixed_Call; + --------------------------------------- + -- Flag_Effectively_Volatile_Objects -- + --------------------------------------- + + procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is + function Flag_Object (N : Node_Id) return Traverse_Result; + -- Determine whether arbitrary node N denotes an effectively volatile + -- object and if it does, emit an error. + + ----------------- + -- Flag_Object -- + ----------------- + + function Flag_Object (N : Node_Id) return Traverse_Result is + Id : Entity_Id; + + begin + -- Do not consider nested function calls because they have already + -- been processed during their own resolution. + + if Nkind (N) = N_Function_Call then + return Skip; + + elsif Is_Entity_Name (N) and then Present (Entity (N)) then + Id := Entity (N); + + if Is_Object (Id) + and then Is_Effectively_Volatile (Id) + and then (Async_Writers_Enabled (Id) + or else Effective_Reads_Enabled (Id)) + then + Error_Msg_N + ("volatile object cannot appear in this context (SPARK " + & "RM 7.1.3(11))", N); + return Skip; + end if; + end if; + + return OK; + end Flag_Object; + + procedure Flag_Objects is new Traverse_Proc (Flag_Object); + + -- Start of processing for Flag_Effectively_Volatile_Objects + + begin + Flag_Objects (Expr); + end Flag_Effectively_Volatile_Objects; + -------------------- -- Insert_Default -- -------------------- @@ -3461,7 +3514,6 @@ then Set_Is_Controlling_Actual (Actval); end if; - end if; -- If the default expression raises constraint error, then just @@ -4473,10 +4525,8 @@ -- they are not standard Ada legality rule. Internally generated -- temporaries are ignored. - if SPARK_Mode = On - and then Comes_From_Source (A) - and then Is_Effectively_Volatile_Object (A) - then + if SPARK_Mode = On and then Comes_From_Source (A) then + -- An effectively volatile object may act as an actual when the -- corresponding formal is of a non-scalar effectively volatile -- type (SPARK RM 7.1.3(11)). @@ -4493,10 +4543,23 @@ elsif Is_Unchecked_Conversion_Instance (Nam) then null; - else + -- The actual denotes an object + + elsif Is_Effectively_Volatile_Object (A) then Error_Msg_N ("volatile object cannot act as actual in a call (SPARK " & "RM 7.1.3(11))", A); + + -- Otherwise the actual denotes an expression. Inspect the + -- expression and flag each effectively volatile object with + -- enabled property Async_Writers or Effective_Reads as illegal + -- because it apprears within an interfering context. Note that + -- this is usually done in Resolve_Entity_Name, but when the + -- effectively volatile object appears as an actual in a call, + -- the call must be resolved first. + + else + Flag_Effectively_Volatile_Objects (A); end if; -- Detect an external variable with an enabled property that Index: sem_util.adb =================================================================== --- sem_util.adb (revision 235491) +++ sem_util.adb (working copy) @@ -9314,7 +9314,7 @@ Has_Default_Aspect (Typ) or else Has_Full_Default_Initialization (Component_Type (Typ)); - -- A protected type, record type or type extension is fully default + -- A protected type, record type, or type extension is fully default -- initialized if all its components either carry an initialization -- expression or have a type that is fully default initialized. The -- parent type of a type extension must be fully default initialized. @@ -13159,7 +13159,7 @@ when N_Function_Call => return Etype (N) /= Standard_Void_Type; - -- Attributes 'Input, 'Loop_Entry, 'Old and 'Result produce + -- Attributes 'Input, 'Loop_Entry, 'Old, and 'Result produce -- objects. when N_Attribute_Reference => @@ -13346,14 +13346,15 @@ is function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean; -- Determine whether an arbitrary node denotes a call to a protected - -- entry, function or procedure in prefixed form where the prefix is + -- entry, function, or procedure in prefixed form where the prefix is -- Obj_Ref. function Within_Check (Nod : Node_Id) return Boolean; -- Determine whether an arbitrary node appears in a check node function Within_Subprogram_Call (Nod : Node_Id) return Boolean; - -- Determine whether an arbitrary node appears in a procedure call + -- Determine whether an arbitrary node appears in an entry, function, or + -- procedure call. function Within_Volatile_Function (Id : Entity_Id) return Boolean; -- Determine whether an arbitrary entity appears in a volatile function @@ -13405,7 +13406,7 @@ if Nkind (Par) in N_Raise_xxx_Error then return True; - -- Prevent the search from going too far + -- Prevent the search from going too far elsif Is_Body_Or_Package_Declaration (Par) then exit; @@ -13435,7 +13436,7 @@ then return True; - -- Prevent the search from going too far + -- Prevent the search from going too far elsif Is_Body_Or_Package_Declaration (Par) then exit; @@ -13481,8 +13482,8 @@ if Nkind (Context) = N_Assignment_Statement then return True; - -- The volatile object is part of the initialization expression of - -- another object. + -- The volatile object is part of the initialization expression of + -- another object. elsif Nkind (Context) = N_Object_Declaration and then Present (Expression (Context)) @@ -13497,21 +13498,21 @@ if Is_Return_Object (Obj_Id) then return Within_Volatile_Function (Obj_Id); - -- Otherwise this is a normal object initialization + -- Otherwise this is a normal object initialization else return True; end if; - -- The volatile object acts as the name of a renaming declaration + -- The volatile object acts as the name of a renaming declaration elsif Nkind (Context) = N_Object_Renaming_Declaration and then Name (Context) = Obj_Ref then return True; - -- The volatile object appears as an actual parameter in a call to an - -- instance of Unchecked_Conversion whose result is renamed. + -- The volatile object appears as an actual parameter in a call to an + -- instance of Unchecked_Conversion whose result is renamed. elsif Nkind (Context) = N_Function_Call and then Is_Entity_Name (Name (Context)) @@ -13520,14 +13521,14 @@ then return True; - -- The volatile object is actually the prefix in a protected entry, - -- function, or procedure call. + -- The volatile object is actually the prefix in a protected entry, + -- function, or procedure call. elsif Is_Protected_Operation_Call (Context) then return True; - -- The volatile object appears as the expression of a simple return - -- statement that applies to a volatile function. + -- The volatile object appears as the expression of a simple return + -- statement that applies to a volatile function. elsif Nkind (Context) = N_Simple_Return_Statement and then Expression (Context) = Obj_Ref @@ -13535,8 +13536,8 @@ return Within_Volatile_Function (Return_Statement_Entity (Context)); - -- The volatile object appears as the prefix of a name occurring in a - -- non-interfering context. + -- The volatile object appears as the prefix of a name occurring in a + -- non-interfering context. elsif Nkind_In (Context, N_Attribute_Reference, N_Explicit_Dereference, @@ -13550,8 +13551,8 @@ then return True; - -- The volatile object appears as the expression of a type conversion - -- occurring in a non-interfering context. + -- The volatile object appears as the expression of a type conversion + -- occurring in a non-interfering context. elsif Nkind_In (Context, N_Type_Conversion, N_Unchecked_Type_Conversion) @@ -13562,21 +13563,22 @@ then return True; - -- Allow references to volatile objects in various checks. This is - -- not a direct SPARK 2014 requirement. + -- Allow references to volatile objects in various checks. This is not a + -- direct SPARK 2014 requirement. elsif Within_Check (Context) then return True; - -- Assume that references to effectively volatile objects that appear - -- as actual parameters in a subprogram call are always legal. A full - -- legality check is done when the actuals are resolved. + -- Assume that references to effectively volatile objects that appear + -- as actual parameters in a subprogram call are always legal. A full + -- legality check is done when the actuals are resolved (see routine + -- Resolve_Actuals). elsif Within_Subprogram_Call (Context) then return True; - -- Otherwise the context is not suitable for an effectively volatile - -- object. + -- Otherwise the context is not suitable for an effectively volatile + -- object. else return False; @@ -13888,7 +13890,7 @@ begin -- Verify that prefix is analyzed and has the proper form. Note that - -- the attributes Elab_Spec, Elab_Body and Elab_Subp_Body which also + -- the attributes Elab_Spec, Elab_Body, and Elab_Subp_Body, which also -- produce the address of an entity, do not analyze their prefix -- because they denote entities that are not necessarily visible. -- Neither of them can apply to a protected type. @@ -16034,7 +16036,7 @@ procedure Copy_Itype_With_Replacement (New_Itype : Entity_Id) is begin - -- Translate Next_Entity, Scope and Etype fields, in case they + -- Translate Next_Entity, Scope, and Etype fields, in case they -- reference entities that have been mapped into copies. Set_Next_Entity (New_Itype, Assoc (Next_Entity (New_Itype))); @@ -19986,8 +19988,8 @@ return False; end if; - -- Check that the size of the component is 8, 16, 32 or 64 bits and that - -- Typ is properly aligned. + -- Check that the size of the component is 8, 16, 32, or 64 bits and + -- that Typ is properly aligned. case Size is when 8 | 16 | 32 | 64 =>