From patchwork Mon Oct 26 15:40:29 2015 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 536079 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 EF1441402B2 for ; Tue, 27 Oct 2015 02:40:45 +1100 (AEDT) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=FAp5Kxjv; 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=fBYB4LfxvVD3mn31U9x8dHjwjgAaeA8RVmnmn2pFfzGBXTleDg L5TmSx8DlRG1e3JePK5tD80JemtDy8P2Vt+MTfHoU36xRg28NHelGBstWfjSqm2i GUatrcES1hGQxEir2BM+Ul4l6yEj++ImU2Tn2HdKV+1qshCnXK+NdNyh8= 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=QtDn/HRw3X8iWcbMEjWV/u2Qd3g=; b=FAp5KxjvNrOHjbocLqVz L+Bj/hFSJTExezSJ8WU7cU7uhQohRi49m7WSWK8w76o3ELDcO2RD4cwL97k5Y9rr cFCfMgu5EraUqpDIZd/bxmSqGlcHrR3kZwMX5ttHkizxIu9XhK5dtt6w619F+kOH QCikkX0ZeQaG9Wf92wIiBrQ= Received: (qmail 30266 invoked by alias); 26 Oct 2015 15:40:34 -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 30251 invoked by uid 89); 26 Oct 2015 15:40:33 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=4.8 required=5.0 tests=BAYES_99, BAYES_999, KAM_ASCII_DIVIDERS, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_LOW autolearn=no version=3.3.2 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; Mon, 26 Oct 2015 15:40:31 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 9677F29771; Mon, 26 Oct 2015 11:40:29 -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 qnrKXg0s5Agg; Mon, 26 Oct 2015 11:40:29 -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 82490D3B15; Mon, 26 Oct 2015 11:40:29 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 7A3FD18F; Mon, 26 Oct 2015 11:40:29 -0400 (EDT) Date: Mon, 26 Oct 2015 11:40:29 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Ghost types, objects and synchronization Message-ID: <20151026154029.GA120587@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch implements the following SPARK RM 6.9(19) rule: A ghost type shall not have a task or protected part. A ghost object shall not be of a type which yields synchronized objects. A ghost object shall not have a volatile part. A synchronized state abstraction shall not be a ghost state abstraction. ------------ -- Source -- ------------ -- yso.ads -- Yields synchronized object with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control; package YSO with SPARK_Mode is -- Protected interface type Prot_Iface is protected interface; -- Protected type protected type Prot_Typ is entry Ent; end Prot_Typ; -- Synchronized interface type Sync_Iface is synchronized interface; -- Task interface type Task_Iface is task interface; -- Task type task type Task_Typ; -- Array type type Arr_Typ is array (1 .. 5) of Prot_Typ; -- Descendant of Suspension_Object type Sus_Obj is new Suspension_Object; -- Record type type Rec_Typ is record Comp_1 : Prot_Typ; Comp_2 : Task_Typ; Comp_3 : Arr_Typ; Comp_4 : Sus_Obj; Comp_5 : Suspension_Object; end record with Volatile; -- Type extension type Deriv_Typ is new Rec_Typ; end YSO; -- lr19.ads th Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control; with YSO; use YSO; package LR19 with SPARK_Mode, -- A synchronized state abstraction shall not be a ghost state -- abstraction. Abstract_State => ((Error_1 with Ghost, Synchronous), -- Error (Error_2 with Synchronous, Ghost)) -- Error is -- A ghost type shall not have a task or protected type protected type Prot_Typ is end Prot_Typ; task type Task_Typ; protected type Error_3 with Ghost is end Error_3; -- Error protected Error_4 with Ghost is end Error_4; -- Error task type Error_5 with Ghost; -- Error task Error_6 with Ghost; -- Error type Error_7 is record Comp : Prot_Typ; -- Error end record with Ghost, Volatile; type Error_8 is array (1 .. 3) of Task_Typ with Ghost; -- Error -- A ghost object shall not be of a type which yields a synchonized object Error_9 : Prot_Typ with Ghost; -- Error Error_10 : Task_Typ with Ghost; -- Error Error_11 : Arr_Typ with Ghost; -- Error Error_12 : Sus_Obj with Ghost; -- Error Error_13 : Suspension_Object with Ghost; -- Error Error_14 : Rec_Typ with Ghost; -- Error Error_15 : Deriv_Typ with Ghost; -- Error -- A ghost object shall not have a [n effectively?] volatile part type Vol_Int is new Integer range 1 .. 5 with Volatile; type Vol_Rec is record Comp : Vol_Int; end record with Volatile; Error_16 : Integer with Ghost, Volatile; -- Error Error_17 : Vol_Int with Ghost; -- Error Error_18 : Vol_Rec with Ghost; -- Error end LR19; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c lr19.ads lr19.ads:10:27: synchronized state cannot be ghost lr19.ads:11:27: synchronized state cannot be ghost lr19.ads:18:32: aspect "GHOST" cannot apply to a protected type lr19.ads:19:27: aspect "GHOST" cannot apply to a protected type lr19.ads:20:27: aspect "GHOST" cannot apply to a task type lr19.ads:21:22: aspect "GHOST" cannot apply to a task type lr19.ads:23:09: ghost type "Error_7" cannot be volatile lr19.ads:24:07: component "Comp" of ghost type "ERROR_7" cannot be concurrent lr19.ads:27:04: ghost array type "ERROR_8" cannot have concurrent component type lr19.ads:31:04: ghost object "Error_9" cannot be synchronized lr19.ads:31:29: aspect "GHOST" cannot apply to a protected object lr19.ads:32:04: ghost object "Error_10" cannot be synchronized lr19.ads:32:29: aspect "GHOST" cannot apply to a task object lr19.ads:33:04: ghost object "Error_11" cannot be synchronized lr19.ads:34:04: ghost object "Error_12" cannot be synchronized lr19.ads:35:04: ghost object "Error_13" cannot be synchronized lr19.ads:36:04: ghost object "Error_14" cannot be synchronized lr19.ads:37:04: ghost object "Error_15" cannot be synchronized lr19.ads:47:04: ghost object "Error_16" cannot be volatile lr19.ads:48:04: ghost object "Error_17" cannot be volatile lr19.ads:49:04: ghost object "Error_18" cannot be volatile Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-26 Hristian Kirtchev * contracts.adb (Analyze_Object_Contract): Set and restore the SPARK_Mode for both constants and objects. Factor out the semantic checks concerning Ghost objects. * freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a concurrent component type. (Freeze_Entity): A Ghost type cannot also be concurrent. (Freeze_Record_Type): A Ghost record type cannot have a concurrent component. * sem_prag.adb (Analyze_Abstract_State): A Ghost abstract state cannot also be synchronized. (Check_Ghost_Synchronous): New routine. * sem_util.adb (Yields_Synchronized_Object): Correct the case of record components to account for the case where the type has no component list. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 229374) +++ sem_prag.adb (working copy) @@ -10068,6 +10068,11 @@ -- Opt is not a duplicate property and sets the flag Status. -- (SPARK RM 7.1.4(2)) + procedure Check_Ghost_Synchronous; + -- Ensure that the abstract state is not subject to both Ghost + -- and Synchronous simple options. Emit an error if this is the + -- case. + procedure Create_Abstract_State (Nam : Name_Id; Decl : Node_Id; @@ -10320,6 +10325,20 @@ Status := True; end Check_Duplicate_Property; + ----------------------------- + -- Check_Ghost_Synchronous -- + ----------------------------- + + procedure Check_Ghost_Synchronous is + begin + -- A synchronized abstract state cannot be Ghost and vice + -- versa (SPARK RM 6.9(19)). + + if Ghost_Seen and Synchronous_Seen then + SPARK_Msg_N ("synchronized state cannot be ghost", State); + end if; + end Check_Ghost_Synchronous; + --------------------------- -- Create_Abstract_State -- --------------------------- @@ -10464,6 +10483,7 @@ elsif Chars (Opt) = Name_Ghost then Check_Duplicate_Option (Opt, Ghost_Seen); + Check_Ghost_Synchronous; if Present (State_Id) then Set_Is_Ghost_Entity (State_Id); @@ -10473,6 +10493,7 @@ elsif Chars (Opt) = Name_Synchronous then Check_Duplicate_Option (Opt, Synchronous_Seen); + Check_Ghost_Synchronous; -- Option Part_Of without an encapsulating state is -- illegal (SPARK RM 7.1.4(9)). Index: freeze.adb =================================================================== --- freeze.adb (revision 229357) +++ freeze.adb (working copy) @@ -2806,6 +2806,15 @@ then Set_Alignment (Arr, Alignment (Component_Type (Arr))); end if; + + -- A Ghost type cannot have a component of protected or task type + -- (SPARK RM 6.9(19)). + + if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then + Error_Msg_N + ("ghost array type & cannot have concurrent component type", + Arr); + end if; end Freeze_Array_Type; ------------------------------- @@ -4341,6 +4350,25 @@ Next_Component (Comp); end loop; end if; + + -- A Ghost type cannot have a component of protected or task type + -- (SPARK RM 6.9(19)). + + if Is_Ghost_Entity (Rec) then + Comp := First_Component (Rec); + while Present (Comp) loop + if Comes_From_Source (Comp) + and then Is_Concurrent_Type (Etype (Comp)) + then + Error_Msg_Name_1 := Chars (Rec); + Error_Msg_N + ("component & of ghost type % cannot be concurrent", + Comp); + end if; + + Next_Component (Comp); + end loop; + end if; end if; -- Make sure that if we have an iterator aspect, then we have @@ -5091,12 +5119,19 @@ end if; end; - -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8)) + if Is_Ghost_Entity (E) then - if Is_Ghost_Entity (E) - and then Is_Effectively_Volatile (E) - then - Error_Msg_N ("ghost type & cannot be volatile", E); + -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify + -- this legality rule first to five a finer-grained diagnostic. + + if Is_Concurrent_Type (E) then + Error_Msg_N ("ghost type & cannot be concurrent", E); + + -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8)) + + elsif Is_Effectively_Volatile (E) then + Error_Msg_N ("ghost type & cannot be volatile", E); + end if; end if; -- Deal with special cases of freezing for subtype Index: sem_util.adb =================================================================== --- sem_util.adb (revision 229374) +++ sem_util.adb (working copy) @@ -20121,7 +20121,8 @@ -------------------------------- function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is - Id : Entity_Id; + Has_Sync_Comp : Boolean := False; + Id : Entity_Id; begin -- An array type yields a synchronized object if its component type @@ -20154,11 +20155,16 @@ Id := First_Entity (Typ); while Present (Id) loop if Comes_From_Source (Id) then - if Ekind (Id) = E_Component - and then not Yields_Synchronized_Object (Etype (Id)) - then - return False; + if Ekind (Id) = E_Component then + if Yields_Synchronized_Object (Etype (Id)) then + Has_Sync_Comp := True; + -- The component does not yield a synchronized object + + else + return False; + end if; + elsif Ekind (Id) = E_Discriminant and then Present (Expression (Parent (Id))) then @@ -20181,7 +20187,7 @@ -- If we get here, then all discriminants lack default values and all -- components are of a type that yields a synchronized object. - return True; + return Has_Sync_Comp; -- A synchronized interface type yields a synchronized object by default Index: contracts.adb =================================================================== --- contracts.adb (revision 229373) +++ contracts.adb (working copy) @@ -648,10 +648,34 @@ end if; end if; + -- The anonymous object created for a single concurrent type inherits + -- the SPARK_Mode from the type. Due to the timing of contract analysis, + -- delayed pragmas may be subject to the wrong SPARK_Mode, usually that + -- of the enclosing context. To remedy this, restore the original mode + -- of the related anonymous object. + + if Is_Single_Concurrent_Object (Obj_Id) + and then Present (SPARK_Pragma (Obj_Id)) + then + Restore_Mode := True; + Save_SPARK_Mode_And_Set (Obj_Id, Mode); + end if; + -- Constant-related checks if Ekind (Obj_Id) = E_Constant then + -- Analyze indicator Part_Of + + Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); + + -- Check whether the lack of indicator Part_Of agrees with the + -- placement of the constant with respect to the state space. + + if No (Prag) then + Check_Missing_Part_Of (Obj_Id); + end if; + -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). -- This check is relevant only when SPARK_Mode is on, as it is not -- a standard Ada legality rule. Internally-generated constants that @@ -666,32 +690,10 @@ Error_Msg_N ("constant cannot be volatile", Obj_Id); end if; - Prag := Get_Pragma (Obj_Id, Pragma_Part_Of); - - -- Check whether the lack of indicator Part_Of agrees with the - -- placement of the constant with respect to the state space. - - if No (Prag) then - Check_Missing_Part_Of (Obj_Id); - end if; - -- Variable-related checks else pragma Assert (Ekind (Obj_Id) = E_Variable); - -- The anonymous object created for a single concurrent type inherits - -- the SPARK_Mode from the type. Due to the timing of contract - -- analysis, delayed pragmas may be subject to the wrong SPARK_Mode, - -- usually that of the enclosing context. To remedy this, restore the - -- original SPARK_Mode of the related variable. - - if Is_Single_Concurrent_Object (Obj_Id) - and then Present (SPARK_Pragma (Obj_Id)) - then - Restore_Mode := True; - Save_SPARK_Mode_And_Set (Obj_Id, Mode); - end if; - -- Analyze all external properties Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); @@ -834,44 +836,42 @@ & "protected type %"), Obj_Id); end if; end if; + end if; - if Is_Ghost_Entity (Obj_Id) then + -- Common checks - -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8)) + if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then - if Is_Effectively_Volatile (Obj_Id) then - Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id); + -- A Ghost object cannot be of a type that yields a synchronized + -- object (SPARK RM 6.9(19)). - -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)) + if Yields_Synchronized_Object (Obj_Typ) then + Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); - elsif Is_Imported (Obj_Id) then - Error_Msg_N ("ghost object & cannot be imported", Obj_Id); + -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and + -- SPARK RM 6.9(19)). - elsif Is_Exported (Obj_Id) then - Error_Msg_N ("ghost object & cannot be exported", Obj_Id); - end if; - end if; + elsif Is_Effectively_Volatile (Obj_Id) then + Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); - -- Restore the SPARK_Mode of the enclosing context after all delayed - -- pragmas have been analyzed. + -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)). + -- One exception to this is the object that represents the dispatch + -- table of a Ghost tagged type, as the symbol needs to be exported. - if Restore_Mode then - Restore_SPARK_Mode (Mode); - end if; - end if; - - -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One - -- exception to this is the object that represents the dispatch table of - -- a Ghost tagged type, as the symbol needs to be exported. - - if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then - if Is_Exported (Obj_Id) then + elsif Is_Exported (Obj_Id) then Error_Msg_N ("ghost object & cannot be exported", Obj_Id); elsif Is_Imported (Obj_Id) then Error_Msg_N ("ghost object & cannot be imported", Obj_Id); end if; end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + if Restore_Mode then + Restore_SPARK_Mode (Mode); + end if; end Analyze_Object_Contract; -----------------------------------