ada: Improve ghost region creation for pragmas

gcc/ada/ChangeLog:

	* atree.adb (Mark_New_Ghost_Node): Set Is_Implicit_Ghost for
	all newly created nodes.
	* gen_il-fields.ads (Is_Implicit_Ghost): New attribute.
	* gen_il-gen-gen_entities.adb (Entity_Kind): Add Is_Implicit_Ghost
	attribute.
	* ghost.adb (Ghost_Policy_In_Effect): Implicit_Ghost_Entities inside
	pragmas get the ghost mode from the region isntead of the global
	ghost policy.
	(Ghost_Assertion_Level_In_Effect): New function that returns the
	applicable assertion level for the given entity in a similar manner
	as Ghost_Policy_In_Effect.
	(Install_Ghost_Region): Set Is_Inside_Statement_Or_Pragma attribute.
	(Mark_And_Set_Ghost_Body): Update the logic for deriving the ghost
	region.
	(Set_Ghost_Mode): Ignored pragmas attached to checked ghost entities
	now create an ignored ghost region. Pragmas attached to non-ghost
	entities create the ghost region based on the policy applied to the
	given pragma.
	* opt.ads (Ghost_Config_Type): add new attribute
	Is_Inside_Statement_Or_Pragama to track whether we should take the
	active ghost mode from the ghost region for implicit ghost entities.
	* sem_prag.adb (Analyze_Pragma): Mark entities that have an explicit
	ghost pragma as non-implicit ghost.

diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index 197d1ee5121075a11eee1366d93d893cd70e84d6..14d9ba4bb2fd90868c79fe6aeaf65a971c5dcc2d 100644 (file)
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -1807,6 +1807,7 @@ package body Atree is
             Set_Is_Checked_Ghost_Entity (N);
             Set_Ghost_Assertion_Level
               (N, Ghost_Config.Ghost_Mode_Assertion_Level);
+            Set_Is_Implicit_Ghost (N);
          end if;
 
       elsif Ghost_Config.Ghost_Mode = Ignore then
@@ -1814,6 +1815,7 @@ package body Atree is
             Set_Is_Ignored_Ghost_Entity (N);
             Set_Ghost_Assertion_Level
               (N, Ghost_Config.Ghost_Mode_Assertion_Level);
+            Set_Is_Implicit_Ghost (N);
          end if;
 
          Set_Is_Ignored_Ghost_Node (N);

diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads
index c9f9bc2c5ba6126db98b1fc126d63de10def82d9..6ff9866e64311e410cd0c4feb4a61f9b386678ce 100644 (file)
--- a/gcc/ada/gen_il-fields.ads
+++ b/gcc/ada/gen_il-fields.ads
@@ -743,6 +743,7 @@ package Gen_IL.Fields is
       Is_Immediately_Visible,
       Is_Implementation_Defined,
       Is_Implicit_Full_View,
+      Is_Implicit_Ghost,
       Is_Imported,
       Is_Independent,
       Is_Initial_Condition_Procedure,

diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb
index dd07b7a6e6e505fff07b538f8311ce3f582e7675..476e69d22cc040412631df861d1deb6ec5ed2f59 100644 (file)
--- a/gcc/ada/gen_il-gen-gen_entities.adb
+++ b/gcc/ada/gen_il-gen-gen_entities.adb
@@ -159,6 +159,7 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Is_Ignored_Ghost_Entity, Flag),
         Sm (Is_Immediately_Visible, Flag),
         Sm (Is_Implementation_Defined, Flag),
+        Sm (Is_Implicit_Ghost, Flag),
         Sm (Is_Imported, Flag),
         Sm (Is_Independent, Flag),
         Sm (Is_Inlined, Flag),

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index ae20ef972c82bb923dfa63c71b37c0c25113df56..bfe6bff0751eecd97a2c22707158238fcb9c6cb9 100644 (file)
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -94,15 +94,30 @@ package body Ghost is
    --  Returns the Assertion_Level entity if the node has a Ghost aspect and
    --  the Ghost aspect is using an Assertion_Level.
 
+   function Ghost_Assertion_Level_In_Effect (Id : Entity_Id) return Entity_Id;
+   --  Returns the ghost level applicable for the given entity Id in a similar
+   --  manner as Ghost_Policy_In_Effect.
+
    function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id;
-   --  Returns the first Assertion Policy in place for either Ghost or the
-   --  Assertion_Level associated with Ghost aspect on the the declaration node
-   --  Decl.
+   --  Returns the ghost policy applicable for the given entity Id.
+   --
+   --  SPARK RM 6.9 (3):
+   --
+   --  An object declaration which occurs inside an expression in a ghost
+   --  declaration, statement, assertion pragma or specification aspect
+   --  declaration is a ghost declaration.
+   --
+   --  If this declaration does not have the Ghost aspect specified, the
+   --  assertion policy applicable to this declaration comes from the policy
+   --  applicable to the enclosing declaration, statement, assertion pragma
+   --  or specification aspect.
+   --
+   --  Otherwise, the assertion policy applicable to an object declaration
+   --  comes either from its assertion level if any, or from the ghost
+   --  policy at the point of declaration.
 
    procedure Install_Ghost_Region
