[Ada] Expose part of ownership checking for use in GNATprove

GNATprove needs to be able to call a subset of the ownership legality
rules from marking. This is provided by a new function
Sem_SPARK.Is_Legal.

There is no impact on compilation.

2019-08-14  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed
	for use in GNATprove, to test legality rules not related to
	permissions.
	(Check_Declaration_Legality): Extract the part of
	Check_Declaration that checks rules not related to permissions.
	(Check_Declaration): Call the new Check_Declaration_Legality.
	(Check_Type_Legality): Rename of Check_Type. Introduce
	parameters to force or not checking, and update a flag detecting
	illegalities.
	(Check_Node): Ignore attribute references in statement position.

From-SVN: r274454

3 files changed, 198 insertions, 33 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cef5e8c..1d13947 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,18 @@
 2019-08-14  Yannick Moy  <moy@adacore.com>
 
+	* sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed
+	for use in GNATprove, to test legality rules not related to
+	permissions.
+	(Check_Declaration_Legality): Extract the part of
+	Check_Declaration that checks rules not related to permissions.
+	(Check_Declaration): Call the new Check_Declaration_Legality.
+	(Check_Type_Legality): Rename of Check_Type. Introduce
+	parameters to force or not checking, and update a flag detecting
+	illegalities.
+	(Check_Node): Ignore attribute references in statement position.
+
+2019-08-14  Yannick Moy  <moy@adacore.com>
+
 	* sem_spark.adb (Check_Old_Loop_Entry): New procedure to check
 	correct use of Old  and Loop_Entry.
 	(Check_Node): Check subprogram contracts.
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 37c6b4d..b0686b7 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -637,6 +637,14 @@ package body Sem_SPARK is
 
    procedure Check_Declaration (Decl : Node_Id);
 
+   procedure Check_Declaration_Legality
+     (Decl  : Node_Id;
+      Force : Boolean;
+      Legal : in out Boolean);
+   --  Check the legality of declaration Decl regarding rules not related to
+   --  permissions. Update Legal to False if a rule is violated. Issue an
+   --  error message if Force is True and Emit_Messages returns True.
+
    procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
    pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
                                         N_Range_Constraint,
@@ -686,7 +694,10 @@ package body Sem_SPARK is
 
    procedure Check_Statement (Stmt : Node_Id);
 
-   procedure Check_Type (Typ : Entity_Id);
+   procedure Check_Type_Legality
+     (Typ   : Entity_Id;
+      Force : Boolean;
+      Legal : in out Boolean);
    --  Check that type Typ is either not deep, or that it is an observing or
    --  owning type according to SPARK RM 3.10
 
@@ -1138,11 +1149,12 @@ package body Sem_SPARK is
       Expr_Root   : Entity_Id;
       Perm        : Perm_Kind;
       Status      : Error_Status;
+      Dummy       : Boolean := True;
 
    --  Start of processing for Check_Assignment
 
    begin
-      Check_Type (Target_Typ);
+      Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
 
       if Is_Anonymous_Access_Type (Target_Typ) then
          Check_Source_Of_Borrow_Or_Observe (Expr, Status);
@@ -1410,11 +1422,18 @@ package body Sem_SPARK is
       Target     : constant Entity_Id := Defining_Identifier (Decl);
       Target_Typ : constant Node_Id := Etype (Target);
       Expr       : Node_Id;
+      Dummy      : Boolean := True;
 
    begin
+      --  Start with legality rules not related to permissions
+
+      Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
+
+      --  Now check permission-related legality rules
+
       case N_Declaration'(Nkind (Decl)) is
          when N_Full_Type_Declaration =>
-            Check_Type (Target);
+            null;
 
             --  ??? What about component declarations with defaults.
 
@@ -1424,7 +1443,105 @@ package body Sem_SPARK is
          when N_Object_Declaration =>
             Expr := Expression (Decl);
 
