diff mbox series

[Ada] Fix handling of ghost entity in predicate

Message ID 20170907094022.GA93697@adacore.com
State New
Headers show
Series [Ada] Fix handling of ghost entity in predicate | expand

Commit Message

Arnaud Charlet Sept. 7, 2017, 9:40 a.m. UTC
Ghost types are allowed to mention ghost entities in their predicate.
Because Ghost is propagated from type to the generated predicate function,
GNAT correctly identified valid from invalid cases, but this modification
simplifies the reason for correction.

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-09-07  Yannick Moy  <moy@adacore.com>

	* ghost.adb (Check_Ghost_Context): Do not err on ghost code inside
	predicate procedure. Check predicate pragma/aspect with Ghost entity.
	* exp_ch6.adb, par-ch6.adb, sem_ch13.adb, sem_prag.adb; Minor
	reformatting.
diff mbox series

Patch

Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 251835)
+++ exp_ch6.adb	(working copy)
@@ -137,7 +137,8 @@ 
    --  there are no tasks.
 
    function Caller_Known_Size
-     (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean;
+     (Func_Call   : Node_Id;
+      Result_Subt : Entity_Id) return Boolean;
    --  True if result subtype is definite, or has a size that does not require
    --  secondary stack usage (i.e. no variant part or components whose type
    --  depends on discriminants). In particular, untagged types with only
@@ -837,11 +838,14 @@ 
    -----------------------
 
    function Caller_Known_Size
-     (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean is
+     (Func_Call   : Node_Id;
+      Result_Subt : Entity_Id) return Boolean
+   is
    begin
-      return (Is_Definite_Subtype (Underlying_Type (Result_Subt))
-              and then No (Controlling_Argument (Func_Call)))
-          or else not Requires_Transient_Scope (Underlying_Type (Result_Subt));
+      return
+          (Is_Definite_Subtype (Underlying_Type (Result_Subt))
+            and then No (Controlling_Argument (Func_Call)))
+        or else not Requires_Transient_Scope (Underlying_Type (Result_Subt));
    end Caller_Known_Size;
 
    --------------------------------
@@ -8081,7 +8085,8 @@ 
 
       declare
          Definite : constant Boolean :=
-           Caller_Known_Size (Func_Call, Result_Subt);
+                      Caller_Known_Size (Func_Call, Result_Subt);
+
       begin
          --  Create an access type designating the function's result subtype.
          --  We use the type of the original call because it may be a call to
Index: ghost.adb
===================================================================
--- ghost.adb	(revision 251834)
+++ ghost.adb	(working copy)
@@ -281,6 +281,13 @@ 
                   if Chars (Subp_Id) = Name_uPostconditions then
                      return True;
 
+                  --  The context is the internally built predicate function,
+                  --  which is OK because the real check was done before the
+                  --  predicate function was generated.
+
+                  elsif Is_Predicate_Function (Subp_Id) then
+                     return True;
+
                   else
                      Subp_Decl :=
                        Original_Node (Unit_Declaration_Node (Subp_Id));
@@ -362,10 +369,12 @@ 
                   return True;
 
                --  An assertion expression pragma is Ghost when it contains a
-               --  reference to a Ghost entity (SPARK RM 6.9(10)).
+               --  reference to a Ghost entity (SPARK RM 6.9(10)), except for
+               --  predicate pragmas (SPARK RM 6.9(11)).
 
-               elsif Assertion_Expression_Pragma (Prag_Id) then
-
+               elsif Assertion_Expression_Pragma (Prag_Id)
+                 and then Prag_Id /= Pragma_Predicate
+               then
                   --  Ensure that the assertion policy and the Ghost policy are
                   --  compatible (SPARK RM 6.9(18)).
 
@@ -464,9 +473,16 @@ 
                   return True;
 
                --  A reference to a Ghost entity can appear within an aspect
-               --  specification (SPARK RM 6.9(10)).
+               --  specification (SPARK RM 6.9(10)). The precise checking will
+               --  occur when analyzing the corresponding pragma. We make an
+               --  exception for predicate aspects that only allow referencing
+               --  a Ghost entity when the corresponding type declaration is
+               --  Ghost (SPARK RM 6.9(11)).
 
-               elsif Nkind (Par) = N_Aspect_Specification then
+               elsif Nkind (Par) = N_Aspect_Specification
+                 and then not Same_Aspect
+                                (Get_Aspect_Id (Par), Aspect_Predicate)
+               then
                   return True;
 
                elsif Is_OK_Declaration (Par) then
Index: par-ch6.adb
===================================================================
--- par-ch6.adb	(revision 251835)
+++ par-ch6.adb	(working copy)
@@ -855,13 +855,14 @@ 
 
                   if Is_Non_Empty_List (Aspects) then
                      if Func then
-                        Error_Msg ("aspect specifications must come after "
-                          & "parenthesized expression",
-                            Sloc (First (Aspects)));
+                        Error_Msg
+                          ("aspect specifications must come after "
+                           & "parenthesized expression",
+                           Sloc (First (Aspects)));
                      else
-                        Error_Msg ("aspect specifications must come after "
-                          & "subprogram specification",
-                            Sloc (First (Aspects)));
+                        Error_Msg
+                          ("aspect specifications must come after subprogram "
+                           & "specification", Sloc (First (Aspects)));
                      end if;
                   end if;
 
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 251835)
+++ sem_ch13.adb	(working copy)
@@ -12649,7 +12649,6 @@ 
    --------------------------------
 
    procedure Resolve_Aspect_Expressions (E : Entity_Id) is
-
       function Resolve_Name (N : Node_Id) return Traverse_Result;
       --  Verify that all identifiers in the expression, with the exception
       --  of references to the current entity, denote visible entities. This
@@ -12668,6 +12667,7 @@ 
 
       function Resolve_Name (N : Node_Id) return Traverse_Result is
          Dummy : Traverse_Result;
+
       begin
          if Nkind (N) = N_Selected_Component then
             if Nkind (Prefix (N)) = N_Identifier
@@ -12700,6 +12700,8 @@ 
 
       procedure Resolve_Aspect_Expression is new Traverse_Proc (Resolve_Name);
 
+      --  Local variables
+
       ASN : Node_Id := First_Rep_Item (E);
 
    --  Start of processing for Resolve_Aspect_Expressions
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 251835)
+++ sem_prag.adb	(working copy)
@@ -1205,126 +1205,173 @@ 
             Item_Is_Output : out Boolean)
          is
          begin