-     (Mode  : Name_Id;
-      N     : Node_Id;
-      Level : Entity_Id);
+     (Mode : Name_Id; N : Node_Id; Level : Entity_Id);
    pragma Inline (Install_Ghost_Region);
    --  Install a Ghost region comprised of mode Mode and ignored region start
    --  node N and Level as the Assertion_Level that was associated with it.
@@ -1561,6 +1576,22 @@ package body Ghost is
       return Empty;
    end Get_Ghost_Assertion_Level;
 
+   -------------------------------------
+   -- Ghost_Assertion_Level_In_Effect --
+   -------------------------------------
+
+   function Ghost_Assertion_Level_In_Effect (Id : Entity_Id) return Entity_Id
+   is
+   begin
+      if Ghost_Config.Is_Inside_Statement_Or_Pragma
+        and then Is_Implicit_Ghost (Id)
+      then
+         return Ghost_Config.Ghost_Mode_Assertion_Level;
+      else
+         return Ghost_Assertion_Level (Id);
+      end if;
+   end Ghost_Assertion_Level_In_Effect;
+
    ----------------------------
    -- Ghost_Policy_In_Effect --
    ----------------------------
@@ -1570,7 +1601,22 @@ package body Ghost is
       Level_Nam : constant Name_Id :=
         (if No (Level) then No_Name else Chars (Level));
    begin
-      return Policy_In_Effect (Name_Ghost, Level_Nam);
+      if Ghost_Config.Is_Inside_Statement_Or_Pragma
+        and then Is_Implicit_Ghost (Id)
+      then
+         case Ghost_Config.Ghost_Mode is
+            when Check =>
+               return Name_Check;
+
+            when Ignore =>
+               return Name_Ignore;
+
+            when None =>
+               return No_Name;
+         end case;
+      else
+         return Policy_In_Effect (Name_Ghost, Level_Nam);
+      end if;
    end Ghost_Policy_In_Effect;
 
    --------------------------------
@@ -1642,12 +1688,18 @@ package body Ghost is
       Ghost_Config.Current_Region := N;
       Ghost_Config.Ghost_Mode := Mode;
       Ghost_Config.Ghost_Mode_Assertion_Level := Level;
+
+      if Nkind (Ghost_Config.Current_Region)
+         in N_Statement_Other_Than_Procedure_Call
+          | N_Procedure_Call_Statement
+          | N_Pragma
+      then
+         Ghost_Config.Is_Inside_Statement_Or_Pragma := True;
+      end if;
    end Install_Ghost_Region;
 
    procedure Install_Ghost_Region
-     (Mode  : Name_Id;
-      N     : Node_Id;
-      Level : Entity_Id) is
+     (Mode : Name_Id; N : Node_Id; Level : Entity_Id) is
    begin
       Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N, Level);
    end Install_Ghost_Region;
@@ -1657,14 +1709,13 @@ package body Ghost is
    -------------------------
 
    function Is_Assertion_Level_Dependent
-     (Self : Entity_Id; Other : Entity_Id) return Boolean
-   is
+     (Self : Entity_Id; Other : Entity_Id) return Boolean is
    begin
       return
-         Self = Standard_Level_Default
-         or else Other = Standard_Level_Default
-         or else Is_Same_Or_Depends_On_Level (Self, Other)
-         or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static);
+        Self = Standard_Level_Default
+        or else Other = Standard_Level_Default
+        or else Is_Same_Or_Depends_On_Level (Self, Other)
+        or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static);
    end Is_Assertion_Level_Dependent;
 
    -------------------------
@@ -1977,10 +2028,7 @@ package body Ghost is
    -- Mark_And_Set_Ghost_Body --
    -----------------------------
 
-   procedure Mark_And_Set_Ghost_Body
-     (N       : Node_Id;
-      Spec_Id : Entity_Id)
-   is
+   procedure Mark_And_Set_Ghost_Body (N : Node_Id; Spec_Id : Entity_Id) is
       Body_Id : constant Entity_Id := Defining_Entity (N);
       Level   : Entity_Id := Empty;
       Policy  : Name_Id := No_Name;
@@ -1991,10 +2039,10 @@ package body Ghost is
       if Is_Subject_To_Ghost (N) then
          if Present (Spec_Id) then
             Policy := Ghost_Policy_In_Effect (Spec_Id);
-            Level  := Ghost_Assertion_Level (Spec_Id);
+            Level := Ghost_Assertion_Level_In_Effect (Spec_Id);
          else
             Policy := Ghost_Policy_In_Effect (Body_Id);
-            Level  := Ghost_Assertion_Level (Body_Id);
+            Level := Ghost_Assertion_Level_In_Effect (Body_Id);
          end if;
 
       --  A body declared within a Ghost region is automatically Ghost
