public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-4515] ada: Allow No_Caching on volatile types
@ 2022-12-06 14:01 Marc Poulhi?s
  0 siblings, 0 replies; only message in thread
From: Marc Poulhi?s @ 2022-12-06 14:01 UTC (permalink / raw)
  To: gcc-cvs

https://gcc.gnu.org/g:400d9fc1f04336118c3200e2af14a620e7ea1d95

commit r13-4515-g400d9fc1f04336118c3200e2af14a620e7ea1d95
Author: Yannick Moy <moy@adacore.com>
Date:   Fri Nov 25 17:16:06 2022 +0100

    ada: Allow No_Caching on volatile types
    
    SPARK RM now allow the property No_Caching on volatile types, to
    indicate that they should be considered volatile for compilation, but
    not by GNATprove's analysis.
    
    gcc/ada/
    
            * contracts.adb (Add_Contract_Item): Allow No_Caching on types.
            (Check_Type_Or_Object_External_Properties): Check No_Caching.
            Check that non-effectively volatile types does not contain an
            effectively volatile component (instead of just a volatile
            component).
            (Analyze_Object_Contract): Remove shared checking of No_Caching.
            * sem_prag.adb (Analyze_External_Property_In_Decl_Part): Adapt checking
            of No_Caching for types.
            (Analyze_Pragma): Allow No_Caching on types.
            * sem_util.adb (Has_Effectively_Volatile_Component): New query function.
            (Is_Effectively_Volatile): Type with Volatile and No_Caching is not
            effectively volatile.
            (No_Caching_Enabled): Remove assertion to apply to all entities.
            * sem_util.ads: Same.

Diff:
---
 gcc/ada/contracts.adb | 32 ++++++++++++++++----------------
 gcc/ada/sem_prag.adb  | 49 ++++++++++++++++++++++++++-----------------------
 gcc/ada/sem_util.adb  | 37 ++++++++++++++++++++++++++++++++++---
 gcc/ada/sem_util.ads  | 11 ++++++++---
 4 files changed, 84 insertions(+), 45 deletions(-)

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 6f474eb2944..59121ca9ea2 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -316,6 +316,7 @@ package body Contracts is
                         | Name_Async_Writers
                         | Name_Effective_Reads
                         | Name_Effective_Writes
+                        | Name_No_Caching
               or else (Ekind (Id) = E_Task_Type
                          and Prag_Nam in Name_Part_Of
                                        | Name_Depends
@@ -859,6 +860,7 @@ package body Contracts is
       AW_Val  : Boolean := False;
       ER_Val  : Boolean := False;
       EW_Val  : Boolean := False;
+      NC_Val  : Boolean;
       Seen    : Boolean := False;
       Prag    : Node_Id;
       Obj_Typ : Entity_Id;
@@ -956,18 +958,25 @@ package body Contracts is
       end if;
 
       --  Verify the mutual interaction of the various external properties.
-      --  For variables for which No_Caching is enabled, it has been checked
-      --  already that only False values for other external properties are
-      --  allowed.
+      --  For types and variables for which No_Caching is enabled, it has been
+      --  checked already that only False values for other external properties
+      --  are allowed.
 
       if Seen
-        and then (Ekind (Type_Or_Obj_Id) /= E_Variable
-                   or else not No_Caching_Enabled (Type_Or_Obj_Id))
+        and then not No_Caching_Enabled (Type_Or_Obj_Id)
       then
          Check_External_Properties
            (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
       end if;
 
+      --  Analyze the non-external volatility property No_Caching
+
+      Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching);
+
+      if Present (Prag) then
+         Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
+      end if;
+
       --  The following checks are relevant only when SPARK_Mode is on, as
       --  they are not standard Ada legality rules. Internally generated
       --  temporaries are ignored, as well as return objects.
@@ -1047,10 +1056,10 @@ package body Contracts is
 
             if Is_Type_Id
               and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
-              and then Has_Volatile_Component (Type_Or_Obj_Id)
+              and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id)
             then
                Error_Msg_N