-            Item_Is_Input  := False;
-            Item_Is_Output := False;
+            case Ekind (Item_Id) is
 
-            --  Abstract states
+               --  Abstract states
 
-            if Ekind (Item_Id) = E_Abstract_State then
+               when E_Abstract_State =>
 
-               --  When pragma Global is present, the mode of the state may be
-               --  further constrained by setting a more restrictive mode.
+                  --  When pragma Global is present it determines the mode of
+                  --  the abstract state.
 
-               if Global_Seen then
-                  if Appears_In (Subp_Inputs, Item_Id) then
-                     Item_Is_Input := True;
-                  end if;
+                  if Global_Seen then
+                     Item_Is_Input  := Appears_In (Subp_Inputs, Item_Id);
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
 
-                  if Appears_In (Subp_Outputs, Item_Id) then
+                  --  Otherwise the state has a default IN OUT mode, because it
+                  --  behaves as a variable.
+
+                  else
+                     Item_Is_Input  := True;
                      Item_Is_Output := True;
                   end if;
 
-               --  Otherwise the state has a default IN OUT mode
+               --  Constants and IN parameters
 
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
+               when E_Constant
+                  | E_Generic_In_Parameter
+                  | E_In_Parameter
+                  | E_Loop_Parameter
+               =>
+                  --  When pragma Global is present it determines the mode
+                  --  of constant objects as inputs (and such objects cannot
+                  --  appear as outputs in the Global contract).
 
