From patchwork Mon Jun 20 12:32:07 2016 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 637959 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 3rY9H30c9Hz9sBM for ; Mon, 20 Jun 2016 22:32:30 +1000 (AEST) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=Gv65u52/; 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=Xpz/BdCknAU7JulOGDuaH99euZNJk6n4AKltQJ410U7btWEfiO SvM6m2ECE65jCiyhN9N7foeYpzVzXMUa3ZgEhALlBrr6I4kawznCPlmIe3/EGnbV X6T7mGxlRGThJes8cmjnZvThHrMK1cpYHpKkvPzZP1LMKtV03rV5k8ii8= 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=jj6MU1kKwSYGmI6VP7zucc9P+9k=; b=Gv65u52/WYMtmZRKoEFI pkYIMs9oSZELVPvjzXCTmZBvQWjEu3cyImQ2D9Lma0wcFB9xs81e9sXujwjCD5+y at28khyuFElHBtS0NEqDoj6YiyskRIAjlloAtJe5QcPlwcOXMSx9c/5qDFMmmUvj 33jqwoY8sWMcfYkVUnXwZAA= Received: (qmail 68206 invoked by alias); 20 Jun 2016 12:32:22 -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 68101 invoked by uid 89); 20 Jun 2016 12:32:22 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: Yes, score=5.1 required=5.0 tests=AWL, BAYES_99, BAYES_999, RCVD_IN_DNSWL_NONE, SPF_PASS, T_FILL_THIS_FORM_SHORT autolearn=no version=3.3.2 spammy=agrees, (unknown), Prot_2_Id, prot_3_id 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, 20 Jun 2016 12:32:09 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 4F82011668B; Mon, 20 Jun 2016 08:32:07 -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 B9I7+qF-t8F8; Mon, 20 Jun 2016 08:32:07 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 3C83911667F; Mon, 20 Jun 2016 08:32:07 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 3B72C40C; Mon, 20 Jun 2016 08:32:07 -0400 (EDT) Date: Mon, 20 Jun 2016 08:32:07 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Reimplementation of type invariants Message-ID: <20160620123207.GA29705@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch prevents the insertion of the invariant procedure declaration and body when the context is a generic unit. This ensures that generated code does not permiate the template. ------------ -- Source -- ------------ -- tester.ads package Tester is type Type_Id is (Ext_1_Id, Ext_1_FV_Id, Ext_2_Id, Ext_3_Id, Ext_4_Id, Ext_4_FV_Id, Ext_5_Id, Ext_6_Id, Ext_6_FV_Id, Ext_7_Id, Ext_8_Id, Iface_1_Id, Iface_2_Id, Iface_3_Id, Iface_4_Id, Par_1_Id, Par_2_FV_Id, Par_3_Id, Par_4_Id, Par_4_FV_Id, Prot_1_FV_Id, Prot_2_Id, Prot_3_Id, Prot_3_FV_Id, Synch_1_Id, Synch_2_Id, Tag_1_Id, Tag_2_Id, Tag_3_Id, Tag_4_Id, Tag_4_FV_Id, Tag_5_Id, Tag_6_Id, Tag_7_Id, Tag_8_Id, Tag_9_Id, Tag_10_Id, Tag_11_Id, Tag_12_Id, Tag_13_Id, Tag_14_Id, Tag_15_Id, Tag_15_FV_Id, Tag_16_Id, Tag_17_Id, Tag_18_Id, Tag_19_Id, Tag_20_Id, Tag_20_FV_Id, Tag_21_Id, Tag_22_Id, Tag_23_Id, Tag_24_Id, Tag_24_FV_Id, Tag_25_Id, Tag_26_Id, Tag_27_Id, Tag_28_Id, Task_1_Id, Task_2_Id, Task_2_FV_Id, Untag_1_Id, Untag_2_Id, Untag_3_Id, Untag_4_Id, Untag_5_Id, Untag_6_Id, Untag_7_Id, Untag_8_Id, Untag_9_Id); type Results is array (Type_Id) of Boolean; function Mark (Typ : Type_Id) return Boolean; -- Mark the result for a particular type as verified. The function always -- returns True. procedure Reset_Results; -- Reset the internally kept result state procedure Test_Results (Test_Id : String; Exp : Results); -- Ensure that the internally kept result state agrees with expected -- results Exp. Emit an error if this is not the case. end Tester; -- tester.adb with Ada.Text_IO; use Ada.Text_IO; package body Tester is State : Results; ---------- -- Mark -- ---------- function Mark (Typ : Type_Id) return Boolean is begin State (Typ) := True; return True; end Mark; ------------------- -- Reset_Results -- ------------------- procedure Reset_Results is begin State := (others => False); end Reset_Results; ------------------ -- Test_Results -- ------------------ procedure Test_Results (Test_Id : String; Exp : Results) is Exp_Val : Boolean; Posted : Boolean := False; State_Val : Boolean; begin for Index in Results'Range loop Exp_Val := Exp (Index); State_Val := State (Index); if State_Val /= Exp_Val then if not Posted then Posted := True; Put_Line (Test_Id & ": ERROR"); end if; Put_Line (" Expected: " & Exp_Val'Img & " for " & Index'Img); Put_Line (" Got: " & State_Val'Img); end if; end loop; if not Posted then Put_Line (Test_Id & ": OK"); end if; end Test_Results; end Tester; -- gen_invariants.ads with Tester; use Tester; generic package Gen_Invariants is type Untag_1 is private with Type_Invariant => Mark (Untag_1_Id); private type Untag_1 is null record; Obj_1 : Untag_1; end Gen_Invariants; ----------------- -- Compilation -- ----------------- $ gcc -c -gnata -gnatDG gen_invariants.ads $ grep "Invariant" gen_invariants.ads.dg Tested on x86_64-pc-linux-gnu, committed on trunk 2016-06-20 Hristian Kirtchev * exp_ch7.adb (Build_Invariant_Procedure_Body): Always install the scope of the invariant procedure in order to produce better error messages. Do not insert the body when the context is a generic unit. (Build_Invariant_Procedure_Declaration): Perform minimal decoration of the invariant procedure and its formal parameter in case they are not analyzed. Do not insert the declaration when the context is a generic unit. Index: exp_ch7.adb =================================================================== --- exp_ch7.adb (revision 237598) +++ exp_ch7.adb (working copy) @@ -4622,7 +4622,16 @@ Set_Ghost_Mode_From_Entity (Work_Typ); + -- Emulate the environment of the invariant procedure by installing + -- its scope and formal parameters. Note that this is not need, but + -- having the scope of the invariant procedure installed helps with + -- the detection of invariant-related errors. + + Push_Scope (Proc_Id); + Install_Formals (Proc_Id); + Obj_Id := First_Formal (Proc_Id); + pragma Assert (Present (Obj_Id)); -- The "partial" invariant procedure verifies the invariants of the -- partial view only. @@ -4631,14 +4640,6 @@ pragma Assert (Present (Priv_Typ)); Freeze_Typ := Priv_Typ; - -- Emulate the environment of the invariant procedure by installing - -- its scope and formal parameters. Note that this is not need, but - -- having the scope of the invariant procedure installed helps with - -- the detection of invariant-related errors. - - Push_Scope (Proc_Id); - Install_Formals (Proc_Id); - Add_Type_Invariants (Priv_Typ => Priv_Typ, Full_Typ => Empty, @@ -4646,8 +4647,6 @@ Obj_Id => Obj_Id, Checks => Stmts); - End_Scope; - -- Otherwise the "full" invariant procedure verifies the invariants of -- the full view, all array or record components, as well as class-wide -- invariants inherited from parent types or interfaces. In addition, it @@ -4744,6 +4743,8 @@ Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts); end if; + End_Scope; + -- At this point there should be at least one invariant check. If this -- is not the case, then the invariant-related flags were not properly -- set, or there is a missing invariant procedure on one of the array @@ -4759,6 +4760,12 @@ Stmts := New_List (Make_Null_Statement (Loc)); end if; + -- Generate: + -- procedure [Partial_]Invariant (_object : ) is + -- begin + -- + -- end [Partial_]Invariant; + Proc_Body := Make_Subprogram_Body (Loc, Specification => @@ -4769,16 +4776,30 @@ Statements => Stmts)); Proc_Body_Id := Defining_Entity (Proc_Body); + -- Perform minor decoration in case the body is not analyzed + Set_Ekind (Proc_Body_Id, E_Subprogram_Body); Set_Etype (Proc_Body_Id, Standard_Void_Type); - Set_Scope (Proc_Body_Id, Scope (Typ)); + Set_Scope (Proc_Body_Id, Current_Scope); -- Link both spec and body to avoid generating duplicates Set_Corresponding_Body (Proc_Decl, Proc_Body_Id); Set_Corresponding_Spec (Proc_Body, Proc_Id); - Append_Freeze_Action (Freeze_Typ, Proc_Body); + -- The body should not be inserted into the tree when the context is a + -- generic unit because it is not part of the template. Note that the + -- body must still be generated in order to resolve the invariants. + + if Inside_A_Generic then + null; + + -- Otherwise the body is part of the freezing actions of the type + + else + Append_Freeze_Action (Freeze_Typ, Proc_Body); + end if; + Ghost_Mode := Save_Ghost_Mode; end Build_Invariant_Procedure_Body; @@ -4794,8 +4815,10 @@ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Proc_Id : Entity_Id; - Typ_Decl : Node_Id; + Proc_Decl : Node_Id; + Proc_Id : Entity_Id; + Proc_Nam : Name_Id; + Typ_Decl : Node_Id; CRec_Typ : Entity_Id; -- The corresponding record type of Full_Typ @@ -4869,24 +4892,27 @@ -- procedure. if Partial_Invariant then - Proc_Id := - Make_Defining_Identifier (Loc, - Chars => - New_External_Name (Chars (Work_Typ), "Partial_Invariant")); + Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant"); - Set_Ekind (Proc_Id, E_Procedure); - Set_Is_Partial_Invariant_Procedure (Proc_Id); - Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id); - -- Otherwise the caller requests the declaration of the "full" invariant -- procedure. else - Proc_Id := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (Work_Typ), "Invariant")); + Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant"); + end if; - Set_Ekind (Proc_Id, E_Procedure); + Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam); + + -- Perform minor decoration in case the declaration is not analyzed + + Set_Ekind (Proc_Id, E_Procedure); + Set_Etype (Proc_Id, Standard_Void_Type); + Set_Scope (Proc_Id, Current_Scope); + + if Partial_Invariant then + Set_Is_Partial_Invariant_Procedure (Proc_Id); + Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id); + else Set_Is_Invariant_Procedure (Proc_Id); Set_Invariant_Procedure (Work_Typ, Proc_Id); end if; @@ -4938,12 +4964,19 @@ -- of the current type instance. Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject); + + -- Perform minor decoration in case the declaration is not analyzed + Set_Ekind (Obj_Id, E_In_Parameter); + Set_Etype (Obj_Id, Work_Typ); + Set_Scope (Obj_Id, Proc_Id); + Set_First_Entity (Proc_Id, Obj_Id); + -- Generate: -- procedure [Partial_]Invariant (_object : ); - Insert_After_And_Analyze (Typ_Decl, + Proc_Decl := Make_Subprogram_Declaration (Loc, Specification => Make_Procedure_Specification (Loc, @@ -4952,8 +4985,21 @@ Make_Parameter_Specification (Loc, Defining_Identifier => Obj_Id, Parameter_Type => - New_Occurrence_Of (Work_Typ, Loc)))))); + New_Occurrence_Of (Work_Typ, Loc))))); + -- The declaration should not be inserted into the tree when the context + -- is a generic unit because it is not part of the template. + + if Inside_A_Generic then + null; + + -- Otherwise insert the declaration + + else + pragma Assert (Present (Typ_Decl)); + Insert_After_And_Analyze (Typ_Decl, Proc_Decl); + end if; + Ghost_Mode := Save_Ghost_Mode; end Build_Invariant_Procedure_Declaration;