-                 ("non-volatile type & cannot have volatile"
+                 ("non-volatile type & cannot have effectively volatile"
                     & " components",
                   Type_Or_Obj_Id);
             end if;
@@ -1076,7 +1085,6 @@ package body Contracts is
       Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
       --  Save the SPARK_Mode-related data to restore on exit
 
-      NC_Val   : Boolean;
       Items    : Node_Id;
       Prag     : Node_Id;
       Ref_Elmt : Elmt_Id;
@@ -1118,14 +1126,6 @@ package body Contracts is
 
       Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id);
 
-      --  Analyze the non-external volatility property No_Caching
-
-      Prag := Get_Pragma (Obj_Id, Pragma_No_Caching);
-
-      if Present (Prag) then
-         Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
-      end if;
-
       --  Constant-related checks
 
       if Ekind (Obj_Id) = E_Constant then
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 27bd879903e..f3c23caeae4 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2116,9 +2116,16 @@ package body Sem_Prag is
                    First (Pragma_Argument_Associations (N));
       Obj_Decl : constant Node_Id   := Find_Related_Context (N);
       Obj_Id   : constant Entity_Id := Defining_Entity (Obj_Decl);
+      Obj_Typ  : Entity_Id;
       Expr     : Node_Id;
 
    begin
+      if Is_Type (Obj_Id) then
+         Obj_Typ := Obj_Id;
+      else
+         Obj_Typ := Etype (Obj_Id);
+      end if;
+
       --  Ensure that the Boolean expression (if present) is static. A missing
       --  argument defaults the value to True (SPARK RM 7.1.2(5)).
 
@@ -2153,9 +2160,7 @@ package body Sem_Prag is
       if Prag_Id /= Pragma_No_Caching
         and then not Is_Effectively_Volatile (Obj_Id)
       then
-         if Ekind (Obj_Id) = E_Variable
-           and then No_Caching_Enabled (Obj_Id)
-         then
+         if No_Caching_Enabled (Obj_Id) then
             if Expr_Val then  --  Confirming value of False is allowed
                SPARK_Msg_N
                  ("illegal combination of external property % and property "
@@ -2167,15 +2172,16 @@ package body Sem_Prag is
                N);
          end if;
 
-      --  Pragma No_Caching should only apply to volatile variables of
+      --  Pragma No_Caching should only apply to volatile types or variables of
       --  a non-effectively volatile type (SPARK RM 7.1.2).
 
       elsif Prag_Id = Pragma_No_Caching then