-            --  Constants
+                  if Global_Seen then
+                     Item_Is_Input := Appears_In (Subp_Inputs, Item_Id);
+                  else
+                     Item_Is_Input := True;
+                  end if;
 
-            elsif Ekind_In (Item_Id, E_Constant,
-                                     E_Loop_Parameter)
-            then
-               Item_Is_Input := True;
+                  Item_Is_Output := False;
 
-            --  Parameters
+               --  Variables and IN OUT parameters
 
-            elsif Ekind_In (Item_Id, E_Generic_In_Parameter,
-                                     E_In_Parameter)
-            then
-               Item_Is_Input := True;
+               when E_Generic_In_Out_Parameter
+                  | E_In_Out_Parameter
+                  | E_Variable
+               =>
+                  --  When pragma Global is present it determines the mode of
+                  --  the object.
 
-            elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
-                                     E_In_Out_Parameter)
-            then
-               Item_Is_Input  := True;
-               Item_Is_Output := True;
+                  if Global_Seen then
 
-            elsif Ekind (Item_Id) = E_Out_Parameter then
-               if Scope (Item_Id) = Spec_Id then
+                     --  A variable has mode IN when its type is unconstrained
+                     --  or tagged because array bounds, discriminants or tags
+                     --  can be read.
 
-                  --  An OUT parameter of the related subprogram has mode IN
-                  --  if its type is unconstrained or tagged because array
-                  --  bounds, discriminants or tags can be read.
+                     Item_Is_Input :=
+                       Appears_In (Subp_Inputs, Item_Id)
+                         or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
 
-                  if Is_Unconstrained_Or_Tagged_Item (Item_Id) then
-                     Item_Is_Input := True;
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+                  --  Otherwise the variable has a default IN OUT mode
+
+                  else
+                     Item_Is_Input  := True;
+                     Item_Is_Output := True;
                   end if;
 
-                  Item_Is_Output := True;
+               when E_Out_Parameter =>
 
-               --  An OUT parameter of an enclosing subprogram behaves as a
-               --  read-write variable in which case the mode is IN OUT.
+                  --  An OUT parameter of the related subprogram; it cannot
+                  --  appear in Global.
 
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
+                  if Scope (Item_Id) = Spec_Id then
 
-            --  Protected types
+                     --  The parameter has mode IN if its type is unconstrained
+                     --  or tagged because array bounds, discriminants or tags
+                     --  can be read.
 
-            elsif Ekind (Item_Id) = E_Protected_Type then
+                     Item_Is_Input :=
+                       Is_Unconstrained_Or_Tagged_Item (Item_Id);
 
-               --  A protected type acts as a formal parameter of mode IN when
-               --  it applies to a protected function.
+                     Item_Is_Output := True;
 
-               if Ekind (Spec_Id) = E_Function then
-                  Item_Is_Input := True;
+                  --  An OUT parameter of an enclosing subprogram; it can
+                  --  appear in Global and behaves as a read-write variable.
 
-               --  Otherwise the protected type acts as a formal of mode IN OUT
+                  else
+                     --  When pragma Global is present it determines the mode
+                     --  of the object.
 
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
+                     if Global_Seen then
 
-            --  Task types
+                        --  A variable has mode IN when its type is
+                        --  unconstrained or tagged because array
+                        --  bounds, discriminants or tags can be read.
 
-            elsif Ekind (Item_Id) = E_Task_Type then
-               Item_Is_Input  := True;
-               Item_Is_Output := True;
+                        Item_Is_Input :=
+                          Appears_In (Subp_Inputs, Item_Id)
+                            or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
 
-            --  Variable case
+                        Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
 
-            else pragma Assert (Ekind (Item_Id) = E_Variable);
+                     --  Otherwise the variable has a default IN OUT mode
 