-            Check_Type (Target_Typ);
+            if Present (Expr) then
+               Check_Assignment (Target => Target,
+                                 Expr   => Expr);
+            end if;
+
+            if Is_Deep (Target_Typ) then
+               declare
+                  Tree : constant Perm_Tree_Access :=
+                    new Perm_Tree_Wrapper'
+                      (Tree =>
+                         (Kind                => Entire_Object,
+                          Is_Node_Deep        => True,
+                          Explanation         => Decl,
+                          Permission          => Read_Write,
+                          Children_Permission => Read_Write));
+               begin
+                  Set (Current_Perm_Env, Target, Tree);
+               end;
+            end if;
+
+         when N_Iterator_Specification =>
+            null;
+
+         when N_Loop_Parameter_Specification =>
+            null;
+
+         --  Checking should not be called directly on these nodes
+
+         when N_Function_Specification
+            | N_Entry_Declaration
+            | N_Procedure_Specification
+            | N_Component_Declaration
+         =>
+            raise Program_Error;
+
+         --  Ignored constructs for pointer checking
+
+         when N_Formal_Object_Declaration
+            | N_Formal_Type_Declaration
+            | N_Incomplete_Type_Declaration
+            | N_Private_Extension_Declaration
+            | N_Private_Type_Declaration
+            | N_Protected_Type_Declaration
+         =>
+            null;
+
+         --  The following nodes are rewritten by semantic analysis
+
+         when N_Expression_Function =>
+            raise Program_Error;
+      end case;
+   end Check_Declaration;
+
+   --------------------------------
+   -- Check_Declaration_Legality --
+   --------------------------------
+
+   procedure Check_Declaration_Legality
+     (Decl  : Node_Id;
+      Force : Boolean;
+      Legal : in out Boolean)
+   is
+      function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+      function Emit_Messages return Boolean;
+      --  Local wrapper around generic formal parameter Emit_Messages, to
+      --  check the value of parameter Force before calling the original
+      --  Emit_Messages, and setting Legal to False.
+
+      -------------------
+      -- Emit_Messages --
+      -------------------
+
+      function Emit_Messages return Boolean is
+      begin
+         Legal := False;
+         return Force and then Original_Emit_Messages;
+      end Emit_Messages;
+
+      --  Local variables
+
+      Target     : constant Entity_Id := Defining_Identifier (Decl);
+      Target_Typ : constant Node_Id := Etype (Target);
+      Expr       : Node_Id;
+
+   --  Start of processing for Check_Declaration_Legality
+
+   begin
+      case N_Declaration'(Nkind (Decl)) is
+         when N_Full_Type_Declaration =>
+            Check_Type_Legality (Target, Force, Legal);
+
+         when N_Subtype_Declaration =>
+            null;
+
+         when N_Object_Declaration =>
+            Expr := Expression (Decl);
+
+            Check_Type_Legality (Target_Typ, Force, Legal);
 
             --  A declaration of a stand-alone object of an anonymous access
             --  type shall have an explicit initial value and shall occur
@@ -1453,26 +1570,6 @@ package body Sem_SPARK is
                end if;
             end if;
 
-            if Present (Expr) then
-               Check_Assignment (Target => Target,
-                                 Expr   => Expr);
-            end if;
-
-            if Is_Deep (Target_Typ) then
-               declare
-                  Tree : constant Perm_Tree_Access :=
-                    new Perm_Tree_Wrapper'
-                      (Tree =>
-                         (Kind                => Entire_Object,
-                          Is_Node_Deep        => True,
-                          Explanation         => Decl,
-                          Permission          => Read_Write,
-                          Children_Permission => Read_Write));
-               begin
-                  Set (Current_Perm_Env, Target, Tree);
-               end;
-            end if;
-
          when N_Iterator_Specification =>
             null;
 
@@ -1504,7 +1601,7 @@ package body Sem_SPARK is
          when N_Expression_Function =>
             raise Program_Error;
       end case;
-   end Check_Declaration;
+   end Check_Declaration_Legality;
 
    ----------------------
    -- Check_Expression --
@@ -2668,6 +2765,12 @@ package body Sem_SPARK is
          when N_Subprogram_Declaration =>
             Check_Subprogram_Contract (N);
 
