From patchwork Mon Aug 29 14:40:19 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 112070 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]) by ozlabs.org (Postfix) with SMTP id 5CBB1B6F92 for ; Tue, 30 Aug 2011 00:40:49 +1000 (EST) Received: (qmail 11036 invoked by alias); 29 Aug 2011 14:40:45 -0000 Received: (qmail 10673 invoked by uid 22791); 29 Aug 2011 14:40:39 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Mon, 29 Aug 2011 14:40:20 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 036FF2BAF57; Mon, 29 Aug 2011 10:40:20 -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 yLWvQs4kPQYf; Mon, 29 Aug 2011 10:40:19 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id DBA002BAF24; Mon, 29 Aug 2011 10:40:19 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id D96403FEE8; Mon, 29 Aug 2011 10:40:19 -0400 (EDT) Date: Mon, 29 Aug 2011 10:40:19 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Store read/write through explicit dereference in ALFA mode Message-ID: <20110829144019.GA18951@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) 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 Formal verification relies on a computation of effects based on the local effects generated in ALFA sections in ALI files. These effects should mention explicitly all read/writes to memory through explicit dereferences. This is now done with a special "HEAP" variable. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-29 Yannick Moy * alfa.ads (Name_Of_Heap_Variable): New constant name. * lib-xref-alfa.adb, lib-xref.adb, lib-xref.ads (Drefs): New global table to hold dereferences. (Add_ALFA_Xrefs): Take into account dereferences as special reads/writes to the variable "HEAP". (Enclosing_Subprogram_Or_Package): Move subprogram here. (Generate_Dereference): New procedure to store a read/write dereferencew in the table Drefs. * put_alfa.adb (Put_ALFA): Use different default than (0,0) used for the special "HEAP" var. * sem_ch4.adb (Analyze_Explicit_Dereference): Store read dereference in ALFA mode. * sem_util.adb (Note_Possible_Modification): Store write dereference in ALFA mode. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 178250) +++ sem_util.adb (working copy) @@ -10506,6 +10506,13 @@ P : constant Node_Id := Prefix (Exp); begin + -- In formal verification mode, keep track of all reads and + -- writes through explicit dereferences. + + if ALFA_Mode then + ALFA.Generate_Dereference (N, 'm'); + end if; + if Nkind (P) = N_Selected_Component and then Present ( Entry_Formal (Entity (Selector_Name (P)))) Index: alfa.ads =================================================================== --- alfa.ads (revision 178155) +++ alfa.ads (working copy) @@ -175,6 +175,11 @@ -- r = reference -- s = subprogram reference in a static call + -- Special entries for reads and writes to memory reference a special + -- variable called "HEAP". These special entries are present in every scope + -- where reads and writes to memory are present. Line and column for this + -- special variable are always 0. + -- Examples: ??? add examples here ---------------- @@ -327,6 +332,14 @@ Table_Initial => 20, Table_Increment => 200); + --------------- + -- Constants -- + --------------- + + Name_Of_Heap_Variable : constant String := "HEAP"; + -- Name of special variable used in effects to denote reads and writes + -- through explicit dereference. + ----------------- -- Subprograms -- ----------------- Index: sem_ch4.adb =================================================================== --- sem_ch4.adb (revision 178239) +++ sem_ch4.adb (working copy) @@ -1761,6 +1761,13 @@ begin Check_SPARK_Restriction ("explicit dereference is not allowed", N); + -- In formal verification mode, keep track of all reads and writes + -- through explicit dereferences. + + if ALFA_Mode then + ALFA.Generate_Dereference (N); + end if; + Analyze (P); Set_Etype (N, Any_Type); Index: put_alfa.adb =================================================================== --- put_alfa.adb (revision 178155) +++ put_alfa.adb (working copy) @@ -153,8 +153,11 @@ Write_Info_Char (S.Scope_Name (N)); end loop; + -- Default value of (0,0) is used for the special HEAP variable + -- so use another default value. + Entity_Line := 0; - Entity_Col := 0; + Entity_Col := 1; -- Loop through cross reference entries for this scope Index: lib-xref-alfa.adb =================================================================== --- lib-xref-alfa.adb (revision 178235) +++ lib-xref-alfa.adb (working copy) @@ -25,6 +25,7 @@ with ALFA; use ALFA; with Einfo; use Einfo; +with Nmake; use Nmake; with Put_ALFA; with GNAT.HTable; @@ -143,6 +144,22 @@ type Entity_Hashed_Range is range 0 .. 255; -- Size of hash table headers + --------------------- + -- Local Variables -- + --------------------- + + package Drefs is new Table.Table ( + Table_Component_Type => Xref_Entry, + Table_Index_Type => Xref_Entry_Number, + Table_Low_Bound => 1, + Table_Initial => Alloc.Xrefs_Initial, + Table_Increment => Alloc.Xrefs_Increment, + Table_Name => "Drefs"); + -- Table of cross-references for reads and writes through explicit + -- dereferences, that are output as reads/writes to the special variable + -- "HEAP". These references are added to the regular references when + -- computing ALFA cross-references. + ----------------------- -- Local Subprograms -- ----------------------- @@ -400,7 +417,9 @@ -- when we eliminate duplicate reference entries as well as references -- not suitable for local cross-references. - Rnums : array (0 .. Nrefs) of Nat; + Nrefs_Add : constant Nat := Drefs.Last; + + Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat; -- This array contains numbers of references in the Xrefs table. This -- list is sorted in output order. The extra 0'th entry is convenient -- for the call to sort. When we sort the table, we move the entries in @@ -506,6 +525,8 @@ Rnums (Nat (To)) := Rnums (Nat (From)); end Move; + Heap : Entity_Id; + -- Start of processing for Add_ALFA_Xrefs begin @@ -520,6 +541,31 @@ Rnums (J) := J; end loop; + -- Add dereferences to the set of regular references, by creating a + -- special "HEAP" variable for these special references. + + Name_Len := Name_Of_Heap_Variable'Length; + Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable; + + Atree.Unlock; + Nlists.Unlock; + Heap := Make_Defining_Identifier (Standard_Location, Name_Enter); + Atree.Lock; + Nlists.Lock; + + Set_Ekind (Heap, E_Variable); + Set_Is_Internal (Heap, True); + Set_Has_Fully_Qualified_Name (Heap); + + for J in Drefs.First .. Drefs.Last loop + Xrefs.Increment_Last; + Xrefs.Table (Xrefs.Last) := Drefs.Table (J); + Xrefs.Table (Xrefs.Last).Ent := Heap; + + Nrefs := Nrefs + 1; + Rnums (Nrefs) := Xrefs.Last; + end loop; + -- Eliminate entries not appropriate for ALFA. Done prior to sorting -- cross-references, as it discards useless references which do not have -- a proper format for the comparison function (like no location). @@ -762,16 +808,29 @@ new String'(Unique_Name (XE.Ent)); end if; - ALFA_Xref_Table.Append ( - (Entity_Name => Cur_Entity_Name, - Entity_Line => Int (Get_Logical_Line_Number (XE.Def)), - Etype => Get_Entity_Type (XE.Ent), - Entity_Col => Int (Get_Column_Number (XE.Def)), - File_Num => Dependency_Num (XE.Lun), - Scope_Num => Get_Scope_Num (XE.Ref_Scope), - Line => Int (Get_Logical_Line_Number (XE.Loc)), - Rtype => XE.Typ, - Col => Int (Get_Column_Number (XE.Loc)))); + if XE.Ent = Heap then + ALFA_Xref_Table.Append ( + (Entity_Name => Cur_Entity_Name, + Entity_Line => 0, + Etype => Get_Entity_Type (XE.Ent), + Entity_Col => 0, + File_Num => Dependency_Num (XE.Lun), + Scope_Num => Get_Scope_Num (XE.Ref_Scope), + Line => Int (Get_Logical_Line_Number (XE.Loc)), + Rtype => XE.Typ, + Col => Int (Get_Column_Number (XE.Loc)))); + else + ALFA_Xref_Table.Append ( + (Entity_Name => Cur_Entity_Name, + Entity_Line => Int (Get_Logical_Line_Number (XE.Def)), + Etype => Get_Entity_Type (XE.Ent), + Entity_Col => Int (Get_Column_Number (XE.Def)), + File_Num => Dependency_Num (XE.Lun), + Scope_Num => Get_Scope_Num (XE.Ref_Scope), + Line => Int (Get_Logical_Line_Number (XE.Loc)), + Rtype => XE.Typ, + Col => Int (Get_Column_Number (XE.Loc)))); + end if; end Add_One_Xref; end loop; @@ -877,6 +936,84 @@ end if; end Detect_And_Add_ALFA_Scope; + ------------------------------------- + -- Enclosing_Subprogram_Or_Package -- + ------------------------------------- + + function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is + Result : Entity_Id; + + begin + -- If N is the defining identifier for a subprogram, then return the + -- enclosing subprogram or package, not this subprogram. + + if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol) + and then Nkind (Parent (N)) in N_Subprogram_Specification + then + Result := Parent (Parent (Parent (N))); + else + Result := N; + end if; + + loop + exit when No (Result); + + case Nkind (Result) is + when N_Package_Specification => + Result := Defining_Unit_Name (Result); + exit; + + when N_Package_Body => + Result := Defining_Unit_Name (Result); + exit; + + when N_Subprogram_Specification => + Result := Defining_Unit_Name (Result); + exit; + + when N_Subprogram_Declaration => + Result := Defining_Unit_Name (Specification (Result)); + exit; + + when N_Subprogram_Body => + Result := Defining_Unit_Name (Specification (Result)); + exit; + + -- The enclosing subprogram for a pre- or postconditions should be + -- the subprogram to which the pragma is attached. This is not + -- always the case in the AST, as the pragma may be declared after + -- the declaration of the subprogram. Return Empty in this case. + + when N_Pragma => + if Get_Pragma_Id (Result) = Pragma_Precondition + or else + Get_Pragma_Id (Result) = Pragma_Postcondition + then + return Empty; + else + Result := Parent (Result); + end if; + + when others => + Result := Parent (Result); + end case; + end loop; + + if Nkind (Result) = N_Defining_Program_Unit_Name then + Result := Defining_Identifier (Result); + end if; + + -- Do no return a scope without a proper location + + if Present (Result) + and then Sloc (Result) = No_Location + then + return Empty; + end if; + + return Result; + end Enclosing_Subprogram_Or_Package; + ----------------- -- Entity_Hash -- ----------------- @@ -887,6 +1024,47 @@ Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1)); end Entity_Hash; + -------------------------- + -- Generate_Dereference -- + -------------------------- + + procedure Generate_Dereference + (N : Node_Id; + Typ : Character := 'r') + is + Indx : Nat; + Ref : Source_Ptr; + Ref_Scope : Entity_Id; + + begin + Ref := Original_Location (Sloc (N)); + + if Ref > No_Location then + Drefs.Increment_Last; + Indx := Drefs.Last; + + Ref_Scope := Enclosing_Subprogram_Or_Package (N); + + -- Entity is filled later on with the special "HEAP" variable + + Drefs.Table (Indx).Ent := Empty; + + Drefs.Table (Indx).Def := No_Location; + Drefs.Table (Indx).Loc := Ref; + Drefs.Table (Indx).Typ := Typ; + + -- It is as if the special "HEAP" was defined in every scope where it + -- is referenced. + + Drefs.Table (Indx).Eun := Get_Source_Unit (Ref); + Drefs.Table (Indx).Lun := Get_Source_Unit (Ref); + + Drefs.Table (Indx).Ref_Scope := Ref_Scope; + Drefs.Table (Indx).Ent_Scope := Ref_Scope; + Drefs.Table (Indx).Ent_Scope_File := Get_Source_Unit (Ref_Scope); + end if; + end Generate_Dereference; + ------------------------------------ -- Traverse_All_Compilation_Units -- ------------------------------------ Index: lib-xref.adb =================================================================== --- lib-xref.adb (revision 178155) +++ lib-xref.adb (working copy) @@ -112,9 +112,6 @@ -- Local Subprograms -- ------------------------ - function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id; - -- Return the closest enclosing subprogram of package - procedure Generate_Prim_Op_References (Typ : Entity_Id); -- For a tagged type, generate implicit references to its primitive -- operations, for source navigation. This is done right before emitting @@ -124,84 +121,6 @@ function Lt (T1, T2 : Xref_Entry) return Boolean; -- Order cross-references - ------------------------------------- - -- Enclosing_Subprogram_Or_Package -- - ------------------------------------- - - function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is - Result : Entity_Id; - - begin - -- If N is the defining identifier for a subprogram, then return the - -- enclosing subprogram or package, not this subprogram. - - if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol) - and then Nkind (Parent (N)) in N_Subprogram_Specification - then - Result := Parent (Parent (Parent (N))); - else - Result := N; - end if; - - loop - exit when No (Result); - - case Nkind (Result) is - when N_Package_Specification => - Result := Defining_Unit_Name (Result); - exit; - - when N_Package_Body => - Result := Defining_Unit_Name (Result); - exit; - - when N_Subprogram_Specification => - Result := Defining_Unit_Name (Result); - exit; - - when N_Subprogram_Declaration => - Result := Defining_Unit_Name (Specification (Result)); - exit; - - when N_Subprogram_Body => - Result := Defining_Unit_Name (Specification (Result)); - exit; - - -- The enclosing subprogram for a pre- or postconditions should be - -- the subprogram to which the pragma is attached. This is not - -- always the case in the AST, as the pragma may be declared after - -- the declaration of the subprogram. Return Empty in this case. - - when N_Pragma => - if Get_Pragma_Id (Result) = Pragma_Precondition - or else - Get_Pragma_Id (Result) = Pragma_Postcondition - then - return Empty; - else - Result := Parent (Result); - end if; - - when others => - Result := Parent (Result); - end case; - end loop; - - if Nkind (Result) = N_Defining_Program_Unit_Name then - Result := Defining_Identifier (Result); - end if; - - -- Do no return a scope without a proper location - - if Present (Result) - and then Sloc (Result) = No_Location - then - return Empty; - end if; - - return Result; - end Enclosing_Subprogram_Or_Package; - ------------------------- -- Generate_Definition -- ------------------------- @@ -946,8 +865,8 @@ Ref := Original_Location (Sloc (Nod)); Def := Original_Location (Sloc (Ent)); - Ref_Scope := Enclosing_Subprogram_Or_Package (N); - Ent_Scope := Enclosing_Subprogram_Or_Package (Ent); + Ref_Scope := ALFA.Enclosing_Subprogram_Or_Package (N); + Ent_Scope := ALFA.Enclosing_Subprogram_Or_Package (Ent); Xrefs.Increment_Last; Indx := Xrefs.Last; Index: lib-xref.ads =================================================================== --- lib-xref.ads (revision 178222) +++ lib-xref.ads (working copy) @@ -590,6 +590,15 @@ package ALFA is + function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id; + -- Return the closest enclosing subprogram of package + + procedure Generate_Dereference + (N : Node_Id; + Typ : Character := 'r'); + -- This procedure is called to record a dereference. N is the location + -- of the dereference. + type Node_Processing is access procedure (N : Node_Id); procedure Traverse_Compilation_Unit