@@ -2002,11 +2050,11 @@ package body Ghost is
 
       elsif Ghost_Config.Ghost_Mode = Check then
          Policy := Name_Check;
-         Level  := Ghost_Config.Ghost_Mode_Assertion_Level;
+         Level := Ghost_Config.Ghost_Mode_Assertion_Level;
 
       elsif Ghost_Config.Ghost_Mode = Ignore then
          Policy := Name_Ignore;
-         Level  := Ghost_Config.Ghost_Mode_Assertion_Level;
+         Level := Ghost_Config.Ghost_Mode_Assertion_Level;
 
       --  Inherit the "ghostness" of the previous declaration when the body
       --  acts as a completion.
@@ -2025,13 +2073,7 @@ package body Ghost is
       --  The Ghost policy in effect at the point of declaration and at the
       --  point of completion must match (SPARK RM 6.9(16)).
 
-      Check_Ghost_Completion
-        (Prev_Id  => Spec_Id,
-         Compl_Id => Body_Id);
-
-      if Present (Level) then
-         Set_Ghost_Assertion_Level (Body_Id, Level);
-      end if;
+      Check_Ghost_Completion (Prev_Id => Spec_Id, Compl_Id => Body_Id);
 
       --  Mark the body as its formals as Ghost
 
@@ -2441,16 +2483,15 @@ package body Ghost is
       end if;
    end Mark_Ghost_Pragma;
 
-   procedure Mark_Ghost_Pragma
-     (N    : Node_Id;
-      Mode : Ghost_Mode_Type)
-   is
+   procedure Mark_Ghost_Pragma (N : Node_Id; Mode : Ghost_Mode_Type) is
    begin
       if Mode = Check then
-         Set_Is_Checked_Ghost_Pragma (N);
+         Set_Is_Checked_Ghost_Pragma (N, True);
+         Set_Is_Ignored_Ghost_Pragma (N, False);
 
       else
-         Set_Is_Ignored_Ghost_Pragma (N);
+         Set_Is_Checked_Ghost_Pragma (N, False);
+         Set_Is_Ignored_Ghost_Pragma (N, True);
          Set_Is_Ignored_Ghost_Node (N);
          Record_Ignored_Ghost_Node (N);
       end if;
@@ -2460,10 +2501,7 @@ package body Ghost is
    -- Mark_Ghost_Renaming --
    -------------------------
 
-   procedure Mark_Ghost_Renaming
-     (N  : Node_Id;
-      Id : Entity_Id)
-   is
+   procedure Mark_Ghost_Renaming (N : Node_Id; Id : Entity_Id) is
       Policy : Name_Id := No_Name;
       Level  : constant Entity_Id := Ghost_Assertion_Level (Id);
    begin
@@ -2661,12 +2699,26 @@ package body Ghost is
 
       elsif Nkind (N) = N_Pragma then
          Level := Pragma_Ghost_Assertion_Level (N);
+
          if Is_Checked_Ghost_Pragma (N) then
-            Install_Ghost_Region (Check, N, Level);
+
+            --  Still install an ignored ghost region if the pragma is attached
+            --  to a checked ghost entity, but the pragma itself is explicitly
+            --  ignored.
+
+            if Is_Ignored (N) then
+               Install_Ghost_Region (Ignore, N, Level);
+            else
+               Install_Ghost_Region (Check, N, Level);
+            end if;
          elsif Is_Ignored_Ghost_Pragma (N) then
             Install_Ghost_Region (Ignore, N, Level);
          else
-            Install_Ghost_Region (None, N, Level);
+            if Is_Checked (N) then
+               Install_Ghost_Region (Check, N, Level);
+            else
+               Install_Ghost_Region (None, N, Level);
+            end if;
          end if;
 
       --  The Ghost mode of a procedure call depends on the Ghost mode of the

diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 109d28245de91f1f5aa2163a8d24777cdc436ff5..ea3390e2b482e80579dcde4cd08b6fce566ac50c 100644 (file)
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -767,6 +767,12 @@ package Opt is
 
       Current_Region : Node_Id := Empty;
       --  Latest ghost region
+
+      Is_Inside_Statement_Or_Pragma : Boolean := False;
+      --  A flag to tag whether we are currently in a region that originated
+      --  from a Statement or a pragma. Inside those regions the ghost policy
+      --  in effect for implicitly defined entities is not the policy for Ghost
+      --  but instead the policy for the region (SPARK RM 6.9 (3)).
    end record;
 
    Ghost_Config : Ghost_Config_Type;

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 00c9b17ff6ee94b2cbd91622f89d0f8c64543648..a17d9d2b81382038fb28127908f7a28cbb35f74b 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19428,6 +19428,7 @@ package body Sem_Prag is
             --  pragma Ghost (False).
 
             if Is_Ghost then
+               Set_Is_Implicit_Ghost (Id, False);
                Set_Is_Ghost_Entity (Id);
             end if;
          end Ghost;