+         --  Attribute references in statement position are not supported in
+         --  SPARK and will be rejected by GNATprove.
+
+         when N_Attribute_Reference =>
+            null;
+
          --  Ignored constructs for pointer checking
 
          when N_Abstract_Subprogram_Declaration
@@ -3503,13 +3606,38 @@ package body Sem_SPARK is
       end case;
    end Check_Statement;
 
-   ----------------
-   -- Check_Type --
-   ----------------
+   -------------------------
+   -- Check_Type_Legality --
+   -------------------------
+
+   procedure Check_Type_Legality
+     (Typ   : Entity_Id;
+      Force : Boolean;
+      Legal : in out Boolean)
+   is
+      function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+      function Emit_Messages return Boolean;
+      --  Local wrapper around generic formal parameter Emit_Messages, to
+      --  check the value of parameter Force before calling the original
+      --  Emit_Messages, and setting Legal to False.
+
+      -------------------
+      -- Emit_Messages --
+      -------------------
+
+      function Emit_Messages return Boolean is
+      begin
+         Legal := False;
+         return Force and then Original_Emit_Messages;
+      end Emit_Messages;
+
+      --  Local variables
 
-   procedure Check_Type (Typ : Entity_Id) is
       Check_Typ : constant Entity_Id := Retysp (Typ);
 
+   --  Start of processing for Check_Type_Legality
+
    begin
       case Type_Kind'(Ekind (Check_Typ)) is
          when Access_Kind =>
@@ -3519,7 +3647,7 @@ package body Sem_SPARK is
                =>
                   null;
                when E_Access_Subtype =>
-                  Check_Type (Base_Type (Check_Typ));
+                  Check_Type_Legality (Base_Type (Check_Typ), Force, Legal);
                when E_Access_Attribute_Type =>
                   if Emit_Messages then
                      Error_Msg_N ("access attribute not allowed in SPARK",
@@ -3546,7 +3674,7 @@ package body Sem_SPARK is
          when E_Array_Type
             | E_Array_Subtype
          =>
-            Check_Type (Component_Type (Check_Typ));
+            Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
 
          when Record_Kind =>
             if Is_Deep (Check_Typ)
@@ -3569,7 +3697,7 @@ package body Sem_SPARK is
                      --  Ignore components which are not visible in SPARK
 
                      if Component_Is_Visible_In_SPARK (Comp) then
-                        Check_Type (Etype (Comp));
+                        Check_Type_Legality (Etype (Comp), Force, Legal);
                      end if;
                      Next_Component_Or_Discriminant (Comp);
                   end loop;
@@ -3595,7 +3723,7 @@ package body Sem_SPARK is
          =>
             null;
       end case;
-   end Check_Type;
+   end Check_Type_Legality;
 
    --------------
    -- Get_Expl --
@@ -4141,6 +4269,24 @@ package body Sem_SPARK is
       end case;
    end Is_Deep;
 
+   --------------
+   -- Is_Legal --
+   --------------
+
+   function Is_Legal (N : Node_Id) return Boolean is
+      Legal : Boolean := True;
+
+   begin
+      case Nkind (N) is
+         when N_Declaration =>
+            Check_Declaration_Legality (N, Force => False, Legal => Legal);
+         when others =>
+            null;
+      end case;
+
+      return Legal;
+   end Is_Legal;
+
    ----------------------
    -- Is_Local_Context --
    ----------------------
diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads
index 195e833..7c16281 100644
--- a/gcc/ada/sem_spark.ads
+++ b/gcc/ada/sem_spark.ads
@@ -152,6 +152,12 @@ generic
 
 package Sem_SPARK is
 
+   function Is_Legal (N : Node_Id) return Boolean;
+   --  Test the legality of a node wrt ownership-checking rules. This does not
+   --  check rules related to the validity of permissions associated with paths
+   --  from objects, so that it can be called from GNATprove on code of library
+   --  units analyzed in SPARK_Mode Auto.
+
    procedure Check_Safe_Pointers (N : Node_Id);
    --  The entry point of this package. It analyzes a node and reports errors
    --  when there are violations of ownership rules.