-         if Is_Effectively_Volatile (Etype (Obj_Id)) then
-            SPARK_Msg_N ("property % must not apply to an object of "
+         if Is_Effectively_Volatile (Obj_Typ) then
+            SPARK_Msg_N ("property % must not apply to a type or object of "
                          & "an effectively volatile type", N);
          elsif not Is_Volatile (Obj_Id) then
-            SPARK_Msg_N ("property % must apply to a volatile object", N);
+            SPARK_Msg_N
+              ("property % must apply to a volatile type or object", N);
          end if;
       end if;
 
@@ -13484,22 +13490,19 @@ package body Sem_Prag is
             Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
 
             --  Pragma must apply to a object declaration or to a type
-            --  declaration (only the former in the No_Caching case).
-            --  Original_Node is necessary to account for untagged derived
-            --  types that are rewritten as subtypes of their
-            --  respective root types.
-
-            if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
-               if Prag_Id = Pragma_No_Caching
-                  or else Nkind (Original_Node (Obj_Or_Type_Decl)) not in
-                            N_Full_Type_Declaration    |
-                            N_Private_Type_Declaration |
-                            N_Formal_Type_Declaration  |
-                            N_Task_Type_Declaration    |
-                            N_Protected_Type_Declaration
-               then
-                  Pragma_Misplaced;
-               end if;
+            --  declaration. Original_Node is necessary to account for
+            --  untagged derived types that are rewritten as subtypes of
+            --  their respective root types.
+
+            if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration
+              and then Nkind (Original_Node (Obj_Or_Type_Decl)) not in
+                N_Full_Type_Declaration    |
+                N_Private_Type_Declaration |
+                N_Formal_Type_Declaration  |
+                N_Task_Type_Declaration    |
+                N_Protected_Type_Declaration
+            then
+               Pragma_Misplaced;
             end if;
 
             Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 1fef8475c05..a1cebb08291 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -13530,6 +13530,36 @@ package body Sem_Util is
       return Has_Undef_Ref;
    end Has_Undefined_Reference;
 
+   ----------------------------------------
+   -- Has_Effectively_Volatile_Component --
+   ----------------------------------------
+
+   function Has_Effectively_Volatile_Component
+     (Typ : Entity_Id) return Boolean
+   is
+      Comp : Entity_Id;
+
+   begin
+      if Has_Volatile_Components (Typ) then
+         return True;
+
+      elsif Is_Array_Type (Typ) then
+         return Is_Effectively_Volatile (Component_Type (Typ));
+
+      elsif Is_Record_Type (Typ) then
+         Comp := First_Component (Typ);
+         while Present (Comp) loop
+            if Is_Effectively_Volatile (Etype (Comp)) then
+               return True;
+            end if;
+
+            Next_Component (Comp);
+         end loop;
+      end if;
+
+      return False;
+   end Has_Effectively_Volatile_Component;
+
    ----------------------------
    -- Has_Volatile_Component --
    ----------------------------
@@ -16663,9 +16693,11 @@ package body Sem_Util is
       if Is_Type (Id) then
 
          --  An arbitrary type is effectively volatile when it is subject to
-         --  pragma Atomic or Volatile.
+         --  pragma Atomic or Volatile, unless No_Caching is enabled.
 
-         if Is_Volatile (Id) then
+         if Is_Volatile (Id)
+           and then not No_Caching_Enabled (Id)
+         then
             return True;
 
          --  An array type is effectively volatile when it is subject to pragma
@@ -24579,7 +24611,6 @@ package body Sem_Util is
    ------------------------
 
    function No_Caching_Enabled (Id : Entity_Id) return Boolean is
-      pragma Assert (Ekind (Id) = E_Variable);
       Prag : constant Node_Id := Get_Pragma (Id, Pragma_No_Caching);
       Arg1 : Node_Id;
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 34aaa9a932f..b647e68ff7f 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1564,6 +1564,11 @@ package Sem_Util is
    --  Given arbitrary expression Expr, determine whether it contains at
    --  least one name whose entity is Any_Id.
 
+   function Has_Effectively_Volatile_Component
+     (Typ : Entity_Id) return Boolean;
+   --  Given arbitrary type Typ, determine whether it contains at least one
+   --  effectively volatile component.
+
    function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
    --  Given arbitrary type Typ, determine whether it contains at least one
    --  volatile component.
@@ -2758,9 +2763,9 @@ package Sem_Util is
    --  inline this procedural form, but not the functional form above.
 
    function No_Caching_Enabled (Id : Entity_Id) return Boolean;
-   --  Given the entity of a variable, determine whether Id is subject to
-   --  volatility property No_Caching and if it is, the related expression
-   --  evaluates to True.
+   --  Given any entity Id, determine whether Id is subject to volatility
+   --  property No_Caching and if it is, the related expression evaluates
+   --  to True.
 
    function No_Heap_Finalization (Typ : Entity_Id) return Boolean;
    --  Determine whether type Typ is subject to pragma No_Heap_Finalization

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2022-12-06 14:01 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-12-06 14:01 [gcc r13-4515] ada: Allow No_Caching on volatile types Marc Poulhi?s

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).