-               --  When pragma Global is present, the mode of the variable may
-               --  be further constrained by setting a more restrictive mode.
+                     else
+                        Item_Is_Input  := True;
+                        Item_Is_Output := True;
+                     end if;
+                  end if;
 
-               if Global_Seen then
+               --  Protected types
 
-                  --  A variable has mode IN when its type is unconstrained or
-                  --  tagged because array bounds, discriminants or tags can be
-                  --  read.
+               when E_Protected_Type =>
+                  if Global_Seen then
 
-                  if Appears_In (Subp_Inputs, Item_Id)
-                    or else Is_Unconstrained_Or_Tagged_Item (Item_Id)
-                  then
-                     Item_Is_Input := True;
+                     --  A variable has mode IN when its type is unconstrained
+                     --  or tagged because array bounds, discriminants or tags
+                     --  can be read.
+
+                     Item_Is_Input :=
+                       Appears_In (Subp_Inputs, Item_Id)
+                         or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
+
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+                  else
+                     --  A protected type acts as a formal parameter of mode IN
+                     --  when it applies to a protected function.
+
+                     if Ekind (Spec_Id) = E_Function then
+                        Item_Is_Input  := True;
+                        Item_Is_Output := False;
+
+                     --  Otherwise the protected type acts as a formal of mode
+                     --  IN OUT.
+
+                     else
+                        Item_Is_Input  := True;
+                        Item_Is_Output := True;
+                     end if;
                   end if;
 
-                  if Appears_In (Subp_Outputs, Item_Id) then
+               --  Task types
+
+               when E_Task_Type =>
+
+                  --  When pragma Global is present it determines the mode of
+                  --  the object.
+
+                  if Global_Seen then
+                     Item_Is_Input :=
+                       Appears_In (Subp_Inputs, Item_Id)
+                         or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
+
+                     Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+                  --  Otherwise task types act as IN OUT parameters
+
+                  else
+                     Item_Is_Input  := True;
                      Item_Is_Output := True;
                   end if;
 
-               --  Otherwise the variable has a default IN OUT mode
-
-               else
-                  Item_Is_Input  := True;
-                  Item_Is_Output := True;
-               end if;
-            end if;
+               when others =>
+                  raise Program_Error;
+            end case;
          end Find_Role;
 
          ----------------
@@ -5069,7 +5116,7 @@ 
                --  pragma is inserted in its declarative part.
 
                elsif From_Aspect_Specification (N)
-                 and then  Ent = Current_Scope
+                 and then Ent = Current_Scope
                  and then
                    Nkind (Unit_Declaration_Node (Ent)) = N_Subprogram_Body
                then
@@ -28300,7 +28347,7 @@ 
          if Nkind (Clause) = N_Null then
             null;
 
-         --  A dependency cause appears as component association
+         --  A dependency clause appears as component association
 
          elsif Nkind (Clause) = N_Component_Association then
             Collect_Dependency_Item
@@ -28424,21 +28471,15 @@ 
          Subp_Decl := Unit_Declaration_Node (Subp_Id);
          Spec_Id   := Unique_Defining_Entity (Subp_Decl);
 
-         --  Process all [generic] formal parameters
+         --  Process all formal parameters
 
          Formal := First_Entity (Spec_Id);
          while Present (Formal) loop
-            if Ekind_In (Formal, E_Generic_In_Parameter,
-                                 E_In_Out_Parameter,
-                                 E_In_Parameter)
-            then
+            if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
                Append_New_Elmt (Formal, Subp_Inputs);
             end if;
 
-            if Ekind_In (Formal, E_Generic_In_Out_Parameter,
-                                 E_In_Out_Parameter,
-                                 E_Out_Parameter)
-            then
+            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
                Append_New_Elmt (Formal, Subp_Outputs);
 
                --  Out parameters can act as inputs when the related type is